Regularity Domain is Connected iff

lemma regularityDomain_isConnected_iff :    IsConnected T.regularityDomain ↔ (ofReal ⁻¹' T.regularityDomain).Nonempty := by  rw [T.regularityDomain_isOpen.isConnected_iff_isPathConnected]  constructor  · intro h    obtain ⟨f, hf⟩ : JoinedIn T.regularityDomain (-I) I :=      h.joinedIn _ (hT.mem_regularityDomain_of_im_ne_zero (by simp)) _        (hT.mem_regularityDomain_of_im_ne_zero (by simp))    have hIVT := intermediate_value_Icc (f := fun t ↦ (f t).im) zero_le_one (by fun_prop)    simp only [Path.source, neg_im, I_im, Path.target] at hIVT    obtain ⟨t, _, ht⟩ := hIVT (show (0 : ℝ) ∈ Icc (-1) 1 by simp)    specialize hf t    rw [← re_add_im (f t), show (f t).im = 0 from ht] at hf    exact ⟨(f t).re, by simp_all⟩  · intro ⟨r, hr⟩    apply mem_preimage.mp at hr    refine isPathConnected_iff.mpr ⟨?_, fun z₁ hz₁ z₂ hz₂ ↦ ?_⟩    · exact ⟨I, hT.mem_regularityDomain_of_im_ne_zero (by simp)⟩    · have h : ∀ z ∈ T.regularityDomain, JoinedIn T.regularityDomain z r := by        intro z hz        by_cases hz_im : z.im = 0        · rcases eq_or_ne z r with rfl | hzr          · exact JoinedIn.refl hr          · let path : Path z r := {              toFun t := ((z + r) + (z - r) * cexp (Real.pi * t * I)) / 2              source' := by simp              target' := by simp [add_comm z r, add_add_sub_cancel]            }            refine ⟨path, fun t ↦ ?_⟩            by_cases! ht : ∃ n : ℤ, n = (t : ℝ)            · obtain ⟨n, htn⟩ := ht              have hexp : cexp (Real.pi * t * I) = (-1) ^ n := by                rw [← exp_pi_mul_I, ← exp_int_mul, ← htn]                exact congrArg cexp (by push_cast; ring)              rcases Int.even_or_odd n with he | ho              · simp [path, hexp, he.neg_one_zpow, hz]              · simp [path, hexp, ho.neg_one_zpow, add_comm z r, hr]            · have hzr' : z.re - r ≠ 0 :=                  fun h ↦ hzr <| Complex.ext (sub_eq_zero.mp h) (by simp [hz_im])              refine hT.mem_regularityDomain_of_im_ne_zero ?_              simp [path, hz_im, exp_im, Real.sin_eq_zero_iff, mul_comm, hzr', ht]        · refine JoinedIn.of_segment_subset fun w ⟨a, b, _, _, _, hw⟩ ↦ ?_          rcases eq_zero_or_neZero a with rfl | _          · simp_all          · exact hT.mem_regularityDomain_of_im_ne_zero fun _ ↦ hz_im (by simp_all [← hw])      exact (h z₁ hz₁).trans (h z₂ hz₂).symm