case h
R₁ : Type u_1
R₂ : Type ?u.674518
R₃ : Type ?u.674521
inst✝²¹ : Semiring R₁
inst✝²⁰ : Semiring R₂
inst✝¹⁹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type ?u.674599
inst✝¹⁸ : TopologicalSpace M₁
inst✝¹⁷ : AddCommMonoid M₁
M'₁ : Type ?u.674608
inst✝¹⁶ : TopologicalSpace M'₁
inst✝¹⁵ : AddCommMonoid M'₁
M₂ : Type u_2
inst✝¹⁴ : TopologicalSpace M₂
inst✝¹³ : AddCommMonoid M₂
M₃ : Type ?u.674626
inst✝¹² : TopologicalSpace M₃
inst✝¹¹ : AddCommMonoid M₃
M₄ : Type ?u.674635
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.674873
inst✝³ : Module R₁ M₂
inst✝² : TopologicalSpace R₁
inst✝¹ : ContinuousSMul R₁ M₂
inst✝ : ContinuousMul R₁
x : M₂
c : R₁
⊢ ↑(comp (smulRight 1 x) (smulRight 1 c)) 1 = ↑(smulRight 1 (c • x)) 1
R₁ : Type u_1
R₂ : Type ?u.674518
R₃ : Type ?u.674521
inst✝²¹ : Semiring R₁
inst✝²⁰ : Semiring R₂
inst✝¹⁹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type ?u.674599
inst✝¹⁸ : TopologicalSpace M₁
inst✝¹⁷ : AddCommMonoid M₁
M'₁ : Type ?u.674608
inst✝¹⁶ : TopologicalSpace M'₁
inst✝¹⁵ : AddCommMonoid M'₁
M₂ : Type u_2
inst✝¹⁴ : TopologicalSpace M₂
inst✝¹³ : AddCommMonoid M₂
M₃ : Type ?u.674626
inst✝¹² : TopologicalSpace M₃
inst✝¹¹ : AddCommMonoid M₃
M₄ : Type ?u.674635
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.674873
inst✝³ : Module R₁ M₂
inst✝² : TopologicalSpace R₁
inst✝¹ : ContinuousSMul R₁ M₂
inst✝ : ContinuousMul R₁
x : M₂
c : R₁
⊢ comp (smulRight 1 x) (smulRight 1 c) = smulRight 1 (c • x)
ext
no goals
case h
R₁ : Type u_1
R₂ : Type ?u.674518
R₃ : Type ?u.674521
inst✝²¹ : Semiring R₁
inst✝²⁰ : Semiring R₂
inst✝¹⁹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type ?u.674599
inst✝¹⁸ : TopologicalSpace M₁
inst✝¹⁷ : AddCommMonoid M₁
M'₁ : Type ?u.674608
inst✝¹⁶ : TopologicalSpace M'₁
inst✝¹⁵ : AddCommMonoid M'₁
M₂ : Type u_2
inst✝¹⁴ : TopologicalSpace M₂
inst✝¹³ : AddCommMonoid M₂
M₃ : Type ?u.674626
inst✝¹² : TopologicalSpace M₃
inst✝¹¹ : AddCommMonoid M₃
M₄ : Type ?u.674635
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.674873
inst✝³ : Module R₁ M₂
inst✝² : TopologicalSpace R₁
inst✝¹ : ContinuousSMul R₁ M₂
inst✝ : ContinuousMul R₁
x : M₂
c : R₁
⊢ ↑(comp (smulRight 1 x) (smulRight 1 c)) 1 = ↑(smulRight 1 (c • x)) 1
simp [mul_smul]