-- Mathlib/Data/Set/Function.lean
/-- **Vertical line test** for functions.

Let `f : α → β × γ` be a function to a product. Assume that `f` is surjective on the first factor
and that the image of `f` intersects every "vertical line" `{(b, c) | c : γ}` at most once.
Then the image of `f` is the graph of some monoid homomorphism `f' : β → γ`. -/
lemma exists_range_eq_graphOn_univ {f : α → β × γ} (hf₁ : Surjective (Prod.fst ∘ f))
    (hf : ∀ g₁ g₂, (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) :
    ∃ f' : β → γ, range f = univ.graphOn f'

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
x : β × γ
⊢ (∃ y, f y = x) ↔ (f ⋯.choose).2 = x.2

Tactic:
refine ⟨?_, fun hi ↦ ⟨(hf₁ x.1).choose, Prod.ext (hf₁ x.1).choose_spec hi⟩⟩

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
x : β × γ
⊢ (∃ y, f y = x) → (f ⋯.choose).2 = x.2

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
⊢ range f = graphOn (fun h => (f ⋯.choose).2) univ

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
x : β × γ
⊢ x ∈ range f ↔ x ∈ graphOn (fun h => (f ⋯.choose).2) univ

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
x : β × γ
⊢ x ∈ range f ↔ x ∈ graphOn (fun h => (f ⋯.choose).2) univ

Tactic:
simp only [mem_range, comp_apply, mem_graphOn, mem_univ, true_and]

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
x : β × γ
⊢ (∃ y, f y = x) ↔ (f ⋯.choose).2 = x.2

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
x : β × γ
⊢ (∃ y, f y = x) → (f ⋯.choose).2 = x.2

Tactic:
rintro ⟨g, rfl⟩

Result:
case h.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
g : α
⊢ (f ⋯.choose).2 = (f g).2

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
⊢ ∃ f', range f = graphOn f' univ

Tactic:
refine ⟨fun h ↦ (f (hf₁ h).choose).snd, ?_⟩

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
⊢ range f = graphOn (fun h => (f ⋯.choose).2) univ

Proof state:
case h.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
g : α
⊢ (f ⋯.choose).2 = (f g).2

Tactic:
exact hf _ _ (hf₁ (f g).1).choose_spec

Result:
no goals