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.477455
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
fst✝ : E
snd✝ : F
⊢ (fst✝, snd✝) ∈ graph f ↔ ∃ y, ↑y = (fst✝, snd✝).fst ∧ ↑f y = (fst✝, snd✝).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.477455
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
x : E × F
⊢ x ∈ graph f ↔ ∃ y, ↑y = x.fst ∧ ↑f y = x.snd
cases x
no goals
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.477455
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
fst✝ : E
snd✝ : F
⊢ (fst✝, snd✝) ∈ graph f ↔ ∃ y, ↑y = (fst✝, snd✝).fst ∧ ↑f y = (fst✝, snd✝).snd
simp_rw [mem_graph_iff', Prod.mk.inj_iff]