English
A refined induction principle for PushoutI φ mirroring the structure of the Con and Coprod inductions.
Русский
Уточнённый принцип индукции для PushoutI φ, повторяющий структуру индукций Con и Coprod.
LaTeX
$$$\text{induction_on} \{motive: PushoutI(\varphi) → Prop\} (x: PushoutI(\varphi))\ldots$$$
Lean4
theorem induction_on {motive : PushoutI φ → Prop} (x : PushoutI φ) (of : ∀ (i : ι) (g : G i), motive (of i g))
(base : ∀ h, motive (base φ h)) (mul : ∀ x y, motive x → motive y → motive (x * y)) : motive x :=
by
delta PushoutI PushoutI.of PushoutI.base at *
induction x using Con.induction_on with
| H x =>
induction x using Coprod.induction_on with
| inl g =>
induction g using CoprodI.induction_on with
| of i g => exact of i g
| mul x y ihx ihy =>
rw [map_mul]
exact mul _ _ ihx ihy
| one => simpa using base 1
| inr h => exact base h
| mul x y ihx ihy => exact mul _ _ ihx ihy
