R : Type ?u.349302
R₁ : Type ?u.349305
R₂ : Type ?u.349308
R₃ : Type ?u.349311
k : Type ?u.349314
S : Type ?u.349317
S₃ : Type ?u.349320
T : Type ?u.349323
M : Type u_1
M₁ : Type ?u.349329
M₂ : Type u_2
M₃ : Type ?u.349335
N₁ : Type ?u.349338
N₂ : Type ?u.349341
N₃ : Type ?u.349344
ι : Type ?u.349347
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
f g : M →+ M₂
h : toNatLinearMap f = toNatLinearMap g
⊢ f = g
R : Type ?u.349302
R₁ : Type ?u.349305
R₂ : Type ?u.349308
R₃ : Type ?u.349311
k : Type ?u.349314
S : Type ?u.349317
S₃ : Type ?u.349320
T : Type ?u.349323
M : Type u_1
M₁ : Type ?u.349329
M₂ : Type u_2
M₃ : Type ?u.349335
N₁ : Type ?u.349338
N₂ : Type ?u.349341
N₃ : Type ?u.349344
ι : Type ?u.349347
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
⊢ Injective toNatLinearMap
intro f g h
case h
R : Type ?u.349302
R₁ : Type ?u.349305
R₂ : Type ?u.349308
R₃ : Type ?u.349311
k : Type ?u.349314
S : Type ?u.349317
S₃ : Type ?u.349320
T : Type ?u.349323
M : Type u_1
M₁ : Type ?u.349329
M₂ : Type u_2
M₃ : Type ?u.349335
N₁ : Type ?u.349338
N₂ : Type ?u.349341
N₃ : Type ?u.349344
ι : Type ?u.349347
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
f g : M →+ M₂
h : toNatLinearMap f = toNatLinearMap g
x : M
⊢ ↑f x = ↑g x
R : Type ?u.349302
R₁ : Type ?u.349305
R₂ : Type ?u.349308
R₃ : Type ?u.349311
k : Type ?u.349314
S : Type ?u.349317
S₃ : Type ?u.349320
T : Type ?u.349323
M : Type u_1
M₁ : Type ?u.349329
M₂ : Type u_2
M₃ : Type ?u.349335
N₁ : Type ?u.349338
N₂ : Type ?u.349341
N₃ : Type ?u.349344
ι : Type ?u.349347
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
f g : M →+ M₂
h : toNatLinearMap f = toNatLinearMap g
⊢ f = g
ext x
no goals
case h
R : Type ?u.349302
R₁ : Type ?u.349305
R₂ : Type ?u.349308
R₃ : Type ?u.349311
k : Type ?u.349314
S : Type ?u.349317
S₃ : Type ?u.349320
T : Type ?u.349323
M : Type u_1
M₁ : Type ?u.349329
M₂ : Type u_2
M₃ : Type ?u.349335
N₁ : Type ?u.349338
N₂ : Type ?u.349341
N₃ : Type ?u.349344
ι : Type ?u.349347
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
f g : M →+ M₂
h : toNatLinearMap f = toNatLinearMap g
x : M
⊢ ↑f x = ↑g x
exact LinearMap.congr_fun h x