awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
inst_3 : OmegaCompletePartialOrder δ
c : Chain (α →𝒄 β)
c' : Chain α
a : β
⊢ (ωSup (c.map toMono)).toFun (ωSup c') ≤ a ↔ ωSup (c'.map (ωSup (c.map toMono))) ≤ a

Tactic:
simp [(c _).ωScottContinuous.map_ωSup]

Premises used: OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous, OmegaCompletePartialOrder.ωScottContinuous.map_ωSup, DFunLike.coe
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
apply : Monotone.{u_2, u_4} (β := γ) fun (x : α) ↦ (f x : (a : β) → γ) (g x)
apply₁ :
  ∀ (c : Chain α),
    Eq.{u_4 + 1} (α := γ) ((f (ωSup c) : (a : β) → γ) (g (ωSup c)) : γ)
      (ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ }) : γ)
⊢ ωScottContinuous.{u_2, u_4} (β := γ) fun (x : α) ↦ (f x : (a : β) → γ) (g x)

Tactic:
apply ωScottContinuous.of_monotone_map_ωSup ⟨?_, fun c ↦ ?_⟩

Premises used: Exists.intro, OmegaCompletePartialOrder.ωScottContinuous.of_monotone_map_ωSup
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
x y : α
hxy : x ≤ y
⊢ LE.le.{u_4} (α := γ) ((fun (x : α) ↦ ((f x : (a : β) → γ) (g x) : γ)) x)
    ((fun (x : α) ↦ ((f x : (a : β) → γ) (g x) : γ)) y)

Tactic:
OrderHom.apply_mono (hf.monotone hxy) (hg.monotone hxy)

Premises used: OrderHom.apply_mono, OmegaCompletePartialOrder.ωScottContinuous.monotone
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
x y : α
hxy : x ≤ y
⊢ LE.le.{u_4} (α := γ) ((fun (x : α) ↦ ((f x : (a : β) → γ) (g x) : γ)) x)
    ((fun (x : α) ↦ ((f x : (a : β) → γ) (g x) : γ)) y)

Tactic:
exact OrderHom.apply_mono (hf.monotone hxy) (hg.monotone hxy)

Premises used: OrderHom.apply_mono, OmegaCompletePartialOrder.ωScottContinuous.monotone
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
rw :
  Eq.{u_4 + 1} (α := γ)
    ((ωSup (c.map { toFun := f, monotone' := ⋯ : α →o β →𝒄 γ }) : (a : β) → γ)
        (ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β })) :
      γ)
    (ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ }) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((f (ωSup c) : (a : β) → γ) (g (ωSup c)) : γ)
    (ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ }) : γ)

Tactic:
rw [hf.map_ωSup, hg.map_ωSup]

Premises used: OmegaCompletePartialOrder.ωScottContinuous.map_ωSup
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
simp :
  ωSup
      (((c.map { toFun := f, monotone' := ⋯ : α →o β →𝒄 γ }).map toMono).map
        (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β })))) =
    ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ })
⊢ Eq.{u_4 + 1} (α := γ)
    ((ωSup (c.map { toFun := f, monotone' := ⋯ : α →o β →𝒄 γ }) : (a : β) → γ)
        (ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β })) :
      γ)
    (ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ }) : γ)

Tactic:
simp only [ωSup_def, ωSup_apply]

Premises used: OmegaCompletePartialOrder.ContinuousHom.ωSup_apply, OmegaCompletePartialOrder.ContinuousHom.ωSup_def
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
a :
  ωSup
      (((c.map { toFun := f, monotone' := ⋯ : α →o β →𝒄 γ }).map toMono).map
        (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β })))) ≤
    ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ })
a₁ :
  ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ }) ≤
    ωSup
      (((c.map { toFun := f, monotone' := ⋯ : α →o β →𝒄 γ }).map toMono).map
        (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β }))))
⊢ ωSup
      (((c.map { toFun := f, monotone' := ⋯ : α →o β →𝒄 γ }).map toMono).map
        (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β })))) =
    ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ })

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
a :
  ∀ (i : ℕ),
    LE.le (α := γ)
      ((((c.map { toFun := f, monotone' := ⋯ : α →o β →𝒄 γ }).map toMono).map
              (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β }))) :
            (a : ℕ) → γ)
          i :
        γ)
      (ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ }) : γ)
⊢ ωSup
      (((c.map { toFun := f, monotone' := ⋯ : α →o β →𝒄 γ }).map toMono).map
        (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β })))) ≤
    ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ })

Tactic:
apply ωSup_le

Premises used: OmegaCompletePartialOrder.ωSup_le
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i : ℕ
a :
  LE.le.{u_4} (α := γ)
    ((f ((c : (a : ℕ) → α) i) : (a : β) → γ) (ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β })) : γ)
    (ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ }) : γ)
⊢ LE.le (α := γ)
    ((((c.map { toFun := f, monotone' := ⋯ : α →o β →𝒄 γ }).map toMono).map
            (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β }))) :
          (a : ℕ) → γ)
        i :
      γ)
    (ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ }) : γ)

Tactic:
dsimp
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i : ℕ
a :
  ωSup ((c.map { toFun := g, monotone' := ⋯ : α →o β }).map (↑(f ((c : (a : ℕ) → α) i)) : β →o γ)) ≤
    ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ })
⊢ LE.le.{u_4} (α := γ)
    ((f ((c : (a : ℕ) → α) i) : (a : β) → γ) (ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β })) : γ)
    (ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ }) : γ)

Tactic:
rw [(f (c i)).continuous]

Premises used: OmegaCompletePartialOrder.ContinuousHom.continuous, DFunLike.coe
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i : ℕ
a :
  ∀ (i_1 : ℕ),
    LE.le (α := γ)
      (((c.map { toFun := g, monotone' := ⋯ : α →o β }).map (↑(f ((c : (a : ℕ) → α) i)) : β →o γ) : (a : ℕ) → γ) i_1 :
        γ)
      (ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ }) : γ)
⊢ ωSup ((c.map { toFun := g, monotone' := ⋯ : α →o β }).map (↑(f ((c : (a : ℕ) → α) i)) : β →o γ)) ≤
    ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ })

Tactic:
apply ωSup_le

Premises used: OmegaCompletePartialOrder.ωSup_le
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i j : ℕ
a :
  LE.le (α := γ)
    (((c.map { toFun := g, monotone' := ⋯ : α →o β }).map (↑(f ((c : (a : ℕ) → α) i)) : β →o γ) : (a : ℕ) → γ) j : γ)
    ((c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ } : (a : ℕ) → γ) (max i j) : γ)
⊢ LE.le (α := γ)
    (((c.map { toFun := g, monotone' := ⋯ : α →o β }).map (↑(f ((c : (a : ℕ) → α) i)) : β →o γ) : (a : ℕ) → γ) j : γ)
    (ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ }) : γ)

Tactic:
apply le_ωSup_of_le (i ⊔ j)

Premises used: Max.max, OmegaCompletePartialOrder.le_ωSup_of_le
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i j : ℕ
a : f ((c : (a : ℕ) → α) i) ≤ f ((c.toOrderHom : (a : ℕ) → α) (max i j))
a₁ :
  ((c.map { toFun := g, monotone' := ⋯ : α →o β }).toOrderHom : (a : ℕ) → β) j ≤
    g ((c.toOrderHom : (a : ℕ) → α) (max i j))
⊢ LE.le (α := γ)
    (((c.map { toFun := g, monotone' := ⋯ : α →o β }).map (↑(f ((c : (a : ℕ) → α) i)) : β →o γ) : (a : ℕ) → γ) j : γ)
    ((c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ } : (a : ℕ) → γ) (max i j) : γ)

Tactic:
apply apply_mono

Premises used: OmegaCompletePartialOrder.ContinuousHom.apply_mono
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i j : ℕ
⊢ f ((c : (a : ℕ) → α) i) ≤ f ((c.toOrderHom : (a : ℕ) → α) (max i j))

Tactic:
apply hf.monotone (c.monotone le_sup_left)

Premises used: OrderHom.monotone, le_sup_left, OmegaCompletePartialOrder.ωScottContinuous.monotone, OmegaCompletePartialOrder.Chain.toOrderHom
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i j : ℕ
⊢ ((c.map { toFun := g, monotone' := ⋯ : α →o β }).toOrderHom : (a : ℕ) → β) j ≤
    g ((c.toOrderHom : (a : ℕ) → α) (max i j))

Tactic:
apply hg.monotone (c.monotone le_sup_right)

Premises used: OrderHom.monotone, le_sup_right, OmegaCompletePartialOrder.ωScottContinuous.monotone, OmegaCompletePartialOrder.Chain.toOrderHom
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
a :
  ∀ (i : ℕ),
    (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ } : (a : ℕ) → γ) i ≤
      ωSup
        (((c.map { toFun := f, monotone' := ⋯ : α →o β →𝒄 γ }).map toMono).map
          (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β }))))
⊢ ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ }) ≤
    ωSup
      (((c.map { toFun := f, monotone' := ⋯ : α →o β →𝒄 γ }).map toMono).map
        (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β }))))

Tactic:
simp only [ωSup_le_iff]

Premises used: OmegaCompletePartialOrder.ωSup_le_iff
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i : ℕ
a :
  LE.le (α := γ) ((c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ } : (a : ℕ) → γ) i : γ)
    ((((c.map { toFun := f, monotone' := ⋯ : α →o β →𝒄 γ }).map toMono).map
            (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β }))) :
          (a : ℕ) → γ)
        i :
      γ)
⊢ (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ } : (a : ℕ) → γ) i ≤
    ωSup
      (((c.map { toFun := f, monotone' := ⋯ : α →o β →𝒄 γ }).map toMono).map
        (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β }))))

Tactic:
apply le_ωSup_of_le i

Premises used: OmegaCompletePartialOrder.le_ωSup_of_le
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i : ℕ
a : g ((c.toOrderHom : (a : ℕ) → α) i) ≤ ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β })
⊢ LE.le (α := γ) ((c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ } : (a : ℕ) → γ) i : γ)
    ((((c.map { toFun := f, monotone' := ⋯ : α →o β →𝒄 γ }).map toMono).map
            (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β }))) :
          (a : ℕ) → γ)
        i :
      γ)

Tactic:
apply (f (c i)).monotone

Premises used: OmegaCompletePartialOrder.ContinuousHom.monotone, DFunLike.coe
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i : ℕ
a : g ((c.toOrderHom : (a : ℕ) → α) i) ≤ g ((c.toOrderHom : (a : ℕ) → α) i)
⊢ g ((c.toOrderHom : (a : ℕ) → α) i) ≤ ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β })

Tactic:
apply le_ωSup_of_le i

Premises used: OmegaCompletePartialOrder.le_ωSup_of_le
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i : ℕ
⊢ g ((c.toOrderHom : (a : ℕ) → α) i) ≤ g ((c.toOrderHom : (a : ℕ) → α) i)

Tactic:
rfl
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
⊢ Eq.{u_3 + 1} (α := β) ((ωSup c₀ : (a : α) → β) (ωSup c₁) : β)
    ((Prod.apply : (a : (α →𝒄 β) × α) → β) (ωSup (c₀.zip c₁)) : β)

Tactic:
simp [Prod.apply_apply, Prod.ωSup_zip]

Premises used: Prod.ωSup_zip, OmegaCompletePartialOrder.ContinuousHom.Prod.apply_apply
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β_1 : Type u_3
γ_1 : Type u_4
δ : Type u_5
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β_1
inst_2 : OmegaCompletePartialOrder γ_1
inst_3 : OmegaCompletePartialOrder δ
β γ : Type v
f : ContinuousHom.{u_2, v} α (Part β)
g : ContinuousHom.{u_2, v} α (β → Part γ)
c : Chain α
rw :
  OrderHom.toFun (OrderHom.partBind (↑f : α →o Part β) (↑g : α →o β → Part γ)) (ωSup c) =
    Bind.bind (α := β) ((f : (a : α) → Part β) (ωSup c)) ((g : (a : α) → β → Part γ) (ωSup c))
⊢ (OrderHom.partBind (↑f : α →o Part β) g.toOrderHom).toFun (ωSup c) =
    ωSup (c.map (OrderHom.partBind (↑f : α →o Part β) g.toOrderHom))

Tactic:
rw [ωSup_bind, ← f.continuous, g.toOrderHom_eq_coe, ← g.continuous]

Premises used: OmegaCompletePartialOrder.ContinuousHom.toOrderHom_eq_coe, OmegaCompletePartialOrder.ContinuousHom.ωSup_bind, OmegaCompletePartialOrder.ContinuousHom.continuous
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β_1 : Type u_3
γ_1 : Type u_4
δ : Type u_5
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β_1
inst_2 : OmegaCompletePartialOrder γ_1
inst_3 : OmegaCompletePartialOrder δ
β γ : Type v
f : ContinuousHom.{u_2, v} α (Part β)
g : ContinuousHom.{u_2, v} α (β → Part γ)
c : Chain α
⊢ OrderHom.toFun (OrderHom.partBind (↑f : α →o Part β) (↑g : α →o β → Part γ)) (ωSup c) =
    Bind.bind (α := β) ((f : (a : α) → Part β) (ωSup c)) ((g : (a : α) → β → Part γ) (ωSup c))

Tactic:
rfl
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β_1 : Type u_3
γ_1 : Type u_4
δ : Type u_5
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β_1
inst_2 : OmegaCompletePartialOrder γ_1
inst_3 : OmegaCompletePartialOrder δ
β γ : Type v
f : β → γ
g : ContinuousHom.{u_2, v} α (Part β)
h : ∀ (x : α), Eq (α := Part γ) (f <$> (g : (a : α) → Part β) x) ((g.bind (const (pure ∘ f)) : (a : α) → Part γ) x)
⊢ Eq (α := α → Part γ) (fun (x : α) ↦ f <$> (g : (a : α) → Part β) x) (⇑(g.bind (const (pure ∘ f))) : (a : α) → Part γ)

Tactic:
ext1
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β_1 : Type u_3
γ_1 : Type u_4
δ : Type u_5
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β_1
inst_2 : OmegaCompletePartialOrder γ_1
inst_3 : OmegaCompletePartialOrder δ
β γ : Type v
f : β → γ
g : ContinuousHom.{u_2, v} α (Part β)
x : α
⊢ Eq (α := Part γ) (f <$> (g : (a : α) → Part β) x) ((g.bind (const (pure ∘ f)) : (a : α) → Part γ) x)

Tactic:
simp only [map_eq_bind_pure_comp, bind, coe_mk, OrderHom.partBind_coe, coe_apply,
      coe_toOrderHom, const_apply, Part.bind_eq_bind]

Premises used: OmegaCompletePartialOrder.ContinuousHom.const_apply, OmegaCompletePartialOrder.ContinuousHom.coe_toOrderHom, OmegaCompletePartialOrder.ContinuousHom.coe_mk, OmegaCompletePartialOrder.ContinuousHom.bind, OmegaCompletePartialOrder.ContinuousHom.coe_apply, Part.bind_eq_bind, map_eq_bind_pure_comp, OrderHom.partBind_coe
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β_1 : Type u_3
γ_1 : Type u_4
δ : Type u_5
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β_1
inst_2 : OmegaCompletePartialOrder γ_1
inst_3 : OmegaCompletePartialOrder δ
β γ : Type v
f : ContinuousHom.{u_2, v} α (Part (β → γ))
g : ContinuousHom.{u_2, v} α (Part β)
h :
  ∀ (x : α) (a : γ),
    Membership.mem (γ := Part γ) ((f : (a : α) → Part (β → γ)) x <*> (g : (a : α) → Part β) x) a ↔
      Membership.mem (γ := Part γ) ((f.bind (flip (_root_.flip map g)) : (a : α) → Part γ) x : Part γ) a
⊢ Eq (α := α → Part γ) (fun (x : α) ↦ (f : (a : α) → Part (β → γ)) x <*> (g : (a : α) → Part β) x)
    (⇑(f.bind (flip (_root_.flip map g))) : (a : α) → Part γ)

Tactic:
ext
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β_1 : Type u_3
γ_1 : Type u_4
δ : Type u_5
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β_1
inst_2 : OmegaCompletePartialOrder γ_1
inst_3 : OmegaCompletePartialOrder δ
β γ : Type v
f : ContinuousHom.{u_2, v} α (Part (β → γ))
g : ContinuousHom.{u_2, v} α (Part β)
x : α
a : γ
⊢ Membership.mem (γ := Part γ) ((f : (a : α) → Part (β → γ)) x <*> (g : (a : α) → Part β) x) a ↔
    Membership.mem (γ := Part γ) ((f.bind (flip (_root_.flip map g)) : (a : α) → Part γ) x : Part γ) a

Tactic:
simp only [seq_eq_bind_map, Part.bind_eq_bind, Part.mem_bind_iff, flip_apply, _root_.flip,
        map_apply, bind_apply, Part.map_eq_map]

Premises used: Part.mem_bind_iff, OmegaCompletePartialOrder.ContinuousHom.bind_apply, flip, Part.map_eq_map, OmegaCompletePartialOrder.ContinuousHom.flip_apply, Part.bind_eq_bind, seq_eq_bind_map, OmegaCompletePartialOrder.ContinuousHom.map_apply
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
rw : ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α)) = ωSup (iterateChain (↑f : α →o α) x h)
⊢ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) (ωSup (iterateChain (↑f : α →o α) x h))

Tactic:
rw [mem_fixedPoints, IsFixedPt, f.continuous]

Premises used: Function.mem_fixedPoints, OmegaCompletePartialOrder.ContinuousHom.continuous, Function.IsFixedPt
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
a : ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α)) ≤ ωSup (iterateChain (↑f : α →o α) x h)
a₁ : ωSup (iterateChain (↑f : α →o α) x h) ≤ ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α))
⊢ ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α)) = ωSup (iterateChain (↑f : α →o α) x h)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
a :
  ∀ (i : ℕ),
    ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α) : (a : ℕ) → α) i ≤ ωSup (iterateChain (↑f : α →o α) x h)
⊢ ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α)) ≤ ωSup (iterateChain (↑f : α →o α) x h)

Tactic:
apply ωSup_le

Premises used: OmegaCompletePartialOrder.ωSup_le
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
n : ℕ
a : (f : (a : α) → α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n : α) ≤ ωSup (iterateChain (↑f : α →o α) x h)
⊢ ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α) : (a : ℕ) → α) n ≤ ωSup (iterateChain (↑f : α →o α) x h)

Tactic:
simp only [Chain.coe_map, OrderHomClass.coe_coe, comp_apply]

Premises used: OmegaCompletePartialOrder.Chain.coe_map, OrderHomClass.coe_coe, Function.comp_apply
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
n : ℕ
⊢ Eq (α := α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n.succ : α)
    ((f : (a : α) → α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n : α) : α)

Tactic:
have : iterateChain f x h (n.succ) = f (iterateChain f x h n) :=
      Function.iterate_succ_apply' ..
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
n : ℕ
this :
  Eq (α := α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n.succ : α)
    ((f : (a : α) → α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n : α) : α)
a : (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n.succ ≤ ωSup (iterateChain (↑f : α →o α) x h)
⊢ (f : (a : α) → α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n : α) ≤ ωSup (iterateChain (↑f : α →o α) x h)

Tactic:
rw [← this]
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
n : ℕ
this :
  Eq (α := α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n.succ : α)
    ((f : (a : α) → α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n : α) : α)
⊢ (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n.succ ≤ ωSup (iterateChain (↑f : α →o α) x h)

Tactic:
apply le_ωSup

Premises used: OmegaCompletePartialOrder.le_ωSup