-- Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean
theorem exp_def_of_smul_comm (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)

Proof state:
case neg
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁸ : Field 𝕜
inst✝¹⁷ : CharZero 𝕜
inst✝¹⁶ : Ring R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Algebra 𝕜 R
inst✝¹³ : Module 𝕜 M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalSpace M
inst✝⁵ : IsTopologicalRing R
inst✝⁴ : IsTopologicalAddGroup M
inst✝³ : ContinuousSMul R M
inst✝² : ContinuousSMul Rᵐᵒᵖ M
inst✝¹ : T2Space R
inst✝ : T2Space M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
h : ¬Summable fun n => ((expSeries 𝕜 (tsze R M) n) fun x_1 => x).fst
⊢ ¬Summable fun n => (expSeries 𝕜 (tsze R M) n) fun x_1 => x

Tactic:
refine mt ?_ h

Result:
case neg
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁸ : Field 𝕜
inst✝¹⁷ : CharZero 𝕜
inst✝¹⁶ : Ring R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Algebra 𝕜 R
inst✝¹³ : Module 𝕜 M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalSpace M
inst✝⁵ : IsTopologicalRing R
inst✝⁴ : IsTopologicalAddGroup M
inst✝³ : ContinuousSMul R M
inst✝² : ContinuousSMul Rᵐᵒᵖ M
inst✝¹ : T2Space R
inst✝ : T2Space M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
h : ¬Summable fun n => ((expSeries 𝕜 (tsze R M) n) fun x_1 => x).fst
⊢ (Summable fun n => (expSeries 𝕜 (tsze R M) n) fun x_1 => x) →
    Summable fun n => ((expSeries 𝕜 (tsze R M) n) fun x_1 => x).fst

Proof state:
case pos
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁸ : Field 𝕜
inst✝¹⁷ : CharZero 𝕜
inst✝¹⁶ : Ring R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Algebra 𝕜 R
inst✝¹³ : Module 𝕜 M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalSpace M
inst✝⁵ : IsTopologicalRing R
inst✝⁴ : IsTopologicalAddGroup M
inst✝³ : ContinuousSMul R M
inst✝² : ContinuousSMul Rᵐᵒᵖ M
inst✝¹ : T2Space R
inst✝ : T2Space M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
h : Summable fun n => (expSeries 𝕜 R n) fun x_1 => x.fst
⊢ HasSum (fun n => (expSeries 𝕜 R n) fun x_1 => x.fst) (∑' (n : ℕ), (expSeries 𝕜 R n) fun x_1 => x.fst)

Tactic:
exact h.hasSum

Result:
no goals

Proof state:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁸ : Field 𝕜
inst✝¹⁷ : CharZero 𝕜
inst✝¹⁶ : Ring R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Algebra 𝕜 R
inst✝¹³ : Module 𝕜 M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalSpace M
inst✝⁵ : IsTopologicalRing R
inst✝⁴ : IsTopologicalAddGroup M
inst✝³ : ContinuousSMul R M
inst✝² : ContinuousSMul Rᵐᵒᵖ M
inst✝¹ : T2Space R
inst✝ : 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)

Tactic:
simp_rw [exp, FormalMultilinearSeries.sum]

Result:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁸ : Field 𝕜
inst✝¹⁷ : CharZero 𝕜
inst✝¹⁶ : Ring R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Algebra 𝕜 R
inst✝¹³ : Module 𝕜 M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalSpace M
inst✝⁵ : IsTopologicalRing R
inst✝⁴ : IsTopologicalAddGroup M
inst✝³ : ContinuousSMul R M
inst✝² : ContinuousSMul Rᵐᵒᵖ M
inst✝¹ : T2Space R
inst✝ : T2Space M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
⊢ (∑' (n : ℕ), (expSeries 𝕜 (tsze R M) n) fun x_1 => x) =
    inl (∑' (n : ℕ), (expSeries 𝕜 R n) fun x_1 => x.fst) +
      inr ((∑' (n : ℕ), (expSeries 𝕜 R n) fun x_1 => x.fst) • x.snd)

Proof state:
case neg
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁸ : Field 𝕜
inst✝¹⁷ : CharZero 𝕜
inst✝¹⁶ : Ring R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Algebra 𝕜 R
inst✝¹³ : Module 𝕜 M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalSpace M
inst✝⁵ : IsTopologicalRing R
inst✝⁴ : IsTopologicalAddGroup M
inst✝³ : ContinuousSMul R M
inst✝² : ContinuousSMul Rᵐᵒᵖ M
inst✝¹ : T2Space R
inst✝ : T2Space M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
h : ¬Summable fun n => (expSeries 𝕜 R n) fun x_1 => x.fst
⊢ ¬Summable fun n => (expSeries 𝕜 (tsze R M) n) fun x_1 => x

Tactic:
simp_rw [← fst_expSeries] at h

Result:
case neg
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁸ : Field 𝕜
inst✝¹⁷ : CharZero 𝕜
inst✝¹⁶ : Ring R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Algebra 𝕜 R
inst✝¹³ : Module 𝕜 M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalSpace M
inst✝⁵ : IsTopologicalRing R
inst✝⁴ : IsTopologicalAddGroup M
inst✝³ : ContinuousSMul R M
inst✝² : ContinuousSMul Rᵐᵒᵖ M
inst✝¹ : T2Space R
inst✝ : T2Space M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
h : ¬Summable fun n => ((expSeries 𝕜 (tsze R M) n) fun x_1 => x).fst
⊢ ¬Summable fun n => (expSeries 𝕜 (tsze R M) n) fun x_1 => x

Proof state:
case pos
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁸ : Field 𝕜
inst✝¹⁷ : CharZero 𝕜
inst✝¹⁶ : Ring R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Algebra 𝕜 R
inst✝¹³ : Module 𝕜 M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalSpace M
inst✝⁵ : IsTopologicalRing R
inst✝⁴ : IsTopologicalAddGroup M
inst✝³ : ContinuousSMul R M
inst✝² : ContinuousSMul Rᵐᵒᵖ M
inst✝¹ : T2Space R
inst✝ : T2Space M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
h : Summable fun n => (expSeries 𝕜 R n) fun x_1 => x.fst
⊢ (∑' (n : ℕ), (expSeries 𝕜 (tsze R M) n) fun x_1 => x) =
    inl (∑' (n : ℕ), (expSeries 𝕜 R n) fun x_1 => x.fst) +
      inr ((∑' (n : ℕ), (expSeries 𝕜 R n) fun x_1 => x.fst) • x.snd)

Tactic:
refine (hasSum_expSeries_of_smul_comm 𝕜 x hx ?_).tsum_eq

Result:
case pos
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁸ : Field 𝕜
inst✝¹⁷ : CharZero 𝕜
inst✝¹⁶ : Ring R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Algebra 𝕜 R
inst✝¹³ : Module 𝕜 M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalSpace M
inst✝⁵ : IsTopologicalRing R
inst✝⁴ : IsTopologicalAddGroup M
inst✝³ : ContinuousSMul R M
inst✝² : ContinuousSMul Rᵐᵒᵖ M
inst✝¹ : T2Space R
inst✝ : T2Space M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
h : Summable fun n => (expSeries 𝕜 R n) fun x_1 => x.fst
⊢ HasSum (fun n => (expSeries 𝕜 R n) fun x_1 => x.fst) (∑' (n : ℕ), (expSeries 𝕜 R n) fun x_1 => x.fst)