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
⊢ map (↑(LinearEquiv.symm (opLinearEquiv R))) 1 = 1
rw [← comap_equiv_eq_map_symm, comap_op_one]