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

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