awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
hh :
  ∃ (i : ℕ),
    Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
y : β a
h₁ :
  Membership.mem (γ := Part (β a))
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
      (Nat.find (p := fun (n : ℕ) ↦
          Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀).succ
      a)
    y
⊢ Membership.mem (γ := Part (β a))
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
      (Nat.find (p := fun (n : ℕ) ↦
          Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀).succ
      a)
    b
have pos : y = b
Tactic: suffices y = b by
      subst this
      exact h₁
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
hh :
  ∃ (i : ℕ),
    Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
y : β a
h₁ :
  Membership.mem (γ := Part (β a))
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
      (Nat.find (p := fun (n : ℕ) ↦
          Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀).succ
      a)
    y
⊢ y = b
have pos : ∀ (i : ℕ)
  (hh :
    Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b),
  y = b
Tactic: obtain ⟨i, hh⟩ := hh
Cleared hypotheses: hh
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
y : β a
h₁ :
  Membership.mem (γ := Part (β a))
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
      (Nat.find (p := fun (n : ℕ) ↦
          Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀).succ
      a)
    y
i : ℕ
hh : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
⊢ y = b
have pos : ∀
  (h₁ :
    Membership.mem (γ := Part (β a))
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
        (Nat.find (p := fun (n : ℕ) ↦
            Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a))
            h₀).succ
        a)
      y),
  y = b
Tactic: revert h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
y : β a
i : ℕ
hh : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
⊢ ∀
    (h₁ :
      Membership.mem (γ := Part (β a))
        (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
          (Nat.find (p := fun (n : ℕ) ↦
              Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a))
              h₀).succ
          a)
        y),
    y = b
have pos : ∀ (j : ℕ)
  (h₁ :
    Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) y),
  y = b
Tactic: generalize succ (Nat.find h₀) = j
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
y : β a
i : ℕ
hh : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
j : ℕ
h₁ : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) y
⊢ y = b
have pos : ∀
  (this :
    ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a)
      (h₀ :
        ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a))
      (y : β a) (i : ℕ)
      (hh :
        Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
          b)
      (j : ℕ)
      (h₁ :
        Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a)
          y)
      (case : i ≤ j), y = b)
  (case : ¬i ≤ j), y = b
Tactic: wlog case : i ≤ j
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
y : β a
i : ℕ
hh : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
j : ℕ
h₁ : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) y
pos :
  ∀
    (this :
      ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a)
        (h₀ :
          ∃ (i : ℕ),
            Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a))
        (y : β a) (i : ℕ)
        (hh :
          Membership.mem (γ := Part (β a))
            (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b)
        (j : ℕ)
        (h₁ :
          Membership.mem (γ := Part (β a))
            (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) y)
        (case : i ≤ j), y = b)
    (case : ¬i ≤ j), y = b
⊢ y = b
have wlog : ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a)
  (h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a))
  (y : β a) (i : ℕ)
  (hh :
    Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b)
  (j : ℕ)
  (h₁ :
    Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) y)
  (case : i ≤ j), y = b
Tactic: wlog case : i ≤ j
Cleared hypotheses: a, b, h₀, y, i, hh, j, h₁
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
y : β a
i : ℕ
hh : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
j : ℕ
h₁ : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) y
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a)
    (h₀ :
      ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a))
    (y : β a) (i : ℕ)
    (hh :
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b)
    (j : ℕ)
    (h₁ :
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) y)
    (case : i ≤ j), y = b
case : ¬i ≤ j
⊢ y = b
have pos : ∀ (H : i ≤ j), y = b
Tactic: rcases le_total i j with H | H
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
y : β a
i : ℕ
hh : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
j : ℕ
h₁ : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) y
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a)
    (h₀ :
      ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a))
    (y : β a) (i : ℕ)
    (hh :
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b)
    (j : ℕ)
    (h₁ :
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) y)
    (case : i ≤ j), y = b
case : ¬i ≤ j
pos : ∀ (H : i ≤ j), y = b
⊢ y = b
have pos₁ : ∀ (H : j ≤ i), y = b
Tactic: rcases le_total i j with H | H
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
y : β a
i : ℕ
hh : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
j : ℕ
h₁ : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) y
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a)
    (h₀ :
      ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a))
    (y : β a) (i : ℕ)
    (hh :
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b)
    (j : ℕ)
    (h₁ :
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) y)
    (case : i ≤ j), y = b
case : ¬i ≤ j
H : j ≤ i
⊢ y = b
have pos : b = y
Tactic: symm
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
y : β a
i : ℕ
hh : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
j : ℕ
h₁ : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) y
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a)
    (h₀ :
      ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a))
    (y : β a) (i : ℕ)
    (hh :
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b)
    (j : ℕ)
    (h₁ :
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) y)
    (case : i ≤ j), y = b
case : ¬i ≤ j
⊢ y = b
have pos : ∀ (H : i ≤ j), y = b
Tactic: rcases le_total i j with H | H <;> [skip; symm]
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
y : β a
i : ℕ
hh : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
j : ℕ
h₁ : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) y
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a)
    (h₀ :
      ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a))
    (y : β a) (i : ℕ)
    (hh :
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b)
    (j : ℕ)
    (h₁ :
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) y)
    (case : i ≤ j), y = b
case : ¬i ≤ j
pos : ∀ (H : i ≤ j), y = b
⊢ y = b
have pos₁ : ∀ (H : j ≤ i), b = y
Tactic: rcases le_total i j with H | H <;> [skip; symm]
-- Lean 4 proof step from Mathlib.Control.LawfulFix (hypothesis)
Goal:
α_1 : Type u_1
β_1 : α_1 → Type u_2
f_1 : ((a : α_1) → Part (β_1 a)) →o (a : α_1) → Part (β_1 a)
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
y : β a
i : ℕ
hh : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
j : ℕ
h₁ : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) y
case : i ≤ j
⊢ y = b
have hh₁ : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) b
Tactic: replace hh := approx_mono f case _ _ hh
Cleared hypotheses: hh
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ¬∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
⊢ Membership.mem (γ := Part (β a)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) a) b ↔
    ∃ (i : ℕ),
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
have neg : ∀ (x : ℕ), b ∉ approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x a
Tactic: simp only [fix_def' (⇑f) h₀, not_exists, false_iff, notMem_none]
-- Lean 4 proof step from Mathlib.Control.LawfulFix (hypothesis)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ¬∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
⊢ ∀ (x : ℕ), b ∉ approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x a
have h₁ : ∀ (x : ℕ) (x_1 : β a), x_1 ∉ approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x a
Tactic: simp only [dom_iff_mem, not_exists] at h₀
Cleared hypotheses: h₀
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
⊢ Membership.mem (γ := Part (β a)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) a) b ↔
    ∃ (i : ℕ),
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
have pos : ∀ (h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)),
  Membership.mem (γ := Part (β a)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) a) b ↔
    ∃ (i : ℕ),
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
Tactic: classical
  by_cases h₀ : ∃ i : ℕ, (approx f i a).Dom
  · simp only [Part.fix_def f h₀]
    constructor <;> intro hh
    · exact ⟨_, hh⟩
    have h₁ := Nat.find_spec h₀
    rw [dom_iff_mem] at h₁
    obtain ⟨y, h₁⟩ := h₁
    replace h₁ := approx_mono' f _ _ h₁
    suffices y = b by
      subst this
      exact h₁
    obtain ⟨i, hh⟩ := hh
    revert h₁; generalize succ (Nat.find h₀) = j; intro h₁
    wlog case : i ≤ j
    · rcases le_total i j with H | H <;> [skip; symm] <;> apply_assumption <;> assumption
    replace hh := approx_mono f case _ _ hh
    apply Part.mem_unique h₁ hh
  · simp only [fix_def' (⇑f) h₀, not_exists, false_iff, notMem_none]
    simp only [dom_iff_mem, not_exists] at h₀
    intro; apply h₀
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
pos :
  ∀
    (h₀ :
      ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)),
    Membership.mem (γ := Part (β a)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) a) b ↔
      ∃ (i : ℕ),
        Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
          b
⊢ Membership.mem (γ := Part (β a)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) a) b ↔
    ∃ (i : ℕ),
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
have neg : ∀
  (h₀ :
    ¬∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)),
  Membership.mem (γ := Part (β a)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) a) b ↔
    ∃ (i : ℕ),
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
Tactic: classical
  by_cases h₀ : ∃ i : ℕ, (approx f i a).Dom
  · simp only [Part.fix_def f h₀]
    constructor <;> intro hh
    · exact ⟨_, hh⟩
    have h₁ := Nat.find_spec h₀
    rw [dom_iff_mem] at h₁
    obtain ⟨y, h₁⟩ := h₁
    replace h₁ := approx_mono' f _ _ h₁
    suffices y = b by
      subst this
      exact h₁
    obtain ⟨i, hh⟩ := hh
    revert h₁; generalize succ (Nat.find h₀) = j; intro h₁
    wlog case : i ≤ j
    · rcases le_total i j with H | H <;> [skip; symm] <;> apply_assumption <;> assumption
    replace hh := approx_mono f case _ _ hh
    apply Part.mem_unique h₁ hh
  · simp only [fix_def' (⇑f) h₀, not_exists, false_iff, notMem_none]
    simp only [dom_iff_mem, not_exists] at h₀
    intro; apply h₀
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
a : α
b : β a
hh : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
⊢ Membership.mem (γ := Part (β a)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) a) b
have rw : ∃ (i : ℕ),
  Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
Tactic: rw [mem_iff f]
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
⊢ ∃ (i : ℕ),
    LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
have pos : ∀
  (hh :
    ∃ (i : ℕ) (b : β x),
      Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
        b),
  ∃ (i : ℕ),
    LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
Tactic: by_cases! hh : ∃ i b, b ∈ approx f i x
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
pos :
  ∀
    (hh :
      ∃ (i : ℕ) (b : β x),
        Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
          b),
    ∃ (i : ℕ),
      LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
        (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
⊢ ∃ (i : ℕ),
    LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
have neg : ∀ (hh : ∀ (i : ℕ) (b : β x), b ∉ approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x),
  ∃ (i : ℕ),
    LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
Tactic: by_cases! hh : ∃ i b, b ∈ approx f i x
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh :
  ∃ (i : ℕ) (b : β x),
    Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x) b
⊢ ∃ (i : ℕ),
    LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
have pos : ∀ (i : ℕ) (b : β x)
  (hb :
    Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x) b),
  ∃ (i : ℕ),
    LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
Tactic: rcases hh with ⟨i, b, hb⟩
Cleared hypotheses: hh
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b : β x
hb : Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x) b
⊢ ∃ (i : ℕ),
    LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
have pos : LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
  (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
Tactic: exists i
-- Lean 4 proof step from Mathlib.Control.LawfulFix (hypothesis)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b : β x
hb : Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x) b
b' : β x
h' : Membership.mem (γ := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x) b'
⊢ Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x) b'
have hb' : Membership.mem (γ := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x) b
Tactic: have hb' := approx_le_fix f i _ _ hb
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (i : ℕ) (b : β x), b ∉ approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x
⊢ ∃ (i : ℕ),
    LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
have neg : LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
  (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) 0 x)
Tactic: exists 0