-- Mathlib/Data/Rel.lean
theorem Relation.is_graph_iff (r : Rel α β) : (∃! f, Function.graph f = r) ↔ ∀ x, ∃! y, r x y

Proof state:
case mpr
α : Type u_1
β : Type u_2
r : Rel α β
h : ∀ (x : α), ∃! y, r x y
⊢ ∃! f, (fun x y => f x = y) = r

Tactic:
choose f hf using fun x ↦ (h x).exists

Result:
case mpr
α : Type u_1
β : Type u_2
r : Rel α β
h : ∀ (x : α), ∃! y, r x y
f : α → β
hf : ∀ (x : α), r x (f x)
⊢ ∃! f, (fun x y => f x = y) = r

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
⊢ (∃! f, (fun x y => f x = y) = r) ↔ ∀ (x : α), ∃! y, r x y

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
r : Rel α β
⊢ (∃! f, (fun x y => f x = y) = r) → ∀ (x : α), ∃! y, r x y

case mpr
α : Type u_1
β : Type u_2
r : Rel α β
⊢ (∀ (x : α), ∃! y, r x y) → ∃! f, (fun x y => f x = y) = r

Proof state:
case h.left.a.h.a.mp
α : Type u_1
β : Type u_2
r : Rel α β
h : ∀ (x : α), ∃! y, r x y
f : α → β
hf : ∀ (x : α), r x (f x)
x : α
⊢ r x (f x)

Tactic:
exact hf x

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
⊢ (∃! f, Function.graph f = r) ↔ ∀ (x : α), ∃! y, r x y

Tactic:
unfold Function.graph

Result:
α : Type u_1
β : Type u_2
r : Rel α β
⊢ (∃! f, (fun x y => f x = y) = r) ↔ ∀ (x : α), ∃! y, r x y

Proof state:
case h.left.a.h.a.mp
α : Type u_1
β : Type u_2
r : Rel α β
h : ∀ (x : α), ∃! y, r x y
f : α → β
hf : ∀ (x : α), r x (f x)
x : α
x✝ : β
⊢ f x = x✝ → r x x✝

Tactic:
rintro rfl

Result:
case h.left.a.h.a.mp
α : Type u_1
β : Type u_2
r : Rel α β
h : ∀ (x : α), ∃! y, r x y
f : α → β
hf : ∀ (x : α), r x (f x)
x : α
⊢ r x (f x)

Proof state:
case h
α : Type u_1
β : Type u_2
r : Rel α β
h : ∀ (x : α), ∃! y, r x y
f : α → β
hf : ∀ (x : α), r x (f x)
⊢ (fun f => (fun x y => f x = y) = r) f ∧ ∀ (y : α → β), (fun f => (fun x y => f x = y) = r) y → y = f

Tactic:
constructor

Result:
case h.left
α : Type u_1
β : Type u_2
r : Rel α β
h : ∀ (x : α), ∃! y, r x y
f : α → β
hf : ∀ (x : α), r x (f x)
⊢ (fun f => (fun x y => f x = y) = r) f

case h.right
α : Type u_1
β : Type u_2
r : Rel α β
h : ∀ (x : α), ∃! y, r x y
f : α → β
hf : ∀ (x : α), r x (f x)
⊢ ∀ (y : α → β), (fun f => (fun x y => f x = y) = r) y → y = f

Proof state:
case mpr
α : Type u_1
β : Type u_2
r : Rel α β
h : ∀ (x : α), ∃! y, r x y
f : α → β
hf : ∀ (x : α), r x (f x)
⊢ ∃! f, (fun x y => f x = y) = r

Tactic:
use f

Result:
case h
α : Type u_1
β : Type u_2
r : Rel α β
h : ∀ (x : α), ∃! y, r x y
f : α → β
hf : ∀ (x : α), r x (f x)
⊢ (fun f => (fun x y => f x = y) = r) f ∧ ∀ (y : α → β), (fun f => (fun x y => f x = y) = r) y → y = f

Proof state:
case h.left
α : Type u_1
β : Type u_2
r : Rel α β
h : ∀ (x : α), ∃! y, r x y
f : α → β
hf : ∀ (x : α), r x (f x)
⊢ (fun f => (fun x y => f x = y) = r) f

Tactic:
ext x _

Result:
case h.left.a.h.a
α : Type u_1
β : Type u_2
r : Rel α β
h : ∀ (x : α), ∃! y, r x y
f : α → β
hf : ∀ (x : α), r x (f x)
x : α
x✝ : β
⊢ f x = x✝ ↔ r x x✝

Proof state:
case h.right
α : Type u_1
β : Type u_2
f y✝ : α → β
h : ∀ (x : α), ∃! y, (fun x y => y✝ x = y) x y
hf : ∀ (x : α), (fun x y => y✝ x = y) x (f x)
⊢ y✝ = f

Tactic:
exact funext hf

Result:
no goals

Proof state:
case h.left.a.h.a.mpr
α : Type u_1
β : Type u_2
r : Rel α β
h : ∀ (x : α), ∃! y, r x y
f : α → β
hf : ∀ (x : α), r x (f x)
x : α
x✝ : β
⊢ r x x✝ → f x = x✝

Tactic:
exact (h x).unique (hf x)

Result:
no goals

Proof state:
case h.right
α : Type u_1
β : Type u_2
r : Rel α β
h : ∀ (x : α), ∃! y, r x y
f : α → β
hf : ∀ (x : α), r x (f x)
⊢ ∀ (y : α → β), (fun f => (fun x y => f x = y) = r) y → y = f

Tactic:
rintro _ rfl

Result:
case h.right
α : Type u_1
β : Type u_2
f y✝ : α → β
h : ∀ (x : α), ∃! y, (fun x y => y✝ x = y) x y
hf : ∀ (x : α), (fun x y => y✝ x = y) x (f x)
⊢ y✝ = f

Proof state:
case h.left.a.h.a
α : Type u_1
β : Type u_2
r : Rel α β
h : ∀ (x : α), ∃! y, r x y
f : α → β
hf : ∀ (x : α), r x (f x)
x : α
x✝ : β
⊢ f x = x✝ ↔ r x x✝

Tactic:
constructor

Result:
case h.left.a.h.a.mp
α : Type u_1
β : Type u_2
r : Rel α β
h : ∀ (x : α), ∃! y, r x y
f : α → β
hf : ∀ (x : α), r x (f x)
x : α
x✝ : β
⊢ f x = x✝ → r x x✝

case h.left.a.h.a.mpr
α : Type u_1
β : Type u_2
r : Rel α β
h : ∀ (x : α), ∃! y, r x y
f : α → β
hf : ∀ (x : α), r x (f x)
x : α
x✝ : β
⊢ r x x✝ → f x = x✝

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
right✝ : ∀ (y : α → β), (fun f_1 => (fun x y => f_1 x = y) = fun x y => f x = y) y → y = f
x : α
⊢ (fun y => (fun x y => f x = y) x y) (f x) ∧ ∀ (y : β), (fun y => (fun x y => f x = y) x y) y → y = f x

Tactic:
simp only [forall_eq', and_self]

Result:
no goals

Proof state:
case mpr
α : Type u_1
β : Type u_2
r : Rel α β
⊢ (∀ (x : α), ∃! y, r x y) → ∃! f, (fun x y => f x = y) = r

Tactic:
intro h

Result:
case mpr
α : Type u_1
β : Type u_2
r : Rel α β
h : ∀ (x : α), ∃! y, r x y
⊢ ∃! f, (fun x y => f x = y) = r

Proof state:
case mp.intro.intro
α : Type u_1
β : Type u_2
f : α → β
right✝ : ∀ (y : α → β), (fun f_1 => (fun x y => f_1 x = y) = fun x y => f x = y) y → y = f
x : α
⊢ ∃! y, (fun x y => f x = y) x y

Tactic:
use f x

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
right✝ : ∀ (y : α → β), (fun f_1 => (fun x y => f_1 x = y) = fun x y => f x = y) y → y = f
x : α
⊢ (fun y => (fun x y => f x = y) x y) (f x) ∧ ∀ (y : β), (fun y => (fun x y => f x = y) x y) y → y = f x

Proof state:
case mp
α : Type u_1
β : Type u_2
r : Rel α β
⊢ (∃! f, (fun x y => f x = y) = r) → ∀ (x : α), ∃! y, r x y

Tactic:
rintro ⟨f, rfl, _⟩ x

Result:
case mp.intro.intro
α : Type u_1
β : Type u_2
f : α → β
right✝ : ∀ (y : α → β), (fun f_1 => (fun x y => f_1 x = y) = fun x y => f x = y) y → y = f
x : α
⊢ ∃! y, (fun x y => f x = y) x y