awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : α
hh : ∀ (i : ℕ) (b : β x), b ∉ approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x
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)) 0 x) b'
have h'₁ : ∃ (i : ℕ),
  Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x) b'
Tactic: simp only [mem_iff f] 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)
x : α
hh : ∀ (i : ℕ) (b : β x), b ∉ approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x
b' : β x
h' :
  ∃ (i : ℕ),
    Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x) b'
⊢ Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) 0 x) b'
have neg : ∀ (i : ℕ)
  (h' :
    Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x) b'),
  Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) 0 x) b'
Tactic: obtain ⟨i, h'⟩ := 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)
x : (a : α) → Part (β a)
⊢ x ∈ approxChain (β := β) f → x ≤ (f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x
have simp : ∀ (x_1 : ℕ) (h : x = (approxChain (β := β) f : (a : ℕ) → (a : α) → Part (β a)) x_1),
  x ≤ (f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x
Tactic: simp only [Membership.mem, forall_exists_index]
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) = ωSup (approxChain (β := β) f)
have a : Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) ≤ ωSup (approxChain (β := β) f)
Tactic: apply le_antisymm
-- 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 : Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) ≤ ωSup (approxChain (β := β) f)
⊢ Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) = ωSup (approxChain (β := β) f)
have a₁ : ωSup (approxChain (β := β) f) ≤ Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
Tactic: apply le_antisymm
-- 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 : α
⊢ Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x ≤ ωSup (approxChain (β := β) f) x
have a : ∀ (i : ℕ)
  (hx :
    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)),
  Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x ≤ ωSup (approxChain (β := β) f) x
Tactic: obtain ⟨i, hx⟩ := exists_fix_le_approx f 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 : α
i : ℕ
hx :
  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)
⊢ Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x ≤ ωSup (approxChain (β := β) f) x
have trans : 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.succ x)
Tactic: trans approx f i.succ 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 : α
i : ℕ
hx :
  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)
trans :
  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.succ x)
⊢ Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x ≤ ωSup (approxChain (β := β) f) x
have trans₁ : approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i.succ x ≤ ωSup (approxChain (β := β) f) x
Tactic: trans approx f i.succ 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 : α
i : ℕ
hx trans :
  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)
⊢ 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.succ x)
have trans₁ : LE.le.{u_2} (α := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
  (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i.succ x)
Tactic: trans
-- 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 : ℕ
hx trans :
  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)
trans₁ :
  LE.le.{u_2} (α := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i.succ x)
⊢ 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.succ x)
have trans₂ : Part (β x)
Tactic: trans
-- 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 : ℕ
hx :
  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)
⊢ approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i.succ x ≤ ωSup (approxChain (β := β) f) x
have apply : LE.le.{u_2} (α := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i.succ x)
  (((approxChain (β := β) f).map (Pi.evalOrderHom (π := fun (a : α) ↦ Part (β a)) x) : (a : ℕ) → Part (β x)) i.succ)
Tactic: apply le_ωSup_of_le i.succ
-- 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 : ℕ
hx :
  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)
⊢ LE.le.{u_2} (α := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i.succ x)
    (((approxChain (β := β) f).map (Pi.evalOrderHom (π := fun (a : α) ↦ Part (β a)) x) : (a : ℕ) → Part (β x)) i.succ)
have dsimp : LE.le.{u_2} (α := Part (β x))
  ((f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i) x :
    Part (β x))
  ((f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i) x :
    Part (β x))
Tactic: dsimp [approx]
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ ωSup (approxChain (β := β) f) ≤ Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
have apply : ∀ (i : ℕ),
  LE.le (α := (x : α) → Part (β x)) ((approxChain (β := β) f : (a : ℕ) → (x : α) → Part (β x)) i : (x : α) → Part (β x))
    (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) : (x : α) → Part (β x))
Tactic: apply ωSup_le _ _ _
-- 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 : (a : α) → Part (β a)
hX : (f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) X ≤ X
⊢ Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) ≤ X
have rw : ωSup (approxChain (β := β) f) ≤ X
Tactic: rw [fix_eq_ωSup 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 : (a : α) → Part (β a)
hX : (f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) X ≤ X
⊢ ωSup (approxChain (β := β) f) ≤ X
have apply : ∀ (i : ℕ), (approxChain (β := β) f : (a : ℕ) → (x : α) → Part (β x)) i ≤ X
Tactic: apply ωSup_le _ _ _
-- 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 : (a : α) → Part (β a)
hX : (f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) X ≤ X
n : ℕ
i_ih :
  ({ toFun := approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)), monotone' := ⋯ :
          Chain ((a : α) → Part (β a)) } :
        (a : ℕ) → (x : α) → Part (β x))
      n ≤
    X
⊢ ({ toFun := approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)), monotone' := ⋯ :
          Chain ((a : α) → Part (β a)) } :
        (a : ℕ) → (x : α) → Part (β x))
      (n + 1) ≤
    X
have trans : LE.le (α := (x : α) → Part (β x))
  (({ toFun := approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)), monotone' := sorry :
          Chain ((a : α) → Part (β a)) } :
        (a : ℕ) → (x : α) → Part (β x))
      (n + 1) :
    (x : α) → Part (β x))
  ((f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) X : (a : α) → Part (β a))
Tactic: trans f 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 : (a : α) → Part (β a)
hX : (f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) X ≤ X
i : ℕ
⊢ ({ toFun := approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)), monotone' := ⋯ :
          Chain ((a : α) → Part (β a)) } :
        (a : ℕ) → (x : α) → Part (β x))
      i ≤
    X
have zero : ({ toFun := approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)), monotone' := sorry :
        Chain ((a : α) → Part (β a)) } :
      (a : ℕ) → (x : α) → Part (β x))
    0 ≤
  X
Tactic: induction i with
  | zero => dsimp [Fix.approx]; apply bot_le
  | succ _ i_ih =>
    trans f X
    · apply f.monotone i_ih
    · apply hX
Cleared hypotheses: i
-- 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 : (a : α) → Part (β a)
hX : (f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) X ≤ X
i : ℕ
zero :
  ({ toFun := approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)), monotone' := ⋯ :
          Chain ((a : α) → Part (β a)) } :
        (a : ℕ) → (x : α) → Part (β x))
      0 ≤
    X
⊢ ({ toFun := approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)), monotone' := ⋯ :
          Chain ((a : α) → Part (β a)) } :
        (a : ℕ) → (x : α) → Part (β x))
      i ≤
    X
have succ : ∀ (n : ℕ)
  (i_ih :
    ({ toFun := approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)), monotone' := sorry :
            Chain ((a : α) → Part (β a)) } :
          (a : ℕ) → (x : α) → Part (β x))
        n ≤
      X),
  ({ toFun := approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)), monotone' := sorry :
          Chain ((a : α) → Part (β a)) } :
        (a : ℕ) → (x : α) → Part (β x))
      (n + 1) ≤
    X
Tactic: induction i with
  | zero => dsimp [Fix.approx]; apply bot_le
  | succ _ i_ih =>
    trans f X
    · apply f.monotone i_ih
    · apply hX
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ Part.fix (β := β) g =
    ωSup (approxChain (β := β) { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) })
have rw : Part.fix (β := β) g =
  Part.fix (β := β)
    (⇑{ toFun := g, monotone' := sorry : ((a : α) → Part (β a)) →o (a : α) → Part (β a) } :
      (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
Tactic: rw [← fix_eq_ωSup]
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ Part.fix (β := β) g = g (Part.fix (β := β) g)
have rw : ωSup (approxChain (β := β) { toFun := g, monotone' := sorry : ((a : α) → Part (β a)) →o (a : α) → Part (β a) }) =
  ωSup
    ((approxChain (β := β) { toFun := g, monotone' := sorry : ((a : α) → Part (β a)) →o (a : α) → Part (β a) }).map
      { toFun := g, monotone' := sorry : ((a : α) → Part (β a)) →o (a : α) → Part (β a) })
Tactic: rw [fix_eq_ωSup_of_ωScottContinuous hc, hc.map_ωSup]
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ ωSup (approxChain (β := β) { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) }) =
    ωSup
      ((approxChain (β := β) { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) }).map
        { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) })
have a : ωSup (approxChain (β := β) { toFun := g, monotone' := sorry : ((a : α) → Part (β a)) →o (a : α) → Part (β a) }) ≤
  ωSup
    ((approxChain (β := β) { toFun := g, monotone' := sorry : ((a : α) → Part (β a)) →o (a : α) → Part (β a) }).map
      { toFun := g, monotone' := sorry : ((a : α) → Part (β a)) →o (a : α) → Part (β a) })
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
a :
  ωSup (approxChain (β := β) { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) }) ≤
    ωSup
      ((approxChain (β := β) { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) }).map
        { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) })
⊢ ωSup (approxChain (β := β) { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) }) =
    ωSup
      ((approxChain (β := β) { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) }).map
        { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) })
have a₁ : ωSup
    ((approxChain (β := β) { toFun := g, monotone' := sorry : ((a : α) → Part (β a)) →o (a : α) → Part (β a) }).map
      { toFun := g, monotone' := sorry : ((a : α) → Part (β a)) →o (a : α) → Part (β a) }) ≤
  ωSup (approxChain (β := β) { toFun := g, monotone' := sorry : ((a : α) → Part (β a)) →o (a : α) → Part (β a) })
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ ωSup (approxChain (β := β) { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) }) ≤
    ωSup
      ((approxChain (β := β) { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) }).map
        { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) })
have apply : approxChain (β := β) { toFun := g, monotone' := sorry : ((a : α) → Part (β a)) →o (a : α) → Part (β a) } ≤
  (approxChain (β := β) { toFun := g, monotone' := sorry : ((a : α) → Part (β a)) →o (a : α) → Part (β a) }).map
    { toFun := g, monotone' := sorry }
Tactic: apply ωSup_le_ωSup_of_le _
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
i : ℕ
⊢ ∃ (j : ℕ),
    LE.le (α := (x : α) → Part (β x))
      ((approxChain (β := β) { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) } :
            (a : ℕ) → (x : α) → Part (β x))
          i :
        (x : α) → Part (β x))
      (((approxChain (β := β) { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) }).map
              { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) } :
            (a : ℕ) → (x : α) → Part (β x))
          j :
        (x : α) → Part (β x))
have exists : LE.le (α := (x : α) → Part (β x))
  ((approxChain (β := β) { toFun := g, monotone' := sorry : ((a : α) → Part (β a)) →o (a : α) → Part (β a) } :
        (a : ℕ) → (x : α) → Part (β x))
      i :
    (x : α) → Part (β x))
  (((approxChain (β := β) { toFun := g, monotone' := sorry : ((a : α) → Part (β a)) →o (a : α) → Part (β a) }).map
          { toFun := g, monotone' := sorry : ((a : α) → Part (β a)) →o (a : α) → Part (β a) } :
        (a : ℕ) → (x : α) → Part (β x))
      i :
    (x : α) → Part (β x))
Tactic: exists i
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ ωSup
      ((approxChain (β := β) { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) }).map
        { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) }) ≤
    ωSup (approxChain (β := β) { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) })
have apply : (approxChain (β := β) { toFun := g, monotone' := sorry : ((a : α) → Part (β a)) →o (a : α) → Part (β a) }).map
    { toFun := g, monotone' := sorry : ((a : α) → Part (β a)) →o (a : α) → Part (β a) } ≤
  approxChain (β := β) { toFun := g, monotone' := sorry }
Tactic: apply ωSup_le_ωSup_of_le _
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
i : ℕ
⊢ ∃ (j : ℕ),
    LE.le (α := (x : α) → Part (β x))
      (((approxChain (β := β) { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) }).map
              { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) } :
            (a : ℕ) → (x : α) → Part (β x))
          i :
        (x : α) → Part (β x))
      ((approxChain (β := β) { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) } :
            (a : ℕ) → (x : α) → Part (β x))
          j :
        (x : α) → Part (β x))
have exists : LE.le (α := (x : α) → Part (β x))
  (((approxChain (β := β) { toFun := g, monotone' := sorry : ((a : α) → Part (β a)) →o (a : α) → Part (β a) }).map
          { toFun := g, monotone' := sorry : ((a : α) → Part (β a)) →o (a : α) → Part (β a) } :
        (a : ℕ) → (x : α) → Part (β x))
      i :
    (x : α) → Part (β x))
  (((approxChain (β := β) { toFun := g, monotone' := sorry : ((a : α) → Part (β a)) →o (a : α) → Part (β a) }).map
          { toFun := g, monotone' := sorry : ((a : α) → Part (β a)) →o (a : α) → Part (β a) } :
        (a : ℕ) → (x : α) → Part (β x))
      i :
    (x : α) → Part (β x))
Tactic: exists i.succ
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
f : Part α → Part α
hc : ωScottContinuous f
x : Chain (Unit → Part α)
⊢ (toUnitMono { toFun := f, monotone' := ⋯ : Part α →o Part α } : (a : Unit → Part α) → Unit → Part α) (ωSup x) =
    ωSup (x.map (toUnitMono { toFun := f, monotone' := ⋯ : Part α →o Part α }))
have h : (toUnitMono { toFun := f, monotone' := sorry : Part α →o Part α } : (a : Unit → Part α) → Unit → Part α) (ωSup x)
    PUnit.unit =
  ωSup (x.map (toUnitMono { toFun := f, monotone' := sorry : Part α →o Part α })) PUnit.unit
Tactic: ext ⟨⟩ : 1
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
f : Part α → Part α
hc : ωScottContinuous f
x : Chain (Unit → Part α)
⊢ (toUnitMono { toFun := f, monotone' := ⋯ : Part α →o Part α } : (a : Unit → Part α) → Unit → Part α) (ωSup x)
      PUnit.unit =
    ωSup (x.map (toUnitMono { toFun := f, monotone' := ⋯ : Part α →o Part α })) PUnit.unit
have h : f (Part.ωSup (x.map (Pi.evalOrderHom (π := fun (a : Unit) ↦ Part α) PUnit.unit))) =
  Part.ωSup
    ((x.map (toUnitMono { toFun := f, monotone' := sorry : Part α →o Part α })).map
      (Pi.evalOrderHom (π := fun (a : Unit) ↦ Part α) PUnit.unit))
Tactic: dsimp [OmegaCompletePartialOrder.ωSup]
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
f : Part α → Part α
hc : ωScottContinuous f
x : Chain (Unit → Part α)
⊢ f (Part.ωSup (x.map (Pi.evalOrderHom (π := fun (a : Unit) ↦ Part α) PUnit.unit))) =
    Part.ωSup
      ((x.map (toUnitMono { toFun := f, monotone' := ⋯ : Part α →o Part α })).map
        (Pi.evalOrderHom (π := fun (a : Unit) ↦ Part α) PUnit.unit))
have h : ωSup
    ((x.map (Pi.evalOrderHom (π := fun (a : Unit) ↦ Part α) PUnit.unit)).map
      { toFun := f, monotone' := sorry : Part α →o Part α }) =
  Part.ωSup
    ((x.map (toUnitMono { toFun := f, monotone' := sorry : Part α →o Part α })).map
      (Pi.evalOrderHom (π := fun (a : Unit) ↦ Part α) PUnit.unit))
Tactic: erw [hc.map_ωSup]
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
f : Part α → Part α
hc : ωScottContinuous f
x : Chain (Unit → Part α)
⊢ ωSup
      ((x.map (Pi.evalOrderHom (π := fun (a : Unit) ↦ Part α) PUnit.unit)).map
        { toFun := f, monotone' := ⋯ : Part α →o Part α }) =
    Part.ωSup
      ((x.map (toUnitMono { toFun := f, monotone' := ⋯ : Part α →o Part α })).map
        (Pi.evalOrderHom (π := fun (a : Unit) ↦ Part α) PUnit.unit))
have h : ωSup
    (x.map
      ({ toFun := f, monotone' := sorry : Part α →o Part α }.comp
        (Pi.evalOrderHom (π := fun (a : Unit) ↦ Part α) PUnit.unit))) =
  Part.ωSup
    ((x.map (toUnitMono { toFun := f, monotone' := sorry : Part α →o Part α })).map
      (Pi.evalOrderHom (π := fun (a : Unit) ↦ Part α) PUnit.unit))
Tactic: rw [Chain.map_comp]
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : Part α → Part α
hc : ωScottContinuous f
⊢ Part.fix (β := fun (a : Unit) ↦ α)
      (⇑(toUnitMono { toFun := f, monotone' := ⋯ : Part α →o Part α }) : (a : Unit → Part α) → Unit → Part α) () =
    f (Fix.fix f)
have rw : (toUnitMono { toFun := f, monotone' := sorry : Part α →o Part α } : (a : Unit → Part α) → Unit → Part α)
    (Part.fix (β := fun (a : Unit) ↦ α)
      (⇑(toUnitMono { toFun := f, monotone' := sorry : Part α →o Part α }) : (a : Unit → Part α) → Unit → Part α))
    () =
  f (Fix.fix f)
Tactic: rw [Part.fix_eq_of_ωScottContinuous (ωScottContinuous_toUnitMono f hc)]