awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.LinearUpperLowerSetTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : Topology.IsUpperSet α
s t : Set α
a : α
ha : a ∈ s
b : α
hsct : Disjoint (α := Set α) {a} (closure {b})
hcst : Disjoint (α := Set α) (closure {a}) {b}
hb : b ∈ t
⊢ Disjoint (α := Set α) (closure {a}) {b} = (a < b)

Tactic:
simp
-- Module: Mathlib.Topology.Separation.LinearUpperLowerSetTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : Topology.IsUpperSet α
s t : Set α
a : α
ha : a ∈ s
b : α
hsct : Disjoint (α := Set α) {a} (closure {b})
hcst : Disjoint (α := Set α) (closure {a}) {b}
hb : b ∈ t
⊢ a < b

Tactic:
conv at hcst => equals a < b => simp
-- Module: Mathlib.Topology.Separation.LinearUpperLowerSetTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : Topology.IsUpperSet α
s t : Set α
a : α
ha : a ∈ s
b : α
hsct : Disjoint (α := Set α) {a} (closure {b})
hcst : Disjoint (α := Set α) (closure {a}) {b}
hb : b ∈ t
hcst₁ : a < b
⊢ b ∈ t

Tactic:
conv at hcst => equals a < b => simp
-- Module: Mathlib.Topology.Separation.LinearUpperLowerSetTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : Topology.IsUpperSet α
s t : Set α
a : α
ha : a ∈ s
b : α
hsct : Disjoint (α := Set α) {a} (closure {b})
hcst : a < b
hb : b ∈ t
⊢ Disjoint (α := Set α) {a} (closure {b}) = (b < a)

Tactic:
simp
-- Module: Mathlib.Topology.Separation.LinearUpperLowerSetTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : Topology.IsUpperSet α
s t : Set α
a : α
ha : a ∈ s
b : α
hsct : Disjoint (α := Set α) {a} (closure {b})
hcst : a < b
hb : b ∈ t
⊢ b < a

Tactic:
conv at hsct => equals b < a => simp
-- Module: Mathlib.Topology.Separation.LinearUpperLowerSetTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : Topology.IsUpperSet α
s t : Set α
a : α
ha : a ∈ s
b : α
hsct : Disjoint (α := Set α) {a} (closure {b})
hcst : a < b
hb : b ∈ t
hsct₁ : b < a
⊢ a < b

Tactic:
conv at hsct => equals b < a => simp
-- Module: Mathlib.Topology.Separation.LinearUpperLowerSetTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : Topology.IsUpperSet α
s t : Set α
a : α
ha : a ∈ s
b : α
hsct : Disjoint (α := Set α) {a} (closure {b})
hcst : a < b
hb : b ∈ t
hsct₁ : b < a
hcst₁ : a < b
⊢ b ∈ t

Tactic:
conv at hsct => equals b < a => simp
-- Module: Mathlib.Topology.Separation.LinearUpperLowerSetTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : Topology.IsUpperSet α
s t : Set α
a : α
ha : a ∈ s
b : α
hsct : b < a
hcst : a < b
hb : b ∈ t
⊢ False

Tactic:
lt_asymm hcst hsct

Premises used: lt_asymm
-- Module: Mathlib.Topology.Separation.LinearUpperLowerSetTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : Topology.IsUpperSet α
s t : Set α
a : α
ha : a ∈ s
b : α
hsct : b < a
hcst : a < b
hb : b ∈ t
⊢ False

Tactic:
exact lt_asymm hcst hsct

Premises used: lt_asymm
-- Module: Mathlib.Topology.Separation.LinearUpperLowerSetTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : Topology.IsLowerSet α
⊢ CompletelyNormalSpace α

Tactic:
inferInstanceAs (CompletelyNormalSpace αᵒᵈ)

Premises used: _private.0.instCompletelyNormalSpaceOfIsLowerSet._proof_1
-- Module: Mathlib.Topology.Separation.LinearUpperLowerSetTopology
Goal:
⊢ CompletelyNormalSpace Prop

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Separation.NotNormal
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s d : Set X
hs : IsClosed s
inst_2 : DiscreteTopology.{u} (↑s : Type u)
hd : Dense d
t : Set X
ht : t ∈ 𝒫 s
rw :
  IsClosed
    (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))
      (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t))
⊢ IsClosed t

Tactic:
rw [← inter_eq_self_of_subset_right ht, ← Subtype.image_preimage_val]

Premises used: Subtype.image_preimage_val, Set.inter_eq_self_of_subset_right
-- Module: Mathlib.Topology.Separation.NotNormal
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s d : Set X
hs : IsClosed s
inst_2 : DiscreteTopology.{u} (↑s : Type u)
hd : Dense d
t : Set X
ht : t ∈ 𝒫 s
⊢ IsClosed
    (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))
      (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t))

Tactic:
hs.isClosedMap_subtype_val _ (isClosed_discrete _)

Premises used: isClosed_discrete, IsClosed.isClosedMap_subtype_val
-- Module: Mathlib.Topology.Separation.NotNormal
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s d : Set X
hs : IsClosed s
inst_2 : DiscreteTopology.{u} (↑s : Type u)
hd : Dense d
t : Set X
ht : t ∈ 𝒫 s
⊢ IsClosed
    (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))
      (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t))

Tactic:
exact hs.isClosedMap_subtype_val _ (isClosed_discrete _)

Premises used: isClosed_discrete, IsClosed.isClosedMap_subtype_val
-- Module: Mathlib.Topology.Separation.NotNormal
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s d : Set X
hs : IsClosed s
inst_2 : DiscreteTopology.{u} (↑s : Type u)
hd : Dense d
⊢ ∀ (t : Set X) (ht : t ∈ 𝒫 s), IsClosed t

Tactic:
have h_closed (t) (ht : t ∈ 𝒫 s) : IsClosed t := by
    rw [← inter_eq_self_of_subset_right ht, ← Subtype.image_preimage_val]
    exact hs.isClosedMap_subtype_val _ (isClosed_discrete _)
-- Module: Mathlib.Topology.Separation.NotNormal
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s d : Set X
hs : IsClosed s
inst_2 : DiscreteTopology.{u} (↑s : Type u)
hd : Dense d
h_closed : ∀ (t : Set X) (ht : t ∈ 𝒫 s), IsClosed t
choose :
  ∀ (U V : (t : (↑(𝒫 s) : Type u)) → Set X) (hU : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (U t))
    (hV : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (V t)) (hUs : ∀ (t : (↑(𝒫 s) : Type u)), (↑t : Set X) ⊆ U t)
    (hVs : ∀ (t : (↑(𝒫 s) : Type u)), s \ (↑t : Set X) ⊆ V t) (hUV : ∀ (t : (↑(𝒫 s) : Type u)), Disjoint (U t) (V t)),
    HPow.hPow (α := Cardinal.{u}) 2 #(↑s : Type u) ≤ HPow.hPow (α := Cardinal.{u}) 2 #(↑d : Type u)
⊢ HPow.hPow (α := Cardinal.{u}) 2 #(↑s : Type u) ≤ HPow.hPow (α := Cardinal.{u}) 2 #(↑d : Type u)

Tactic:
choose U V hU hV hUs hVs hUV using fun t : 𝒫 s ↦
    normal_separation (h_closed t t.2) (h_closed _ diff_subset) disjoint_sdiff_right

Premises used: Set.diff_subset, normal_separation, SDiff.sdiff, Set.disjoint_sdiff_right, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Separation.NotNormal
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s d : Set X
hs : IsClosed s
inst_2 : DiscreteTopology.{u} (↑s : Type u)
hd : Dense d
h_closed : ∀ (t : Set X) (ht : t ∈ 𝒫 s), IsClosed t
U V : (t : (↑(𝒫 s) : Type u)) → Set X
hU : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (U t)
hV : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (V t)
hUs : ∀ (t : (↑(𝒫 s) : Type u)), (↑t : Set X) ⊆ U t
hVs : ∀ (t : (↑(𝒫 s) : Type u)), s \ (↑t : Set X) ⊆ V t
hUV : ∀ (t : (↑(𝒫 s) : Type u)), Disjoint (U t) (V t)
t₁ t₂ : (↑(𝒫 s) : Type u)
h : U t₁ ∩ d = U t₂ ∩ d
by_contra : ∀ (ht : ¬(↑t₁ : Set X) ⊆ (↑t₂ : Set X)), False
⊢ (↑t₁ : Set X) ⊆ (↑t₂ : Set X)

Tactic:
by_contra ht
-- Module: Mathlib.Topology.Separation.NotNormal
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s d : Set X
hs : IsClosed s
inst_2 : DiscreteTopology.{u} (↑s : Type u)
hd : Dense d
h_closed : ∀ (t : Set X) (ht : t ∈ 𝒫 s), IsClosed t
U V : (t : (↑(𝒫 s) : Type u)) → Set X
hU : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (U t)
hV : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (V t)
hUs : ∀ (t : (↑(𝒫 s) : Type u)), (↑t : Set X) ⊆ U t
hVs : ∀ (t : (↑(𝒫 s) : Type u)), s \ (↑t : Set X) ⊆ V t
hUV : ∀ (t : (↑(𝒫 s) : Type u)), Disjoint (U t) (V t)
t₁ t₂ : (↑(𝒫 s) : Type u)
h : U t₁ ∩ d = U t₂ ∩ d
ht : ¬(↑t₁ : Set X) ⊆ (↑t₂ : Set X)
⊢ ((↑t₁ : Set X) \ (↑t₂ : Set X)).Nonempty

Tactic:
rw [← diff_nonempty] at ht

Premises used: Set.diff_nonempty
-- Module: Mathlib.Topology.Separation.NotNormal
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s d : Set X
hs : IsClosed s
inst_2 : DiscreteTopology.{u} (↑s : Type u)
hd : Dense d
h_closed : ∀ (t : Set X) (ht : t ∈ 𝒫 s), IsClosed t
U V : (t : (↑(𝒫 s) : Type u)) → Set X
hU : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (U t)
hV : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (V t)
hUs : ∀ (t : (↑(𝒫 s) : Type u)), (↑t : Set X) ⊆ U t
hVs : ∀ (t : (↑(𝒫 s) : Type u)), s \ (↑t : Set X) ⊆ V t
hUV : ∀ (t : (↑(𝒫 s) : Type u)), Disjoint (U t) (V t)
t₁ t₂ : (↑(𝒫 s) : Type u)
h : U t₁ ∩ d = U t₂ ∩ d
ht : ((↑t₁ : Set X) \ (↑t₂ : Set X)).Nonempty
⊢ (U t₁ ∩ V t₂ ∩ d).Nonempty

Tactic:
have hUVd := hd.inter_open_nonempty _ ((hU t₁).inter (hV t₂)) <| ht.mono <|
      subset_inter (diff_subset.trans (hUs t₁)) ((diff_subset_diff_left t₁.2).trans (hVs t₂))
-- Module: Mathlib.Topology.Separation.NotNormal
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s d : Set X
hs : IsClosed s
inst_2 : DiscreteTopology.{u} (↑s : Type u)
hd : Dense d
h_closed : ∀ (t : Set X) (ht : t ∈ 𝒫 s), IsClosed t
U V : (t : (↑(𝒫 s) : Type u)) → Set X
hU : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (U t)
hV : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (V t)
hUs : ∀ (t : (↑(𝒫 s) : Type u)), (↑t : Set X) ⊆ U t
hVs : ∀ (t : (↑(𝒫 s) : Type u)), s \ (↑t : Set X) ⊆ V t
hUV : ∀ (t : (↑(𝒫 s) : Type u)), Disjoint (U t) (V t)
t₁ t₂ : (↑(𝒫 s) : Type u)
h : U t₁ ∩ d = U t₂ ∩ d
ht : ((↑t₁ : Set X) \ (↑t₂ : Set X)).Nonempty
hUVd : (U t₁ ∩ V t₂ ∩ d).Nonempty
⊢ (U t₂ ∩ d ∩ V t₂).Nonempty

Tactic:
rw [inter_right_comm, h] at hUVd

Premises used: Set.inter_right_comm
-- Module: Mathlib.Topology.Separation.NotNormal
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s d : Set X
hs : IsClosed s
inst_2 : DiscreteTopology.{u} (↑s : Type u)
hd : Dense d
h_closed : ∀ (t : Set X) (ht : t ∈ 𝒫 s), IsClosed t
U V : (t : (↑(𝒫 s) : Type u)) → Set X
hU : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (U t)
hV : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (V t)
hUs : ∀ (t : (↑(𝒫 s) : Type u)), (↑t : Set X) ⊆ U t
hVs : ∀ (t : (↑(𝒫 s) : Type u)), s \ (↑t : Set X) ⊆ V t
hUV : ∀ (t : (↑(𝒫 s) : Type u)), Disjoint (U t) (V t)
t₁ t₂ : (↑(𝒫 s) : Type u)
h : U t₁ ∩ d = U t₂ ∩ d
ht : ((↑t₁ : Set X) \ (↑t₂ : Set X)).Nonempty
hUVd : (U t₂ ∩ d ∩ V t₂).Nonempty
⊢ False

Tactic:
hUVd.not_disjoint <| disjoint_of_subset_left inter_subset_left (hUV t₂)

Premises used: Set.disjoint_of_subset_left, Set.inter_subset_left, Set.Nonempty.not_disjoint
-- Module: Mathlib.Topology.Separation.NotNormal
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s d : Set X
hs : IsClosed s
inst_2 : DiscreteTopology.{u} (↑s : Type u)
hd : Dense d
h_closed : ∀ (t : Set X) (ht : t ∈ 𝒫 s), IsClosed t
U V : (t : (↑(𝒫 s) : Type u)) → Set X
hU : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (U t)
hV : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (V t)
hUs : ∀ (t : (↑(𝒫 s) : Type u)), (↑t : Set X) ⊆ U t
hVs : ∀ (t : (↑(𝒫 s) : Type u)), s \ (↑t : Set X) ⊆ V t
hUV : ∀ (t : (↑(𝒫 s) : Type u)), Disjoint (U t) (V t)
t₁ t₂ : (↑(𝒫 s) : Type u)
h : U t₁ ∩ d = U t₂ ∩ d
ht : ((↑t₁ : Set X) \ (↑t₂ : Set X)).Nonempty
hUVd : (U t₂ ∩ d ∩ V t₂).Nonempty
⊢ False

Tactic:
exact hUVd.not_disjoint <| disjoint_of_subset_left inter_subset_left (hUV t₂)

Premises used: Set.disjoint_of_subset_left, Set.inter_subset_left, Set.Nonempty.not_disjoint
-- Module: Mathlib.Topology.Separation.NotNormal
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s d : Set X
hs : IsClosed s
inst_2 : DiscreteTopology.{u} (↑s : Type u)
hd : Dense d
h_closed : ∀ (t : Set X) (ht : t ∈ 𝒫 s), IsClosed t
U V : (t : (↑(𝒫 s) : Type u)) → Set X
hU : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (U t)
hV : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (V t)
hUs : ∀ (t : (↑(𝒫 s) : Type u)), (↑t : Set X) ⊆ U t
hVs : ∀ (t : (↑(𝒫 s) : Type u)), s \ (↑t : Set X) ⊆ V t
hUV : ∀ (t : (↑(𝒫 s) : Type u)), Disjoint (U t) (V t)
⊢ ∀ {t₁ t₂ : (↑(𝒫 s) : Type u)} (h : U t₁ ∩ d = U t₂ ∩ d), (↑t₁ : Set X) ⊆ (↑t₂ : Set X)

Tactic:
have hUd {t₁ t₂} (h : U t₁ ∩ d = U t₂ ∩ d) : t₁.1 ⊆ t₂.1 := by
    by_contra ht
    rw [← diff_nonempty] at ht
    have hUVd := hd.inter_open_nonempty _ ((hU t₁).inter (hV t₂)) <| ht.mono <|
      subset_inter (diff_subset.trans (hUs t₁)) ((diff_subset_diff_left t₁.2).trans (hVs t₂))
    rw [inter_right_comm, h] at hUVd
    exact hUVd.not_disjoint <| disjoint_of_subset_left inter_subset_left (hUV t₂)
-- Module: Mathlib.Topology.Separation.NotNormal
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s d : Set X
hs : IsClosed s
inst_2 : DiscreteTopology.{u} (↑s : Type u)
hd : Dense d
h_closed : ∀ (t : Set X) (ht : t ∈ 𝒫 s), IsClosed t
U V : (t : (↑(𝒫 s) : Type u)) → Set X
hU : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (U t)
hV : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (V t)
hUs : ∀ (t : (↑(𝒫 s) : Type u)), (↑t : Set X) ⊆ U t
hVs : ∀ (t : (↑(𝒫 s) : Type u)), s \ (↑t : Set X) ⊆ V t
hUV : ∀ (t : (↑(𝒫 s) : Type u)), Disjoint (U t) (V t)
hUd : ∀ {t₁ t₂ : (↑(𝒫 s) : Type u)} (h : U t₁ ∩ d = U t₂ ∩ d), (↑t₁ : Set X) ⊆ (↑t₂ : Set X)
⊢ Injective (β := Set X) fun (x : (↑(𝒫 s) : Type u)) ↦ U x ∩ d

Tactic:
have h_inj : Injective (U · ∩ d) := fun _ _ h ↦ SetCoe.ext <| (hUd h).antisymm (hUd h.symm)
-- Module: Mathlib.Topology.Separation.NotNormal
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s d : Set X
hs : IsClosed s
inst_2 : DiscreteTopology.{u} (↑s : Type u)
hd : Dense d
h_closed : ∀ (t : Set X) (ht : t ∈ 𝒫 s), IsClosed t
U V : (t : (↑(𝒫 s) : Type u)) → Set X
hU : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (U t)
hV : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (V t)
hUs : ∀ (t : (↑(𝒫 s) : Type u)), (↑t : Set X) ⊆ U t
hVs : ∀ (t : (↑(𝒫 s) : Type u)), s \ (↑t : Set X) ⊆ V t
hUV : ∀ (t : (↑(𝒫 s) : Type u)), Disjoint (U t) (V t)
hUd : ∀ {t₁ t₂ : (↑(𝒫 s) : Type u)} (h : U t₁ ∩ d = U t₂ ∩ d), (↑t₁ : Set X) ⊆ (↑t₂ : Set X)
h_inj : Injective (β := Set X) fun (x : (↑(𝒫 s) : Type u)) ↦ U x ∩ d
rw : #(↑(range fun (x : (↑(𝒫 s) : Type u)) ↦ U x ∩ d) : Type u) ≤ #(↑(𝒫 d) : Type u)
⊢ HPow.hPow (α := Cardinal.{u}) 2 #(↑s : Type u) ≤ HPow.hPow (α := Cardinal.{u}) 2 #(↑d : Type u)

Tactic:
rw [← mk_powerset, ← mk_powerset, ← mk_range_eq _ h_inj]

Premises used: Cardinal.mk_powerset, Cardinal.mk_range_eq
-- Module: Mathlib.Topology.Separation.NotNormal
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s d : Set X
hs : IsClosed s
inst_2 : DiscreteTopology.{u} (↑s : Type u)
hd : Dense d
h_closed : ∀ (t : Set X) (ht : t ∈ 𝒫 s), IsClosed t
U V : (t : (↑(𝒫 s) : Type u)) → Set X
hU : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (U t)
hV : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (V t)
hUs : ∀ (t : (↑(𝒫 s) : Type u)), (↑t : Set X) ⊆ U t
hVs : ∀ (t : (↑(𝒫 s) : Type u)), s \ (↑t : Set X) ⊆ V t
hUV : ∀ (t : (↑(𝒫 s) : Type u)), Disjoint (U t) (V t)
hUd : ∀ {t₁ t₂ : (↑(𝒫 s) : Type u)} (h : U t₁ ∩ d = U t₂ ∩ d), (↑t₁ : Set X) ⊆ (↑t₂ : Set X)
h_inj : Injective (β := Set X) fun (x : (↑(𝒫 s) : Type u)) ↦ U x ∩ d
h : (range fun (x : (↑(𝒫 s) : Type u)) ↦ U x ∩ d) ⊆ 𝒫 d
⊢ #(↑(range fun (x : (↑(𝒫 s) : Type u)) ↦ U x ∩ d) : Type u) ≤ #(↑(𝒫 d) : Type u)

Tactic:
apply mk_le_mk_of_subset

Premises used: Cardinal.mk_le_mk_of_subset
-- Module: Mathlib.Topology.Separation.NotNormal
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s d : Set X
hs : IsClosed s
inst_2 : DiscreteTopology.{u} (↑s : Type u)
hd : Dense d
h_closed : ∀ (t : Set X) (ht : t ∈ 𝒫 s), IsClosed t
U V : (t : (↑(𝒫 s) : Type u)) → Set X
hU : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (U t)
hV : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (V t)
hUs : ∀ (t : (↑(𝒫 s) : Type u)), (↑t : Set X) ⊆ U t
hVs : ∀ (t : (↑(𝒫 s) : Type u)), s \ (↑t : Set X) ⊆ V t
hUV : ∀ (t : (↑(𝒫 s) : Type u)), Disjoint (U t) (V t)
hUd : ∀ {t₁ t₂ : (↑(𝒫 s) : Type u)} (h : U t₁ ∩ d = U t₂ ∩ d), (↑t₁ : Set X) ⊆ (↑t₂ : Set X)
h_inj : Injective (β := Set X) fun (x : (↑(𝒫 s) : Type u)) ↦ U x ∩ d
h : ∀ (y : (↑(𝒫 s) : Type u)), U y ∩ d ∈ 𝒫 d
⊢ (range fun (x : (↑(𝒫 s) : Type u)) ↦ U x ∩ d) ⊆ 𝒫 d

Tactic:
rw [range_subset_iff]

Premises used: Set.range_subset_iff
-- Module: Mathlib.Topology.Separation.NotNormal
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s d : Set X
hs : IsClosed s
inst_2 : DiscreteTopology.{u} (↑s : Type u)
hd : Dense d
h_closed : ∀ (t : Set X) (ht : t ∈ 𝒫 s), IsClosed t
U V : (t : (↑(𝒫 s) : Type u)) → Set X
hU : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (U t)
hV : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (V t)
hUs : ∀ (t : (↑(𝒫 s) : Type u)), (↑t : Set X) ⊆ U t
hVs : ∀ (t : (↑(𝒫 s) : Type u)), s \ (↑t : Set X) ⊆ V t
hUV : ∀ (t : (↑(𝒫 s) : Type u)), Disjoint (U t) (V t)
hUd : ∀ {t₁ t₂ : (↑(𝒫 s) : Type u)} (h : U t₁ ∩ d = U t₂ ∩ d), (↑t₁ : Set X) ⊆ (↑t₂ : Set X)
h_inj : Injective (β := Set X) fun (x : (↑(𝒫 s) : Type u)) ↦ U x ∩ d
y : (↑(𝒫 s) : Type u)
⊢ U y ∩ d ∈ 𝒫 d

Tactic:
inter_subset_right

Premises used: Set.Mem, setOf, Set.powerset, Set.inter_subset_right
-- Module: Mathlib.Topology.Separation.NotNormal
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s d : Set X
hs : IsClosed s
inst_2 : DiscreteTopology.{u} (↑s : Type u)
hd : Dense d
h_closed : ∀ (t : Set X) (ht : t ∈ 𝒫 s), IsClosed t
U V : (t : (↑(𝒫 s) : Type u)) → Set X
hU : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (U t)
hV : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (V t)
hUs : ∀ (t : (↑(𝒫 s) : Type u)), (↑t : Set X) ⊆ U t
hVs : ∀ (t : (↑(𝒫 s) : Type u)), s \ (↑t : Set X) ⊆ V t
hUV : ∀ (t : (↑(𝒫 s) : Type u)), Disjoint (U t) (V t)
hUd : ∀ {t₁ t₂ : (↑(𝒫 s) : Type u)} (h : U t₁ ∩ d = U t₂ ∩ d), (↑t₁ : Set X) ⊆ (↑t₂ : Set X)
h_inj : Injective (β := Set X) fun (x : (↑(𝒫 s) : Type u)) ↦ U x ∩ d
y : (↑(𝒫 s) : Type u)
⊢ U y ∩ d ∈ 𝒫 d

Tactic:
exact inter_subset_right

Premises used: Set.inter_subset_right
-- Module: Mathlib.Topology.Separation.NotNormal
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s d : Set X
hs : IsClosed s
inst_2 : DiscreteTopology.{u} (↑s : Type u)
hd : Dense d
⊢ #(↑s : Type u) < HPow.hPow (α := Cardinal.{u}) 2 #(↑d : Type u)

Tactic:
(#s).cantor.trans_le <| hs.two_pow_mk_le_two_pow_mk_dense hd

Premises used: Cardinal.mk, Set.Elem, IsClosed.two_pow_mk_le_two_pow_mk_dense, Cardinal.cantor, LT.lt.trans_le
-- Module: Mathlib.Topology.Separation.NotNormal
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : SeparableSpace X
inst_2 : NormalSpace X
s : Set X
hs : IsClosed s
inst_3 : DiscreteTopology.{u} (↑s : Type u)
⊢ HPow.hPow (α := Cardinal.{u}) 2 #(↑s : Type u) ≤ 𝔠

Tactic:
have ⟨d, hd_countable, hd_dense⟩ := exists_countable_dense X
  calc
    2 ^ #s ≤ 2 ^ #d := hs.two_pow_mk_le_two_pow_mk_dense hd_dense
    _ ≤ 2 ^ ℵ₀ := power_le_power_left two_ne_zero hd_countable.le_aleph0
    _ = 𝔠 := two_power_aleph0

Premises used: _private.0.IsClosed.two_pow_mk_lt_continuum.match_1, Trans.trans, Cardinal.mk, Set.Elem, IsClosed.two_pow_mk_le_two_pow_mk_dense, LE.le, TopologicalSpace.exists_countable_dense, Cardinal.continuum, Set.Countable.le_aleph0, two_ne_zero, HPow.hPow, Cardinal.two_power_aleph0, OfNat.ofNat, Cardinal.power_le_power_left
-- Module: Mathlib.Topology.Separation.NotNormal
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : SeparableSpace X
inst_2 : NormalSpace X
s : Set X
hs : IsClosed s
inst_3 : DiscreteTopology.{u} (↑s : Type u)
⊢ #(↑s : Type u) < 𝔠

Tactic:
(#s).cantor.trans_le hs.two_pow_mk_lt_continuum

Premises used: Cardinal.mk, Set.Elem, IsClosed.two_pow_mk_lt_continuum, Cardinal.cantor, LT.lt.trans_le
-- Module: Mathlib.Topology.Separation.NotNormal
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : SeparableSpace X
s : Set X
hs : IsClosed s
inst_2 : DiscreteTopology.{u} (↑s : Type u)
hmk : 𝔠 ≤ #(↑s : Type u)
⊢ ¬NormalSpace X

Tactic:
fun _ ↦ hs.mk_lt_continuum.not_ge hmk

Premises used: IsClosed.mk_lt_continuum, LT.lt.not_ge, Not
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h : PerfectlyNormalSpace X
s : Set X
hs : IsClosed[inst] s
obtain :
  ∀ (U : ℕ → Set X) (ho : ∀ (n : ℕ), IsOpen[inst] (U n)) (hu : s = ⋂ (n : ℕ), U n),
    ∃ (f : C(X, ℝ)),
      s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
        ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
⊢ ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
obtain ⟨U, ho, hu⟩ := isGδ_iff_eq_iInter_nat.1 hs.isGδ

Premises used: IsClosed.isGδ, Iff.mp, isGδ_iff_eq_iInter_nat
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h : PerfectlyNormalSpace X
s : Set X
hs : IsClosed[inst] s
U : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen[inst] (U n)
hu : s = ⋂ (n : ℕ), U n
n : ℕ
a : s ⊆ U n
⊢ Disjoint s (U n)ᶜ

Tactic:
apply HasSubset.Subset.disjoint_compl_right

Premises used: HasSubset.Subset.disjoint_compl_right
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h : PerfectlyNormalSpace X
s : Set X
hs : IsClosed[inst] s
U : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen[inst] (U n)
hu : s = ⋂ (n : ℕ), U n
n : ℕ
a : ⋂ (n : ℕ), U n ⊆ U n
a₁ : U n ⊆ U n
a₂ : ℕ
a₃ : U n ⊆ U n
a₄ : ℕ
⊢ s ⊆ U n

Tactic:
grw [hu, iInter_subset]

Premises used: Set.iInter_subset
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h : PerfectlyNormalSpace X
s : Set X
hs : IsClosed[inst] s
U : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen[inst] (U n)
hu : s = ⋂ (n : ℕ), U n
⊢ ∀ (n : ℕ), Disjoint s (U n)ᶜ

Tactic:
have (n : ℕ) : Disjoint s (U n)ᶜ := by
      apply HasSubset.Subset.disjoint_compl_right
      grw [hu, iInter_subset]
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h : PerfectlyNormalSpace X
s : Set X
hs : IsClosed[inst] s
U : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen[inst] (U n)
hu : s = ⋂ (n : ℕ), U n
this : ∀ (n : ℕ), Disjoint s (U n)ᶜ
choose :
  ∀ (f : (n : ℕ) → C(X, ℝ)) (hfs : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 0 s)
    (hfu : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 1 (U n)ᶜ)
    (hfr : ∀ (n : ℕ) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f n : (a : X) → ℝ) x : ℝ)),
    ∃ (f : C(X, ℝ)),
      s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
        ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
⊢ ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
choose f hfs hfu hfr using fun n =>
      exists_continuous_zero_one_of_isClosed hs (ho n).isClosed_compl (this n)

Premises used: exists_continuous_zero_one_of_isClosed, IsOpen.isClosed_compl
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h : PerfectlyNormalSpace X
s : Set X
hs : IsClosed[inst] s
U : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen[inst] (U n)
hu : s = ⋂ (n : ℕ), U n
this : ∀ (n : ℕ), Disjoint s (U n)ᶜ
f : (n : ℕ) → C(X, ℝ)
hfs : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 0 s
hfu : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 1 (U n)ᶜ
hfr : ∀ (n : ℕ) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f n : (a : X) → ℝ) x : ℝ)
x : X
n : ℕ
⊢ ‖HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n)‖ ≤ 1 / 2 / HPow.hPow (α := ℝ) 2 n

Tactic:
simp [abs_of_nonneg (hfr n x).1, (hfr n x).2]

Premises used: And.right, And.left, abs_of_nonneg
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h : PerfectlyNormalSpace X
s : Set X
hs : IsClosed[inst] s
U : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen[inst] (U n)
hu : s = ⋂ (n : ℕ), U n
this : ∀ (n : ℕ), Disjoint s (U n)ᶜ
f : (n : ℕ) → C(X, ℝ)
hfs : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 0 s
hfu : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 1 (U n)ᶜ
hfr : ∀ (n : ℕ) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f n : (a : X) → ℝ) x : ℝ)
⊢ ∀ (x : X) (n : ℕ),
    ‖HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n)‖ ≤ 1 / 2 / HPow.hPow (α := ℝ) 2 n

Tactic:
have hsb (x : X) (n : ℕ) : ‖(f n) x * (1 / 2 / 2 ^ n)‖ ≤ 1 / 2 / 2 ^ n := by
      simp [abs_of_nonneg (hfr n x).1, (hfr n x).2]