α : Type u_1
β : Type ?u.30661
γ : Type ?u.30664
δ : Type ?u.30667
r : α → α → Prop
a b : α
h✝ : Equivalence r
h : EqvGen r a b
⊢ r a b
α : Type u_1
β : Type ?u.30661
γ : Type ?u.30664
δ : Type ?u.30667
r : α → α → Prop
a b : α
h : Equivalence r
⊢ EqvGen r a b → r a b
intro h
no goals
α : Type u_1
β : Type ?u.30661
γ : Type ?u.30664
δ : Type ?u.30667
r : α → α → Prop
a b : α
h✝ : Equivalence r
h : EqvGen r a b
⊢ r a b
induction h with
| rel => assumption
| refl => exact h.1 _
| symm => apply h.symm; assumption
| trans _ _ _ _ _ hab hbc => exact h.trans hab hbc
no goals
case rel
α : Type u_1
β : Type ?u.30661
γ : Type ?u.30664
δ : Type ?u.30667
r : α → α → Prop
a b : α
h : Equivalence r
x✝ y✝ : α
a✝ : r x✝ y✝
⊢ r x✝ y✝
assumption
no goals
case refl
α : Type u_1
β : Type ?u.30661
γ : Type ?u.30664
δ : Type ?u.30667
r : α → α → Prop
a b : α
h : Equivalence r
x✝ : α
⊢ r x✝ x✝
exact h.1 _
case symm
α : Type u_1
β : Type ?u.30661
γ : Type ?u.30664
δ : Type ?u.30667
r : α → α → Prop
a b : α
h : Equivalence r
x✝ y✝ : α
a✝ : EqvGen r x✝ y✝
a_ih✝ : r x✝ y✝
⊢ r x✝ y✝
case symm
α : Type u_1
β : Type ?u.30661
γ : Type ?u.30664
δ : Type ?u.30667
r : α → α → Prop
a b : α
h : Equivalence r
x✝ y✝ : α
a✝ : EqvGen r x✝ y✝
a_ih✝ : r x✝ y✝
⊢ r y✝ x✝
apply h.symm
no goals
case symm
α : Type u_1
β : Type ?u.30661
γ : Type ?u.30664
δ : Type ?u.30667
r : α → α → Prop
a b : α
h : Equivalence r
x✝ y✝ : α
a✝ : EqvGen r x✝ y✝
a_ih✝ : r x✝ y✝
⊢ r x✝ y✝
assumption
no goals
case trans
α : Type u_1
β : Type ?u.30661
γ : Type ?u.30664
δ : Type ?u.30667
r : α → α → Prop
a b : α
h : Equivalence r
x✝ y✝ z✝ : α
a✝¹ : EqvGen r x✝ y✝
a✝ : EqvGen r y✝ z✝
hab : r x✝ y✝
hbc : r y✝ z✝
⊢ r x✝ z✝
exact h.trans hab hbc