[GOAL]
𝕜 : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁵ : TopologicalSpace R
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : Field 𝕜
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Algebra 𝕜 R
inst✝⁹ : Module R M
inst✝⁸ : Module Rᵐᵒᵖ M
inst✝⁷ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁶ : Module 𝕜 M
inst✝⁵ : IsScalarTower 𝕜 R M
inst✝⁴ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
e : R
h : HasSum (fun n => ↑(expSeries 𝕜 R n) fun x_1 => fst x) e
⊢ HasSum (fun n => fst (↑(expSeries 𝕜 (tsze R M) n) fun x_1 => x)) e
[PROOFSTEP]
simpa [expSeries_apply_eq] using h
[GOAL]
𝕜 : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁶ : TopologicalSpace R
inst✝¹⁵ : TopologicalSpace M
inst✝¹⁴ : Field 𝕜
inst✝¹³ : CharZero 𝕜
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Algebra 𝕜 R
inst✝⁹ : Module R M
inst✝⁸ : Module Rᵐᵒᵖ M
inst✝⁷ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁶ : Module 𝕜 M
inst✝⁵ : IsScalarTower 𝕜 R M
inst✝⁴ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op (fst x) • snd x = fst x • snd x
e : R
h : HasSum (fun n => ↑(expSeries 𝕜 R n) fun x_1 => fst x) e
⊢ HasSum (fun n => snd (↑(expSeries 𝕜 (tsze R M) n) fun x_1 => x)) (e • snd x)
[PROOFSTEP]
simp_rw [expSeries_apply_eq] at *
[GOAL]
𝕜 : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁶ : TopologicalSpace R
inst✝¹⁵ : TopologicalSpace M
inst✝¹⁴ : Field 𝕜
inst✝¹³ : CharZero 𝕜
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Algebra 𝕜 R
inst✝⁹ : Module R M
inst✝⁸ : Module Rᵐᵒᵖ M
inst✝⁷ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁶ : Module 𝕜 M
inst✝⁵ : IsScalarTower 𝕜 R M
inst✝⁴ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op (fst x) • snd x = fst x • snd x
e : R
h : HasSum (fun n => (↑(Nat.factorial n))⁻¹ • fst x ^ n) e
⊢ HasSum (fun n => snd ((↑(Nat.factorial n))⁻¹ • x ^ n)) (e • snd x)
[PROOFSTEP]
conv =>
  congr
  ext n
  rw [snd_smul, snd_pow_of_smul_comm _ _ hx, nsmul_eq_smul_cast 𝕜 n, smul_smul, inv_mul_eq_div, ← inv_div, ← smul_assoc]
[GOAL]
𝕜 : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁶ : TopologicalSpace R
inst✝¹⁵ : TopologicalSpace M
inst✝¹⁴ : Field 𝕜
inst✝¹³ : CharZero 𝕜
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Algebra 𝕜 R
inst✝⁹ : Module R M
inst✝⁸ : Module Rᵐᵒᵖ M
inst✝⁷ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁶ : Module 𝕜 M
inst✝⁵ : IsScalarTower 𝕜 R M
inst✝⁴ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op (fst x) • snd x = fst x • snd x
e : R
h : HasSum (fun n => (↑(Nat.factorial n))⁻¹ • fst x ^ n) e
| HasSum (fun n => snd ((↑(Nat.factorial n))⁻¹ • x ^ n)) (e • snd x)
[PROOFSTEP]
  congr
  ext n
  rw [snd_smul, snd_pow_of_smul_comm _ _ hx, nsmul_eq_smul_cast 𝕜 n, smul_smul, inv_mul_eq_div, ← inv_div, ← smul_assoc]
[GOAL]
𝕜 : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁶ : TopologicalSpace R
inst✝¹⁵ : TopologicalSpace M
inst✝¹⁴ : Field 𝕜
inst✝¹³ : CharZero 𝕜
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Algebra 𝕜 R
inst✝⁹ : Module R M
inst✝⁸ : Module Rᵐᵒᵖ M
inst✝⁷ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁶ : Module 𝕜 M
inst✝⁵ : IsScalarTower 𝕜 R M
inst✝⁴ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op (fst x) • snd x = fst x • snd x
e : R
h : HasSum (fun n => (↑(Nat.factorial n))⁻¹ • fst x ^ n) e
| HasSum (fun n => snd ((↑(Nat.factorial n))⁻¹ • x ^ n)) (e • snd x)
[PROOFSTEP]
  congr
  ext n
  rw [snd_smul, snd_pow_of_smul_comm _ _ hx, nsmul_eq_smul_cast 𝕜 n, smul_smul, inv_mul_eq_div, ← inv_div, ← smul_assoc]
[GOAL]
𝕜 : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁶ : TopologicalSpace R
inst✝¹⁵ : TopologicalSpace M
inst✝¹⁴ : Field 𝕜
inst✝¹³ : CharZero 𝕜
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Algebra 𝕜 R
inst✝⁹ : Module R M
inst✝⁸ : Module Rᵐᵒᵖ M
inst✝⁷ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁶ : Module 𝕜 M
inst✝⁵ : IsScalarTower 𝕜 R M
inst✝⁴ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op (fst x) • snd x = fst x • snd x
e : R
h : HasSum (fun n => (↑(Nat.factorial n))⁻¹ • fst x ^ n) e
| HasSum (fun n => snd ((↑(Nat.factorial n))⁻¹ • x ^ n)) (e • snd x)
[PROOFSTEP]
congr
[GOAL]
case f
𝕜 : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁶ : TopologicalSpace R
inst✝¹⁵ : TopologicalSpace M
inst✝¹⁴ : Field 𝕜
inst✝¹³ : CharZero 𝕜
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Algebra 𝕜 R
inst✝⁹ : Module R M
inst✝⁸ : Module Rᵐᵒᵖ M
inst✝⁷ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁶ : Module 𝕜 M
inst✝⁵ : IsScalarTower 𝕜 R M
inst✝⁴ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op (fst x) • snd x = fst x • snd x
e : R
h : HasSum (fun n => (↑(Nat.factorial n))⁻¹ • fst x ^ n) e
| fun n => snd ((↑(Nat.factorial n))⁻¹ • x ^ n)
case a
𝕜 : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁶ : TopologicalSpace R
inst✝¹⁵ : TopologicalSpace M
inst✝¹⁴ : Field 𝕜
inst✝¹³ : CharZero 𝕜
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Algebra 𝕜 R
inst✝⁹ : Module R M
inst✝⁸ : Module Rᵐᵒᵖ M
inst✝⁷ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁶ : Module 𝕜 M
inst✝⁵ : IsScalarTower 𝕜 R M
inst✝⁴ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op (fst x) • snd x = fst x • snd x
e : R
h : HasSum (fun n => (↑(Nat.factorial n))⁻¹ • fst x ^ n) e
| e • snd x
[PROOFSTEP]
ext n
[GOAL]
case f.h
𝕜 : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁶ : TopologicalSpace R
inst✝¹⁵ : TopologicalSpace M
inst✝¹⁴ : Field 𝕜
inst✝¹³ : CharZero 𝕜
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Algebra 𝕜 R
inst✝⁹ : Module R M
inst✝⁸ : Module Rᵐᵒᵖ M
inst✝⁷ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁶ : Module 𝕜 M
inst✝⁵ : IsScalarTower 𝕜 R M
inst✝⁴ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op (fst x) • snd x = fst x • snd x
e : R
h : HasSum (fun n => (↑(Nat.factorial n))⁻¹ • fst x ^ n) e
n : ℕ
| snd ((↑(Nat.factorial n))⁻¹ • x ^ n)
case a
𝕜 : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁶ : TopologicalSpace R
inst✝¹⁵ : TopologicalSpace M
inst✝¹⁴ : Field 𝕜
inst✝¹³ : CharZero 𝕜
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Algebra 𝕜 R
inst✝⁹ : Module R M
inst✝⁸ : Module Rᵐᵒᵖ M
inst✝⁷ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁶ : Module 𝕜 M
inst✝⁵ : IsScalarTower 𝕜 R M
inst✝⁴ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op (fst x) • snd x = fst x • snd x
e : R
h : HasSum (fun n => (↑(Nat.factorial n))⁻¹ • fst x ^ n) e
| e • snd x
[PROOFSTEP]
rw [snd_smul, snd_pow_of_smul_comm _ _ hx, nsmul_eq_smul_cast 𝕜 n, smul_smul, inv_mul_eq_div, ← inv_div, ← smul_assoc]
[GOAL]
𝕜 : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁶ : TopologicalSpace R
inst✝¹⁵ : TopologicalSpace M
inst✝¹⁴ : Field 𝕜
inst✝¹³ : CharZero 𝕜
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Algebra 𝕜 R
inst✝⁹ : Module R M
inst✝⁸ : Module Rᵐᵒᵖ M
inst✝⁷ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁶ : Module 𝕜 M
inst✝⁵ : IsScalarTower 𝕜 R M
inst✝⁴ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op (fst x) • snd x = fst x • snd x
e : R
h : HasSum (fun n => (↑(Nat.factorial n))⁻¹ • fst x ^ n) e
⊢ HasSum (fun n => ((↑(Nat.factorial n) / ↑n)⁻¹ • fst x ^ Nat.pred n) • snd x) (e • snd x)
[PROOFSTEP]
apply HasSum.smul_const
[GOAL]
case hf
𝕜 : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁶ : TopologicalSpace R
inst✝¹⁵ : TopologicalSpace M
inst✝¹⁴ : Field 𝕜
inst✝¹³ : CharZero 𝕜
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Algebra 𝕜 R
inst✝⁹ : Module R M
inst✝⁸ : Module Rᵐᵒᵖ M
inst✝⁷ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁶ : Module 𝕜 M
inst✝⁵ : IsScalarTower 𝕜 R M
inst✝⁴ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op (fst x) • snd x = fst x • snd x
e : R
h : HasSum (fun n => (↑(Nat.factorial n))⁻¹ • fst x ^ n) e
⊢ HasSum (fun z => (↑(Nat.factorial z) / ↑z)⁻¹ • fst x ^ Nat.pred z) e
[PROOFSTEP]
rw [← hasSum_nat_add_iff' 1]
[GOAL]
case hf
𝕜 : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁶ : TopologicalSpace R
inst✝¹⁵ : TopologicalSpace M
inst✝¹⁴ : Field 𝕜
inst✝¹³ : CharZero 𝕜
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Algebra 𝕜 R
inst✝⁹ : Module R M
inst✝⁸ : Module Rᵐᵒᵖ M
inst✝⁷ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁶ : Module 𝕜 M
inst✝⁵ : IsScalarTower 𝕜 R M
inst✝⁴ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op (fst x) • snd x = fst x • snd x
e : R
h : HasSum (fun n => (↑(Nat.factorial n))⁻¹ • fst x ^ n) e
⊢ HasSum (fun n => (↑(Nat.factorial (n + 1)) / ↑(n + 1))⁻¹ • fst x ^ Nat.pred (n + 1))
    (e - Finset.sum (Finset.range 1) fun i => (↑(Nat.factorial i) / ↑i)⁻¹ • fst x ^ Nat.pred i)
[PROOFSTEP]
rw [Finset.range_one, Finset.sum_singleton, Nat.cast_zero, div_zero, inv_zero, zero_smul, sub_zero]
[GOAL]
case hf
𝕜 : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁶ : TopologicalSpace R
inst✝¹⁵ : TopologicalSpace M
inst✝¹⁴ : Field 𝕜
inst✝¹³ : CharZero 𝕜
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Algebra 𝕜 R
inst✝⁹ : Module R M
inst✝⁸ : Module Rᵐᵒᵖ M
inst✝⁷ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁶ : Module 𝕜 M
inst✝⁵ : IsScalarTower 𝕜 R M
inst✝⁴ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op (fst x) • snd x = fst x • snd x
e : R
h : HasSum (fun n => (↑(Nat.factorial n))⁻¹ • fst x ^ n) e
⊢ HasSum (fun n => (↑(Nat.factorial (n + 1)) / ↑(n + 1))⁻¹ • fst x ^ Nat.pred (n + 1)) e
[PROOFSTEP]
simp_rw [← Nat.succ_eq_add_one, Nat.pred_succ, Nat.factorial_succ, Nat.cast_mul, ← Nat.succ_eq_add_one,
  mul_div_cancel_left _ ((@Nat.cast_ne_zero 𝕜 _ _ _).mpr <| Nat.succ_ne_zero _)]
[GOAL]
case hf
𝕜 : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁶ : TopologicalSpace R
inst✝¹⁵ : TopologicalSpace M
inst✝¹⁴ : Field 𝕜
inst✝¹³ : CharZero 𝕜
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Algebra 𝕜 R
inst✝⁹ : Module R M
inst✝⁸ : Module Rᵐᵒᵖ M
inst✝⁷ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁶ : Module 𝕜 M
inst✝⁵ : IsScalarTower 𝕜 R M
inst✝⁴ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op (fst x) • snd x = fst x • snd x
e : R
h : HasSum (fun n => (↑(Nat.factorial n))⁻¹ • fst x ^ n) e
⊢ HasSum (fun n => (↑(Nat.factorial n))⁻¹ • fst x ^ n) e
[PROOFSTEP]
exact h
[GOAL]
𝕜 : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁶ : TopologicalSpace R
inst✝¹⁵ : TopologicalSpace M
inst✝¹⁴ : Field 𝕜
inst✝¹³ : CharZero 𝕜
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Algebra 𝕜 R
inst✝⁹ : Module R M
inst✝⁸ : Module Rᵐᵒᵖ M
inst✝⁷ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁶ : Module 𝕜 M
inst✝⁵ : IsScalarTower 𝕜 R M
inst✝⁴ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op (fst x) • snd x = fst x • snd x
e : R
h : HasSum (fun n => ↑(expSeries 𝕜 R n) fun x_1 => fst x) e
⊢ HasSum (fun n => ↑(expSeries 𝕜 (tsze R M) n) fun x_1 => x) (inl e + inr (e • snd x))
[PROOFSTEP]
simpa only [inl_fst_add_inr_snd_eq] using
  (hasSum_inl _ <| hasSum_fst_expSeries 𝕜 x h).add (hasSum_inr _ <| hasSum_snd_expSeries_of_smul_comm 𝕜 x hx h)
[GOAL]
𝕜 : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁷ : IsROrC 𝕜
inst✝¹⁶ : NormedRing R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : NormedAlgebra 𝕜 R
inst✝¹³ : Module R M
inst✝¹² : Module Rᵐᵒᵖ M
inst✝¹¹ : SMulCommClass R Rᵐᵒᵖ M
inst✝¹⁰ : Module 𝕜 M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalRing R
inst✝⁵ : TopologicalAddGroup M
inst✝⁴ : ContinuousSMul R M
inst✝³ : ContinuousSMul Rᵐᵒᵖ M
inst✝² : CompleteSpace R
inst✝¹ : T2Space R
inst✝ : T2Space M
x : tsze R M
hx : MulOpposite.op (fst x) • snd x = fst x • snd x
⊢ exp 𝕜 x = inl (exp 𝕜 (fst x)) + inr (exp 𝕜 (fst x) • snd x)
[PROOFSTEP]
simp_rw [exp, FormalMultilinearSeries.sum]
[GOAL]
𝕜 : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁷ : IsROrC 𝕜
inst✝¹⁶ : NormedRing R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : NormedAlgebra 𝕜 R
inst✝¹³ : Module R M
inst✝¹² : Module Rᵐᵒᵖ M
inst✝¹¹ : SMulCommClass R Rᵐᵒᵖ M
inst✝¹⁰ : Module 𝕜 M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalRing R
inst✝⁵ : TopologicalAddGroup M
inst✝⁴ : ContinuousSMul R M
inst✝³ : ContinuousSMul Rᵐᵒᵖ M
inst✝² : CompleteSpace R
inst✝¹ : T2Space R
inst✝ : T2Space M
x : tsze R M
hx : MulOpposite.op (fst x) • snd x = fst x • snd x
⊢ (∑' (n : ℕ), ↑(expSeries 𝕜 (tsze R M) n) fun x_1 => x) =
    inl (∑' (n : ℕ), ↑(expSeries 𝕜 R n) fun x_1 => fst x) +
      inr ((∑' (n : ℕ), ↑(expSeries 𝕜 R n) fun x_1 => fst x) • snd x)
[PROOFSTEP]
refine' (hasSum_expSeries_of_smul_comm 𝕜 x hx _).tsum_eq
[GOAL]
𝕜 : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁷ : IsROrC 𝕜
inst✝¹⁶ : NormedRing R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : NormedAlgebra 𝕜 R
inst✝¹³ : Module R M
inst✝¹² : Module Rᵐᵒᵖ M
inst✝¹¹ : SMulCommClass R Rᵐᵒᵖ M
inst✝¹⁰ : Module 𝕜 M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalRing R
inst✝⁵ : TopologicalAddGroup M
inst✝⁴ : ContinuousSMul R M
inst✝³ : ContinuousSMul Rᵐᵒᵖ M
inst✝² : CompleteSpace R
inst✝¹ : T2Space R
inst✝ : T2Space M
x : tsze R M
hx : MulOpposite.op (fst x) • snd x = fst x • snd x
⊢ HasSum (fun n => ↑(expSeries 𝕜 R n) fun x_1 => fst x) (∑' (n : ℕ), ↑(expSeries 𝕜 R n) fun x_1 => fst x)
[PROOFSTEP]
exact expSeries_hasSum_exp _
[GOAL]
𝕜 : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁷ : IsROrC 𝕜
inst✝¹⁶ : NormedRing R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : NormedAlgebra 𝕜 R
inst✝¹³ : Module R M
inst✝¹² : Module Rᵐᵒᵖ M
inst✝¹¹ : SMulCommClass R Rᵐᵒᵖ M
inst✝¹⁰ : Module 𝕜 M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalRing R
inst✝⁵ : TopologicalAddGroup M
inst✝⁴ : ContinuousSMul R M
inst✝³ : ContinuousSMul Rᵐᵒᵖ M
inst✝² : CompleteSpace R
inst✝¹ : T2Space R
inst✝ : T2Space M
x : R
⊢ exp 𝕜 (inl x) = inl (exp 𝕜 x)
[PROOFSTEP]
rw [exp_def_of_smul_comm, snd_inl, fst_inl, smul_zero, inr_zero, add_zero]
[GOAL]
case hx
𝕜 : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁷ : IsROrC 𝕜
inst✝¹⁶ : NormedRing R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : NormedAlgebra 𝕜 R
inst✝¹³ : Module R M
inst✝¹² : Module Rᵐᵒᵖ M
inst✝¹¹ : SMulCommClass R Rᵐᵒᵖ M
inst✝¹⁰ : Module 𝕜 M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalRing R
inst✝⁵ : TopologicalAddGroup M
inst✝⁴ : ContinuousSMul R M
inst✝³ : ContinuousSMul Rᵐᵒᵖ M
inst✝² : CompleteSpace R
inst✝¹ : T2Space R
inst✝ : T2Space M
x : R
⊢ MulOpposite.op (fst (inl x)) • snd (inl x) = fst (inl x) • snd (inl x)
[PROOFSTEP]
rw [snd_inl, fst_inl, smul_zero, smul_zero]
[GOAL]
𝕜 : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁷ : IsROrC 𝕜
inst✝¹⁶ : NormedRing R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : NormedAlgebra 𝕜 R
inst✝¹³ : Module R M
inst✝¹² : Module Rᵐᵒᵖ M
inst✝¹¹ : SMulCommClass R Rᵐᵒᵖ M
inst✝¹⁰ : Module 𝕜 M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalRing R
inst✝⁵ : TopologicalAddGroup M
inst✝⁴ : ContinuousSMul R M
inst✝³ : ContinuousSMul Rᵐᵒᵖ M
inst✝² : CompleteSpace R
inst✝¹ : T2Space R
inst✝ : T2Space M
m : M
⊢ exp 𝕜 (inr m) = 1 + inr m
[PROOFSTEP]
rw [exp_def_of_smul_comm, snd_inr, fst_inr, exp_zero, one_smul, inl_one]
[GOAL]
case hx
𝕜 : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁷ : IsROrC 𝕜
inst✝¹⁶ : NormedRing R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : NormedAlgebra 𝕜 R
inst✝¹³ : Module R M
inst✝¹² : Module Rᵐᵒᵖ M
inst✝¹¹ : SMulCommClass R Rᵐᵒᵖ M
inst✝¹⁰ : Module 𝕜 M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalRing R
inst✝⁵ : TopologicalAddGroup M
inst✝⁴ : ContinuousSMul R M
inst✝³ : ContinuousSMul Rᵐᵒᵖ M
inst✝² : CompleteSpace R
inst✝¹ : T2Space R
inst✝ : T2Space M
m : M
⊢ MulOpposite.op (fst (inr m)) • snd (inr m) = fst (inr m) • snd (inr m)
[PROOFSTEP]
rw [snd_inr, fst_inr, MulOpposite.op_zero, zero_smul, zero_smul]
[GOAL]
𝕜 : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁵ : IsROrC 𝕜
inst✝¹⁴ : NormedCommRing R
inst✝¹³ : AddCommGroup M
inst✝¹² : NormedAlgebra 𝕜 R
inst✝¹¹ : Module R M
inst✝¹⁰ : Module Rᵐᵒᵖ M
inst✝⁹ : IsCentralScalar R M
inst✝⁸ : Module 𝕜 M
inst✝⁷ : IsScalarTower 𝕜 R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalRing R
inst✝⁴ : TopologicalAddGroup M
inst✝³ : ContinuousSMul R M
inst✝² : CompleteSpace R
inst✝¹ : T2Space R
inst✝ : T2Space M
x : tsze R M
⊢ fst (exp 𝕜 x) = exp 𝕜 (fst x)
[PROOFSTEP]
rw [exp_def, fst_add, fst_inl, fst_inr, add_zero]
[GOAL]
𝕜 : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁵ : IsROrC 𝕜
inst✝¹⁴ : NormedCommRing R
inst✝¹³ : AddCommGroup M
inst✝¹² : NormedAlgebra 𝕜 R
inst✝¹¹ : Module R M
inst✝¹⁰ : Module Rᵐᵒᵖ M
inst✝⁹ : IsCentralScalar R M
inst✝⁸ : Module 𝕜 M
inst✝⁷ : IsScalarTower 𝕜 R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalRing R
inst✝⁴ : TopologicalAddGroup M
inst✝³ : ContinuousSMul R M
inst✝² : CompleteSpace R
inst✝¹ : T2Space R
inst✝ : T2Space M
x : tsze R M
⊢ snd (exp 𝕜 x) = exp 𝕜 (fst x) • snd x
[PROOFSTEP]
rw [exp_def, snd_add, snd_inl, snd_inr, zero_add]
[GOAL]
𝕜 : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁶ : IsROrC 𝕜
inst✝¹⁵ : NormedCommRing R
inst✝¹⁴ : AddCommGroup M
inst✝¹³ : NormedAlgebra 𝕜 R
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : IsCentralScalar R M
inst✝⁹ : Module 𝕜 M
inst✝⁸ : IsScalarTower 𝕜 R M
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalRing R
inst✝⁵ : TopologicalAddGroup M
inst✝⁴ : ContinuousSMul R M
inst✝³ : CompleteSpace R
inst✝² : T2Space R
inst✝¹ : T2Space M
x : tsze R M
inst✝ : Invertible (fst x)
⊢ x = fst x • exp 𝕜 (⅟(fst x) • inr (snd x))
[PROOFSTEP]
rw [← inr_smul, exp_inr, smul_add, ← inl_one, ← inl_smul, ← inr_smul, smul_eq_mul, mul_one, smul_smul, mul_invOf_self,
  one_smul, inl_fst_add_inr_snd_eq]
