awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Control.Fix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
z : Upto p
_this : p (0 + (↑z : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = 0 + (↑z : ℕ)
x' : α
hwf : WellFounded fun (y x : Upto p) ↦ x < y
⊢ f
      (fun (x : α) ↦
        assert (¬p (↑z : ℕ)) fun (h : ¬p (↑z : ℕ)) ↦
          hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
            (fixAux (β := β) f (p := p)) (z.succ (p := p) h) x)
      x' =
    f (Fix.approx (β := β) f 0) x'
have zero : (fun (x : α) ↦
    assert (¬p (↑z : ℕ)) fun (h : ¬p (↑z : ℕ)) ↦
      hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) (z.succ (p := p) h) x) =
  Fix.approx (β := β) f 0
Tactic: congr
-- Lean 4 proof step from Mathlib.Control.Fix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
z : Upto p
_this : p (0 + (↑z : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = 0 + (↑z : ℕ)
x' : α
hwf : WellFounded fun (y x : Upto p) ↦ x < y
⊢ (fun (x : α) ↦
      assert (¬p (↑z : ℕ)) fun (h : ¬p (↑z : ℕ)) ↦
        hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
          (fixAux (β := β) f (p := p)) (z.succ (p := p) h) x) =
    Fix.approx (β := β) f 0
have zero : ∀ (x : α),
  (assert (¬p (↑z : ℕ)) fun (h : ¬p (↑z : ℕ)) ↦
      hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) (z.succ (p := p) h) x) =
    Fix.approx (β := β) f 0 x
Tactic: ext x : 1
-- Lean 4 proof step from Mathlib.Control.Fix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x_1 : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x_1).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x_1).Dom
z : Upto p
_this : p (0 + (↑z : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x_1).Dom) h' = 0 + (↑z : ℕ)
x' : α
hwf : WellFounded fun (y x : Upto p) ↦ x < y
x : α
⊢ (assert (¬p (↑z : ℕ)) fun (h : ¬p (↑z : ℕ)) ↦
      hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) (z.succ (p := p) h) x) =
    Fix.approx (β := β) f 0 x
have zero : none = Fix.approx (β := β) f 0 x
Tactic: rw [assert_neg]
-- Lean 4 proof step from Mathlib.Control.Fix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x_1 : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x_1).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x_1).Dom
z : Upto p
_this : p (0 + (↑z : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x_1).Dom) h' = 0 + (↑z : ℕ)
x' : α
hwf : WellFounded fun (y x : Upto p) ↦ x < y
x : α
zero : none = Fix.approx (β := β) f 0 x
⊢ (assert (¬p (↑z : ℕ)) fun (h : ¬p (↑z : ℕ)) ↦
      hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) (z.succ (p := p) h) x) =
    Fix.approx (β := β) f 0 x
have zero₁ : ¬¬p (↑z : ℕ)
Tactic: rw [assert_neg]
-- Lean 4 proof step from Mathlib.Control.Fix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x_1 : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x_1).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x_1).Dom
z : Upto p
_this : p (0 + (↑z : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x_1).Dom) h' = 0 + (↑z : ℕ)
x' : α
hwf : WellFounded fun (y x : Upto p) ↦ x < y
x : α
⊢ ¬¬p (↑z : ℕ)
have zero : ∀ (_this : p (↑z : ℕ)) (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x_1).Dom) h' = 0 + (↑z : ℕ))
  (x' : α), (WellFounded fun (y x : Upto p) ↦ x < y) → ∀ (x : α), ¬¬p (↑z : ℕ)
Tactic: rw [Nat.zero_add] at _this
Cleared hypotheses: _this, hk, x', hwf, x
-- Lean 4 proof step from Mathlib.Control.Fix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p) (_this : p (n + (↑z : ℕ)))
    (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + (↑z : ℕ)) (x' : α)
    (hwf : WellFounded fun (y x : Upto p) ↦ x < y),
    hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) z x' =
      Fix.approx (β := β) f n.succ x'
z : Upto p
_this : p (n + 1 + (↑z : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + 1 + (↑z : ℕ)
x' : α
hwf : WellFounded fun (y x : Upto p) ↦ x < y
⊢ hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y) (fixAux (β := β) f (p := p))
      z x' =
    Fix.approx (β := β) f (n + 1).succ x'
have succ : f
    (fun (x : α) ↦
      assert (¬p (↑z : ℕ)) fun (h : ¬p (↑z : ℕ)) ↦
        hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
          (fixAux (β := β) f (p := p)) (z.succ (p := p) h) x)
    x' =
  f (Fix.approx (β := β) f (n + 1)) x'
Tactic: rw [Fix.approx, WellFounded.fix_eq, fixAux]
-- Lean 4 proof step from Mathlib.Control.Fix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p) (_this : p (n + (↑z : ℕ)))
    (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + (↑z : ℕ)) (x' : α)
    (hwf : WellFounded fun (y x : Upto p) ↦ x < y),
    hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) z x' =
      Fix.approx (β := β) f n.succ x'
z : Upto p
_this : p (n + 1 + (↑z : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + 1 + (↑z : ℕ)
x' : α
hwf : WellFounded fun (y x : Upto p) ↦ x < y
⊢ f
      (fun (x : α) ↦
        assert (¬p (↑z : ℕ)) fun (h : ¬p (↑z : ℕ)) ↦
          hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
            (fixAux (β := β) f (p := p)) (z.succ (p := p) h) x)
      x' =
    f (Fix.approx (β := β) f (n + 1)) x'
have succ : (fun (x : α) ↦
    assert (¬p (↑z : ℕ)) fun (h : ¬p (↑z : ℕ)) ↦
      hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) (z.succ (p := p) h) x) =
  Fix.approx (β := β) f (n + 1)
Tactic: congr
-- Lean 4 proof step from Mathlib.Control.Fix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p) (_this : p (n + (↑z : ℕ)))
    (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + (↑z : ℕ)) (x' : α)
    (hwf : WellFounded fun (y x : Upto p) ↦ x < y),
    hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) z x' =
      Fix.approx (β := β) f n.succ x'
z : Upto p
_this : p (n + 1 + (↑z : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + 1 + (↑z : ℕ)
x' : α
hwf : WellFounded fun (y x : Upto p) ↦ x < y
⊢ (fun (x : α) ↦
      assert (¬p (↑z : ℕ)) fun (h : ¬p (↑z : ℕ)) ↦
        hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
          (fixAux (β := β) f (p := p)) (z.succ (p := p) h) x) =
    Fix.approx (β := β) f (n + 1)
have succ : ∀ (x : α),
  (assert (¬p (↑z : ℕ)) fun (h : ¬p (↑z : ℕ)) ↦
      hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) (z.succ (p := p) h) x) =
    Fix.approx (β := β) f (n + 1) x
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Control.Fix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p) (_this : p (n + (↑z : ℕ)))
    (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + (↑z : ℕ)) (x' : α)
    (hwf : WellFounded fun (y x : Upto p) ↦ x < y),
    hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) z x' =
      Fix.approx (β := β) f n.succ x'
z : Upto p
_this : p (n + 1 + (↑z : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + 1 + (↑z : ℕ)
x' : α
hwf : WellFounded fun (y x : Upto p) ↦ x < y
x_1 : α
⊢ ¬(Fix.approx (β := β) f (↑z : ℕ) x).Dom
have apply : (↑z : ℕ) < Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h'
Tactic: apply Nat.find_min h'
-- Lean 4 proof step from Mathlib.Control.Fix (hypothesis)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p) (_this : p (n + (↑z : ℕ)))
    (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + (↑z : ℕ)) (x' : α)
    (hwf : WellFounded fun (y x : Upto p) ↦ x < y),
    hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) z x' =
      Fix.approx (β := β) f n.succ x'
z : Upto p
_this : p (n + 1 + (↑z : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + 1 + (↑z : ℕ)
x' : α
hwf : WellFounded fun (y x : Upto p) ↦ x < y
x_1 : α
⊢ (assert (¬p (↑z : ℕ)) fun (h : ¬p (↑z : ℕ)) ↦
      hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) (z.succ (p := p) h) x_1) =
    Fix.approx (β := β) f (n + 1) x_1
have hh : ¬(Fix.approx (β := β) f (↑z : ℕ) x).Dom
Tactic: have hh : ¬(Fix.approx f z.val x).Dom := by
      apply Nat.find_min h'
      lia
-- Lean 4 proof step from Mathlib.Control.Fix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p) (_this : p (n + (↑z : ℕ)))
    (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + (↑z : ℕ)) (x' : α)
    (hwf : WellFounded fun (y x : Upto p) ↦ x < y),
    hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) z x' =
      Fix.approx (β := β) f n.succ x'
z : Upto p
_this : p (n + 1 + (↑z : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + 1 + (↑z : ℕ)
x' : α
hwf : WellFounded fun (y x : Upto p) ↦ x < y
x_1 : α
hh : ¬(Fix.approx (β := β) f (↑z : ℕ) x).Dom
⊢ (assert (¬p (↑z : ℕ)) fun (h : ¬p (↑z : ℕ)) ↦
      hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) (z.succ (p := p) h) x_1) =
    Fix.approx (β := β) f (n + 1) x_1
have succ : ∀ (_this : p (n + (↑z : ℕ).succ))
  (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + (↑z : ℕ).succ) (x' : α)
  (hwf : WellFounded fun (y x : Upto p) ↦ x < y) (x_2 : α) (hh : ¬(Fix.approx (β := β) f (↑z : ℕ) x).Dom),
  (assert (¬p (↑z : ℕ)) fun (h : ¬p (↑z : ℕ)) ↦
      hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) (z.succ (p := p) h) x_2) =
    Fix.approx (β := β) f (n + 1) x_2
Tactic: rw [succ_add_eq_add_succ] at _this hk
Cleared hypotheses: _this, hk, x', hwf, x_1, hh
-- Lean 4 proof step from Mathlib.Control.Fix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p) (_this : p (n + (↑z : ℕ)))
    (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + (↑z : ℕ)) (x' : α)
    (hwf : WellFounded fun (y x : Upto p) ↦ x < y),
    hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) z x' =
      Fix.approx (β := β) f n.succ x'
z : Upto p
_this : p (n + (↑z : ℕ).succ)
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + (↑z : ℕ).succ
x' : α
hwf : WellFounded fun (y x : Upto p) ↦ x < y
x_1 : α
hh : ¬(Fix.approx (β := β) f (↑z : ℕ) x).Dom
⊢ (assert (¬p (↑z : ℕ)) fun (h : ¬p (↑z : ℕ)) ↦
      hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) (z.succ (p := p) h) x_1) =
    Fix.approx (β := β) f (n + 1) x_1
have succ : hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y) (fixAux (β := β) f (p := p))
    (z.succ (p := p) hh) x_1 =
  Fix.approx (β := β) f (n + 1) x_1
Tactic: rw [assert_pos hh, n_ih (Upto.succ z hh) _this hk]
-- Lean 4 proof step from Mathlib.Control.Fix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p) (_this : p (n + (↑z : ℕ)))
    (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + (↑z : ℕ)) (x' : α)
    (hwf : WellFounded fun (y x : Upto p) ↦ x < y),
    hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) z x' =
      Fix.approx (β := β) f n.succ x'
z : Upto p
_this : p (n + (↑z : ℕ).succ)
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + (↑z : ℕ).succ
x' : α
hwf : WellFounded fun (y x : Upto p) ↦ x < y
x_1 : α
hh : ¬(Fix.approx (β := β) f (↑z : ℕ) x).Dom
succ :
  hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y) (fixAux (β := β) f (p := p))
      (z.succ (p := p) hh) x_1 =
    Fix.approx (β := β) f (n + 1) x_1
⊢ (assert (¬p (↑z : ℕ)) fun (h : ¬p (↑z : ℕ)) ↦
      hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) (z.succ (p := p) h) x_1) =
    Fix.approx (β := β) f (n + 1) x_1
have succ₁ : Fix.approx (β := β) f n.succ x_1 = Fix.approx (β := β) f (n + 1) x_1
Tactic: rw [assert_pos hh, n_ih (Upto.succ z hh) _this hk]
-- Lean 4 proof step from Mathlib.Control.Fix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
k : ℕ
z : Upto p
_this : p (k + (↑z : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = k + (↑z : ℕ)
⊢ ∀ (x' : α) (hwf : WellFounded fun (y x : Upto p) ↦ x < y),
    hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) z x' =
      Fix.approx (β := β) f k.succ x'
have zero : ∀ (z : Upto p) (_this : p (0 + (↑z : ℕ)))
  (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = 0 + (↑z : ℕ)) (x' : α)
  (hwf : WellFounded fun (y x : Upto p) ↦ x < y),
  hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y) (fixAux (β := β) f (p := p))
      z x' =
    Fix.approx (β := β) f (Nat.succ 0) x'
Tactic: 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'
      lia
    rw [succ_add_eq_add_succ] at _this hk
    rw [assert_pos hh, n_ih (Upto.succ z hh) _this hk]
Cleared hypotheses: k, z, _this, hk
-- Lean 4 proof step from Mathlib.Control.Fix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
k : ℕ
z : Upto p
_this : p (k + (↑z : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = k + (↑z : ℕ)
zero :
  ∀ (z : Upto p) (_this : p (0 + (↑z : ℕ)))
    (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = 0 + (↑z : ℕ)) (x' : α)
    (hwf : WellFounded fun (y x : Upto p) ↦ x < y),
    hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) z x' =
      Fix.approx (β := β) f (Nat.succ 0) x'
⊢ ∀ (x' : α) (hwf : WellFounded fun (y x : Upto p) ↦ x < y),
    hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) z x' =
      Fix.approx (β := β) f k.succ x'
have succ : ∀ (n : ℕ)
  (n_ih :
    ∀ (z : Upto p) (_this : p (n + (↑z : ℕ)))
      (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + (↑z : ℕ)) (x' : α)
      (hwf : WellFounded fun (y x : Upto p) ↦ x < y),
      hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
          (fixAux (β := β) f (p := p)) z x' =
        Fix.approx (β := β) f n.succ x')
  (z : Upto p) (_this : p (n + 1 + (↑z : ℕ)))
  (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + 1 + (↑z : ℕ)) (x' : α)
  (hwf : WellFounded fun (y x : Upto p) ↦ x < y),
  hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y) (fixAux (β := β) f (p := p))
      z x' =
    Fix.approx (β := β) f (n + 1).succ x'
Tactic: 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'
      lia
    rw [succ_add_eq_add_succ] at _this hk
    rw [assert_pos hh, n_ih (Upto.succ z hh) _this hk]
Cleared hypotheses: k, z, _this, hk
-- Lean 4 proof step from Mathlib.Control.Fix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ¬∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
⊢ Eq.{u_2 + 1} (α := Part (β x))
    (assert (∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom) fun (h : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom) ↦
      ⋯.fix (C := fun (y : Upto fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom) ↦ (a : α) → Part (β a)) (r :=
        Upto.GT fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom)
        (fixAux (β := β) f (p := fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom))
        (Upto.zero (p := fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom)) x)
    none
have rw : Eq.{u_2 + 1} (α := Part (β x)) none none
Tactic: rw [assert_neg h']
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
m : Type u → Type u
inst : Monad m
α β : Type u
f : β → α → β
x y : FreeMonoid α
⊢ op (↾flip (List.foldl f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (x * y))) =
    op (↾flip (List.foldl f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x)) *
      op (↾flip (List.foldl f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) y))
have simp : op
    (↾fun (a : β) ↦
      List.foldl f (List.foldl f a ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x))
        ((FreeMonoid.toList : (a : FreeMonoid α) → List α) y)) =
  HMul.hMul (α := Foldl β) (op (↾fun (a : β) ↦ List.foldl f a ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x)))
    (op (↾fun (a : β) ↦ List.foldl f a ((FreeMonoid.toList : (a : FreeMonoid α) → List α) y)))
Tactic: simp only [FreeMonoid.toList_mul, List.foldl_append, Function.flip_def]
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
m : Type u → Type u
inst : Monad m
α β : Type u
f : α → β → β
x x_1 : FreeMonoid α
⊢ ↾flip (List.foldr f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (x * x_1)) =
    ↾flip (List.foldr f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x) *
      ↾flip (List.foldr f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x_1)
have h : ConcreteCategory.hom (FC := TypeCat.Fun)
    (↾flip (List.foldr f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (x * x_1))) =
  ConcreteCategory.hom (FC := TypeCat.Fun)
    (↾flip (List.foldr f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x) *
      ↾flip (List.foldr f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x_1))
Tactic: apply ConcreteCategory.ext
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
m : Type u → Type u
inst : Monad m
α β : Type u
f : α → β → β
x x_1 : FreeMonoid α
⊢ ConcreteCategory.hom (FC := TypeCat.Fun)
      (↾flip (List.foldr f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (x * x_1))) =
    ConcreteCategory.hom (FC := TypeCat.Fun)
      (↾flip (List.foldr f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x) *
        ↾flip (List.foldr f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x_1))
have h : ∀ (x_2 : β),
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾flip (List.foldr f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (x * x_1)))).toFun
      x_2 =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾flip (List.foldr f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x) *
            ↾flip (List.foldr f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x_1))).toFun
      x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
m : Type u → Type u
inst : Monad m
α β : Type u
inst_1 : LawfulMonad m
f : β → α → m β
x y : FreeMonoid α
⊢ op (flip (List.foldlM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (x * y))) =
    op (flip (List.foldlM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x)) *
      op (flip (List.foldlM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) y))
have a : unop (op (flip (List.foldlM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (x * y)))) =
  unop
    (op (flip (List.foldlM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x)) *
      op (flip (List.foldlM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) y)))
Tactic: apply unop_injective
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
m : Type u → Type u
inst : Monad m
α β : Type u
inst_1 : LawfulMonad m
f : β → α → m β
x y : FreeMonoid α
⊢ unop (op (flip (List.foldlM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (x * y)))) =
    unop
      (op (flip (List.foldlM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x)) *
        op (flip (List.foldlM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) y)))
have a : ∀ (x_1 : KleisliCat.mk m β),
  unop (op (flip (List.foldlM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (x * y)))) x_1 =
    unop
      (op (flip (List.foldlM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x)) *
        op (flip (List.foldlM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) y)))
      x_1
Tactic: funext