α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
s : Set α
⊢ (∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → ∃ z, z ∈ s ∧ r x z ∧ r y z) ↔
    ∀ (a : α), a ∈ s → ∀ (a_1 : α), a_1 ∈ s → ∃ a_2, r a a_2 ∧ a_2 ∈ s ∧ r a_1 a_2
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
s : Set α
⊢ DirectedOn r s ↔ Directed r Subtype.val
simp [Directed, DirectedOn]
no goals
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
s : Set α
⊢ (∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → ∃ z, z ∈ s ∧ r x z ∧ r y z) ↔
    ∀ (a : α), a ∈ s → ∀ (a_1 : α), a_1 ∈ s → ∃ a_2, r a a_2 ∧ a_2 ∈ s ∧ r a_1 a_2
refine' ball_congr fun x _ => by simp [And.comm, and_assoc]
no goals
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
s : Set α
x : α
x✝ : x ∈ s
⊢ (∀ (y : α), y ∈ s → ∃ z, z ∈ s ∧ r x z ∧ r y z) ↔ ∀ (a : α), a ∈ s → ∃ a_1, r x a_1 ∧ a_1 ∈ s ∧ r a a_1
simp [And.comm, and_assoc]