Lean4
protected theorem fix_def {x : α} (h' : ∃ i, (Fix.approx f i x).Dom) :
Part.fix f x = Fix.approx f (Nat.succ (Nat.find h')) x :=
by
let p := fun i : ℕ => (Fix.approx f i x).Dom
have : p (Nat.find h') := Nat.find_spec h'
generalize hk : Nat.find h' = k
replace hk : Nat.find h' = k + (@Upto.zero p).val := hk
rw [hk] at this
revert hk
dsimp [Part.fix]; rw [assert_pos h']; revert this
generalize Upto.zero = z; intro _this hk
suffices ∀ x' hwf, WellFounded.fix hwf (fixAux f) z x' = Fix.approx f (succ k) x' from this _ _
induction k generalizing z with
| zero =>
intro x' _
rw [Fix.approx, WellFounded.fix_eq, fixAux]
congr
ext x : 1
rw [assert_neg]
· rfl
· rw [Nat.zero_add] at _this
simpa only [not_not, Coe]
| succ n n_ih =>
intro x' _
rw [Fix.approx, WellFounded.fix_eq, fixAux]
congr
ext : 1
have hh : ¬(Fix.approx f z.val x).Dom := by
apply Nat.find_min h'
omega
rw [succ_add_eq_add_succ] at _this hk
rw [assert_pos hh, n_ih (Upto.succ z hh) _this hk]
