awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
b c : α
h : Iio (min b c) = (Ici b)ᶜ ∩ (Ici c)ᶜ
⊢ (Ici (min b c))ᶜ = (Ici b)ᶜ ∩ (Ici c)ᶜ
have h₁ : Iio (min b c) = Iio b ∩ (Ici c)ᶜ
Tactic: rw [compl_Ici, compl_Ici, compl_Ici, Iio_inter_Iio]
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
b c : α
h : Iio (min b c) = (Ici b)ᶜ ∩ (Ici c)ᶜ
h₁ : Iio (min b c) = Iio b ∩ (Ici c)ᶜ
⊢ (Ici (min b c))ᶜ = (Ici b)ᶜ ∩ (Ici c)ᶜ
have h₂ : Iio (min b c) = Iio b ∩ Iio c
Tactic: rw [compl_Ici, compl_Ici, compl_Ici, Iio_inter_Iio]
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
b c : α
h : Iio (min b c) = (Ici b)ᶜ ∩ (Ici c)ᶜ
h₁ : Iio (min b c) = Iio b ∩ (Ici c)ᶜ
h₂ : Iio (min b c) = Iio b ∩ Iio c
⊢ (Ici (min b c))ᶜ = (Ici b)ᶜ ∩ (Ici c)ᶜ
have h₃ : Iio (min b c) = Iio (min b c)
Tactic: rw [compl_Ici, compl_Ici, compl_Ici, Iio_inter_Iio]
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
⊢ IsOpen[t] U ↔ U = univ ∨ ∃ (a : α), (Ici a)ᶜ = U
have pos : ∀ (hU : U = univ), IsOpen[t] U ↔ U = univ ∨ ∃ (a : α), (Ici a)ᶜ = U
Tactic: by_cases hU : U = univ
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
pos : ∀ (hU : U = univ), IsOpen[t] U ↔ U = univ ∨ ∃ (a : α), (Ici a)ᶜ = U
⊢ IsOpen[t] U ↔ U = univ ∨ ∃ (a : α), (Ici a)ᶜ = U
have neg : ∀ (hU : ¬U = univ), IsOpen[t] U ↔ U = univ ∨ ∃ (a : α), (Ici a)ᶜ = U
Tactic: by_cases hU : U = univ
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
⊢ IsOpen[t] U ↔ U = univ ∨ ∃ (a : α), (Ici a)ᶜ = U
have neg : IsOpen[t] U → U = univ ∨ ∃ (a : α), (Ici a)ᶜ = U
Tactic: refine ⟨?_, isTopologicalBasis_insert_univ_subbasis.isOpen⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
⊢ U = univ ∨ ∃ (a : α), (Ici a)ᶜ = U
have neg : ∃ (a : α), (Ici a)ᶜ = U
Tactic: apply Or.inr
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
⊢ ∃ (a : α), (Ici a)ᶜ = U
have a : (∃ (a : α), (Ici a)ᶜ = U) ↔ ∃ S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}, U = ⋃₀ S
Tactic: convert! IsTopologicalBasis.open_eq_sUnion isTopologicalBasis_insert_univ_subbasis hO
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
⊢ (∃ (a : α), (Ici a)ᶜ = U) ↔ ∃ S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}, U = ⋃₀ S
have a : (∃ (a : α), (Ici a)ᶜ = U) → ∃ S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}, U = ⋃₀ S
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
a : (∃ (a : α), (Ici a)ᶜ = U) → ∃ S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}, U = ⋃₀ S
⊢ (∃ (a : α), (Ici a)ᶜ = U) ↔ ∃ S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}, U = ⋃₀ S
have a₁ : (∃ S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}, U = ⋃₀ S) → ∃ (a : α), (Ici a)ᶜ = U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
a : α
ha : (Ici a)ᶜ = U
⊢ ∃ S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}, U = ⋃₀ S
have h : Subset (α := Set (Set α)) {U} (insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}) ∧ U = ⋃₀ {U}
Tactic: use {U}
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
a : α
ha : (Ici a)ᶜ = U
⊢ Subset (α := Set (Set α)) {U} (insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}) ∧ U = ⋃₀ {U}
have h : Subset (α := Set (Set α)) {U} (insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s})
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
a : α
ha : (Ici a)ᶜ = U
h : Subset (α := Set (Set α)) {U} (insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s})
⊢ Subset (α := Set (Set α)) {U} (insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}) ∧ U = ⋃₀ {U}
have h₁ : U = ⋃₀ {U}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
a : α
ha : (Ici a)ᶜ = U
⊢ Subset (α := Set (Set α)) {U} (insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s})
have apply : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), (Ici a)ᶜ = s} U
Tactic: apply subset_trans (singleton_subset_iff.mpr _) (subset_insert _ _)
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
a : α
ha : (Ici a)ᶜ = U
⊢ U = ⋃₀ {U}
have h : U = U
Tactic: rw [sUnion_singleton]
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS' : univ ∈ S
⊢ False
have apply : U = univ
Tactic: apply hU
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS' : univ ∈ S
⊢ U = univ
have rw : ⋃₀ S = univ
Tactic: rw [hS2]
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (hypothesis)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
⊢ ∃ (a : α), (Ici a)ᶜ = U
have hUS : univ ∉ S
Tactic: have hUS : univ ∉ S := by
      by_contra hUS'
      apply hU
      rw [hS2]
      exact sUnion_eq_univ_iff.mpr (fun a => ⟨univ, hUS', trivial⟩)
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
⊢ ∃ (a : α), (Ici a)ᶜ = U
have h : (Ici (sSup {a : α | (Ici a)ᶜ ∈ S}))ᶜ = U
Tactic: use sSup {a | (Ici a)ᶜ ∈ S}
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
⊢ (Ici (sSup {a : α | (Ici a)ᶜ ∈ S}))ᶜ = U
have h : Ici (sSup {a : α | (Ici a)ᶜ ∈ S}) = ⋂₀ (compl '' S)
Tactic: rw [hS2, sUnion_eq_compl_sInter_compl, compl_inj_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
⊢ Ici (sSup {a : α | (Ici a)ᶜ ∈ S}) = ⋂₀ (compl '' S)
have h : Ici (sSup {a : α | (Ici a)ᶜ ∈ S}) ≤ ⋂₀ (compl '' S)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
h : Ici (sSup {a : α | (Ici a)ᶜ ∈ S}) ≤ ⋂₀ (compl '' S)
⊢ Ici (sSup {a : α | (Ici a)ᶜ ∈ S}) = ⋂₀ (compl '' S)
have h₁ : ⋂₀ (compl '' S) ≤ Ici (sSup {a : α | (Ici a)ᶜ ∈ S})
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b : α
hb : Membership.mem (γ := Set α) (Ici (sSup {a : α | (Ici a)ᶜ ∈ S})) b
⊢ b ∈ ⋂₀ (compl '' S)
have h : ∀ (i : Set α) (i_1 : i ∈ S), b ∉ i
Tactic: simp only [sInter_image, mem_iInter, mem_compl_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b : α
hb : Membership.mem (γ := Set α) (Ici (sSup {a : α | (Ici a)ᶜ ∈ S})) b
s : Set α
hs : s ∈ S
⊢ b ∉ s
have h : ∀ (a : α) (ha : (Ici a)ᶜ = s), b ∉ s
Tactic: obtain ⟨a, ha⟩ := (subset_insert_iff_of_notMem hUS).mp hS1 hs
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b : α
hb : Membership.mem (γ := Set α) (Ici (sSup {a : α | (Ici a)ᶜ ∈ S})) b
s : Set α
hs : s ∈ S
a : α
ha : (Ici a)ᶜ = s
⊢ b ∉ s
have h : ∀ (hU : ¬⋃₀ S = univ) (hO : IsOpen[t] (⋃₀ S)) (hs : (Ici a)ᶜ ∈ S), b ∉ (Ici a)ᶜ
Tactic: subst hS2 ha
Cleared hypotheses: U, hU, hO, hS2, s, hs, ha
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b : α
hb : b ∈ ⋂₀ (compl '' S)
⊢ Membership.mem (γ := Set α) (Ici (sSup {a : α | (Ici a)ᶜ ∈ S})) b
have h : ∀ (b_1 : α), Membership.mem (γ := Set α) {a : α | (Ici a)ᶜ ∈ S} b_1 → b_1 ≤ b
Tactic: rw [mem_Ici, sSup_le_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (hypothesis)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b : α
hb : b ∈ ⋂₀ (compl '' S)
c : α
hc : Membership.mem (γ := Set α) {a : α | (Ici a)ᶜ ∈ S} c
⊢ c ≤ b
have hb₁ : ∀ (i : Set α) (i_1 : i ∈ S), b ∈ iᶜ
Tactic: simp only [sInter_image, mem_iInter] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b c : α
hc : Membership.mem (γ := Set α) {a : α | (Ici a)ᶜ ∈ S} c
hb : ∀ (i : Set α) (i_1 : i ∈ S), b ∈ iᶜ
⊢ c ≤ b
have h : b ∉ (Ici c)ᶜ
Tactic: rw [← not_lt, ← mem_Iio, ← compl_Ici]
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsUpper α
s : Set α
⊢ IsOpen[inst_1] s ↔ GenerateOpen {t : Set α | ∃ (a : α), (Iic a)ᶜ = t} s
have rw : IsOpen[upper α] s ↔ GenerateOpen {t : Set α | ∃ (a : α), (Iic a)ᶜ = t} s
Tactic: rw [topology_eq α]
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
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 (α × β))
have refine_1 : ∀ (s : Set (α × β)),
  Membership.mem (γ := Set (Set (α × β))) {s : Set (α × β) | ∃ (a : α × β), (Ici a)ᶜ = s} s →
    IsOpen[instTopologicalSpaceProd] s
Tactic: refine le_antisymm (le_generateFrom ?_) ?_
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
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
⊢ Eq (α := TopologicalSpace (α × β)) instTopologicalSpaceProd (lower (α × β))
have refine_2 : LE.le (α := TopologicalSpace (α × β)) (lower (α × β)) instTopologicalSpaceProd
Tactic: refine le_antisymm (le_generateFrom ?_) ?_
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
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 β
⊢ LE.le (α := TopologicalSpace (α × β)) (lower (α × β)) instTopologicalSpaceProd
have refine_2 : ∀ x ∈ IsLower.lowerBasis α,
  ∀ y ∈ IsLower.lowerBasis β,
    Membership.mem (γ := Set (Set (α × β))) {s : Set (α × β) | IsOpen[lower (α × β)] s} (x ×ˢ y)
Tactic: rw [(IsLower.isTopologicalBasis.prod
      IsLower.isTopologicalBasis).eq_generateFrom, le_generateFrom_iff_subset_isOpen,
      image2_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
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
⊢ IsOpen[lower (α × β)] ((↑(upperClosure s) : Set α)ᶜ ×ˢ (↑(upperClosure t) : Set β)ᶜ)
have refine_2 : IsOpen[lower (α × β)] ((⋂ i ∈ s, (Prod.fst ⁻¹' Ici i)ᶜ) ∩ ⋂ i ∈ t, (Prod.snd ⁻¹' Ici i)ᶜ)
Tactic: simp_rw [coe_upperClosure, compl_iUnion, prod_eq, preimage_iInter, preimage_compl]
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
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)ᶜ)
have refine_2 : ∀ a ∈ s, IsOpen[lower (α × β)] (Prod.fst ⁻¹' Ici a)ᶜ
Tactic: refine (hs.isOpen_biInter fun a _ => ?_).inter (ht.isOpen_biInter fun b _ => ?_)
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
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)ᶜ
⊢ IsOpen[lower (α × β)] ((⋂ i ∈ s, (Prod.fst ⁻¹' Ici i)ᶜ) ∩ ⋂ i ∈ t, (Prod.snd ⁻¹' Ici i)ᶜ)
have refine_2₁ : ∀ b ∈ t, IsOpen[lower (α × β)] (Prod.snd ⁻¹' Ici b)ᶜ
Tactic: refine (hs.isOpen_biInter fun a _ => ?_).inter (ht.isOpen_biInter fun b _ => ?_)
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
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 β
⊢ Eq (α := TopologicalSpace (α × β)) instTopologicalSpaceProd (upper (α × β))
have suffices : IsLower (α × β)ᵒᵈ
Tactic: suffices IsLower (α × β)ᵒᵈ from IsLower.topology_eq_lowerTopology (α := (α × β)ᵒᵈ)
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
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 : α) → β)
have refine : ∀ (b : β), IsClosed[inst_2] ((⇑f : (a : α) → β) ⁻¹' Ici b)
Tactic: refine IsLower.continuous_iff_Ici.2 fun b => ?_
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
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] ((⇑f : (a : α) → β) ⁻¹' Ici b)
have h : Eq.{u_1 + 1} (α := Set α) ((⇑f : (a : α) → β) ⁻¹' Ici b) (Ici (sInf ((⇑f : (a : α) → β) ⁻¹' Ici b)))
Tactic: convert! isClosed_Ici (a := sInf <| f ⁻¹' Ici b)
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
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)))
have h : ∀ (a : α) (ha : Membership.mem (γ := Set α) (Ici (sInf ((⇑f : (a : α) → β) ⁻¹' Ici b))) a),
  b ≤ ((↑f : α →o β) : (a : α) → β) (sInf ((⇑f : (a : α) → β) ⁻¹' Ici b))
Tactic: refine Subset.antisymm (fun a => sInf_le) fun a ha => le_trans ?_ <|
    OrderHomClass.mono (f : α →o β) ha
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
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))
have h : b ≤ sInf (image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) ⁻¹' Ici b))
Tactic: refine LE.le.trans ?_ (map_sInf f _).ge
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
⊢ IsUpper.{u_1} αᵒᵈ ↔ IsLower α
have mp : IsUpper.{u_1} αᵒᵈ → IsLower α
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
mp : IsUpper.{u_1} αᵒᵈ → IsLower α
⊢ IsUpper.{u_1} αᵒᵈ ↔ IsLower α
have mpr : IsLower α → IsUpper.{u_1} αᵒᵈ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
⊢ sierpinskiSpace = upper Prop
have rw : Eq (α := TopologicalSpace Prop) (generateFrom {∅, {True}}) (generateFrom {s : Set Prop | ∃ (a : Prop), (Iic a)ᶜ = s})
Tactic: rw [Topology.upper, sierpinskiSpace, ← generateFrom_insert_empty]
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
⊢ Eq (α := TopologicalSpace Prop) (generateFrom {∅, {True}}) (generateFrom {s : Set Prop | ∃ (a : Prop), (Iic a)ᶜ = s})
have e_g : Eq (α := Set (Set Prop)) {∅, {True}} {s : Set Prop | ∃ (a : Prop), (Iic a)ᶜ = s}
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
h : Set Prop
hs : Membership.mem (γ := Set (Set Prop)) {∅, {True}} h
⊢ Membership.mem (γ := Set (Set Prop)) {s : Set Prop | ∃ (a : Prop), (Iic a)ᶜ = s} h
have simp : ∃ (a : Prop), Ioi a = h
Tactic: simp only [compl_Iic, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (hypothesis)
Goal:
h : Set Prop
hs : Membership.mem (γ := Set (Set Prop)) {∅, {True}} h
⊢ ∃ (a : Prop), Ioi a = h
have hs₁ : Membership.mem (γ := Set (Set Prop)) {Ioi True, Ioi False} h
Tactic: rw [← Ioi_True, ← Ioi_False] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
h : Set Prop
hs : Membership.mem (γ := Set (Set Prop)) {Ioi True, Ioi False} h
⊢ ∃ (a : Prop), Ioi a = h
have inl : ∃ (a : Prop), Ioi a = Ioi True
Tactic: rcases hs with (rfl | rfl)
Cleared hypotheses: h, hs
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
h : Set Prop
hs : Membership.mem (γ := Set (Set Prop)) {Ioi True, Ioi False} h
inl : ∃ (a : Prop), Ioi a = Ioi True
⊢ ∃ (a : Prop), Ioi a = h
have inr : ∃ (a : Prop), Ioi a = Ioi False
Tactic: rcases hs with (rfl | rfl)
Cleared hypotheses: h, hs
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
⊢ ∃ (a : Prop), Ioi a = Ioi True
have w : Prop
Tactic: use True
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
w : Prop
⊢ ∃ (a : Prop), Ioi a = Ioi True
have h : Ioi True = Ioi True
Tactic: use True
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
⊢ ∃ (a : Prop), Ioi a = Ioi False
have w : Prop
Tactic: use False
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
w : Prop
⊢ ∃ (a : Prop), Ioi a = Ioi False
have h : Ioi False = Ioi False
Tactic: use False
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
a : Prop
⊢ Membership.mem (γ := Set (Set Prop)) {∅, {True}} (Iic a)ᶜ
have pos : a → Membership.mem (γ := Set (Set Prop)) {∅, {True}} (Iic a)ᶜ
Tactic: by_cases a
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
a : Prop
pos : a → Membership.mem (γ := Set (Set Prop)) {∅, {True}} (Iic a)ᶜ
⊢ Membership.mem (γ := Set (Set Prop)) {∅, {True}} (Iic a)ᶜ
have neg : ¬a → Membership.mem (γ := Set (Set Prop)) {∅, {True}} (Iic a)ᶜ
Tactic: by_cases a
-- Lean 4 proof step from Mathlib.Topology.Order.MonotoneContinuity (hypothesis)
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
⊢ ContinuousWithinAt f (Ici a) a
have has : a ∈ s
Tactic: have has : a ∈ s := mem_of_mem_nhdsWithin self_mem_Ici hs
-- Lean 4 proof step from Mathlib.Topology.Order.MonotoneContinuity (goal)
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
have refine_1 : ∀ (b : β) (hb : b < f a), ∀ᶠ (b_1 : α) in 𝓝[≥] a, b < f b_1
Tactic: refine tendsto_order.2 ⟨fun b hb => ?_, fun b hb => ?_⟩