Theorem: Function.Graph₂.iff_right (Arithmetization/Vorspiel/Graph.lean)

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