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

Goal state before:
pp: case refine_3
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
F : OptimalGHCoupling X Y → ↥(lp (fun x ↦ ℝ) ∞) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun x ↦ ℝ) ∞) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun x ↦ ℝ) ∞) := F ∘ optimalGHInjr X Y
⊢ ghDist X Y = hausdorffDist (range Φ) (range Ψ)

Tactic:
· rw [← image_univ, ← image_univ, image_comp F, image_univ, image_comp F (optimalGHInjr X Y),
      image_univ, ← hausdorffDist_optimal]
    exact (hausdorffDist_image (kuratowskiEmbedding.isometry _)).symm

Goal state after:
Module: Mathlib.Topology.Sets.BaseChangeNhds

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x✝ : ↑⊥.openNhds
⊢ ⊥ ≤ x✝

Tactic:
by tauto

Goal state after:
Module: Mathlib.Topology.Sets.BaseChangeNhds

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x✝¹ : ↑⊥.openNhds
x✝ : ⊥ ⟶ x✝¹
⊢ ∀ {Z : ↑⊥.openNhds} (h : Z ⟶ ⊥), h ≫ x✝ = h ≫ homOfLE ⋯

Tactic:
by tauto

Goal state after:
Module: Mathlib.Topology.Separation.PerfectlyNormal

Goal state before:
pp: 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 : ℕ → C(X, ℝ)
hfs : ∀ (n : ℕ), EqOn (⇑(f n)) 0 s
hfu : ∀ (n : ℕ), EqOn (⇑(f n)) 1 (U n)ᶜ
hfr : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1
⊢ ∃ f, s = ⇑f ⁻¹' {0} ∧ ∀ (x : X), f x ∈ Icc 0 1

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]

Goal state after:
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 : ℕ → C(X, ℝ)
hfs : ∀ (n : ℕ), EqOn (⇑(f n)) 0 s
hfu : ∀ (n : ℕ), EqOn (⇑(f n)) 1 (U n)ᶜ
hfr : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1
hsb : ∀ (x : X) (n : ℕ), ‖(f n) x * (1 / 2 / 2 ^ n)‖ ≤ 1 / 2 / 2 ^ n
⊢ ∃ f, s = ⇑f ⁻¹' {0} ∧ ∀ (x : X), f x ∈ Icc 0 1
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.{w, v} C
inst✝ : HasTerminal C
A : C
hd : (U : Opens ↑(of PUnit.{u + 1})) → Decidable (PUnit.unit ∈ U)
⊢ skyscraperPresheaf p₀ A =
    (Presheaf.pushforward C (ofHom (ContinuousMap.const (↑(of PUnit.{u + 1})) p₀))).obj
      (skyscraperPresheaf PUnit.unit A)

Tactic:
by
  convert_to @skyscraperPresheaf X p₀ (fun U => hd <| (Opens.map <| ofHom <|
      ContinuousMap.const _ p₀).obj U)
    C _ _ A = _ <;> congr

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x : q.Rep
this : x ∈ ⋃ y ∈ s q, ball y ε
y : q.Rep
ys : y ∈ s q
hy : x ∈ ball y ε
i : ℕ := ↑((E q) ⟨y, ys⟩)
hi : ↑((E q) ⟨y, ys⟩) < Nat.card ↑(s q) := Fin.is_lt ((E q) ⟨y, ys⟩)
⊢ ⟨i, hi⟩ = (E q) ⟨y, ys⟩

Tactic:
rw [Fin.ext_iff, Fin.val_mk]

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
j' : j = ↑((E q) (Ψ y))
this✝¹ : (F p).snd ((E p) x) ((E p) y) = ⌊ε⁻¹ * dist x y⌋
Ap : (F p).snd ⟨i, hip⟩ ⟨j, hjp⟩ = ⌊ε⁻¹ * dist x y⌋
this✝ : (F q).snd ((E q) (Ψ x)) ((E q) (Ψ y)) = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
Aq : (F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
this : ⌊ε⁻¹ * dist x y⌋ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
I : ε⁻¹ * |dist x y - dist (Ψ x) (Ψ y)| ≤ 1
⊢ ε * (ε⁻¹ * |dist x y - dist (Ψ x) (Ψ y)|) ≤ ε * 1

Tactic:
gcongr

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x : q.Rep
this : x ∈ ⋃ y ∈ s q, ball y (u n)
y : q.Rep
ys : y ∈ s q
hy : x ∈ ball y (u n)
i : ℕ := ↑((E q) ⟨y, ys⟩)
hi : ↑((E q) ⟨y, ys⟩) < N q := ((E q) ⟨y, ys⟩).isLt
⊢ ⟨i, hi⟩ = (E q) ⟨y, ys⟩

Tactic:
rw [Fin.ext_iff, Fin.val_mk]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
Y Z : WalkingParallelPair
f : Y ⟶ Z
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map f ≫
      WalkingParallelPair.casesOn Z (Pi.lift fun i ↦ c.π.app (op (single i)))
        (Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) =
    WalkingParallelPair.casesOn Y (Pi.lift fun i ↦ c.π.app (op (single i)))
        (Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map f

Tactic:
cases Y

Goal state after:
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
Z : WalkingParallelPair
f : WalkingParallelPair.zero ⟶ Z
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map f ≫
      WalkingParallelPair.casesOn Z (Pi.lift fun i ↦ c.π.app (op (single i)))
        (Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) =
    WalkingParallelPair.casesOn WalkingParallelPair.zero (Pi.lift fun i ↦ c.π.app (op (single i)))
        (Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map f

case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
Z : WalkingParallelPair
f : WalkingParallelPair.one ⟶ Z
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map f ≫
      WalkingParallelPair.casesOn Z (Pi.lift fun i ↦ c.π.app (op (single i)))
        (Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) =
    WalkingParallelPair.casesOn WalkingParallelPair.one (Pi.lift fun i ↦ c.π.app (op (single i)))
        (Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map f
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
inst✝³ : CompactSpace X
inst✝² : CompactSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
x : X
A : ⨅ y, (candidatesBDist X Y) (inl x, inr y) ≤ (candidatesBDist X Y) (inl x, inr default)
⊢ dist x default + 1 + dist default default ≤ diam univ + 1 + diam univ

Tactic:
gcongr

Goal state after:
case h₁
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
inst✝³ : CompactSpace X
inst✝² : CompactSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
x : X
A : ⨅ y, (candidatesBDist X Y) (inl x, inr y) ≤ (candidatesBDist X Y) (inl x, inr default)
⊢ dist x default ≤ diam univ

case h₂
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
inst✝³ : CompactSpace X
inst✝² : CompactSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
x : X
A : ⨅ y, (candidatesBDist X Y) (inl x, inr y) ≤ (candidatesBDist X Y) (inl x, inr default)
⊢ dist default default ≤ diam univ
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
inst✝³ : CompactSpace X
inst✝² : CompactSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
y : Y
A : ⨅ x, (candidatesBDist X Y) (inl x, inr y) ≤ (candidatesBDist X Y) (inl default, inr y)
⊢ dist default default + 1 + dist default y ≤ diam univ + 1 + diam univ

Tactic:
gcongr

Goal state after:
case h₁
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
inst✝³ : CompactSpace X
inst✝² : CompactSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
y : Y
A : ⨅ x, (candidatesBDist X Y) (inl x, inr y) ≤ (candidatesBDist X Y) (inl default, inr y)
⊢ dist default default ≤ diam univ

case h₂
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
inst✝³ : CompactSpace X
inst✝² : CompactSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
y : Y
A : ⨅ x, (candidatesBDist X Y) (inl x, inr y) ≤ (candidatesBDist X Y) (inl default, inr y)
⊢ dist default y ≤ diam univ
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
b : β
y y' : ↑Y
z : ↑(segment ℝ ↑y ↑y')
x : ↑X
hfx' : Convex ℝ {x_1 | x_1 ∈ Y ∧ min (f ↑x ↑y) (f ↑x ↑y') ≤ (fun y ↦ f (↑x) y) x_1}
hx : x ∈ sublevelLeft X f b ↑z
⊢ min (f ↑x ↑y) (f ↑x ↑y') ≤ b

Tactic:
convex_iff_segment_subset

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✝¹ : AddCommGroup F
inst✝ : Module ℝ F
b : β
y y' : ↑Y
z : ↑(segment ℝ ↑y ↑y')
x : ↑X
hfx' :
  ∀ ⦃x_1 : F⦄,
    x_1 ∈ {x_2 | x_2 ∈ Y ∧ min (f ↑x ↑y) (f ↑x ↑y') ≤ (fun y ↦ f (↑x) y) x_2} →
      ∀ ⦃y_1 : F⦄,
        y_1 ∈ {x_2 | x_2 ∈ Y ∧ min (f ↑x ↑y) (f ↑x ↑y') ≤ (fun y ↦ f (↑x) y) x_2} →
          segment ℝ x_1 y_1 ⊆ {x_2 | x_2 ∈ Y ∧ min (f ↑x ↑y) (f ↑x ↑y') ≤ (fun y ↦ f (↑x) y) x_2}
hx : x ∈ sublevelLeft X f b ↑z
⊢ min (f ↑x ↑y) (f ↑x ↑y') ≤ b
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'
⊢ IsClosed J

Tactic:
rw [isClosed_iff_clusterPt]

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') := setOfPred_sublevelLeft_subset X Y f b b' y y'
⊢ ∀ (a : ↑(segment ℝ ↑y ↑y')), ClusterPt a (𝓟 J) → a ∈ J
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: case refine_1
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : QuasiSeparatedSpace X
s : Set (Set X)
hs : s ⊆ constructibleTopologySubbasis X
hf : s.Finite
t : Set X
ht : t ∈ s
⊢ IsOpen[inst✝²] t ∨ IsClosed[inst✝²] t

pp: case refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : QuasiSeparatedSpace X
s : Set (Set X)
hs : s ⊆ constructibleTopologySubbasis X
hf : s.Finite
t : Set X
ht : t ∈ s
⊢ IsCompact t

Tactic:
· apply (hs ht).imp <;> grind

Goal state after:
case refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : QuasiSeparatedSpace X
s : Set (Set X)
hs : s ⊆ constructibleTopologySubbasis X
hf : s.Finite
t : Set X
ht : t ∈ s
⊢ IsCompact t
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
hη : IsGenericPoint hZ_irred.genericPoint Z
i : Set X
hi : i ∈ B
hiB' : i ∉ B'
hi_cmpt : IsCompact i
a : Set (Set X)
ha : a ⊆ B'
hfa : a.Finite
⊢ (i ∩ ⋂₀ a).Nonempty

Tactic:
rw [← Set.sInter_insert]

Goal state after:
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
hη : IsGenericPoint hZ_irred.genericPoint Z
i : Set X
hi : i ∈ B
hiB' : i ∉ B'
hi_cmpt : IsCompact i
a : Set (Set X)
ha : a ⊆ B'
hfa : a.Finite
⊢ (⋂₀ insert i a).Nonempty
Module: Mathlib.Topology.UniformSpace.Ultra.Completion

Goal state before:
pp: case h_trans
X : Type u_1
Y : Type u_2
inst✝² : UniformSpace X
inst✝¹ : UniformSpace Y
inst✝ : IsUltraUniformity X
this :
  (𝓤 (SeparationQuotient X)).HasBasis (fun s ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun i ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
⊢ ∀ (i : SetRel X X),
    i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans → SetRel.IsTrans (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i)

Tactic:
rintro U ⟨hU', _, hU⟩
    constructor
    rintro x y z
    simp only [id_eq, Set.mem_image, Prod.exists, Prod.map_apply, Prod.mk.injEq,
      forall_exists_index, and_imp]
    rintro a b hab rfl rfl c d hcd hc rfl
    have hbc : (b, c) ∈ U := by
      rw [eq_comm, SeparationQuotient.mk_eq_mk, inseparable_iff_ker_uniformity,
          Filter.mem_ker] at hc
      exact hc _ hU'
    exact ⟨a, d, U.trans (U.trans hab hbc) hcd, by simp, by simp⟩

Goal state after: