awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
refine_1 : ∀ (b : β) (hb : b < f a), ∀ᶠ (b_1 : α) in 𝓝[≥] a, b < f b_1
⊢ ContinuousWithinAt f (Ici a) a
have refine_2 : ∀ (b : β) (hb : b > f a), ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b
Tactic: refine tendsto_order.2 ⟨fun b hb => ?_, fun b hb => ?_⟩
-- 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
b : β
hb : b < f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, b < f b_1
have 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
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)
-- 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
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
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, b < f b_1
have h₁ : ∀ a_1 ∈ s, a_1 ∈ Ici a → b < f a_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)
-- 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
b : β
hb : b > f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b
have refine_2 : ∀ (c : α) (hcs : c ∈ s) (hac : f a < f c) (hcb : f c ≤ b), ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b
Tactic: rcases hfs b hb with ⟨c, hcs, hac, hcb⟩
-- 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
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : f a < f c
hcb : f c ≤ b
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b
have hac₁ : a < c
Tactic: rw [h_mono.lt_iff_lt has hcs] at hac
Cleared hypotheses: hac, hcb
-- 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
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : a < c
hcb : f c ≤ b
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b
have h : ∀ a_1 ∈ s, a_1 ∈ Ico a c → f a_1 < b
Tactic: filter_upwards [hs, Ico_mem_nhdsGE hac]
-- 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 : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (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 : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (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 => ?_⟩
-- 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 : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
has : a ∈ s
refine_1 : ∀ (b : β) (hb : b < f a), ∀ᶠ (b_1 : α) in 𝓝[≥] a, b < f b_1
⊢ ContinuousWithinAt f (Ici a) a
have refine_2 : ∀ (b : β) (hb : b > f a), ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b
Tactic: refine tendsto_order.2 ⟨fun b hb => ?_, fun b hb => ?_⟩
-- 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 : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
has : a ∈ s
b : β
hb : b < f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, b < f b_1
have 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
Tactic: filter_upwards [hs, @self_mem_nhdsWithin _ _ a (Ici a)] with _ hxs hxa using hb.trans_le
      (h_mono has hxs hxa)
-- 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 : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (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
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, b < f b_1
have h₁ : ∀ a_1 ∈ s, a_1 ∈ Ici a → b < f a_1
Tactic: filter_upwards [hs, @self_mem_nhdsWithin _ _ a (Ici a)] with _ hxs hxa using hb.trans_le
      (h_mono has hxs hxa)
-- 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 : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
has : a ∈ s
b : β
hb : b > f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b
have refine_2 : ∀ (c : α) (hcs : c ∈ s) (hac : f a < f c) (hcb : f c < b), ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b
Tactic: rcases hfs b hb with ⟨c, hcs, hac, hcb⟩
-- 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 : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : f a < f c
hcb : f c < b
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b
have this : a < c
Tactic: have : a < c := not_le.1 fun h => hac.not_ge <| h_mono hcs has h
-- 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 : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : f a < f c
hcb : f c < b
this : a < c
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b
have h : ∀ a_1 ∈ s, a_1 ∈ Ico a c → f a_1 < b
Tactic: filter_upwards [hs, Ico_mem_nhdsGE this]
-- 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 β
inst_6 : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : closure[inst_4] (f '' s) ∈ 𝓝[≥] f a
⊢ ContinuousWithinAt f (Ici a) a
have refine : ∀ (b : β) (hb : b > f a), ∃ c ∈ s, f c ∈ Ioo (f a) b
Tactic: refine continuousWithinAt_right_of_monotoneOn_of_exists_between h_mono hs fun b hb => ?_
-- 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 β
inst_6 : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : closure[inst_4] (f '' s) ∈ 𝓝[≥] f a
b : β
hb : b > f a
⊢ ∃ c ∈ s, f c ∈ Ioo (f a) b
have rcases : ∀ (b' : β) (hb' : Ico (f a) b' ⊆ closure[inst_4] (f '' s)) (hab' : f a < b') (hbb' : b' ≤ b), ∃ c ∈ s, f c ∈ Ioo (f a) b
Tactic: rcases (mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset hb).1 hfs with ⟨b', ⟨hab', hbb'⟩, hb'⟩
-- 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 β
inst_6 : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : closure[inst_4] (f '' s) ∈ 𝓝[≥] f a
b : β
hb : b > f a
b' : β
hb' : Ico (f a) b' ⊆ closure[inst_4] (f '' s)
hab' : f a < b'
hbb' : b' ≤ b
⊢ ∃ c ∈ s, f c ∈ Ioo (f a) b
have rcases : ∀ (c' : β) (hc' : f a < c' ∧ c' < b'), ∃ c ∈ s, f c ∈ Ioo (f a) b
Tactic: rcases exists_between hab' with ⟨c', hc'⟩
-- 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 β
inst_6 : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : closure[inst_4] (f '' s) ∈ 𝓝[≥] f a
b : β
hb : b > f a
b' : β
hb' : Ico (f a) b' ⊆ closure[inst_4] (f '' s)
hab' : f a < b'
hbb' : b' ≤ b
c' : β
hc' : f a < c' ∧ c' < b'
⊢ ∃ c ∈ s, f c ∈ Ioo (f a) b
have rcases : ∀ (c : α) (hcs : c ∈ s) (hc : f c ∈ Ioo (f a) b'), ∃ c ∈ s, f c ∈ Ioo (f a) b
Tactic: rcases mem_closure_iff.1 (hb' ⟨hc'.1.le, hc'.2⟩) (Ioo (f a) b') isOpen_Ioo hc' with
    ⟨_, hc, ⟨c, hcs, rfl⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Order.MonotoneContinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : OrderTopology α
inst_5 : OrderTopology β
e : α ≃o β
⊢ Continuous[inst_2, inst_3] (⇑e : (a : α) → β)
have rw : ∀ (s : Set β),
  Membership.mem (γ := Set (Set β)) {s : Set β | ∃ (a : β), s = Ioi a ∨ s = Iio a} s →
    IsOpen[inst_2] ((⇑e : (a : α) → β) ⁻¹' s)
Tactic: rw [‹OrderTopology β›.topology_eq_generate_intervals, continuous_generateFrom_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.MonotoneContinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : OrderTopology α
inst_5 : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen[inst_2] ((⇑e : (a : α) → β) ⁻¹' Ioi a)
have inl : IsOpen[inst_2] (Ioi ((e.symm : (a : β) → α) a) : Set α)
Tactic: rw [e.preimage_Ioi]
-- Lean 4 proof step from Mathlib.Topology.Order.MonotoneContinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : OrderTopology α
inst_5 : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen[inst_2] ((⇑e : (a : α) → β) ⁻¹' Iio a)
have inr : IsOpen[inst_2] (Iio ((e.symm : (a : β) → α) a) : Set α)
Tactic: rw [e.preimage_Iio]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun (s : Set (γ × γ)) ↦ s ○ s
⊢ F ≤ 𝓝Δ
have rw : ∀ V ∈ 𝓝Δ, F ⊓ 𝓟 Vᶜ = ⊥
Tactic: rw [le_iff_forall_inf_principal_compl]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun (s : Set (γ × γ)) ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
⊢ F ⊓ 𝓟 Vᶜ = ⊥
have by_contra : ∀ (H : ¬F ⊓ 𝓟 Vᶜ = ⊥), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (hypothesis)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun (s : Set (γ × γ)) ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
⊢ False
have this : (F ⊓ 𝓟 Vᶜ).NeBot
Tactic: haveI : NeBot (F ⊓ 𝓟 Vᶜ) := ⟨H⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun (s : Set (γ × γ)) ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : (F ⊓ 𝓟 Vᶜ).NeBot
⊢ False
have obtain : ∀ (x y : γ) (hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)), False
Tactic: obtain ⟨⟨x, y⟩, hxy⟩ : ∃ p : γ × γ, ClusterPt p (F ⊓ 𝓟 Vᶜ) := exists_clusterPt_of_compactSpace _
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (hypothesis)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun (s : Set (γ × γ)) ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
⊢ False
have clV : ClusterPt (x, y) (𝓟 Vᶜ)
Tactic: have clV : ClusterPt (x, y) (𝓟 <| Vᶜ) := hxy.of_inf_right
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (hypothesis)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun (s : Set (γ × γ)) ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
h : Inseparable x y
⊢ False
have clV₁ : (y, y) ∈ (interior V)ᶜ
Tactic: rw [← mem_closure_iff_clusterPt, (h.prod .rfl).mem_closed_iff isClosed_closure,
        closure_compl] at clV
Cleared hypotheses: clV, h
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun (s : Set (γ × γ)) ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : (y, y) ∈ (interior V)ᶜ
h : Inseparable x y
⊢ False
have apply : (y, y) ∈ interior V
Tactic: apply clV
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun (s : Set (γ × γ)) ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : (y, y) ∈ (interior V)ᶜ
h : Inseparable x y
⊢ (y, y) ∈ interior V
have rw : V ∈ 𝓝 (y, y)
Tactic: rw [mem_interior_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (hypothesis)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun (s : Set (γ × γ)) ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
⊢ False
have ninsep_xy : ¬Inseparable x y
Tactic: have ninsep_xy : ¬Inseparable x y := by
      intro h
      rw [← mem_closure_iff_clusterPt, (h.prod .rfl).mem_closed_iff isClosed_closure,
        closure_compl] at clV
      apply clV
      rw [mem_interior_iff_mem_nhds]
      exact nhds_le_nhdsSet (mem_diagonal y) V_in
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun (s : Set (γ × γ)) ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
ninsep_xy : ¬Inseparable x y
⊢ False
have disjoint_nested_nhds_of_not_inseparable : ∀ (U₁ V₁ : Set γ) (V₁_in : V₁ ∈ 𝓝 x) (U₂ V₂ : Set γ) (V₂_in : V₂ ∈ 𝓝 y) (V₁_cl : IsClosed[inst] V₁)
  (V₂_cl : IsClosed[inst] V₂) (U₁_op : IsOpen[inst] U₁) (U₂_op : IsOpen[inst] U₂) (VU₁ : V₁ ⊆ U₁) (VU₂ : V₂ ⊆ U₂)
  (hU₁₂ : Disjoint U₁ U₂), False
Tactic: obtain
      ⟨U₁, -, V₁, V₁_in, U₂, -, V₂, V₂_in, V₁_cl, V₂_cl, U₁_op, U₂_op, VU₁, VU₂, hU₁₂⟩ :=
      disjoint_nested_nhds_of_not_inseparable ninsep_xy
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (hypothesis)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun (s : Set (γ × γ)) ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
ninsep_xy : ¬Inseparable x y
U₁ V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed[inst] V₁
V₂_cl : IsClosed[inst] V₂
U₁_op : IsOpen[inst] U₁
U₂_op : IsOpen[inst] U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
⊢ False
have U₃_op : IsOpen[inst] U₃
Tactic: have U₃_op : IsOpen U₃ := (V₁_cl.union V₂_cl).isOpen_compl
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun (s : Set (γ × γ)) ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
ninsep_xy : ¬Inseparable x y
U₁ V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed[inst] V₁
V₂_cl : IsClosed[inst] V₂
U₁_op : IsOpen[inst] U₁
U₂_op : IsOpen[inst] U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
U₃_op : IsOpen[inst] U₃
W : Set (γ × γ) := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃
⊢ W ∈ 𝓝Δ
have rw : ∀ x ∈ diagonal γ, W ∈ 𝓝 x
Tactic: rw [mem_nhdsSet_iff_forall]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun (s : Set (γ × γ)) ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
ninsep_xy : ¬Inseparable x y
U₁ V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed[inst] V₁
V₂_cl : IsClosed[inst] V₂
U₁_op : IsOpen[inst] U₁
U₂_op : IsOpen[inst] U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
U₃_op : IsOpen[inst] U₃
W : Set (γ × γ) := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃
z z' : γ
hzz' : (z, z') ∈ diagonal γ
⊢ W ∈ 𝓝 (z, z')
have refine_1 : IsOpen[instTopologicalSpaceProd] W
Tactic: refine IsOpen.mem_nhds ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun (s : Set (γ × γ)) ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
ninsep_xy : ¬Inseparable x y
U₁ V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed[inst] V₁
V₂_cl : IsClosed[inst] V₂
U₁_op : IsOpen[inst] U₁
U₂_op : IsOpen[inst] U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
U₃_op : IsOpen[inst] U₃
W : Set (γ × γ) := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃
z z' : γ
hzz' : (z, z') ∈ diagonal γ
refine_1 : IsOpen[instTopologicalSpaceProd] W
⊢ W ∈ 𝓝 (z, z')
have refine_2 : (z, z') ∈ W
Tactic: refine IsOpen.mem_nhds ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun (s : Set (γ × γ)) ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
ninsep_xy : ¬Inseparable x y
U₁ V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed[inst] V₁
V₂_cl : IsClosed[inst] V₂
U₁_op : IsOpen[inst] U₁
U₂_op : IsOpen[inst] U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
U₃_op : IsOpen[inst] U₃
W : Set (γ × γ) := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃
z z' : γ
hzz' : (z, z') ∈ diagonal γ
⊢ (z, z') ∈ W
have refine_2 : (z, z) ∈ W
Tactic: cases hzz'
Cleared hypotheses: z', hzz'
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun (s : Set (γ × γ)) ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
ninsep_xy : ¬Inseparable x y
U₁ V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed[inst] V₁
V₂_cl : IsClosed[inst] V₂
U₁_op : IsOpen[inst] U₁
U₂_op : IsOpen[inst] U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
U₃_op : IsOpen[inst] U₃
W : Set (γ × γ) := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃
z : γ
⊢ (z, z) ∈ W
have refine_2 : (z ∈ U₁ ∧ z ∈ U₁ ∨ z ∈ U₂ ∧ z ∈ U₂) ∨ z ∈ (V₁ ∪ V₂)ᶜ ∧ z ∈ (V₁ ∪ V₂)ᶜ
Tactic: simp only [W, U₃, mem_union, mem_prod]