awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.CoveringMap
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
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

Tactic:
exact (e.left_inv _).symm

Premises used: Homeomorph.toEquiv, Eq.symm, Equiv.left_inv
-- Module: Mathlib.Analysis.Complex.CoveringMap
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 ≠ 0 ↔ Membership.mem (γ := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) x
⊢ Eq.{u_1 + 1} (α := 𝕜 → Prop) (fun (g : 𝕜) ↦ g ≠ 0) fun (x : 𝕜) ↦
    Membership.mem (γ := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) x

Tactic:
ext
-- Module: Mathlib.Analysis.Complex.CoveringMap
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
x : 𝕜
⊢ x ≠ 0 ↔ Membership.mem (γ := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) x

Tactic:
simp [NeZero.ne]

Premises used: NeZero.ne
-- Module: Mathlib.Analysis.Complex.CoveringMap
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)
⊢ 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]
-- Module: Mathlib.Analysis.Complex.CoveringMap
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 𝕜ˣ)

Tactic:
this.isQuotientCoveringMap_of_subgroup _
    (Set.Finite.isDiscrete <| inferInstanceAs (Finite (rootsOfUnity ..))) ?_

Premises used: Topology.IsQuotientMap.isQuotientCoveringMap_of_subgroup, Membership.mem, Subtype, Finite.of_fintype, rootsOfUnity, Set.Finite.isDiscrete
-- Module: Mathlib.Analysis.Complex.CoveringMap
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
refine :
  ∀ {e₁ e₂ : 𝕜ˣ}, e₁ ^ n = e₂ ^ n ↔ Membership.mem (γ := Subgroup 𝕜ˣ) (rootsOfUnity n 𝕜 : Subgroup 𝕜ˣ) (e₂ * e₁⁻¹)
⊢ IsQuotientCoveringMap (X := 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ x ^ n) ↥(rootsOfUnity n 𝕜 : Subgroup 𝕜ˣ)

Tactic:
refine this.isQuotientCoveringMap_of_subgroup _
    (Set.Finite.isDiscrete <| inferInstanceAs (Finite (rootsOfUnity ..))) ?_

Premises used: Topology.IsQuotientMap.isQuotientCoveringMap_of_subgroup, Set.Finite.isDiscrete
-- Module: Mathlib.Analysis.Complex.CoveringMap
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
⊢ ∀ {e₁ e₂ : 𝕜ˣ}, e₁ ^ n = e₂ ^ n ↔ Membership.mem (γ := Subgroup 𝕜ˣ) (rootsOfUnity n 𝕜 : Subgroup 𝕜ˣ) (e₂ * e₁⁻¹)

Tactic:
simp [mul_pow, mul_inv_eq_one, eq_comm]

Premises used: mul_inv_eq_one, eq_comm, mul_pow
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
n : ℕ
inst : NeZero n
⊢ Ne (α := ℂ) (↑n : ℂ) 0

Tactic:
simp [NeZero.ne]

Premises used: NeZero.ne
-- Module: Mathlib.Analysis.Complex.CoveringMap
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 : ℤ)))
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 : ℤ))))
⊢ IsQuotientCoveringMap (X := 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ x ^ n) ↥(MonoidHom.ker (M := 𝕜ˣ) (zpowGroupHom n))

Tactic:
obtain ⟨n, rfl | rfl⟩ := n.eq_nat_or_neg

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.Analysis.Complex.CoveringMap
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 : ℤ)
⊢ Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.CoveringMap
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

Tactic:
simpa using surj
-- Module: Mathlib.Analysis.Complex.CoveringMap
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 : ℤ)))

Tactic:
exact isQuotientCoveringMap_npow n (by aesop) (by simpa using surj)

Premises used: isQuotientCoveringMap_npow
-- Module: Mathlib.Analysis.Complex.CoveringMap
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 :
  ∀ (x : 𝕜ˣ),
    Membership.mem (γ := Subgroup 𝕜ˣ) (MonoidHom.ker (M := 𝕜ˣ) (zpowGroupHom (-(↑n : ℤ)))) x ↔
      Membership.mem (γ := Subgroup 𝕜ˣ) (MonoidHom.ker (M := 𝕜ˣ) (powMonoidHom n)) x
⊢ Eq.{u_1 + 1} (α := Subgroup 𝕜ˣ) (MonoidHom.ker (M := 𝕜ˣ) (zpowGroupHom (-(↑n : ℤ))))
    (MonoidHom.ker (M := 𝕜ˣ) (powMonoidHom n))

Tactic:
ext
-- Module: Mathlib.Analysis.Complex.CoveringMap
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 : ℤ))
x : 𝕜ˣ
⊢ Membership.mem (γ := Subgroup 𝕜ˣ) (MonoidHom.ker (M := 𝕜ˣ) (zpowGroupHom (-(↑n : ℤ)))) x ↔
    Membership.mem (γ := Subgroup 𝕜ˣ) (MonoidHom.ker (M := 𝕜ˣ) (powMonoidHom n)) x

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.CoveringMap
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 : ℤ))
inr :
  IsQuotientCoveringMap (X := 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ HPow.hPow (β := ℤ) x (-(↑n : ℤ)))
    ↥(MonoidHom.ker (M := 𝕜ˣ) (powMonoidHom n))
⊢ IsQuotientCoveringMap (X := 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ HPow.hPow (β := ℤ) x (-(↑n : ℤ)))
    ↥(MonoidHom.ker (M := 𝕜ˣ) (zpowGroupHom (-(↑n : ℤ))))

Tactic:
rw [show (zpowGroupHom (α := 𝕜ˣ) (-n)).ker = (powMonoidHom n).ker by ext; simp]
-- Module: Mathlib.Analysis.Complex.CoveringMap
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 : ℤ))
⊢ Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.CoveringMap
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)
inr : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ x ^ n
⊢ IsQuotientCoveringMap (X := 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ HPow.hPow (β := ℤ) x (-(↑n : ℤ)))
    ↥(MonoidHom.ker (M := 𝕜ˣ) (powMonoidHom n))

Tactic:
convert! (isQuotientCoveringMap_npow n (by aesop) _).homeomorph_comp (.inv 𝕜ˣ) using 1

Premises used: Units, isQuotientCoveringMap_npow, Homeomorph.inv, IsQuotientCoveringMap.homeomorph_comp
-- Module: Mathlib.Analysis.Complex.CoveringMap
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 :
  ∀ (x : 𝕜ˣ),
    (↑(HPow.hPow (β := ℤ) x (-(↑n : ℤ))) : 𝕜) =
      (↑(Function.comp (β := 𝕜ˣ) (⇑(Homeomorph.inv 𝕜ˣ) : (a : 𝕜ˣ) → 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ x ^ n) x) : 𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜ˣ → 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ HPow.hPow (β := ℤ) x (-(↑n : ℤ)))
    (Function.comp (β := 𝕜ˣ) (⇑(Homeomorph.inv 𝕜ˣ) : (a : 𝕜ˣ) → 𝕜ˣ) fun (x : 𝕜ˣ) ↦ x ^ n)

Tactic:
ext
-- Module: Mathlib.Analysis.Complex.CoveringMap
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 : ℤ))
x : 𝕜ˣ
⊢ (↑(HPow.hPow (β := ℤ) x (-(↑n : ℤ))) : 𝕜) =
    (↑(Function.comp (β := 𝕜ˣ) (⇑(Homeomorph.inv 𝕜ˣ) : (a : 𝕜ˣ) → 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ x ^ n) x) : 𝕜)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.CoveringMap
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.{u_1 + 1, u_1 + 1} (α := 𝕜) (β := 𝕜) (Inv.inv ∘ fun (x : 𝕜) ↦ HPow.hPow (β := ℤ) x (-(↑n : ℤ)))

Tactic:
inv_involutive.surjective.comp surj

Premises used: Function.Involutive.surjective, inv_involutive, Function.Surjective.comp
-- Module: Mathlib.Analysis.Complex.CoveringMap
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 : ∀ (x : 𝕜), x ^ n = (Inv.inv ∘ fun (x : 𝕜) ↦ HPow.hPow (β := ℤ) x (-(↑n : ℤ))) x
⊢ Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ x ^ n

Tactic:
convert! inv_involutive.surjective.comp surj

Premises used: Function.Involutive.surjective, inv_involutive, Function.Surjective.comp
-- Module: Mathlib.Analysis.Complex.CoveringMap
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 : ℤ))
x : 𝕜
⊢ x ^ n = (Inv.inv ∘ fun (x : 𝕜) ↦ HPow.hPow (β := ℤ) x (-(↑n : ℤ))) x

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
z : ℂ
n : ℕ
hn : ‖z‖ < (↑n : ℝ)
hn0 : LT.lt (α := ℝ) 0 (↑n : ℝ)
rwa : ‖z‖ < HMul.hMul (α := ℝ) 1 (↑n : ℝ)
rwa₁ rwa₂ rwa₃ rwa₄ : ‖z‖ < (↑n : ℝ)
⊢ ‖z‖ / (↑n : ℝ) < 1

Tactic:
rwa [div_lt_iff₀ hn0, one_mul]

Premises used: div_lt_iff₀, one_mul
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
z : ℂ
n : ℕ
hn : ‖z‖ < (↑n : ℝ)
hn0 : LT.lt (α := ℝ) 0 (↑n : ℝ)
m : ℕ
hm : n ≤ m
rw : ‖z‖ / (↑m.succ : ℝ) * ‖z ^ m / (↑m.factorial : ℂ)‖ ≤ ‖z‖ / (↑n : ℝ) * ‖z ^ m / (↑m.factorial : ℂ)‖
⊢ |‖z ^ m.succ / (↑m.succ.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]

Premises used: Nat.factorial_succ, Complex.norm_natCast, mul_div_assoc, mul_div_right_comm, Complex.norm_div, Nat.cast_mul, mul_comm, abs_norm, div_div, Nat.succ, Complex.norm_mul, pow_succ'
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
z : ℂ
n : ℕ
hn : ‖z‖ < (↑n : ℝ)
hn0 : LT.lt (α := ℝ) 0 (↑n : ℝ)
m : ℕ
hm : n ≤ m
hbc : n ≤ m.succ
⊢ ‖z‖ / (↑m.succ : ℝ) * ‖z ^ m / (↑m.factorial : ℂ)‖ ≤ ‖z‖ / (↑n : ℝ) * ‖z ^ m / (↑m.factorial : ℂ)‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
z : ℂ
n : ℕ
hn : ‖z‖ < (↑n : ℝ)
hn0 : LT.lt (α := ℝ) 0 (↑n : ℝ)
m : ℕ
hm : n ≤ m
⊢ n ≤ m.succ

Tactic:
le_trans hm (Nat.le_succ _)

Premises used: Nat.le_succ, le_trans
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
z : ℂ
n : ℕ
hn : ‖z‖ < (↑n : ℝ)
hn0 : LT.lt (α := ℝ) 0 (↑n : ℝ)
m : ℕ
hm : n ≤ m
⊢ n ≤ m.succ

Tactic:
exact le_trans hm (Nat.le_succ _)

Premises used: Nat.le_succ, le_trans
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
z : ℂ
⊢ IsCauSeq (α := ℝ) (fun (x : ℂ) ↦ ‖x‖) fun (n : ℕ) ↦ ∑ m ∈ range n, z ^ m / (↑m.factorial : ℂ)

Tactic:
(isCauSeq_norm_exp z).of_abv

Premises used: IsCauSeq.of_abv, Complex.isCauSeq_norm_exp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
rw : (exp' 0).lim = 1
⊢ cexp 0 = 1

Tactic:
rw [exp]

Premises used: Complex.exp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
⊢ (exp' 0).lim = 1

Tactic:
lim_eq_of_equiv_const fun ε ε0 => ⟨1, fun j hj => ?_⟩

Premises used: CauSeq.lim_eq_of_equiv_const, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
refine : ∀ (ε : ℝ) (ε0 : ε > 0) (j : ℕ) (hj : j ≥ 1), ‖(↑(exp' 0 - const (fun (x : ℂ) ↦ ‖x‖) 1) : ℕ → ℂ) j‖ < ε
⊢ (exp' 0).lim = 1

Tactic:
refine lim_eq_of_equiv_const fun ε ε0 => ⟨1, fun j hj => ?_⟩

Premises used: CauSeq.lim_eq_of_equiv_const, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : j ≥ 1
⊢ ε > 0

Tactic:
ε0
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : j ≥ 1
h : ‖(↑(exp' 0 - const (fun (x : ℂ) ↦ ‖x‖) 1) : ℕ → ℂ) j‖ = 0
⊢ ‖(↑(exp' 0 - const (fun (x : ℂ) ↦ ‖x‖) 1) : ℕ → ℂ) j‖ < ε

Tactic:
convert! (config := .unfoldSameFun) ε0
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : j ≥ 1
h : ∀ (hj : GE.ge (α := ℕ) 0 1), ‖(↑(exp' 0 - const (fun (x : ℂ) ↦ ‖x‖) 1) : ℕ → ℂ) 0‖ = 0
h₁ : ∀ (j : ℕ) (hj : j + 1 ≥ 1), ‖(↑(exp' 0 - const (fun (x : ℂ) ↦ ‖x‖) 1) : ℕ → ℂ) (j + 1)‖ = 0
⊢ ‖(↑(exp' 0 - const (fun (x : ℂ) ↦ ‖x‖) 1) : ℕ → ℂ) j‖ = 0

Tactic:
rcases j with - | j
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
ε : ℝ
ε0 : ε > 0
hj : GE.ge (α := ℕ) 0 1
⊢ ‖(↑(exp' 0 - const (fun (x : ℂ) ↦ ‖x‖) 1) : ℕ → ℂ) 0‖ = 0

Tactic:
absurd hj (not_le_of_gt zero_lt_one)

Premises used: zero_lt_one, absurd, not_le_of_gt
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
ε : ℝ
ε0 : ε > 0
hj : GE.ge (α := ℕ) 0 1
⊢ ‖(↑(exp' 0 - const (fun (x : ℂ) ↦ ‖x‖) 1) : ℕ → ℂ) 0‖ = 0

Tactic:
exact absurd hj (not_le_of_gt zero_lt_one)

Premises used: zero_lt_one, absurd, not_le_of_gt
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
ε : ℝ
ε0 : ε > 0
hj : HAdd.hAdd (α := ℕ) 0 1 ≥ 1
⊢ ‖HSub.hSub (α := ℂ) (∑ m ∈ range (HAdd.hAdd (α := ℕ) 0 1), HPow.hPow (α := ℂ) 0 m / (↑m.factorial : ℂ)) 1‖ = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Exponential
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
⊢ j + 1 ≥ 1

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Exponential
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
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‖
⊢ ‖HSub.hSub (α := ℂ) (∑ m ∈ range (j + 1 + 1), HPow.hPow (α := ℂ) 0 m / (↑m.factorial : ℂ)) 1‖ = 0

Tactic:
rw [← ih (by simp)]
-- Module: Mathlib.Analysis.Complex.Exponential
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
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‖
⊢ ‖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:
simp only [sum_range_succ, pow_succ]

Premises used: pow_succ, Finset.sum_range_succ
-- Module: Mathlib.Analysis.Complex.Exponential
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
⊢ ‖∑ 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
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : j + 1 ≥ 1
h :
  ∀ (hj : HAdd.hAdd (α := ℕ) 0 1 ≥ 1),
    ‖HSub.hSub (α := ℂ) (∑ m ∈ range (HAdd.hAdd (α := ℕ) 0 1), HPow.hPow (α := ℂ) 0 m / (↑m.factorial : ℂ)) 1‖ = 0
h₁ :
  ∀ (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
⊢ ‖HSub.hSub (α := ℂ) (∑ m ∈ range (j + 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

Premises used: pow_succ, Finset.sum_range_succ
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x y : ℂ
j : ℕ
⊢ Eq (α := ℂ) (∑ m ∈ range j, (x + y) ^ m / (↑m.factorial : ℂ))
    (∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / (↑k.factorial : ℂ) * (y ^ (i - k) / (↑(i - k).factorial : ℂ)))

Tactic:
Finset.sum_congr rfl fun m _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x y : ℂ
j : ℕ
refine :
  ∀ m ∈ range j,
    (x + y) ^ m / (↑m.factorial : ℂ) =
      ∑ k ∈ range (m + 1), x ^ k / (↑k.factorial : ℂ) * (y ^ (m - k) / (↑(m - k).factorial : ℂ))
⊢ Eq (α := ℂ) (∑ m ∈ range j, (x + y) ^ m / (↑m.factorial : ℂ))
    (∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / (↑k.factorial : ℂ) * (y ^ (i - k) / (↑(i - k).factorial : ℂ)))

Tactic:
refine Finset.sum_congr rfl fun m _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x y : ℂ
j m : ℕ
h : m ∈ range j
rw :
  Eq (α := ℂ) (∑ i ∈ range (m + 1), x ^ i * y ^ (m - i) * (↑(m.choose i) : ℂ) * (↑m.factorial : ℂ)⁻¹)
    (∑ k ∈ range (m + 1), x ^ k / (↑k.factorial : ℂ) * (y ^ (m - k) / (↑(m - k).factorial : ℂ)))
⊢ (x + y) ^ m / (↑m.factorial : ℂ) =
    ∑ k ∈ range (m + 1), x ^ k / (↑k.factorial : ℂ) * (y ^ (m - k) / (↑(m - k).factorial : ℂ))

Tactic:
rw [add_pow, div_eq_mul_inv, sum_mul]

Premises used: div_eq_mul_inv, add_pow, Finset.sum_mul
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x y : ℂ
j m : ℕ
h : m ∈ range j
⊢ Eq (α := ℂ) (∑ i ∈ range (m + 1), x ^ i * y ^ (m - i) * (↑(m.choose i) : ℂ) * (↑m.factorial : ℂ)⁻¹)
    (∑ k ∈ range (m + 1), x ^ k / (↑k.factorial : ℂ) * (y ^ (m - k) / (↑(m - k).factorial : ℂ)))

Tactic:
Finset.sum_congr rfl fun I hi => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x y : ℂ
j m : ℕ
h : m ∈ range j
refine :
  ∀ (I : ℕ) (hi : I ∈ range (m + 1)),
    x ^ I * y ^ (m - I) * (↑(m.choose I) : ℂ) * (↑m.factorial : ℂ)⁻¹ =
      x ^ I / (↑I.factorial : ℂ) * (y ^ (m - I) / (↑(m - I).factorial : ℂ))
⊢ Eq (α := ℂ) (∑ i ∈ range (m + 1), x ^ i * y ^ (m - i) * (↑(m.choose i) : ℂ) * (↑m.factorial : ℂ)⁻¹)
    (∑ k ∈ range (m + 1), x ^ k / (↑k.factorial : ℂ) * (y ^ (m - k) / (↑(m - k).factorial : ℂ)))

Tactic:
refine Finset.sum_congr rfl fun I hi => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x y : ℂ
j m : ℕ
h : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
⊢ Ne (α := ℂ) (↑(m.choose I) : ℂ) 0

Tactic:
have h₁ : (m.choose I : ℂ) ≠ 0 :=
      Nat.cast_ne_zero.2 (pos_iff_ne_zero.1 (Nat.choose_pos (Nat.le_of_lt_succ (mem_range.1 hi))))
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x y : ℂ
j m : ℕ
h : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : Ne (α := ℂ) (↑(m.choose I) : ℂ) 0
⊢ m.choose I * I.factorial * (m - I).factorial = m.factorial

Tactic:
have h₂ := Nat.choose_mul_factorial_mul_factorial (Nat.le_of_lt_succ <| Finset.mem_range.1 hi)
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x y : ℂ
j m : ℕ
h : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : Ne (α := ℂ) (↑(m.choose I) : ℂ) 0
h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
rw :
  x ^ I * y ^ (m - I) * (↑(m.choose I) : ℂ) *
      (HMul.hMul (α := ℂ) (↑(m.choose I) : ℂ)⁻¹ (↑I.factorial : ℂ)⁻¹ * (↑(m - I).factorial : ℂ)⁻¹) =
    x ^ I / (↑I.factorial : ℂ) * (y ^ (m - I) / (↑(m - I).factorial : ℂ))
⊢ x ^ I * y ^ (m - I) * (↑(m.choose I) : ℂ) * (↑m.factorial : ℂ)⁻¹ =
    x ^ I / (↑I.factorial : ℂ) * (y ^ (m - I) / (↑(m - I).factorial : ℂ))

Tactic:
rw [← h₂, Nat.cast_mul, Nat.cast_mul, mul_inv, mul_inv]

Premises used: mul_inv, Nat.cast_mul