α : Type u_1
β : Type ?u.8031
S : Set (Setoid α)
⊢ sSup S = sInf {s | ∀ ⦃x y : α⦄, (∃ r, r ∈ S ∧ Rel r x y) → Rel s x y}
α : Type u_1
β : Type ?u.8031
S : Set (Setoid α)
⊢ sSup S = EqvGen.Setoid fun x y => ∃ r, r ∈ S ∧ Rel r x y
rw [eqvGen_eq]
α : Type u_1
β : Type ?u.8031
S : Set (Setoid α)
⊢ upperBounds S = {s | ∀ ⦃x y : α⦄, (∃ r, r ∈ S ∧ Rel r x y) → Rel s x y}
α : Type u_1
β : Type ?u.8031
S : Set (Setoid α)
⊢ sSup S = sInf {s | ∀ ⦃x y : α⦄, (∃ r, r ∈ S ∧ Rel r x y) → Rel s x y}
apply congr_arg sInf
α : Type u_1
β : Type ?u.8031
S : Set (Setoid α)
⊢ {x | ∀ ⦃a : Setoid α⦄, a ∈ S → ∀ {x_1 y : α}, Rel a x_1 y → Rel x x_1 y} =
    {s | ∀ ⦃x y : α⦄ (x_1 : Setoid α), x_1 ∈ S → Rel x_1 x y → Rel s x y}
α : Type u_1
β : Type ?u.8031
S : Set (Setoid α)
⊢ upperBounds S = {s | ∀ ⦃x y : α⦄, (∃ r, r ∈ S ∧ Rel r x y) → Rel s x y}
simp only [upperBounds, le_def, and_imp, exists_imp]
case h
α : Type u_1
β : Type ?u.8031
S : Set (Setoid α)
x✝ : Setoid α
⊢ x✝ ∈ {x | ∀ ⦃a : Setoid α⦄, a ∈ S → ∀ {x_1 y : α}, Rel a x_1 y → Rel x x_1 y} ↔
    x✝ ∈ {s | ∀ ⦃x y : α⦄ (x_1 : Setoid α), x_1 ∈ S → Rel x_1 x y → Rel s x y}
α : Type u_1
β : Type ?u.8031
S : Set (Setoid α)
⊢ {x | ∀ ⦃a : Setoid α⦄, a ∈ S → ∀ {x_1 y : α}, Rel a x_1 y → Rel x x_1 y} =
    {s | ∀ ⦃x y : α⦄ (x_1 : Setoid α), x_1 ∈ S → Rel x_1 x y → Rel s x y}
ext
no goals
case h
α : Type u_1
β : Type ?u.8031
S : Set (Setoid α)
x✝ : Setoid α
⊢ x✝ ∈ {x | ∀ ⦃a : Setoid α⦄, a ∈ S → ∀ {x_1 y : α}, Rel a x_1 y → Rel x x_1 y} ↔
    x✝ ∈ {s | ∀ ⦃x y : α⦄ (x_1 : Setoid α), x_1 ∈ S → Rel x_1 x y → Rel s x y}
exact ⟨fun H x y r hr => H hr, fun H r hr x y => H r hr⟩