α : Type u_1
β : Type ?u.21101
γ : Type ?u.21104
δ : Type ?u.21107
r : α → α → Prop
a b c d : α
h : TransGen r a c
⊢ ∃ b, ReflTransGen r a b ∧ r b c
α : Type u_1
β : Type ?u.21101
γ : Type ?u.21104
δ : Type ?u.21107
r : α → α → Prop
a b c d : α
⊢ TransGen r a c ↔ ∃ b, ReflTransGen r a b ∧ r b c
refine' ⟨fun h ↦ _, fun ⟨b, hab, hbc⟩ ↦ tail' hab hbc⟩
case single
α : Type u_1
β : Type ?u.21101
γ : Type ?u.21104
δ : Type ?u.21107
r : α → α → Prop
a b c d : α
hac : r a c
⊢ ∃ b, ReflTransGen r a b ∧ r b c

case tail
α : Type u_1
β : Type ?u.21101
γ : Type ?u.21104
δ : Type ?u.21107
r : α → α → Prop
a b✝ c d b : α
hab : TransGen r a b
hbc : r b c
⊢ ∃ b, ReflTransGen r a b ∧ r b c
α : Type u_1
β : Type ?u.21101
γ : Type ?u.21104
δ : Type ?u.21107
r : α → α → Prop
a b c d : α
h : TransGen r a c
⊢ ∃ b, ReflTransGen r a b ∧ r b c
cases' h with _ hac b _ hab hbc
no goals
case single
α : Type u_1
β : Type ?u.21101
γ : Type ?u.21104
δ : Type ?u.21107
r : α → α → Prop
a b c d : α
hac : r a c
⊢ ∃ b, ReflTransGen r a b ∧ r b c
exact ⟨_, by rfl, hac⟩
no goals
α : Type u_1
β : Type ?u.21101
γ : Type ?u.21104
δ : Type ?u.21107
r : α → α → Prop
a b c d : α
hac : r a c
⊢ ReflTransGen r a a
rfl
no goals
case tail
α : Type u_1
β : Type ?u.21101
γ : Type ?u.21104
δ : Type ?u.21107
r : α → α → Prop
a b✝ c d b : α
hab : TransGen r a b
hbc : r b c
⊢ ∃ b, ReflTransGen r a b ∧ r b c
exact ⟨_, hab.to_reflTransGen, hbc⟩