awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (hypothesis)
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
b : Bool
x : (↑(S b) : Type u)
hST : Disjoint (S b) (closure[inst.toTopologicalSpace] (S !b))
⊢ ∃ (i : ι), Disjoint (ball (↑x : α) ((B i).comp (B i).inv)) (S !b)
have hST₁ : (S !b)ᶜ ∈ 𝓝ˢ (S b)
Tactic: rw [← disjoint_nhdsSet_principal, disjoint_principal_right] at hST
Cleared hypotheses: hST
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
b : Bool
x : (↑(S b) : Type u)
hST : (S !b)ᶜ ∈ 𝓝ˢ (S b)
⊢ ∃ (i : ι), Disjoint (ball (↑x : α) ((B i).comp (B i).inv)) (S !b)
have obtain : ∀ (U : Set (α × α)) (hUu : U ∈ 𝓤 α) (hU : ball (↑x : α) U ⊆ (S !b)ᶜ),
  ∃ (i : ι), Disjoint (ball (↑x : α) ((B i).comp (B i).inv)) (S !b)
Tactic: obtain ⟨U, hUu, hU⟩ := UniformSpace.mem_nhds_iff.1 (nhds_le_nhdsSet x.2 hST)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
b : Bool
x : (↑(S b) : Type u)
hST : (S !b)ᶜ ∈ 𝓝ˢ (S b)
U : Set (α × α)
hUu : U ∈ 𝓤 α
hU : ball (↑x : α) U ⊆ (S !b)ᶜ
⊢ ∃ (i : ι), Disjoint (ball (↑x : α) ((B i).comp (B i).inv)) (S !b)
have obtain : ∀ (V : SetRel α α) (hV : V ∈ 𝓤 α) (hVs : V.IsSymm) (hVU : V.comp V ⊆ U),
  ∃ (i : ι), Disjoint (ball (↑x : α) ((B i).comp (B i).inv)) (S !b)
Tactic: obtain ⟨(V : SetRel α α), hV, hVs, hVU⟩ := comp_symm_mem_uniformity_sets hUu
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
b : Bool
x : (↑(S b) : Type u)
hST : (S !b)ᶜ ∈ 𝓝ˢ (S b)
U : Set (α × α)
hUu : U ∈ 𝓤 α
hU : ball (↑x : α) U ⊆ (S !b)ᶜ
V : SetRel α α
hV : V ∈ 𝓤 α
hVs : V.IsSymm
hVU : V.comp V ⊆ U
⊢ ∃ (i : ι), Disjoint (ball (↑x : α) ((B i).comp (B i).inv)) (S !b)
have obtain : ∀ (i : ι) (hi : B i ⊆ V), ∃ (i : ι), Disjoint (ball (↑x : α) ((B i).comp (B i).inv)) (S !b)
Tactic: obtain ⟨i, hi⟩ := hB.mem_iff.1 hV
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
b : Bool
x : (↑(S b) : Type u)
hST : (S !b)ᶜ ∈ 𝓝ˢ (S b)
U : Set (α × α)
hUu : U ∈ 𝓤 α
hU : ball (↑x : α) U ⊆ (S !b)ᶜ
V : SetRel α α
hV : V ∈ 𝓤 α
hVs : V.IsSymm
hVU : V.comp V ⊆ U
i : ι
hi : B i ⊆ V
⊢ ∃ (i : ι), Disjoint (ball (↑x : α) ((B i).comp (B i).inv)) (S !b)
have refine : (B i).comp (B i).inv ⊆ U
Tactic: refine ⟨i, subset_compl_iff_disjoint_right.1 (subset_trans (ball_mono ?_ x.1) hU)⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (hypothesis)
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
have hx : ∀ (b : Bool) (x : (↑(S b) : Type u)), ∃ (i : ι), Disjoint (ball (↑x : α) ((B i).comp (B i).inv)) (S !b)
Tactic: have hx (b : Bool) (x : S b) : ∃ i, Disjoint (ball x.1 ((B i).comp (B i).inv)) (S (!b)) := by
      have hST : Disjoint (S b) (closure (S !b)) := b.casesOn (false := hsT) (true := hSt.symm)
      rw [← disjoint_nhdsSet_principal, disjoint_principal_right] at hST
      obtain ⟨U, hUu, hU⟩ := UniformSpace.mem_nhds_iff.1 (nhds_le_nhdsSet x.2 hST)
      obtain ⟨(V : SetRel α α), hV, hVs, hVU⟩ := comp_symm_mem_uniformity_sets hUu
      obtain ⟨i, hi⟩ := hB.mem_iff.1 hV
      refine ⟨i, subset_compl_iff_disjoint_right.1 (subset_trans (ball_mono ?_ x.1) hU)⟩
      exact subset_trans (SetRel.comp_subset_comp hi (V.inv_eq_self ▸ (SetRel.inv_mono hi))) hVU
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
hx : ∀ (b : Bool) (x : (↑(S b) : Type u)), ∃ (i : ι), Disjoint (ball (↑x : α) ((B i).comp (B i).inv)) (S !b)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
have choose : ∀ (U : (b : Bool) → (x : (↑(S b) : Type u)) → ι)
  (hU : ∀ (b : Bool) (x : (↑(S b) : Type u)), Disjoint (ball (↑x : α) ((B (U b x)).comp (B (U b x)).inv)) (S !b)),
  Disjoint (𝓝ˢ s) (𝓝ˢ t)
Tactic: choose U hU using hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
U : (b : Bool) → (x : (↑(S b) : Type u)) → ι
hU : ∀ (b : Bool) (x : (↑(S b) : Type u)), Disjoint (ball (↑x : α) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
b : Bool
⊢ ⋃ (x : (↑(S b) : Type u)), ball (↑x : α) (B (U b x)) ∈ 𝓝ˢ (S b)
have rw : ∀ x ∈ S b, ⋃ (x : (↑(S b) : Type u)), ball (↑x : α) (B (U b x)) ∈ 𝓝 x
Tactic: rw [mem_nhdsSet_iff_forall]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
U : (b : Bool) → (x : (↑(S b) : Type u)) → ι
hU : ∀ (b : Bool) (x : (↑(S b) : Type u)), Disjoint (ball (↑x : α) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
b : Bool
x : α
hx : x ∈ S b
⊢ ⋃ (x : (↑(S b) : Type u)), ball (↑x : α) (B (U b x)) ∈ 𝓝 x
have apply : ball x (B (U b (Subtype.mk (p := fun (x : α) ↦ x ∈ S b) x hx))) ⊆ ⋃ (x : (↑(S b) : Type u)), ball (↑x : α) (B (U b x))
Tactic: apply mem_of_superset (ball_mem_nhds x (hB.mem (U b ⟨x, hx⟩)))
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (hypothesis)
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
U : (b : Bool) → (x : (↑(S b) : Type u)) → ι
hU : ∀ (b : Bool) (x : (↑(S b) : Type u)), Disjoint (ball (↑x : α) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
have hUS : ∀ (b : Bool), ⋃ (x : (↑(S b) : Type u)), ball (↑x : α) (B (U b x)) ∈ 𝓝ˢ (S b)
Tactic: have hUS (b : Bool) : ⋃ x, ball x.1 (B (U b x)) ∈ nhdsSet (S b) := by
      rw [mem_nhdsSet_iff_forall]
      intro x hx
      apply mem_of_superset (ball_mem_nhds x (hB.mem (U b ⟨x, hx⟩)))
      exact subset_iUnion (fun x => ball x.1 (B (U b x))) ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
U : (b : Bool) → (x : (↑(S b) : Type u)) → ι
hU : ∀ (b : Bool) (x : (↑(S b) : Type u)), Disjoint (ball (↑x : α) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
hUS : ∀ (b : Bool), ⋃ (x : (↑(S b) : Type u)), ball (↑x : α) (B (U b x)) ∈ 𝓝ˢ (S b)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
have rw : ∃ s_1 ∈ 𝓝ˢ s, ∃ t_1 ∈ 𝓝ˢ t, Disjoint s_1 t_1
Tactic: rw [Filter.disjoint_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
U : (b : Bool) → (x : (↑(S b) : Type u)) → ι
hU : ∀ (b : Bool) (x : (↑(S b) : Type u)), Disjoint (ball (↑x : α) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
hUS : ∀ (b : Bool), ⋃ (x : (↑(S b) : Type u)), ball (↑x : α) (B (U b x)) ∈ 𝓝ˢ (S b)
⊢ ∃ s_1 ∈ 𝓝ˢ s, ∃ t_1 ∈ 𝓝ˢ t, Disjoint s_1 t_1
have refine : Disjoint.{u} (α := Set α) (⋃ (x : (↑(S false) : Type u)), ball (↑x : α) (B (U false x)))
  (⋃ (x : (↑(S true) : Type u)), ball (↑x : α) (B (U true x)))
Tactic: refine ⟨_, hUS false, _, hUS true, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
U : (b : Bool) → (x : (↑(S b) : Type u)) → ι
hU : ∀ (b : Bool) (x : (↑(S b) : Type u)), Disjoint (ball (↑x : α) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
hUS : ∀ (b : Bool), ⋃ (x : (↑(S b) : Type u)), ball (↑x : α) (B (U b x)) ∈ 𝓝ˢ (S b)
b : Bool
x : (↑(S b) : Type u)
y : (↑(S !b) : Type u)
hxy : U b x ≤ U (!b) y
⊢ Disjoint (ball (↑x : α) (B (U b x))) (ball (↑y : α) (B (U (!b) y)))
have rw : ball (↑x : α) (B (U b x)) ∩ ball (↑y : α) (B (U (!b) y)) ⊆ ∅
Tactic: rw [Set.disjoint_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (hypothesis)
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
U : (b : Bool) → (x : (↑(S b) : Type u)) → ι
hU : ∀ (b : Bool) (x : (↑(S b) : Type u)), Disjoint (ball (↑x : α) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
hUS : ∀ (b : Bool), ⋃ (x : (↑(S b) : Type u)), ball (↑x : α) (B (U b x)) ∈ 𝓝ˢ (S b)
⊢ Disjoint.{u} (α := Set α) (⋃ (x : (↑(S false) : Type u)), ball (↑x : α) (B (U false x)))
    (⋃ (x : (↑(S true) : Type u)), ball (↑x : α) (B (U true x)))
have hdj : ∀ (b : Bool) (x : (↑(S b) : Type u)) (y : (↑(S !b) : Type u)) (hxy : U b x ≤ U (!b) y),
  Disjoint (ball (↑x : α) (B (U b x))) (ball (↑y : α) (B (U (!b) y)))
Tactic: have hdj (b : Bool) (x : S b) (y : S (!b)) (hxy : U b x ≤ U (!b) y) :
        Disjoint (ball x.1 (B (U b x))) (ball y.1 (B (U (!b) y))) := by
      rw [Set.disjoint_iff]
      intro z hz
      exact (hU b x).notMem_of_mem_left (mem_ball_comp hz.1 (hB.antitone hxy hz.2)) y.2
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
U : (b : Bool) → (x : (↑(S b) : Type u)) → ι
hU : ∀ (b : Bool) (x : (↑(S b) : Type u)), Disjoint (ball (↑x : α) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
hUS : ∀ (b : Bool), ⋃ (x : (↑(S b) : Type u)), ball (↑x : α) (B (U b x)) ∈ 𝓝ˢ (S b)
hdj :
  ∀ (b : Bool) (x : (↑(S b) : Type u)) (y : (↑(S !b) : Type u)) (hxy : U b x ≤ U (!b) y),
    Disjoint (ball (↑x : α) (B (U b x))) (ball (↑y : α) (B (U (!b) y)))
⊢ Disjoint.{u} (α := Set α) (⋃ (x : (↑(S false) : Type u)), ball (↑x : α) (B (U false x)))
    (⋃ (x : (↑(S true) : Type u)), ball (↑x : α) (B (U true x)))
have simp_rw : ∀ (i : (↑(S false) : Type u)) (i_1 : (↑(S true) : Type u)),
  Disjoint (ball (↑i : α) (B (U false i))) (ball (↑i_1 : α) (B (U true i_1)))
Tactic: simp_rw [disjoint_iUnion_left, disjoint_iUnion_right]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
x y : α
h : Inseparable x y
⊢ 𝓝 (x, y) ≤ 𝓤 α
have rw : 𝓝 (y, y) ≤ 𝓤 α
Tactic: rw [h.prod rfl]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
x y : α
⊢ Inseparable x y ↔ ClusterPt (x, y) (𝓤 α)
have refine : ∀ (h : ClusterPt (x, y) (𝓤 α)), Inseparable x y
Tactic: refine ⟨fun h ↦ .of_nhds_le h.nhds_le_uniformity, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
x y : α
h : ClusterPt (x, y) (𝓤 α)
⊢ Inseparable x y
have simp_rw : ∀ (i : SetRel α α), (i ∈ 𝓤 α ∧ ∀ (a : α × α), ClusterPt a (𝓟 i) → a ∈ i) → (x, y) ∈ id i
Tactic: simp_rw [uniformity_hasBasis_closed.inseparable_iff_uniformity, isClosed_iff_clusterPt]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
⊢ T0Space α ↔ (𝓤 α).ker = diagonal α
have simp_rw : (∀ (x y : α), (∀ r ∈ 𝓤 α, (x, y) ∈ r) → x = y) → ∀ (x : α), ∀ s ∈ 𝓤 α, (x, x) ∈ s
Tactic: simp_rw [t0Space_iff_uniformity, subset_antisymm_iff, diagonal_subset_iff, subset_def,
    Prod.forall, Filter.mem_ker, mem_diagonal_iff, iff_self_and]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
β : Type u_1
l : Filter β
inst_1 : l.NeBot
f g : β → α
a b : α
ha : Tendsto f l (𝓝 a)
hb : Tendsto g l (𝓝 b)
⊢ Inseparable a b ↔ Tendsto (fun (x : β) ↦ (f x, g x)) l (𝓤 α)
have refine : ∀ (h : Tendsto (fun (x : β) ↦ (f x, g x)) l (𝓤 α)), Inseparable a b
Tactic: refine ⟨fun h ↦ (ha.prodMk_nhds hb).mono_right h.nhds_le_uniformity, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
β : Type u_1
l : Filter β
inst_1 : l.NeBot
f g : β → α
a b : α
ha : Tendsto f l (𝓝 a)
hb : Tendsto g l (𝓝 b)
h : Tendsto (fun (x : β) ↦ (f x, g x)) l (𝓤 α)
⊢ Inseparable a b
have rw : ClusterPt (a, b) (𝓤 α)
Tactic: rw [inseparable_iff_clusterPt_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
inst_1 : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun (x y : α) ↦ (x, y) ∉ V₀
⊢ IsClosed[inst.toTopologicalSpace] s
have rcases : ∀ (V₁ : Set (α × α)) (V₁_in : V₁ ∈ 𝓤 α) (V₁_symm : SetRel.IsSymm V₁) (h_comp : SetRel.comp V₁ V₁ ⊆ V₀),
  IsClosed[inst.toTopologicalSpace] s
Tactic: rcases comp_symm_mem_uniformity_sets V₀_in with ⟨V₁, V₁_in, V₁_symm, h_comp⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
inst_1 : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun (x y : α) ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
⊢ IsClosed[inst.toTopologicalSpace] s
have h : closure[inst.toTopologicalSpace] s ⊆ s
Tactic: apply isClosed_of_closure_subset
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (hypothesis)
Goal:
α : Type u
inst : UniformSpace α
inst_1 : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun (x y : α) ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : x ∈ closure[inst.toTopologicalSpace] s
⊢ x ∈ s
have hx₁ : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
Tactic: rw [mem_closure_iff_ball] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
inst_1 : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun (x y : α) ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
⊢ x ∈ s
have h : ∀ (y : α) (hy : y ∈ ball x V₁) (hy' : y ∈ s), x ∈ s
Tactic: rcases hx V₁_in with ⟨y, hy, hy'⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
inst_1 : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun (x y : α) ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
⊢ x ∈ s
have h : x = y
Tactic: suffices x = y by rwa [this]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
inst_1 : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun (x y : α) ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
⊢ x = y
have h : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → SetRel.IsSymm V → (x, y) ∈ V
Tactic: apply eq_of_forall_symmetric
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
inst_1 : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun (x y : α) ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
h : SetRel.IsSymm V
⊢ (x, y) ∈ V
have h : ∀ (z : α) (hz : z ∈ ball x (V₁ ∩ V)) (hz' : z ∈ s), (x, y) ∈ V
Tactic: rcases hx (inter_mem V₁_in V_in) with ⟨z, hz, hz'⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
inst_1 : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun (x y : α) ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
h : SetRel.IsSymm V
z : α
hz : z ∈ ball x (V₁ ∩ V)
hz' : z ∈ s
⊢ z = y
have by_contra : ∀ (hzy : ¬z = y), False
Tactic: by_contra hzy
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
inst_1 : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun (x y : α) ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
h : SetRel.IsSymm V
z : α
hz : z ∈ ball x (V₁ ∩ V)
hz' : z ∈ s
⊢ (x, y) ∈ V
have h : ∀ (hy : z ∈ ball x V₁) (hy' : z ∈ s), (x, z) ∈ V
Tactic: obtain rfl : z = y := by
    by_contra hzy
    exact hs hz' hy' hzy (h_comp <| mem_comp_of_mem_ball (ball_inter_left x _ _ hz) hy)
Cleared hypotheses: y, hy, hy'
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
⊢ Filter.comap (β := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk) (map (Prod.map mk mk) (𝓤 α)) = 𝓤 α
have refine : Filter.comap (β := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk) (map (Prod.map mk mk) (𝓤 α)) ≤ 𝓤 α
Tactic: refine le_antisymm ?_ le_comap_map
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
⊢ Filter.comap (β := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk) (map (Prod.map mk mk) (𝓤 α)) ≤ 𝓤 α
have refine : ∀ (U : SetRel α α) (hU : U ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] U),
  ∃ i ∈ 𝓤 α,
    preimage (β := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk) (Prod.map mk mk '' id i) ⊆ id U
Tactic: refine ((((𝓤 α).basis_sets.map _).comap _).le_basis_iff uniformity_hasBasis_open).2 fun U hU ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
inst : UniformSpace α
U : SetRel α α
hU : U ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] U
⊢ ∃ i ∈ 𝓤 α,
    preimage (β := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk) (Prod.map mk mk '' id i) ⊆ id U
have refine : ∀ (x : α × α) (x₁ x₂ : α),
  (x₁, x₂) ∈ preimage (β := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk) (Prod.map mk mk '' id U) →
    ∀ (y₁ y₂ : α) (hyU : (y₁, y₂) ∈ id U)
      (hxy : Eq (α := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk (y₁, y₂)) (Prod.map mk mk (x₁, x₂))),
      (x₁, x₂) ∈ id U
Tactic: refine ⟨U, hU.1, fun (x₁, x₂) ⟨(y₁, y₂), hyU, hxy⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (hypothesis)
Goal:
α : Type u
inst : UniformSpace α
U : SetRel α α
hU : U ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] U
x : α × α
x₁ x₂ : α
h : (x₁, x₂) ∈ preimage (β := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk) (Prod.map mk mk '' id U)
y₁ y₂ : α
hyU : (y₁, y₂) ∈ id U
hxy : Eq (α := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk (y₁, y₂)) (Prod.map mk mk (x₁, x₂))
⊢ (x₁, x₂) ∈ id U
have hxy₁ : Inseparable y₁ x₁ ∧ Inseparable y₂ x₂
Tactic: simp only [Prod.map, Prod.ext_iff, mk_eq_mk] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
t : Set (SeparationQuotient α × SeparationQuotient α)
ht : Membership.mem (γ := Filter (SeparationQuotient α × SeparationQuotient α)) (map (Prod.map mk mk) (𝓤 α)) t
⊢ Membership.mem (γ := Filter (SeparationQuotient α × SeparationQuotient α))
    (Filter.lift' (α := SeparationQuotient α × SeparationQuotient α) (map (Prod.map mk mk) (𝓤 α))
      fun (s : Set (SeparationQuotient α × SeparationQuotient α)) ↦ SetRel.comp s s)
    t
have rcases : ∀ (U : Set (α × α)) (hU : U ∈ 𝓤 α) (hUo : IsOpen[instTopologicalSpaceProd] U)
  (hUt : SetRel.comp U U ⊆ Prod.map mk mk ⁻¹' t),
  Membership.mem (γ := Filter (SeparationQuotient α × SeparationQuotient α))
    (Filter.lift' (α := SeparationQuotient α × SeparationQuotient α) (map (Prod.map mk mk) (𝓤 α))
      fun (s : Set (SeparationQuotient α × SeparationQuotient α)) ↦ SetRel.comp s s)
    t
Tactic: rcases comp_open_symm_mem_uniformity_sets ht with ⟨U, hU, hUo, -, hUt⟩