awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hst : Disjoint s t
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
g : C(X, ℝ)
hg : t = preimage (β := ℝ) (⇑g : (a : X) → ℝ) {0}
hgr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : X) → ℝ) x : ℝ)
hsn : SeparatedNhds (X := ℝ) {0} {1}
hfg : ∀ (x : X), HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0
⊢ s =
    preimage (β := ℝ)
      (fun (a : X) ↦
        HDiv.hDiv (α := ℝ) ((f : (a : X) → ℝ) a : ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) a : ℝ) ((g : (a : X) → ℝ) a : ℝ)))
      {0}

Tactic:
simp_all [preimage]

Premises used: Set.preimage
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hst : Disjoint s t
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
g : C(X, ℝ)
hg : t = preimage (β := ℝ) (⇑g : (a : X) → ℝ) {0}
hgr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : X) → ℝ) x : ℝ)
hsn : SeparatedNhds (X := ℝ) {0} {1}
hfg : ∀ (x : X), HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0
⊢ s =
    preimage (β := ℝ)
      (fun (a : X) ↦
        HDiv.hDiv (α := ℝ) ((f : (a : X) → ℝ) a : ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) a : ℝ) ((g : (a : X) → ℝ) a : ℝ)))
      {0}

Tactic:
have hp : s = (fun a => f a / (f a + g a)) ⁻¹' {0} := by simp_all [preimage]
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hst : Disjoint s t
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
g : C(X, ℝ)
hg : t = preimage (β := ℝ) (⇑g : (a : X) → ℝ) {0}
hgr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : X) → ℝ) x : ℝ)
hsn : SeparatedNhds (X := ℝ) {0} {1}
hfg : ∀ (x : X), HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0
hp :
  s =
    preimage (β := ℝ)
      (fun (a : X) ↦
        HDiv.hDiv (α := ℝ) ((f : (a : X) → ℝ) a : ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) a : ℝ) ((g : (a : X) → ℝ) a : ℝ)))
      {0}
⊢ t =
    preimage (β := ℝ)
      (fun (a : X) ↦
        HDiv.hDiv (α := ℝ) ((f : (a : X) → ℝ) a : ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) a : ℝ) ((g : (a : X) → ℝ) a : ℝ)))
      {1}

Tactic:
simp_all [preimage, div_eq_one_iff_eq]

Premises used: div_eq_one_iff_eq, Set.preimage
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hst : Disjoint s t
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
g : C(X, ℝ)
hg : t = preimage (β := ℝ) (⇑g : (a : X) → ℝ) {0}
hgr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : X) → ℝ) x : ℝ)
hsn : SeparatedNhds (X := ℝ) {0} {1}
hfg : ∀ (x : X), HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0
hp :
  s =
    preimage (β := ℝ)
      (fun (a : X) ↦
        HDiv.hDiv (α := ℝ) ((f : (a : X) → ℝ) a : ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) a : ℝ) ((g : (a : X) → ℝ) a : ℝ)))
      {0}
⊢ t =
    preimage (β := ℝ)
      (fun (a : X) ↦
        HDiv.hDiv (α := ℝ) ((f : (a : X) → ℝ) a : ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) a : ℝ) ((g : (a : X) → ℝ) a : ℝ)))
      {1}

Tactic:
have : t = (fun a => f a / (f a + g a)) ⁻¹' {1} := by simp_all [preimage, div_eq_one_iff_eq]
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hst : Disjoint s t
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
g : C(X, ℝ)
hg : t = preimage (β := ℝ) (⇑g : (a : X) → ℝ) {0}
hgr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : X) → ℝ) x : ℝ)
hsn : SeparatedNhds (X := ℝ) {0} {1}
hfg : ∀ (x : X), HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0
hp :
  s =
    preimage (β := ℝ)
      (fun (a : X) ↦
        HDiv.hDiv (α := ℝ) ((f : (a : X) → ℝ) a : ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) a : ℝ) ((g : (a : X) → ℝ) a : ℝ)))
      {0}
this :
  t =
    preimage (β := ℝ)
      (fun (a : X) ↦
        HDiv.hDiv (α := ℝ) ((f : (a : X) → ℝ) a : ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) a : ℝ) ((g : (a : X) → ℝ) a : ℝ)))
      {1}
rw :
  SeparatedNhds.{u_1} (X := X)
    (preimage (β := ℝ)
      (fun (a : X) ↦
        HDiv.hDiv (α := ℝ) ((f : (a : X) → ℝ) a : ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) a : ℝ) ((g : (a : X) → ℝ) a : ℝ)))
      {0})
    (preimage (β := ℝ)
      (fun (a : X) ↦
        HDiv.hDiv (α := ℝ) ((f : (a : X) → ℝ) a : ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) a : ℝ) ((g : (a : X) → ℝ) a : ℝ)))
      {1})
⊢ SeparatedNhds s t

Tactic:
rw [hp, this]
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hst : Disjoint s t
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
g : C(X, ℝ)
hg : t = preimage (β := ℝ) (⇑g : (a : X) → ℝ) {0}
hgr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : X) → ℝ) x : ℝ)
hsn : SeparatedNhds (X := ℝ) {0} {1}
hfg : ∀ (x : X), HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0
hp :
  s =
    preimage (β := ℝ)
      (fun (a : X) ↦
        HDiv.hDiv (α := ℝ) ((f : (a : X) → ℝ) a : ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) a : ℝ) ((g : (a : X) → ℝ) a : ℝ)))
      {0}
this :
  t =
    preimage (β := ℝ)
      (fun (a : X) ↦
        HDiv.hDiv (α := ℝ) ((f : (a : X) → ℝ) a : ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) a : ℝ) ((g : (a : X) → ℝ) a : ℝ)))
      {1}
⊢ SeparatedNhds.{u_1} (X := X)
    (preimage (β := ℝ)
      (fun (a : X) ↦
        HDiv.hDiv (α := ℝ) ((f : (a : X) → ℝ) a : ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) a : ℝ) ((g : (a : X) → ℝ) a : ℝ)))
      {0})
    (preimage (β := ℝ)
      (fun (a : X) ↦
        HDiv.hDiv (α := ℝ) ((f : (a : X) → ℝ) a : ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) a : ℝ) ((g : (a : X) → ℝ) a : ℝ)))
      {1})

Tactic:
hsn.preimage (f.continuous.div₀ (f.continuous.add g.continuous) hfg)

Premises used: ContinuousMap.continuous, SeparatedNhds.preimage, Continuous.div₀, Continuous.add
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hst : Disjoint s t
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
g : C(X, ℝ)
hg : t = preimage (β := ℝ) (⇑g : (a : X) → ℝ) {0}
hgr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : X) → ℝ) x : ℝ)
hsn : SeparatedNhds (X := ℝ) {0} {1}
hfg : ∀ (x : X), HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0
hp :
  s =
    preimage (β := ℝ)
      (fun (a : X) ↦
        HDiv.hDiv (α := ℝ) ((f : (a : X) → ℝ) a : ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) a : ℝ) ((g : (a : X) → ℝ) a : ℝ)))
      {0}
this :
  t =
    preimage (β := ℝ)
      (fun (a : X) ↦
        HDiv.hDiv (α := ℝ) ((f : (a : X) → ℝ) a : ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) a : ℝ) ((g : (a : X) → ℝ) a : ℝ)))
      {1}
⊢ SeparatedNhds.{u_1} (X := X)
    (preimage (β := ℝ)
      (fun (a : X) ↦
        HDiv.hDiv (α := ℝ) ((f : (a : X) → ℝ) a : ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) a : ℝ) ((g : (a : X) → ℝ) a : ℝ)))
      {0})
    (preimage (β := ℝ)
      (fun (a : X) ↦
        HDiv.hDiv (α := ℝ) ((f : (a : X) → ℝ) a : ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) a : ℝ) ((g : (a : X) → ℝ) a : ℝ)))
      {1})

Tactic:
exact hsn.preimage (f.continuous.div₀ (f.continuous.add g.continuous) hfg)

Premises used: ContinuousMap.continuous, SeparatedNhds.preimage, Continuous.div₀, Continuous.add
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
pos : ∀ (hse : s = ∅), IsGδ s
neg : ∀ (hse : s.Nonempty), IsGδ s
⊢ IsGδ s

Tactic:
by_cases! hse : s = ∅
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s = ∅
⊢ IsGδ s

Tactic:
simp_all
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
neg :
  ∀ (f : C(X, ℝ)) (hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0})
    (hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)), IsGδ s
⊢ IsGδ s

Tactic:
obtain ⟨f, hf, hfr⟩ := h s hs
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
⊢ IsGδ s

Tactic:
isGδ_iff_eq_iInter_nat.2 ⟨fun n => f ⁻¹' (Iio (1 / (n + 1))),
          fun n => ?_, ?_⟩

Premises used: Iff.mpr, HDiv.hDiv, Nat.cast, Set.preimage, HAdd.hAdd, And.intro, Exists.intro, isGδ_iff_eq_iInter_nat, OfNat.ofNat, Set.Iio, DFunLike.coe
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
neg :
  ∀ (n : ℕ), IsOpen[inst] ((fun (n : ℕ) ↦ ((⇑f : (a : X) → ℝ) ⁻¹' Iio (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : Set X)) n)
neg₁ : s = ⋂ (n : ℕ), (fun (n : ℕ) ↦ ((⇑f : (a : X) → ℝ) ⁻¹' Iio (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : Set X)) n
⊢ IsGδ s

Tactic:
refine isGδ_iff_eq_iInter_nat.2 ⟨fun n => f ⁻¹' (Iio (1 / (n + 1))),
          fun n => ?_, ?_⟩

Premises used: Iff.mpr, HDiv.hDiv, Nat.cast, Set.preimage, HAdd.hAdd, And.intro, Exists.intro, isGδ_iff_eq_iInter_nat, OfNat.ofNat, Set.Iio, DFunLike.coe
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
n : ℕ
⊢ IsOpen[inst] ((fun (n : ℕ) ↦ ((⇑f : (a : X) → ℝ) ⁻¹' Iio (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : Set X)) n)

Tactic:
f.continuous.isOpen_preimage _ isOpen_Iio

Premises used: ContinuousMap.continuous, isOpen_Iio, Continuous.isOpen_preimage
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
n : ℕ
⊢ IsOpen[inst] ((fun (n : ℕ) ↦ ((⇑f : (a : X) → ℝ) ⁻¹' Iio (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : Set X)) n)

Tactic:
exact f.continuous.isOpen_preimage _ isOpen_Iio

Premises used: ContinuousMap.continuous, isOpen_Iio, Continuous.isOpen_preimage
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
neg :
  Eq (α := Set X) (preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0})
    (preimage (β := ℝ) (⇑f : (a : X) → ℝ)
      (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1)))
⊢ s = ⋂ (n : ℕ), (fun (n : ℕ) ↦ ((⇑f : (a : X) → ℝ) ⁻¹' Iio (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : Set X)) n

Tactic:
simp only [hf, ← preimage_iInter,
            ← preimage_range_inter (s := ⋂ (n : ℕ), Iio (1 / (n + 1) : ℝ)), inter_iInter]

Premises used: Set.inter_iInter, Set.preimage_range_inter, Set.preimage_iInter
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
neg : Eq (α := Set ℝ) {0} (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1))
⊢ Eq (α := Set X) (preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0})
    (preimage (β := ℝ) (⇑f : (a : X) → ℝ)
      (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1)))

Tactic:
congr
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
neg :
  Membership.mem (γ := Set ℝ) (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1))
      0 ∧
    ∀ (x : ℝ),
      Membership.mem (γ := Set ℝ)
          (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1)) x →
        x = 0
⊢ Eq (α := Set ℝ) {0} (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1))

Tactic:
rw [eq_comm, eq_singleton_iff_unique_mem]

Premises used: eq_comm, Set.eq_singleton_iff_unique_mem
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
⊢ Membership.mem (γ := Set ℝ) (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1))
      0 ∧
    ∀ (x : ℝ),
      Membership.mem (γ := Set ℝ)
          (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1)) x →
        x = 0

Tactic:
⟨mem_iInter_of_mem fun n => ?_, fun x h => ?_⟩

Premises used: Set.mem_iInter_of_mem, And.intro
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
neg : ∀ (n : ℕ), 0 ∈ range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
neg₁ :
  ∀ (x : ℝ)
    (h :
      Membership.mem (γ := Set ℝ)
        (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1)) x),
    x = 0
⊢ Membership.mem (γ := Set ℝ) (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1))
      0 ∧
    ∀ (x : ℝ),
      Membership.mem (γ := Set ℝ)
          (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1)) x →
        x = 0

Tactic:
refine ⟨mem_iInter_of_mem fun n => ?_, fun x h => ?_⟩
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
n : ℕ
⊢ 0 < 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
positivity
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
n : ℕ
⊢ 0 ∈ range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
exact ⟨(hf ▸ hse : (f ⁻¹' {0}).Nonempty), show 0 < (1 / (n + 1) : ℝ) by positivity⟩
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h_1 :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
x : ℝ
h :
  Membership.mem (γ := Set ℝ) (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1)) x
neg : x ≤ 0
neg₁ : 0 ≤ x
⊢ x = 0

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h_1 :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
x : ℝ
h :
  Membership.mem (γ := Set ℝ) (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1)) x
⊢ ∀ (i : ℕ), Membership.mem (γ := Set ℝ) (range (ι := X) (⇑f : (a : X) → ℝ)) x ∧ x < 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1

Tactic:
simp only [mem_iInter, mem_inter_iff, mem_Iio] at h

Premises used: Set.mem_Iio, Set.mem_inter_iff, Set.mem_iInter
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h_1 :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
x : ℝ
h : ∀ (i : ℕ), Membership.mem (γ := Set ℝ) (range (ι := X) (⇑f : (a : X) → ℝ)) x ∧ x < 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
⊢ x ≤ 0

Tactic:
ge_of_tendsto' tendsto_one_div_add_atTop_nhds_zero_nat (fun n => (h n).2.le)

Premises used: tendsto_one_div_add_atTop_nhds_zero_nat, LT.lt.le, ge_of_tendsto', And.right