-- Mathlib/Data/Set/Function.lean
/-- **Line test** for equivalences.

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

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

Tactic:
obtain ⟨e₁, he₁⟩ := exists_range_eq_graphOn_univ hf₁ fun _ _ ↦ (hf _ _).1

Result:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
⊢ ∃ e, range f = graphOn (⇑e) univ

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range (⇑(prodComm β γ) ∘ f) = graphOn e₂ univ
he₁₂ : ∀ (h : β) (i : γ), e₁ h = i ↔ e₂ i = h
⊢ ∃ e, range f = graphOn (⇑e) univ

Tactic:
exact ⟨
{ toFun := e₁
  invFun := e₂
  left_inv := fun h ↦ by rw [← he₁₂]
  right_inv := fun i ↦ by rw [he₁₂] }, he₁⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : ∀ (x : β × γ), x ∈ range f ↔ x ∈ graphOn e₁ univ
e₂ : γ → β
he₂ : ∀ (x : γ × β), x ∈ range (⇑(prodComm β γ) ∘ f) ↔ x ∈ graphOn e₂ univ
h : β
i : γ
⊢ e₁ h = i ↔ e₂ i = h

Tactic:
aesop (add simp [Prod.swap_eq_iff_eq_swap])

Result:
no goals

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

Tactic:
simp [hf]

Result:
no goals

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

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range (⇑(prodComm β γ) ∘ f) = graphOn e₂ univ
he₁₂ : ∀ (h : β) (i : γ), e₁ h = i ↔ e₂ i = h
i : γ
⊢ e₁ (e₂ i) = i

Tactic:
rw [he₁₂]

Result:
no goals

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

Tactic:
obtain ⟨e₂, he₂⟩ := exists_range_eq_graphOn_univ (f := Equiv.prodComm _ _ ∘ f) (by simpa) <|
  by simp [hf]

Result:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range (⇑(prodComm β γ) ∘ f) = graphOn e₂ univ
⊢ ∃ e, range f = graphOn (⇑e) univ

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range (⇑(prodComm β γ) ∘ f) = graphOn e₂ univ
he₁₂ : ∀ (h : β) (i : γ), e₁ h = i ↔ e₂ i = h
h : β
⊢ e₂ (e₁ h) = h

Tactic:
rw [← he₁₂]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range (⇑(prodComm β γ) ∘ f) = graphOn e₂ univ
h : β
i : γ
⊢ e₁ h = i ↔ e₂ i = h

Tactic:
rw [Set.ext_iff] at he₁ he₂

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : ∀ (x : β × γ), x ∈ range f ↔ x ∈ graphOn e₁ univ
e₂ : γ → β
he₂ : ∀ (x : γ × β), x ∈ range (⇑(prodComm β γ) ∘ f) ↔ x ∈ graphOn e₂ univ
h : β
i : γ
⊢ e₁ h = i ↔ e₂ i = h

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range (⇑(prodComm β γ) ∘ f) = graphOn e₂ univ
⊢ ∃ e, range f = graphOn (⇑e) univ

Tactic:
have he₁₂ h i : e₁ h = i ↔ e₂ i = h := by
  rw [Set.ext_iff] at he₁ he₂
  aesop (add simp [Prod.swap_eq_iff_eq_swap])

Result:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range (⇑(prodComm β γ) ∘ f) = graphOn e₂ univ
he₁₂ : ∀ (h : β) (i : γ), e₁ h = i ↔ e₂ i = h
⊢ ∃ e, range f = graphOn (⇑e) univ