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
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : CharZero 𝕂
x : 𝔸
h :
  (if h : Nonempty.{u_2 + 1} (Algebra ℚ 𝔸) then
      FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) x
    else 1) =
    FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) x
h₁ :
  FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) x =
    FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) x
⊢ exp x = FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) x
have h₂ : FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) x =
  FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) x
Tactic: rw [exp, dif_pos ⟨RestrictScalars.algebra ℚ 𝕂 𝔸⟩, ← @expSeries_sum_eq_rat (𝕂 := 𝕂)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : CharZero 𝕂
⊢ Eq.{u_2 + 1} (α := (x : 𝔸) → 𝔸) exp fun (x : 𝔸) ↦
    ∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n)
have rw : FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) = fun (x : 𝔸) ↦
  ∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n)
Tactic: rw [exp_eq_expSeries_sum 𝕂]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : CharZero 𝕂
⊢ FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) = fun (x : 𝔸) ↦
    ∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n)
have h : ∀ (x : 𝔸),
  FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) x =
    ∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : CharZero 𝕂
⊢ Eq.{u_2 + 1} (α := (x : 𝔸) → 𝔸) exp (ofScalarsSum.{u_1, u_2} (𝕜 := 𝕂) fun (n : ℕ) ↦ (↑n ! : 𝕂)⁻¹)
have rw : Eq.{u_2 + 1} (α := (x : 𝔸) → 𝔸) (fun (x : 𝔸) ↦ ∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n))
  (ofScalarsSum.{u_1, u_2} (𝕜 := 𝕂) fun (n : ℕ) ↦ (↑n ! : 𝕂)⁻¹)
Tactic: rw [exp_eq_tsum 𝕂, ofScalarsSum_eq_tsum]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : CharZero 𝕂
rw :
  Eq.{u_2 + 1} (α := (x : 𝔸) → 𝔸) (fun (x : 𝔸) ↦ ∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n))
    (ofScalarsSum.{u_1, u_2} (𝕜 := 𝕂) fun (n : ℕ) ↦ (↑n ! : 𝕂)⁻¹)
⊢ Eq.{u_2 + 1} (α := (x : 𝔸) → 𝔸) exp (ofScalarsSum.{u_1, u_2} (𝕜 := 𝕂) fun (n : ℕ) ↦ (↑n ! : 𝕂)⁻¹)
have rw₁ : Eq.{u_2 + 1} (α := (x : 𝔸) → 𝔸) (fun (x : 𝔸) ↦ ∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n))
  fun (x : 𝔸) ↦ ∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n)
Tactic: rw [exp_eq_tsum 𝕂, ofScalarsSum_eq_tsum]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
n : ℕ
⊢ Eq (α := 𝔸) ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x : Fin n) ↦ 0 : 𝔸)
    (Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 n : 𝔸)
have rw : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (HPow.hPow (α := 𝔸) 0 n) = Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 n
Tactic: rw [expSeries_apply_eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
n : ℕ
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (HPow.hPow (α := 𝔸) 0 n) = Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 n
have zero : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑0! : 𝕂)⁻¹ (HPow.hPow (α := 𝔸) (β := ℕ) 0 0) =
  Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 0
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
n : ℕ
zero :
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑0! : 𝕂)⁻¹ (HPow.hPow (α := 𝔸) (β := ℕ) 0 0) =
    Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 0
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (HPow.hPow (α := 𝔸) 0 n) = Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 n
have succ : ∀ (n : ℕ),
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑(n + 1)! : 𝕂)⁻¹ (HPow.hPow (α := 𝔸) 0 (n + 1)) =
    Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 (n + 1)
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
n : ℕ
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑(n + 1)! : 𝕂)⁻¹ (HPow.hPow (α := 𝔸) 0 (n + 1)) =
    Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 (n + 1)
have succ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (β := 𝔸) (↑(n + 1)! : 𝕂)⁻¹ 0 = Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 (n + 1)
Tactic: rw [zero_pow (Nat.succ_ne_zero _), smul_zero, Pi.single_eq_of_ne n.succ_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
n : ℕ
succ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (β := 𝔸) (↑(n + 1)! : 𝕂)⁻¹ 0 = Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 (n + 1)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑(n + 1)! : 𝕂)⁻¹ (HPow.hPow (α := 𝔸) 0 (n + 1)) =
    Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 (n + 1)
have succ₁ : Eq.{u_2 + 1} (α := 𝔸) (0 : 𝔸) (Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 (n + 1) : 𝔸)
Tactic: rw [zero_pow (Nat.succ_ne_zero _), smul_zero, Pi.single_eq_of_ne n.succ_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
n : ℕ
succ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (β := 𝔸) (↑(n + 1)! : 𝕂)⁻¹ 0 = Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 (n + 1)
succ₁ : Eq.{u_2 + 1} (α := 𝔸) (0 : 𝔸) (Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 (n + 1) : 𝔸)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑(n + 1)! : 𝕂)⁻¹ (HPow.hPow (α := 𝔸) 0 (n + 1)) =
    Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 (n + 1)
have succ₂ : Eq.{u_2 + 1} (α := 𝔸) 0 0
Tactic: rw [zero_pow (Nat.succ_ne_zero _), smul_zero, Pi.single_eq_of_ne n.succ_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
⊢ Eq.{u_2 + 1} (α := 𝔸) (exp 0) 1
have rw : Eq.{u_2 + 1} (α := 𝔸)
  (if h : Nonempty.{u_2 + 1} (Algebra ℚ 𝔸) then
    FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) 0
  else 1)
  1
Tactic: rw [exp]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
⊢ Eq.{u_2 + 1} (α := 𝔸)
    (if h : Nonempty.{u_2 + 1} (Algebra ℚ 𝔸) then
      FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) 0
    else 1)
    1
have pos : ∀ (h : Nonempty.{u_2 + 1} (Algebra ℚ 𝔸)),
  FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) 0 = 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
pos :
  ∀ (h : Nonempty.{u_2 + 1} (Algebra ℚ 𝔸)),
    FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) 0 = 1
⊢ Eq.{u_2 + 1} (α := 𝔸)
    (if h : Nonempty.{u_2 + 1} (Algebra ℚ 𝔸) then
      FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) 0
    else 1)
    1
have neg : ¬Nonempty.{u_2 + 1} (Algebra ℚ 𝔸) → Eq.{u_2 + 1} (α := 𝔸) 1 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
h : Nonempty.{u_2 + 1} (Algebra ℚ 𝔸)
⊢ FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) 0 = 1
have pos : Eq.{u_2 + 1} (α := 𝔸) (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (HPow.hPow (α := 𝔸) 0 n)) 1
Tactic: simp_rw [expSeries_sum_eq, ← expSeries_apply_eq, expSeries_apply_zero, tsum_pi_single]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
h : Nonempty.{u_2 + 1} (Algebra ℚ 𝔸)
pos : Eq.{u_2 + 1} (α := 𝔸) (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (HPow.hPow (α := 𝔸) 0 n)) 1
⊢ FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) 0 = 1
have pos₁ : Eq.{u_2 + 1} (α := 𝔸) (∑' (n : ℕ), (expSeries ℚ 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x : Fin n) ↦ 0) 1
Tactic: simp_rw [expSeries_sum_eq, ← expSeries_apply_eq, expSeries_apply_zero, tsum_pi_single]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
h : Nonempty.{u_2 + 1} (Algebra ℚ 𝔸)
pos : Eq.{u_2 + 1} (α := 𝔸) (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (HPow.hPow (α := 𝔸) 0 n)) 1
pos₁ : Eq.{u_2 + 1} (α := 𝔸) (∑' (n : ℕ), (expSeries ℚ 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x : Fin n) ↦ 0) 1
⊢ FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) 0 = 1
have pos₂ : Eq.{u_2 + 1} (α := 𝔸) (∑' (n : ℕ), Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 n) 1
Tactic: simp_rw [expSeries_sum_eq, ← expSeries_apply_eq, expSeries_apply_zero, tsum_pi_single]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
x : 𝔸
⊢ exp (MulOpposite.op x) = MulOpposite.op (exp x)
have inl : ∀ (h : IsEmpty.{max (u_2 + 1) 1} (Algebra ℚ 𝔸)), exp (MulOpposite.op x) = MulOpposite.op (exp x)
Tactic: obtain h | ⟨⟨_⟩⟩ := isEmpty_or_nonempty (Algebra ℚ 𝔸)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
x : 𝔸
inl : ∀ (h : IsEmpty.{max (u_2 + 1) 1} (Algebra ℚ 𝔸)), exp (MulOpposite.op x) = MulOpposite.op (exp x)
⊢ exp (MulOpposite.op x) = MulOpposite.op (exp x)
have inr : ∀ (val : Algebra ℚ 𝔸), exp (MulOpposite.op x) = MulOpposite.op (exp x)
Tactic: obtain h | ⟨⟨_⟩⟩ := isEmpty_or_nonempty (Algebra ℚ 𝔸)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (hypothesis)
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
x : 𝔸
h : IsEmpty.{max (u_2 + 1) 1} (Algebra ℚ 𝔸)
⊢ exp (MulOpposite.op x) = MulOpposite.op (exp x)
have this : IsEmpty.{max (u_2 + 1) 1} (Algebra ℚ 𝔸ᵐᵒᵖ)
Tactic: have : IsEmpty (Algebra ℚ 𝔸ᵐᵒᵖ) := ⟨fun _ => h.elim <| (RingEquiv.opOp 𝔸).algebra ℚ⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
x : 𝔸
val : Algebra ℚ 𝔸
⊢ exp (MulOpposite.op x) = MulOpposite.op (exp x)
have inr : Eq.{u_2 + 1} (α := 𝔸ᵐᵒᵖ)
  ((fun (x : 𝔸ᵐᵒᵖ) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n) : 𝔸ᵐᵒᵖ)) (MulOpposite.op x))
  (MulOpposite.op ((fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n) : 𝔸)) x))
Tactic: rw [exp_eq_tsum ℚ, exp_eq_tsum ℚ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
x : 𝔸
val : Algebra ℚ 𝔸
inr inr₁ :
  Eq.{u_2 + 1} (α := 𝔸ᵐᵒᵖ) (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (MulOpposite.op x ^ n))
    (MulOpposite.op (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n)))
⊢ Eq.{u_2 + 1} (α := 𝔸ᵐᵒᵖ)
    ((fun (x : 𝔸ᵐᵒᵖ) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n) : 𝔸ᵐᵒᵖ)) (MulOpposite.op x))
    (MulOpposite.op ((fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n) : 𝔸)) x))
have inr₂ : Eq.{u_2 + 1} (α := 𝔸ᵐᵒᵖ) (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (MulOpposite.op (x ^ n)))
  (MulOpposite.op (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n)))
Tactic: simp_rw [← MulOpposite.op_pow, ← MulOpposite.op_smul, tsum_op]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
x : 𝔸
val : Algebra ℚ 𝔸
inr inr₁ :
  Eq.{u_2 + 1} (α := 𝔸ᵐᵒᵖ) (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (MulOpposite.op x ^ n))
    (MulOpposite.op (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n)))
inr₂ :
  Eq.{u_2 + 1} (α := 𝔸ᵐᵒᵖ) (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (MulOpposite.op (x ^ n)))
    (MulOpposite.op (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n)))
⊢ Eq.{u_2 + 1} (α := 𝔸ᵐᵒᵖ)
    ((fun (x : 𝔸ᵐᵒᵖ) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n) : 𝔸ᵐᵒᵖ)) (MulOpposite.op x))
    (MulOpposite.op ((fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n) : 𝔸)) x))
have inr₃ : Eq.{u_2 + 1} (α := 𝔸ᵐᵒᵖ) (∑' (n : ℕ), MulOpposite.op (HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n)))
  (MulOpposite.op (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n)))
Tactic: simp_rw [← MulOpposite.op_pow, ← MulOpposite.op_smul, tsum_op]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
x : 𝔸ᵐᵒᵖ
⊢ exp (MulOpposite.unop x) = MulOpposite.unop (exp x)
have h : ∀ (X : 𝔸), exp (MulOpposite.unop (MulOpposite.op X)) = MulOpposite.unop (exp (MulOpposite.op X))
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
inst_4 : StarRing 𝔸
inst_5 : ContinuousStar 𝔸
x : 𝔸
⊢ star (exp x) = exp (star x)
have inl : IsEmpty.{max (u_2 + 1) 1} (Algebra ℚ 𝔸) → star (exp x) = exp (star x)
Tactic: obtain _ | ⟨⟨_⟩⟩ := isEmpty_or_nonempty (Algebra ℚ 𝔸)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
inst_4 : StarRing 𝔸
inst_5 : ContinuousStar 𝔸
x : 𝔸
inl : IsEmpty.{max (u_2 + 1) 1} (Algebra ℚ 𝔸) → star (exp x) = exp (star x)
⊢ star (exp x) = exp (star x)
have inr : ∀ (val : Algebra ℚ 𝔸), star (exp x) = exp (star x)
Tactic: obtain _ | ⟨⟨_⟩⟩ := isEmpty_or_nonempty (Algebra ℚ 𝔸)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
inst_4 : StarRing 𝔸
inst_5 : ContinuousStar 𝔸
x : 𝔸
val : Algebra ℚ 𝔸
⊢ star (exp x) = exp (star x)
have inr : Eq.{u_2 + 1} (α := 𝔸) (star (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n)))
  (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (star x ^ n))
Tactic: simp_rw [exp_eq_tsum ℚ, ← star_pow, ← star_inv_natCast_smul, ← tsum_star]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
inst_4 : StarRing 𝔸
inst_5 : ContinuousStar 𝔸
x : 𝔸
val : Algebra ℚ 𝔸
inr :
  Eq.{u_2 + 1} (α := 𝔸) (star (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n)))
    (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (star x ^ n))
⊢ star (exp x) = exp (star x)
have inr₁ : Eq.{u_2 + 1} (α := 𝔸) (star (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n)))
  (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (star (x ^ n)))
Tactic: simp_rw [exp_eq_tsum ℚ, ← star_pow, ← star_inv_natCast_smul, ← tsum_star]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
inst_4 : StarRing 𝔸
inst_5 : ContinuousStar 𝔸
x : 𝔸
val : Algebra ℚ 𝔸
inr :
  Eq.{u_2 + 1} (α := 𝔸) (star (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n)))
    (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (star x ^ n))
inr₁ :
  Eq.{u_2 + 1} (α := 𝔸) (star (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n)))
    (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (star (x ^ n)))
⊢ star (exp x) = exp (star x)
have inr₂ : Eq.{u_2 + 1} (α := 𝔸) (star (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n)))
  (∑' (n : ℕ), star (HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n)))
Tactic: simp_rw [exp_eq_tsum ℚ, ← star_pow, ← star_inv_natCast_smul, ← tsum_star]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (hypothesis)
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
R : Type u_3
S : Type u_4
inst_3 : Monoid R
inst_4 : SMul ℚ R
inst_5 : MulAction R 𝔸
inst_6 : Algebra ℚ 𝔸
inst_7 : IsScalarTower ℚ R 𝔸
inst_8 : SetLike S 𝔸
inst_9 : SubsemiringClass S 𝔸
inst_10 : SMulMemClass S R 𝔸
s : S
h_closed : IsClosed[inst_1] (↑s : Set 𝔸)
x : 𝔸
h : x ∈ s
⊢ exp x ∈ s
have this : SMulMemClass S ℚ 𝔸
Tactic: have := SMulMemClass.ofIsScalarTower S ℚ R 𝔸
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
R : Type u_3
S : Type u_4
inst_3 : Monoid R
inst_4 : SMul ℚ R
inst_5 : MulAction R 𝔸
inst_6 : Algebra ℚ 𝔸
inst_7 : IsScalarTower ℚ R 𝔸
inst_8 : SetLike S 𝔸
inst_9 : SubsemiringClass S 𝔸
inst_10 : SMulMemClass S R 𝔸
s : S
h_closed : IsClosed[inst_1] (↑s : Set 𝔸)
x : 𝔸
h : x ∈ s
this : SMulMemClass S ℚ 𝔸
⊢ exp x ∈ s
have rw : (fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n) : 𝔸)) x ∈ s
Tactic: rw [exp_eq_tsum ℚ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
x y : 𝔸
h : Commute x y
⊢ Commute x (exp y)
have inl : IsEmpty.{max (u_2 + 1) 1} (Algebra ℚ 𝔸) → Commute x (exp y)
Tactic: obtain _ | ⟨⟨_⟩⟩ := isEmpty_or_nonempty (Algebra ℚ 𝔸)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
x y : 𝔸
h : Commute x y
inl : IsEmpty.{max (u_2 + 1) 1} (Algebra ℚ 𝔸) → Commute x (exp y)
⊢ Commute x (exp y)
have inr : ∀ (val : Algebra ℚ 𝔸), Commute x (exp y)
Tactic: obtain _ | ⟨⟨_⟩⟩ := isEmpty_or_nonempty (Algebra ℚ 𝔸)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
x y : 𝔸
h : Commute x y
val : Algebra ℚ 𝔸
⊢ Commute x (exp y)
have inr : Commute x ((fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n) : 𝔸)) y)
Tactic: rw [exp_eq_tsum ℚ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : DivisionRing 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
x : 𝔸
n : ℕ
⊢ ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) = x ^ n / (↑n ! : 𝔸)
have rw : ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) = x ^ n * (↑n ! : 𝔸)⁻¹
Tactic: rw [div_eq_mul_inv, ← (Nat.cast_commute n ! (x ^ n)).inv_left₀.eq, ← smul_eq_mul,
    expSeries_apply_eq, inv_natCast_smul_eq 𝕂 𝔸]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : DivisionRing 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
x : 𝔸
n : ℕ
rw : ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) = x ^ n * (↑n ! : 𝔸)⁻¹
⊢ ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) = x ^ n / (↑n ! : 𝔸)
have rw₁ : ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) = (↑n ! : 𝔸)⁻¹ * x ^ n
Tactic: rw [div_eq_mul_inv, ← (Nat.cast_commute n ! (x ^ n)).inv_left₀.eq, ← smul_eq_mul,
    expSeries_apply_eq, inv_natCast_smul_eq 𝕂 𝔸]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : DivisionRing 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
x : 𝔸
n : ℕ
rw : ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) = x ^ n * (↑n ! : 𝔸)⁻¹
rw₁ : ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) = (↑n ! : 𝔸)⁻¹ * x ^ n
⊢ ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) = x ^ n / (↑n ! : 𝔸)
have rw₂ : ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) = HSMul.hSMul (α := 𝔸) (↑n ! : 𝔸)⁻¹ (x ^ n)
Tactic: rw [div_eq_mul_inv, ← (Nat.cast_commute n ! (x ^ n)).inv_left₀.eq, ← smul_eq_mul,
    expSeries_apply_eq, inv_natCast_smul_eq 𝕂 𝔸]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : DivisionRing 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
x : 𝔸
n : ℕ
rw : ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) = x ^ n * (↑n ! : 𝔸)⁻¹
rw₁ : ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) = (↑n ! : 𝔸)⁻¹ * x ^ n
rw₂ : ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) = HSMul.hSMul (α := 𝔸) (↑n ! : 𝔸)⁻¹ (x ^ n)
⊢ ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) = x ^ n / (↑n ! : 𝔸)
have rw₃ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n) = HSMul.hSMul (α := 𝔸) (↑n ! : 𝔸)⁻¹ (x ^ n)
Tactic: rw [div_eq_mul_inv, ← (Nat.cast_commute n ! (x ^ n)).inv_left₀.eq, ← smul_eq_mul,
    expSeries_apply_eq, inv_natCast_smul_eq 𝕂 𝔸]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : DivisionRing 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
x : 𝔸
n : ℕ
rw : ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) = x ^ n * (↑n ! : 𝔸)⁻¹
rw₁ : ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) = (↑n ! : 𝔸)⁻¹ * x ^ n
rw₂ : ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) = HSMul.hSMul (α := 𝔸) (↑n ! : 𝔸)⁻¹ (x ^ n)
rw₃ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n) = HSMul.hSMul (α := 𝔸) (↑n ! : 𝔸)⁻¹ (x ^ n)
⊢ ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) = x ^ n / (↑n ! : 𝔸)
have rw₄ : HSMul.hSMul (α := 𝔸) (↑n ! : 𝔸)⁻¹ (x ^ n) = HSMul.hSMul (α := 𝔸) (↑n ! : 𝔸)⁻¹ (x ^ n)
Tactic: rw [div_eq_mul_inv, ← (Nat.cast_commute n ! (x ^ n)).inv_left₀.eq, ← smul_eq_mul,
    expSeries_apply_eq, inv_natCast_smul_eq 𝕂 𝔸]
-- 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 𝔸
⊢ Eq.{u_2 + 1} (α := (x : 𝔸) → 𝔸) exp fun (x : 𝔸) ↦ ∑' (n : ℕ), x ^ n / (↑n ! : 𝔸)
have rw : FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) = fun (x : 𝔸) ↦
  ∑' (n : ℕ), x ^ n / (↑n ! : 𝔸)
Tactic: rw [exp_eq_expSeries_sum ℚ]