awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_2
inst : DivisionRing 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : CharZero 𝔸
⊢ FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) = fun (x : 𝔸) ↦
    ∑' (n : ℕ), x ^ n / (↑n ! : 𝔸)
have h : ∀ (x : 𝔸),
  FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) x = ∑' (n : ℕ), x ^ n / (↑n ! : 𝔸)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n)‖
have change : Summable
  (Function.comp.{1, u_2 + 1, 1} (β := 𝔸) norm fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n))
Tactic: change Summable (norm ∘ _)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
⊢ Summable
    (Function.comp.{1, u_2 + 1, 1} (β := 𝔸) norm fun (n : ℕ) ↦
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n))
have rw : Summable
  (Function.comp.{1, u_2 + 1, 1} (β := 𝔸) norm fun (n : ℕ) ↦
    (expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x)
Tactic: rw [← expSeries_apply_eq']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
⊢ HasSum (fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n)) (exp x)
have rw : HasSum (fun (n : ℕ) ↦ (expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) (exp x)
Tactic: rw [← expSeries_apply_eq']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (hypothesis)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
⊢ ContinuousOn.{u_2, u_2} (X := 𝔸) exp
    (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸)))
have this : ContinuousOn (FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸))
  (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸)))
Tactic: have := FormalMultilinearSeries.continuousOn (p := expSeries 𝕂 𝔸)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
⊢ AnalyticAt 𝕂 exp x
have pos : ∀ (h : radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸) = 0), AnalyticAt 𝕂 exp x
Tactic: by_cases h : (expSeries 𝕂 𝔸).radius = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
pos : ∀ (h : radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸) = 0), AnalyticAt 𝕂 exp x
⊢ AnalyticAt 𝕂 exp x
have neg : ∀ (h : ¬radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸) = 0), AnalyticAt 𝕂 exp x
Tactic: by_cases h : (expSeries 𝕂 𝔸).radius = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (hypothesis)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
h : radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸) = 0
⊢ AnalyticAt 𝕂 exp x
have hx₁ : Membership.mem (γ := Set 𝔸) (Metric.eball 0 0) x
Tactic: rw [h] at hx
Cleared hypotheses: hx, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (hypothesis)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
h : ¬radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸) = 0
⊢ AnalyticAt 𝕂 exp x
have h₁ : 0 < radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸)
Tactic: have h := pos_iff_ne_zero.mpr h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
hy : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) y
⊢ exp (x + y) = exp x * exp y
have rw : Eq.{u_2 + 1} (α := 𝔸)
  ((fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n) : 𝔸)) (x + y))
  (∑' (n : ℕ),
    ∑ kl ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑kl.1! : 𝕂)⁻¹ (x ^ kl.1) *
        HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑kl.2! : 𝕂)⁻¹ (y ^ kl.2))
Tactic: rw [exp_eq_tsum 𝕂,
    tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm
      (norm_expSeries_summable_of_mem_ball' x hx) (norm_expSeries_summable_of_mem_ball' y hy)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
hy : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) y
| ∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ ((x + y) ^ n)
have f : fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ ((x + y) ^ n)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
hy : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) y
f : fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ ((x + y) ^ n)
| ∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ ((x + y) ^ n)
have L : SummationFilter.unconditional ℕ
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
hy : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) y
| fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ ((x + y) ^ n)
have f : ∀ (x_1 : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑x_1 ! : 𝕂)⁻¹ ((x + y) ^ x_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
hy : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) y
x_1 : ℕ
| HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑x_1 ! : 𝕂)⁻¹ ((x + y) ^ x_1)
have f : ∑ x_2 ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ x_1,
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑x_1 ! : 𝕂)⁻¹ (x_1.choose x_2.1 • (x ^ x_2.1 * y ^ x_2.2))
Tactic: rw [hxy.add_pow' _, Finset.smul_sum]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
hy : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) y
| ∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ ((x + y) ^ n)
have f : ∀ (x_1 : ℕ),
  ∑ x_2 ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ x_1,
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑x_1 ! : 𝕂)⁻¹ (x_1.choose x_2.1 • (x ^ x_2.1 * y ^ x_2.2))
Tactic: congr
    ext
    rw [hxy.add_pow' _, Finset.smul_sum]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
hy : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) y
f :
  ∀ (x_1 : ℕ),
    ∑ x_2 ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ x_1,
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑x_1 ! : 𝕂)⁻¹ (x_1.choose x_2.1 • (x ^ x_2.1 * y ^ x_2.2))
| ∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ ((x + y) ^ n)
have L : SummationFilter.unconditional ℕ
Tactic: congr
    ext
    rw [hxy.add_pow' _, Finset.smul_sum]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
hy : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) y
⊢ Eq.{u_2 + 1} (α := 𝔸) (∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ ((x + y) ^ n))
    (∑' (n : ℕ),
      ∑ kl ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
        HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑kl.1! : 𝕂)⁻¹ (x ^ kl.1) *
          HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑kl.2! : 𝕂)⁻¹ (y ^ kl.2))
have conv_lhs : Eq.{u_2 + 1} (α := 𝔸)
  (∑' (x_1 : ℕ),
    ∑ x_2 ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ x_1,
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑x_1 ! : 𝕂)⁻¹ (x_1.choose x_2.1 • (x ^ x_2.1 * y ^ x_2.2)))
  (∑' (n : ℕ),
    ∑ kl ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑kl.1! : 𝕂)⁻¹ (x ^ kl.1) *
        HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑kl.2! : 𝕂)⁻¹ (y ^ kl.2))
Tactic: conv_lhs =>
    congr
    ext
    rw [hxy.add_pow' _, Finset.smul_sum]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
hy : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) y
⊢ Eq.{u_2 + 1} (α := 𝔸)
    (∑' (x_1 : ℕ),
      ∑ x_2 ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ x_1,
        HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑x_1 ! : 𝕂)⁻¹ (x_1.choose x_2.1 • (x ^ x_2.1 * y ^ x_2.2)))
    (∑' (n : ℕ),
      ∑ kl ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
        HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑kl.1! : 𝕂)⁻¹ (x ^ kl.1) *
          HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑kl.2! : 𝕂)⁻¹ (y ^ kl.2))
have refine : ∀ (n : ℕ) (kl : ℕ × ℕ) (hkl : kl ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n),
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (n.choose kl.1 • (x ^ kl.1 * y ^ kl.2)) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑kl.1! : 𝕂)⁻¹ (x ^ kl.1) *
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑kl.2! : 𝕂)⁻¹ (y ^ kl.2)
Tactic: refine tsum_congr fun n => Finset.sum_congr rfl fun kl hkl => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
hy : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) y
n : ℕ
kl : ℕ × ℕ
hkl : kl ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (n.choose kl.1 • (x ^ kl.1 * y ^ kl.2)) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑kl.1! : 𝕂)⁻¹ (x ^ kl.1) *
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑kl.2! : 𝕂)⁻¹ (y ^ kl.2)
have rw : ((↑n ! : 𝕂)⁻¹ * ((↑n ! : 𝕂) / HMul.hMul (α := 𝕂) (↑kl.1! : 𝕂) (↑kl.2! : 𝕂))) • (x ^ kl.1 * y ^ kl.2) =
  HMul.hMul (α := 𝕂) (↑kl.1! : 𝕂)⁻¹ (↑kl.2! : 𝕂)⁻¹ • (x ^ kl.1 * y ^ kl.2)
Tactic: rw [← Nat.cast_smul_eq_nsmul 𝕂, smul_smul, smul_mul_smul_comm, ← Finset.mem_antidiagonal.mp hkl,
    Nat.cast_add_choose, Finset.mem_antidiagonal.mp hkl]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedRing 𝔹
inst_3 : NormedAlgebra 𝕂 𝔸
inst_4 : CompleteSpace 𝔸
inst_5 : CharZero 𝕂
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
⊢ Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (-x)
have rw : edist x 0 < radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸)
Tactic: rw [Metric.mem_eball, ← neg_zero, edist_neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (hypothesis)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedRing 𝔹
inst_3 : NormedAlgebra 𝕂 𝔸
inst_4 : CompleteSpace 𝔸
inst_5 : CharZero 𝕂
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
⊢ exp (-x) * exp x = 1
have hnx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (-x)
Tactic: have hnx : -x ∈ Metric.eball (0 : 𝔸) (expSeries 𝕂 𝔸).radius := by
      rw [Metric.mem_eball, ← neg_zero, edist_neg_neg]
      exact hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedRing 𝔹
inst_3 : NormedAlgebra 𝕂 𝔸
inst_4 : CompleteSpace 𝔸
inst_5 : CharZero 𝕂
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
hnx :
  Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (-x)
⊢ exp (-x) * exp x = 1
have rw : exp (-x + x) = 1
Tactic: rw [← exp_add_of_commute_of_mem_ball (Commute.neg_left <| Commute.refl x) hnx hx,
      neg_add_cancel, exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedRing 𝔹
inst_3 : NormedAlgebra 𝕂 𝔸
inst_4 : CompleteSpace 𝔸
inst_5 : CharZero 𝕂
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
hnx :
  Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (-x)
rw : exp (-x + x) = 1
⊢ exp (-x) * exp x = 1
have rw₁ : Eq.{u_2 + 1} (α := 𝔸) (exp 0) 1
Tactic: rw [← exp_add_of_commute_of_mem_ball (Commute.neg_left <| Commute.refl x) hnx hx,
      neg_add_cancel, exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedRing 𝔹
inst_3 : NormedAlgebra 𝕂 𝔸
inst_4 : CompleteSpace 𝔸
inst_5 : CharZero 𝕂
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
hnx :
  Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (-x)
rw : exp (-x + x) = 1
rw₁ : Eq.{u_2 + 1} (α := 𝔸) (exp 0) 1
⊢ exp (-x) * exp x = 1
have rw₂ : Eq.{u_2 + 1} (α := 𝔸) 1 1
Tactic: rw [← exp_add_of_commute_of_mem_ball (Commute.neg_left <| Commute.refl x) hnx hx,
      neg_add_cancel, exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (hypothesis)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedRing 𝔹
inst_3 : NormedAlgebra 𝕂 𝔸
inst_4 : CompleteSpace 𝔸
inst_5 : CharZero 𝕂
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
⊢ exp x * exp (-x) = 1
have hnx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (-x)
Tactic: have hnx : -x ∈ Metric.eball (0 : 𝔸) (expSeries 𝕂 𝔸).radius := by
      rw [Metric.mem_eball, ← neg_zero, edist_neg_neg]
      exact hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedRing 𝔹
inst_3 : NormedAlgebra 𝕂 𝔸
inst_4 : CompleteSpace 𝔸
inst_5 : CharZero 𝕂
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
hnx :
  Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (-x)
⊢ exp x * exp (-x) = 1
have rw : exp (x + -x) = 1
Tactic: rw [← exp_add_of_commute_of_mem_ball (Commute.neg_right <| Commute.refl x) hx hnx,
      add_neg_cancel, exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedRing 𝔹
inst_3 : NormedAlgebra 𝕂 𝔸
inst_4 : CompleteSpace 𝔸
inst_5 : CharZero 𝕂
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
hnx :
  Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (-x)
rw : exp (x + -x) = 1
⊢ exp x * exp (-x) = 1
have rw₁ : Eq.{u_2 + 1} (α := 𝔸) (exp 0) 1
Tactic: rw [← exp_add_of_commute_of_mem_ball (Commute.neg_right <| Commute.refl x) hx hnx,
      add_neg_cancel, exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedRing 𝔹
inst_3 : NormedAlgebra 𝕂 𝔸
inst_4 : CompleteSpace 𝔸
inst_5 : CharZero 𝕂
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
hnx :
  Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (-x)
rw : exp (x + -x) = 1
rw₁ : Eq.{u_2 + 1} (α := 𝔸) (exp 0) 1
⊢ exp x * exp (-x) = 1
have rw₂ : Eq.{u_2 + 1} (α := 𝔸) 1 1
Tactic: rw [← exp_add_of_commute_of_mem_ball (Commute.neg_right <| Commute.refl x) hx hnx,
      add_neg_cancel, exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedRing 𝔹
inst_3 : NormedAlgebra 𝕂 𝔸
inst_4 : CompleteSpace 𝔸
inst_5 : Algebra 𝕂 𝔹
inst_6 : CharZero 𝕂
F : Type u_4
inst_7 : FunLike F 𝔸 𝔹
inst_8 : RingHomClass F 𝔸 𝔹
f : F
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : 𝔸) → 𝔹)
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
⊢ Eq.{u_3 + 1} (α := 𝔹) ((f : (a : 𝔸) → 𝔹) (exp x) : 𝔹) (exp ((f : (a : 𝔸) → 𝔹) x) : 𝔹)
have rw : Eq.{u_3 + 1} (α := 𝔹)
  ((f : (a : 𝔸) → 𝔹) ((fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n) : 𝔸)) x) :
    𝔹)
  ((fun (x : 𝔹) ↦ (∑' (n : ℕ), HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n) : 𝔹)) ((f : (a : 𝔸) → 𝔹) x) :
    𝔹)
Tactic: rw [exp_eq_tsum 𝕂, exp_eq_tsum 𝕂]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedRing 𝔹
inst_3 : NormedAlgebra 𝕂 𝔸
inst_4 : CompleteSpace 𝔸
inst_5 : Algebra 𝕂 𝔹
inst_6 : CharZero 𝕂
F : Type u_4
inst_7 : FunLike F 𝔸 𝔹
inst_8 : RingHomClass F 𝔸 𝔹
f : F
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : 𝔸) → 𝔹)
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
⊢ Eq.{u_3 + 1} (α := 𝔹)
    ((f : (a : 𝔸) → 𝔹) ((fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n) : 𝔸)) x) :
      𝔹)
    ((fun (x : 𝔹) ↦ (∑' (n : ℕ), HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n) : 𝔹)) ((f : (a : 𝔸) → 𝔹) x) :
      𝔹)
have refine : Eq.{u_3 + 1} (α := 𝔹)
  (∑' (b : ℕ),
    Function.comp.{1, u_2 + 1, u_3 + 1} (β := 𝔸) (⇑f : (a : 𝔸) → 𝔹)
      (fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n)) b)
  ((fun (x : 𝔹) ↦ (∑' (n : ℕ), HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n) : 𝔹)) ((f : (a : 𝔸) → 𝔹) x))
Tactic: refine ((expSeries_summable_of_mem_ball' _ hx).hasSum.map f hf).tsum_eq.symm.trans ?_