Theorem: ExponentialModule.coe_add (DividedPowers/ExponentialModule/Basic.lean)

State before:
A✝ : Type u_1
R✝ : Type u_2
inst✝⁵ : CommRing A✝
inst✝⁴ : CommRing R✝
inst✝³ : Algebra A✝ R✝
A : Type u_3
R : Type u_4
inst✝² : CommRing A
inst✝¹ : CommRing R
inst✝ : Algebra A R
f g : ↥(ExponentialModule R)
⊢ ↑(f + g) = ↑f * ↑g
Tactic:
simp only [toPowerSeries, AddSubmonoid.coe_add, toMul_add]
State after:
no goals