I1_prop_1

lemma I1_prop_1 {k : ℤ} (hk : -S ≤ k) {x : X} {y1 y2 : Yk X k} :      x ∈ I1 hk y1 ∩ I1 hk y2 → y1 = y2 := by    rw [I1,I1]    by_cases hk_s : k = -S    · rw [dif_pos hk_s,dif_pos hk_s]      subst hk_s      intro hx      ext      rw [(Yk_pairwise (-S)).elim (y1.property) (y2.property)]      rw [not_disjoint_iff]      exact ⟨x, hx⟩    · have : -S ≤ k - 1 := I_induction_proof hk hk_s      have : ((2 * (S + (k - 1))).toNat : ℤ) + 1 < 2 * (S + k) := by        rw [Int.toNat_of_nonneg (by linarith)]        linarith      rw [dif_neg hk_s, dif_neg hk_s]      intro hx      push _ ∈ _ at hx      obtain ⟨⟨z1, hz1, hz1'⟩, ⟨z2, hz2, hz2'⟩⟩ := hx      have hz_eq : z1 = z2 := I3_prop_1 (I_induction_proof hk hk_s) ⟨hz1', hz2'⟩      subst hz_eq      ext      apply (Yk_pairwise k).elim (y1.property) (y2.property)      rw [not_disjoint_iff]      use z1