mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
Comm : toGlueL hΦ hΨ ∘ optimalGHInjr X Y = toGlueR hΦ hΨ ∘ optimalGHInjl Y Z
⊢ hausdorffDist (range (toGlueL hΦ hΨ ∘ optimalGHInjl X Y)) (range (toGlueR hΦ hΨ ∘ optimalGHInjr Y Z)) ≤
    hausdorffDist (range (toGlueL hΦ hΨ ∘ optimalGHInjl X Y)) (range (toGlueL hΦ hΨ ∘ optimalGHInjr X Y)) +
      hausdorffDist (range (toGlueL hΦ hΨ ∘ optimalGHInjr X Y)) (range (toGlueR hΦ hΨ ∘ optimalGHInjr Y Z))

Tactic:
refine hausdorffDist_triangle <| hausdorffEDist_ne_top_of_nonempty_of_bounded
          (range_nonempty _) (range_nonempty _) ?_ ?_

Goal state after:
case refine_1
x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
Comm : toGlueL hΦ hΨ ∘ optimalGHInjr X Y = toGlueR hΦ hΨ ∘ optimalGHInjl Y Z
⊢ Bornology.IsBounded (range (toGlueL hΦ hΨ ∘ optimalGHInjl X Y))

case refine_2
x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
Comm : toGlueL hΦ hΨ ∘ optimalGHInjr X Y = toGlueR hΦ hΨ ∘ optimalGHInjl Y Z
⊢ Bornology.IsBounded (range (toGlueL hΦ hΨ ∘ optimalGHInjr X Y))
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : p₀ ⤳ y
U V : (OpenNhds y)ᵒᵖ
inc : U ⟶ V
⊢ ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A).map inc ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ ((Functor.const (OpenNhds y)ᵒᵖ).obj A).map inc

Tactic:
change dite _ _ _ ≫ _ = _; rw [dif_pos]
        swap
        · exact h.mem_open V.unop.1.2 V.unop.2
        · simp only [Functor.comp_obj, Functor.op_obj, skyscraperPresheaf_obj, unop_op,
            Functor.const_obj_obj, eqToHom_trans, Functor.const_obj_map, Category.comp_id]

Goal state after:
Module: Mathlib.Topology.Sheaves.Abelian

Goal state before:
pp: X✝ : TopCat
C : Type v
inst✝⁶ : Category.{u, v} C
inst✝⁵ : HasColimits C
inst✝⁴ : HasLimits C
FC : C → C → Type u_1
CC : C → Type u
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝² : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : Abelian C
X : TopCat
p₀ : ↑X
S : ShortComplex (Sheaf C X)
h : S.ShortExact
this✝ :
  ∀ (S : ShortComplex (Sheaf C X)),
    S.ShortExact → (S.map (forget C X ⋙ stalkFunctor C p₀)).Exact ∧ Epi ((forget C X ⋙ stalkFunctor C p₀).map S.g)
this : Mono S.f
⊢ Mono (S.map (forget C X ⋙ stalkFunctor C p₀)).f

Tactic:
exact Functor.map_mono (forget C X ⋙ stalkFunctor C p₀) _

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case zero.one.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ (diagram F U).map WalkingParallelPairHom.left ≫
      (WalkingParallelPair.casesOn WalkingParallelPair.one (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom =
    (WalkingParallelPair.casesOn WalkingParallelPair.zero (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom ≫
      (diagram G U).map WalkingParallelPairHom.left

pp: case zero.one.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ (diagram F U).map WalkingParallelPairHom.right ≫
      (WalkingParallelPair.casesOn WalkingParallelPair.one (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom =
    (WalkingParallelPair.casesOn WalkingParallelPair.zero (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom ≫
      (diagram G U).map WalkingParallelPairHom.right

pp: case one.one.id
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ (diagram F U).map (WalkingParallelPairHom.id WalkingParallelPair.one) ≫
      (WalkingParallelPair.casesOn WalkingParallelPair.one (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom =
    (WalkingParallelPair.casesOn WalkingParallelPair.one (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom ≫
      (diagram G U).map (WalkingParallelPairHom.id WalkingParallelPair.one)

Tactic:
· dsimp
        refine Pi.hom_ext _ _ fun b ↦ ?_
        simp [leftRes]

Goal state after:
case zero.one.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ (diagram F U).map WalkingParallelPairHom.right ≫
      (WalkingParallelPair.casesOn WalkingParallelPair.one (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom =
    (WalkingParallelPair.casesOn WalkingParallelPair.zero (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom ≫
      (diagram G U).map WalkingParallelPairHom.right

case one.one.id
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ (diagram F U).map (WalkingParallelPairHom.id WalkingParallelPair.one) ≫
      (WalkingParallelPair.casesOn WalkingParallelPair.one (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom =
    (WalkingParallelPair.casesOn WalkingParallelPair.one (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom ≫
      (diagram G U).map (WalkingParallelPairHom.id WalkingParallelPair.one)
Module: Mathlib.Topology.Sheaves.Sheafify

Goal state before:
pp: case h.refine_3
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : ↥↑U) → F.stalk ↑y
hU : (Sheafify.isLocallyGerm F).pred fU
fV : (y : ↥↑V) → F.stalk ↑y
hV : (Sheafify.isLocallyGerm F).pred fV
U' : Opens ↑X
mU : ↑⟨x, ⋯⟩ ∈ U'
iU : U' ⟶ ↑U
gU : F.obj (op U')
wU : ∀ (x_1 : ↥U'), (fun x_2 ↦ fU (iU x_2)) x_1 = (ConcreteCategory.hom (F.germ U' ↑x_1 ⋯)) gU
V' : Opens ↑X
mV : ↑⟨x, ⋯⟩ ∈ V'
iV : V' ⟶ ↑V
gV : F.obj (op V')
e : (ConcreteCategory.hom (F.germ U' x ⋯)) gU = (ConcreteCategory.hom (F.germ V' x ⋯)) gV
wV : ∀ (x_1 : ↥V'), (fun x_2 ↦ fV (iV x_2)) x_1 = (ConcreteCategory.hom (F.germ V' ↑x_1 ⋯)) gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : (ConcreteCategory.hom (F.map iU'.op)) gU = (ConcreteCategory.hom (F.map iV'.op)) gV
⊢ ∀ (w : ↥↑⟨W ⊓ (U' ⊓ V'), ⋯⟩),
    fU ((id (W.infLERight (U' ⊓ V') ≫ U'.infLELeft V' ≫ iU)) w) =
      fV ((id (W.infLERight (U' ⊓ V') ≫ U'.infLERight V' ≫ iV)) w)

Tactic:
intro w

Goal state after:
case h.refine_3
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : ↥↑U) → F.stalk ↑y
hU : (Sheafify.isLocallyGerm F).pred fU
fV : (y : ↥↑V) → F.stalk ↑y
hV : (Sheafify.isLocallyGerm F).pred fV
U' : Opens ↑X
mU : ↑⟨x, ⋯⟩ ∈ U'
iU : U' ⟶ ↑U
gU : F.obj (op U')
wU : ∀ (x_1 : ↥U'), (fun x_2 ↦ fU (iU x_2)) x_1 = (ConcreteCategory.hom (F.germ U' ↑x_1 ⋯)) gU
V' : Opens ↑X
mV : ↑⟨x, ⋯⟩ ∈ V'
iV : V' ⟶ ↑V
gV : F.obj (op V')
e : (ConcreteCategory.hom (F.germ U' x ⋯)) gU = (ConcreteCategory.hom (F.germ V' x ⋯)) gV
wV : ∀ (x_1 : ↥V'), (fun x_2 ↦ fV (iV x_2)) x_1 = (ConcreteCategory.hom (F.germ V' ↑x_1 ⋯)) gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : (ConcreteCategory.hom (F.map iU'.op)) gU = (ConcreteCategory.hom (F.map iV'.op)) gV
w : ↥↑⟨W ⊓ (U' ⊓ V'), ⋯⟩
⊢ fU ((id (W.infLERight (U' ⊓ V') ≫ U'.infLELeft V' ≫ iU)) w) =
    fV ((id (W.infLERight (U' ⊓ V') ≫ U'.infLERight V' ≫ iV)) w)
Module: Mathlib.Topology.Sion

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
inst✝² : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
b : β
y y' : ↑Y
z : ↑(segment ℝ ↑y ↑y')
x : ↑X
hx : x ∈ sublevelLeft X f b ↑z
⊢ x ∈ sublevelLeft X f b ↑y ∪ sublevelLeft X f b ↑y'

Tactic:
by
    simp only [Set.mem_union, mem_sublevelLeft_iff, ← inf_le_iff]
    specialize hfx' x x.2 (f x y ⊓ f x y')
    rw [convex_iff_segment_subset] at hfx'
    specialize hfx' ⟨y.prop, inf_le_left⟩ ⟨y'.prop, inf_le_right⟩ z.prop
    exact le_trans hfx'.2 hx

Goal state after:
Module: Mathlib.Topology.SmallInductiveDimension

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (Set X)
hs : IsTopologicalBasis s
h : ∀ U ∈ s, HasSmallInductiveDimensionLT (↑(frontier U)) 0
U : Set X
hU : U ∈ s
⊢ IsClosed[inst✝] U

Tactic:
rw [← closure_subset_iff_isClosed]

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (Set X)
hs : IsTopologicalBasis s
h : ∀ U ∈ s, HasSmallInductiveDimensionLT (↑(frontier U)) 0
U : Set X
hU : U ∈ s
⊢ closure[inst✝] U ⊆ U
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: 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 = ∅}
this : 𝒮 = ∅
⊢ ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty

Tactic:
contrapose! this

Goal state after:
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 = ∅}
this : ∃ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅
⊢ 𝒮.Nonempty
Module: Mathlib.Topology.Sion

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
inst✝⁸ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝² : TopologicalSpace F
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
a : E
b b' : β
y y' : ↑Y
ha : ∀ x ∈ X, max (f a ↑y) (f a ↑y') ≤ max (f x ↑y) (f x ↑y')
hb : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
hb' : b' < max (f a ↑y) (f a ↑y')
hbb' : b < b'
J : Set ↑(segment ℝ ↑y ↑y') := setOfPred_sublevelLeft_subset X Y f b b' y y'
z : ↑(segment ℝ ↑y ↑y')
hz : ClusterPt z (𝓟 J)
x : ↑X
hx : x ∈ sublevelLeft X f b ↑z
z' : ↑(segment ℝ ↑y ↑y')
hz' : z' ∈ setOfPred_sublevelLeft_subset X Y f b b' y y'
hxz' : x ∈ sublevelLeft X f b' ↑z'
hz'2 : sublevelLeft X f b' ↑z' ⊆ sublevelLeft X f b' ↑y'
hz'Y : ↑z' ∈ Y
⊢ False

Tactic:
apply (nonempty_sublevelLeft ne_X kX hfy ⟨z', hz'Y⟩ hb).not_subset_empty

Goal state after:
E : Type u_1
F : Type u_2
β : Type u_3
inst✝⁸ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝² : TopologicalSpace F
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
a : E
b b' : β
y y' : ↑Y
ha : ∀ x ∈ X, max (f a ↑y) (f a ↑y') ≤ max (f x ↑y) (f x ↑y')
hb : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
hb' : b' < max (f a ↑y) (f a ↑y')
hbb' : b < b'
J : Set ↑(segment ℝ ↑y ↑y') := ⋯
z : ↑(segment ℝ ↑y ↑y')
hz : ClusterPt z (𝓟 J)
x : ↑X
hx : x ∈ sublevelLeft X f b ↑z
z' : ↑(segment ℝ ↑y ↑y')
hz' : z' ∈ setOfPred_sublevelLeft_subset X Y f b b' y y'
hxz' : x ∈ sublevelLeft X f b' ↑z'
hz'2 : sublevelLeft X f b' ↑z' ⊆ sublevelLeft X f b' ↑y'
hz'Y : ↑z' ∈ Y
⊢ sublevelLeft X f b ↑⟨↑z', hz'Y⟩ ⊆ ∅
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X✝ : ℕ → Type
inst✝² : (n : ℕ) → MetricSpace (X✝ n)
inst✝¹ : ∀ (n : ℕ), CompactSpace (X✝ n)
inst✝ : ∀ (n : ℕ), Nonempty (X✝ n)
d : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
this : ∀ (n : ℕ), 0 < d n
u : ℕ → GHSpace
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < d N
X : ℕ → Type := fun n ↦ (u n).Rep
Y : (n : ℕ) → AuxGluingStruct (X n) := auxGluing X
⊢ ∃ x, Tendsto u atTop (𝓝 x)

Tactic:
have E :
    ∀ n : ℕ,
      GlueSpace (Y n).isom (isometry_optimalGHInjl (X n) (X (n + 1))) = (Y (n + 1)).Space :=
    fun n => by dsimp only [Y, auxGluing]

Goal state after:
X✝ : ℕ → Type
inst✝² : (n : ℕ) → MetricSpace (X✝ n)
inst✝¹ : ∀ (n : ℕ), CompactSpace (X✝ n)
inst✝ : ∀ (n : ℕ), Nonempty (X✝ n)
d : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
this : ∀ (n : ℕ), 0 < d n
u : ℕ → GHSpace
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < d N
X : ℕ → Type := fun n ↦ (u n).Rep
Y : (n : ℕ) → AuxGluingStruct (X n) := auxGluing X
E : ∀ (n : ℕ), GlueSpace ⋯ ⋯ = (Y (n + 1)).Space
⊢ ∃ x, Tendsto u atTop (𝓝 x)
Module: Mathlib.Topology.Subpath

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ↑I
⊢ (γ.subpath t₀ t₁).symm = γ.subpath t₁ t₀

Tactic:
ext s

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ s : ↑I
⊢ (γ.subpath t₀ t₁).symm s = (γ.subpath t₁ t₀) s
Module: Mathlib.Topology.Subpath

Goal state before:
pp: case right
t₀ t₁ : ↑I
t : ↑(Icc 0 1)
ht : ↑t ∈ (fun θ ↦ (1 - θ) • ↑t₀ + θ • ↑t₁) '' Icc 0 1
⊢ ∃ a, Icc.convexComb t₀ t₁ a = t

Tactic:
obtain ⟨s, hs, hst⟩ := ht

Goal state after:
case right
t₀ t₁ : ↑I
t : ↑(Icc 0 1)
s : ℝ
hs : s ∈ Icc 0 1
hst : (fun θ ↦ (1 - θ) • ↑t₀ + θ • ↑t₁) s = ↑t
⊢ ∃ a, Icc.convexComb t₀ t₁ a = t
Module: Mathlib.Topology.Subpath

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ↑I
⊢ γ.subpath t t = refl (γ t)

Tactic:
ext s

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t s : ↑I
⊢ (γ.subpath t t) s = (refl (γ t)) s
Module: Mathlib.Topology.Subpath

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
⊢ γ.subpath 0 1 = γ.cast ⋯ ⋯

Tactic:
ext s

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
s : ↑I
⊢ (γ.subpath 0 1) s = (γ.cast ⋯ ⋯) s
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := ⋯
𝒮 : Set (Set (Set X)) := ⋯
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun x ↦ x ∈ 𝒮) B
B' : Set (Set X) := ⋯
Z : Set X := ⋯
hZ_closed : IsClosed[inst✝⁴] Z
hZ_nonempty : Z.Nonempty
hZ_irred : ¬IsPreirreducible Z
Y₁ Y₂ : Set X
hY₁_cl : IsClosed[inst✝⁴] Y₁
hY₂_cl : IsClosed[inst✝⁴] Y₂
hc₁ : IsCompact Y₁ᶜ
hc₂ : IsCompact Y₂ᶜ
hsub : Z ⊆ Y₁ ∪ Y₂
x₁ : X
hx₁ : x₁ ∈ Z ∩ Y₁ᶜ
x₂ : X
hx₂ : x₂ ∈ Z ∩ Y₂ᶜ
hY₁ : Y₁ ∈ 𝔅
hY₂ : Y₂ ∈ 𝔅
hY₁_inter_B : Y₁ ∩ ⋂₀ B = ∅
hY₂_inter_B : Y₂ ∩ ⋂₀ B = ∅
A₁ : Set (Set X)
hA₁ : A₁ ⊆ insert Y₁ B
hA₁' : A₁.Finite
hA₁'' : ⋂₀ A₁ = ∅
A₂ : Set (Set X)
hA₂ : A₂ ⊆ insert Y₂ B
hA₂' : A₂.Finite
hA₂'' : ⋂₀ A₂ = ∅
this : ¬(Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂})).Nonempty
⊢ A₁ \ {Y₁} ∪ A₂ \ {Y₂} ⊆ constructibleTopologySubbasis X

Tactic:
grind [hB.prop, Set.union_subset_iff]

Goal state after:
Module: Mathlib.Topology.UniformSpace.CompareReals

Goal state before:
pp: ⊢ AbsoluteValue.abs.uniformSpace = PseudoMetricSpace.toUniformSpace

Tactic:
ext s

Goal state after:
s : Set (ℚ × ℚ)
⊢ s ∈ uniformity ℚ ↔ s ∈ uniformity ℚ
Module: Mathlib.Topology.UniformSpace.OfCompactT2

Goal state before:
pp: case a
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x i : γ
hi : Inseparable x i
| comap (fun x_1 ↦ x) (𝓝 x) ⊓ 𝓝 x

Tactic:
comap_const_of_mem fun V => mem_of_mem_nhds

Goal state after:
case a
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x i : γ
hi : Inseparable x i
| ⊤ ⊓ 𝓝 x