case mk
α : Type u_1
β : Type ?u.1790
γ : Type ?u.1793
ι : Type ?u.1796
M : Type u_2
M' : Type ?u.1802
N : Type ?u.1805
P : Type ?u.1808
G : Type ?u.1811
H : Type ?u.1814
R : Type ?u.1817
S : Type ?u.1820
inst✝ : Zero M
f : α →₀ M
fst✝ : α
snd✝ : M
⊢ (fst✝, snd✝) ∈ graph f ↔ ↑f (fst✝, snd✝).fst = (fst✝, snd✝).snd ∧ (fst✝, snd✝).snd ≠ 0
α : Type u_1
β : Type ?u.1790
γ : Type ?u.1793
ι : Type ?u.1796
M : Type u_2
M' : Type ?u.1802
N : Type ?u.1805
P : Type ?u.1808
G : Type ?u.1811
H : Type ?u.1814
R : Type ?u.1817
S : Type ?u.1820
inst✝ : Zero M
c : α × M
f : α →₀ M
⊢ c ∈ graph f ↔ ↑f c.fst = c.snd ∧ c.snd ≠ 0
cases c
no goals
case mk
α : Type u_1
β : Type ?u.1790
γ : Type ?u.1793
ι : Type ?u.1796
M : Type u_2
M' : Type ?u.1802
N : Type ?u.1805
P : Type ?u.1808
G : Type ?u.1811
H : Type ?u.1814
R : Type ?u.1817
S : Type ?u.1820
inst✝ : Zero M
f : α →₀ M
fst✝ : α
snd✝ : M
⊢ (fst✝, snd✝) ∈ graph f ↔ ↑f (fst✝, snd✝).fst = (fst✝, snd✝).snd ∧ (fst✝, snd✝).snd ≠ 0
exact mk_mem_graph_iff