awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
this :
  ∀
    (hf :
      ContinuousOn (X := αᵒᵈ) (f ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → β)
        (Ioo ((OrderDual.toDual : (a : α) → αᵒᵈ) b) ((OrderDual.toDual : (a : α) → αᵒᵈ) a) : Set αᵒᵈ))
    (ha :
      Tendsto (α := αᵒᵈ) (f ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → β)
        (𝓝[>] (OrderDual.toDual : (a : α) → αᵒᵈ) b : Filter αᵒᵈ) (𝓝 lb)),
    ContinuousOn (X := αᵒᵈ)
      (extendFrom (Ioo ((OrderDual.toDual : (a : α) → αᵒᵈ) b) ((OrderDual.toDual : (a : α) → αᵒᵈ) a))
          (f ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α)) :
        αᵒᵈ → β)
      (Ico ((OrderDual.toDual : (a : α) → αᵒᵈ) b) ((OrderDual.toDual : (a : α) → αᵒᵈ) a) : Set αᵒᵈ)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b)
have this₁ : ∀
  (hf :
    ContinuousOn (X := αᵒᵈ) (f ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α)) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioo a b))
  (ha :
    Tendsto (α := αᵒᵈ) (f ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → β)
      (𝓝[(⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Iio b] (OrderDual.toDual : (a : α) → αᵒᵈ) b : Filter αᵒᵈ) (𝓝 lb)),
  ContinuousOn (X := αᵒᵈ)
    (extendFrom ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioo a b) (f ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α)))
    ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioc a b)
Tactic: rw [Ico_toDual, Ioi_toDual, Ioo_toDual] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la : β
inst_5 : T2Space β
hab : a < b
ha : Tendsto f (𝓝[>] a) (𝓝 la)
⊢ extendFrom (Ioo a b) f a = la
have hx : a ∈ closure[inst] (Ioo a b)
Tactic: apply extendFrom_eq
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la : β
inst_5 : T2Space β
hab : a < b
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hx : a ∈ closure[inst] (Ioo a b)
⊢ extendFrom (Ioo a b) f a = la
have hf : Tendsto f (𝓝[Ioo a b] a) (𝓝 la)
Tactic: apply extendFrom_eq
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la : β
inst_5 : T2Space β
hab : a < b
ha : Tendsto f (𝓝[>] a) (𝓝 la)
⊢ a ∈ closure[inst] (Ioo a b)
have hx : a ∈ Icc a b
Tactic: rw [closure_Ioo hab.ne]
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
lb : β
inst_5 : T2Space β
hab : a < b
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
⊢ extendFrom (Ioo a b) f b = lb
have hx : b ∈ closure[inst] (Ioo a b)
Tactic: apply extendFrom_eq
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
lb : β
inst_5 : T2Space β
hab : a < b
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hx : b ∈ closure[inst] (Ioo a b)
⊢ extendFrom (Ioo a b) f b = lb
have hf : Tendsto f (𝓝[Ioo a b] b) (𝓝 lb)
Tactic: apply extendFrom_eq
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
lb : β
inst_5 : T2Space β
hab : a < b
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
⊢ b ∈ closure[inst] (Ioo a b)
have hx : b ∈ Icc a b
Tactic: rw [closure_Ioo hab.ne]
-- Lean 4 proof step from Mathlib.Topology.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hf : IsNormal f
⊢ Continuous f
have rw : ∀ (a : β), IsOpen (f ⁻¹' Ioi a) ∧ IsOpen (f ⁻¹' Iio a)
Tactic: rw [OrderTopology.continuous_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hf : IsNormal f
⊢ ∀ (a : β), IsOpen (f ⁻¹' Ioi a) ∧ IsOpen (f ⁻¹' Iio a)
have refine : ∀ (b : β), IsOpen (f ⁻¹' Ioi b)
Tactic: refine fun b ↦ ⟨?_, ((isLowerSet_Iio b).preimage hf.strictMono.monotone).isOpen⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hf : IsNormal f
b : β
⊢ IsOpen (f ⁻¹' Ioi b)
have rw : IsClosed (f ⁻¹' Iic b)
Tactic: rw [← isClosed_compl_iff, ← Set.preimage_compl, Set.compl_Ioi]
-- Lean 4 proof step from Mathlib.Topology.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hf : IsNormal f
b : β
⊢ IsClosed (f ⁻¹' Iic b)
have inl : ∀ (ha : f ⁻¹' Iic b = univ), IsClosed (f ⁻¹' Iic b)
Tactic: obtain ha | ⟨a, ha⟩ := ((isLowerSet_Iic b).preimage hf.strictMono.monotone).eq_univ_or_Iio
-- Lean 4 proof step from Mathlib.Topology.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hf : IsNormal f
b : β
inl : ∀ (ha : f ⁻¹' Iic b = univ), IsClosed (f ⁻¹' Iic b)
⊢ IsClosed (f ⁻¹' Iic b)
have inr : ∀ (a : α) (ha : f ⁻¹' Iic b = Iio a), IsClosed (f ⁻¹' Iic b)
Tactic: obtain ha | ⟨a, ha⟩ := ((isLowerSet_Iic b).preimage hf.strictMono.monotone).eq_univ_or_Iio
-- Lean 4 proof step from Mathlib.Topology.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
⊢ IsClosed (f ⁻¹' Iic b)
have inr : ∀ (h : f ⁻¹' Iic b = ∅), IsClosed (f ⁻¹' Iic b)
Tactic: obtain h | h := (f ⁻¹' Iic b).eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Topology.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
inr : ∀ (h : f ⁻¹' Iic b = ∅), IsClosed (f ⁻¹' Iic b)
⊢ IsClosed (f ⁻¹' Iic b)
have inr₁ : ∀ (h : (f ⁻¹' Iic b).Nonempty), IsClosed (f ⁻¹' Iic b)
Tactic: obtain h | h := (f ⁻¹' Iic b).eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Topology.Order.IsNormal (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
h : (f ⁻¹' Iic b).Nonempty
⊢ IsClosed (f ⁻¹' Iic b)
have this : Nonempty α
Tactic: have : Nonempty α := ⟨a⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IsNormal (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
h : (f ⁻¹' Iic b).Nonempty
this : Nonempty α
⊢ IsClosed (f ⁻¹' Iic b)
have this₁ : Nonempty β
Tactic: have : Nonempty β := ⟨b⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
h : (f ⁻¹' Iic b).Nonempty
this_1 : Nonempty α
this : Nonempty β
⊢ IsClosed (f ⁻¹' Iic b)
have inr : IsClosed (Iic (sSup (f ⁻¹' Iic b)))
Tactic: rw [hf.preimage_Iic h (ha ▸ bddAbove_Iio)]
-- Lean 4 proof step from Mathlib.Topology.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hs : StrictMono f
hc : Continuous f
⊢ IsNormal f
have refine_1 : ∀ {a : α} (ha : IsSuccLimit a), f a ∈ upperBounds (f '' Iio a)
Tactic: refine ⟨hs, fun {a} ha ↦ (isLUB_of_mem_closure ?_ ?_).2⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hs : StrictMono f
hc : Continuous f
refine_1 : ∀ {a : α} (ha : IsSuccLimit a), f a ∈ upperBounds (f '' Iio a)
⊢ IsNormal f
have refine_2 : ∀ {a : α} (ha : IsSuccLimit a), f a ∈ closure (f '' Iio a)
Tactic: refine ⟨hs, fun {a} ha ↦ (isLUB_of_mem_closure ?_ ?_).2⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hs : StrictMono f
hc : Continuous f
a : α
ha : IsSuccLimit a
⊢ f a ∈ closure (f '' Iio a)
have apply : a ∈ closure (Iio a)
Tactic: apply image_closure_subset_closure_image hc (mem_image_of_mem ..)
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s : Set α
⊢ IsOpen[inst_1] s ↔ GenerateOpen {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} s
have rw : IsOpen[lower α] s ↔ GenerateOpen {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} s
Tactic: rw [topology_eq α]
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s : Set α
h : s.Finite
⊢ IsClosed[inst_1] (↑(upperClosure s) : Set α)
have simp : IsClosed[inst_1] (⋃ i ∈ s, (↑(UpperSet.Ici i) : Set α))
Tactic: simp only [← UpperSet.iInf_Ici, UpperSet.coe_iInf]
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s : Set α
h : IsOpen[inst_1] s
⊢ IsLowerSet s
have h₁ : GenerateOpen {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} s
Tactic: replace h := isOpen_iff_generate_Ici_compl.1 h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s u : Set α
h' : Membership.mem (γ := Set (Set α)) {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} u
⊢ IsLowerSet u
have basic : ∀ (a : α), IsLowerSet (Ici a)ᶜ
Tactic: obtain ⟨a, rfl⟩ := h'
Cleared hypotheses: u, h'
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s : Set α
h : GenerateOpen {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} s
⊢ IsLowerSet s
have basic : ∀ (u : Set α) (h' : Membership.mem (γ := Set (Set α)) {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} u), IsLowerSet u
Tactic: induction h with
  | basic u h' => obtain ⟨a, rfl⟩ := h'; exact (isUpperSet_Ici a).compl
  | univ => exact isLowerSet_univ
  | inter u v _ _ hu2 hv2 => exact hu2.inter hv2
  | sUnion _ _ ih => exact isLowerSet_sUnion ih
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s : Set α
h : GenerateOpen {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} s
basic : ∀ (u : Set α) (h' : Membership.mem (γ := Set (Set α)) {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} u), IsLowerSet u
⊢ IsLowerSet s
have univ : IsLowerSet.{u_1} (α := α) univ
Tactic: induction h with
  | basic u h' => obtain ⟨a, rfl⟩ := h'; exact (isUpperSet_Ici a).compl
  | univ => exact isLowerSet_univ
  | inter u v _ _ hu2 hv2 => exact hu2.inter hv2
  | sUnion _ _ ih => exact isLowerSet_sUnion ih
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s : Set α
h : GenerateOpen {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} s
basic : ∀ (u : Set α) (h' : Membership.mem (γ := Set (Set α)) {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} u), IsLowerSet u
univ : IsLowerSet.{u_1} (α := α) Set.univ
⊢ IsLowerSet s
have inter : ∀ (u v : Set α),
  GenerateOpen {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} u →
    GenerateOpen {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} v →
      ∀ (hu2 : IsLowerSet u) (hv2 : IsLowerSet v), IsLowerSet (u ∩ v)
Tactic: induction h with
  | basic u h' => obtain ⟨a, rfl⟩ := h'; exact (isUpperSet_Ici a).compl
  | univ => exact isLowerSet_univ
  | inter u v _ _ hu2 hv2 => exact hu2.inter hv2
  | sUnion _ _ ih => exact isLowerSet_sUnion ih
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s : Set α
h : GenerateOpen {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} s
basic : ∀ (u : Set α) (h' : Membership.mem (γ := Set (Set α)) {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} u), IsLowerSet u
univ : IsLowerSet.{u_1} (α := α) Set.univ
inter :
  ∀ (u v : Set α),
    GenerateOpen {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} u →
      GenerateOpen {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} v →
        ∀ (hu2 : IsLowerSet u) (hv2 : IsLowerSet v), IsLowerSet (u ∩ v)
⊢ IsLowerSet s
have sUnion : ∀ (S : Set (Set α)),
  (∀ s ∈ S, GenerateOpen {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} s) → ∀ (ih : ∀ s ∈ S, IsLowerSet s), IsLowerSet (⋃₀ S)
Tactic: induction h with
  | basic u h' => obtain ⟨a, rfl⟩ := h'; exact (isUpperSet_Ici a).compl
  | univ => exact isLowerSet_univ
  | inter u v _ _ hu2 hv2 => exact hu2.inter hv2
  | sUnion _ _ ih => exact isLowerSet_sUnion ih
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
⊢ IsTopologicalBasis (lowerBasis α)
have h : lowerBasis α =
  (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}}
Tactic: convert! isTopologicalBasis_of_subbasis (topology_eq α)
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
⊢ lowerBasis α =
    (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}}
have h : Eq.{u_1 + 1} (α := Set (Set α)) {s : Set α | ∃ (t : Set α), t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s}
  ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}})
Tactic: simp_rw [lowerBasis, coe_upperClosure, compl_iUnion]
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
⊢ Eq.{u_1 + 1} (α := Set (Set α)) {s : Set α | ∃ (t : Set α), t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s}
    ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}})
have h : ∀ (s : Set α),
  Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (t : Set α), t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s} s ↔
    Membership.mem (γ := Set (Set α))
      ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}}) s
Tactic: ext s
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s : Set α
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (t : Set α), t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s} s ↔
    Membership.mem (γ := Set (Set α))
      ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}}) s
have h : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (t : Set α), t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s} s →
  Membership.mem (γ := Set (Set α))
    ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}}) s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s : Set α
h :
  Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (t : Set α), t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s} s →
    Membership.mem (γ := Set (Set α))
      ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}}) s
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (t : Set α), t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s} s ↔
    Membership.mem (γ := Set (Set α))
      ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}}) s
have h₁ : Membership.mem (γ := Set (Set α))
    ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}}) s →
  Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (t : Set α), t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s} s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
F : Set α
hF : F.Finite
⊢ Membership.mem (γ := Set (Set α))
    ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}})
    (⋂ i ∈ F, (Ici i)ᶜ)
have h : Eq.{u_1 + 1} (α := Set α) ((fun (f : Set (Set α)) ↦ ⋂₀ f) ((fun (a : α) ↦ (Ici a)ᶜ) '' F)) (⋂ i ∈ F, (Ici i)ᶜ)
Tactic: refine ⟨(fun a => (Ici a)ᶜ) '' F, ⟨hF.image _, image_subset_iff.2 fun _ _ => ⟨_, rfl⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
F : Set (Set α)
hF : F.Finite
hs : F ⊆ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (t : Set α), t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s}
    ((fun (f : Set (Set α)) ↦ ⋂₀ f) F)
have this : Finite.{u_1 + 1} (↑F : Type u_1)
Tactic: haveI := hF.to_subtype
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
F : Set (Set α)
hF : F.Finite
hs : F ⊆ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
this : Finite.{u_1 + 1} (↑F : Type u_1)
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (t : Set α), t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s}
    ((fun (f : Set (Set α)) ↦ ⋂₀ f) F)
have hs₁ : ∀ (x : { a : Set α // a ∈ F }), Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), (Ici a)ᶜ = s} (↑x : Set α)
Tactic: rw [subset_def, Subtype.forall'] at hs
Cleared hypotheses: hs, this
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
F : Set (Set α)
hF : F.Finite
hs :
  ∀ (x : { a : Set α // a ∈ F }), Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), (Ici a)ᶜ = s} (↑x : Set α)
this : Finite.{u_1 + 1} (↑F : Type u_1)
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (t : Set α), t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s}
    ((fun (f : Set (Set α)) ↦ ⋂₀ f) F)
have h : ∀ (f : (x : { a : Set α // a ∈ F }) → α) (hf : ∀ (x : { a : Set α // a ∈ F }), (Ici (f x))ᶜ = (↑x : Set α)),
  Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (t : Set α), t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s}
    ((fun (f : Set (Set α)) ↦ ⋂₀ f) F)
Tactic: choose f hf using hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
F : Set (Set α)
hF : F.Finite
this : Finite.{u_1 + 1} (↑F : Type u_1)
f : (x : { a : Set α // a ∈ F }) → α
hf : ∀ (x : { a : Set α // a ∈ F }), (Ici (f x))ᶜ = (↑x : Set α)
simp_rw simp_rw₁ : ⋂ i ∈ range f, (Ici i)ᶜ = ⋂₀ F
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ i ∈ range f, (Ici i)ᶜ) ((fun (f : Set (Set α)) ↦ ⋂₀ f) F)
have simp_rw₂ : ⋂ (y : { a : Set α // a ∈ F }), (Ici (f y))ᶜ = ⋂₀ F
Tactic: simp_rw [biInter_range, hf, sInter_eq_iInter]
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
F : Set (Set α)
hF : F.Finite
this : Finite.{u_1 + 1} (↑F : Type u_1)
f : (x : { a : Set α // a ∈ F }) → α
hf : ∀ (x : { a : Set α // a ∈ F }), (Ici (f x))ᶜ = (↑x : Set α)
simp_rw simp_rw₁ : ⋂ i ∈ range f, (Ici i)ᶜ = ⋂₀ F
simp_rw₂ : ⋂ (y : { a : Set α // a ∈ F }), (Ici (f y))ᶜ = ⋂₀ F
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ i ∈ range f, (Ici i)ᶜ) ((fun (f : Set (Set α)) ↦ ⋂₀ f) F)
have simp_rw₃ : ⋂ (y : { a : Set α // a ∈ F }), (↑y : Set α) = ⋂₀ F
Tactic: simp_rw [biInter_range, hf, sInter_eq_iInter]
-- 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 : TopologicalSpace β
f : β → α
⊢ Continuous[inst_3, inst_1] f ↔ ∀ (a : α), IsClosed[inst_3] (f ⁻¹' Ici a)
have obtain : ∀ [IsLower α], Continuous[inst_3, lower α] f ↔ ∀ (a : α), IsClosed[inst_3] (f ⁻¹' Ici a)
Tactic: obtain rfl := IsLower.topology_eq α
Cleared hypotheses: inst_1, inst_2
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
⊢ inst_1 = generateFrom {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
have rw : lower α = generateFrom {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
Tactic: rw [topology_eq α, lower]
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
rw : lower α = generateFrom {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
⊢ inst_1 = generateFrom {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
have rw₁ : Eq.{u_1 + 1} (α := TopologicalSpace α) (generateFrom {s : Set α | ∃ (a : α), (Ici a)ᶜ = s})
  (generateFrom {s : Set α | ∃ (a : α), (Ici a)ᶜ = s})
Tactic: rw [topology_eq α, lower]
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
b c : α
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), (Ici a)ᶜ = s} ((Ici b)ᶜ ∩ (Ici c)ᶜ)
have h : (Ici (min b c))ᶜ = (Ici b)ᶜ ∩ (Ici c)ᶜ
Tactic: use b ⊓ c
-- Lean 4 proof step from Mathlib.Topology.Order.LowerUpperTopology (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
b c : α
⊢ (Ici (min b c))ᶜ = (Ici b)ᶜ ∩ (Ici c)ᶜ
have h : Iio (min b c) = (Ici b)ᶜ ∩ (Ici c)ᶜ
Tactic: rw [compl_Ici, compl_Ici, compl_Ici, Iio_inter_Iio]