I3_prop_1

lemma I3_prop_1 {k:ℤ} (hk : -S ≤ k) {x : X} {y1 y2 : Yk X k} :      x ∈ I3 hk y1 ∩ I3 hk y2 → y1 = y2 := by    intro hx    have hx' := hx    rw [I3,I3] at hx    obtain ⟨hl,hr⟩ := hx'    push _ ∈ _ at hx    simp only [not_or, not_exists] at hx    by_cases hx_mem_Xk : x ∈ Xk hk    · rw [not_iff_false_intro hx_mem_Xk] at hx      simp_rw [false_and,and_false,or_false] at hx      exact I1_prop_1 hk hx    have hx_notMem_i1 (y' : Yk X k): x ∉ I1 hk y' := by      simp only [Xk, mem_iUnion, not_exists] at hx_mem_Xk      exact hx_mem_Xk _    rw [iff_false_intro (hx_notMem_i1 y1), iff_false_intro (hx_notMem_i1 y2)] at hx    rw [false_or,false_or,iff_true_intro hx_mem_Xk,true_and,true_and] at hx    apply Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt    · exact fun h ↦ hx.right.right y1 h hl    exact fun h ↦ hx.left.right y2 h hr