case inl
α : Type u_2
β : Type ?u.6322
γ : Type ?u.6325
ι : Type u_1
ι' : Type ?u.6331
r✝ p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
inst✝¹ : Nonempty ι
f : α → ι
r : ι → ι → Prop
inst✝ : IsEquiv ι r
⊢ Set.Pairwise ∅ (r on f) ↔ ∃ z, ∀ (x : α), x ∈ ∅ → r (f x) z

case inr
α : Type u_2
β : Type ?u.6322
γ : Type ?u.6325
ι : Type u_1
ι' : Type ?u.6331
r✝ p q : α → α → Prop
f✝ g : ι → α
s✝ t u : Set α
a b : α
inst✝¹ : Nonempty ι
s : Set α
f : α → ι
r : ι → ι → Prop
inst✝ : IsEquiv ι r
hne : Set.Nonempty s
⊢ Set.Pairwise s (r on f) ↔ ∃ z, ∀ (x : α), x ∈ s → r (f x) z
α : Type u_2
β : Type ?u.6322
γ : Type ?u.6325
ι : Type u_1
ι' : Type ?u.6331
r✝ p q : α → α → Prop
f✝ g : ι → α
s✝ t u : Set α
a b : α
inst✝¹ : Nonempty ι
s : Set α
f : α → ι
r : ι → ι → Prop
inst✝ : IsEquiv ι r
⊢ Set.Pairwise s (r on f) ↔ ∃ z, ∀ (x : α), x ∈ s → r (f x) z
rcases s.eq_empty_or_nonempty with (rfl | hne)
no goals
case inl
α : Type u_2
β : Type ?u.6322
γ : Type ?u.6325
ι : Type u_1
ι' : Type ?u.6331
r✝ p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
inst✝¹ : Nonempty ι
f : α → ι
r : ι → ι → Prop
inst✝ : IsEquiv ι r
⊢ Set.Pairwise ∅ (r on f) ↔ ∃ z, ∀ (x : α), x ∈ ∅ → r (f x) z
simp
no goals
case inr
α : Type u_2
β : Type ?u.6322
γ : Type ?u.6325
ι : Type u_1
ι' : Type ?u.6331
r✝ p q : α → α → Prop
f✝ g : ι → α
s✝ t u : Set α
a b : α
inst✝¹ : Nonempty ι
s : Set α
f : α → ι
r : ι → ι → Prop
inst✝ : IsEquiv ι r
hne : Set.Nonempty s
⊢ Set.Pairwise s (r on f) ↔ ∃ z, ∀ (x : α), x ∈ s → r (f x) z
exact hne.pairwise_iff_exists_forall