Complex.isPathConnected_halfSpace_re_gt_diff_singleton

theorem isPathConnected_halfSpace_re_gt_diff_singleton (a : ℝ) (p : ℂ) (hp : a < p.re) :    IsPathConnected ({z : ℂ | a < z.re} \ ({p} : Set ℂ)) := by  classical  let S1 : Set ℂ := {z : ℂ | a < z.re ∧ z.im < p.im}  let S2 : Set ℂ := {z : ℂ | a < z.re ∧ z.re < p.re}  let S3 : Set ℂ := {z : ℂ | a < z.re ∧ p.im < z.im}  let S4 : Set ℂ := {z : ℂ | p.re < z.re}  have hS1conv : Convex ℝ S1 := by    have h1 : Convex ℝ {z : ℂ | a < z.re} := convex_halfSpace_re_gt (r := a)    have h2 : Convex ℝ {z : ℂ | z.im < p.im} := convex_halfSpace_im_lt (r := p.im)    simpa [S1, Set.setOf_and] using h1.inter h2  have hS2conv : Convex ℝ S2 := by    have h1 : Convex ℝ {z : ℂ | a < z.re} := convex_halfSpace_re_gt (r := a)    have h2 : Convex ℝ {z : ℂ | z.re < p.re} := convex_halfSpace_re_lt (r := p.re)    simpa [S2, Set.setOf_and] using h1.inter h2  have hS3conv : Convex ℝ S3 := by    have h1 : Convex ℝ {z : ℂ | a < z.re} := convex_halfSpace_re_gt (r := a)    have h2 : Convex ℝ {z : ℂ | p.im < z.im} := convex_halfSpace_im_gt (r := p.im)    simpa [S3, Set.setOf_and] using h1.inter h2  have hS4conv : Convex ℝ S4 := by    simpa [S4] using (convex_halfSpace_re_gt (r := p.re))  have hS1ne : S1.Nonempty := by    refine ⟨((max a p.re) + 1 : ℝ) + (p.im - 1) * Complex.I, ?_⟩    have h1 : a < (max a p.re) + 1 := by      have : a ≤ max a p.re := le_max_left _ _      exact lt_of_le_of_lt this (by linarith)    have h2 : (p.im - 1) < p.im := by linarith    simpa [S1, Complex.add_re, Complex.add_im, Complex.mul_re, Complex.mul_im]      using And.intro h1 h2  have hS2ne : S2.Nonempty := by    refine ⟨((a + p.re) / 2 : ℝ) + (p.im : ℝ) * Complex.I, ?_⟩    have h1 : a < (a + p.re) / 2 := by linarith    have h2 : (a + p.re) / 2 < p.re := by linarith    simpa [S2, Complex.add_re, Complex.add_im, Complex.mul_re, Complex.mul_im]      using And.intro h1 h2  have hS3ne : S3.Nonempty := by    refine ⟨((max a p.re) + 1 : ℝ) + (p.im + 1) * Complex.I, ?_⟩    have h1 : a < (max a p.re) + 1 := by      have : a ≤ max a p.re := le_max_left _ _      exact lt_of_le_of_lt this (by linarith)    have h2 : p.im < (p.im + 1) := by linarith    simpa [S3, Complex.add_re, Complex.add_im, Complex.mul_re, Complex.mul_im]      using And.intro h1 h2  have hS4ne : S4.Nonempty := by    refine ⟨(p.re + 1 : ℝ) + (0 : ℝ) * Complex.I, ?_⟩    have : p.re < p.re + 1 := by linarith    simp [S4, Complex.add_re]  have hS1pc : IsPathConnected S1 := (hS1conv.isPathConnected hS1ne)  have hS2pc : IsPathConnected S2 := (hS2conv.isPathConnected hS2ne)  have hS3pc : IsPathConnected S3 := (hS3conv.isPathConnected hS3ne)  have hS4pc : IsPathConnected S4 := (hS4conv.isPathConnected hS4ne)  let A : Set ℂ := S1 ∪ S2  let B : Set ℂ := S3 ∪ S4  have hS1S2_int : (S1 ∩ S2).Nonempty := by    refine ⟨((a + p.re) / 2 : ℝ) + (p.im - (1/2)) * Complex.I, ?_⟩    have h1a : a < (a + p.re) / 2 := by linarith    have h1b : (p.im - (1/2)) < p.im := by linarith    have h2a : a < (a + p.re) / 2 := by linarith    have h2b : (a + p.re) / 2 < p.re := by linarith    constructor    · simpa [S1, Complex.add_re, Complex.add_im, Complex.mul_re, Complex.mul_im]        using And.intro h1a h1b    · simpa [S2, Complex.add_re, Complex.add_im, Complex.mul_re, Complex.mul_im]        using And.intro h2a h2b  have hApc : IsPathConnected A :=    IsPathConnected.union (U := S1) (V := S2) hS1pc hS2pc (by      rcases hS1S2_int with ⟨z, hz⟩; exact ⟨z, hz⟩)  have hS3S4_int : (S3 ∩ S4).Nonempty := by    refine ⟨(p.re + 1 : ℝ) + (p.im + 1) * Complex.I, ?_⟩    have h3a : a < p.re + 1 := lt_trans hp (by linarith)    have h3b : p.im < p.im + 1 := by linarith    have h4 : p.re < p.re + 1 := by linarith    constructor    · simpa [S3, Complex.add_re, Complex.add_im, Complex.mul_re, Complex.mul_im]        using And.intro h3a h3b    · simp [S4, Complex.add_re, Complex.mul_re]  have hBpc : IsPathConnected B :=    IsPathConnected.union (U := S3) (V := S4) hS3pc hS4pc (by      rcases hS3S4_int with ⟨z, hz⟩; exact ⟨z, hz⟩)  have hABint : (A ∩ B).Nonempty := by    refine ⟨(p.re + 1 : ℝ) + (p.im - 1) * Complex.I, ?_⟩    constructor    · refine Or.inl ?_      have h1 : a < p.re + 1 := lt_trans hp (by linarith)      have h2 : (p.im - 1) < p.im := by linarith      simpa [S1, Complex.add_re, Complex.add_im, Complex.mul_re, Complex.mul_im]        using And.intro h1 h2    · refine Or.inr ?_      have h4 : p.re < p.re + 1 := by linarith      simp [S4, Complex.add_re, Complex.mul_re]  have hUnionPC : IsPathConnected (A ∪ B) :=    IsPathConnected.union (U := A) (V := B) hApc hBpc (by      rcases hABint with ⟨z, hz⟩; exact ⟨z, hz⟩)  have hcover : ({z : ℂ | a < z.re} \ ({p} : Set ℂ)) = A ∪ B := by    ext z; constructor    · intro hz      rcases hz with ⟨hzH, hznot⟩      rcases lt_trichotomy z.re p.re with hlt | heq | hgt      · exact Or.inl (Or.inr ⟨hzH, hlt⟩)      · rcases lt_trichotomy z.im p.im with himlt | himeq | himgt        · exact Or.inl (Or.inl ⟨hzH, himlt⟩)        · have hz_eq : z = p := by            have hzdecomp : (z.re : ℂ) + (z.im : ℝ) * Complex.I = z := by simp            have hpdecomp : (p.re : ℂ) + (p.im : ℝ) * Complex.I = p := by simp            have : (z.re : ℂ) + (z.im : ℝ) * Complex.I = (p.re : ℂ) + (p.im : ℝ) * Complex.I := by              simp [heq, himeq]            simpa [hzdecomp, hpdecomp] using this          have : z ∈ ({p} : Set ℂ) := by simp [Set.mem_singleton_iff, hz_eq]          exact (hznot this).elim        · exact Or.inr (Or.inl ⟨hzH, himgt⟩)      · exact Or.inr (Or.inr hgt)    · intro hz      have hzH : a < z.re := by        rcases hz with hA | hB        · rcases hA with hS1 | hS2          · exact hS1.1          · exact hS2.1        · rcases hB with hS3 | hS4          · exact hS3.1          · exact lt_trans hp hS4      have hzneq : z ≠ p := by        rcases hz with hA | hB        · rcases hA with hS1 | hS2          · intro h            have : z.im = p.im := by simp [h]            have : z.im < z.im := by simpa [this] using hS1.2            exact lt_irrefl _ this          · intro h            have : z.re = p.re := by simp [h]            exact (ne_of_lt hS2.2) this        · rcases hB with hS3 | hS4          · intro h            have : p.im = z.im := by simp [h]            have : z.im < z.im := by simpa [this] using hS3.2            exact lt_irrefl _ this          · intro h            have : p.re = z.re := by simp [h]            exact (ne_of_gt hS4) this.symm      exact And.intro hzH (by intro hzmem; exact hzneq (by simpa [Set.mem_singleton_iff] using hzmem))  simpa [hcover] using hUnionPC