case refl
α : Type u_1
β : Type ?u.17670
γ : Type ?u.17673
δ : Type ?u.17676
r : α → α → Prop
a b c d : α
⊢ b = b ∨ ∃ c, r b c ∧ ReflTransGen r c b

case head
α : Type u_1
β : Type ?u.17670
γ : Type ?u.17673
δ : Type ?u.17676
r : α → α → Prop
a b c d a✝¹ c✝ : α
h'✝ : r a✝¹ c✝
h✝ : ReflTransGen r c✝ b
a✝ : c✝ = b ∨ ∃ c, r c✝ c ∧ ReflTransGen r c b
⊢ a✝¹ = b ∨ ∃ c, r a✝¹ c ∧ ReflTransGen r c b
α : Type u_1
β : Type ?u.17670
γ : Type ?u.17673
δ : Type ?u.17676
r : α → α → Prop
a b c d : α
h : ReflTransGen r a b
⊢ a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b
induction h using Relation.ReflTransGen.head_induction_on
case refl.h
α : Type u_1
β : Type ?u.17670
γ : Type ?u.17673
δ : Type ?u.17676
r : α → α → Prop
a b c d : α
⊢ b = b
case refl
α : Type u_1
β : Type ?u.17670
γ : Type ?u.17673
δ : Type ?u.17676
r : α → α → Prop
a b c d : α
⊢ b = b ∨ ∃ c, r b c ∧ ReflTransGen r c b
left
no goals
case refl.h
α : Type u_1
β : Type ?u.17670
γ : Type ?u.17673
δ : Type ?u.17676
r : α → α → Prop
a b c d : α
⊢ b = b
rfl
case head.h
α : Type u_1
β : Type ?u.17670
γ : Type ?u.17673
δ : Type ?u.17676
r : α → α → Prop
a b c d a✝¹ c✝ : α
h'✝ : r a✝¹ c✝
h✝ : ReflTransGen r c✝ b
a✝ : c✝ = b ∨ ∃ c, r c✝ c ∧ ReflTransGen r c b
⊢ ∃ c, r a✝¹ c ∧ ReflTransGen r c b
case head
α : Type u_1
β : Type ?u.17670
γ : Type ?u.17673
δ : Type ?u.17676
r : α → α → Prop
a b c d a✝¹ c✝ : α
h'✝ : r a✝¹ c✝
h✝ : ReflTransGen r c✝ b
a✝ : c✝ = b ∨ ∃ c, r c✝ c ∧ ReflTransGen r c b
⊢ a✝¹ = b ∨ ∃ c, r a✝¹ c ∧ ReflTransGen r c b
right
no goals
case head.h
α : Type u_1
β : Type ?u.17670
γ : Type ?u.17673
δ : Type ?u.17676
r : α → α → Prop
a b c d a✝¹ c✝ : α
h'✝ : r a✝¹ c✝
h✝ : ReflTransGen r c✝ b
a✝ : c✝ = b ∨ ∃ c, r c✝ c ∧ ReflTransGen r c b
⊢ ∃ c, r a✝¹ c ∧ ReflTransGen r c b
exact ⟨_, by assumption, by assumption⟩
no goals
α : Type u_1
β : Type ?u.17670
γ : Type ?u.17673
δ : Type ?u.17676
r : α → α → Prop
a b c d a✝¹ c✝ : α
h'✝ : r a✝¹ c✝
h✝ : ReflTransGen r c✝ b
a✝ : c✝ = b ∨ ∃ c, r c✝ c ∧ ReflTransGen r c b
⊢ r a✝¹ ?m.17808
assumption
no goals
α : Type u_1
β : Type ?u.17670
γ : Type ?u.17673
δ : Type ?u.17676
r : α → α → Prop
a b c d a✝¹ c✝ : α
h'✝ : r a✝¹ c✝
h✝ : ReflTransGen r c✝ b
a✝ : c✝ = b ∨ ∃ c, r c✝ c ∧ ReflTransGen r c b
⊢ ReflTransGen r c✝ b
assumption