awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
hfg : f x ≠ g x
⊢ ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x
have mp : ∀ (Uf Ug : Set Y) (h₁U : IsOpen[inst_1] Uf) (h₂U : IsOpen[inst_1] Ug) (h₃U : f x ∈ Uf) (h₄U : g x ∈ Ug)
  (h₅U : Disjoint Uf Ug), ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x
Tactic: obtain ⟨Uf, Ug, h₁U, h₂U, h₃U, h₄U, h₅U⟩ := t2_separation hfg
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
hfg : f x ≠ g x
Uf Ug : Set Y
h₁U : IsOpen[inst_1] Uf
h₂U : IsOpen[inst_1] Ug
h₃U : f x ∈ Uf
h₄U : g x ∈ Ug
h₅U : Disjoint Uf Ug
⊢ ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x
have h₅U₁ : Uf ∩ Ug = ∅
Tactic: rw [Set.disjoint_iff_inter_eq_empty] at h₅U
Cleared hypotheses: h₅U
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
hfg : f x ≠ g x
Uf Ug : Set Y
h₁U : IsOpen[inst_1] Uf
h₂U : IsOpen[inst_1] Ug
h₃U : f x ∈ Uf
h₄U : g x ∈ Ug
h₅U : Uf ∩ Ug = ∅
⊢ ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x
have h : ∀ a ∈ f ⁻¹' Uf ∩ g ⁻¹' Ug, f a ≠ g a
Tactic: filter_upwards [inter_mem
      (hf.preimage_mem_nhds (IsOpen.mem_nhds h₁U h₃U))
      (hg.preimage_mem_nhds (IsOpen.mem_nhds h₂U h₄U))]
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x_1 : X
f g : X → Y
hf : ContinuousAt f x_1
hg : ContinuousAt g x_1
hfg : f x_1 ≠ g x_1
Uf Ug : Set Y
h₁U : IsOpen[inst_1] Uf
h₂U : IsOpen[inst_1] Ug
h₃U : f x_1 ∈ Uf
h₄U : g x_1 ∈ Ug
h₅U : Uf ∩ Ug = ∅
x : X
hx : x ∈ f ⁻¹' Uf ∩ g ⁻¹' Ug
⊢ f x ≠ g x
have hx₁ : f x ∈ Uf ∧ g x ∈ Ug
Tactic: simp only [Set.mem_inter_iff, Set.mem_preimage] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x_1 : X
f g : X → Y
hf : ContinuousAt f x_1
hg : ContinuousAt g x_1
hfg : f x_1 ≠ g x_1
Uf Ug : Set Y
h₁U : IsOpen[inst_1] Uf
h₂U : IsOpen[inst_1] Ug
h₃U : f x_1 ∈ Uf
h₄U : g x_1 ∈ Ug
h₅U : Uf ∩ Ug = ∅
x : X
hx : f x ∈ Uf ∧ g x ∈ Ug
H : f x = g x
⊢ False
have hx₁ : g x ∈ Uf ∧ g x ∈ Ug
Tactic: rw [H] at hx
Cleared hypotheses: hx, H
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x_1 : X
f g : X → Y
hf : ContinuousAt f x_1
hg : ContinuousAt g x_1
hfg : f x_1 ≠ g x_1
Uf Ug : Set Y
h₁U : IsOpen[inst_1] Uf
h₂U : IsOpen[inst_1] Ug
h₃U : f x_1 ∈ Uf
h₄U : g x_1 ∈ Ug
h₅U : Uf ∩ Ug = ∅
x : X
hx : g x ∈ Uf ∧ g x ∈ Ug
H : f x = g x
⊢ False
have this : g x ∈ Uf ∩ Ug
Tactic: have : g x ∈ Uf ∩ Ug := hx
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
hfg : ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x
⊢ f x ≠ g x
have mpr : ∀ (t : Set X) (h₁t : ∀ y ∈ t, f y ≠ g y) (h₂t : IsOpen[inst] t) (h₃t : x ∈ t), f x ≠ g x
Tactic: obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 hfg
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst_3 : (𝓝[≠] x).NeBot
⊢ f =ᶠ[𝓝[≠] x] g ↔ f =ᶠ[𝓝 x] g
have mp : f =ᶠ[𝓝[≠] x] g → f =ᶠ[𝓝 x] g
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst_3 : (𝓝[≠] x).NeBot
mp : f =ᶠ[𝓝[≠] x] g → f =ᶠ[𝓝 x] g
⊢ f =ᶠ[𝓝[≠] x] g ↔ f =ᶠ[𝓝 x] g
have mpr : f =ᶠ[𝓝 x] g → f =ᶠ[𝓝[≠] x] g
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst_3 : (𝓝[≠] x).NeBot
hfg : f =ᶠ[𝓝[≠] x] g
⊢ f =ᶠ[𝓝 x] g
have mp : f x = g x
Tactic: apply eventuallyEq_nhds_of_eventuallyEq_nhdsNE hfg
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst_3 : (𝓝[≠] x).NeBot
hfg : f =ᶠ[𝓝[≠] x] g
⊢ f x = g x
have mp : ∀ (hCon : ¬f x = g x), False
Tactic: by_contra hCon
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst_3 : (𝓝[≠] x).NeBot
hfg : f =ᶠ[𝓝[≠] x] g
hCon : ¬f x = g x
⊢ Set.Nonempty.{u_1} (α := X) {x : X | f x ≠ g x ∧ f x = g x}
have h₁ : ∀ᶠ (x : X) in 𝓝[≠] x, f x ≠ g x ∧ f x = g x
Tactic: have h₁ := (eventually_nhdsWithin_of_eventually_nhds
        ((hf.ne_iff_eventually_ne hg).1 hCon)).and hfg
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst_3 : (𝓝[≠] x).NeBot
hfg : f =ᶠ[𝓝[≠] x] g
hCon : ¬f x = g x
h₁ : ∀ᶠ (x : X) in 𝓝[≠] x, f x ≠ g x ∧ f x = g x
⊢ Set.Nonempty.{u_1} (α := X) {x : X | f x ≠ g x ∧ f x = g x}
have h₂ : ∅ ∉ 𝓝[≠] x
Tactic: have h₂ : ∅ ∉ 𝓝[≠] x := by exact empty_notMem (𝓝[≠] x)
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst_3 : (𝓝[≠] x).NeBot
hfg : f =ᶠ[𝓝[≠] x] g
hCon : ¬f x = g x
⊢ False
have mp : ∀ (a : X) (ha : Membership.mem (γ := Set X) {x : X | f x ≠ g x ∧ f x = g x} a), False
Tactic: obtain ⟨a, ha⟩ : {x | f x ≠ g x ∧ f x = g x}.Nonempty := by
      have h₁ := (eventually_nhdsWithin_of_eventually_nhds
        ((hf.ne_iff_eventually_ne hg).1 hCon)).and hfg
      have h₂ : ∅ ∉ 𝓝[≠] x := by exact empty_notMem (𝓝[≠] x)
      simp_all
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
S : Set X
⊢ IsPreirreducible S ↔ ∀ x ∈ S, S ⊆ closure[inst] {x}
have mp : IsPreirreducible S → ∀ x ∈ S, S ⊆ closure[inst] {x}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
S : Set X
mp : IsPreirreducible S → ∀ x ∈ S, S ⊆ closure[inst] {x}
⊢ IsPreirreducible S ↔ ∀ x ∈ S, S ⊆ closure[inst] {x}
have mpr : (∀ x ∈ S, S ⊆ closure[inst] {x}) → IsPreirreducible S
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
S : Set X
h : IsPreirreducible S
x : X
hx : x ∈ S
y : X
hy : y ∈ S
⊢ Membership.mem (γ := Set X) (closure[inst] {x}) y
have mp : ∀ (e : y ∉ closure[inst] {x}), False
Tactic: by_contra e
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
S : Set X
h : IsPreirreducible S
x : X
hx : x ∈ S
y : X
hy : y ∈ S
e : y ∉ closure[inst] {x}
⊢ False
have mp : ∀ (U V : Set X) (hU : IsOpen[inst] U) (hV : IsOpen[inst] V) (hxU : x ∈ U) (hyV : y ∈ V) (h' : Disjoint U V), False
Tactic: obtain ⟨U, V, hU, hV, hxU, hyV, h'⟩ := r1_separation fun h => e h.specializes.mem_closure
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
S : Set X
h : ∀ x ∈ S, S ⊆ closure[inst] {x}
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
⊢ (S ∩ u).Nonempty → (S ∩ v).Nonempty → (S ∩ (u ∩ v)).Nonempty
have mpr : ∀ (x : X) (hxs : x ∈ S) (hxu : x ∈ u), (S ∩ v).Nonempty → (S ∩ (u ∩ v)).Nonempty
Tactic: ⟨x, hxs, hxu⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
S : Set X
h : ∀ x ∈ S, S ⊆ closure[inst] {x}
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
x : X
hxs : x ∈ S
hxu : x ∈ u
⊢ (S ∩ v).Nonempty → (S ∩ (u ∩ v)).Nonempty
have mpr : ∀ (y : X) (hys : y ∈ S) (hyv : y ∈ v), (S ∩ (u ∩ v)).Nonempty
Tactic: ⟨y, hys, hyv⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
S : Set X
⊢ IsIrreducible S ↔ ∃ (x : X), S = {x}
have rw : S.Nonempty ∧ IsPreirreducible S ↔ ∃ (x : X), S = {x}
Tactic: rw [IsIrreducible, isPreirreducible_iff_subsingleton,
    exists_eq_singleton_iff_nonempty_subsingleton]
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
S : Set X
rw : S.Nonempty ∧ IsPreirreducible S ↔ ∃ (x : X), S = {x}
⊢ IsIrreducible S ↔ ∃ (x : X), S = {x}
have rw₁ : S.Nonempty ∧ S.Subsingleton ↔ ∃ (x : X), S = {x}
Tactic: rw [IsIrreducible, isPreirreducible_iff_subsingleton,
    exists_eq_singleton_iff_nonempty_subsingleton]
-- Lean 4 proof step from Mathlib.Topology.Separation.Hausdorff (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
S : Set X
rw : S.Nonempty ∧ IsPreirreducible S ↔ ∃ (x : X), S = {x}
rw₁ : S.Nonempty ∧ S.Subsingleton ↔ ∃ (x : X), S = {x}
⊢ IsIrreducible S ↔ ∃ (x : X), S = {x}
have rw₂ : S.Nonempty ∧ S.Subsingleton ↔ S.Nonempty ∧ S.Subsingleton
Tactic: rw [IsIrreducible, isPreirreducible_iff_subsingleton,
    exists_eq_singleton_iff_nonempty_subsingleton]
-- Lean 4 proof step from Mathlib.Topology.Separation.Lemmas (goal)
Goal:
X : Type u_1
inst : MetricSpace X
s : Set X
hs : s.Countable
⊢ IsTotallyDisconnected s
have rw : TotallyDisconnectedSpace.{u_1} (↑s : Type u_1)
Tactic: rw [← totallyDisconnectedSpace_subtype_iff]
-- Lean 4 proof step from Mathlib.Topology.Separation.Lemmas (hypothesis)
Goal:
X : Type u_1
inst : MetricSpace X
s : Set X
hs : s.Countable
⊢ TotallyDisconnectedSpace.{u_1} (↑s : Type u_1)
have this : Countable.{u_1 + 1} (↑s : Type u_1)
Tactic: have : Countable s := hs
-- Lean 4 proof step from Mathlib.Topology.Separation.LinearUpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : Topology.IsUpperSet α
s t : Set α
hcst : Disjoint (closure s) t
hsct : Disjoint s (closure t)
⊢ Disjoint (nhdsSet s) (nhdsSet t)
have obtain : ∀ (hcst : Disjoint (closure ∅) t) (hsct : Disjoint ∅ (closure t)), Disjoint (nhdsSet ∅) (nhdsSet t)
Tactic: obtain (rfl | ⟨a, ha⟩) := s.eq_empty_or_nonempty
Cleared hypotheses: s, hcst, hsct
-- Lean 4 proof step from Mathlib.Topology.Separation.LinearUpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : Topology.IsUpperSet α
s t : Set α
hcst : Disjoint (closure s) t
hsct : Disjoint s (closure t)
obtain : ∀ (hcst : Disjoint (closure ∅) t) (hsct : Disjoint ∅ (closure t)), Disjoint (nhdsSet ∅) (nhdsSet t)
⊢ Disjoint (nhdsSet s) (nhdsSet t)
have inr : ∀ (a : α) (ha : a ∈ s), Disjoint (nhdsSet s) (nhdsSet t)
Tactic: obtain (rfl | ⟨a, ha⟩) := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Topology.Separation.LinearUpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : Topology.IsUpperSet α
s t : Set α
hcst : Disjoint (closure s) t
hsct : Disjoint s (closure t)
a : α
ha : a ∈ s
⊢ Disjoint (nhdsSet s) (nhdsSet t)
have obtain : ∀ (hcst : Disjoint (closure s) ∅) (hsct : Disjoint s (closure ∅)), Disjoint (nhdsSet s) (nhdsSet ∅)
Tactic: obtain (rfl | ⟨b, hb⟩) := t.eq_empty_or_nonempty
Cleared hypotheses: t, hcst, hsct
-- Lean 4 proof step from Mathlib.Topology.Separation.LinearUpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : Topology.IsUpperSet α
s t : Set α
hcst : Disjoint (closure s) t
hsct : Disjoint s (closure t)
a : α
ha : a ∈ s
obtain : ∀ (hcst : Disjoint (closure s) ∅) (hsct : Disjoint s (closure ∅)), Disjoint (nhdsSet s) (nhdsSet ∅)
⊢ Disjoint (nhdsSet s) (nhdsSet t)
have inr : ∀ (b : α) (hb : b ∈ t), Disjoint (nhdsSet s) (nhdsSet t)
Tactic: obtain (rfl | ⟨b, hb⟩) := t.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Topology.Separation.LinearUpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : Topology.IsUpperSet α
s t : Set α
hcst : Disjoint (closure s) t
hsct : Disjoint s (closure t)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
⊢ Disjoint (nhdsSet s) (nhdsSet t)
have inr : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Topology.Separation.LinearUpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : Topology.IsUpperSet α
s t : Set α
hcst : Disjoint (closure s) t
hsct : Disjoint s (closure t)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
⊢ False
have inr : ∀ (ha : a ∈ s) (b : α) (hsct : Disjoint (α := Set α) {a} (closure {b})) (hcst : Disjoint (α := Set α) (closure {a}) {b})
  (hb : b ∈ t), False
Tactic: grewrite [← singleton_subset_iff.mpr ha, ← singleton_subset_iff.mpr hb] at hcst hsct
Cleared hypotheses: hcst, hsct, ha, b, hb
-- Lean 4 proof step from Mathlib.Topology.Separation.LinearUpperLowerSetTopology (hypothesis)
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
⊢ False
have hcst₁ : a < b
Tactic: conv at hcst => equals a < b => simp
Cleared hypotheses: hcst, hb
-- Lean 4 proof step from Mathlib.Topology.Separation.LinearUpperLowerSetTopology (hypothesis)
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
⊢ False
have hsct₁ : b < a
Tactic: conv at hsct => equals b < a => simp
Cleared hypotheses: hsct, hcst, hb
-- Lean 4 proof step from Mathlib.Topology.Separation.NotNormal (goal)
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
have rw : IsClosed
  (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))
    (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t))
Tactic: rw [← inter_eq_self_of_subset_right ht, ← Subtype.image_preimage_val]
-- Lean 4 proof step from Mathlib.Topology.Separation.NotNormal (hypothesis)
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
⊢ HPow.hPow (α := Cardinal.{u}) 2 #(↑s : Type u) ≤ HPow.hPow (α := Cardinal.{u}) 2 #(↑d : Type u)
have h_closed : ∀ (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 _)
-- Lean 4 proof step from Mathlib.Topology.Separation.NotNormal (goal)
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
⊢ HPow.hPow (α := Cardinal.{u}) 2 #(↑s : Type u) ≤ HPow.hPow (α := Cardinal.{u}) 2 #(↑d : Type u)
have 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)
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
-- Lean 4 proof step from Mathlib.Topology.Separation.NotNormal (goal)
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)
have by_contra : ∀ (ht : ¬(↑t₁ : Set X) ⊆ (↑t₂ : Set X)), False
Tactic: by_contra ht
-- Lean 4 proof step from Mathlib.Topology.Separation.NotNormal (hypothesis)
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)
⊢ False
have ht₁ : ((↑t₁ : Set X) \ (↑t₂ : Set X)).Nonempty
Tactic: rw [← diff_nonempty] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Topology.Separation.NotNormal (hypothesis)
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
⊢ False
have hUVd : (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₂))
-- Lean 4 proof step from Mathlib.Topology.Separation.NotNormal (hypothesis)
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
⊢ False
have hUVd₁ : (U t₂ ∩ d ∩ V t₂).Nonempty
Tactic: rw [inter_right_comm, h] at hUVd
Cleared hypotheses: hUVd
-- Lean 4 proof step from Mathlib.Topology.Separation.NotNormal (hypothesis)
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)
⊢ HPow.hPow (α := Cardinal.{u}) 2 #(↑s : Type u) ≤ HPow.hPow (α := Cardinal.{u}) 2 #(↑d : Type u)
have hUd : ∀ {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₂)
-- Lean 4 proof step from Mathlib.Topology.Separation.NotNormal (hypothesis)
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)
⊢ HPow.hPow (α := Cardinal.{u}) 2 #(↑s : Type u) ≤ HPow.hPow (α := Cardinal.{u}) 2 #(↑d : Type u)
have h_inj : 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)
-- Lean 4 proof step from Mathlib.Topology.Separation.NotNormal (goal)
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
⊢ HPow.hPow (α := Cardinal.{u}) 2 #(↑s : Type u) ≤ HPow.hPow (α := Cardinal.{u}) 2 #(↑d : Type u)
have rw : #(↑(range fun (x : (↑(𝒫 s) : Type u)) ↦ U x ∩ d) : Type u) ≤ #(↑(𝒫 d) : Type u)
Tactic: rw [← mk_powerset, ← mk_powerset, ← mk_range_eq _ h_inj]
-- Lean 4 proof step from Mathlib.Topology.Separation.NotNormal (goal)
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
⊢ #(↑(range fun (x : (↑(𝒫 s) : Type u)) ↦ U x ∩ d) : Type u) ≤ #(↑(𝒫 d) : Type u)
have h : (range fun (x : (↑(𝒫 s) : Type u)) ↦ U x ∩ d) ⊆ 𝒫 d
Tactic: apply mk_le_mk_of_subset