α : Type u_1
β : Type ?u.44384
γ : Type ?u.44387
r : α → α → Prop
⊢ ∀ (e : Sym2 α), e ∈ fromRel (_ : ∀ (x y : α), ⊤ x y → ⊤ x y)
α : Type u_1
β : Type ?u.44384
γ : Type ?u.44387
r : α → α → Prop
⊢ fromRel (_ : ∀ (x y : α), ⊤ x y → ⊤ x y) = Set.univ
apply Set.eq_univ_of_forall fun e => _
case h
α : Type u_1
β : Type ?u.44384
γ : Type ?u.44387
r : α → α → Prop
⊢ ∀ (x y : α), Quotient.mk (Rel.setoid α) (x, y) ∈ fromRel (_ : ∀ (x y : α), ⊤ x y → ⊤ x y)
α : Type u_1
β : Type ?u.44384
γ : Type ?u.44387
r : α → α → Prop
⊢ ∀ (e : Sym2 α), e ∈ fromRel (_ : ∀ (x y : α), ⊤ x y → ⊤ x y)
apply Sym2.ind
no goals
case h
α : Type u_1
β : Type ?u.44384
γ : Type ?u.44387
r : α → α → Prop
⊢ ∀ (x y : α), Quotient.mk (Rel.setoid α) (x, y) ∈ fromRel (_ : ∀ (x y : α), ⊤ x y → ⊤ x y)
simp [-Set.top_eq_univ, Prop.top_eq_true]