no goals
α : Type u_1
β : Type ?u.31015
γ : Type ?u.31018
δ : Type ?u.31021
r✝ : α → α → Prop
a b : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
h : EqvGen r a b
⊢ EqvGen p a b
induction h with
| rel a b h => exact EqvGen.rel _ _ (hrp _ _ h)
| refl => exact EqvGen.refl _
| symm a b _ ih => exact EqvGen.symm _ _ ih
| trans a b c _ _ hab hbc => exact EqvGen.trans _ _ _ hab hbc
no goals
case rel
α : Type u_1
β : Type ?u.31015
γ : Type ?u.31018
δ : Type ?u.31021
r✝ : α → α → Prop
a✝ b✝ : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
a b : α
h : r a b
⊢ EqvGen p a b
exact EqvGen.rel _ _ (hrp _ _ h)
no goals
case refl
α : Type u_1
β : Type ?u.31015
γ : Type ?u.31018
δ : Type ?u.31021
r✝ : α → α → Prop
a b : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
x✝ : α
⊢ EqvGen p x✝ x✝
exact EqvGen.refl _
no goals
case symm
α : Type u_1
β : Type ?u.31015
γ : Type ?u.31018
δ : Type ?u.31021
r✝ : α → α → Prop
a✝¹ b✝ : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
a b : α
a✝ : EqvGen r a b
ih : EqvGen p a b
⊢ EqvGen p b a
exact EqvGen.symm _ _ ih
no goals
case trans
α : Type u_1
β : Type ?u.31015
γ : Type ?u.31018
δ : Type ?u.31021
r✝ : α → α → Prop
a✝² b✝ : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
a b c : α
a✝¹ : EqvGen r a b
a✝ : EqvGen r b c
hab : EqvGen p a b
hbc : EqvGen p b c
⊢ EqvGen p a c
exact EqvGen.trans _ _ _ hab hbc