case mk
R : Type u_1
R₁ : Type ?u.2231117
R₂ : Type ?u.2231120
R₃ : Type ?u.2231123
R₄ : Type ?u.2231126
S : Type ?u.2231129
K : Type ?u.2231132
K₂ : Type ?u.2231135
M : Type u_2
M' : Type ?u.2231141
M₁ : Type ?u.2231144
M₂ : Type ?u.2231147
M₃ : Type ?u.2231150
M₄ : Type ?u.2231153
N : Type ?u.2231156
N₂ : Type ?u.2231159
ι : Type ?u.2231162
V : Type ?u.2231165
V₂ : Type ?u.2231168
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
q : Submodule R { x // x ∈ p }
val✝ : M
property✝ : val✝ ∈ map (Submodule.subtype p) q
⊢ ↑↑(↑(LinearEquiv.symm (equivSubtypeMap p q)) { val := val✝, property := property✝ }) =
    ↑{ val := val✝, property := property✝ }
R : Type u_1
R₁ : Type ?u.2231117
R₂ : Type ?u.2231120
R₃ : Type ?u.2231123
R₄ : Type ?u.2231126
S : Type ?u.2231129
K : Type ?u.2231132
K₂ : Type ?u.2231135
M : Type u_2
M' : Type ?u.2231141
M₁ : Type ?u.2231144
M₂ : Type ?u.2231147
M₃ : Type ?u.2231150
M₄ : Type ?u.2231153
N : Type ?u.2231156
N₂ : Type ?u.2231159
ι : Type ?u.2231162
V : Type ?u.2231165
V₂ : Type ?u.2231168
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
q : Submodule R { x // x ∈ p }
x : { x // x ∈ map (Submodule.subtype p) q }
⊢ ↑↑(↑(LinearEquiv.symm (equivSubtypeMap p q)) x) = ↑x
cases x
no goals
case mk
R : Type u_1
R₁ : Type ?u.2231117
R₂ : Type ?u.2231120
R₃ : Type ?u.2231123
R₄ : Type ?u.2231126
S : Type ?u.2231129
K : Type ?u.2231132
K₂ : Type ?u.2231135
M : Type u_2
M' : Type ?u.2231141
M₁ : Type ?u.2231144
M₂ : Type ?u.2231147
M₃ : Type ?u.2231150
M₄ : Type ?u.2231153
N : Type ?u.2231156
N₂ : Type ?u.2231159
ι : Type ?u.2231162
V : Type ?u.2231165
V₂ : Type ?u.2231168
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
q : Submodule R { x // x ∈ p }
val✝ : M
property✝ : val✝ ∈ map (Submodule.subtype p) q
⊢ ↑↑(↑(LinearEquiv.symm (equivSubtypeMap p q)) { val := val✝, property := property✝ }) =
    ↑{ val := val✝, property := property✝ }
rfl