awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Convex (goal)
Goal:
z w : ℂ
simp_rw :
  uIcc z.re w.re ×ℂ uIcc z.im w.im =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
simp_rw₁ :
  segment ℝ z.re w.re ×ℂ segment ℝ z.im w.im =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
simp_rw₂ :
  (convexHull ℝ : (a : Set ℝ) → Set ℝ) {z.re, w.re} ×ℂ (convexHull ℝ : (a : Set ℝ) → Set ℝ) {z.im, w.im} =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
simp_rw₃ :
  Eq (α := Set ℂ) ((convexHull ℝ : (a : Set ℂ) → Set ℂ) ({z.re, w.re} ×ℂ {z.im, w.im}) : Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
simp_rw₄ :
  Eq (α := Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ)
        ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (α := Set ℝ) (β := Set ℝ) {z.re, w.re} {z.im, w.im}) :
      Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
⊢ z.Rectangle w =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
have simp_rw₅ : Eq (α := Set ℂ)
  ((convexHull ℝ : (a : Set ℂ) → Set ℂ)
      ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹'
        (Prod.mk z.re '' {z.im, w.im} ∪ SProd.sprod (α := Set ℝ) (β := Set ℝ) {w.re} {z.im, w.im})) :
    Set ℂ)
  ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
Tactic: simp_rw [Rectangle, ← segment_eq_uIcc, ← convexHull_pair, ← convexHull_reProdIm,
    ← preimage_equivRealProd_prod, insert_prod, singleton_prod, image_pair, insert_union,
    ← insert_eq, ← Equiv.image_symm_eq_preimage, image_insert_eq, image_singleton,
    equivRealProd_symm_apply, re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Convex (goal)
Goal:
z w : ℂ
simp_rw :
  uIcc z.re w.re ×ℂ uIcc z.im w.im =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
simp_rw₁ :
  segment ℝ z.re w.re ×ℂ segment ℝ z.im w.im =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
simp_rw₂ :
  (convexHull ℝ : (a : Set ℝ) → Set ℝ) {z.re, w.re} ×ℂ (convexHull ℝ : (a : Set ℝ) → Set ℝ) {z.im, w.im} =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
simp_rw₃ :
  Eq (α := Set ℂ) ((convexHull ℝ : (a : Set ℂ) → Set ℂ) ({z.re, w.re} ×ℂ {z.im, w.im}) : Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
simp_rw₄ :
  Eq (α := Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ)
        ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (α := Set ℝ) (β := Set ℝ) {z.re, w.re} {z.im, w.im}) :
      Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
simp_rw₅ :
  Eq (α := Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ)
        ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹'
          (Prod.mk z.re '' {z.im, w.im} ∪ SProd.sprod (α := Set ℝ) (β := Set ℝ) {w.re} {z.im, w.im})) :
      Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
⊢ z.Rectangle w =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
have simp_rw₆ : Eq (α := Set ℂ)
  ((convexHull ℝ : (a : Set ℂ) → Set ℂ)
      (preimage (β := ℝ × ℝ) (⇑equivRealProd : (a : ℂ) → ℝ × ℝ)
        (Prod.mk z.re '' {z.im, w.im} ∪ Prod.mk w.re '' {z.im, w.im})) :
    Set ℂ)
  ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
Tactic: simp_rw [Rectangle, ← segment_eq_uIcc, ← convexHull_pair, ← convexHull_reProdIm,
    ← preimage_equivRealProd_prod, insert_prod, singleton_prod, image_pair, insert_union,
    ← insert_eq, ← Equiv.image_symm_eq_preimage, image_insert_eq, image_singleton,
    equivRealProd_symm_apply, re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Convex (goal)
Goal:
z w : ℂ
simp_rw :
  uIcc z.re w.re ×ℂ uIcc z.im w.im =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
simp_rw₁ :
  segment ℝ z.re w.re ×ℂ segment ℝ z.im w.im =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
simp_rw₂ :
  (convexHull ℝ : (a : Set ℝ) → Set ℝ) {z.re, w.re} ×ℂ (convexHull ℝ : (a : Set ℝ) → Set ℝ) {z.im, w.im} =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
simp_rw₃ :
  Eq (α := Set ℂ) ((convexHull ℝ : (a : Set ℂ) → Set ℂ) ({z.re, w.re} ×ℂ {z.im, w.im}) : Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
simp_rw₄ :
  Eq (α := Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ)
        ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (α := Set ℝ) (β := Set ℝ) {z.re, w.re} {z.im, w.im}) :
      Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
simp_rw₅ :
  Eq (α := Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ)
        ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹'
          (Prod.mk z.re '' {z.im, w.im} ∪ SProd.sprod (α := Set ℝ) (β := Set ℝ) {w.re} {z.im, w.im})) :
      Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
simp_rw₆ :
  Eq (α := Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ)
        (preimage (β := ℝ × ℝ) (⇑equivRealProd : (a : ℂ) → ℝ × ℝ)
          (Prod.mk z.re '' {z.im, w.im} ∪ Prod.mk w.re '' {z.im, w.im})) :
      Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
⊢ z.Rectangle w =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
have simp_rw₇ : Eq (α := Set ℂ)
  ((convexHull ℝ : (a : Set ℂ) → Set ℂ)
      (preimage (β := ℝ × ℝ) (⇑equivRealProd : (a : ℂ) → ℝ × ℝ)
        ({(z.re, z.im), (z.re, w.im)} ∪ {(w.re, z.im), (w.re, w.im)})) :
    Set ℂ)
  ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
Tactic: simp_rw [Rectangle, ← segment_eq_uIcc, ← convexHull_pair, ← convexHull_reProdIm,
    ← preimage_equivRealProd_prod, insert_prod, singleton_prod, image_pair, insert_union,
    ← insert_eq, ← Equiv.image_symm_eq_preimage, image_insert_eq, image_singleton,
    equivRealProd_symm_apply, re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Convex (goal)
Goal:
z w : ℂ
simp_rw :
  uIcc z.re w.re ×ℂ uIcc z.im w.im =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
simp_rw₁ :
  segment ℝ z.re w.re ×ℂ segment ℝ z.im w.im =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
simp_rw₂ :
  (convexHull ℝ : (a : Set ℝ) → Set ℝ) {z.re, w.re} ×ℂ (convexHull ℝ : (a : Set ℝ) → Set ℝ) {z.im, w.im} =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
simp_rw₃ :
  Eq (α := Set ℂ) ((convexHull ℝ : (a : Set ℂ) → Set ℂ) ({z.re, w.re} ×ℂ {z.im, w.im}) : Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
simp_rw₄ :
  Eq (α := Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ)
        ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (α := Set ℝ) (β := Set ℝ) {z.re, w.re} {z.im, w.im}) :
      Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
simp_rw₅ :
  Eq (α := Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ)
        ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹'
          (Prod.mk z.re '' {z.im, w.im} ∪ SProd.sprod (α := Set ℝ) (β := Set ℝ) {w.re} {z.im, w.im})) :
      Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
simp_rw₆ :
  Eq (α := Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ)
        (preimage (β := ℝ × ℝ) (⇑equivRealProd : (a : ℂ) → ℝ × ℝ)
          (Prod.mk z.re '' {z.im, w.im} ∪ Prod.mk w.re '' {z.im, w.im})) :
      Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
simp_rw₇ :
  Eq (α := Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ)
        (preimage (β := ℝ × ℝ) (⇑equivRealProd : (a : ℂ) → ℝ × ℝ)
          ({(z.re, z.im), (z.re, w.im)} ∪ {(w.re, z.im), (w.re, w.im)})) :
      Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
⊢ z.Rectangle w =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
have simp_rw₈ : Eq (α := Set ℂ)
  ((convexHull ℝ : (a : Set ℂ) → Set ℂ)
      (preimage (β := ℝ × ℝ) (⇑equivRealProd : (a : ℂ) → ℝ × ℝ)
        (insert (z.re, z.im) ({(z.re, w.im)} ∪ {(w.re, z.im), (w.re, w.im)}))) :
    Set ℂ)
  ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
Tactic: simp_rw [Rectangle, ← segment_eq_uIcc, ← convexHull_pair, ← convexHull_reProdIm,
    ← preimage_equivRealProd_prod, insert_prod, singleton_prod, image_pair, insert_union,
    ← insert_eq, ← Equiv.image_symm_eq_preimage, image_insert_eq, image_singleton,
    equivRealProd_symm_apply, re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Convex (goal)
Goal:
r : ℝ
⊢ IsPathConnected (X := ℂ) {0}ᶜ
have h : Eq (α := Set ℂ) {0}ᶜ ({c : ℂ | 0 < c.im} ∪ {c : ℂ | 0 < c.re} ∪ ({c : ℂ | c.im < 0} ∪ {c : ℂ | c.re < 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Convex (goal)
Goal:
r : ℝ
⊢ Eq (α := Set ℂ) {0}ᶜ ({c : ℂ | 0 < c.im} ∪ {c : ℂ | 0 < c.re} ∪ ({c : ℂ | c.im < 0} ∪ {c : ℂ | c.re < 0}))
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Complex.Convex (goal)
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
have 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
Tactic: refine ⟨?_, by aesop⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.CoveringMap (goal)
Goal:
⊢ IsAddQuotientCoveringMap (X := { z : ℂ // z ≠ 0 }) (fun (z : ℂ) ↦ Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (cexp z) ⋯)
    ↥(AddSubgroup.zmultiples (2 * (↑Real.pi : ℂ) * I))
have refine_1 : IsQuotientMap (Y := { z : ℂ // z ≠ 0 }) fun (z : ℂ) ↦ Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (cexp z) sorry
Tactic: refine Topology.IsQuotientMap.isAddQuotientCoveringMap_of_addSubgroup ?_
    _ ⟨NormedSpace.discreteTopology_zmultiples _⟩ fun {z _} ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.CoveringMap (goal)
Goal:
refine_1 : IsQuotientMap (Y := { z : ℂ // z ≠ 0 }) fun (z : ℂ) ↦ Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (cexp z) ⋯
⊢ IsAddQuotientCoveringMap (X := { z : ℂ // z ≠ 0 }) (fun (z : ℂ) ↦ Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (cexp z) ⋯)
    ↥(AddSubgroup.zmultiples (2 * (↑Real.pi : ℂ) * I))
have refine_2 : ∀ {z x : ℂ},
  Eq (α := { z : ℂ // z ≠ 0 }) (Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (cexp z) sorry)
      (Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (cexp x) sorry) ↔
    Membership.mem (γ := AddSubgroup ℂ) (AddSubgroup.zmultiples (2 * (↑Real.pi : ℂ) * I)) (x + -z)
Tactic: refine Topology.IsQuotientMap.isAddQuotientCoveringMap_of_addSubgroup ?_
    _ ⟨NormedSpace.discreteTopology_zmultiples _⟩ fun {z _} ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.CoveringMap (goal)
Goal:
⊢ IsQuotientMap (Y := { z : ℂ // z ≠ 0 }) fun (z : ℂ) ↦ Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (cexp z) ⋯
have refine_1 : IsOpenMap (Y := { z : ℂ // z ≠ 0 }) fun (z : ℂ) ↦ Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (cexp z) sorry
Tactic: refine IsOpenMap.isQuotientMap ?_ (by fun_prop) fun z ↦ ⟨_, Subtype.ext (exp_log z.2)⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.CoveringMap (goal)
Goal:
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)
have refine_2 : cexp z = 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CoveringMap (goal)
Goal:
z x : ℂ
refine_2 :
  cexp z = cexp x ↔ Membership.mem (γ := AddSubgroup ℂ) (AddSubgroup.zmultiples (2 * (↑Real.pi : ℂ) * I)) (x + -z)
⊢ 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)
have refine_2₁ : cexp x = cexp z ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CoveringMap (goal)
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)
⊢ 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)
have refine_2₂ : (∃ (n : ℤ), x = z + (↑n : ℂ) * (2 * (↑Real.pi : ℂ) * I)) ↔
  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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CoveringMap (goal)
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)
⊢ 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)
have refine_2₃ : (∃ (n : ℤ), x = z + (↑n : ℂ) * (2 * (↑Real.pi : ℂ) * I)) ↔ ∃ (k : ℤ), k • (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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CoveringMap (goal)
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
⊢ 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)
have refine_2₄ : (∃ (n : ℤ), x = z + (↑n : ℂ) * (2 * (↑Real.pi : ℂ) * I)) ↔ ∃ (k : ℤ), k • (2 * (↑Real.pi : ℂ) * I) + z = x
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CoveringMap (goal)
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
⊢ 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)
have refine_2₅ : (∃ (n : ℤ), x = z + (↑n : ℂ) * (2 * (↑Real.pi : ℂ) * I)) ↔ ∃ (k : ℤ), x = k • (2 * (↑Real.pi : ℂ) * I) + 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CoveringMap (goal)
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
⊢ 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)
have refine_2₆ : (∃ (n : ℤ), x = z + (↑n : ℂ) * (2 * (↑Real.pi : ℂ) * I)) ↔ ∃ (k : ℤ), x = z + k • (2 * (↑Real.pi : ℂ) * I)
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CoveringMap (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
p : 𝕜[X]
⊢ IsCoveringMapOn (X := 𝕜) (fun (x : 𝕜) ↦ eval x p)
    ((fun (x : 𝕜) ↦ eval x p) '' {k : 𝕜 | eval k ((derivative : (a : 𝕜[X]) → 𝕜[X]) p) = 0})ᶜ
have refine : ∀ (x : 𝕜)
  (hx :
    Membership.mem (γ := Set 𝕜) ((fun (x : 𝕜) ↦ eval x p) '' {k : 𝕜 | eval k ((derivative : (a : 𝕜[X]) → 𝕜[X]) p) = 0})ᶜ
      x),
  Set.Finite (α := 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ eval x p) {x})
Tactic: refine p.isClosedMap_eval.isCoveringMapOn_of_openPartialHomeomorph (fun x hx ↦ ?_)
    fun x hx ↦ ⟨_, ((p.hasStrictDerivAt x).hasStrictFDerivAt_equiv
      fun h ↦ hx ⟨x, h, rfl⟩).mem_toOpenPartialHomeomorph_source, by simp⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.CoveringMap (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
p : 𝕜[X]
x : 𝕜
hx :
  Membership.mem (γ := Set 𝕜) ((fun (x : 𝕜) ↦ eval x p) '' {k : 𝕜 | eval k ((derivative : (a : 𝕜[X]) → 𝕜[X]) p) = 0})ᶜ x
⊢ Set.Finite (α := 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ eval x p) {x})
have inl : ∀
  (hx :
    Membership.mem (γ := Set 𝕜)
      ((fun (x_1 : 𝕜) ↦ eval x_1 ((C : (a : 𝕜) → 𝕜[X]) x)) ''
          {k : 𝕜 | eval k ((derivative : (a : 𝕜[X]) → 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) x)) = 0})ᶜ
      x),
  Set.Finite (α := 𝕜) (Set.preimage (β := 𝕜) (fun (x_1 : 𝕜) ↦ eval x_1 ((C : (a : 𝕜) → 𝕜[X]) x)) {x})
Tactic: obtain rfl | ne := eq_or_ne p (C x)
Cleared hypotheses: p, hx
-- Lean 4 proof step from Mathlib.Analysis.Complex.CoveringMap (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
p : 𝕜[X]
x : 𝕜
hx :
  Membership.mem (γ := Set 𝕜) ((fun (x : 𝕜) ↦ eval x p) '' {k : 𝕜 | eval k ((derivative : (a : 𝕜[X]) → 𝕜[X]) p) = 0})ᶜ x
inl :
  ∀
    (hx :
      Membership.mem (γ := Set 𝕜)
        ((fun (x_1 : 𝕜) ↦ eval x_1 ((C : (a : 𝕜) → 𝕜[X]) x)) ''
            {k : 𝕜 | eval k ((derivative : (a : 𝕜[X]) → 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) x)) = 0})ᶜ
        x),
    Set.Finite (α := 𝕜) (Set.preimage (β := 𝕜) (fun (x_1 : 𝕜) ↦ eval x_1 ((C : (a : 𝕜) → 𝕜[X]) x)) {x})
⊢ Set.Finite (α := 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ eval x p) {x})
have inr : ∀ (ne : p ≠ (C : (a : 𝕜) → 𝕜[X]) x), Set.Finite (α := 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ eval x p) {x})
Tactic: obtain rfl | ne := eq_or_ne p (C x)
-- Lean 4 proof step from Mathlib.Analysis.Complex.CoveringMap (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
⊢ IsCoveringMapOn (X := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ
have h : ∀ (x : 𝕜), x ^ n = eval x (HPow.hPow (α := 𝕜[X]) X n)
Tactic: convert! (X ^ n).isCoveringMapOn_eval.mono fun x' h ↦ _ with x
-- Lean 4 proof step from Mathlib.Analysis.Complex.CoveringMap (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
h : ∀ (x : 𝕜), x ^ n = eval x (HPow.hPow (α := 𝕜[X]) X n)
convert_2 : ProperSpace 𝕜
⊢ IsCoveringMapOn (X := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ
have convert_5 : ∀ (x' : 𝕜) (h : Membership.mem (γ := Set 𝕜) {0}ᶜ x'),
  Membership.mem (γ := Set 𝕜)
    ((fun (x : 𝕜) ↦ eval x (HPow.hPow (α := 𝕜[X]) X n)) ''
        {k : 𝕜 | eval k ((derivative : (a : 𝕜[X]) → 𝕜[X]) (HPow.hPow (α := 𝕜[X]) X n)) = 0})ᶜ
    x'
Tactic: convert! (X ^ n).isCoveringMapOn_eval.mono fun x' h ↦ _ with x
-- Lean 4 proof step from Mathlib.Analysis.Complex.CoveringMap (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
⊢ IsCoveringMap (X := { x : 𝕜 // x ≠ 0 }) fun (x : { x : 𝕜 // x ≠ 0 }) ↦
    Subtype.mk (p := fun (x : 𝕜) ↦ x ≠ 0) ((↑x : 𝕜) ^ n) ⋯
have n₁ : Eq (α := Set 𝕜) {x : 𝕜 | x ≠ 0} (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ)
Tactic: convert!
    (isCoveringMapOn_npow n hn).isCoveringMap_restrictPreimage.comp_homeomorph
      (.setCongr (s := {x | x ≠ 0}) _) using 1