-- Mathlib/Data/Set/Pairwise/Basic.lean
theorem Nonempty.pairwise_iff_exists_forall [IsEquiv α r] {s : Set ι} (hs : s.Nonempty) :
    s.Pairwise (r on f) ↔ ∃ z, ∀ x ∈ s, r (f x) z

Proof state:
case mp.intro
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
H : s.Pairwise (r on f)
x : ι
hx : x ∈ s
⊢ r (f x) (f y)

Tactic:
rcases eq_or_ne x y with (rfl | hne)

Result:
case mp.intro.inl
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
H : s.Pairwise (r on f)
x : ι
hx hy : x ∈ s
⊢ r (f x) (f x)

case mp.intro.inr
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
H : s.Pairwise (r on f)
x : ι
hx : x ∈ s
hne : x ≠ y
⊢ r (f x) (f y)

Proof state:
case mp.intro.inl
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
H : s.Pairwise (r on f)
x : ι
hx hy : x ∈ s
⊢ r (f x) (f x)

Tactic:
apply IsRefl.refl

Result:
no goals

Proof state:
case mpr.intro
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
hs : s.Nonempty
z : α
hz : ∀ x ∈ s, r (f x) z
x : ι
hx : x ∈ s
y : ι
hy : y ∈ s
a✝ : x ≠ y
⊢ (r on f) x y

Tactic:
exact @IsTrans.trans α r _ (f x) z (f y) (hz _ hx) (IsSymm.symm _ _ <| hz _ hy)

Result:
no goals

Proof state:
case mp.intro.inr
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
H : s.Pairwise (r on f)
x : ι
hx : x ∈ s
hne : x ≠ y
⊢ r (f x) (f y)

Tactic:
exact H hx hy hne

Result:
no goals

Proof state:
case mpr
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
hs : s.Nonempty
⊢ (∃ z, ∀ x ∈ s, r (f x) z) → s.Pairwise (r on f)

Tactic:
rintro ⟨z, hz⟩ x hx y hy _

Result:
case mpr.intro
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
hs : s.Nonempty
z : α
hz : ∀ x ∈ s, r (f x) z
x : ι
hx : x ∈ s
y : ι
hy : y ∈ s
a✝ : x ≠ y
⊢ (r on f) x y

Proof state:
case mp.intro
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
⊢ s.Pairwise (r on f) → ∃ z, ∀ x ∈ s, r (f x) z

Tactic:
refine fun H => ⟨f y, fun x hx => ?_⟩

Result:
case mp.intro
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
H : s.Pairwise (r on f)
x : ι
hx : x ∈ s
⊢ r (f x) (f y)

Proof state:
case mp
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
hs : s.Nonempty
⊢ s.Pairwise (r on f) → ∃ z, ∀ x ∈ s, r (f x) z

Tactic:
rcases hs with ⟨y, hy⟩

Result:
case mp.intro
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
⊢ s.Pairwise (r on f) → ∃ z, ∀ x ∈ s, r (f x) z

Proof state:
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
hs : s.Nonempty
⊢ s.Pairwise (r on f) ↔ ∃ z, ∀ x ∈ s, r (f x) z

Tactic:
constructor

Result:
case mp
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
hs : s.Nonempty
⊢ s.Pairwise (r on f) → ∃ z, ∀ x ∈ s, r (f x) z

case mpr
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
hs : s.Nonempty
⊢ (∃ z, ∀ x ∈ s, r (f x) z) → s.Pairwise (r on f)