case mp
α : Type u_1
β : Type ?u.5561
γ : Type ?u.5564
ι : Type u_2
ι' : Type ?u.5570
r p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
inst✝ : IsEquiv α r
s : Set ι
hs : Set.Nonempty s
⊢ Set.Pairwise s (r on f) → ∃ z, ∀ (x : ι), x ∈ s → r (f x) z

case mpr
α : Type u_1
β : Type ?u.5561
γ : Type ?u.5564
ι : Type u_2
ι' : Type ?u.5570
r p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
inst✝ : IsEquiv α r
s : Set ι
hs : Set.Nonempty s
⊢ (∃ z, ∀ (x : ι), x ∈ s → r (f x) z) → Set.Pairwise s (r on f)
α : Type u_1
β : Type ?u.5561
γ : Type ?u.5564
ι : Type u_2
ι' : Type ?u.5570
r p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
inst✝ : IsEquiv α r
s : Set ι
hs : Set.Nonempty s
⊢ Set.Pairwise s (r on f) ↔ ∃ z, ∀ (x : ι), x ∈ s → r (f x) z
constructor
case mp.intro
α : Type u_1
β : Type ?u.5561
γ : Type ?u.5564
ι : Type u_2
ι' : Type ?u.5570
r p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
inst✝ : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
⊢ Set.Pairwise s (r on f) → ∃ z, ∀ (x : ι), x ∈ s → r (f x) z
case mp
α : Type u_1
β : Type ?u.5561
γ : Type ?u.5564
ι : Type u_2
ι' : Type ?u.5570
r p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
inst✝ : IsEquiv α r
s : Set ι
hs : Set.Nonempty s
⊢ Set.Pairwise s (r on f) → ∃ z, ∀ (x : ι), x ∈ s → r (f x) z
rcases hs with ⟨y, hy⟩
case mp.intro
α : Type u_1
β : Type ?u.5561
γ : Type ?u.5564
ι : Type u_2
ι' : Type ?u.5570
r p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
inst✝ : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
H : Set.Pairwise s (r on f)
x : ι
hx : x ∈ s
⊢ r (f x) (f y)
case mp.intro
α : Type u_1
β : Type ?u.5561
γ : Type ?u.5564
ι : Type u_2
ι' : Type ?u.5570
r p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
inst✝ : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
⊢ Set.Pairwise s (r on f) → ∃ z, ∀ (x : ι), x ∈ s → r (f x) z
refine' fun H => ⟨f y, fun x hx => _⟩
case mp.intro.inl
α : Type u_1
β : Type ?u.5561
γ : Type ?u.5564
ι : Type u_2
ι' : Type ?u.5570
r p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
inst✝ : IsEquiv α r
s : Set ι
H : Set.Pairwise s (r on f)
x : ι
hx hy : x ∈ s
⊢ r (f x) (f x)

case mp.intro.inr
α : Type u_1
β : Type ?u.5561
γ : Type ?u.5564
ι : Type u_2
ι' : Type ?u.5570
r p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
inst✝ : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
H : Set.Pairwise s (r on f)
x : ι
hx : x ∈ s
hne : x ≠ y
⊢ r (f x) (f y)
case mp.intro
α : Type u_1
β : Type ?u.5561
γ : Type ?u.5564
ι : Type u_2
ι' : Type ?u.5570
r p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
inst✝ : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
H : Set.Pairwise s (r on f)
x : ι
hx : x ∈ s
⊢ r (f x) (f y)
rcases eq_or_ne x y with (rfl | hne)
no goals
case mp.intro.inl
α : Type u_1
β : Type ?u.5561
γ : Type ?u.5564
ι : Type u_2
ι' : Type ?u.5570
r p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
inst✝ : IsEquiv α r
s : Set ι
H : Set.Pairwise s (r on f)
x : ι
hx hy : x ∈ s
⊢ r (f x) (f x)
apply IsRefl.refl
no goals
case mp.intro.inr
α : Type u_1
β : Type ?u.5561
γ : Type ?u.5564
ι : Type u_2
ι' : Type ?u.5570
r p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
inst✝ : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
H : Set.Pairwise s (r on f)
x : ι
hx : x ∈ s
hne : x ≠ y
⊢ r (f x) (f y)
exact H hx hy hne
case mpr.intro
α : Type u_1
β : Type ?u.5561
γ : Type ?u.5564
ι : Type u_2
ι' : Type ?u.5570
r p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
inst✝ : IsEquiv α r
s : Set ι
hs : Set.Nonempty s
z : α
hz : ∀ (x : ι), x ∈ s → r (f x) z
x : ι
hx : x ∈ s
y : ι
hy : y ∈ s
a✝ : x ≠ y
⊢ (r on f) x y
case mpr
α : Type u_1
β : Type ?u.5561
γ : Type ?u.5564
ι : Type u_2
ι' : Type ?u.5570
r p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
inst✝ : IsEquiv α r
s : Set ι
hs : Set.Nonempty s
⊢ (∃ z, ∀ (x : ι), x ∈ s → r (f x) z) → Set.Pairwise s (r on f)
rintro ⟨z, hz⟩ x hx y hy _
no goals
case mpr.intro
α : Type u_1
β : Type ?u.5561
γ : Type ?u.5564
ι : Type u_2
ι' : Type ?u.5570
r p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
inst✝ : IsEquiv α r
s : Set ι
hs : Set.Nonempty s
z : α
hz : ∀ (x : ι), x ∈ s → r (f x) z
x : ι
hx : x ∈ s
y : ι
hy : y ∈ s
a✝ : x ≠ y
⊢ (r on f) x y
exact @IsTrans.trans α r _ (f x) z (f y) (hz _ hx) (IsSymm.symm _ _ <| hz _ hy)