English
If h ∈ f.fix a and h' ∈ f.fix a', with fa : inr(a') ∈ f(a), then fixInduction' h hbase hind equals hind a a' h' (fixInduction' h' hbase hind).
Русский
Если h ∈ f.fix(a) и h' ∈ f.fix(a'), при fa = inr(a') ∈ f(a), тогда fixInduction' h hbase hind = hind a a' h' (fixInduction' h' hbase hind).
LaTeX
$$$\\text{FixInduction'}\\ h\\ h'\\ fa\\ hbase\\ hind = \\ hind\\ a\\ a'\\ h'\\ fa\\ (\\text{FixInduction'}\\ h'\\ hbase\\ hind)$$$
Lean4
theorem fixInduction'_fwd {C : α → Sort*} {f : α →. β ⊕ α} {b : β} {a a' : α} (h : b ∈ f.fix a) (h' : b ∈ f.fix a')
(fa : Sum.inr a' ∈ 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 = hind a a' h' fa (fixInduction' h' hbase hind) :=
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 (motive := fun y => (f a).get (dom_of_mem_fix h) = y → C a) x ?_ ?_
(Eq.trans (Part.get_eq_of_mem fa (dom_of_mem_fix h)) e) =
_)
?_ (Part.get_eq_of_mem fa (dom_of_mem_fix h)).symm
simp
