case a
R : Type u_1
R₁ : Type ?u.321615
R₂ : Type ?u.321618
R₃ : Type ?u.321621
k : Type ?u.321624
S : Type ?u.321627
S₃ : Type ?u.321630
T : Type ?u.321633
M : Type u_2
M₁ : Type ?u.321639
M₂ : Type u_3
M₃ : Type ?u.321645
N₁ : Type ?u.321648
N₂ : Type ?u.321651
N₃ : Type ?u.321654
ι : Type ?u.321657
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f g : M →+[R] M₂
h : ↑f = ↑g
m : M
⊢ ↑f m = ↑g m
R : Type u_1
R₁ : Type ?u.321615
R₂ : Type ?u.321618
R₃ : Type ?u.321621
k : Type ?u.321624
S : Type ?u.321627
S₃ : Type ?u.321630
T : Type ?u.321633
M : Type u_2
M₁ : Type ?u.321639
M₂ : Type u_3
M₃ : Type ?u.321645
N₁ : Type ?u.321648
N₂ : Type ?u.321651
N₃ : Type ?u.321654
ι : Type ?u.321657
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f g : M →+[R] M₂
h : ↑f = ↑g
⊢ f = g
ext m
no goals
case a
R : Type u_1
R₁ : Type ?u.321615
R₂ : Type ?u.321618
R₃ : Type ?u.321621
k : Type ?u.321624
S : Type ?u.321627
S₃ : Type ?u.321630
T : Type ?u.321633
M : Type u_2
M₁ : Type ?u.321639
M₂ : Type u_3
M₃ : Type ?u.321645
N₁ : Type ?u.321648
N₂ : Type ?u.321651
N₃ : Type ?u.321654
ι : Type ?u.321657
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f g : M →+[R] M₂
h : ↑f = ↑g
m : M
⊢ ↑f m = ↑g m
exact LinearMap.congr_fun h m