-- Mathlib/Logic/Relation.lean
theorem total_of_right_unique (U : Relator.RightUnique r) (ab : ReflTransGen r a b)
    (ac : ReflTransGen r a c) : ReflTransGen r b c ∨ ReflTransGen r c b

Proof state:
case refl
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
⊢ ReflTransGen r a c ∨ ReflTransGen r c a

Tactic:
exact Or.inl ac

Result:
no goals

Proof state:
case tail.inl.inr.intro.intro.refl
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r b✝ c
be : r b✝ c✝
ec : ReflTransGen r c✝ c
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝

Tactic:
exact Or.inl ec

Result:
no goals

Proof state:
case tail.inl.inl
α : Type u_1
r : α → α → Prop
a b : α
U : Relator.RightUnique r
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
ac : ReflTransGen r a b✝
IH : ReflTransGen r b✝ b✝
⊢ ReflTransGen r c✝ b✝ ∨ ReflTransGen r b✝ c✝

Tactic:
exact Or.inr (single bd)

Result:
no goals

Proof state:
case tail
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r b✝ c ∨ ReflTransGen r c b✝
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝

Tactic:
rcases IH with (IH | IH)

Result:
case tail.inl
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r b✝ c
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝

case tail.inr
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r c b✝
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝

Proof state:
case tail.inl
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r b✝ c
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝

Tactic:
rcases cases_head IH with (rfl | ⟨e, be, ec⟩)

Result:
case tail.inl.inl
α : Type u_1
r : α → α → Prop
a b : α
U : Relator.RightUnique r
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
ac : ReflTransGen r a b✝
IH : ReflTransGen r b✝ b✝
⊢ ReflTransGen r c✝ b✝ ∨ ReflTransGen r b✝ c✝

case tail.inl.inr.intro.intro
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r b✝ c
e : α
be : r b✝ e
ec : ReflTransGen r e c
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝

Proof state:
case tail.inr
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r c b✝
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝

Tactic:
exact Or.inr (IH.tail bd)

Result:
no goals

Proof state:
case tail.inl.inr.intro.intro
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r b✝ c
e : α
be : r b✝ e
ec : ReflTransGen r e c
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝

Tactic:
cases U bd be

Result:
case tail.inl.inr.intro.intro.refl
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r b✝ c
be : r b✝ c✝
ec : ReflTransGen r c✝ c
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝