α : Type u_1
β : Type ?u.46398
γ : Type ?u.46401
r : α → α → Prop
sym : Symmetric r
h : Irreflexive r
⊢ ∀ {z : Sym2 α}, z ∈ fromRel sym → ¬IsDiag z
α : Type u_1
β : Type ?u.46398
γ : Type ?u.46401
r : α → α → Prop
sym : Symmetric r
⊢ Irreflexive r → ∀ {z : Sym2 α}, z ∈ fromRel sym → ¬IsDiag z
intro h
case h
α : Type u_1
β : Type ?u.46398
γ : Type ?u.46401
r : α → α → Prop
sym : Symmetric r
h : Irreflexive r
⊢ ∀ (x y : α), Quotient.mk (Rel.setoid α) (x, y) ∈ fromRel sym → ¬IsDiag (Quotient.mk (Rel.setoid α) (x, y))
α : Type u_1
β : Type ?u.46398
γ : Type ?u.46401
r : α → α → Prop
sym : Symmetric r
h : Irreflexive r
⊢ ∀ {z : Sym2 α}, z ∈ fromRel sym → ¬IsDiag z
apply Sym2.ind
no goals
case h
α : Type u_1
β : Type ?u.46398
γ : Type ?u.46401
r : α → α → Prop
sym : Symmetric r
h : Irreflexive r
⊢ ∀ (x y : α), Quotient.mk (Rel.setoid α) (x, y) ∈ fromRel sym → ¬IsDiag (Quotient.mk (Rel.setoid α) (x, y))
aesop