awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
Goal:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst : Field 𝕜
inst_1 : CharZero 𝕜
inst_2 : Ring R
inst_3 : AddCommGroup M
inst_4 : Algebra 𝕜 R
inst_5 : Module 𝕜 M
inst_6 : Module R M
inst_7 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower 𝕜 R M
inst_10 : IsScalarTower.{u_1, u_3, u_4} 𝕜 Rᵐᵒᵖ M
inst_11 : TopologicalSpace R
inst_12 : TopologicalSpace M
inst_13 : IsTopologicalRing R
inst_14 : IsTopologicalAddGroup M
inst_15 : ContinuousSMul R M
inst_16 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
n : ℕ
simp_rw :
  (HSMul.hSMul (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (x ^ (n + 1))).snd =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₁ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (x ^ (n + 1)).snd =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₂ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ ((n + 1) • x.fst ^ (n + 1).pred • x.snd) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₃ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1) : 𝕜) (x.fst ^ (n + 1).pred • x.snd)) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₄ :
  HMul.hMul (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (↑(n + 1) : 𝕜) • x.fst ^ (n + 1).pred • x.snd =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₅ :
  HMul.hMul (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (↑(n + 1) : 𝕜) • x.fst ^ (n + 1).pred • x.snd =
    HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n • x.snd)
simp_rw₆ :
  HMul.hMul (α := 𝕜) (↑((n + 1) * n.factorial) : 𝕜)⁻¹ (↑(n + 1) : 𝕜) • x.fst ^ (n + 1).pred • x.snd =
    HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n • x.snd)
⊢ snd.{u_3, u_4} (R := R)
      ((expSeries 𝕜 (tsze R M) (n + 1) : (a : (i : Fin (n + 1)) → tsze R M) → tsze R M) fun (x_1 : Fin (n + 1)) ↦ x) =
    HSMul.hSMul (α := R) ((expSeries 𝕜 R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst : R) x.snd
have simp_rw₇ : HMul.hMul (α := 𝕜) (↑((n + 1) * n.factorial) : 𝕜)⁻¹ (↑(n + 1) : 𝕜) • x.fst ^ n • x.snd =
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n • x.snd)
Tactic: simp_rw [expSeries_apply_eq, snd_smul, snd_pow_of_smul_comm _ _ hx,
    ← Nat.cast_smul_eq_nsmul 𝕜 (n + 1), smul_smul, smul_assoc, Nat.factorial_succ, Nat.pred_succ,
    Nat.cast_mul, mul_inv_rev,
    inv_mul_cancel_right₀ ((Nat.cast_ne_zero (R := 𝕜)).mpr <| Nat.succ_ne_zero n)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
Goal:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst : Field 𝕜
inst_1 : CharZero 𝕜
inst_2 : Ring R
inst_3 : AddCommGroup M
inst_4 : Algebra 𝕜 R
inst_5 : Module 𝕜 M
inst_6 : Module R M
inst_7 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower 𝕜 R M
inst_10 : IsScalarTower.{u_1, u_3, u_4} 𝕜 Rᵐᵒᵖ M
inst_11 : TopologicalSpace R
inst_12 : TopologicalSpace M
inst_13 : IsTopologicalRing R
inst_14 : IsTopologicalAddGroup M
inst_15 : ContinuousSMul R M
inst_16 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
n : ℕ
simp_rw :
  (HSMul.hSMul (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (x ^ (n + 1))).snd =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₁ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (x ^ (n + 1)).snd =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₂ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ ((n + 1) • x.fst ^ (n + 1).pred • x.snd) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₃ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1) : 𝕜) (x.fst ^ (n + 1).pred • x.snd)) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₄ :
  HMul.hMul (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (↑(n + 1) : 𝕜) • x.fst ^ (n + 1).pred • x.snd =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₅ :
  HMul.hMul (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (↑(n + 1) : 𝕜) • x.fst ^ (n + 1).pred • x.snd =
    HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n • x.snd)
simp_rw₆ :
  HMul.hMul (α := 𝕜) (↑((n + 1) * n.factorial) : 𝕜)⁻¹ (↑(n + 1) : 𝕜) • x.fst ^ (n + 1).pred • x.snd =
    HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n • x.snd)
simp_rw₇ :
  HMul.hMul (α := 𝕜) (↑((n + 1) * n.factorial) : 𝕜)⁻¹ (↑(n + 1) : 𝕜) • x.fst ^ n • x.snd =
    HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n • x.snd)
⊢ snd.{u_3, u_4} (R := R)
      ((expSeries 𝕜 (tsze R M) (n + 1) : (a : (i : Fin (n + 1)) → tsze R M) → tsze R M) fun (x_1 : Fin (n + 1)) ↦ x) =
    HSMul.hSMul (α := R) ((expSeries 𝕜 R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst : R) x.snd
have simp_rw₈ : ((HMul.hMul (α := 𝕜) (↑(n + 1) : 𝕜) (↑n.factorial : 𝕜))⁻¹ * (↑(n + 1) : 𝕜)) • x.fst ^ n • x.snd =
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n • x.snd)
Tactic: simp_rw [expSeries_apply_eq, snd_smul, snd_pow_of_smul_comm _ _ hx,
    ← Nat.cast_smul_eq_nsmul 𝕜 (n + 1), smul_smul, smul_assoc, Nat.factorial_succ, Nat.pred_succ,
    Nat.cast_mul, mul_inv_rev,
    inv_mul_cancel_right₀ ((Nat.cast_ne_zero (R := 𝕜)).mpr <| Nat.succ_ne_zero n)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
Goal:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst : Field 𝕜
inst_1 : CharZero 𝕜
inst_2 : Ring R
inst_3 : AddCommGroup M
inst_4 : Algebra 𝕜 R
inst_5 : Module 𝕜 M
inst_6 : Module R M
inst_7 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower 𝕜 R M
inst_10 : IsScalarTower.{u_1, u_3, u_4} 𝕜 Rᵐᵒᵖ M
inst_11 : TopologicalSpace R
inst_12 : TopologicalSpace M
inst_13 : IsTopologicalRing R
inst_14 : IsTopologicalAddGroup M
inst_15 : ContinuousSMul R M
inst_16 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
n : ℕ
simp_rw :
  (HSMul.hSMul (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (x ^ (n + 1))).snd =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₁ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (x ^ (n + 1)).snd =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₂ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ ((n + 1) • x.fst ^ (n + 1).pred • x.snd) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₃ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1) : 𝕜) (x.fst ^ (n + 1).pred • x.snd)) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₄ :
  HMul.hMul (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (↑(n + 1) : 𝕜) • x.fst ^ (n + 1).pred • x.snd =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₅ :
  HMul.hMul (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (↑(n + 1) : 𝕜) • x.fst ^ (n + 1).pred • x.snd =
    HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n • x.snd)
simp_rw₆ :
  HMul.hMul (α := 𝕜) (↑((n + 1) * n.factorial) : 𝕜)⁻¹ (↑(n + 1) : 𝕜) • x.fst ^ (n + 1).pred • x.snd =
    HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n • x.snd)
simp_rw₇ :
  HMul.hMul (α := 𝕜) (↑((n + 1) * n.factorial) : 𝕜)⁻¹ (↑(n + 1) : 𝕜) • x.fst ^ n • x.snd =
    HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n • x.snd)
simp_rw₈ :
  ((HMul.hMul (α := 𝕜) (↑(n + 1) : 𝕜) (↑n.factorial : 𝕜))⁻¹ * (↑(n + 1) : 𝕜)) • x.fst ^ n • x.snd =
    HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n • x.snd)
⊢ snd.{u_3, u_4} (R := R)
      ((expSeries 𝕜 (tsze R M) (n + 1) : (a : (i : Fin (n + 1)) → tsze R M) → tsze R M) fun (x_1 : Fin (n + 1)) ↦ x) =
    HSMul.hSMul (α := R) ((expSeries 𝕜 R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst : R) x.snd
have simp_rw₉ : (HMul.hMul (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (↑(n + 1) : 𝕜)⁻¹ * (↑(n + 1) : 𝕜)) • x.fst ^ n • x.snd =
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n • x.snd)
Tactic: simp_rw [expSeries_apply_eq, snd_smul, snd_pow_of_smul_comm _ _ hx,
    ← Nat.cast_smul_eq_nsmul 𝕜 (n + 1), smul_smul, smul_assoc, Nat.factorial_succ, Nat.pred_succ,
    Nat.cast_mul, mul_inv_rev,
    inv_mul_cancel_right₀ ((Nat.cast_ne_zero (R := 𝕜)).mpr <| Nat.succ_ne_zero n)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
Goal:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst : Field 𝕜
inst_1 : CharZero 𝕜
inst_2 : Ring R
inst_3 : AddCommGroup M
inst_4 : Algebra 𝕜 R
inst_5 : Module 𝕜 M
inst_6 : Module R M
inst_7 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower 𝕜 R M
inst_10 : IsScalarTower.{u_1, u_3, u_4} 𝕜 Rᵐᵒᵖ M
inst_11 : TopologicalSpace R
inst_12 : TopologicalSpace M
inst_13 : IsTopologicalRing R
inst_14 : IsTopologicalAddGroup M
inst_15 : ContinuousSMul R M
inst_16 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
e : R
h : HasSum (fun (n : ℕ) ↦ (expSeries 𝕜 R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst) e
⊢ HasSum
    (fun (n : ℕ) ↦
      snd.{u_3, u_4} (R := R)
        ((expSeries 𝕜 (tsze R M) n : (a : (i : Fin n) → tsze R M) → tsze R M) fun (x_1 : Fin n) ↦ x))
    (e • x.snd)
have rw : HasSum
  (fun (n : ℕ) ↦
    snd.{u_3, u_4} (R := R)
      ((expSeries 𝕜 (tsze R M) (n + 1) : (a : (i : Fin (n + 1)) → tsze R M) → tsze R M) fun (x_1 : Fin (n + 1)) ↦ x))
  (e • x.snd -
    ∑ i ∈ Finset.range 1,
      snd.{u_3, u_4} (R := R)
        ((expSeries 𝕜 (tsze R M) i : (a : (i : Fin i) → tsze R M) → tsze R M) fun (x_1 : Fin i) ↦ x))
Tactic: rw [← hasSum_nat_add_iff' 1]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
Goal:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst : Field 𝕜
inst_1 : CharZero 𝕜
inst_2 : Ring R
inst_3 : AddCommGroup M
inst_4 : Algebra 𝕜 R
inst_5 : Module 𝕜 M
inst_6 : Module R M
inst_7 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower 𝕜 R M
inst_10 : IsScalarTower.{u_1, u_3, u_4} 𝕜 Rᵐᵒᵖ M
inst_11 : TopologicalSpace R
inst_12 : TopologicalSpace M
inst_13 : IsTopologicalRing R
inst_14 : IsTopologicalAddGroup M
inst_15 : ContinuousSMul R M
inst_16 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
e : R
h : HasSum (fun (n : ℕ) ↦ (expSeries 𝕜 R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst) e
⊢ HasSum
    (fun (n : ℕ) ↦
      snd.{u_3, u_4} (R := R)
        ((expSeries 𝕜 (tsze R M) (n + 1) : (a : (i : Fin (n + 1)) → tsze R M) → tsze R M) fun (x_1 : Fin (n + 1)) ↦ x))
    (e • x.snd -
      ∑ i ∈ Finset.range 1,
        snd.{u_3, u_4} (R := R)
          ((expSeries 𝕜 (tsze R M) i : (a : (i : Fin i) → tsze R M) → tsze R M) fun (x_1 : Fin i) ↦ x))
have simp_rw : HasSum
  (fun (n : ℕ) ↦
    HSMul.hSMul (α := R) ((expSeries 𝕜 R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst : R) x.snd)
  (e • x.snd -
    ∑ i ∈ Finset.range 1,
      snd.{u_3, u_4} (R := R)
        ((expSeries 𝕜 (tsze R M) i : (a : (i : Fin i) → tsze R M) → tsze R M) fun (x_1 : Fin i) ↦ x))
Tactic: simp_rw [snd_expSeries_of_smul_comm _ _ hx]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
Goal:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst : Field 𝕜
inst_1 : CharZero 𝕜
inst_2 : Ring R
inst_3 : AddCommGroup M
inst_4 : Algebra 𝕜 R
inst_5 : Module 𝕜 M
inst_6 : Module R M
inst_7 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower 𝕜 R M
inst_10 : IsScalarTower.{u_1, u_3, u_4} 𝕜 Rᵐᵒᵖ M
inst_11 : TopologicalSpace R
inst_12 : TopologicalSpace M
inst_13 : IsTopologicalRing R
inst_14 : IsTopologicalAddGroup M
inst_15 : ContinuousSMul R M
inst_16 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
e : R
h : HasSum (fun (n : ℕ) ↦ (expSeries 𝕜 R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst) e
⊢ HasSum
    (fun (n : ℕ) ↦
      HSMul.hSMul (α := R) ((expSeries 𝕜 R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst : R) x.snd)
    (e • x.snd -
      ∑ i ∈ Finset.range 1,
        snd.{u_3, u_4} (R := R)
          ((expSeries 𝕜 (tsze R M) i : (a : (i : Fin i) → tsze R M) → tsze R M) fun (x_1 : Fin i) ↦ x))
have simp_rw : ∀ (h : HasSum (fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n)) e),
  HasSum (fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd)
    (e • x.snd - ∑ x_1 ∈ Finset.range 1, (HSMul.hSMul (α := 𝕜) (↑x_1.factorial : 𝕜)⁻¹ (x ^ x_1)).snd)
Tactic: simp_rw [expSeries_apply_eq] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
Goal:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst : Field 𝕜
inst_1 : CharZero 𝕜
inst_2 : Ring R
inst_3 : AddCommGroup M
inst_4 : Algebra 𝕜 R
inst_5 : Module 𝕜 M
inst_6 : Module R M
inst_7 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower 𝕜 R M
inst_10 : IsScalarTower.{u_1, u_3, u_4} 𝕜 Rᵐᵒᵖ M
inst_11 : TopologicalSpace R
inst_12 : TopologicalSpace M
inst_13 : IsTopologicalRing R
inst_14 : IsTopologicalAddGroup M
inst_15 : ContinuousSMul R M
inst_16 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
e : R
h : HasSum (fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n)) e
⊢ HasSum (fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd)
    (e • x.snd - ∑ x_1 ∈ Finset.range 1, (HSMul.hSMul (α := 𝕜) (↑x_1.factorial : 𝕜)⁻¹ (x ^ x_1)).snd)
have rw : HasSum (fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd) (e • x.snd)
Tactic: rw [Finset.range_one, Finset.sum_singleton, Nat.factorial_zero, Nat.cast_one, pow_zero,
    inv_one, one_smul, snd_one, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (hypothesis)
Goal:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst : Field 𝕜
inst_1 : CharZero 𝕜
inst_2 : Ring R
inst_3 : AddCommGroup M
inst_4 : Algebra 𝕜 R
inst_5 : Module 𝕜 M
inst_6 : Module R M
inst_7 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower 𝕜 R M
inst_10 : IsScalarTower.{u_1, u_3, u_4} 𝕜 Rᵐᵒᵖ M
inst_11 : TopologicalSpace R
inst_12 : TopologicalSpace M
inst_13 : IsTopologicalRing R
inst_14 : IsTopologicalAddGroup M
inst_15 : ContinuousSMul R M
inst_16 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
e : R
h : HasSum (fun (n : ℕ) ↦ (expSeries 𝕜 R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst) e
⊢ HasSum (fun (n : ℕ) ↦ (expSeries 𝕜 (tsze R M) n : (a : (i : Fin n) → tsze R M) → tsze R M) fun (x_1 : Fin n) ↦ x)
    (inl e + inr (e • x.snd))
have this : HasSum
  (fun (n : ℕ) ↦
    fst.{u_3, u_4} (M := M)
      ((expSeries 𝕜 (tsze R M) n : (a : (i : Fin n) → tsze R M) → tsze R M) fun (x_1 : Fin n) ↦ x))
  e
Tactic: have : HasSum (fun n => fst (expSeries 𝕜 (tsze R M) n fun _ => x)) e := by
    simpa [fst_expSeries] using h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
Goal:
R : Type u_3
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
inst_5 : TopologicalSpace R
inst_6 : TopologicalSpace M
inst_7 : IsTopologicalRing R
inst_8 : IsTopologicalAddGroup M
inst_9 : ContinuousSMul R M
inst_10 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_11 : Algebra ℚ R
inst_12 : Module ℚ M
inst_13 : T2Space R
inst_14 : T2Space M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
⊢ exp x = inl (exp x.fst) + inr (exp x.fst • x.snd)
have simp_rw : (∑' (n : ℕ), (expSeries ℚ (tsze R M) n : (a : (i : Fin n) → tsze R M) → tsze R M) fun (x_1 : Fin n) ↦ x) =
  HAdd.hAdd (α := tsze R M) (inl (∑' (n : ℕ), (expSeries ℚ R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst))
    (inr
      (HSMul.hSMul.{u_3, u_4, u_4} (α := R)
        (∑' (n : ℕ), (expSeries ℚ R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst) x.snd))
Tactic: simp_rw [exp_eq_expSeries_sum ℚ, FormalMultilinearSeries.sum]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
Goal:
R : Type u_3
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
inst_5 : TopologicalSpace R
inst_6 : TopologicalSpace M
inst_7 : IsTopologicalRing R
inst_8 : IsTopologicalAddGroup M
inst_9 : ContinuousSMul R M
inst_10 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_11 : Algebra ℚ R
inst_12 : Module ℚ M
inst_13 : T2Space R
inst_14 : T2Space M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
⊢ (∑' (n : ℕ), (expSeries ℚ (tsze R M) n : (a : (i : Fin n) → tsze R M) → tsze R M) fun (x_1 : Fin n) ↦ x) =
    HAdd.hAdd (α := tsze R M)
      (inl (∑' (n : ℕ), (expSeries ℚ R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst))
      (inr
        (HSMul.hSMul.{u_3, u_4, u_4} (α := R)
          (∑' (n : ℕ), (expSeries ℚ R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst) x.snd))
have pos : ∀
  (h :
    Summable.{u_3, 0} (α := R) fun (n : ℕ) ↦ (expSeries ℚ R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst),
  (∑' (n : ℕ), (expSeries ℚ (tsze R M) n : (a : (i : Fin n) → tsze R M) → tsze R M) fun (x_1 : Fin n) ↦ x) =
    HAdd.hAdd (α := tsze R M)
      (inl (∑' (n : ℕ), (expSeries ℚ R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst))
      (inr
        (HSMul.hSMul.{u_3, u_4, u_4} (α := R)
          (∑' (n : ℕ), (expSeries ℚ R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst) x.snd))
Tactic: by_cases h : Summable (fun (n : ℕ) => (expSeries ℚ R n) fun _ ↦ fst x)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
Goal:
R : Type u_3
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
inst_5 : TopologicalSpace R
inst_6 : TopologicalSpace M
inst_7 : IsTopologicalRing R
inst_8 : IsTopologicalAddGroup M
inst_9 : ContinuousSMul R M
inst_10 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_11 : Algebra ℚ R
inst_12 : Module ℚ M
inst_13 : T2Space R
inst_14 : T2Space M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
pos :
  ∀
    (h :
      Summable.{u_3, 0} (α := R) fun (n : ℕ) ↦ (expSeries ℚ R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst),
    (∑' (n : ℕ), (expSeries ℚ (tsze R M) n : (a : (i : Fin n) → tsze R M) → tsze R M) fun (x_1 : Fin n) ↦ x) =
      HAdd.hAdd (α := tsze R M)
        (inl (∑' (n : ℕ), (expSeries ℚ R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst))
        (inr
          (HSMul.hSMul.{u_3, u_4, u_4} (α := R)
            (∑' (n : ℕ), (expSeries ℚ R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst) x.snd))
⊢ (∑' (n : ℕ), (expSeries ℚ (tsze R M) n : (a : (i : Fin n) → tsze R M) → tsze R M) fun (x_1 : Fin n) ↦ x) =
    HAdd.hAdd (α := tsze R M)
      (inl (∑' (n : ℕ), (expSeries ℚ R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst))
      (inr
        (HSMul.hSMul.{u_3, u_4, u_4} (α := R)
          (∑' (n : ℕ), (expSeries ℚ R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst) x.snd))
have neg : ∀
  (h :
    ¬Summable.{u_3, 0} (α := R) fun (n : ℕ) ↦ (expSeries ℚ R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst),
  (∑' (n : ℕ), (expSeries ℚ (tsze R M) n : (a : (i : Fin n) → tsze R M) → tsze R M) fun (x_1 : Fin n) ↦ x) =
    HAdd.hAdd (α := tsze R M)
      (inl (∑' (n : ℕ), (expSeries ℚ R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst))
      (inr
        (HSMul.hSMul.{u_3, u_4, u_4} (α := R)
          (∑' (n : ℕ), (expSeries ℚ R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst) x.snd))
Tactic: by_cases h : Summable (fun (n : ℕ) => (expSeries ℚ R n) fun _ ↦ fst x)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
Goal:
R : Type u_3
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
inst_5 : TopologicalSpace R
inst_6 : TopologicalSpace M
inst_7 : IsTopologicalRing R
inst_8 : IsTopologicalAddGroup M
inst_9 : ContinuousSMul R M
inst_10 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_11 : Algebra ℚ R
inst_12 : Module ℚ M
inst_13 : T2Space R
inst_14 : T2Space M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
h : Summable.{u_3, 0} (α := R) fun (n : ℕ) ↦ (expSeries ℚ R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst
⊢ (∑' (n : ℕ), (expSeries ℚ (tsze R M) n : (a : (i : Fin n) → tsze R M) → tsze R M) fun (x_1 : Fin n) ↦ x) =
    HAdd.hAdd (α := tsze R M)
      (inl (∑' (n : ℕ), (expSeries ℚ R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst))
      (inr
        (HSMul.hSMul.{u_3, u_4, u_4} (α := R)
          (∑' (n : ℕ), (expSeries ℚ R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst) x.snd))
have pos : HasSum.{u_3, 0} (α := R) (fun (n : ℕ) ↦ (expSeries ℚ R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst)
  (∑' (n : ℕ), (expSeries ℚ R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst)
Tactic: refine (hasSum_expSeries_of_smul_comm ℚ x hx ?_).tsum_eq
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
Goal:
R : Type u_3
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
inst_5 : TopologicalSpace R
inst_6 : TopologicalSpace M
inst_7 : IsTopologicalRing R
inst_8 : IsTopologicalAddGroup M
inst_9 : ContinuousSMul R M
inst_10 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_11 : Algebra ℚ R
inst_12 : Module ℚ M
inst_13 : T2Space R
inst_14 : T2Space M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
h : ¬Summable.{u_3, 0} (α := R) fun (n : ℕ) ↦ (expSeries ℚ R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst
⊢ (∑' (n : ℕ), (expSeries ℚ (tsze R M) n : (a : (i : Fin n) → tsze R M) → tsze R M) fun (x_1 : Fin n) ↦ x) =
    HAdd.hAdd (α := tsze R M)
      (inl (∑' (n : ℕ), (expSeries ℚ R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst))
      (inr
        (HSMul.hSMul.{u_3, u_4, u_4} (α := R)
          (∑' (n : ℕ), (expSeries ℚ R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst) x.snd))
have neg : ¬Summable (α := tsze R M) fun (n : ℕ) ↦
    (expSeries ℚ (tsze R M) n : (a : (i : Fin n) → tsze R M) → tsze R M) fun (x_1 : Fin n) ↦ x
Tactic: rw [tsum_eq_zero_of_not_summable h, zero_smul, inr_zero, inl_zero, zero_add,
      tsum_eq_zero_of_not_summable]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (hypothesis)
Goal:
R : Type u_3
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
inst_5 : TopologicalSpace R
inst_6 : TopologicalSpace M
inst_7 : IsTopologicalRing R
inst_8 : IsTopologicalAddGroup M
inst_9 : ContinuousSMul R M
inst_10 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_11 : Algebra ℚ R
inst_12 : Module ℚ M
inst_13 : T2Space R
inst_14 : T2Space M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
h : ¬Summable.{u_3, 0} (α := R) fun (n : ℕ) ↦ (expSeries ℚ R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst
⊢ ¬Summable (α := tsze R M) fun (n : ℕ) ↦
      (expSeries ℚ (tsze R M) n : (a : (i : Fin n) → tsze R M) → tsze R M) fun (x_1 : Fin n) ↦ x
have h₁ : ¬Summable.{u_3, 0} (α := R) fun (n : ℕ) ↦
    fst.{u_3, u_4} (M := M) ((expSeries ℚ (tsze R M) n : (a : (i : Fin n) → tsze R M) → tsze R M) fun (x_1 : Fin n) ↦ x)
Tactic: simp_rw [← fst_expSeries] at h
Cleared hypotheses: h