Theorem: LoVe.RTC.head (LoVe/LoVelib.lean)

State before:
α : Type
R : α → α → Prop
a b c : α
hab : R a b
hbc : RTC R b c
⊢ RTC R a c
Tactic:
induction hbc with
| refl =>
  exact tail _ _ refl hab
| tail c d hbc hcd hac =>
  apply tail <;>
    assumption
State after:
no goals

State before:
case refl
α : Type
R : α → α → Prop
a b c : α
hab : R a b
⊢ RTC R a b
Tactic:
exact tail _ _ refl hab
State after:
no goals

State before:
case tail
α : Type
R : α → α → Prop
a b c✝ : α
hab : R a b
c d : α
hbc : RTC R b c
hcd : R c d
hac : RTC R a c
⊢ RTC R a d
Tactic:
apply tail <;>
  assumption
State after:
no goals