-- Mathlib/Control/Fix.lean
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

Proof state:
case 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' : α), ⋯.fix (fixAux f) z x' = Fix.approx f n.succ x'
z : Upto p
_this : p (n + (↑z).succ)
hk : Nat.find h' = n + (↑z).succ
x' x✝ : α
hh : ¬(Fix.approx f (↑z) x).Dom
⊢ (assert (¬(Fix.approx f (↑z) x).Dom) fun h => ⋯.fix (fixAux f) (z.succ h) x✝) = Fix.approx f (n + 1) x✝

Tactic:
rw [assert_pos hh, n_ih (Upto.succ z hh) _this hk]

Result:
no goals

Proof state:
α : 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.find h').succ x

Tactic:
generalize hk : Nat.find h' = k

Result:
α : 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 k.succ x

Proof state:
α : 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 k.succ x

Tactic:
replace hk : Nat.find h' = k + (@Upto.zero p).val := hk

Result:
α : 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 k.succ x

Proof state:
α : 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 => ⋯.fix (fixAux f) Upto.zero x) = Fix.approx f (k + 1) x

Tactic:
rw [assert_pos h']

Result:
α : 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 → ⋯.fix (fixAux f) Upto.zero x = Fix.approx f (k + 1) x

Proof state:
case 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 (0 + ↑z)
hk : Nat.find h' = 0 + ↑z
x' : α
⊢ ⋯.fix (fixAux f) z x' = Fix.approx f (Nat.succ 0) x'

Tactic:
rw [Fix.approx, WellFounded.fix_eq, fixAux]

Result:
case 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 (0 + ↑z)
hk : Nat.find h' = 0 + ↑z
x' : α
⊢ f (fun x_1 => assert (¬(Fix.approx f (↑z) x).Dom) fun h => ⋯.fix (fixAux f) (z.succ h) x_1) x' = f (Fix.approx f 0) x'

Proof state:
α : 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 → ⋯.fix (fixAux f) Upto.zero x = Fix.approx f (k + 1) x

Tactic:
revert this

Result:
α : 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 → ⋯.fix (fixAux f) Upto.zero x = Fix.approx f (k + 1) x

Proof state:
case 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 (0 + ↑z)
hk : Nat.find h' = 0 + ↑z
x' : α
⊢ f (fun x_1 => assert (¬(Fix.approx f (↑z) x).Dom) fun h => ⋯.fix (fixAux f) (z.succ h) x_1) x' = f (Fix.approx f 0) x'

Tactic:
congr

Result:
case 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 (0 + ↑z)
hk : Nat.find h' = 0 + ↑z
x' : α
⊢ (fun x_1 => assert (¬(Fix.approx f (↑z) x).Dom) fun h => ⋯.fix (fixAux f) (z.succ h) x_1) = Fix.approx f 0

Proof state:
α : 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 k.succ x

Tactic:
dsimp [Part.fix]

Result:
α : 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 => ⋯.fix (fixAux f) Upto.zero x) = Fix.approx f (k + 1) x

Proof state:
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' : α), ⋯.fix (fixAux f) z x' = Fix.approx f n.succ x'
z : Upto p
_this : p (n + 1 + ↑z)
hk : Nat.find h' = n + 1 + ↑z
x' x✝ : α
⊢ (↑z).succ ≤ n + (↑z).succ

Tactic:
apply Nat.le_add_left

Result:
no goals

Proof state:
α : 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.find h').succ x

Tactic:
let p := fun i : ℕ => (Fix.approx f i x).Dom

Result:
α : 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.find h').succ x

Proof state:
case 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' : α), ⋯.fix (fixAux f) z x' = Fix.approx f n.succ x'
z : Upto p
_this : p (n + 1 + ↑z)
hk : Nat.find h' = n + 1 + ↑z
x' : α
⊢ ⋯.fix (fixAux f) z x' = Fix.approx f (n + 1).succ x'

Tactic:
rw [Fix.approx, WellFounded.fix_eq, fixAux]

Result:
case 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' : α), ⋯.fix (fixAux f) z x' = Fix.approx f n.succ x'
z : Upto p
_this : p (n + 1 + ↑z)
hk : Nat.find h' = n + 1 + ↑z
x' : α
⊢ f (fun x_1 => assert (¬(Fix.approx f (↑z) x).Dom) fun h => ⋯.fix (fixAux f) (z.succ h) x_1) x' =
    f (Fix.approx f (n + 1)) x'

Proof state:
α : 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 → ⋯.fix (fixAux f) z x = Fix.approx f (k + 1) x

Tactic:
intro _this hk

Result:
α : 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
⊢ ⋯.fix (fixAux f) z x = Fix.approx f (k + 1) x