awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
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
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))
⊢ 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)

Tactic:
rw [← hasSum_nat_add_iff' 1]

Premises used: hasSum_nat_add_iff', OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
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
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))
⊢ 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:
simp_rw [snd_expSeries_of_smul_comm _ _ hx]

Premises used: TrivSqZeroExt.snd_expSeries_of_smul_comm
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
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
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)
⊢ 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 [expSeries_apply_eq] at *

Premises used: NormedSpace.expSeries_apply_eq
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
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
rw : HasSum (fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd) (e • x.snd)
⊢ 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:
rw [Finset.range_one, Finset.sum_singleton, Nat.factorial_zero, Nat.cast_one, pow_zero,
    inv_one, one_smul, snd_one, sub_zero]

Premises used: inv_one, sub_zero, pow_zero, one_smul, Finset.sum_singleton, TrivSqZeroExt.snd_one, Finset.range_one, Nat.factorial_zero, Nat.cast_one
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
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)

Tactic:
h.smul_const _

Premises used: HasSum.smul_const
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
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)

Tactic:
exact h.smul_const _

Premises used: HasSum.smul_const
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
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 : ℕ) ↦
      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:
simpa [fst_expSeries] using h

Premises used: TrivSqZeroExt.fst_expSeries
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
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 : ℕ) ↦
      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
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
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
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
⊢ 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))

Tactic:
simpa only [inl_fst_add_inr_snd_eq] using
    (hasSum_inl _ <| this).add (hasSum_inr _ <| hasSum_snd_expSeries_of_smul_comm 𝕜 x hx h)

Premises used: HasSum.add, TrivSqZeroExt.hasSum_inr, TrivSqZeroExt.inl_fst_add_inr_snd_eq, TrivSqZeroExt.hasSum_snd_expSeries_of_smul_comm, TrivSqZeroExt.hasSum_inl
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
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
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))
⊢ exp x = inl (exp x.fst) + inr (exp x.fst • x.snd)

Tactic:
simp_rw [exp_eq_expSeries_sum ℚ, FormalMultilinearSeries.sum]

Premises used: Rat, FormalMultilinearSeries.sum, NormedSpace.exp_eq_expSeries_sum
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
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))
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))
⊢ (∑' (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)

Premises used: Rat, TrivSqZeroExt.fst, NormedSpace.expSeries, Summable, DFunLike.coe, SummationFilter.unconditional
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
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))

Tactic:
(hasSum_expSeries_of_smul_comm ℚ x hx ?_).tsum_eq

Premises used: Rat, TrivSqZeroExt.hasSum_expSeries_of_smul_comm, HasSum.tsum_eq
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
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
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)
⊢ (∑' (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:
refine (hasSum_expSeries_of_smul_comm ℚ x hx ?_).tsum_eq

Premises used: Rat, TrivSqZeroExt.hasSum_expSeries_of_smul_comm, HasSum.tsum_eq
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
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
⊢ 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:
h.hasSum

Premises used: Summable.hasSum
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
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
⊢ 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:
exact h.hasSum

Premises used: Summable.hasSum
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
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
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
⊢ (∑' (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:
rw [tsum_eq_zero_of_not_summable h, zero_smul, inr_zero, inl_zero, zero_add,
      tsum_eq_zero_of_not_summable]

Premises used: zero_add, zero_smul, tsum_eq_zero_of_not_summable, TrivSqZeroExt.inl_zero, TrivSqZeroExt.inr_zero
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
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.{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

Premises used: TrivSqZeroExt.fst_expSeries
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
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 : ℕ) ↦
      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)
⊢ ¬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:
mt ?_ h

Premises used: mt
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
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 : ℕ) ↦
      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)
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) →
    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)
⊢ ¬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:
refine mt ?_ h

Premises used: mt