mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: case neg
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun x ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s | s ∈ B ∧ IsClosed[inst✝⁴] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst✝⁴] Z
hZ_nonempty : Z.Nonempty
hZ_irred : ¬IsIrreducible Z
⊢ False

Tactic:
simp only [IsIrreducible, hZ_nonempty, true_and] at hZ_irred
    obtain ⟨Y₁, Y₂, hY₁_cl, hY₂_cl, hc₁, hc₂, hsub, ⟨x₁, hx₁⟩, ⟨x₂, hx₂⟩⟩ :=
      PrespectralSpace.exists_isClosed_of_not_isPreirreducible _ hZ_irred
    have hY₁ : Y₁ ∈ 𝔅 := .inr ⟨hY₁_cl, hc₁⟩
    have hY₂ : Y₂ ∈ 𝔅 := .inr ⟨hY₂_cl, hc₂⟩
    have hY₁_inter_B : Y₁ ∩ ⋂₀ B = ∅ := by grind
    have hY₂_inter_B : Y₂ ∩ ⋂₀ B = ∅ := by grind
    -- By maximality of `B`, neither `B ∪ {Y₁}` nor `B ∪ {Y₂}` is contained in `𝒮`
    have hY₁B : insert Y₁ B ∉ 𝒮 := by
      intro hY₁B
      grind [show insert Y₁ B ⊆ B from hB.le_of_ge hY₁B (Set.subset_insert Y₁ B)]
    have hY₂B : insert Y₂ B ∉ 𝒮 := by
      intro hY₂B
      grind [show insert Y₂ B ⊆ B from hB.le_of_ge hY₂B (Set.subset_insert Y₂ B)]
    dsimp [𝒮] at hY₁B hY₂B
    simp only [Set.insert_subset_iff, hY₁, hB.prop.1, and_self, Set.sInter_insert, hY₁_inter_B,
      and_true, true_and, not_forall, Set.not_nonempty_iff_eq_empty, hY₂, hY₂_inter_B] at hY₁B hY₂B
    -- Hence there exist finitely many `{Aᵢ} ⊆ B` such that `Z ∩ ⋂ Aᵢ = ∅`.
    obtain ⟨A₁, hA₁, hA₁', hA₁''⟩ := hY₁B
    obtain ⟨A₂, hA₂, hA₂', hA₂''⟩ := hY₂B
    have : Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂}) = ∅ := by grind
    rw [← Set.not_nonempty_iff_eq_empty] at this
    apply this
    rw [Set.inter_comm]
    refine IsCompact.nonempty_inter_sInter ?_ (fun _ hb ↦ hb.2) fun F hsub hF ↦ ?_
    · apply isCompact_sInter_of_subset_constructibleTopologySubbasis _ (hA₁'.sdiff.union hA₂'.sdiff)
      grind [hB.prop, Set.union_subset_iff]
    · rw [← Set.sInter_union]
      refine hB.prop.2.1 (_ ∪ F) ?_ <| (hA₁'.sdiff.union hA₂'.sdiff).union hF
      grind [Set.sdiff_singleton_subset_iff, Set.union_subset_iff]

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ultra.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : UniformSpace X
inst✝ : IsUltraUniformity X
x : X
s : Set X
⊢ s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s

Tactic:
rw [UniformSpace.mem_nhds_iff]

Goal state after:
X : Type u_1
inst✝¹ : UniformSpace X
inst✝ : IsUltraUniformity X
x : X
s : Set X
⊢ (∃ V ∈ 𝓤 X, ball x V ⊆ s) ↔ ∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s
Module: Mathlib.Topology.UniformSpace.OfCompactT2

Goal state before:
pp: γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x : γ
⊢ 𝓝 x = ⨆ i, comap (fun x_1 ↦ x) (𝓝 i) ⊓ 𝓝 i

Tactic:
rw [iSup_split _ (Inseparable x)]

Goal state after:
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x : γ
⊢ 𝓝 x =
    (⨆ i, ⨆ (_ : Inseparable x i), comap (fun x_2 ↦ x) (𝓝 i) ⊓ 𝓝 i) ⊔
      ⨆ i, ⨆ (_ : ¬Inseparable x i), comap (fun x_2 ↦ x) (𝓝 i) ⊓ 𝓝 i