no goals
R₁ : Type u_1
R₂ : Type ?u.1520303
R₃ : Type ?u.1520306
inst✝²⁵ : Semiring R₁
inst✝²⁴ : Semiring R₂
inst✝²³ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝²² : RingHomInvPair σ₁₂ σ₂₁
inst✝²¹ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝²⁰ : RingHomInvPair σ₂₃ σ₃₂
inst✝¹⁹ : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝¹⁸ : RingHomInvPair σ₁₃ σ₃₁
inst✝¹⁷ : RingHomInvPair σ₃₁ σ₁₃
inst✝¹⁶ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁵ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_2
inst✝¹⁴ : TopologicalSpace M₁
inst✝¹³ : AddCommMonoid M₁
M'₁ : Type ?u.1521160
inst✝¹² : TopologicalSpace M'₁
inst✝¹¹ : AddCommMonoid M'₁
M₂ : Type ?u.1521169
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
M₃ : Type ?u.1521178
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : AddCommMonoid M₃
M₄ : Type ?u.1521187
inst✝⁶ : TopologicalSpace M₄
inst✝⁵ : AddCommMonoid M₄
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₁ M'₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : TopologicalSpace R₁
f g : R₁ ≃L[R₁] M₁
h : ↑f 1 = ↑g 1
x : R₁
⊢ ↑f (x * 1) = ↑g (x * 1)
rw [← smul_eq_mul, map_smul, h, map_smul]