-- Mathlib/Data/Set/Function.lean
lemma exists_eq_graphOn_image_fst [Nonempty β] {s : Set (α × β)} :
    (∃ f : α → β, s = graphOn f (Prod.fst '' s)) ↔ InjOn Prod.fst s

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
f : α → β
hf : ∀ ⦃x : α × β⦄, x ∈ s → (x.1, f x.1) ∈ s
⊢ ∃ f, s = graphOn f (Prod.fst '' s)

Tactic:
use f

Result:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
f : α → β
hf : ∀ ⦃x : α × β⦄, x ∈ s → (x.1, f x.1) ∈ s
⊢ s = graphOn f (Prod.fst '' s)

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
f : α → β
hf : ∀ x ∈ Prod.fst '' s, (x, f x) ∈ s
⊢ ∃ f, s = graphOn f (Prod.fst '' s)

Tactic:
rw [forall_mem_image] at hf

Result:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
f : α → β
hf : ∀ ⦃x : α × β⦄, x ∈ s → (x.1, f x.1) ∈ s
⊢ ∃ f, s = graphOn f (Prod.fst '' s)

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
this : ∀ x ∈ Prod.fst '' s, ∃ y, (x, y) ∈ s
⊢ ∃ f, s = graphOn f (Prod.fst '' s)

Tactic:
choose! f hf using this

Result:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
f : α → β
hf : ∀ x ∈ Prod.fst '' s, (x, f x) ∈ s
⊢ ∃ f, s = graphOn f (Prod.fst '' s)

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
⊢ (∃ f, s = graphOn f (Prod.fst '' s)) → InjOn Prod.fst s

Tactic:
rintro ⟨f, hf⟩

Result:
case refine_1.intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
f : α → β
hf : s = graphOn f (Prod.fst '' s)
⊢ InjOn Prod.fst s

Proof state:
case refine_1.intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
f : α → β
hf : s = graphOn f (Prod.fst '' s)
⊢ InjOn Prod.fst (graphOn f (Prod.fst '' s))

Tactic:
exact InjOn.image_of_comp <| injOn_id _

Result:
no goals

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
⊢ ∃ f, s = graphOn f (Prod.fst '' s)

Tactic:
have : ∀ x ∈ Prod.fst '' s, ∃ y, (x, y) ∈ s := forall_mem_image.2 fun (x, y) h ↦ ⟨y, h⟩

Result:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
this : ∀ x ∈ Prod.fst '' s, ∃ y, (x, y) ∈ s
⊢ ∃ f, s = graphOn f (Prod.fst '' s)

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
f : α → β
hf : ∀ ⦃x : α × β⦄, x ∈ s → (x.1, f x.1) ∈ s
⊢ EqOn (fun x => (x.1, f x.1)) id s

Tactic:
exact fun x hx ↦ h (hf hx) hx rfl

Result:
no goals

Proof state:
case refine_1.intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
f : α → β
hf : s = graphOn f (Prod.fst '' s)
⊢ InjOn Prod.fst s

Tactic:
rw [hf]

Result:
case refine_1.intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
f : α → β
hf : s = graphOn f (Prod.fst '' s)
⊢ InjOn Prod.fst (graphOn f (Prod.fst '' s))

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
⊢ (∃ f, s = graphOn f (Prod.fst '' s)) ↔ InjOn Prod.fst s

Tactic:
refine ⟨?_, fun h ↦ ?_⟩

Result:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
⊢ (∃ f, s = graphOn f (Prod.fst '' s)) → InjOn Prod.fst s

case refine_2
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
⊢ ∃ f, s = graphOn f (Prod.fst '' s)

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
f : α → β
hf : ∀ ⦃x : α × β⦄, x ∈ s → (x.1, f x.1) ∈ s
⊢ s = graphOn f (Prod.fst '' s)

Tactic:
rw [graphOn, image_image, EqOn.image_eq_self]

Result:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
f : α → β
hf : ∀ ⦃x : α × β⦄, x ∈ s → (x.1, f x.1) ∈ s
⊢ EqOn (fun x => (x.1, f x.1)) id s