Theorem: Function.Graph.iff_left (Arithmetization/Vorspiel/Graph.lean)

State before:
σ : Sort u_1
α : Sort u_2
β : Sort u_3
f : α → σ
y : σ
x : α
⊢ f x = y ↔ Graph f y x
Tactic:
simp [Graph, eq_comm]
State after:
no goals