no goals
R₁ : Type u_1
R₂ : Type ?u.669818
R₃ : Type ?u.669821
inst✝²⁰ : Semiring R₁
inst✝¹⁹ : Semiring R₂
inst✝¹⁸ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type ?u.669899
inst✝¹⁷ : TopologicalSpace M₁
inst✝¹⁶ : AddCommMonoid M₁
M'₁ : Type ?u.669908
inst✝¹⁵ : TopologicalSpace M'₁
inst✝¹⁴ : AddCommMonoid M'₁
M₂ : Type u_2
inst✝¹³ : TopologicalSpace M₂
inst✝¹² : AddCommMonoid M₂
M₃ : Type ?u.669926
inst✝¹¹ : TopologicalSpace M₃
inst✝¹⁰ : AddCommMonoid M₃
M₄ : Type ?u.669935
inst✝⁹ : TopologicalSpace M₄
inst✝⁸ : AddCommMonoid M₄
inst✝⁷ : Module R₁ M₁
inst✝⁶ : Module R₁ M'₁
inst✝⁵ : Module R₂ M₂
inst✝⁴ : Module R₃ M₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
F : Type ?u.670173
inst✝² : Module R₁ M₂
inst✝¹ : TopologicalSpace R₁
inst✝ : ContinuousSMul R₁ M₂
f f' : M₂
⊢ smulRight 1 f = smulRight 1 f' ↔ f = f'
simp only [ext_ring_iff, smulRight_apply, one_apply, one_smul]