awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
x : α
i : ℕ
h : x ≤ (c : (a : ℕ) → α) i
⊢ x ≤ ωSup c

Tactic:
le_trans h (le_ωSup c _)

Premises used: OmegaCompletePartialOrder.le_ωSup, le_trans
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
x : α
h : ∀ (i : ℕ), (c : (a : ℕ) → α) i ≤ x ∨ x ≤ (c : (a : ℕ) → α) i
this : ¬∀ (i : ℕ), (c : (a : ℕ) → α) i ≤ x
⊢ ∃ (x_1 : ℕ), ¬(c : (a : ℕ) → α) x_1 ≤ x

Tactic:
simp only [not_forall] at this ⊢

Premises used: Classical.not_forall
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
x : α
h : ∀ (i : ℕ), (c : (a : ℕ) → α) i ≤ x ∨ x ≤ (c : (a : ℕ) → α) i
this : ∃ (x_1 : ℕ), ¬(c : (a : ℕ) → α) x_1 ≤ x
⊢ ∃ (i : ℕ), ¬(c : (a : ℕ) → α) i ≤ x

Tactic:
assumption
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c₀ c₁ : Chain α
h : c₀ ≤ c₁
i : ℕ
obtain :
  ∀ (w : ℕ) (h : LE.le (α := α) ((c₀ : (a : ℕ) → α) i : α) ((c₁ : (a : ℕ) → α) w : α)), (c₀ : (a : ℕ) → α) i ≤ ωSup c₁
⊢ (c₀ : (a : ℕ) → α) i ≤ ωSup c₁

Tactic:
obtain ⟨_, h⟩ := h i
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c₀ c₁ : Chain α
h_1 : c₀ ≤ c₁
i w : ℕ
h : LE.le (α := α) ((c₀ : (a : ℕ) → α) i : α) ((c₁ : (a : ℕ) → α) w : α)
⊢ (c₀ : (a : ℕ) → α) i ≤ ωSup c₁

Tactic:
le_trans h (le_ωSup _ _)

Premises used: OmegaCompletePartialOrder.le_ωSup, le_trans
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c₀ c₁ : Chain α
h_1 : c₀ ≤ c₁
i w : ℕ
h : LE.le (α := α) ((c₀ : (a : ℕ) → α) i : α) ((c₁ : (a : ℕ) → α) w : α)
⊢ (c₀ : (a : ℕ) → α) i ≤ ωSup c₁

Tactic:
exact le_trans h (le_ωSup _ _)

Premises used: OmegaCompletePartialOrder.le_ωSup, le_trans
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
x : α
mp : ωSup c ≤ x → ∀ (i : ℕ), (c : (a : ℕ) → α) i ≤ x
mpr : (∀ (i : ℕ), (c : (a : ℕ) → α) i ≤ x) → ωSup c ≤ x
⊢ ωSup c ≤ x ↔ ∀ (i : ℕ), (c : (a : ℕ) → α) i ≤ x

Tactic:
constructor
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
x : α
h : ωSup c ≤ x
i : ℕ
trans : (c : (a : ℕ) → α) i ≤ ωSup c
trans₁ : ωSup c ≤ x
⊢ (c : (a : ℕ) → α) i ≤ x

Tactic:
trans ωSup c

Premises used: OmegaCompletePartialOrder.ωSup
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
x : α
h : ωSup c ≤ x
i : ℕ
⊢ (c : (a : ℕ) → α) i ≤ ωSup c

Tactic:
le_ωSup _ _

Premises used: OmegaCompletePartialOrder.le_ωSup
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
x : α
h : ωSup c ≤ x
i : ℕ
⊢ (c : (a : ℕ) → α) i ≤ ωSup c

Tactic:
exact le_ωSup _ _

Premises used: OmegaCompletePartialOrder.le_ωSup
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
x : α
h : ωSup c ≤ x
i : ℕ
⊢ ωSup c ≤ x

Tactic:
assumption
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
x : α
h : ∀ (i : ℕ), (c : (a : ℕ) → α) i ≤ x
⊢ ωSup c ≤ x

Tactic:
ωSup_le _ _ ‹_›

Premises used: OmegaCompletePartialOrder.ωSup_le
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
x : α
h : ∀ (i : ℕ), (c : (a : ℕ) → α) i ≤ x
⊢ ωSup c ≤ x

Tactic:
exact ωSup_le _ _ ‹_›

Premises used: OmegaCompletePartialOrder.ωSup_le
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
left : Membership.mem (γ := Set α) (upperBounds (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α))) (ωSup c)
right : Membership.mem (γ := Set α) (lowerBounds (upperBounds (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α)))) (ωSup c)
⊢ IsLUB (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α)) (ωSup c)

Tactic:
constructor
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
left : ∀ (a : ℕ), (c : (a : ℕ) → α) a ≤ ωSup c
⊢ Membership.mem (γ := Set α) (upperBounds (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α))) (ωSup c)

Tactic:
simp only [upperBounds, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff,
      Set.mem_setOf_eq]

Premises used: Set.mem_range, forall_exists_index, upperBounds, Set.mem_setOf_eq, forall_apply_eq_imp_iff
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
⊢ ∀ (a : ℕ), (c : (a : ℕ) → α) a ≤ ωSup c

Tactic:
fun a ↦ le_ωSup c a

Premises used: OmegaCompletePartialOrder.le_ωSup
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
⊢ ∀ (a : ℕ), (c : (a : ℕ) → α) a ≤ ωSup c

Tactic:
exact fun a ↦ le_ωSup c a

Premises used: OmegaCompletePartialOrder.le_ωSup
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
right : ∀ ⦃a : α⦄, (∀ (a_1 : ℕ), (c : (a : ℕ) → α) a_1 ≤ a) → ωSup c ≤ a
⊢ Membership.mem (γ := Set α) (lowerBounds (upperBounds (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α)))) (ωSup c)

Tactic:
simp only [lowerBounds, upperBounds, Set.mem_range, forall_exists_index,
      forall_apply_eq_imp_iff, Set.mem_setOf_eq]

Premises used: Set.mem_range, lowerBounds, forall_exists_index, upperBounds, Set.mem_setOf_eq, forall_apply_eq_imp_iff
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
⊢ ∀ ⦃a : α⦄, (∀ (a_1 : ℕ), (c : (a : ℕ) → α) a_1 ≤ a) → ωSup c ≤ a

Tactic:
fun ⦃a⦄ a_1 ↦ ωSup_le c a a_1

Premises used: OmegaCompletePartialOrder.ωSup_le
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
⊢ ∀ ⦃a : α⦄, (∀ (a_1 : ℕ), (c : (a : ℕ) → α) a_1 ≤ a) → ωSup c ≤ a

Tactic:
exact fun ⦃a⦄ a_1 ↦ ωSup_le c a a_1

Premises used: OmegaCompletePartialOrder.ωSup_le
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
a : α
h : IsLUB (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α)) a
rw : a ≤ ωSup c ∧ ωSup c ≤ a
⊢ a = ωSup c

Tactic:
rw [le_antisymm_iff]

Premises used: le_antisymm_iff
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
a : α
h : IsLUB (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α)) a
⊢ (∀ (a_1 : ℕ), (c : (a : ℕ) → α) a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), (c : (a : ℕ) → α) a ≤ a_1) → a ≤ a_1

Tactic:
simp only [IsLUB, IsLeast, upperBounds, lowerBounds, Set.mem_range, forall_exists_index,
    forall_apply_eq_imp_iff, Set.mem_setOf_eq] at h

Premises used: Set.mem_range, lowerBounds, forall_exists_index, upperBounds, Set.mem_setOf_eq, IsLeast, IsLUB, forall_apply_eq_imp_iff
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), (c : (a : ℕ) → α) a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), (c : (a : ℕ) → α) a ≤ a_1) → a ≤ a_1
left : a ≤ ωSup c
right : ωSup c ≤ a
⊢ a ≤ ωSup c ∧ ωSup c ≤ a

Tactic:
constructor
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), (c : (a : ℕ) → α) a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), (c : (a : ℕ) → α) a ≤ a_1) → a ≤ a_1
left : ∀ (a : ℕ), (c : (a : ℕ) → α) a ≤ ωSup c
⊢ a ≤ ωSup c

Tactic:
apply h.2

Premises used: And.right
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), (c : (a : ℕ) → α) a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), (c : (a : ℕ) → α) a ≤ a_1) → a ≤ a_1
⊢ ∀ (a : ℕ), (c : (a : ℕ) → α) a ≤ ωSup c

Tactic:
fun a ↦ le_ωSup c a

Premises used: OmegaCompletePartialOrder.le_ωSup
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), (c : (a : ℕ) → α) a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), (c : (a : ℕ) → α) a ≤ a_1) → a ≤ a_1
⊢ ∀ (a : ℕ), (c : (a : ℕ) → α) a ≤ ωSup c

Tactic:
exact fun a ↦ le_ωSup c a

Premises used: OmegaCompletePartialOrder.le_ωSup
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), (c : (a : ℕ) → α) a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), (c : (a : ℕ) → α) a ≤ a_1) → a ≤ a_1
right : ∀ (i : ℕ), (c : (a : ℕ) → α) i ≤ a
⊢ ωSup c ≤ a

Tactic:
rw [ωSup_le_iff]

Premises used: OmegaCompletePartialOrder.ωSup_le_iff
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), (c : (a : ℕ) → α) a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), (c : (a : ℕ) → α) a ≤ a_1) → a ≤ a_1
⊢ ∀ (i : ℕ), (c : (a : ℕ) → α) i ≤ a

Tactic:
apply h.1

Premises used: And.left
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
hf : ScottContinuous f
⊢ ωScottContinuous f

Tactic:
hf.scottContinuousOn

Premises used: OmegaCompletePartialOrder.ωScottContinuous, ScottContinuous.scottContinuousOn
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
h : ωScottContinuous f
a b : α
hab : a ≤ b
h₁ : Eq (α := Set α) ((fun (c : Chain α) ↦ (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) (pair a b hab)) {a, b}
⊢ Membership.mem (γ := Set (Set α)) (Set.range fun (c : Chain α) ↦ Set.range (ι := ℕ) (⇑c : (a : ℕ) → α)) {a, b}

Tactic:
use pair a b hab

Premises used: OmegaCompletePartialOrder.Chain.pair
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
h : ωScottContinuous f
a b : α
hab : a ≤ b
⊢ Eq (α := Set α) ((fun (c : Chain α) ↦ (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) (pair a b hab)) {a, b}

Tactic:
range_pair a b hab

Premises used: OmegaCompletePartialOrder.Chain.range_pair
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
h : ωScottContinuous f
a b : α
hab : a ≤ b
⊢ Eq (α := Set α) ((fun (c : Chain α) ↦ (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) (pair a b hab)) {a, b}

Tactic:
exact range_pair a b hab

Premises used: OmegaCompletePartialOrder.Chain.range_pair
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
c : Chain α
hf : ωScottContinuous f
⊢ Membership.mem (γ := Set (Set α)) (Set.range fun (c : Chain α) ↦ Set.range (ι := ℕ) (⇑c : (a : ℕ) → α))
    (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α))

Tactic:
simp
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
c : Chain α
hf : ωScottContinuous f
⊢ IsLUB (Set.range (ι := ℕ) (⇑(c.map { toFun := f, monotone' := ⋯ : α →o β }) : (a : ℕ) → β)) (f (ωSup c))

Tactic:
simpa [Set.range_comp]
    using hf (by simp) (Set.range_nonempty _) (isChain_range c).directedOn (isLUB_range_ωSup c)

Premises used: Set.range_comp, IsChain.directedOn, Set.range_nonempty, OmegaCompletePartialOrder.Chain.isChain_range, OmegaCompletePartialOrder.isLUB_range_ωSup
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
⊢ ωScottContinuous.{u_2, u_2} (α := α) _root_.id

Tactic:
ScottContinuousOn.id

Premises used: ScottContinuousOn.id, OmegaCompletePartialOrder.ωScottContinuous
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
hf : ωScottContinuous f
c : Chain α
⊢ f (ωSup c) = ωSup (c.map { toFun := f, monotone' := ⋯ : α →o β })

Tactic:
ωSup_eq_of_isLUB hf.isLUB

Premises used: OmegaCompletePartialOrder.ωScottContinuous.isLUB, OmegaCompletePartialOrder.ωSup_eq_of_isLUB
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
⊢ ωScottContinuous f ↔
    ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf : α →o β })

Tactic:
⟨fun hf ↦ ⟨hf.monotone, hf.map_ωSup⟩, ?_⟩

Premises used: OmegaCompletePartialOrder.ωScottContinuous.map_ωSup, OmegaCompletePartialOrder.ωScottContinuous.monotone, Iff.intro, Exists.intro
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
refine :
  (∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf : α →o β })) →
    ωScottContinuous f
⊢ ωScottContinuous f ↔
    ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf : α →o β })

Tactic:
refine ⟨fun hf ↦ ⟨hf.monotone, hf.map_ωSup⟩, ?_⟩
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf : α →o β })
_ :
  ∀ ⦃d : Set α⦄,
    Membership.mem (γ := Set (Set α)) (Set.range fun (c : Chain α) ↦ Set.range (ι := ℕ) (⇑c : (a : ℕ) → α)) d →
      d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → IsLUB (f '' d) (f a)
⊢ ωScottContinuous f

Tactic:
_
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf : α →o β })
d : Set α
this :
  ∀ (c : Chain α) (hc : (fun (c : Chain α) ↦ (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) c = d),
    d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → IsLUB (f '' d) (f a)
⊢ Membership.mem (γ := Set (Set α)) (Set.range fun (c : Chain α) ↦ Set.range (ι := ℕ) (⇑c : (a : ℕ) → α)) d →
    d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → IsLUB (f '' d) (f a)

Tactic:
⟨c, hc⟩
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf : α →o β })
d : Set α
c : Chain α
hc : (fun (c : Chain α) ↦ (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) c = d
_ : d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → IsLUB (f '' d) (f a)
⊢ d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → IsLUB (f '' d) (f a)

Tactic:
_
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf : α →o β })
d : Set α
c : Chain α
hc : (fun (c : Chain α) ↦ (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) c = d
h : d.Nonempty
_ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → IsLUB (f '' d) (f a)
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → IsLUB (f '' d) (f a)

Tactic:
_
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf : α →o β })
d : Set α
c : Chain α
hc : (fun (c : Chain α) ↦ (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) c = d
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
_ : ∀ ⦃a : α⦄, IsLUB d a → IsLUB (f '' d) (f a)
⊢ ∀ ⦃a : α⦄, IsLUB d a → IsLUB (f '' d) (f a)

Tactic:
_
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf : α →o β })
d : Set α
c : Chain α
hc : (fun (c : Chain α) ↦ (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) c = d
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
⊢ IsLUB (Set.range (ι := ℕ) (⇑(c.map { toFun := f, monotone' := ⋯ }) : (a : ℕ) → β))
    (ωSup (c.map { toFun := f, monotone' := ⋯ : α →o β }))

Tactic:
isLUB_range_ωSup (c.map { toFun := f, monotone' := hf.1 })

Premises used: OrderHom.mk, OmegaCompletePartialOrder.Chain.map, OmegaCompletePartialOrder.isLUB_range_ωSup
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf : α →o β })
d : Set α
c : Chain α
hc : (fun (c : Chain α) ↦ (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) c = d
h_1 : d.Nonempty
h_2 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
h : f '' d = Set.range (ι := ℕ) (⇑(c.map { toFun := f, monotone' := ⋯ }) : (a : ℕ) → β)
h₁ : f a = ωSup (c.map { toFun := f, monotone' := ⋯ })
⊢ IsLUB (f '' d) (f a)

Tactic:
convert! isLUB_range_ωSup (c.map { toFun := f, monotone' := hf.1 })

Premises used: OrderHom.mk, OmegaCompletePartialOrder.Chain.map, OmegaCompletePartialOrder.isLUB_range_ωSup
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf : α →o β })
d : Set α
c : Chain α
hc : (fun (c : Chain α) ↦ (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) c = d
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
⊢ f '' d = Set.range (ι := ℕ) (⇑(c.map { toFun := f, monotone' := ⋯ }) : (a : ℕ) → β)

Tactic:
simp [← hc, ← (Set.range_comp f ⇑c)]

Premises used: Set.range_comp, DFunLike.coe
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf : α →o β })
d : Set α
c : Chain α
hc : (fun (c : Chain α) ↦ (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) c = d
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
⊢ IsLUB ((fun (c : Chain α) ↦ (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) c) a

Tactic:
rw [← hc] at hda
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf : α →o β })
d : Set α
c : Chain α
hc : (fun (c : Chain α) ↦ (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) c = d
h_1 : d.Nonempty
h_2 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB ((fun (c : Chain α) ↦ (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) c) a
h : f a = f (ωSup c)
h₁ h₂ : f (ωSup c) = f (ωSup c)
⊢ f a = ωSup (c.map { toFun := f, monotone' := ⋯ })

Tactic:
rw [← hf.2 c, ωSup_eq_of_isLUB hda]

Premises used: OmegaCompletePartialOrder.ωSup_eq_of_isLUB
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α →o β
rw :
  (∃ (hf : Monotone.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)),
      ∀ (c : Chain α),
        (f : (a : α) → β) (ωSup c) = ωSup (c.map { toFun := (⇑f : (a : α) → β), monotone' := hf : α →o β })) ↔
    ∀ (c : Chain α), (f : (a : α) → β) (ωSup c) = ωSup (c.map f)
⊢ ωScottContinuous.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β) ↔
    ∀ (c : Chain α), (f : (a : α) → β) (ωSup c) = ωSup (c.map f)

Tactic:
rw [ωScottContinuous_iff_monotone_map_ωSup]

Premises used: OmegaCompletePartialOrder.ωScottContinuous_iff_monotone_map_ωSup
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α →o β
⊢ (∃ (hf : Monotone.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)),
      ∀ (c : Chain α),
        (f : (a : α) → β) (ωSup c) = ωSup (c.map { toFun := (⇑f : (a : α) → β), monotone' := hf : α →o β })) ↔
    ∀ (c : Chain α), (f : (a : α) → β) (ωSup c) = ωSup (c.map f)

Tactic:
exists_prop_of_true f.monotone'

Premises used: exists_prop_of_true, OrderHom.monotone'
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α →o β
⊢ (∃ (hf : Monotone.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)),
      ∀ (c : Chain α),
        (f : (a : α) → β) (ωSup c) = ωSup (c.map { toFun := (⇑f : (a : α) → β), monotone' := hf : α →o β })) ↔
    ∀ (c : Chain α), (f : (a : α) → β) (ωSup c) = ωSup (c.map f)

Tactic:
exact exists_prop_of_true f.monotone'

Premises used: exists_prop_of_true, OrderHom.monotone'
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β
g : β → γ
hg : ωScottContinuous g
hf : ωScottContinuous f
⊢ ∀ (c : Chain α), (g ∘ f) (ωSup c) = ωSup (c.map { toFun := g ∘ f, monotone' := ⋯ : α →o γ })

Tactic:
simp [hf.map_ωSup, hg.map_ωSup, map_comp]

Premises used: OmegaCompletePartialOrder.ωScottContinuous.map_ωSup, OmegaCompletePartialOrder.Chain.map_comp
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
x : β
⊢ ωScottContinuous (Function.const α x)

Tactic:
ScottContinuousOn.const x

Premises used: ScottContinuousOn.const, OmegaCompletePartialOrder.ωScottContinuous
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
c : Chain (Part α)
a b : α
ha : some a ∈ c
hb : some b ∈ c
obtain : ∀ (i : ℕ) (ha : some a = (c : (a : ℕ) → Part α) i), a = b
⊢ a = b

Tactic:
obtain ⟨i, ha⟩ := ha
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
c : Chain (Part α)
a b : α
hb : some b ∈ c
i : ℕ
ha : some a = (c : (a : ℕ) → Part α) i
⊢ (c : (a : ℕ) → Part α) i = some a

Tactic:
replace ha := ha.symm
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
c : Chain (Part α)
a b : α
hb : some b ∈ c
i : ℕ
ha : (c : (a : ℕ) → Part α) i = some a
obtain : ∀ (j : ℕ) (hb : some b = (c : (a : ℕ) → Part α) j), a = b
⊢ a = b

Tactic:
obtain ⟨j, hb⟩ := hb
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : (c : (a : ℕ) → Part α) i = some a
j : ℕ
hb : some b = (c : (a : ℕ) → Part α) j
⊢ (c : (a : ℕ) → Part α) j = some b

Tactic:
replace hb := hb.symm
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : (c : (a : ℕ) → Part α) i = some a
j : ℕ
hb : (c : (a : ℕ) → Part α) j = some b
rw :
  ∀ (ha : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) i : Part α) a) (j : ℕ)
    (hb : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) j : Part α) b), a = b
⊢ a = b

Tactic:
rw [eq_some_iff] at ha hb

Premises used: Part.eq_some_iff
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) i : Part α) a
j : ℕ
hb : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) j : Part α) b
inl : ∀ (hij : i ≤ j), a = b
inr : ∀ (hji : j ≤ i), a = b
⊢ a = b

Tactic:
rcases le_total i j with hij | hji

Premises used: le_total