English
Equality showing that fixInduction' specialized to a forward stop yields the base case: fixInduction'_stop h fa = hbase a fa.
Русский
Равенство: фиксInduction'_stop, стягиваемое к базовому случаю: fixInduction'_stop h fa = hbase a fa.
LaTeX
$$$\\text{fixInduction' }(h,hbase,hind) = hbase\\ a\\ fa$$$
Lean4
theorem fixInduction'_stop {C : α → Sort*} {f : α →. β ⊕ α} {b : β} {a : α} (h : b ∈ f.fix a) (fa : Sum.inl b ∈ f 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₀) :
@fixInduction' _ _ C _ _ _ h hbase hind = hbase a fa :=
by
unfold fixInduction'
rw [fixInduction_spec]
-- Porting note: the explicit motive required because `simp` does not apply `Part.get_eq_of_mem`
refine
Eq.rec (motive := fun x e ↦
Sum.casesOn x ?_ ?_ (Eq.trans (Part.get_eq_of_mem fa (dom_of_mem_fix h)) e) = hbase a fa) ?_
(Part.get_eq_of_mem fa (dom_of_mem_fix h)).symm
simp
