α : Type u_1
β : Type ?u.7133
r s : Setoid α
⊢ r ⊔ s = sInf {s_1 | ∀ ⦃x y : α⦄, Rel r x y ∨ Rel s x y → Rel s_1 x y}
α : Type u_1
β : Type ?u.7133
r s : Setoid α
⊢ r ⊔ s = EqvGen.Setoid fun x y => Rel r x y ∨ Rel s x y
rw [eqvGen_eq]
α : Type u_1
β : Type ?u.7133
r s : Setoid α
⊢ {x | r ≤ x ∧ s ≤ x} = {s_1 | ∀ ⦃x y : α⦄, Rel r x y ∨ Rel s x y → Rel s_1 x y}
α : Type u_1
β : Type ?u.7133
r s : Setoid α
⊢ r ⊔ s = sInf {s_1 | ∀ ⦃x y : α⦄, Rel r x y ∨ Rel s x y → Rel s_1 x y}
apply congr_arg sInf
no goals
α : Type u_1
β : Type ?u.7133
r s : Setoid α
⊢ {x | r ≤ x ∧ s ≤ x} = {s_1 | ∀ ⦃x y : α⦄, Rel r x y ∨ Rel s x y → Rel s_1 x y}
simp only [le_def, or_imp, ← forall_and]