awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Control.LawfulFix
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)
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))
⊢ 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:
dsimp [approx]

Premises used: Part.Fix.approx
-- Module: Mathlib.Control.LawfulFix
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))
    ((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:
rfl
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
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))
⊢ ωSup (approxChain (β := β) f) ≤ Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))

Tactic:
apply ωSup_le _ _ _

Premises used: OmegaCompletePartialOrder.ωSup_le
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
y : ℕ
x : α
⊢ LE.le.{u_2} (α := (fun (a : α) ↦ Part.{u_2} (β a)) x)
    (({ toFun := approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)), monotone' := ⋯ :
            Chain ((a : α) → Part (β a)) } :
          (a : ℕ) → (x : α) → Part (β x))
        y x :
      Part (β x))
    (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x : Part (β x))

Tactic:
apply approx_le_fix f

Premises used: Part.Fix.approx_le_fix
-- Module: Mathlib.Control.LawfulFix
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
rw : ωSup (approxChain (β := β) f) ≤ X
⊢ Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) ≤ X

Tactic:
rw [fix_eq_ωSup f]

Premises used: Part.fix_eq_ωSup
-- Module: Mathlib.Control.LawfulFix
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
apply : ∀ (i : ℕ), (approxChain (β := β) f : (a : ℕ) → (x : α) → Part (β x)) i ≤ X
⊢ ωSup (approxChain (β := β) f) ≤ X

Tactic:
apply ωSup_le _ _ _

Premises used: OmegaCompletePartialOrder.ωSup_le
-- Module: Mathlib.Control.LawfulFix
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
⊢ ({ toFun := approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)), monotone' := ⋯ :
          Chain ((a : α) → Part (β a)) } :
        (a : ℕ) → (x : α) → Part (β x))
      0 ≤
    X

Tactic:
apply bot_le

Premises used: bot_le
-- Module: Mathlib.Control.LawfulFix
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
trans :
  LE.le (α := (x : α) → Part (β x))
    (({ toFun := approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)), monotone' := ⋯ :
            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))
trans₁ : (f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) X ≤ X
⊢ ({ toFun := approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)), monotone' := ⋯ :
          Chain ((a : α) → Part (β a)) } :
        (a : ℕ) → (x : α) → Part (β x))
      (n + 1) ≤
    X

Tactic:
trans f X

Premises used: DFunLike.coe
-- Module: Mathlib.Control.LawfulFix
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
⊢ LE.le (α := (x : α) → Part (β x))
    (({ toFun := approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)), monotone' := ⋯ :
            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:
apply f.monotone i_ih

Premises used: OrderHom.monotone
-- Module: Mathlib.Control.LawfulFix
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
⊢ (f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) X ≤ X

Tactic:
apply hX
-- Module: Mathlib.Control.LawfulFix
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
succ :
  ∀ (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
⊢ ({ toFun := approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)), monotone' := ⋯ :
          Chain ((a : α) → Part (β a)) } :
        (a : ℕ) → (x : α) → Part (β x))
      i ≤
    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

Premises used: Part.Fix.approx, DFunLike.coe, bot_le
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
rw :
  Part.fix (β := β) g =
    Part.fix (β := β)
      (⇑{ toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) } :
        (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
⊢ Part.fix (β := β) g =
    ωSup (approxChain (β := β) { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) })

Tactic:
rw [← fix_eq_ωSup]

Premises used: Part.fix_eq_ωSup
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ Part.fix (β := β) g =
    Part.fix (β := β)
      (⇑{ toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) } :
        (a : (a : α) → Part (β a)) → (a : α) → Part (β a))

Tactic:
rfl
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
rw :
  ω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) })
⊢ Part.fix (β := β) g = g (Part.fix (β := β) g)

Tactic:
rw [fix_eq_ωSup_of_ωScottContinuous hc, hc.map_ωSup]

Premises used: OmegaCompletePartialOrder.ωScottContinuous.map_ωSup, Part.fix_eq_ωSup_of_ωScottContinuous
-- Module: Mathlib.Control.LawfulFix
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) })
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) }) =
    ωSup
      ((approxChain (β := β) { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) }).map
        { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) })

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
apply :
  approxChain (β := β) { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) } ≤
    (approxChain (β := β) { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) }).map
      { toFun := g, monotone' := ⋯ }
⊢ ω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) })

Tactic:
apply ωSup_le_ωSup_of_le _

Premises used: OmegaCompletePartialOrder.ωSup_le_ωSup_of_le
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
i : ℕ
exists :
  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))
        i :
      (x : α) → Part (β x))
⊢ ∃ (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))

Tactic:
exists i
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
i : ℕ
⊢ 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))
        i :
      (x : α) → Part (β x))

Tactic:
apply le_f_of_mem_approx _ ⟨i, rfl⟩

Premises used: Part.Fix.le_f_of_mem_approx, Exists.intro, rfl
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
apply :
  (approxChain (β := β) { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) }).map
      { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) } ≤
    approxChain (β := β) { toFun := g, monotone' := ⋯ }
⊢ ω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) })

Tactic:
apply ωSup_le_ωSup_of_le _

Premises used: OmegaCompletePartialOrder.ωSup_le_ωSup_of_le
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
i : ℕ
exists exists₁ :
  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) }).map
            { toFun := g, monotone' := ⋯ : ((a : α) → Part (β a)) →o (a : α) → Part (β a) } :
          (a : ℕ) → (x : α) → Part (β x))
        i :
      (x : α) → Part (β x))
⊢ ∃ (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))

Tactic:
exists i.succ

Premises used: Nat.succ
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
f : Part α → Part α
hc : ωScottContinuous f
x : Chain (Unit → Part α)
h :
  (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
⊢ (toUnitMono { toFun := f, monotone' := ⋯ : Part α →o Part α } : (a : Unit → Part α) → Unit → Part α) (ωSup x) =
    ωSup (x.map (toUnitMono { toFun := f, monotone' := ⋯ : Part α →o Part α }))

Tactic:
ext ⟨⟩ : 1
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
f : Part α → Part α
hc : ωScottContinuous f
x : Chain (Unit → Part α)
h :
  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))
⊢ (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

Tactic:
dsimp [OmegaCompletePartialOrder.ωSup]

Premises used: OmegaCompletePartialOrder.ωSup
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
f : Part α → Part α
hc : ωScottContinuous f
x : Chain (Unit → Part α)
h :
  ω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))
⊢ 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))

Tactic:
erw [hc.map_ωSup]

Premises used: OmegaCompletePartialOrder.ωScottContinuous.map_ωSup
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
f : Part α → Part α
hc : ωScottContinuous f
x : Chain (Unit → Part α)
h :
  ωSup
      (x.map
        ({ toFun := f, monotone' := ⋯ : Part α →o Part α }.comp
          (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))
⊢ ω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))

Tactic:
rw [Chain.map_comp]

Premises used: OmegaCompletePartialOrder.Chain.map_comp
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
f : Part α → Part α
hc : ωScottContinuous f
x : Chain (Unit → Part α)
⊢ ωSup
      (x.map
        ({ toFun := f, monotone' := ⋯ : Part α →o Part α }.comp
          (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))

Tactic:
rfl
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : Part α → Part α
hc : ωScottContinuous f
rw :
  (toUnitMono { toFun := f, monotone' := ⋯ : Part α →o Part α } : (a : Unit → Part α) → Unit → Part α)
      (Part.fix (β := fun (a : Unit) ↦ α)
        (⇑(toUnitMono { toFun := f, monotone' := ⋯ : Part α →o Part α }) : (a : Unit → Part α) → Unit → Part α))
      () =
    f (Fix.fix f)
⊢ Part.fix (β := fun (a : Unit) ↦ α)
      (⇑(toUnitMono { toFun := f, monotone' := ⋯ : Part α →o Part α }) : (a : Unit → Part α) → Unit → Part α) () =
    f (Fix.fix f)

Tactic:
rw [Part.fix_eq_of_ωScottContinuous (ωScottContinuous_toUnitMono f hc)]

Premises used: Part.ωScottContinuous_toUnitMono, Part.fix_eq_of_ωScottContinuous
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : Part α → Part α
hc : ωScottContinuous f
⊢ (toUnitMono { toFun := f, monotone' := ⋯ : Part α →o Part α } : (a : Unit → Part α) → Unit → Part α)
      (Part.fix (β := fun (a : Unit) ↦ α)
        (⇑(toUnitMono { toFun := f, monotone' := ⋯ : Part α →o Part α }) : (a : Unit → Part α) → Unit → Part α))
      () =
    f (Fix.fix f)

Tactic:
rfl
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((x : (a : α) × β a) → γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a)))
h :
  ∀ (x : α) (y : β x),
    Eq.{u_3 + 1} (α := γ x y)
      (((monotoneCurry α β γ :
              ((x : (a : α) × β a) → γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) →o
                (a : α) → (b : β a) → γ a b) :
            (a : (x : (a : α) × β a) → γ x.fst x.snd) → (a : α) → (b : β a) → γ a b)
          (ωSup c) x y :
        γ x y)
      (ωSup (c.map (monotoneCurry α β γ)) x y : γ x y)
⊢ Eq (α := (a : α) → (b : β a) → γ a b)
    (((monotoneCurry α β γ :
            ((x : (a : α) × β a) → γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) →o
              (a : α) → (b : β a) → γ a b) :
          (a : (x : (a : α) × β a) → γ x.fst x.snd) → (a : α) → (b : β a) → γ a b)
        (ωSup c) :
      (a : α) → (b : β a) → γ a b)
    (ωSup (c.map (monotoneCurry α β γ)) : (a : α) → (b : β a) → γ a b)

Tactic:
ext x y
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((x : (a : α) × β a) → γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a)))
x : α
y : β x
h :
  ωSup
      (c.map
        (evalOrderHom (π := fun (x : (a : α) × β a) ↦
          γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a)))
          (Sigma.mk (β := fun (a : α) ↦ β a) x y))) =
    ωSup
      (Chain.map (α := (a : β x) → γ x a)
        (Chain.map (α := (a : α) → (b : β a) → γ a b) (c.map (monotoneCurry α β γ))
            (evalOrderHom (π := fun (a : α) ↦ (b : β a) → γ a b) x) :
          Chain ((b : β x) → γ x b))
        (evalOrderHom (π := γ x) y : ((j : β x) → γ x j) →o γ x y))
⊢ Eq.{u_3 + 1} (α := γ x y)
    (((monotoneCurry α β γ :
            ((x : (a : α) × β a) → γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) →o
              (a : α) → (b : β a) → γ a b) :
          (a : (x : (a : α) × β a) → γ x.fst x.snd) → (a : α) → (b : β a) → γ a b)
        (ωSup c) x y :
      γ x y)
    (ωSup (c.map (monotoneCurry α β γ)) x y : γ x y)

Tactic:
dsimp [curry, ωSup]

Premises used: Sigma.curry, OmegaCompletePartialOrder.ωSup
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((x : (a : α) × β a) → γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a)))
x : α
y : β x
h :
  ωSup
      (c.map
        (evalOrderHom (π := fun (x : (a : α) × β a) ↦
          γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a)))
          (Sigma.mk (β := fun (a : α) ↦ β a) x y))) =
    ωSup
      (c.map
        (OrderHom.comp (β := (a : α) → (b : β a) → γ a b)
          (OrderHom.comp (evalOrderHom (π := γ x) y) (evalOrderHom (π := fun (a : α) ↦ (b : β a) → γ a b) x))
          (monotoneCurry α β γ)))
⊢ ωSup
      (c.map
        (evalOrderHom (π := fun (x : (a : α) × β a) ↦
          γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a)))
          (Sigma.mk (β := fun (a : α) ↦ β a) x y))) =
    ωSup
      (Chain.map (α := (a : β x) → γ x a)
        (Chain.map (α := (a : α) → (b : β a) → γ a b) (c.map (monotoneCurry α β γ))
            (evalOrderHom (π := fun (a : α) ↦ (b : β a) → γ a b) x) :
          Chain ((b : β x) → γ x b))
        (evalOrderHom (π := γ x) y : ((j : β x) → γ x j) →o γ x y))

Tactic:
rw [map_comp, map_comp]

Premises used: OmegaCompletePartialOrder.Chain.map_comp