α : Type u_1
β : Type ?u.21585
γ : Type ?u.21588
δ : Type ?u.21591
r : α → α → Prop
a b c d : α
h : TransGen r a c
⊢ ∃ b, r a b ∧ ReflTransGen r b c
α : Type u_1
β : Type ?u.21585
γ : Type ?u.21588
δ : Type ?u.21591
r : α → α → Prop
a b c d : α
⊢ TransGen r a c ↔ ∃ b, r a b ∧ ReflTransGen r b c
refine' ⟨fun h ↦ _, fun ⟨b, hab, hbc⟩ ↦ head' hab hbc⟩
case single
α : Type u_1
β : Type ?u.21585
γ : Type ?u.21588
δ : Type ?u.21591
r : α → α → Prop
a b c d b✝ : α
a✝ : r a b✝
⊢ ∃ b, r a b ∧ ReflTransGen r b b✝

case tail
α : Type u_1
β : Type ?u.21585
γ : Type ?u.21588
δ : Type ?u.21591
r : α → α → Prop
a b c d b✝ c✝ : α
a✝¹ : TransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : ∃ b, r a b ∧ ReflTransGen r b b✝
⊢ ∃ b, r a b ∧ ReflTransGen r b c✝
α : Type u_1
β : Type ?u.21585
γ : Type ?u.21588
δ : Type ?u.21591
r : α → α → Prop
a b c d : α
h : TransGen r a c
⊢ ∃ b, r a b ∧ ReflTransGen r b c
induction h
case tail
α : Type u_1
β : Type ?u.21585
γ : Type ?u.21588
δ : Type ?u.21591
r : α → α → Prop
a b c d b✝ c✝ : α
a✝¹ : TransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : ∃ b, r a b ∧ ReflTransGen r b b✝
⊢ ∃ b, r a b ∧ ReflTransGen r b c✝
case single
α : Type u_1
β : Type ?u.21585
γ : Type ?u.21588
δ : Type ?u.21591
r : α → α → Prop
a b c d b✝ : α
a✝ : r a b✝
⊢ ∃ b, r a b ∧ ReflTransGen r b b✝

case tail
α : Type u_1
β : Type ?u.21585
γ : Type ?u.21588
δ : Type ?u.21591
r : α → α → Prop
a b c d b✝ c✝ : α
a✝¹ : TransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : ∃ b, r a b ∧ ReflTransGen r b b✝
⊢ ∃ b, r a b ∧ ReflTransGen r b c✝
case single c hac => exact ⟨_, hac, by rfl⟩
no goals
case tail
α : Type u_1
β : Type ?u.21585
γ : Type ?u.21588
δ : Type ?u.21591
r : α → α → Prop
a b c d b✝ c✝ : α
a✝¹ : TransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : ∃ b, r a b ∧ ReflTransGen r b b✝
⊢ ∃ b, r a b ∧ ReflTransGen r b c✝
case tail b c _ hbc IH =>
rcases IH with ⟨d, had, hdb⟩
exact ⟨_, had, hdb.tail hbc⟩
no goals
α : Type u_1
β : Type ?u.21585
γ : Type ?u.21588
δ : Type ?u.21591
r : α → α → Prop
a b c✝ d c : α
hac : r a c
⊢ ∃ b, r a b ∧ ReflTransGen r b c
exact ⟨_, hac, by rfl⟩
no goals
α : Type u_1
β : Type ?u.21585
γ : Type ?u.21588
δ : Type ?u.21591
r : α → α → Prop
a b c✝ d c : α
hac : r a c
⊢ ReflTransGen r c c
rfl
case intro.intro
α : Type u_1
β : Type ?u.21585
γ : Type ?u.21588
δ : Type ?u.21591
r : α → α → Prop
a b✝ c✝ d✝ b c : α
a✝ : TransGen r a b
hbc : r b c
d : α
had : r a d
hdb : ReflTransGen r d b
⊢ ∃ b, r a b ∧ ReflTransGen r b c
α : Type u_1
β : Type ?u.21585
γ : Type ?u.21588
δ : Type ?u.21591
r : α → α → Prop
a b✝ c✝ d b c : α
a✝ : TransGen r a b
hbc : r b c
IH : ∃ b_1, r a b_1 ∧ ReflTransGen r b_1 b
⊢ ∃ b, r a b ∧ ReflTransGen r b c
rcases IH with ⟨d, had, hdb⟩
no goals
case intro.intro
α : Type u_1
β : Type ?u.21585
γ : Type ?u.21588
δ : Type ?u.21591
r : α → α → Prop
a b✝ c✝ d✝ b c : α
a✝ : TransGen r a b
hbc : r b c
d : α
had : r a d
hdb : ReflTransGen r d b
⊢ ∃ b, r a b ∧ ReflTransGen r b c
exact ⟨_, had, hdb.tail hbc⟩