Theorem: ExponentialModule.coe_injective (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, EmbeddingLike.apply_eq_iff_eq, SetLike.coe_eq_coe, imp_self]
State after:
no goals