-- 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:
α : 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 < Nat.find h'

Tactic:
rw [hk, Nat.succ_add_eq_add_succ]

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
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 < n + (↑z).succ

Proof state:
case 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' = 0 + ↑z
x' x : α
⊢ ¬¬(Fix.approx f (↑z) x✝).Dom

Tactic:
simpa only [not_not, Coe]

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
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✝ : α
⊢ ¬(Fix.approx f (↑z) x).Dom

Tactic:
apply Nat.find_min 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
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 < Nat.find h'

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

Tactic:
ext : 1

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

Tactic:
congr

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

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

Tactic:
rw [Nat.zero_add] at _this

Result:
case 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' = 0 + ↑z
x' x : α
⊢ ¬¬(Fix.approx f (↑z) x✝).Dom

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
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 < n + (↑z).succ

Tactic:
apply Nat.lt_of_succ_le

Result:
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

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 + 1 + ↑z)
hk : Nat.find h' = n + 1 + ↑z
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 [succ_add_eq_add_succ] at _this hk

Result:
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✝