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ᵐᵒᵖ
this : Function.Injective ↑↑(opLinearEquiv R)
⊢ map (↑(opLinearEquiv R)) (map (↑(LinearEquiv.symm (opLinearEquiv R))) (M * N)) =
    map (↑(opLinearEquiv R))
      (map (↑(LinearEquiv.symm (opLinearEquiv R))) N * map (↑(LinearEquiv.symm (opLinearEquiv R))) M)
rw [← map_comp, map_op_mul, ← map_comp, ← map_comp, LinearEquiv.comp_coe,
  LinearEquiv.symm_trans_self, LinearEquiv.refl_toLinearMap, map_id, map_id, map_id]