R : Type ?u.355190
R₁ : Type ?u.355193
R₂ : Type ?u.355196
R₃ : Type ?u.355199
k : Type ?u.355202
S : Type ?u.355205
S₃ : Type ?u.355208
T : Type ?u.355211
M : Type u_1
M₁ : Type ?u.355217
M₂ : Type u_2
M₃ : Type ?u.355223
N₁ : Type ?u.355226
N₂ : Type ?u.355229
N₃ : Type ?u.355232
ι : Type ?u.355235
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
f g : M →+ M₂
h : toIntLinearMap f = toIntLinearMap g
⊢ f = g
R : Type ?u.355190
R₁ : Type ?u.355193
R₂ : Type ?u.355196
R₃ : Type ?u.355199
k : Type ?u.355202
S : Type ?u.355205
S₃ : Type ?u.355208
T : Type ?u.355211
M : Type u_1
M₁ : Type ?u.355217
M₂ : Type u_2
M₃ : Type ?u.355223
N₁ : Type ?u.355226
N₂ : Type ?u.355229
N₃ : Type ?u.355232
ι : Type ?u.355235
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
⊢ Injective toIntLinearMap
intro f g h
case h
R : Type ?u.355190
R₁ : Type ?u.355193
R₂ : Type ?u.355196
R₃ : Type ?u.355199
k : Type ?u.355202
S : Type ?u.355205
S₃ : Type ?u.355208
T : Type ?u.355211
M : Type u_1
M₁ : Type ?u.355217
M₂ : Type u_2
M₃ : Type ?u.355223
N₁ : Type ?u.355226
N₂ : Type ?u.355229
N₃ : Type ?u.355232
ι : Type ?u.355235
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
f g : M →+ M₂
h : toIntLinearMap f = toIntLinearMap g
x : M
⊢ ↑f x = ↑g x
R : Type ?u.355190
R₁ : Type ?u.355193
R₂ : Type ?u.355196
R₃ : Type ?u.355199
k : Type ?u.355202
S : Type ?u.355205
S₃ : Type ?u.355208
T : Type ?u.355211
M : Type u_1
M₁ : Type ?u.355217
M₂ : Type u_2
M₃ : Type ?u.355223
N₁ : Type ?u.355226
N₂ : Type ?u.355229
N₃ : Type ?u.355232
ι : Type ?u.355235
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
f g : M →+ M₂
h : toIntLinearMap f = toIntLinearMap g
⊢ f = g
ext x
no goals
case h
R : Type ?u.355190
R₁ : Type ?u.355193
R₂ : Type ?u.355196
R₃ : Type ?u.355199
k : Type ?u.355202
S : Type ?u.355205
S₃ : Type ?u.355208
T : Type ?u.355211
M : Type u_1
M₁ : Type ?u.355217
M₂ : Type u_2
M₃ : Type ?u.355223
N₁ : Type ?u.355226
N₂ : Type ?u.355229
N₃ : Type ?u.355232
ι : Type ?u.355235
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
f g : M →+ M₂
h : toIntLinearMap f = toIntLinearMap g
x : M
⊢ ↑f x = ↑g x
exact LinearMap.congr_fun h x