case h
R : Type ?u.382607
R₁ : Type ?u.382610
R₂ : Type ?u.382613
R₃ : Type ?u.382616
k : Type ?u.382619
S : Type ?u.382622
M : Type u_1
M₁ : Type ?u.382628
M₂ : Type u_2
M₃ : Type ?u.382634
N₁ : Type ?u.382637
N₂ : Type ?u.382640
N₃ : Type ?u.382643
N₄ : Type ?u.382646
ι : Type ?u.382649
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M
inst✝ : Module R M₂
e : M ≃+ M₂
x✝ : M
⊢ ↑↑(toNatLinearEquiv e) x✝ = ↑e x✝
R : Type ?u.382607
R₁ : Type ?u.382610
R₂ : Type ?u.382613
R₃ : Type ?u.382616
k : Type ?u.382619
S : Type ?u.382622
M : Type u_1
M₁ : Type ?u.382628
M₂ : Type u_2
M₃ : Type ?u.382634
N₁ : Type ?u.382637
N₂ : Type ?u.382640
N₃ : Type ?u.382643
N₄ : Type ?u.382646
ι : Type ?u.382649
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M
inst✝ : Module R M₂
e : M ≃+ M₂
⊢ ↑(toNatLinearEquiv e) = e
ext
no goals
case h
R : Type ?u.382607
R₁ : Type ?u.382610
R₂ : Type ?u.382613
R₃ : Type ?u.382616
k : Type ?u.382619
S : Type ?u.382622
M : Type u_1
M₁ : Type ?u.382628
M₂ : Type u_2
M₃ : Type ?u.382634
N₁ : Type ?u.382637
N₂ : Type ?u.382640
N₃ : Type ?u.382643
N₄ : Type ?u.382646
ι : Type ?u.382649
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M
inst✝ : Module R M₂
e : M ≃+ M₂
x✝ : M
⊢ ↑↑(toNatLinearEquiv e) x✝ = ↑e x✝
rfl