awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ Eq (α := Set 𝕜) {x : 𝕜 | x ≠ 0} (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ)
have h : ∀ (x : 𝕜),
  Membership.mem (γ := Set 𝕜) {x : 𝕜 | x ≠ 0} x ↔
    Membership.mem (γ := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) x
Tactic: ext
-- 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 inl : ∀ (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) (HPow.hPow (β := ℤ) (↑x : 𝕜) (↑n : ℤ)) sorry
Tactic: obtain ⟨n, rfl | rfl⟩ := n.eq_nat_or_neg
Cleared hypotheses: n, hn
-- 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
inl :
  ∀ (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) (HPow.hPow (β := ℤ) (↑x : 𝕜) (↑n : ℤ)) ⋯
⊢ IsCoveringMap (X := { x : 𝕜 // x ≠ 0 }) fun (x : { x : 𝕜 // x ≠ 0 }) ↦
    Subtype.mk (p := fun (x : 𝕜) ↦ x ≠ 0) ((↑x : 𝕜) ^ n) ⋯
have inr : ∀ (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) (HPow.hPow (β := ℤ) (↑x : 𝕜) (-(↑n : ℤ))) sorry
Tactic: obtain ⟨n, rfl | rfl⟩ := n.eq_nat_or_neg
Cleared hypotheses: n, hn
-- 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) (HPow.hPow (β := ℤ) (↑x : 𝕜) (↑n : ℤ)) ⋯
have h : ∀ (x : { x : 𝕜 // x ≠ 0 }), HPow.hPow (β := ℤ) (↑x : 𝕜) (↑n : ℤ) = (↑x : 𝕜) ^ n
Tactic: convert! isCoveringMap_npow n _
-- 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 : 𝕜 // x ≠ 0 }), HPow.hPow (β := ℤ) (↑x : 𝕜) (↑n : ℤ) = (↑x : 𝕜) ^ n
inl : ProperSpace 𝕜
⊢ IsCoveringMap (X := { x : 𝕜 // x ≠ 0 }) fun (x : { x : 𝕜 // x ≠ 0 }) ↦
    Subtype.mk (p := fun (x : 𝕜) ↦ x ≠ 0) (HPow.hPow (β := ℤ) (↑x : 𝕜) (↑n : ℤ)) ⋯
have inl₁ : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
Tactic: convert! isCoveringMap_npow n _
-- 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) (HPow.hPow (β := ℤ) (↑x : 𝕜) (-(↑n : ℤ))) ⋯
have h : ∀ (x : { x : 𝕜 // x ≠ 0 }),
  HPow.hPow (β := ℤ) (↑x : 𝕜) (-(↑n : ℤ)) =
    (↑(((fun (x : { x : 𝕜 // x ≠ 0 }) ↦ Subtype.mk (p := fun (x : 𝕜) ↦ x ≠ 0) ((↑x : 𝕜) ^ n) sorry) ∘
            (⇑(Homeomorph.inv₀ 𝕜) : (a : { g : 𝕜 // g ≠ 0 }) → { x : 𝕜 // x ≠ 0 }))
          x) :
      𝕜)
Tactic: convert! (isCoveringMap_npow n _).comp_homeomorph (.inv₀ 𝕜)
-- 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 : 𝕜 // x ≠ 0 }),
    HPow.hPow (β := ℤ) (↑x : 𝕜) (-(↑n : ℤ)) =
      (↑(((fun (x : { x : 𝕜 // x ≠ 0 }) ↦ Subtype.mk (p := fun (x : 𝕜) ↦ x ≠ 0) ((↑x : 𝕜) ^ n) ⋯) ∘
              (⇑(Homeomorph.inv₀ 𝕜) : (a : { g : 𝕜 // g ≠ 0 }) → { x : 𝕜 // x ≠ 0 }))
            x) :
        𝕜)
⊢ IsCoveringMap (X := { x : 𝕜 // x ≠ 0 }) fun (x : { x : 𝕜 // x ≠ 0 }) ↦
    Subtype.mk (p := fun (x : 𝕜) ↦ x ≠ 0) (HPow.hPow (β := ℤ) (↑x : 𝕜) (-(↑n : ℤ))) ⋯
have inr : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
Tactic: convert! (isCoveringMap_npow n _).comp_homeomorph (.inv₀ 𝕜)
-- Lean 4 proof step from Mathlib.Analysis.Complex.CoveringMap (hypothesis)
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 this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
Tactic: have (x : 𝕜) : x ^ n = 0 ↔ x = 0 := zpow_eq_zero_iff (by aesop)
-- 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
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
⊢ IsCoveringMapOn (X := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ
have refine_1 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ)
Tactic: refine .of_isCoveringMap_restrictPreimage _ (by simp) ?_ ?_
-- 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
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
refine_1 :
  IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ)
⊢ IsCoveringMapOn (X := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ
have refine_2 : IsCoveringMap (E := (↑(Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) : Type u_1))
  (Set.restrictPreimage {0}ᶜ fun (x : 𝕜) ↦ x ^ n)
Tactic: refine .of_isCoveringMap_restrictPreimage _ (by simp) ?_ ?_
-- 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
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ)
have h : Eq (α := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) {0}ᶜ
Tactic: convert! isClosed_singleton (x := (0 : 𝕜)).isOpen_compl using 1
-- 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
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
⊢ Eq (α := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) {0}ᶜ
have h : ∀ (x : 𝕜),
  Membership.mem (γ := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) x ↔ Membership.mem (γ := Set 𝕜) {0}ᶜ x
Tactic: ext
-- 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
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
⊢ IsCoveringMap (E := (↑(Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) : Type u_1))
    (Set.restrictPreimage {0}ᶜ fun (x : 𝕜) ↦ x ^ n)
have refine_2 : Eq.{u_1 + 1} (α := 𝕜 → Prop)
  (fun (x : 𝕜) ↦ Membership.mem (γ := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) x) fun (x : 𝕜) ↦ x ≠ 0
Tactic: convert! (isCoveringMap_zpow n hn).comp_homeomorph (.ofEqSubtypes _) using 1
-- 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
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
⊢ Eq.{u_1 + 1} (α := 𝕜 → Prop)
    (fun (x : 𝕜) ↦ Membership.mem (γ := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) x) fun (x : 𝕜) ↦ x ≠ 0
have refine_2 : ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) x ↔ x ≠ 0
Tactic: ext
-- 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
surj : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ x ^ n
⊢ IsQuotientCoveringMap (X := 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ x ^ n) ↥(MonoidHom.ker (M := 𝕜ˣ) (powMonoidHom n))
have rw : IsQuotientCoveringMap (X := 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ x ^ n) ↥(rootsOfUnity n 𝕜 : Subgroup 𝕜ˣ)
Tactic: rw [← rootsOfUnity_eq_ker]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CoveringMap (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
surj : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ x ^ n
⊢ IsQuotientCoveringMap (X := 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ x ^ n) ↥(rootsOfUnity n 𝕜 : Subgroup 𝕜ˣ)
have this : NeZero n
Tactic: have : NeZero n := ⟨by aesop⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.CoveringMap (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
surj : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ x ^ n
this : NeZero n
⊢ IsQuotientCoveringMap (X := 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ x ^ n) ↥(rootsOfUnity n 𝕜 : Subgroup 𝕜ˣ)
have this₁ : IsQuotientMap (X := (↑(Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) : Type u_1))
  (Set.restrictPreimage {0}ᶜ fun (x : 𝕜) ↦ x ^ n)
Tactic: have := ((isClosedMap_pow 𝕜 n).restrictPreimage {0}ᶜ).isQuotientMap
    (by fun_prop) (.restrictPreimage _ surj)
-- 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
surj : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ x ^ n
this_1 : NeZero n
this :
  IsQuotientMap (X := (↑(Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) : Type u_1))
    (Set.restrictPreimage {0}ᶜ fun (x : 𝕜) ↦ x ^ n)
e : 𝕜ˣ ≃ₜ { g : 𝕜 // g ≠ 0 } := unitsHomeomorphNeZero
⊢ IsQuotientMap (Y := 𝕜ˣ) fun (x : 𝕜ˣ) ↦ x ^ n
have h : ∀ (x : 𝕜ˣ),
  x ^ n =
    Function.comp (β := (↑(Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) : Type u_1))
      ((⇑e.symm : (a : { g : 𝕜 // g ≠ 0 }) → 𝕜ˣ) ∘ Set.restrictPreimage {0}ᶜ fun (x : 𝕜) ↦ x ^ n)
      (⇑(e.trans
            (Homeomorph.ofEqSubtypes (p := fun (g : 𝕜) ↦ g ≠ 0) (q := fun (x : 𝕜) ↦
              Membership.mem (γ := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) x) sorry)) :
        (a : 𝕜ˣ) → { x : 𝕜 // x ∈ (fun (x : 𝕜) ↦ x ^ n) ⁻¹' {0}ᶜ })
      x
Tactic: convert! (e.symm.isQuotientMap.comp this).comp (e.trans (.ofEqSubtypes _)).isQuotientMap
-- 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
surj : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ x ^ n
this_1 : NeZero n
this :
  IsQuotientMap (X := (↑(Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) : Type u_1))
    (Set.restrictPreimage {0}ᶜ fun (x : 𝕜) ↦ x ^ n)
e : 𝕜ˣ ≃ₜ { g : 𝕜 // g ≠ 0 } := unitsHomeomorphNeZero
h :
  ∀ (x : 𝕜ˣ),
    x ^ n =
      Function.comp (β := (↑(Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) : Type u_1))
        ((⇑e.symm : (a : { g : 𝕜 // g ≠ 0 }) → 𝕜ˣ) ∘ Set.restrictPreimage {0}ᶜ fun (x : 𝕜) ↦ x ^ n)
        (⇑(e.trans
              (Homeomorph.ofEqSubtypes (p := fun (g : 𝕜) ↦ g ≠ 0) (q := fun (x : 𝕜) ↦
                Membership.mem (γ := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) x) ⋯)) :
          (a : 𝕜ˣ) → { x : 𝕜 // x ∈ (fun (x : 𝕜) ↦ x ^ n) ⁻¹' {0}ᶜ })
        x
⊢ IsQuotientMap (Y := 𝕜ˣ) fun (x : 𝕜ˣ) ↦ x ^ n
have convert! : Eq.{u_1 + 1} (α := 𝕜 → Prop) (fun (g : 𝕜) ↦ g ≠ 0) fun (x : 𝕜) ↦
  Membership.mem (γ := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) x
Tactic: convert! (e.symm.isQuotientMap.comp this).comp (e.trans (.ofEqSubtypes _)).isQuotientMap
-- 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
surj : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ x ^ n
this_1 : NeZero n
this :
  IsQuotientMap (X := (↑(Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) : Type u_1))
    (Set.restrictPreimage {0}ᶜ fun (x : 𝕜) ↦ x ^ n)
e : 𝕜ˣ ≃ₜ { g : 𝕜 // g ≠ 0 } := unitsHomeomorphNeZero
⊢ Eq.{u_1 + 1} (α := 𝕜 → Prop) (fun (g : 𝕜) ↦ g ≠ 0) fun (x : 𝕜) ↦
    Membership.mem (γ := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) x
have h : ∀ (x : 𝕜), x ≠ 0 ↔ Membership.mem (γ := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Complex.CoveringMap (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
surj : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ x ^ n
this_1 : NeZero n
this :
  IsQuotientMap (X := (↑(Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) : Type u_1))
    (Set.restrictPreimage {0}ᶜ fun (x : 𝕜) ↦ x ^ n)
⊢ IsQuotientCoveringMap (X := 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ x ^ n) ↥(rootsOfUnity n 𝕜 : Subgroup 𝕜ˣ)
have this₁ : IsQuotientMap (Y := 𝕜ˣ) fun (x : 𝕜ˣ) ↦ x ^ n
Tactic: have : IsQuotientMap fun x : 𝕜ˣ ↦ x ^ n := by
    let e := unitsHomeomorphNeZero (G₀ := 𝕜)
    convert! (e.symm.isQuotientMap.comp this).comp (e.trans (.ofEqSubtypes _)).isQuotientMap
    · exact (e.left_inv _).symm
    · ext; simp [NeZero.ne]
-- 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
surj : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ x ^ n
this_1 : NeZero n
this_2 :
  IsQuotientMap (X := (↑(Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) : Type u_1))
    (Set.restrictPreimage {0}ᶜ fun (x : 𝕜) ↦ x ^ n)
this : IsQuotientMap (Y := 𝕜ˣ) fun (x : 𝕜ˣ) ↦ x ^ n
⊢ IsQuotientCoveringMap (X := 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ x ^ n) ↥(rootsOfUnity n 𝕜 : Subgroup 𝕜ˣ)
have refine : ∀ {e₁ e₂ : 𝕜ˣ}, e₁ ^ n = e₂ ^ n ↔ Membership.mem (γ := Subgroup 𝕜ˣ) (rootsOfUnity n 𝕜 : Subgroup 𝕜ˣ) (e₂ * e₁⁻¹)
Tactic: refine this.isQuotientCoveringMap_of_subgroup _
    (Set.Finite.isDiscrete <| inferInstanceAs (Finite (rootsOfUnity ..))) ?_
-- 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
surj : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ x ^ n
⊢ IsQuotientCoveringMap (X := 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ x ^ n) ↥(MonoidHom.ker (M := 𝕜ˣ) (zpowGroupHom n))
have inl : ∀ (n : ℕ) (hn : Ne.{u_1 + 1} (α := 𝕜) (↑(↑n : ℤ) : 𝕜) 0)
  (surj : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ HPow.hPow (β := ℤ) x (↑n : ℤ)),
  IsQuotientCoveringMap (X := 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ HPow.hPow (β := ℤ) x (↑n : ℤ))
    ↥(MonoidHom.ker (M := 𝕜ˣ) (zpowGroupHom (↑n : ℤ)))
Tactic: obtain ⟨n, rfl | rfl⟩ := n.eq_nat_or_neg
Cleared hypotheses: n, hn, surj
-- 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
surj : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ x ^ n
inl :
  ∀ (n : ℕ) (hn : Ne.{u_1 + 1} (α := 𝕜) (↑(↑n : ℤ) : 𝕜) 0)
    (surj : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ HPow.hPow (β := ℤ) x (↑n : ℤ)),
    IsQuotientCoveringMap (X := 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ HPow.hPow (β := ℤ) x (↑n : ℤ))
      ↥(MonoidHom.ker (M := 𝕜ˣ) (zpowGroupHom (↑n : ℤ)))
⊢ IsQuotientCoveringMap (X := 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ x ^ n) ↥(MonoidHom.ker (M := 𝕜ˣ) (zpowGroupHom n))
have inr : ∀ (n : ℕ) (hn : Ne.{u_1 + 1} (α := 𝕜) (↑(-(↑n : ℤ)) : 𝕜) 0)
  (surj : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ HPow.hPow (β := ℤ) x (-(↑n : ℤ))),
  IsQuotientCoveringMap (X := 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ HPow.hPow (β := ℤ) x (-(↑n : ℤ)))
    ↥(MonoidHom.ker (M := 𝕜ˣ) (zpowGroupHom (-(↑n : ℤ))))
Tactic: obtain ⟨n, rfl | rfl⟩ := n.eq_nat_or_neg
Cleared hypotheses: n, hn, surj
-- 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
surj : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ HPow.hPow (β := ℤ) x (-(↑n : ℤ))
⊢ Eq.{u_1 + 1} (α := Subgroup 𝕜ˣ) (MonoidHom.ker (M := 𝕜ˣ) (zpowGroupHom (-(↑n : ℤ))))
    (MonoidHom.ker (M := 𝕜ˣ) (powMonoidHom n))
have h : ∀ (x : 𝕜ˣ),
  Membership.mem (γ := Subgroup 𝕜ˣ) (MonoidHom.ker (M := 𝕜ˣ) (zpowGroupHom (-(↑n : ℤ)))) x ↔
    Membership.mem (γ := Subgroup 𝕜ˣ) (MonoidHom.ker (M := 𝕜ˣ) (powMonoidHom n)) x
Tactic: ext
-- 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
surj : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ HPow.hPow (β := ℤ) x (-(↑n : ℤ))
⊢ IsQuotientCoveringMap (X := 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ HPow.hPow (β := ℤ) x (-(↑n : ℤ)))
    ↥(MonoidHom.ker (M := 𝕜ˣ) (zpowGroupHom (-(↑n : ℤ))))
have inr : IsQuotientCoveringMap (X := 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ HPow.hPow (β := ℤ) x (-(↑n : ℤ)))
  ↥(MonoidHom.ker (M := 𝕜ˣ) (powMonoidHom n))
Tactic: rw [show (zpowGroupHom (α := 𝕜ˣ) (-n)).ker = (powMonoidHom n).ker by ext; simp]
-- 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
surj : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ HPow.hPow (β := ℤ) x (-(↑n : ℤ))
⊢ IsQuotientCoveringMap (X := 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ HPow.hPow (β := ℤ) x (-(↑n : ℤ)))
    ↥(MonoidHom.ker (M := 𝕜ˣ) (powMonoidHom n))
have h : Eq.{u_1 + 1} (α := 𝕜ˣ → 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ HPow.hPow (β := ℤ) x (-(↑n : ℤ)))
  (Function.comp (β := 𝕜ˣ) (⇑(Homeomorph.inv 𝕜ˣ) : (a : 𝕜ˣ) → 𝕜ˣ) fun (x : 𝕜ˣ) ↦ x ^ n)
Tactic: convert! (isQuotientCoveringMap_npow n (by aesop) _).homeomorph_comp (.inv 𝕜ˣ) using 1
-- 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
surj : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ HPow.hPow (β := ℤ) x (-(↑n : ℤ))
h :
  Eq.{u_1 + 1} (α := 𝕜ˣ → 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ HPow.hPow (β := ℤ) x (-(↑n : ℤ)))
    (Function.comp (β := 𝕜ˣ) (⇑(Homeomorph.inv 𝕜ˣ) : (a : 𝕜ˣ) → 𝕜ˣ) fun (x : 𝕜ˣ) ↦ x ^ n)
⊢ IsQuotientCoveringMap (X := 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ HPow.hPow (β := ℤ) x (-(↑n : ℤ)))
    ↥(MonoidHom.ker (M := 𝕜ˣ) (powMonoidHom n))
have inr : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ x ^ n
Tactic: convert! (isQuotientCoveringMap_npow n (by aesop) _).homeomorph_comp (.inv 𝕜ˣ) using 1
-- 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
surj : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ HPow.hPow (β := ℤ) x (-(↑n : ℤ))
⊢ Eq.{u_1 + 1} (α := 𝕜ˣ → 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ HPow.hPow (β := ℤ) x (-(↑n : ℤ)))
    (Function.comp (β := 𝕜ˣ) (⇑(Homeomorph.inv 𝕜ˣ) : (a : 𝕜ˣ) → 𝕜ˣ) fun (x : 𝕜ˣ) ↦ x ^ n)
have h : ∀ (x : 𝕜ˣ),
  (↑(HPow.hPow (β := ℤ) x (-(↑n : ℤ))) : 𝕜) =
    (↑(Function.comp (β := 𝕜ˣ) (⇑(Homeomorph.inv 𝕜ˣ) : (a : 𝕜ˣ) → 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ x ^ n) x) : 𝕜)
Tactic: ext
-- 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
surj : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ HPow.hPow (β := ℤ) x (-(↑n : ℤ))
⊢ Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ x ^ n
have h : ∀ (x : 𝕜), x ^ n = (Inv.inv ∘ fun (x : 𝕜) ↦ HPow.hPow (β := ℤ) x (-(↑n : ℤ))) x
Tactic: convert! inv_involutive.surjective.comp surj
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
z : ℂ
n : ℕ
hn : ‖z‖ < (↑n : ℝ)
hn0 : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ ‖z‖ / (↑n : ℝ) < 1
have rwa : ‖z‖ < HMul.hMul (α := ℝ) 1 (↑n : ℝ)
Tactic: rwa [div_lt_iff₀ hn0, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
z : ℂ
n : ℕ
hn : ‖z‖ < (↑n : ℝ)
hn0 : LT.lt (α := ℝ) 0 (↑n : ℝ)
m : ℕ
hm : n ≤ m
⊢ |‖z ^ m.succ / (↑m.succ.factorial : ℂ)‖| ≤ ‖z‖ / (↑n : ℝ) * |‖z ^ m / (↑m.factorial : ℂ)‖|
have rw : ‖z‖ / (↑m.succ : ℝ) * ‖z ^ m / (↑m.factorial : ℂ)‖ ≤ ‖z‖ / (↑n : ℝ) * ‖z ^ m / (↑m.factorial : ℂ)‖
Tactic: rw [abs_norm, abs_norm, Nat.factorial_succ, pow_succ', mul_comm m.succ, Nat.cast_mul,
        ← div_div, mul_div_assoc, mul_div_right_comm, Complex.norm_mul, Complex.norm_div,
        norm_natCast]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
z : ℂ
n : ℕ
hn : ‖z‖ < (↑n : ℝ)
hn0 : LT.lt (α := ℝ) 0 (↑n : ℝ)
m : ℕ
hm : n ≤ m
⊢ ‖z‖ / (↑m.succ : ℝ) * ‖z ^ m / (↑m.factorial : ℂ)‖ ≤ ‖z‖ / (↑n : ℝ) * ‖z ^ m / (↑m.factorial : ℂ)‖
have hbc : n ≤ m.succ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
⊢ cexp 0 = 1
have rw : (exp' 0).lim = 1
Tactic: rw [exp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
⊢ (exp' 0).lim = 1
have refine : ∀ (ε : ℝ) (ε0 : ε > 0) (j : ℕ) (hj : j ≥ 1), ‖(↑(exp' 0 - const (fun (x : ℂ) ↦ ‖x‖) 1) : ℕ → ℂ) j‖ < ε
Tactic: refine lim_eq_of_equiv_const fun ε ε0 => ⟨1, fun j hj => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : j ≥ 1
⊢ ‖(↑(exp' 0 - const (fun (x : ℂ) ↦ ‖x‖) 1) : ℕ → ℂ) j‖ < ε
have h : ‖(↑(exp' 0 - const (fun (x : ℂ) ↦ ‖x‖) 1) : ℕ → ℂ) j‖ = 0
Tactic: convert! (config := .unfoldSameFun) ε0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : j ≥ 1
⊢ ‖(↑(exp' 0 - const (fun (x : ℂ) ↦ ‖x‖) 1) : ℕ → ℂ) j‖ = 0
have h : ∀ (hj : GE.ge (α := ℕ) 0 1), ‖(↑(exp' 0 - const (fun (x : ℂ) ↦ ‖x‖) 1) : ℕ → ℂ) 0‖ = 0
Tactic: rcases j with - | j
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : j ≥ 1
h : ∀ (hj : GE.ge (α := ℕ) 0 1), ‖(↑(exp' 0 - const (fun (x : ℂ) ↦ ‖x‖) 1) : ℕ → ℂ) 0‖ = 0
⊢ ‖(↑(exp' 0 - const (fun (x : ℂ) ↦ ‖x‖) 1) : ℕ → ℂ) j‖ = 0
have h₁ : ∀ (j : ℕ) (hj : j + 1 ≥ 1), ‖(↑(exp' 0 - const (fun (x : ℂ) ↦ ‖x‖) 1) : ℕ → ℂ) (j + 1)‖ = 0
Tactic: rcases j with - | j
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
ε : ℝ
ε0 : ε > 0
j : ℕ
ih : ∀ (hj : j + 1 ≥ 1), ‖HSub.hSub (α := ℂ) (∑ m ∈ range (j + 1), HPow.hPow (α := ℂ) 0 m / (↑m.factorial : ℂ)) 1‖ = 0
hj : j + 1 + 1 ≥ 1
⊢ ‖HSub.hSub (α := ℂ) (∑ m ∈ range (j + 1 + 1), HPow.hPow (α := ℂ) 0 m / (↑m.factorial : ℂ)) 1‖ = 0
have h : ‖HSub.hSub (α := ℂ) (∑ m ∈ range (j + 1 + 1), HPow.hPow (α := ℂ) 0 m / (↑m.factorial : ℂ)) 1‖ =
  ‖HSub.hSub (α := ℂ) (∑ m ∈ range (j + 1), HPow.hPow (α := ℂ) 0 m / (↑m.factorial : ℂ)) 1‖
Tactic: rw [← ih (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
ε : ℝ
ε0 : ε > 0
j : ℕ
ih : ∀ (hj : j + 1 ≥ 1), ‖HSub.hSub (α := ℂ) (∑ m ∈ range (j + 1), HPow.hPow (α := ℂ) 0 m / (↑m.factorial : ℂ)) 1‖ = 0
hj : j + 1 + 1 ≥ 1
⊢ ‖HSub.hSub (α := ℂ) (∑ m ∈ range (j + 1 + 1), HPow.hPow (α := ℂ) 0 m / (↑m.factorial : ℂ)) 1‖ =
    ‖HSub.hSub (α := ℂ) (∑ m ∈ range (j + 1), HPow.hPow (α := ℂ) 0 m / (↑m.factorial : ℂ)) 1‖
have h : ‖∑ m ∈ range j, HPow.hPow (α := ℂ) 0 m / (↑m.factorial : ℂ) + HPow.hPow (α := ℂ) 0 j / (↑j.factorial : ℂ) +
        HPow.hPow (α := ℂ) 0 j * 0 / (↑(j + 1).factorial : ℂ) -
      1‖ =
  ‖∑ m ∈ range j, HPow.hPow (α := ℂ) 0 m / (↑m.factorial : ℂ) + HPow.hPow (α := ℂ) 0 j / (↑j.factorial : ℂ) - 1‖
Tactic: simp only [sum_range_succ, pow_succ]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : j + 1 ≥ 1
⊢ ‖HSub.hSub (α := ℂ) (∑ m ∈ range (j + 1), HPow.hPow (α := ℂ) 0 m / (↑m.factorial : ℂ)) 1‖ = 0
have h : ∀ (hj : HAdd.hAdd (α := ℕ) 0 1 ≥ 1),
  ‖HSub.hSub (α := ℂ) (∑ m ∈ range (HAdd.hAdd (α := ℕ) 0 1), HPow.hPow (α := ℂ) 0 m / (↑m.factorial : ℂ)) 1‖ = 0
Tactic: induction j with
    | zero => simp
    | succ j ih =>
      rw [← ih (by simp)]
      simp only [sum_range_succ, pow_succ]
      simp
Cleared hypotheses: j, hj