case mk
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.558597
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.559113
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
y : E × F
hy : y ∈ graph f
fst✝ : E
snd✝ : F
hx : (fst✝, snd✝) ∈ graph f
hxy : (fst✝, snd✝).fst = y.fst
⊢ (fst✝, snd✝).snd = y.snd
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.558597
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.559113
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
x y : E × F
hx : x ∈ graph f
hy : y ∈ graph f
hxy : x.fst = y.fst
⊢ x.snd = y.snd
cases x
case mk.mk
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.558597
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.559113
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y : M
f : E →ₗ.[R] F
fst✝¹ : E
snd✝¹ : F
hx : (fst✝¹, snd✝¹) ∈ graph f
fst✝ : E
snd✝ : F
hy : (fst✝, snd✝) ∈ graph f
hxy : (fst✝¹, snd✝¹).fst = (fst✝, snd✝).fst
⊢ (fst✝¹, snd✝¹).snd = (fst✝, snd✝).snd
case mk
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.558597
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.559113
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
y : E × F
hy : y ∈ graph f
fst✝ : E
snd✝ : F
hx : (fst✝, snd✝) ∈ graph f
hxy : (fst✝, snd✝).fst = y.fst
⊢ (fst✝, snd✝).snd = y.snd
cases y
no goals
case mk.mk
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.558597
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.559113
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y : M
f : E →ₗ.[R] F
fst✝¹ : E
snd✝¹ : F
hx : (fst✝¹, snd✝¹) ∈ graph f
fst✝ : E
snd✝ : F
hy : (fst✝, snd✝) ∈ graph f
hxy : (fst✝¹, snd✝¹).fst = (fst✝, snd✝).fst
⊢ (fst✝¹, snd✝¹).snd = (fst✝, snd✝).snd
exact f.mem_graph_snd_inj hx hy hxy