[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
⊢ Part.fix f x = Fix.approx f (Nat.succ (Nat.find h')) x
[PROOFSTEP]
let p := fun i : ℕ => (Fix.approx f i x).Dom
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
⊢ Part.fix f x = Fix.approx f (Nat.succ (Nat.find h')) x
[PROOFSTEP]
have : p (Nat.find h') := Nat.find_spec h'
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
this : p (Nat.find h')
⊢ Part.fix f x = Fix.approx f (Nat.succ (Nat.find h')) x
[PROOFSTEP]
generalize hk : Nat.find h' = k
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
this : p (Nat.find h')
k : ℕ
hk : Nat.find h' = k
⊢ Part.fix f x = Fix.approx f (Nat.succ k) x
[PROOFSTEP]
replace hk : Nat.find h' = k + (@Upto.zero p).val := hk
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
this : p (Nat.find h')
k : ℕ
hk : Nat.find h' = k + ↑Upto.zero
⊢ Part.fix f x = Fix.approx f (Nat.succ k) x
[PROOFSTEP]
rw [hk] at this 
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
k : ℕ
this : p (k + ↑Upto.zero)
hk : Nat.find h' = k + ↑Upto.zero
⊢ Part.fix f x = Fix.approx f (Nat.succ k) x
[PROOFSTEP]
revert hk
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
k : ℕ
this : p (k + ↑Upto.zero)
⊢ Nat.find h' = k + ↑Upto.zero → Part.fix f x = Fix.approx f (Nat.succ k) x
[PROOFSTEP]
dsimp [Part.fix]
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
k : ℕ
this : p (k + ↑Upto.zero)
⊢ Nat.find h' = k + ↑Upto.zero →
    (assert (∃ i, (Fix.approx f i x).Dom) fun h =>
        WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) Upto.zero x) =
      Fix.approx f (Nat.succ k) x
[PROOFSTEP]
rw [assert_pos h']
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
k : ℕ
this : p (k + ↑Upto.zero)
⊢ Nat.find h' = k + ↑Upto.zero →
    WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) Upto.zero x =
      Fix.approx f (Nat.succ k) x
[PROOFSTEP]
revert this
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
k : ℕ
⊢ p (k + ↑Upto.zero) →
    Nat.find h' = k + ↑Upto.zero →
      WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) Upto.zero x =
        Fix.approx f (Nat.succ k) x
[PROOFSTEP]
generalize Upto.zero = z
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
k : ℕ
z : Upto p
⊢ p (k + ↑z) →
    Nat.find h' = k + ↑z →
      WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x =
        Fix.approx f (Nat.succ k) x
[PROOFSTEP]
intro _this hk
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
k : ℕ
z : Upto p
_this : p (k + ↑z)
hk : Nat.find h' = k + ↑z
⊢ WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x =
    Fix.approx f (Nat.succ k) x
[PROOFSTEP]
suffices : ∀ x', WellFounded.fix (Part.fix.proof_1 f x h') (fixAux f) z x' = Fix.approx f (succ k) x'
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
k : ℕ
z : Upto p
_this : p (k + ↑z)
hk : Nat.find h' = k + ↑z
this :
  ∀ (x' : α),
    WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
      Fix.approx f (Nat.succ k) x'
⊢ WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x =
    Fix.approx f (Nat.succ k) x
case this
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
k : ℕ
z : Upto p
_this : p (k + ↑z)
hk : Nat.find h' = k + ↑z
⊢ ∀ (x' : α),
    WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
      Fix.approx f (Nat.succ k) x'
[PROOFSTEP]
exact this _
[GOAL]
case this
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
k : ℕ
z : Upto p
_this : p (k + ↑z)
hk : Nat.find h' = k + ↑z
⊢ ∀ (x' : α),
    WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
      Fix.approx f (Nat.succ k) x'
[PROOFSTEP]
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'
    rw [hk, Nat.succ_add, ← Nat.add_succ]
    apply Nat.lt_of_succ_le
    apply Nat.le_add_left
  rw [succ_add_eq_succ_add] at _this hk 
  rw [assert_pos hh, n_ih (Upto.succ z hh) _this hk]
[GOAL]
case this
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
k : ℕ
z : Upto p
_this : p (k + ↑z)
hk : Nat.find h' = k + ↑z
⊢ ∀ (x' : α),
    WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
      Fix.approx f (Nat.succ k) x'
[PROOFSTEP]
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'
    rw [hk, Nat.succ_add, ← Nat.add_succ]
    apply Nat.lt_of_succ_le
    apply Nat.le_add_left
  rw [succ_add_eq_succ_add] at _this hk 
  rw [assert_pos hh, n_ih (Upto.succ z hh) _this hk]
[GOAL]
case this.zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
z : Upto p
_this : p (Nat.zero + ↑z)
hk : Nat.find h' = Nat.zero + ↑z
⊢ ∀ (x' : α),
    WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
      Fix.approx f (Nat.succ Nat.zero) x'
[PROOFSTEP]

| 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]
[GOAL]
case this.zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
z : Upto p
_this : p (Nat.zero + ↑z)
hk : Nat.find h' = Nat.zero + ↑z
⊢ ∀ (x' : α),
    WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
      Fix.approx f (Nat.succ Nat.zero) x'
[PROOFSTEP]
intro x'
[GOAL]
case this.zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
z : Upto p
_this : p (Nat.zero + ↑z)
hk : Nat.find h' = Nat.zero + ↑z
x' : α
⊢ WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
    Fix.approx f (Nat.succ Nat.zero) x'
[PROOFSTEP]
rw [Fix.approx, WellFounded.fix_eq, fixAux]
[GOAL]
case this.zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
z : Upto p
_this : p (Nat.zero + ↑z)
hk : Nat.find h' = Nat.zero + ↑z
x' : α
⊢ f
      (fun x_1 =>
        assert (¬(Fix.approx f (↑z) x).Dom) fun h =>
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_2 => (Fix.approx f x_2 x).Dom)) (fixAux f) (Upto.succ z h)
            x_1)
      x' =
    f (Fix.approx f Nat.zero) x'
[PROOFSTEP]
congr
[GOAL]
case this.zero.e_a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
z : Upto p
_this : p (Nat.zero + ↑z)
hk : Nat.find h' = Nat.zero + ↑z
x' : α
⊢ (fun x_1 =>
      assert (¬(Fix.approx f (↑z) x).Dom) fun h =>
        WellFounded.fix (_ : WellFounded (Upto.GT fun x_2 => (Fix.approx f x_2 x).Dom)) (fixAux f) (Upto.succ z h)
          x_1) =
    Fix.approx f Nat.zero
[PROOFSTEP]
ext x : 1
[GOAL]
case this.zero.e_a.h
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x✝ : α
h' : ∃ i, (Fix.approx f i x✝).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x✝).Dom
z : Upto p
_this : p (Nat.zero + ↑z)
hk : Nat.find h' = Nat.zero + ↑z
x' x : α
⊢ (assert (¬(Fix.approx f (↑z) x✝).Dom) fun h =>
      WellFounded.fix (_ : WellFounded (Upto.GT fun x => (Fix.approx f x x✝).Dom)) (fixAux f) (Upto.succ z h) x) =
    Fix.approx f Nat.zero x
[PROOFSTEP]
rw [assert_neg]
[GOAL]
case this.zero.e_a.h
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x✝ : α
h' : ∃ i, (Fix.approx f i x✝).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x✝).Dom
z : Upto p
_this : p (Nat.zero + ↑z)
hk : Nat.find h' = Nat.zero + ↑z
x' x : α
⊢ none = Fix.approx f Nat.zero x
case this.zero.e_a.h
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x✝ : α
h' : ∃ i, (Fix.approx f i x✝).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x✝).Dom
z : Upto p
_this : p (Nat.zero + ↑z)
hk : Nat.find h' = Nat.zero + ↑z
x' x : α
⊢ ¬¬(Fix.approx f (↑z) x✝).Dom
[PROOFSTEP]
rfl
[GOAL]
case this.zero.e_a.h
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x✝ : α
h' : ∃ i, (Fix.approx f i x✝).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x✝).Dom
z : Upto p
_this : p (Nat.zero + ↑z)
hk : Nat.find h' = Nat.zero + ↑z
x' x : α
⊢ ¬¬(Fix.approx f (↑z) x✝).Dom
[PROOFSTEP]
rw [Nat.zero_add] at _this 
[GOAL]
case this.zero.e_a.h
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x✝ : α
h' : ∃ i, (Fix.approx f i x✝).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x✝).Dom
z : Upto p
_this : p ↑z
hk : Nat.find h' = Nat.zero + ↑z
x' x : α
⊢ ¬¬(Fix.approx f (↑z) x✝).Dom
[PROOFSTEP]
simpa only [not_not, Coe]
[GOAL]
case this.succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α),
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
            Fix.approx f (Nat.succ n) x'
z : Upto p
_this : p (Nat.succ n + ↑z)
hk : Nat.find h' = Nat.succ n + ↑z
⊢ ∀ (x' : α),
    WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
      Fix.approx f (Nat.succ (Nat.succ n)) x'
[PROOFSTEP]

| 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'
    rw [hk, Nat.succ_add, ← Nat.add_succ]
    apply Nat.lt_of_succ_le
    apply Nat.le_add_left
  rw [succ_add_eq_succ_add] at _this hk 
  rw [assert_pos hh, n_ih (Upto.succ z hh) _this hk]
[GOAL]
case this.succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α),
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
            Fix.approx f (Nat.succ n) x'
z : Upto p
_this : p (Nat.succ n + ↑z)
hk : Nat.find h' = Nat.succ n + ↑z
⊢ ∀ (x' : α),
    WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
      Fix.approx f (Nat.succ (Nat.succ n)) x'
[PROOFSTEP]
intro x'
[GOAL]
case this.succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α),
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
            Fix.approx f (Nat.succ n) x'
z : Upto p
_this : p (Nat.succ n + ↑z)
hk : Nat.find h' = Nat.succ n + ↑z
x' : α
⊢ WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
    Fix.approx f (Nat.succ (Nat.succ n)) x'
[PROOFSTEP]
rw [Fix.approx, WellFounded.fix_eq, fixAux]
[GOAL]
case this.succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α),
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
            Fix.approx f (Nat.succ n) x'
z : Upto p
_this : p (Nat.succ n + ↑z)
hk : Nat.find h' = Nat.succ n + ↑z
x' : α
⊢ f
      (fun x_1 =>
        assert (¬(Fix.approx f (↑z) x).Dom) fun h =>
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_2 => (Fix.approx f x_2 x).Dom)) (fixAux f) (Upto.succ z h)
            x_1)
      x' =
    f (Fix.approx f (n + 1)) x'
[PROOFSTEP]
congr
[GOAL]
case this.succ.e_a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α),
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
            Fix.approx f (Nat.succ n) x'
z : Upto p
_this : p (Nat.succ n + ↑z)
hk : Nat.find h' = Nat.succ n + ↑z
x' : α
⊢ (fun x_1 =>
      assert (¬(Fix.approx f (↑z) x).Dom) fun h =>
        WellFounded.fix (_ : WellFounded (Upto.GT fun x_2 => (Fix.approx f x_2 x).Dom)) (fixAux f) (Upto.succ z h)
          x_1) =
    Fix.approx f (n + 1)
[PROOFSTEP]
ext : 1
[GOAL]
case this.succ.e_a.h
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α),
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
            Fix.approx f (Nat.succ n) x'
z : Upto p
_this : p (Nat.succ n + ↑z)
hk : Nat.find h' = Nat.succ n + ↑z
x' x✝ : α
⊢ (assert (¬(Fix.approx f (↑z) x).Dom) fun h =>
      WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) (Upto.succ z h) x✝) =
    Fix.approx f (n + 1) x✝
[PROOFSTEP]
have hh : ¬(Fix.approx f z.val x).Dom := by
  apply Nat.find_min h'
  rw [hk, Nat.succ_add, ← Nat.add_succ]
  apply Nat.lt_of_succ_le
  apply Nat.le_add_left
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α),
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
            Fix.approx f (Nat.succ n) x'
z : Upto p
_this : p (Nat.succ n + ↑z)
hk : Nat.find h' = Nat.succ n + ↑z
x' x✝ : α
⊢ ¬(Fix.approx f (↑z) x).Dom
[PROOFSTEP]
apply Nat.find_min h'
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α),
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
            Fix.approx f (Nat.succ n) x'
z : Upto p
_this : p (Nat.succ n + ↑z)
hk : Nat.find h' = Nat.succ n + ↑z
x' x✝ : α
⊢ ↑z < Nat.find h'
[PROOFSTEP]
rw [hk, Nat.succ_add, ← Nat.add_succ]
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α),
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
            Fix.approx f (Nat.succ n) x'
z : Upto p
_this : p (Nat.succ n + ↑z)
hk : Nat.find h' = Nat.succ n + ↑z
x' x✝ : α
⊢ ↑z < n + Nat.succ ↑z
[PROOFSTEP]
apply Nat.lt_of_succ_le
[GOAL]
case h
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α),
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
            Fix.approx f (Nat.succ n) x'
z : Upto p
_this : p (Nat.succ n + ↑z)
hk : Nat.find h' = Nat.succ n + ↑z
x' x✝ : α
⊢ Nat.succ ↑z ≤ n + Nat.succ ↑z
[PROOFSTEP]
apply Nat.le_add_left
[GOAL]
case this.succ.e_a.h
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α),
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
            Fix.approx f (Nat.succ n) x'
z : Upto p
_this : p (Nat.succ n + ↑z)
hk : Nat.find h' = Nat.succ n + ↑z
x' x✝ : α
hh : ¬(Fix.approx f (↑z) x).Dom
⊢ (assert (¬(Fix.approx f (↑z) x).Dom) fun h =>
      WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) (Upto.succ z h) x✝) =
    Fix.approx f (n + 1) x✝
[PROOFSTEP]
rw [succ_add_eq_succ_add] at _this hk 
[GOAL]
case this.succ.e_a.h
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i => (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α),
          WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) z x' =
            Fix.approx f (Nat.succ n) x'
z : Upto p
_this : p (n + Nat.succ ↑z)
hk : Nat.find h' = n + Nat.succ ↑z
x' x✝ : α
hh : ¬(Fix.approx f (↑z) x).Dom
⊢ (assert (¬(Fix.approx f (↑z) x).Dom) fun h =>
      WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) (Upto.succ z h) x✝) =
    Fix.approx f (n + 1) x✝
[PROOFSTEP]
rw [assert_pos hh, n_ih (Upto.succ z hh) _this hk]
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ¬∃ i, (Fix.approx f i x).Dom
⊢ Part.fix f x = none
[PROOFSTEP]
dsimp [Part.fix]
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ¬∃ i, (Fix.approx f i x).Dom
⊢ (assert (∃ i, (Fix.approx f i x).Dom) fun h =>
      WellFounded.fix (_ : WellFounded (Upto.GT fun x_1 => (Fix.approx f x_1 x).Dom)) (fixAux f) Upto.zero x) =
    none
[PROOFSTEP]
rw [assert_neg h']
