α : Type u_1
β : Type ?u.10696
r : α → α → Prop
s : Setoid α
h : ∀ (x y : α), r x y → Rel s x y
⊢ sInf {s | ∀ ⦃x y : α⦄, r x y → Rel s x y} ≤ s
α : Type u_1
β : Type ?u.10696
r : α → α → Prop
s : Setoid α
h : ∀ (x y : α), r x y → Rel s x y
⊢ EqvGen.Setoid r ≤ s
rw [eqvGen_eq]
no goals
α : Type u_1
β : Type ?u.10696
r : α → α → Prop
s : Setoid α
h : ∀ (x y : α), r x y → Rel s x y
⊢ sInf {s | ∀ ⦃x y : α⦄, r x y → Rel s x y} ≤ s
exact sInf_le h