English
A variant of the induction principle: fixInduction' h hbase hind equals hind a a' h' fa (fixInduction' h' hbase hind).
Русский
Вариант принципа индукции: fixInduction' h hbase hind равно hind a a' h' fa (fixInduction' h' hbase hind).
LaTeX
$$$\\text{fixInduction'}\\ h\\ hbase\\ hind = \\ \\ hind\\ a\\ a'\\ h'\\ fa\\ (\\text{fixInduction'}\\ h'\\ hbase\\ hind)$$$
Lean4
/-- Another induction lemma for `b ∈ f.fix a` which allows one to prove a predicate `P` holds for
`a` given that `f a` inherits `P` from `a` and `P` holds for preimages of `b`.
-/
@[elab_as_elim]
def fixInduction' {C : α → Sort*} {f : α →. β ⊕ α} {b : β} {a : α} (h : b ∈ f.fix a)
(hbase : ∀ a_final : α, Sum.inl b ∈ f a_final → C a_final)
(hind : ∀ a₀ a₁ : α, b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀) : C a :=
by
refine fixInduction h fun a' h ih => ?_
rcases e : (f a').get (dom_of_mem_fix h) with b' | a'' <;> replace e : _ ∈ f a' := ⟨_, e⟩
· apply hbase
convert e
exact Part.mem_unique h (fix_stop e)
· exact hind _ _ (fix_fwd h e) e (ih _ e)
