English
Induction principle for TransGen: to prove a property for h : TransGen r a b, it suffices to prove it for single-step occurrences and to show how to extend with transitivity.
Русский
Индукция по TransGen: чтобы доказать свойство для h : TransGen r a b, достаточно доказать для одиночного шага и показать как расширять через конкатенацию.
LaTeX
$$$ ∀ {α} {r} {motive : {a b : α} → \mathrm{TransGen} r a b → \mathrm{Prop}} {a b} (h : TransGen r a b), (single : ∀ {a b} (h : r a b), motive (single h)) \\n (trans : ∀ {a b c} (h₁ : TransGen r a b) (h₂ : TransGen r b c), motive h₁ → motive h₂ → motive (h₁.trans h₂)) : motive h $$$
Lean4
theorem cases_head_iff : ReflTransGen r a b ↔ a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b :=
by
use cases_head
rintro (rfl | ⟨c, hac, hcb⟩)
· rfl
· exact head hac hcb
