awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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} (α := 𝔹)
    (∑' (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))
have dsimp : Eq.{u_3 + 1} (α := 𝔹) (∑' (b : ℕ), (f : (a : 𝔸) → 𝔹) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑b ! : 𝕂)⁻¹ (x ^ b)))
  (∑' (n : ℕ), HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (HPow.hPow (α := 𝔹) ((f : (a : 𝔸) → 𝔹) x : 𝔹) n))
Tactic: dsimp only [Function.comp_def]
-- 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} (α := 𝔹) (∑' (b : ℕ), (f : (a : 𝔸) → 𝔹) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑b ! : 𝕂)⁻¹ (x ^ b)))
    (∑' (n : ℕ), HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (HPow.hPow (α := 𝔹) ((f : (a : 𝔸) → 𝔹) x : 𝔹) n))
have simp_rw : Eq.{u_3 + 1} (α := 𝔹)
  (∑' (b : ℕ), HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕂) (β := 𝔹) (↑b ! : 𝕂)⁻¹ ((f : (a : 𝔸) → 𝔹) (x ^ b) : 𝔹))
  (∑' (n : ℕ), HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (HPow.hPow (α := 𝔹) ((f : (a : 𝔸) → 𝔹) x : 𝔹) n))
Tactic: simp_rw [map_inv_natCast_smul f 𝕂 𝕂, map_pow]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedDivisionRing 𝔸
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 : ℕ) ↦ ‖x ^ n / (↑n ! : 𝔸)‖
have change : Summable (Function.comp.{1, u_2 + 1, 1} (β := 𝔸) norm fun (n : ℕ) ↦ x ^ n / (↑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 : NormedDivisionRing 𝔸
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 : ℕ) ↦ x ^ n / (↑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_div' (𝕂 := 𝕂) x]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CharZero 𝕂
inst_4 : CompleteSpace 𝔸
x : 𝔸
hx : Membership.mem (γ := Set 𝔸) (Metric.eball 0 (radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
⊢ HasSum (fun (n : ℕ) ↦ x ^ n / (↑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_div' (𝕂 := 𝕂) x]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (hypothesis)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸) = ∞
have this : ∀ {n : ℕ}, Ne.{u_1 + 1} (α := 𝕂) (↑n ! : 𝕂) 0
Tactic: have {n : ℕ} : (Nat.factorial n : 𝕂) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero n)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, Ne.{u_1 + 1} (α := 𝕂) (↑n ! : 𝕂) 0
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸) = ∞
have apply : Tendsto (β := ℝ) (fun (n : ℕ) ↦ norm.{u_1} (E := 𝕂) (↑n.succ ! : 𝕂)⁻¹ / norm.{u_1} (E := 𝕂) (↑n ! : 𝕂)⁻¹) atTop (𝓝 0)
Tactic: apply expSeries_eq_ofScalars 𝕂 𝔸 ▸
    ofScalars_radius_eq_top_of_tendsto 𝔸 _ (Eventually.of_forall fun n => ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, Ne.{u_1 + 1} (α := 𝕂) (↑n ! : 𝕂) 0
apply :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ norm.{u_1} (E := 𝕂) (↑n.succ ! : 𝕂)⁻¹ / norm.{u_1} (E := 𝕂) (↑n ! : 𝕂)⁻¹) atTop (𝓝 0)
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸) = ∞
have apply₁ : ∀ (n : ℕ), Ne.{u_1 + 1} (α := 𝕂) (↑n ! : 𝕂)⁻¹ 0
Tactic: apply expSeries_eq_ofScalars 𝕂 𝔸 ▸
    ofScalars_radius_eq_top_of_tendsto 𝔸 _ (Eventually.of_forall fun n => ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, Ne.{u_1 + 1} (α := 𝕂) (↑n ! : 𝕂) 0
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ norm.{u_1} (E := 𝕂) (↑n.succ ! : 𝕂)⁻¹ / norm.{u_1} (E := 𝕂) (↑n ! : 𝕂)⁻¹) atTop (𝓝 0)
have simp_rw : Tendsto (β := ℝ) (fun (n : ℕ) ↦ norm.{u_1} (E := 𝕂) (↑(n + 1) : 𝕂)⁻¹) atTop (𝓝 0)
Tactic: simp_rw [← norm_div, Nat.factorial_succ, Nat.cast_mul, mul_inv_rev, mul_div_right_comm,
      inv_div_inv, norm_mul, div_self this, norm_one, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, Ne.{u_1 + 1} (α := 𝕂) (↑n ! : 𝕂) 0
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ norm.{u_1} (E := 𝕂) (↑(n + 1) : 𝕂)⁻¹) atTop (𝓝 0)
have apply : Tendsto.{0, u_1} (β := 𝕂) (fun (x : ℕ) ↦ (↑(x + 1) : 𝕂)⁻¹) atTop (𝓝 0)
Tactic: apply norm_zero (E := 𝕂) ▸ Filter.Tendsto.norm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, Ne.{u_1 + 1} (α := 𝕂) (↑n ! : 𝕂) 0
⊢ Tendsto.{0, u_1} (β := 𝕂) (fun (x : ℕ) ↦ (↑(x + 1) : 𝕂)⁻¹) atTop (𝓝 0)
have apply : Tendsto.{0, u_1} (β := 𝕂) (fun (n : ℕ) ↦ (↑n : 𝕂)⁻¹) atTop (𝓝 0)
Tactic: apply (Filter.tendsto_add_atTop_iff_nat (f := fun n => (n : 𝕂)⁻¹) 1).mpr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : ContinuousSMul ℚ 𝕂
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕂 𝔸
⊢ 0 < radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸)
have rw : LT.lt (α := ℝ≥0∞) 0 ∞
Tactic: rw [expSeries_radius_eq_top]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    exp
have rw : ContinuousOn.{u_1, u_1} (X := 𝔸) exp (Metric.eball 0 (radius.{0, u_1, u_1} (𝕜 := ℚ) (E := 𝔸) (F := 𝔸) (expSeries ℚ 𝔸)))
Tactic: rw [← continuousOn_univ, ← Metric.eball_top_eq_univ (0 : 𝔸), ←
    expSeries_radius_eq_top ℚ 𝔸]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
inst_3 : StarRing 𝔸
inst_4 : ContinuousStar 𝔸
x : 𝔸
h : Membership.mem (γ := AddSubgroup 𝔸) (skewAdjoint 𝔸) x
⊢ Membership.mem (γ := Submonoid 𝔸) (unitary 𝔸) (exp x)
have rw : star (exp x) * exp x = 1 ∧ exp x * star (exp x) = 1
Tactic: rw [Unitary.mem_iff, star_exp, skewAdjoint.mem_iff.mp h, ←
    exp_add_of_commute (Commute.refl x).neg_left, ← exp_add_of_commute (Commute.refl x).neg_right,
    neg_add_cancel, add_neg_cancel, exp_zero, and_self_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
inst_3 : StarRing 𝔸
inst_4 : ContinuousStar 𝔸
x : 𝔸
h : Membership.mem (γ := AddSubgroup 𝔸) (skewAdjoint 𝔸) x
rw : star (exp x) * exp x = 1 ∧ exp x * star (exp x) = 1
⊢ Membership.mem (γ := Submonoid 𝔸) (unitary 𝔸) (exp x)
have rw₁ : exp (star x) * exp x = 1 ∧ exp x * exp (star x) = 1
Tactic: rw [Unitary.mem_iff, star_exp, skewAdjoint.mem_iff.mp h, ←
    exp_add_of_commute (Commute.refl x).neg_left, ← exp_add_of_commute (Commute.refl x).neg_right,
    neg_add_cancel, add_neg_cancel, exp_zero, and_self_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
inst_3 : StarRing 𝔸
inst_4 : ContinuousStar 𝔸
x : 𝔸
h : Membership.mem (γ := AddSubgroup 𝔸) (skewAdjoint 𝔸) x
rw : star (exp x) * exp x = 1 ∧ exp x * star (exp x) = 1
rw₁ : exp (star x) * exp x = 1 ∧ exp x * exp (star x) = 1
⊢ Membership.mem (γ := Submonoid 𝔸) (unitary 𝔸) (exp x)
have rw₂ : exp (-x) * exp x = 1 ∧ exp x * exp (-x) = 1
Tactic: rw [Unitary.mem_iff, star_exp, skewAdjoint.mem_iff.mp h, ←
    exp_add_of_commute (Commute.refl x).neg_left, ← exp_add_of_commute (Commute.refl x).neg_right,
    neg_add_cancel, add_neg_cancel, exp_zero, and_self_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
inst_3 : StarRing 𝔸
inst_4 : ContinuousStar 𝔸
x : 𝔸
h : Membership.mem (γ := AddSubgroup 𝔸) (skewAdjoint 𝔸) x
rw : star (exp x) * exp x = 1 ∧ exp x * star (exp x) = 1
rw₁ : exp (star x) * exp x = 1 ∧ exp x * exp (star x) = 1
rw₂ : exp (-x) * exp x = 1 ∧ exp x * exp (-x) = 1
⊢ Membership.mem (γ := Submonoid 𝔸) (unitary 𝔸) (exp x)
have rw₃ : exp (-x + x) = 1 ∧ exp x * exp (-x) = 1
Tactic: rw [Unitary.mem_iff, star_exp, skewAdjoint.mem_iff.mp h, ←
    exp_add_of_commute (Commute.refl x).neg_left, ← exp_add_of_commute (Commute.refl x).neg_right,
    neg_add_cancel, add_neg_cancel, exp_zero, and_self_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
inst_3 : StarRing 𝔸
inst_4 : ContinuousStar 𝔸
x : 𝔸
h : Membership.mem (γ := AddSubgroup 𝔸) (skewAdjoint 𝔸) x
rw : star (exp x) * exp x = 1 ∧ exp x * star (exp x) = 1
rw₁ : exp (star x) * exp x = 1 ∧ exp x * exp (star x) = 1
rw₂ : exp (-x) * exp x = 1 ∧ exp x * exp (-x) = 1
rw₃ : exp (-x + x) = 1 ∧ exp x * exp (-x) = 1
⊢ Membership.mem (γ := Submonoid 𝔸) (unitary 𝔸) (exp x)
have rw₄ : exp (-x + x) = 1 ∧ exp (x + -x) = 1
Tactic: rw [Unitary.mem_iff, star_exp, skewAdjoint.mem_iff.mp h, ←
    exp_add_of_commute (Commute.refl x).neg_left, ← exp_add_of_commute (Commute.refl x).neg_right,
    neg_add_cancel, add_neg_cancel, exp_zero, and_self_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
inst_3 : StarRing 𝔸
inst_4 : ContinuousStar 𝔸
x : 𝔸
h : Membership.mem (γ := AddSubgroup 𝔸) (skewAdjoint 𝔸) x
rw : star (exp x) * exp x = 1 ∧ exp x * star (exp x) = 1
rw₁ : exp (star x) * exp x = 1 ∧ exp x * exp (star x) = 1
rw₂ : exp (-x) * exp x = 1 ∧ exp x * exp (-x) = 1
rw₃ : exp (-x + x) = 1 ∧ exp x * exp (-x) = 1
rw₄ : exp (-x + x) = 1 ∧ exp (x + -x) = 1
⊢ Membership.mem (γ := Submonoid 𝔸) (unitary 𝔸) (exp x)
have rw₅ : Eq.{u_1 + 1} (α := 𝔸) (exp 0) 1 ∧ exp (x + -x) = 1
Tactic: rw [Unitary.mem_iff, star_exp, skewAdjoint.mem_iff.mp h, ←
    exp_add_of_commute (Commute.refl x).neg_left, ← exp_add_of_commute (Commute.refl x).neg_right,
    neg_add_cancel, add_neg_cancel, exp_zero, and_self_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
inst_3 : StarRing 𝔸
inst_4 : ContinuousStar 𝔸
x : 𝔸
h : Membership.mem (γ := AddSubgroup 𝔸) (skewAdjoint 𝔸) x
rw : star (exp x) * exp x = 1 ∧ exp x * star (exp x) = 1
rw₁ : exp (star x) * exp x = 1 ∧ exp x * exp (star x) = 1
rw₂ : exp (-x) * exp x = 1 ∧ exp x * exp (-x) = 1
rw₃ : exp (-x + x) = 1 ∧ exp x * exp (-x) = 1
rw₄ : exp (-x + x) = 1 ∧ exp (x + -x) = 1
rw₅ : Eq.{u_1 + 1} (α := 𝔸) (exp 0) 1 ∧ exp (x + -x) = 1
⊢ Membership.mem (γ := Submonoid 𝔸) (unitary 𝔸) (exp x)
have rw₆ : Eq.{u_1 + 1} (α := 𝔸) (exp 0) 1 ∧ Eq.{u_1 + 1} (α := 𝔸) (exp 0) 1
Tactic: rw [Unitary.mem_iff, star_exp, skewAdjoint.mem_iff.mp h, ←
    exp_add_of_commute (Commute.refl x).neg_left, ← exp_add_of_commute (Commute.refl x).neg_right,
    neg_add_cancel, add_neg_cancel, exp_zero, and_self_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
inst_3 : StarRing 𝔸
inst_4 : ContinuousStar 𝔸
x : 𝔸
h : Membership.mem (γ := AddSubgroup 𝔸) (skewAdjoint 𝔸) x
rw : star (exp x) * exp x = 1 ∧ exp x * star (exp x) = 1
rw₁ : exp (star x) * exp x = 1 ∧ exp x * exp (star x) = 1
rw₂ : exp (-x) * exp x = 1 ∧ exp x * exp (-x) = 1
rw₃ : exp (-x + x) = 1 ∧ exp x * exp (-x) = 1
rw₄ : exp (-x + x) = 1 ∧ exp (x + -x) = 1
rw₅ : Eq.{u_1 + 1} (α := 𝔸) (exp 0) 1 ∧ exp (x + -x) = 1
rw₆ : Eq.{u_1 + 1} (α := 𝔸) (exp 0) 1 ∧ Eq.{u_1 + 1} (α := 𝔸) (exp 0) 1
⊢ Membership.mem (γ := Submonoid 𝔸) (unitary 𝔸) (exp x)
have rw₇ : Eq.{u_1 + 1} (α := 𝔸) 1 1 ∧ Eq.{u_1 + 1} (α := 𝔸) 1 1
Tactic: rw [Unitary.mem_iff, star_exp, skewAdjoint.mem_iff.mp h, ←
    exp_add_of_commute (Commute.refl x).neg_left, ← exp_add_of_commute (Commute.refl x).neg_right,
    neg_add_cancel, add_neg_cancel, exp_zero, and_self_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
inst_3 : StarRing 𝔸
inst_4 : ContinuousStar 𝔸
x : 𝔸
h : Membership.mem (γ := AddSubgroup 𝔸) (skewAdjoint 𝔸) x
rw : star (exp x) * exp x = 1 ∧ exp x * star (exp x) = 1
rw₁ : exp (star x) * exp x = 1 ∧ exp x * exp (star x) = 1
rw₂ : exp (-x) * exp x = 1 ∧ exp x * exp (-x) = 1
rw₃ : exp (-x + x) = 1 ∧ exp x * exp (-x) = 1
rw₄ : exp (-x + x) = 1 ∧ exp (x + -x) = 1
rw₅ : Eq.{u_1 + 1} (α := 𝔸) (exp 0) 1 ∧ exp (x + -x) = 1
rw₆ : Eq.{u_1 + 1} (α := 𝔸) (exp 0) 1 ∧ Eq.{u_1 + 1} (α := 𝔸) (exp 0) 1
rw₇ : Eq.{u_1 + 1} (α := 𝔸) 1 1 ∧ Eq.{u_1 + 1} (α := 𝔸) 1 1
⊢ Membership.mem (γ := Submonoid 𝔸) (unitary 𝔸) (exp x)
have rw₈ : Eq.{u_1 + 1} (α := 𝔸) 1 1
Tactic: rw [Unitary.mem_iff, star_exp, skewAdjoint.mem_iff.mp h, ←
    exp_add_of_commute (Commute.refl x).neg_left, ← exp_add_of_commute (Commute.refl x).neg_right,
    neg_add_cancel, add_neg_cancel, exp_zero, and_self_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x a b : 𝔸
h : SemiconjBy x a b
⊢ SemiconjBy x (exp a) (exp b)
have rw : SemiconjBy x ((fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n) : 𝔸)) a)
  ((fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n) : 𝔸)) b)
Tactic: rw [exp_eq_tsum ℚ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x a b : 𝔸
h : SemiconjBy x a b
⊢ SemiconjBy x ((fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n) : 𝔸)) a)
    ((fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n) : 𝔸)) b)
have apply : ∀ (i : ℕ), SemiconjBy x (HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i)) (HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (b ^ i))
Tactic: apply SemiconjBy.tsum_right x (expSeries_summable' _) (expSeries_summable' _)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
ι : Type u_3
f : ι → 𝔸
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (h : (↑s : Set ι).Pairwise (Commute on f)),
    Eq.{u_1 + 1} (α := 𝔸) (exp (∑ i ∈ s, f i)) (s.noncommProd (fun (i : ι) ↦ exp (f i)) ⋯)
h : (↑(insert a s) : Set ι).Pairwise (Commute on f)
⊢ Eq.{u_1 + 1} (α := 𝔸) (exp (∑ i ∈ insert a s, f i)) ((insert a s).noncommProd (fun (i : ι) ↦ exp (f i)) ⋯)
have insert : Commute (f a) (∑ x ∈ s, f x)
Tactic: rw [Finset.noncommProd_insert_of_notMem _ _ _ _ ha, Finset.sum_insert ha, exp_add_of_commute,
      ih (h.mono <| Finset.subset_insert _ _)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
ι : Type u_3
f : ι → 𝔸
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (h : (↑s : Set ι).Pairwise (Commute on f)),
    Eq.{u_1 + 1} (α := 𝔸) (exp (∑ i ∈ s, f i)) (s.noncommProd (fun (i : ι) ↦ exp (f i)) ⋯)
h : (↑(insert a s) : Set ι).Pairwise (Commute on f)
⊢ Commute (f a) (∑ x ∈ s, f x)
have insert : ∀ (i : ι) (hi : i ∈ s), Commute (f a) (f i)
Tactic: refine Commute.sum_right _ _ _ fun i hi => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
ι : Type u_3
s : Finset ι
f : ι → 𝔸
h : (↑s : Set ι).Pairwise (Commute on f)
⊢ Eq.{u_1 + 1} (α := 𝔸) (exp (∑ i ∈ s, f i)) (s.noncommProd (fun (i : ι) ↦ exp (f i)) ⋯)
have empty : ∀ (h : (↑∅ : Set ι).Pairwise (Commute on f)),
  Eq.{u_1 + 1} (α := 𝔸) (exp (∑ i ∈ ∅, f i)) (Finset.noncommProd ∅ (fun (i : ι) ↦ exp (f i)) sorry)
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert a s ha ih =>
    rw [Finset.noncommProd_insert_of_notMem _ _ _ _ ha, Finset.sum_insert ha, exp_add_of_commute,
      ih (h.mono <| Finset.subset_insert _ _)]
    refine Commute.sum_right _ _ _ fun i hi => ?_
    exact h.of_refl (Finset.mem_insert_self _ _) (Finset.mem_insert_of_mem hi)
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
ι : Type u_3
s : Finset ι
f : ι → 𝔸
h : (↑s : Set ι).Pairwise (Commute on f)
empty :
  ∀ (h : (↑∅ : Set ι).Pairwise (Commute on f)),
    Eq.{u_1 + 1} (α := 𝔸) (exp (∑ i ∈ ∅, f i)) (Finset.noncommProd ∅ (fun (i : ι) ↦ exp (f i)) ⋯)
⊢ Eq.{u_1 + 1} (α := 𝔸) (exp (∑ i ∈ s, f i)) (s.noncommProd (fun (i : ι) ↦ exp (f i)) ⋯)
have insert : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
  (ih :
    ∀ (h : (↑s : Set ι).Pairwise (Commute on f)),
      Eq.{u_1 + 1} (α := 𝔸) (exp (∑ i ∈ s, f i)) (s.noncommProd (fun (i : ι) ↦ exp (f i)) sorry))
  (h : (↑(insert a s) : Set ι).Pairwise (Commute on f)),
  Eq.{u_1 + 1} (α := 𝔸) (exp (∑ i ∈ insert a s, f i)) ((insert a s).noncommProd (fun (i : ι) ↦ exp (f i)) sorry)
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert a s ha ih =>
    rw [Finset.noncommProd_insert_of_notMem _ _ _ _ ha, Finset.sum_insert ha, exp_add_of_commute,
      ih (h.mono <| Finset.subset_insert _ _)]
    refine Commute.sum_right _ _ _ fun i hi => ?_
    exact h.of_refl (Finset.mem_insert_self _ _) (Finset.mem_insert_of_mem hi)
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
ι : Type u_3
s : Finset ι
f : ι → 𝔸
h : (↑s : Set ι).Pairwise (Commute on f)
⊢ Eq.{u_1 + 1} (α := 𝔸) (exp (∑ i ∈ s, f i)) (s.noncommProd (fun (i : ι) ↦ exp (f i)) ⋯)
have empty : ∀ (h : (↑∅ : Set ι).Pairwise (Commute on f)),
  Eq.{u_1 + 1} (α := 𝔸) (exp (∑ i ∈ ∅, f i)) (Finset.noncommProd ∅ (fun (i : ι) ↦ exp (f i)) sorry)
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert a s ha ih =>
    rw [Finset.noncommProd_insert_of_notMem _ _ _ _ ha, Finset.sum_insert ha, exp_add_of_commute,
      ih (h.mono <| Finset.subset_insert _ _)]
    refine Commute.sum_right _ _ _ fun i hi => ?_
    exact h.of_refl (Finset.mem_insert_self _ _) (Finset.mem_insert_of_mem hi)
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
ι : Type u_3
s : Finset ι
f : ι → 𝔸
h : (↑s : Set ι).Pairwise (Commute on f)
empty :
  ∀ (h : (↑∅ : Set ι).Pairwise (Commute on f)),
    Eq.{u_1 + 1} (α := 𝔸) (exp (∑ i ∈ ∅, f i)) (Finset.noncommProd ∅ (fun (i : ι) ↦ exp (f i)) ⋯)
⊢ Eq.{u_1 + 1} (α := 𝔸) (exp (∑ i ∈ s, f i)) (s.noncommProd (fun (i : ι) ↦ exp (f i)) ⋯)
have insert : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
  (ih :
    ∀ (h : (↑s : Set ι).Pairwise (Commute on f)),
      Eq.{u_1 + 1} (α := 𝔸) (exp (∑ i ∈ s, f i)) (s.noncommProd (fun (i : ι) ↦ exp (f i)) sorry))
  (h : (↑(insert a s) : Set ι).Pairwise (Commute on f)),
  Eq.{u_1 + 1} (α := 𝔸) (exp (∑ i ∈ insert a s, f i)) ((insert a s).noncommProd (fun (i : ι) ↦ exp (f i)) sorry)
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert a s ha ih =>
    rw [Finset.noncommProd_insert_of_notMem _ _ _ _ ha, Finset.sum_insert ha, exp_add_of_commute,
      ih (h.mono <| Finset.subset_insert _ _)]
    refine Commute.sum_right _ _ _ fun i hi => ?_
    exact h.of_refl (Finset.mem_insert_self _ _) (Finset.mem_insert_of_mem hi)
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x : 𝔸
⊢ exp (HSMul.hSMul (α := ℕ) 0 x) = HPow.hPow (β := ℕ) (exp x) 0
have zero : exp 0 = HPow.hPow (β := ℕ) (exp x) 0
Tactic: rw [zero_smul, pow_zero, exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x : 𝔸
zero : exp 0 = HPow.hPow (β := ℕ) (exp x) 0
⊢ exp (HSMul.hSMul (α := ℕ) 0 x) = HPow.hPow (β := ℕ) (exp x) 0
have zero₁ : Eq.{u_1 + 1} (α := 𝔸) (exp 0) 1
Tactic: rw [zero_smul, pow_zero, exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x : 𝔸
zero : exp 0 = HPow.hPow (β := ℕ) (exp x) 0
zero₁ : Eq.{u_1 + 1} (α := 𝔸) (exp 0) 1
⊢ exp (HSMul.hSMul (α := ℕ) 0 x) = HPow.hPow (β := ℕ) (exp x) 0
have zero₂ : Eq.{u_1 + 1} (α := 𝔸) 1 1
Tactic: rw [zero_smul, pow_zero, exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x : 𝔸
n : ℕ
ih : exp (n • x) = exp x ^ n
⊢ exp ((n + 1) • x) = exp x ^ (n + 1)
have succ : exp (n • x + x) = exp x ^ (n + 1)
Tactic: rw [succ_nsmul, pow_succ, exp_add_of_commute ((Commute.refl x).smul_left n), ih]