awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
s : Set ℂ
hs : UniqueDiffWithinAt ℝ s x
h : DifferentiableWithinAt ℂ f s x
⊢ HSMul.hSMul (β := E) I ((fderivWithin ℂ f s x : (a : ℂ) → E) 1 : E) =
    HSMul.hSMul (β := E) (HSMul.hSMul (β := ℂ) I 1) ((fderivWithin ℂ f s x : (a : ℂ) → E) 1 : E)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
s : Set ℂ
hs : UniqueDiffWithinAt ℝ s x
h :
  DifferentiableWithinAt ℝ f s x ∧
    (fderivWithin ℝ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℝ f s x : (a : ℂ) → E) 1 : E)
h₁ : DifferentiableWithinAt ℝ f s x
h₂ : (fderivWithin ℝ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℝ f s x : (a : ℂ) → E) 1 : E)
refine_2 : ∃ (g' : ℂ →L[ℂ] E), Eq (α := ℂ →L[ℝ] E) (restrictScalars ℝ g') (fderivWithin ℝ f s x)
⊢ DifferentiableWithinAt ℂ f s x

Tactic:
apply (differentiableWithinAt_iff_restrictScalars ℝ h₁ hs).2

Premises used: Iff.mpr, Real, differentiableWithinAt_iff_restrictScalars
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
s : Set ℂ
hs : UniqueDiffWithinAt ℝ s x
h_1 :
  DifferentiableWithinAt ℝ f s x ∧
    (fderivWithin ℝ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℝ f s x : (a : ℂ) → E) 1 : E)
h₁ : DifferentiableWithinAt ℝ f s x
h₂ : (fderivWithin ℝ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℝ f s x : (a : ℂ) → E) 1 : E)
h : Eq (α := ℂ →L[ℝ] E) (restrictScalars ℝ (complexOfReal (fderivWithin ℝ f s x) h₂)) (fderivWithin ℝ f s x)
⊢ ∃ (g' : ℂ →L[ℂ] E), Eq (α := ℂ →L[ℝ] E) (restrictScalars ℝ g') (fderivWithin ℝ f s x)

Tactic:
use (fderivWithin ℝ f s x).complexOfReal h₂

Premises used: Real, ContinuousLinearMap.complexOfReal, fderivWithin
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
s : Set ℂ
hs : UniqueDiffWithinAt ℝ s x
h :
  DifferentiableWithinAt ℝ f s x ∧
    (fderivWithin ℝ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℝ f s x : (a : ℂ) → E) 1 : E)
h₁ : DifferentiableWithinAt ℝ f s x
h₂ : (fderivWithin ℝ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℝ f s x : (a : ℂ) → E) 1 : E)
⊢ Eq (α := ℂ →L[ℝ] E) (restrictScalars ℝ (complexOfReal (fderivWithin ℝ f s x) h₂)) (fderivWithin ℝ f s x)

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
s : Set ℂ
f' : ℂ →L[ℝ] E
h₁ : HasFDerivWithinAt f f' s x
h₂ : (f' : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((f' : (a : ℂ) → E) 1 : E)
⊢ HasFDerivWithinAt f (f'.complexOfReal h₂) s x

Tactic:
.of_restrictScalars ℝ h₁ rfl

Premises used: Real, HasFDerivWithinAt.of_restrictScalars, rfl
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
s : Set ℂ
h₁ : DifferentiableWithinAt ℝ f s x
h₂ : (fderivWithin ℝ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℝ f s x : (a : ℂ) → E) 1 : E)
hs : UniqueDiffWithinAt ℝ s x
⊢ Eq (α := ℂ →L[ℝ] E) (restrictScalars ℝ (fderivWithin ℂ f s x)) (fderivWithin ℝ f s x)

Tactic:
have := ((differentiableWithinAt_complex_iff_differentiableWithinAt_real hs).2
      ⟨h₁, h₂⟩).restrictScalars_fderivWithin ℝ hs
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
s : Set ℂ
h₁ : DifferentiableWithinAt ℝ f s x
h₂ : (fderivWithin ℝ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℝ f s x : (a : ℂ) → E) 1 : E)
hs : UniqueDiffWithinAt ℝ s x
this : Eq (α := ℂ →L[ℝ] E) (restrictScalars ℝ (fderivWithin ℂ f s x)) (fderivWithin ℝ f s x)
⊢ fderivWithin ℂ f s x = complexOfReal (fderivWithin ℝ f s x) h₂

Tactic:
simpa [DFunLike.ext_iff]

Premises used: DFunLike.ext_iff
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
s : Set ℂ
h₁ : DifferentiableWithinAt ℝ f s x
h₂ : (fderivWithin ℝ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℝ f s x : (a : ℂ) → E) 1 : E)
rw : HasFDerivWithinAt f (complexOfReal (fderivWithin ℝ f s x) h₂) s x
⊢ HasDerivWithinAt f ((complexOfReal (fderivWithin ℝ f s x) h₂ : (a : ℂ) → E) 1) s x

Tactic:
rw [hasDerivWithinAt_iff_hasFDerivWithinAt, toSpanSingleton_apply_map_one]

Premises used: ContinuousLinearMap.toSpanSingleton_apply_map_one, hasDerivWithinAt_iff_hasFDerivWithinAt
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
s : Set ℂ
h₁ : DifferentiableWithinAt ℝ f s x
h₂ : (fderivWithin ℝ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℝ f s x : (a : ℂ) → E) 1 : E)
⊢ HasFDerivWithinAt f (complexOfReal (fderivWithin ℝ f s x) h₂) s x

Tactic:
h₁.hasFDerivWithinAt.complexOfReal h₂

Premises used: HasFDerivWithinAt.complexOfReal, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
s : Set ℂ
h₁ : DifferentiableWithinAt ℝ f s x
h₂ : (fderivWithin ℝ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℝ f s x : (a : ℂ) → E) 1 : E)
⊢ HasFDerivWithinAt f (complexOfReal (fderivWithin ℝ f s x) h₂) s x

Tactic:
exact h₁.hasFDerivWithinAt.complexOfReal h₂

Premises used: HasFDerivWithinAt.complexOfReal, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
s : Set ℂ
h₁ : DifferentiableWithinAt ℝ f s x
h₂ : (fderivWithin ℝ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℝ f s x : (a : ℂ) → E) 1 : E)
hs : UniqueDiffWithinAt ℂ s x
⊢ derivWithin f s x = (fderivWithin ℝ f s x : (a : ℂ) → E) 1

Tactic:
HasDerivWithinAt.derivWithin (complexOfReal_hasDerivWithinAt h₁ h₂) hs

Premises used: complexOfReal_hasDerivWithinAt, HasDerivWithinAt.derivWithin
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
h : DifferentiableAt ℂ f x
⊢ DifferentiableAt ℝ f x ∧ (fderiv ℝ f x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderiv ℝ f x : (a : ℂ) → E) 1 : E)

Tactic:
simp [h.restrictScalars ℝ, h.fderiv_restrictScalars ℝ]

Premises used: Real, DifferentiableAt.fderiv_restrictScalars, DifferentiableAt.restrictScalars
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
f' : ℂ →L[ℝ] E
h₁ : HasFDerivAt f f' x
h₂ : (f' : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((f' : (a : ℂ) → E) 1 : E)
⊢ HasFDerivAt f (f'.complexOfReal h₂) x

Tactic:
hasFDerivAt_of_restrictScalars ℝ h₁ rfl

Premises used: Real, hasFDerivAt_of_restrictScalars, rfl
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
h₁ : DifferentiableAt ℝ f x
h₂ : (fderiv ℝ f x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderiv ℝ f x : (a : ℂ) → E) 1 : E)
rw : HasFDerivAt f (complexOfReal (fderiv ℝ f x) h₂) x
⊢ HasDerivAt f ((complexOfReal (fderiv ℝ f x) h₂ : (a : ℂ) → E) 1) x

Tactic:
rw [hasDerivAt_iff_hasFDerivAt, toSpanSingleton_apply_map_one]

Premises used: ContinuousLinearMap.toSpanSingleton_apply_map_one, hasDerivAt_iff_hasFDerivAt
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
h₁ : DifferentiableAt ℝ f x
h₂ : (fderiv ℝ f x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderiv ℝ f x : (a : ℂ) → E) 1 : E)
⊢ HasFDerivAt f (complexOfReal (fderiv ℝ f x) h₂) x

Tactic:
hasFDerivAt_of_restrictScalars ℝ h₁.hasFDerivAt rfl

Premises used: Real, hasFDerivAt_of_restrictScalars, DifferentiableAt.hasFDerivAt, rfl
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
h₁ : DifferentiableAt ℝ f x
h₂ : (fderiv ℝ f x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderiv ℝ f x : (a : ℂ) → E) 1 : E)
⊢ HasFDerivAt f (complexOfReal (fderiv ℝ f x) h₂) x

Tactic:
exact hasFDerivAt_of_restrictScalars ℝ h₁.hasFDerivAt rfl

Premises used: Real, hasFDerivAt_of_restrictScalars, DifferentiableAt.hasFDerivAt, rfl
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
h₁ : DifferentiableAt ℝ f x
h₂ : (fderiv ℝ f x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderiv ℝ f x : (a : ℂ) → E) 1 : E)
⊢ deriv f x = (fderiv ℝ f x : (a : ℂ) → E) 1

Tactic:
HasDerivAt.deriv (complexOfReal_hasDerivAt h₁ h₂)

Premises used: HasDerivAt.deriv, complexOfReal_hasDerivAt
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
h₁ : DifferentiableAt ℝ f x
h₂ : (fderiv ℝ f x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderiv ℝ f x : (a : ℂ) → E) 1 : E)
⊢ complexOfReal (fderiv ℝ f x) h₂ = fderiv ℂ f x

Tactic:
(h₁.hasFDerivAt.complexOfReal_hasFDerivAt h₂).fderiv.symm

Premises used: HasFDerivAt.complexOfReal_hasFDerivAt, DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv, Eq.symm
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
s t : Set ℝ
⊢ Eq (α := Set ℂ) ((convexHull ℝ : (a : Set ℂ) → Set ℂ) ((⇑equivRealProdLm : (a : ℂ) → ℝ × ℝ) ⁻¹' s ×ˢ t) : Set ℂ)
    (preimage (β := ℝ × ℝ) (⇑equivRealProdLm : (a : ℂ) → ℝ × ℝ)
        ((convexHull ℝ : (a : Set (ℝ × ℝ)) → Set (ℝ × ℝ)) (s ×ˢ t)) :
      Set ℂ)

Tactic:
simpa only [← LinearEquiv.image_symm_eq_preimage]
        using ((equivRealProdLm.symm.toLinearMap).image_convexHull (s ×ˢ t)).symm

Premises used: LinearEquiv.symm, SProd.sprod, LinearEquiv.image_symm_eq_preimage, LinearEquiv.toLinearMap, LinearMap.image_convexHull, Eq.symm, Complex.equivRealProdLm
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
s t : Set ℝ
rw :
  (⇑equivRealProdLm : (a : ℂ) → ℝ × ℝ) ⁻¹'
      SProd.sprod (α := Set ℝ) (β := Set ℝ) ((convexHull ℝ : (a : Set ℝ) → Set ℝ) s : Set ℝ)
        ((convexHull ℝ : (a : Set ℝ) → Set ℝ) t : Set ℝ) =
    (convexHull ℝ : (a : Set ℝ) → Set ℝ) s ×ℂ (convexHull ℝ : (a : Set ℝ) → Set ℝ) t
⊢ preimage (β := ℝ × ℝ) (⇑equivRealProdLm : (a : ℂ) → ℝ × ℝ)
      ((convexHull ℝ : (a : Set (ℝ × ℝ)) → Set (ℝ × ℝ)) (s ×ˢ t)) =
    (convexHull ℝ : (a : Set ℝ) → Set ℝ) s ×ℂ (convexHull ℝ : (a : Set ℝ) → Set ℝ) t

Tactic:
rw [convexHull_prod]

Premises used: convexHull_prod
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
s t : Set ℝ
⊢ (⇑equivRealProdLm : (a : ℂ) → ℝ × ℝ) ⁻¹'
      SProd.sprod (α := Set ℝ) (β := Set ℝ) ((convexHull ℝ : (a : Set ℝ) → Set ℝ) s : Set ℝ)
        ((convexHull ℝ : (a : Set ℝ) → Set ℝ) t : Set ℝ) =
    (convexHull ℝ : (a : Set ℝ) → Set ℝ) s ×ℂ (convexHull ℝ : (a : Set ℝ) → Set ℝ) t

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
z : ℂ
hz : 0 < z
⊢ StarConvex ℝ z slitPlane

Tactic:
Complex.compl_Iic_zero ▸ starConvex_compl_Iic hz

Premises used: Eq.rec, Complex.compl_Iic_zero, starConvex_compl_Iic
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
x : ℝ
hx : 0 < x
⊢ StarConvex ℝ (↑x : ℂ) slitPlane

Tactic:
starConvex_slitPlane <| zero_lt_real.2 hx

Premises used: Iff.mpr, Complex.zero_lt_real, Complex.starConvex_slitPlane
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
⊢ StarConvex ℝ 1 slitPlane

Tactic:
starConvex_slitPlane one_pos

Premises used: Complex.starConvex_slitPlane, one_pos
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
⊢ Convex ℝ (E := ℂ) {c : ℂ | c.re < r}

Tactic:
convex_halfSpace_lt (.mk add_re smul_re) _

Premises used: setOf, Complex.add_re, IsLinearMap.mk, convex_halfSpace_lt
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
⊢ Convex ℝ (E := ℂ) {c : ℂ | c.re ≤ r}

Tactic:
convex_halfSpace_le (.mk add_re smul_re) _

Premises used: setOf, Complex.add_re, convex_halfSpace_le, IsLinearMap.mk
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
⊢ Convex ℝ (E := ℂ) {c : ℂ | r < c.re}

Tactic:
convex_halfSpace_gt (.mk add_re smul_re) _

Premises used: setOf, Complex.add_re, convex_halfSpace_gt, IsLinearMap.mk
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
⊢ Convex ℝ (E := ℂ) {c : ℂ | r ≤ c.re}

Tactic:
convex_halfSpace_ge (.mk add_re smul_re) _

Premises used: setOf, convex_halfSpace_ge, Complex.add_re, IsLinearMap.mk
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
⊢ Convex ℝ (E := ℂ) {c : ℂ | c.im < r}

Tactic:
convex_halfSpace_lt (.mk add_im smul_im) _

Premises used: Complex.add_im, setOf, IsLinearMap.mk, convex_halfSpace_lt
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
⊢ Convex ℝ (E := ℂ) {c : ℂ | c.im ≤ r}

Tactic:
convex_halfSpace_le (.mk add_im smul_im) _

Premises used: Complex.add_im, setOf, convex_halfSpace_le, IsLinearMap.mk
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
⊢ Convex ℝ (E := ℂ) {c : ℂ | r < c.im}

Tactic:
convex_halfSpace_gt (.mk add_im smul_im) _

Premises used: Complex.add_im, setOf, convex_halfSpace_gt, IsLinearMap.mk
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
⊢ Convex ℝ (E := ℂ) {c : ℂ | r ≤ c.im}

Tactic:
convex_halfSpace_ge (.mk add_im smul_im) _

Premises used: Complex.add_im, setOf, convex_halfSpace_ge, IsLinearMap.mk
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
s : Set ℂ
hs₁ : {z : ℂ | r < z.im} ⊆ s
hs₂ : s ⊆ {z : ℂ | r ≤ z.im}
⊢ s ⊆ closure {z : ℂ | r < z.im}

Tactic:
simpa only [closure_setOf_lt_im] using hs₂

Premises used: Complex.closure_setOf_lt_im
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
s : Set ℂ
hs₁ : {z : ℂ | r < z.im} ⊆ s
hs₂ : s ⊆ {z : ℂ | r ≤ z.im}
refine : IsConnected (α := ℂ) {z : ℂ | r < z.im}
⊢ IsConnected s

Tactic:
refine .subset_closure ?_ hs₁ (by simpa only [closure_setOf_lt_im] using hs₂)
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
s : Set ℂ
hs₁ : {z : ℂ | r < z.im} ⊆ s
hs₂ : s ⊆ {z : ℂ | r ≤ z.im}
⊢ Membership.mem (γ := Set ℂ) {c : ℂ | r < c.im} (((↑r : ℂ) + 1) * I)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
s : Set ℂ
hs₁ : {z : ℂ | r < z.im} ⊆ s
hs₂ : s ⊆ {z : ℂ | r ≤ z.im}
⊢ IsConnected (α := ℂ) {z : ℂ | r < z.im}

Tactic:
exact (convex_halfSpace_im_gt r).isConnected ⟨(r + 1) * I, by simp⟩

Premises used: HMul.hMul, Convex.isConnected, convex_halfSpace_im_gt, Complex.ofReal, HAdd.hAdd, Exists.intro, OfNat.ofNat, Complex.I
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
s : Set ℂ
hs₁ : {z : ℂ | z.im < r} ⊆ s
hs₂ : s ⊆ {z : ℂ | z.im ≤ r}
⊢ s ⊆ closure {z : ℂ | z.im < r}

Tactic:
simpa only [closure_setOf_im_lt] using hs₂

Premises used: Complex.closure_setOf_im_lt
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
s : Set ℂ
hs₁ : {z : ℂ | z.im < r} ⊆ s
hs₂ : s ⊆ {z : ℂ | z.im ≤ r}
refine : IsConnected (α := ℂ) {z : ℂ | z.im < r}
⊢ IsConnected s

Tactic:
refine .subset_closure ?_ hs₁ (by simpa only [closure_setOf_im_lt] using hs₂)
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
s : Set ℂ
hs₁ : {z : ℂ | z.im < r} ⊆ s
hs₂ : s ⊆ {z : ℂ | z.im ≤ r}
⊢ Membership.mem (γ := Set ℂ) {c : ℂ | c.im < r} (((↑r : ℂ) - 1) * I)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
s : Set ℂ
hs₁ : {z : ℂ | z.im < r} ⊆ s
hs₂ : s ⊆ {z : ℂ | z.im ≤ r}
⊢ IsConnected (α := ℂ) {z : ℂ | z.im < r}

Tactic:
exact (convex_halfSpace_im_lt r).isConnected ⟨(r - 1) * I, by simp⟩

Premises used: HMul.hMul, Convex.isConnected, HSub.hSub, convex_halfSpace_im_lt, Complex.ofReal, Exists.intro, OfNat.ofNat, Complex.I
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
U : Set ℂ
U_convex : Convex ℝ U
z w : ℂ
hz : z ∈ U
hw : w ∈ U
hzw : (↑z.re : ℂ) + (↑w.im : ℂ) * I ∈ U
hwz : (↑w.re : ℂ) + (↑z.im : ℂ) * I ∈ U
⊢ {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} ⊆ U

Tactic:
grind
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
U : Set ℂ
U_convex : Convex ℝ U
z w : ℂ
hz : z ∈ U
hw : w ∈ U
hzw : (↑z.re : ℂ) + (↑w.im : ℂ) * I ∈ U
hwz : (↑w.re : ℂ) + (↑z.im : ℂ) * I ∈ U
⊢ z.Rectangle w ⊆ U

Tactic:
simpa only [rectangle_eq_convexHull] using convexHull_min (by grind) U_convex

Premises used: convexHull_min, Complex.rectangle_eq_convexHull
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
⊢ Membership.mem (γ := Set ℂ) {c : ℂ | 0 < c.im} I

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
⊢ Membership.mem (γ := Set ℂ) {c : ℂ | 0 < c.re} 1

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
⊢ Membership.mem (γ := Set ℂ) ({c : ℂ | 0 < c.im} ∩ {c : ℂ | 0 < c.re}) (1 + I)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
⊢ Membership.mem (γ := Set ℂ) {c : ℂ | c.im < 0} (-I)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
⊢ Membership.mem (γ := Set ℂ) {c : ℂ | c.re < 0} (-1)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
⊢ Membership.mem (γ := Set ℂ) ({c : ℂ | c.im < 0} ∩ {c : ℂ | c.re < 0}) (-1 - I)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
⊢ Membership.mem (γ := Set ℂ) (({c : ℂ | 0 < c.im} ∪ {c : ℂ | 0 < c.re}) ∩ ({c : ℂ | c.im < 0} ∪ {c : ℂ | c.re < 0}))
    (1 - I)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
h : Eq (α := Set ℂ) {0}ᶜ ({c : ℂ | 0 < c.im} ∪ {c : ℂ | 0 < c.re} ∪ ({c : ℂ | c.im < 0} ∪ {c : ℂ | c.re < 0}))
⊢ IsPathConnected (X := ℂ) {0}ᶜ

Tactic:
convert!
        (((convex_halfSpace_im_gt 0).isPathConnected ⟨.I, by simp⟩).union
              ((convex_halfSpace_re_gt 0).isPathConnected ⟨1, by simp⟩) ⟨1 + .I, by simp⟩).union
          (((convex_halfSpace_im_lt 0).isPathConnected ⟨-.I, by simp⟩).union
            ((convex_halfSpace_re_lt 0).isPathConnected ⟨-1, by simp⟩) ⟨-1 - .I, by simp⟩)
          ⟨1 - .I, by simp⟩ using 1

Premises used: HSub.hSub, convex_halfSpace_im_gt, Convex.isPathConnected, convex_halfSpace_im_lt, convex_halfSpace_re_lt, HAdd.hAdd, Exists.intro, IsPathConnected.union, OfNat.ofNat, convex_halfSpace_re_gt, Neg.neg, Complex.I
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
h :
  ∀ (x : ℂ),
    Membership.mem (γ := Set ℂ) {0}ᶜ x ↔
      Membership.mem (γ := Set ℂ) ({c : ℂ | 0 < c.im} ∪ {c : ℂ | 0 < c.re} ∪ ({c : ℂ | c.im < 0} ∪ {c : ℂ | c.re < 0}))
        x
⊢ Eq (α := Set ℂ) {0}ᶜ ({c : ℂ | 0 < c.im} ∪ {c : ℂ | 0 < c.re} ∪ ({c : ℂ | c.im < 0} ∪ {c : ℂ | c.re < 0}))

Tactic:
ext x
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
x : ℂ
⊢ Membership.mem (γ := Set ℂ) ({c : ℂ | 0 < c.im} ∪ {c : ℂ | 0 < c.re} ∪ ({c : ℂ | c.im < 0} ∪ {c : ℂ | c.re < 0})) x →
    Membership.mem (γ := Set ℂ) {0}ᶜ x

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
x : ℂ
h :
  Membership.mem (γ := Set ℂ) {0}ᶜ x →
    Membership.mem (γ := Set ℂ) ({c : ℂ | 0 < c.im} ∪ {c : ℂ | 0 < c.re} ∪ ({c : ℂ | c.im < 0} ∪ {c : ℂ | c.re < 0})) x
⊢ Membership.mem (γ := Set ℂ) {0}ᶜ x ↔
    Membership.mem (γ := Set ℂ) ({c : ℂ | 0 < c.im} ∪ {c : ℂ | 0 < c.re} ∪ ({c : ℂ | c.im < 0} ∪ {c : ℂ | c.re < 0})) x

Tactic:
refine ⟨?_, by aesop⟩
-- Module: Mathlib.Analysis.Complex.Convex
Goal:
r : ℝ
x : ℂ
⊢ Membership.mem (γ := Set ℂ) {0}ᶜ x →
    Membership.mem (γ := Set ℂ) ({c : ℂ | 0 < c.im} ∪ {c : ℂ | 0 < c.re} ∪ ({c : ℂ | c.im < 0} ∪ {c : ℂ | c.re < 0})) x

Tactic:
simp +contextual [Complex.ext_iff, -not_and, not_and_or, or_imp, ← ne_eq, ← lt_or_lt_iff_ne]

Premises used: or_imp, Complex.ext_iff, ne_eq, not_and_or, lt_or_lt_iff_ne, not_and
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
⊢ IsAddQuotientCoveringMap (X := { z : ℂ // z ≠ 0 }) (fun (z : ℂ) ↦ Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (cexp z) ⋯)
    ↥(AddSubgroup.zmultiples (2 * (↑Real.pi : ℂ) * I))

Tactic:
Topology.IsQuotientMap.isAddQuotientCoveringMap_of_addSubgroup ?_
    _ ⟨NormedSpace.discreteTopology_zmultiples _⟩ fun {z _} ↦ ?_

Premises used: Topology.IsQuotientMap.isAddQuotientCoveringMap_of_addSubgroup, IsDiscrete.mk, NormedSpace.discreteTopology_zmultiples
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
refine_1 : IsQuotientMap (Y := { z : ℂ // z ≠ 0 }) fun (z : ℂ) ↦ Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (cexp z) ⋯
refine_2 :
  ∀ {z x : ℂ},
    Eq (α := { z : ℂ // z ≠ 0 }) (Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (cexp z) ⋯)
        (Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (cexp x) ⋯) ↔
      Membership.mem (γ := AddSubgroup ℂ) (AddSubgroup.zmultiples (2 * (↑Real.pi : ℂ) * I)) (x + -z)
⊢ IsAddQuotientCoveringMap (X := { z : ℂ // z ≠ 0 }) (fun (z : ℂ) ↦ Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (cexp z) ⋯)
    ↥(AddSubgroup.zmultiples (2 * (↑Real.pi : ℂ) * I))

Tactic:
refine Topology.IsQuotientMap.isAddQuotientCoveringMap_of_addSubgroup ?_
    _ ⟨NormedSpace.discreteTopology_zmultiples _⟩ fun {z _} ↦ ?_

Premises used: Topology.IsQuotientMap.isAddQuotientCoveringMap_of_addSubgroup, IsDiscrete.mk, NormedSpace.discreteTopology_zmultiples
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
⊢ Continuous (Y := { z : ℂ // z ≠ 0 }) fun (z : ℂ) ↦ Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (cexp z) ⋯

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
refine_1 : IsOpenMap (Y := { z : ℂ // z ≠ 0 }) fun (z : ℂ) ↦ Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (cexp z) ⋯
⊢ IsQuotientMap (Y := { z : ℂ // z ≠ 0 }) fun (z : ℂ) ↦ Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (cexp z) ⋯

Tactic:
refine IsOpenMap.isQuotientMap ?_ (by fun_prop) fun z ↦ ⟨_, Subtype.ext (exp_log z.2)⟩

Premises used: IsOpenMap.isQuotientMap, Exists.intro, Subtype.ext
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
⊢ IsOpenMap (Y := { z : ℂ // z ≠ 0 }) fun (z : ℂ) ↦ Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (cexp z) ⋯

Tactic:
(IsOpen.isOpenEmbedding_subtypeVal isClosed_singleton.1).isOpenMap_iff.mpr isOpenMap_exp

Premises used: Iff.mpr, IsOpen.isOpenEmbedding_subtypeVal, IsClosed.isOpen_compl, Set.Mem, setOf, Topology.IsOpenEmbedding.isOpenMap_iff, Set.singleton, Complex.isOpenMap_exp, Not
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
⊢ IsOpenMap (Y := { z : ℂ // z ≠ 0 }) fun (z : ℂ) ↦ Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (cexp z) ⋯

Tactic:
exact (IsOpen.isOpenEmbedding_subtypeVal isClosed_singleton.1).isOpenMap_iff.mpr isOpenMap_exp
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
z x : ℂ
refine_2 :
  cexp z = cexp x ↔ Membership.mem (γ := AddSubgroup ℂ) (AddSubgroup.zmultiples (2 * (↑Real.pi : ℂ) * I)) (x + -z)
refine_2₁ :
  cexp x = cexp z ↔ Membership.mem (γ := AddSubgroup ℂ) (AddSubgroup.zmultiples (2 * (↑Real.pi : ℂ) * I)) (x + -z)
refine_2₂ :
  (∃ (n : ℤ), x = z + (↑n : ℂ) * (2 * (↑Real.pi : ℂ) * I)) ↔
    Membership.mem (γ := AddSubgroup ℂ) (AddSubgroup.zmultiples (2 * (↑Real.pi : ℂ) * I)) (x + -z)
refine_2₃ : (∃ (n : ℤ), x = z + (↑n : ℂ) * (2 * (↑Real.pi : ℂ) * I)) ↔ ∃ (k : ℤ), k • (2 * (↑Real.pi : ℂ) * I) = x + -z
refine_2₄ : (∃ (n : ℤ), x = z + (↑n : ℂ) * (2 * (↑Real.pi : ℂ) * I)) ↔ ∃ (k : ℤ), k • (2 * (↑Real.pi : ℂ) * I) + z = x
refine_2₅ : (∃ (n : ℤ), x = z + (↑n : ℂ) * (2 * (↑Real.pi : ℂ) * I)) ↔ ∃ (k : ℤ), x = k • (2 * (↑Real.pi : ℂ) * I) + z
refine_2₆ : (∃ (n : ℤ), x = z + (↑n : ℂ) * (2 * (↑Real.pi : ℂ) * I)) ↔ ∃ (k : ℤ), x = z + k • (2 * (↑Real.pi : ℂ) * I)
⊢ Eq (α := { z : ℂ // z ≠ 0 }) (Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (cexp z) ⋯)
      (Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (cexp x) ⋯) ↔
    Membership.mem (γ := AddSubgroup ℂ) (AddSubgroup.zmultiples (2 * (↑Real.pi : ℂ) * I)) (x + -z)

Tactic:
simp_rw [Subtype.ext_iff, eq_comm (a := exp z), exp_eq_exp_iff_exists_int,
      AddSubgroup.mem_zmultiples_iff, eq_add_neg_iff_add_eq, eq_comm, add_comm, zsmul_eq_mul]

Premises used: Complex.exp_eq_exp_iff_exists_int, zsmul_eq_mul, AddSubgroup.mem_zmultiples_iff, eq_comm, add_comm, Subtype.ext_iff, eq_add_neg_iff_add_eq
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
⊢ IsCoveringMap (X := { z : ℂ // z ≠ 0 }) fun (z : ℂ) ↦ Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (cexp z) ⋯

Tactic:
isAddQuotientCoveringMap_exp.isCoveringMap

Premises used: IsAddQuotientCoveringMap.isCoveringMap, Complex.isAddQuotientCoveringMap_exp
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
⊢ IsOpen (X := ℂ) {0}ᶜ

Tactic:
simp