awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst_1] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
have pos : ∀ (H : Disjoint (Icc a b) (s.ordSeparatingSet t).ordConnectedSection),
  (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
Tactic: by_cases H : Disjoint (Icc a b) (ordConnectedSection <| ordSeparatingSet s t)
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst_1] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
pos :
  ∀ (H : Disjoint (Icc a b) (s.ordSeparatingSet t).ordConnectedSection),
    (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
have neg : ∀ (H : ¬Disjoint (Icc a b) (s.ordSeparatingSet t).ordConnectedSection),
  (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
Tactic: by_cases H : Disjoint (Icc a b) (ordConnectedSection <| ordSeparatingSet s t)
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (hypothesis)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst_1] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
H : ¬Disjoint (Icc a b) (s.ordSeparatingSet t).ordConnectedSection
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
have H₁ : ∃ (x : X) (_ : x ∈ Icc a b), x ∈ (s.ordSeparatingSet t).ordConnectedSection
Tactic: simp only [Set.disjoint_left, not_forall, Classical.not_not] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst_1] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
H : ∃ (x : X) (_ : x ∈ Icc a b), x ∈ (s.ordSeparatingSet t).ordConnectedSection
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
have neg : ∀ (c : X) (hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection) (hac : a ≤ c) (hcb : c ≤ b),
  (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
Tactic: rcases H with ⟨c, ⟨hac, hcb⟩, hc⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (hypothesis)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst_1] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hac : a ≤ c
hcb : c ≤ b
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
have hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
Tactic: have hsub' : Icc a b ⊆ ordConnectedComponent tᶜ a :=
      subset_ordConnectedComponent (left_mem_Icc.2 hab) hsub
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (hypothesis)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst_1] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hac : a ≤ c
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
have hd₁ : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
Tactic: have hd : Disjoint s (ordConnectedSection (ordSeparatingSet s t)) :=
      disjoint_left_ordSeparatingSet.mono_right ordConnectedSection_subset
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (hypothesis)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd_1 : Disjoint s (closure[inst_1] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hac : a ≤ c
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
have hac₁ : a < c
Tactic: replace hac : a < c := hac.lt_of_ne <| Ne.symm <| ne_of_mem_of_not_mem hc <|
      disjoint_left.1 hd ha
Cleared hypotheses: hac
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd_1 : Disjoint s (closure[inst_1] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
have h : ∀ (x : X) (hx : x ∈ Ico a c) (hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection), False
Tactic: filter_upwards [Ico_mem_nhdsGE hac] with x hx hx'
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd_1 : Disjoint s (closure[inst_1] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
⊢ False
have h : [[x, c]] ⊆ s.ordSeparatingSet t
Tactic: refine hx.2.ne (eq_of_mem_ordConnectedSection_of_uIcc_subset hx' hc ?_)
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd_1 : Disjoint s (closure[inst_1] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
⊢ [[x, c]] ⊆ s.ordSeparatingSet t
have h : [[x, c]] ⊆ tᶜ.ordConnectedComponent a
Tactic: refine subset_inter (subset_iUnion₂_of_subset a ha ?_) ?_
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd_1 : Disjoint s (closure[inst_1] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
h : [[x, c]] ⊆ tᶜ.ordConnectedComponent a
⊢ [[x, c]] ⊆ s.ordSeparatingSet t
have h₁ : [[x, c]] ⊆ ⋃ x ∈ t, sᶜ.ordConnectedComponent x
Tactic: refine subset_inter (subset_iUnion₂_of_subset a ha ?_) ?_
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd_1 : Disjoint s (closure[inst_1] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
⊢ [[x, c]] ⊆ ⋃ x ∈ t, sᶜ.ordConnectedComponent x
have h : ∀ (y : X) (hyt : y ∈ t) (hxy : x ∈ sᶜ.ordConnectedComponent y), [[x, c]] ⊆ ⋃ x ∈ t, sᶜ.ordConnectedComponent x
Tactic: rcases mem_iUnion₂.1 (ordConnectedSection_subset hx').2 with ⟨y, hyt, hxy⟩
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd_1 : Disjoint s (closure[inst_1] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
⊢ [[x, c]] ⊆ ⋃ x ∈ t, sᶜ.ordConnectedComponent x
have h : c ∈ sᶜ.ordConnectedComponent y
Tactic: refine subset_iUnion₂_of_subset y hyt (OrdConnected.uIcc_subset inferInstance hxy ?_)
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd_1 : Disjoint s (closure[inst_1] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
⊢ c ∈ sᶜ.ordConnectedComponent y
have h : c ∈ [[y, x]]
Tactic: refine subset_ordConnectedComponent left_mem_uIcc hxy ?_
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd_1 : Disjoint s (closure[inst_1] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
this : c < y
⊢ c ∈ [[y, x]]
have rw : c ∈ Icc x y
Tactic: rw [uIcc_of_ge (hx.2.trans this).le]
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd_1 : Disjoint s (closure[inst_1] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
⊢ c ∈ [[y, x]]
have h : c < y
Tactic: suffices c < y by
        rw [uIcc_of_ge (hx.2.trans this).le]
        exact ⟨hx.2.le, this.le⟩
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd_1 : Disjoint s (closure[inst_1] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
⊢ c < y
have h : ∀ (hyc : y ≤ c), False
Tactic: refine lt_of_not_ge fun hyc => ?_
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (hypothesis)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd_1 : Disjoint s (closure[inst_1] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
hyc : y ≤ c
⊢ False
have hya : y < a
Tactic: have hya : y < a := not_le.1 fun hay => hsub ⟨hay, hyc.trans hcb⟩ hyt
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (hypothesis)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst_1] t)
ha : a ∈ s
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≤] a
have hd' : Disjoint (α := Set Xᵒᵈ) ((⇑ofDual : (a : Xᵒᵈ) → X) ⁻¹' s)
  (closure[instTopologicalSpace] ((⇑ofDual : (a : Xᵒᵈ) → X) ⁻¹' t))
Tactic: have hd' : Disjoint (ofDual ⁻¹' s) (closure <| ofDual ⁻¹' t) := hd
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (hypothesis)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst_1] t)
ha : a ∈ s
hd' :
  Disjoint (α := Set Xᵒᵈ) ((⇑ofDual : (a : Xᵒᵈ) → X) ⁻¹' s)
    (closure[instTopologicalSpace] ((⇑ofDual : (a : Xᵒᵈ) → X) ⁻¹' t))
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≤] a
have ha' : Membership.mem (α := Xᵒᵈ) (γ := Set Xᵒᵈ) ((⇑ofDual : (a : Xᵒᵈ) → X) ⁻¹' s) ((toDual : (a : X) → Xᵒᵈ) a : Xᵒᵈ)
Tactic: have ha' : toDual a ∈ ofDual ⁻¹' s := ha
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst_1] t)
ha : a ∈ s
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝 a
have rw : (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≤] a ∧ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
Tactic: rw [← nhdsLE_sup_nhdsGE, mem_sup]
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s t : Set X
hd : Disjoint s (closure[inst_1] t)
x : X
hx : x ∈ s
⊢ tᶜ ∈ 𝓝 x
have rw : x ∈ (closure[inst_1] t)ᶜ
Tactic: rw [← mem_interior_iff_mem_nhds, interior_compl]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
⊢ Eq.{u_1 + 1} (α := TopologicalSpace αᵒᵈ) OrderDual.instTopologicalSpace (lowerSet αᵒᵈ)
have a : ∀ (x : Set αᵒᵈ), IsOpen[OrderDual.instTopologicalSpace] x ↔ IsOpen[lowerSet αᵒᵈ] x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
x : Set αᵒᵈ
⊢ IsOpen[OrderDual.instTopologicalSpace] x ↔ IsOpen[lowerSet αᵒᵈ] x
have a : IsOpen[OrderDual.instTopologicalSpace] x ↔ IsOpen[lowerSet αᵒᵈ] x
Tactic: rw [IsUpperSet.topology_eq α]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
⊢ IsOpen[inst_1] s ↔ IsUpperSet s
have rw : IsOpen[upperSet α] s ↔ IsUpperSet s
Tactic: rw [topology_eq α]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
⊢ IsClosed[inst_1] s ↔ IsLowerSet s
have rw : IsOpen[inst_1] sᶜ ↔ IsLowerSet s
Tactic: rw [← isOpen_compl_iff, isOpen_iff_isUpperSet,
    isLowerSet_compl.symm, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
rw : IsOpen[inst_1] sᶜ ↔ IsLowerSet s
⊢ IsClosed[inst_1] s ↔ IsLowerSet s
have rw₁ : IsUpperSet sᶜ ↔ IsLowerSet s
Tactic: rw [← isOpen_compl_iff, isOpen_iff_isUpperSet,
    isLowerSet_compl.symm, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
rw : IsOpen[inst_1] sᶜ ↔ IsLowerSet s
rw₁ : IsUpperSet sᶜ ↔ IsLowerSet s
⊢ IsClosed[inst_1] s ↔ IsLowerSet s
have rw₂ : IsLowerSet sᶜᶜ ↔ IsLowerSet s
Tactic: rw [← isOpen_compl_iff, isOpen_iff_isUpperSet,
    isLowerSet_compl.symm, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
rw : IsOpen[inst_1] sᶜ ↔ IsLowerSet s
rw₁ : IsUpperSet sᶜ ↔ IsLowerSet s
rw₂ : IsLowerSet sᶜᶜ ↔ IsLowerSet s
⊢ IsClosed[inst_1] s ↔ IsLowerSet s
have rw₃ : IsLowerSet s ↔ IsLowerSet s
Tactic: rw [← isOpen_compl_iff, isOpen_iff_isUpperSet,
    isLowerSet_compl.symm, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
⊢ closure[inst_1] s = (↑(lowerClosure s) : Set α)
have rw : closure[inst_1] s ⊆ (↑(lowerClosure s) : Set α) ∧ (↑(lowerClosure s) : Set α) ⊆ closure[inst_1] s
Tactic: rw [subset_antisymm_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
⊢ closure[inst_1] s ⊆ (↑(lowerClosure s) : Set α) ∧ (↑(lowerClosure s) : Set α) ⊆ closure[inst_1] s
have refine : closure[inst_1] s ⊆ (↑(lowerClosure s) : Set α)
Tactic: refine ⟨?_, lowerClosure_min subset_closure (isClosed_iff_isLower.1 isClosed_closure)⟩
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
⊢ closure[inst_1] s ⊆ (↑(lowerClosure s) : Set α)
have apply : IsClosed[inst_1] (↑(lowerClosure s) : Set α)
Tactic: apply closure_minimal subset_lowerClosure _
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
⊢ IsClosed[inst_1] (↑(lowerClosure s) : Set α)
have rw : IsLowerSet (↑(lowerClosure s) : Set α)
Tactic: rw [isClosed_iff_isLower]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
a : α
⊢ closure[inst_1] {a} = Iic a
have rw : (↑(LowerSet.Iic a) : Set α) = Iic a
Tactic: rw [closure_eq_lowerClosure, lowerClosure_singleton]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
⊢ nhdsKer s = (↑(upperClosure s) : Set α)
have h : ∀ (x : α), x ∈ nhdsKer s ↔ x ∈ (↑(upperClosure s) : Set α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
a : α
⊢ nhdsKer {a} = Ici a
have rw : (↑(upperClosure {a}) : Set α) = Ici a
Tactic: rw [nhdsKer_eq_upperClosure, upperClosure_singleton, UpperSet.coe_Ici]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
a : α
rw : (↑(upperClosure {a}) : Set α) = Ici a
⊢ nhdsKer {a} = Ici a
have rw₁ : (↑(UpperSet.Ici a) : Set α) = Ici a
Tactic: rw [nhdsKer_eq_upperClosure, upperClosure_singleton, UpperSet.coe_Ici]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
a : α
rw : (↑(upperClosure {a}) : Set α) = Ici a
rw₁ : (↑(UpperSet.Ici a) : Set α) = Ici a
⊢ nhdsKer {a} = Ici a
have rw₂ : Ici a = Ici a
Tactic: rw [nhdsKer_eq_upperClosure, upperClosure_singleton, UpperSet.coe_Ici]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
a : α
⊢ 𝓝 a = 𝓟 (Ici a)
have rw : 𝓟 (nhdsKer {a}) = 𝓟 (Ici a)
Tactic: rw [← principal_nhdsKer_singleton, nhdsKer_singleton]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
a : α
rw : 𝓟 (nhdsKer {a}) = 𝓟 (Ici a)
⊢ 𝓝 a = 𝓟 (Ici a)
have rw₁ : 𝓟 (Ici a) = 𝓟 (Ici a)
Tactic: rw [← principal_nhdsKer_singleton, nhdsKer_singleton]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
⊢ 𝓝ˢ s = 𝓟 (↑(upperClosure s) : Set α)
have rw : 𝓟 (nhdsKer s) = 𝓟 (↑(upperClosure s) : Set α)
Tactic: rw [← principal_nhdsKer, nhdsKer_eq_upperClosure]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
rw : 𝓟 (nhdsKer s) = 𝓟 (↑(upperClosure s) : Set α)
⊢ 𝓝ˢ s = 𝓟 (↑(upperClosure s) : Set α)
have rw₁ : 𝓟 (↑(upperClosure s) : Set α) = 𝓟 (↑(upperClosure s) : Set α)
Tactic: rw [← principal_nhdsKer, nhdsKer_eq_upperClosure]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : Topology.IsUpperSet α
inst_5 : Topology.IsUpperSet β
f : α → β
⊢ Monotone f ↔ Continuous[inst_2, inst_3] f
have mp : Monotone f → Continuous[inst_2, inst_3] f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : Topology.IsUpperSet α
inst_5 : Topology.IsUpperSet β
f : α → β
mp : Monotone f → Continuous[inst_2, inst_3] f
⊢ Monotone f ↔ Continuous[inst_2, inst_3] f
have mpr : Continuous[inst_2, inst_3] f → Monotone f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : Topology.IsUpperSet α
inst_5 : Topology.IsUpperSet β
f : α → β
hf : Monotone f
⊢ Continuous[inst_2, inst_3] f
have mp : ∀ (s : Set β), IsUpperSet s → IsUpperSet (f ⁻¹' s)
Tactic: simp_rw [continuous_def, isOpen_iff_isUpperSet]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : Topology.IsUpperSet α
inst_5 : Topology.IsUpperSet β
f : α → β
hf : Continuous[inst_2, inst_3] f
a b : α
hab : a ≤ b
⊢ f a ≤ f b
have mpr : ∀ (hab : Membership.mem (γ := Set α) (closure[inst_2] {b}) a), Membership.mem (γ := Set β) (closure[inst_3] {f b}) (f a)
Tactic: rw [← mem_Iic, ← closure_singleton] at hab ⊢
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : Topology.IsUpperSet α
inst_5 : Topology.IsUpperSet β
f : α → β
hf : Continuous[inst_2, inst_3] f
a b : α
hab : Membership.mem (γ := Set α) (closure[inst_2] {b}) a
⊢ Membership.mem (γ := Set β) (closure[inst_3] {f b}) (f a)
have mpr : a ∈ closure[inst_2] (f ⁻¹' {f b})
Tactic: apply Continuous.closure_preimage_subset hf {f b}