case refl
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a b c d : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
⊢ Join (ReflTransGen r) a c

case tail
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a b c d : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
b✝ c✝ : α
a✝¹ : ReflTransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : Join (ReflTransGen r) b✝ c
⊢ Join (ReflTransGen r) c✝ c
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a b c d : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hab : ReflTransGen r a b
hac : ReflTransGen r a c
⊢ Join (ReflTransGen r) b c
induction hab
case tail
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a b c d : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
b✝ c✝ : α
a✝¹ : ReflTransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : Join (ReflTransGen r) b✝ c
⊢ Join (ReflTransGen r) c✝ c
case refl
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a b c d : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
⊢ Join (ReflTransGen r) a c

case tail
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a b c d : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
b✝ c✝ : α
a✝¹ : ReflTransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : Join (ReflTransGen r) b✝ c
⊢ Join (ReflTransGen r) c✝ c
case refl => exact ⟨c, hac, refl⟩
no goals
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a b c d : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
⊢ Join (ReflTransGen r) a c
exact ⟨c, hac, refl⟩
case intro.intro
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a b✝ c d✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
a✝ : ReflTransGen r a d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
⊢ Join (ReflTransGen r) e c
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a b c d✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
a✝ : ReflTransGen r a d
hde : r d e
ih : Join (ReflTransGen r) d c
⊢ Join (ReflTransGen r) e c
rcases ih with ⟨b, hdb, hcb⟩
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a✝¹ b✝ c d✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a✝¹ c
d e : α
a✝ : ReflTransGen r a✝¹ d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
a : α
hea : ReflTransGen r e a
hba : ReflGen r b a
⊢ Join (ReflTransGen r) e c
case intro.intro
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a b✝ c d✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
a✝ : ReflTransGen r a d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
this : ∃ a, ReflTransGen r e a ∧ ReflGen r b a
⊢ Join (ReflTransGen r) e c
rcases this with ⟨a, hea, hba⟩
case intro.intro.intro.intro.refl
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a b✝ c d✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
a✝ : ReflTransGen r a d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
hea : ReflTransGen r e b
⊢ Join (ReflTransGen r) e c

case intro.intro.intro.intro.single
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a✝¹ b✝ c d✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a✝¹ c
d e : α
a✝ : ReflTransGen r a✝¹ d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
a : α
hea : ReflTransGen r e a
hba : r b a
⊢ Join (ReflTransGen r) e c
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a✝¹ b✝ c d✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a✝¹ c
d e : α
a✝ : ReflTransGen r a✝¹ d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
a : α
hea : ReflTransGen r e a
hba : ReflGen r b a
⊢ Join (ReflTransGen r) e c
cases' hba with _ hba
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a b✝ c d✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
a✝ : ReflTransGen r a d
hde : r d e
b : α
hdb : ReflTransGen r d b
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r b a
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a b✝ c d✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
a✝ : ReflTransGen r a d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r b a
clear hcb
case refl
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a b✝ c d✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
a✝ : ReflTransGen r a d
hde : r d e
b : α
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r d a

case tail
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a b✝¹ c d✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
a✝² : ReflTransGen r a d
hde : r d e
b b✝ c✝ : α
a✝¹ : ReflTransGen r d b✝
a✝ : r b✝ c✝
a_ih✝ : ∃ a, ReflTransGen r e a ∧ ReflGen r b✝ a
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r c✝ a
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a b✝ c d✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
a✝ : ReflTransGen r a d
hde : r d e
b : α
hdb : ReflTransGen r d b
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r b a
induction hdb
case tail
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a b✝¹ c d✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
a✝² : ReflTransGen r a d
hde : r d e
b b✝ c✝ : α
a✝¹ : ReflTransGen r d b✝
a✝ : r b✝ c✝
a_ih✝ : ∃ a, ReflTransGen r e a ∧ ReflGen r b✝ a
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r c✝ a
case refl
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a b✝ c d✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
a✝ : ReflTransGen r a d
hde : r d e
b : α
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r d a

case tail
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a b✝¹ c d✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
a✝² : ReflTransGen r a d
hde : r d e
b b✝ c✝ : α
a✝¹ : ReflTransGen r d b✝
a✝ : r b✝ c✝
a_ih✝ : ∃ a, ReflTransGen r e a ∧ ReflGen r b✝ a
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r c✝ a
case refl => exact ⟨e, refl, ReflGen.single hde⟩
no goals
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a b✝ c d✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
a✝ : ReflTransGen r a d
hde : r d e
b : α
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r d a
exact ⟨e, refl, ReflGen.single hde⟩
case intro.intro
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a✝² b✝¹ c d✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a✝² c
d e : α
a✝¹ : ReflTransGen r a✝² d
hde : r d e
b✝ f b : α
a✝ : ReflTransGen r d f
hfb : r f b
a : α
hea : ReflTransGen r e a
hfa : ReflGen r f a
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r b a
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a b✝¹ c d✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
a✝¹ : ReflTransGen r a d
hde : r d e
b✝ f b : α
a✝ : ReflTransGen r d f
hfb : r f b
ih : ∃ a, ReflTransGen r e a ∧ ReflGen r f a
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r b a
rcases ih with ⟨a, hea, hfa⟩
case intro.intro.refl
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a b✝¹ c d✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
a✝¹ : ReflTransGen r a d
hde : r d e
b✝ f b : α
a✝ : ReflTransGen r d f
hfb : r f b
hea : ReflTransGen r e f
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r b a

case intro.intro.single
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a✝² b✝¹ c d✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a✝² c
d e : α
a✝¹ : ReflTransGen r a✝² d
hde : r d e
b✝ f b : α
a✝ : ReflTransGen r d f
hfb : r f b
a : α
hea : ReflTransGen r e a
hfa : r f a
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r b a
case intro.intro
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a✝² b✝¹ c d✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a✝² c
d e : α
a✝¹ : ReflTransGen r a✝² d
hde : r d e
b✝ f b : α
a✝ : ReflTransGen r d f
hfb : r f b
a : α
hea : ReflTransGen r e a
hfa : ReflGen r f a
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r b a
cases' hfa with _ hfa
no goals
case intro.intro.refl
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a b✝¹ c d✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
a✝¹ : ReflTransGen r a d
hde : r d e
b✝ f b : α
a✝ : ReflTransGen r d f
hfb : r f b
hea : ReflTransGen r e f
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r b a
exact ⟨b, hea.tail hfb, ReflGen.refl⟩
case intro.intro.single.intro.intro
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a✝² b✝¹ c✝ d✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac✝ : ReflTransGen r a✝² c✝
d e : α
a✝¹ : ReflTransGen r a✝² d
hde : r d e
b✝ f b : α
a✝ : ReflTransGen r d f
hfb : r f b
a : α
hea : ReflTransGen r e a
hfa : r f a
c : α
hbc : ReflGen r b c
hac : ReflTransGen r a c
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r b a
case intro.intro.single
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a✝² b✝¹ c d✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a✝² c
d e : α
a✝¹ : ReflTransGen r a✝² d
hde : r d e
b✝ f b : α
a✝ : ReflTransGen r d f
hfb : r f b
a : α
hea : ReflTransGen r e a
hfa : r f a
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r b a
rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
no goals
case intro.intro.single.intro.intro
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a✝² b✝¹ c✝ d✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac✝ : ReflTransGen r a✝² c✝
d e : α
a✝¹ : ReflTransGen r a✝² d
hde : r d e
b✝ f b : α
a✝ : ReflTransGen r d f
hfb : r f b
a : α
hea : ReflTransGen r e a
hfa : r f a
c : α
hbc : ReflGen r b c
hac : ReflTransGen r a c
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r b a
exact ⟨c, hea.trans hac, hbc⟩
no goals
case intro.intro.intro.intro.refl
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a b✝ c d✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
a✝ : ReflTransGen r a d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
hea : ReflTransGen r e b
⊢ Join (ReflTransGen r) e c
exact ⟨b, hea, hcb⟩
no goals
case intro.intro.intro.intro.single
α : Type u_1
β : Type ?u.27200
γ : Type ?u.27203
δ : Type ?u.27206
r : α → α → Prop
a✝¹ b✝ c d✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a✝¹ c
d e : α
a✝ : ReflTransGen r a✝¹ d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
a : α
hea : ReflTransGen r e a
hba : r b a
⊢ Join (ReflTransGen r) e c
exact ⟨a, hea, hcb.tail hba⟩