awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsUpper α
⊢ IsTopologicalBasis (upperBasis α)

Tactic:
IsLower.isTopologicalBasis (α := αᵒᵈ)

Premises used: Set.Mem, setOf, Topology.IsLower.isTopologicalBasis, OrderDual, Topology.IsUpper.upperBasis
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsUpper α
inst_3 : TopologicalSpace β
f : β → α
⊢ Continuous[inst_3, inst_1] f ↔ ∀ (a : α), IsClosed[inst_3] (f ⁻¹' Iic a)

Tactic:
IsLower.continuous_iff_Ici (α := αᵒᵈ)

Premises used: Topology.IsLower.continuous_iff_Ici, setOf, Set.Iic, OrderDual
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : TopologicalSpace α
inst_2 : IsUpper α
⊢ T0Space α

Tactic:
IsLower.t0Space (α := αᵒᵈ)

Premises used: OrderDual, Topology.IsLower.t0Space
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsUpper α
⊢ IsTopologicalBasis (α := α) (insert univ {s : Set α | ∃ (a : α), (Iic a)ᶜ = s})

Tactic:
IsLower.isTopologicalBasis_insert_univ_subbasis (α := αᵒᵈ)

Premises used: Set.Mem, setOf, Set.Iic, Topology.IsLower.isTopologicalBasis_insert_univ_subbasis, OrderDual
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsUpper α
β : Type u_3
f : β → α
l : Filter β
x : α
⊢ Filter.Tendsto f l (𝓝 x) ↔ ∀ y < x, ∀ᶠ (z : β) in l, y < f z

Tactic:
IsLower.tendsto_nhds_iff_lt (α := αᵒᵈ)

Premises used: Topology.IsLower.tendsto_nhds_iff_lt, OrderDual
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsUpper α
U : Set α
⊢ IsOpen[t] U ↔ U = univ ∨ ∃ (a : α), (Iic a)ᶜ = U

Tactic:
IsLower.isTopologicalSpace_basis (α := αᵒᵈ) U

Premises used: Set.Mem, setOf, Set.Iic, OrderDual, Topology.IsLower.isTopologicalSpace_basis
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
inst_3 : OrderBot α
inst_4 : Preorder β
inst_5 : TopologicalSpace β
inst_6 : IsLower β
inst_7 : OrderBot β
⊢ Eq (α := TopologicalSpace (α × β)) instTopologicalSpaceProd (lower (α × β))

Tactic:
le_antisymm (le_generateFrom ?_) ?_

Premises used: le_antisymm, le_generateFrom
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
inst_3 : OrderBot α
inst_4 : Preorder β
inst_5 : TopologicalSpace β
inst_6 : IsLower β
inst_7 : OrderBot β
refine_1 :
  ∀ (s : Set (α × β)),
    Membership.mem (γ := Set (Set (α × β))) {s : Set (α × β) | ∃ (a : α × β), (Ici a)ᶜ = s} s →
      IsOpen[instTopologicalSpaceProd] s
refine_2 : LE.le (α := TopologicalSpace (α × β)) (lower (α × β)) instTopologicalSpaceProd
⊢ Eq (α := TopologicalSpace (α × β)) instTopologicalSpaceProd (lower (α × β))

Tactic:
refine le_antisymm (le_generateFrom ?_) ?_

Premises used: le_antisymm, le_generateFrom
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
inst_3 : OrderBot α
inst_4 : Preorder β
inst_5 : TopologicalSpace β
inst_6 : IsLower β
inst_7 : OrderBot β
x : α × β
⊢ IsOpen[instTopologicalSpaceProd] (Ici x)ᶜ

Tactic:
(isClosed_Ici.prod isClosed_Ici).isOpen_compl

Premises used: Set.Ici, IsClosed.isOpen_compl, Set.Mem, setOf, Set.prod
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
inst_3 : OrderBot α
inst_4 : Preorder β
inst_5 : TopologicalSpace β
inst_6 : IsLower β
inst_7 : OrderBot β
x : α × β
⊢ IsOpen[instTopologicalSpaceProd] (Ici x)ᶜ

Tactic:
exact (isClosed_Ici.prod isClosed_Ici).isOpen_compl

Premises used: IsClosed.isOpen_compl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
inst_3 : OrderBot α
inst_4 : Preorder β
inst_5 : TopologicalSpace β
inst_6 : IsLower β
inst_7 : OrderBot β
refine_2 :
  ∀ x ∈ IsLower.lowerBasis α,
    ∀ y ∈ IsLower.lowerBasis β,
      Membership.mem (γ := Set (Set (α × β))) {s : Set (α × β) | IsOpen[lower (α × β)] s} (x ×ˢ y)
⊢ LE.le (α := TopologicalSpace (α × β)) (lower (α × β)) instTopologicalSpaceProd

Tactic:
rw [(IsLower.isTopologicalBasis.prod
      IsLower.isTopologicalBasis).eq_generateFrom, le_generateFrom_iff_subset_isOpen,
      image2_subset_iff]

Premises used: TopologicalSpace.IsTopologicalBasis.prod, Topology.IsLower.isTopologicalBasis, Set.image2_subset_iff, TopologicalSpace.IsTopologicalBasis.eq_generateFrom, TopologicalSpace.le_generateFrom_iff_subset_isOpen
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
inst_3 : OrderBot α
inst_4 : Preorder β
inst_5 : TopologicalSpace β
inst_6 : IsLower β
inst_7 : OrderBot β
s : Set α
hs : s.Finite
t : Set β
ht : t.Finite
refine_2 : IsOpen[lower (α × β)] ((⋂ i ∈ s, (Prod.fst ⁻¹' Ici i)ᶜ) ∩ ⋂ i ∈ t, (Prod.snd ⁻¹' Ici i)ᶜ)
⊢ IsOpen[lower (α × β)] ((↑(upperClosure s) : Set α)ᶜ ×ˢ (↑(upperClosure t) : Set β)ᶜ)

Tactic:
simp_rw [coe_upperClosure, compl_iUnion, prod_eq, preimage_iInter, preimage_compl]

Premises used: Set.prod_eq, Set.compl_iUnion, coe_upperClosure, Set.preimage_iInter, Set.preimage_compl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
inst_3 : OrderBot α
inst_4 : Preorder β
inst_5 : TopologicalSpace β
inst_6 : IsLower β
inst_7 : OrderBot β
s : Set α
hs : s.Finite
t : Set β
ht : t.Finite
x : TopologicalSpace (α × β) := lower (α × β)
⊢ IsOpen[lower (α × β)] ((⋂ i ∈ s, (Prod.fst ⁻¹' Ici i)ᶜ) ∩ ⋂ i ∈ t, (Prod.snd ⁻¹' Ici i)ᶜ)

Tactic:
(hs.isOpen_biInter fun a _ => ?_).inter (ht.isOpen_biInter fun b _ => ?_)

Premises used: IsOpen.inter, Set.Finite.isOpen_biInter
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
inst_3 : OrderBot α
inst_4 : Preorder β
inst_5 : TopologicalSpace β
inst_6 : IsLower β
inst_7 : OrderBot β
s : Set α
hs : s.Finite
t : Set β
ht : t.Finite
x : TopologicalSpace (α × β) := lower (α × β)
refine_2 : ∀ a ∈ s, IsOpen[lower (α × β)] (Prod.fst ⁻¹' Ici a)ᶜ
refine_2₁ : ∀ b ∈ t, IsOpen[lower (α × β)] (Prod.snd ⁻¹' Ici b)ᶜ
⊢ IsOpen[lower (α × β)] ((⋂ i ∈ s, (Prod.fst ⁻¹' Ici i)ᶜ) ∩ ⋂ i ∈ t, (Prod.snd ⁻¹' Ici i)ᶜ)

Tactic:
refine (hs.isOpen_biInter fun a _ => ?_).inter (ht.isOpen_biInter fun b _ => ?_)

Premises used: IsOpen.inter, Set.Finite.isOpen_biInter
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
inst_3 : OrderBot α
inst_4 : Preorder β
inst_5 : TopologicalSpace β
inst_6 : IsLower β
inst_7 : OrderBot β
s : Set α
hs : s.Finite
t : Set β
ht : t.Finite
x : TopologicalSpace (α × β) := lower (α × β)
a : α
h : a ∈ s
⊢ Eq (α := Set (α × β)) (Ici (a, ⊥))ᶜ (Prod.fst ⁻¹' Ici a)ᶜ

Tactic:
simp [Ici_prod_eq, prod_univ]

Premises used: Set.prod_univ, Set.Ici_prod_eq
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
inst_3 : OrderBot α
inst_4 : Preorder β
inst_5 : TopologicalSpace β
inst_6 : IsLower β
inst_7 : OrderBot β
s : Set α
hs : s.Finite
t : Set β
ht : t.Finite
x : TopologicalSpace (α × β) := lower (α × β)
a : α
h : a ∈ s
⊢ IsOpen[lower (α × β)] (Prod.fst ⁻¹' Ici a)ᶜ

Tactic:
exact GenerateOpen.basic _ ⟨(a, ⊥), by simp [Ici_prod_eq, prod_univ]⟩
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
inst_3 : OrderBot α
inst_4 : Preorder β
inst_5 : TopologicalSpace β
inst_6 : IsLower β
inst_7 : OrderBot β
s : Set α
hs : s.Finite
t : Set β
ht : t.Finite
x : TopologicalSpace (α × β) := lower (α × β)
b : β
h : b ∈ t
⊢ Eq (α := Set (α × β)) (Ici (⊥, b))ᶜ (Prod.snd ⁻¹' Ici b)ᶜ

Tactic:
simp [Ici_prod_eq, univ_prod]

Premises used: Set.univ_prod, Set.Ici_prod_eq
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
inst_3 : OrderBot α
inst_4 : Preorder β
inst_5 : TopologicalSpace β
inst_6 : IsLower β
inst_7 : OrderBot β
s : Set α
hs : s.Finite
t : Set β
ht : t.Finite
x : TopologicalSpace (α × β) := lower (α × β)
b : β
h : b ∈ t
⊢ IsOpen[lower (α × β)] (Prod.snd ⁻¹' Ici b)ᶜ

Tactic:
exact GenerateOpen.basic _ ⟨(⊥, b), by simp [Ici_prod_eq, univ_prod]⟩
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsUpper α
inst_3 : OrderTop α
inst_4 : Preorder β
inst_5 : TopologicalSpace β
inst_6 : IsUpper β
inst_7 : OrderTop β
suffices : IsLower (α × β)ᵒᵈ
⊢ Eq (α := TopologicalSpace (α × β)) instTopologicalSpaceProd (upper (α × β))

Tactic:
suffices IsLower (α × β)ᵒᵈ from IsLower.topology_eq_lowerTopology (α := (α × β)ᵒᵈ)
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsUpper α
inst_3 : OrderTop α
inst_4 : Preorder β
inst_5 : TopologicalSpace β
inst_6 : IsUpper β
inst_7 : OrderTop β
⊢ IsLower (α × β)ᵒᵈ

Tactic:
instIsLowerProd (α := αᵒᵈ) (β := βᵒᵈ)

Premises used: Topology.instIsLowerProd, setOf, OrderDual
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsUpper α
inst_3 : OrderTop α
inst_4 : Preorder β
inst_5 : TopologicalSpace β
inst_6 : IsUpper β
inst_7 : OrderTop β
⊢ IsLower (α × β)ᵒᵈ

Tactic:
exact instIsLowerProd (α := αᵒᵈ) (β := βᵒᵈ)

Premises used: Topology.instIsLowerProd
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : TopologicalSpace α
inst_3 : IsLower α
inst_4 : TopologicalSpace β
inst_5 : IsLower β
f : sInfHom α β
⊢ Continuous[inst_2, inst_4] (⇑f : (a : α) → β)

Tactic:
IsLower.continuous_iff_Ici.2 fun b => ?_

Premises used: Iff.mpr, Topology.IsLower.continuous_iff_Ici
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : TopologicalSpace α
inst_3 : IsLower α
inst_4 : TopologicalSpace β
inst_5 : IsLower β
f : sInfHom α β
refine : ∀ (b : β), IsClosed[inst_2] ((⇑f : (a : α) → β) ⁻¹' Ici b)
⊢ Continuous[inst_2, inst_4] (⇑f : (a : α) → β)

Tactic:
refine IsLower.continuous_iff_Ici.2 fun b => ?_

Premises used: Iff.mpr, Topology.IsLower.continuous_iff_Ici
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : TopologicalSpace α
inst_3 : IsLower α
inst_4 : TopologicalSpace β
inst_5 : IsLower β
f : sInfHom α β
b : β
⊢ IsClosed[inst_2] (Ici (sInf ((⇑f : (a : α) → β) ⁻¹' Ici b)))

Tactic:
isClosed_Ici (a := sInf <| f ⁻¹' Ici b)

Premises used: isClosed_Ici
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : TopologicalSpace α
inst_3 : IsLower α
inst_4 : TopologicalSpace β
inst_5 : IsLower β
f : sInfHom α β
b : β
h : Eq.{u_1 + 1} (α := Set α) ((⇑f : (a : α) → β) ⁻¹' Ici b) (Ici (sInf ((⇑f : (a : α) → β) ⁻¹' Ici b)))
⊢ IsClosed[inst_2] ((⇑f : (a : α) → β) ⁻¹' Ici b)

Tactic:
convert! isClosed_Ici (a := sInf <| f ⁻¹' Ici b)

Premises used: isClosed_Ici
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : TopologicalSpace α
inst_3 : IsLower α
inst_4 : TopologicalSpace β
inst_5 : IsLower β
f : sInfHom α β
b : β
⊢ Eq.{u_1 + 1} (α := Set α) ((⇑f : (a : α) → β) ⁻¹' Ici b) (Ici (sInf ((⇑f : (a : α) → β) ⁻¹' Ici b)))

Tactic:
Subset.antisymm (fun a => sInf_le) fun a ha => le_trans ?_ <|
    OrderHomClass.mono (f : α →o β) ha

Premises used: Set.Subset.antisymm, OrderHomClass.mono, sInf_le, OrderHomClass.toOrderHom, le_trans
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : TopologicalSpace α
inst_3 : IsLower α
inst_4 : TopologicalSpace β
inst_5 : IsLower β
f : sInfHom α β
b : β
h :
  ∀ (a : α) (ha : Membership.mem (γ := Set α) (Ici (sInf ((⇑f : (a : α) → β) ⁻¹' Ici b))) a),
    b ≤ ((↑f : α →o β) : (a : α) → β) (sInf ((⇑f : (a : α) → β) ⁻¹' Ici b))
⊢ Eq.{u_1 + 1} (α := Set α) ((⇑f : (a : α) → β) ⁻¹' Ici b) (Ici (sInf ((⇑f : (a : α) → β) ⁻¹' Ici b)))

Tactic:
refine Subset.antisymm (fun a => sInf_le) fun a ha => le_trans ?_ <|
    OrderHomClass.mono (f : α →o β) ha

Premises used: Set.Subset.antisymm, OrderHomClass.mono, sInf_le, OrderHomClass.toOrderHom, le_trans
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : TopologicalSpace α
inst_3 : IsLower α
inst_4 : TopologicalSpace β
inst_5 : IsLower β
f : sInfHom α β
b : β
a : α
ha : Membership.mem (γ := Set α) (Ici (sInf ((⇑f : (a : α) → β) ⁻¹' Ici b))) a
⊢ b ≤ ((↑f : α →o β) : (a : α) → β) (sInf ((⇑f : (a : α) → β) ⁻¹' Ici b))

Tactic:
LE.le.trans ?_ (map_sInf f _).ge

Premises used: sInfHomClass.map_sInf, Eq.ge, LE.le.trans
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : TopologicalSpace α
inst_3 : IsLower α
inst_4 : TopologicalSpace β
inst_5 : IsLower β
f : sInfHom α β
b : β
a : α
ha : Membership.mem (γ := Set α) (Ici (sInf ((⇑f : (a : α) → β) ⁻¹' Ici b))) a
h : b ≤ sInf (image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) ⁻¹' Ici b))
⊢ b ≤ ((↑f : α →o β) : (a : α) → β) (sInf ((⇑f : (a : α) → β) ⁻¹' Ici b))

Tactic:
refine LE.le.trans ?_ (map_sInf f _).ge

Premises used: sInfHomClass.map_sInf, Eq.ge, LE.le.trans
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : TopologicalSpace α
inst_3 : IsLower α
inst_4 : TopologicalSpace β
inst_5 : IsLower β
f : sInfHom α β
b : β
a : α
ha : Membership.mem (γ := Set α) (Ici (sInf ((⇑f : (a : α) → β) ⁻¹' Ici b))) a
⊢ b ≤ sInf (image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) ⁻¹' Ici b))

Tactic:
simp
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : TopologicalSpace α
inst_3 : IsLower α
inst_4 : TopologicalSpace β
inst_5 : IsLower β
⊢ ContinuousInf α

Tactic:
⟨(infsInfHom : sInfHom (α × α) α).continuous⟩

Premises used: sInfHom.continuous, infsInfHom, ContinuousInf.mk
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : TopologicalSpace α
inst_3 : IsUpper α
inst_4 : TopologicalSpace β
inst_5 : IsUpper β
f : sSupHom α β
⊢ Continuous[inst_2, inst_4] (⇑f : (a : α) → β)

Tactic:
sInfHom.continuous (α := αᵒᵈ) (β := βᵒᵈ) (sSupHom.dual.toFun f)

Premises used: sSupHom.dual, sInfHom.continuous, Equiv.toFun, OrderDual
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : TopologicalSpace α
inst_3 : IsUpper α
inst_4 : TopologicalSpace β
inst_5 : IsUpper β
⊢ ContinuousSup α

Tactic:
⟨(supsSupHom : sSupHom (α × α) α).continuous⟩

Premises used: supsSupHom, sSupHom.continuous, ContinuousSup.mk
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
mp : IsUpper.{u_1} αᵒᵈ → IsLower α
mpr : IsLower α → IsUpper.{u_1} αᵒᵈ
⊢ IsUpper.{u_1} αᵒᵈ ↔ IsLower α

Tactic:
constructor
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
⊢ IsUpper.{u_1} αᵒᵈ → IsLower α

Tactic:
apply OrderDual.instIsLower

Premises used: OrderDual.instIsLower
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
⊢ IsLower α → IsUpper.{u_1} αᵒᵈ

Tactic:
apply OrderDual.instIsUpper

Premises used: OrderDual.instIsUpper
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
⊢ IsLower.{u_1} αᵒᵈ ↔ IsUpper α

Tactic:
isUpper_orderDual.symm

Premises used: Topology.isUpper_orderDual, OrderDual, Iff.symm
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
rw :
  Eq (α := TopologicalSpace Prop) (generateFrom {∅, {True}}) (generateFrom {s : Set Prop | ∃ (a : Prop), (Iic a)ᶜ = s})
⊢ sierpinskiSpace = upper Prop

Tactic:
rw [Topology.upper, sierpinskiSpace, ← generateFrom_insert_empty]

Premises used: generateFrom_insert_empty, Topology.upper, sierpinskiSpace
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
e_g : Eq (α := Set (Set Prop)) {∅, {True}} {s : Set Prop | ∃ (a : Prop), (Iic a)ᶜ = s}
⊢ Eq (α := TopologicalSpace Prop) (generateFrom {∅, {True}}) (generateFrom {s : Set Prop | ∃ (a : Prop), (Iic a)ᶜ = s})

Tactic:
congr
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
h : Set Prop
hs : Membership.mem (γ := Set (Set Prop)) {∅, {True}} h
simp : ∃ (a : Prop), Ioi a = h
⊢ Membership.mem (γ := Set (Set Prop)) {s : Set Prop | ∃ (a : Prop), (Iic a)ᶜ = s} h

Tactic:
simp only [compl_Iic, mem_setOf_eq]

Premises used: Set.mem_setOf_eq, Set.compl_Iic
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
h : Set Prop
hs : Membership.mem (γ := Set (Set Prop)) {∅, {True}} h
⊢ Membership.mem (γ := Set (Set Prop)) {Ioi True, Ioi False} h

Tactic:
rw [← Ioi_True, ← Ioi_False] at hs

Premises used: Set.Ioi_True, Set.Ioi_False
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
h : Set Prop
hs : Membership.mem (γ := Set (Set Prop)) {Ioi True, Ioi False} h
inl : ∃ (a : Prop), Ioi a = Ioi True
inr : ∃ (a : Prop), Ioi a = Ioi False
⊢ ∃ (a : Prop), Ioi a = h

Tactic:
rcases hs with (rfl | rfl)

Premises used: rfl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
w : Prop
h : Ioi True = Ioi True
⊢ ∃ (a : Prop), Ioi a = Ioi True

Tactic:
use True

Premises used: True
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
w : Prop
h : Ioi False = Ioi False
⊢ ∃ (a : Prop), Ioi a = Ioi False

Tactic:
use False

Premises used: False
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
a : Prop
pos : a → Membership.mem (γ := Set (Set Prop)) {∅, {True}} (Iic a)ᶜ
neg : ¬a → Membership.mem (γ := Set (Set Prop)) {∅, {True}} (Iic a)ᶜ
⊢ Membership.mem (γ := Set (Set Prop)) {∅, {True}} (Iic a)ᶜ

Tactic:
by_cases a
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
a : Prop
h : a
⊢ Membership.mem (γ := Set (Set Prop)) {∅, {True}} (Iic a)ᶜ

Tactic:
aesop (add simp [Ioi, lt_iff_le_not_ge])

Premises used: Set.Ioi, lt_iff_le_not_ge
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
a : Prop
h : ¬a
⊢ Membership.mem (γ := Set (Set Prop)) {∅, {True}} (Iic a)ᶜ

Tactic:
aesop (add simp [Ioi, lt_iff_le_not_ge])

Premises used: Set.Ioi, lt_iff_le_not_ge
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
⊢ Eq (α := Set (Set Prop)) {∅, {True}} {s : Set Prop | ∃ (a : Prop), (Iic a)ᶜ = s}

Tactic:
exact le_antisymm
      (fun h hs => by
        simp only [compl_Iic, mem_setOf_eq]
        rw [← Ioi_True, ← Ioi_False] at hs
        rcases hs with (rfl | rfl)
        · use True
        · use False)
      (by rintro _ ⟨a, rfl⟩; by_cases a <;> aesop (add simp [Ioi, lt_iff_le_not_ge]))

Premises used: le_antisymm
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b
⊢ a ∈ s

Tactic:
have has : a ∈ s := mem_of_mem_nhdsWithin self_mem_Ici hs
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b
has : a ∈ s
⊢ ContinuousWithinAt f (Ici a) a

Tactic:
tendsto_order.2 ⟨fun b hb => ?_, fun b hb => ?_⟩

Premises used: Iff.mpr, ContinuousWithinAt, tendsto_order, And.intro
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b
has : a ∈ s
refine_1 : ∀ (b : β) (hb : b < f a), ∀ᶠ (b_1 : α) in 𝓝[≥] a, b < f b_1
refine_2 : ∀ (b : β) (hb : b > f a), ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b
⊢ ContinuousWithinAt f (Ici a) a

Tactic:
refine tendsto_order.2 ⟨fun b hb => ?_, fun b hb => ?_⟩

Premises used: Iff.mpr, tendsto_order, And.intro
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b
has : a ∈ s
b : β
hb : b < f a
a_1 : α
hxs : a_1 ∈ s
hxa : a_1 ∈ Ici a
⊢ b < f a_1

Tactic:
hb.trans_le
      ((h_mono.le_iff_le has hxs).2 hxa)

Premises used: Iff.mpr, LT.lt.trans_le, StrictMonoOn.le_iff_le
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b
has : a ∈ s
b : β
hb : b < f a
h :
  ∀ (a_1 : α),
    Membership.mem (γ := Set α)
      {x : α |
        x ∈ s →
          Membership.mem (γ := Set α)
            {x : α | x ∈ Ici a → Membership.mem (γ := Set α) {x : α | (fun (b_1 : α) ↦ b < f b_1) x} x} x}
      a_1
h₁ h₂ : ∀ (a_1 : α) (hxs : a_1 ∈ s) (hxa : a_1 ∈ Ici a), b < f a_1
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, b < f b_1

Tactic:
filter_upwards [hs, @self_mem_nhdsWithin _ _ a (Ici a)] with _ hxs hxa using hb.trans_le
      ((h_mono.le_iff_le has hxs).2 hxa)

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b
has : a ∈ s
b : β
hb : b > f a
refine_2 : ∀ (c : α) (hcs : c ∈ s) (hac : f a < f c) (hcb : f c ≤ b), ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b

Tactic:
rcases hfs b hb with ⟨c, hcs, hac, hcb⟩
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : f a < f c
hcb : f c ≤ b
⊢ a < c

Tactic:
rw [h_mono.lt_iff_lt has hcs] at hac

Premises used: StrictMonoOn.lt_iff_lt