no goals
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M✝ N✝ P Q : Submodule R A
m n : A
M N : Submodule R Aᵐᵒᵖ
⊢ comap (↑(opLinearEquiv R)) (M * N) = comap (↑(opLinearEquiv R)) N * comap (↑(opLinearEquiv R)) M
simp_rw [comap_equiv_eq_map_symm, map_unop_mul]