case single
α : Type u_1
β : Type ?u.22591
γ : Type ?u.22594
δ : Type ?u.22597
r : α → α → Prop
a✝¹ b✝¹ c d : α
trans : Transitive r
a b b✝ : α
a✝ : r a b✝
⊢ r a b✝

case tail
α : Type u_1
β : Type ?u.22591
γ : Type ?u.22594
δ : Type ?u.22597
r : α → α → Prop
a✝² b✝¹ c d : α
trans : Transitive r
a b b✝ c✝ : α
a✝¹ : TransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : r a b✝
⊢ r a c✝
α : Type u_1
β : Type ?u.22591
γ : Type ?u.22594
δ : Type ?u.22597
r : α → α → Prop
a✝ b✝ c d : α
trans : Transitive r
a b : α
h : TransGen r a b
⊢ r a b
induction h
case tail
α : Type u_1
β : Type ?u.22591
γ : Type ?u.22594
δ : Type ?u.22597
r : α → α → Prop
a✝² b✝¹ c d : α
trans : Transitive r
a b b✝ c✝ : α
a✝¹ : TransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : r a b✝
⊢ r a c✝
case single
α : Type u_1
β : Type ?u.22591
γ : Type ?u.22594
δ : Type ?u.22597
r : α → α → Prop
a✝¹ b✝¹ c d : α
trans : Transitive r
a b b✝ : α
a✝ : r a b✝
⊢ r a b✝

case tail
α : Type u_1
β : Type ?u.22591
γ : Type ?u.22594
δ : Type ?u.22597
r : α → α → Prop
a✝² b✝¹ c d : α
trans : Transitive r
a b b✝ c✝ : α
a✝¹ : TransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : r a b✝
⊢ r a c✝
case single _ hc => exact hc
no goals
case tail
α : Type u_1
β : Type ?u.22591
γ : Type ?u.22594
δ : Type ?u.22597
r : α → α → Prop
a✝² b✝¹ c d : α
trans : Transitive r
a b b✝ c✝ : α
a✝¹ : TransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : r a b✝
⊢ r a c✝
case tail c d _ hcd hac => exact trans hac hcd
no goals
α : Type u_1
β : Type ?u.22591
γ : Type ?u.22594
δ : Type ?u.22597
r : α → α → Prop
a✝ b✝¹ c d : α
trans : Transitive r
a b b✝ : α
hc : r a b✝
⊢ r a b✝
exact hc
no goals
α : Type u_1
β : Type ?u.22591
γ : Type ?u.22594
δ : Type ?u.22597
r : α → α → Prop
a✝¹ b✝ c✝ d✝ : α
trans : Transitive r
a b c d : α
a✝ : TransGen r a c
hcd : r c d
hac : r a c
⊢ r a d
exact trans hac hcd