mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ IsTerminal (if PUnit.unit ∈ ⊥ then A else ⊤_ C)

Tactic:
if_neg

Goal state after:
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
⊢ IsTerminal (⊤_ C)

case hnc
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
⊢ PUnit.unit ∉ ⊥
Module: Mathlib.Topology.Sheaves.Abelian

Goal state before:
pp: X : TopCat
p₀ : ↑X
C : Type v
inst✝² : Category.{u, v} C
inst✝¹ : Abelian C
inst✝ : HasColimits C
⊢ ∀ {X_1 Y : (Opens ↑X)ᵒᵖ ⥤ C} {f g : X_1 ⟶ Y},
    ((Functor.whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion p₀).op).map (f + g) =
      ((Functor.whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion p₀).op).map f +
        ((Functor.whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion p₀).op).map g

Tactic:
by cat_disch

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

Goal state before:
pp: case pos
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 𝓖 : Presheaf C X
f : 𝓕 ⟶ 𝓖
U : Opens ↑X
h : p₀ ∈ U
⊢ f.app (op U) ≫ 𝓖.germ U p₀ h ≫ 𝟙 (𝓖.stalk p₀) ≫ eqToHom ⋯ =
    (𝓕.germ U p₀ h ≫ 𝟙 (𝓕.stalk p₀) ≫ eqToHom ⋯) ≫ eqToHom ⋯ ≫ (Presheaf.stalkFunctor C p₀).map f ≫ eqToHom ⋯

pp: case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 𝓖 : Presheaf C X
f : 𝓕 ⟶ 𝓖
U : Opens ↑X
h : p₀ ∉ U
⊢ f.app (op U) ≫ (⋯ ▸ terminalIsTerminal).from (𝓖.obj (op U)) =
    (⋯ ▸ terminalIsTerminal).from (𝓕.obj (op U)) ≫ (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ U then 𝓕.stalk p₀ else ⊤_ C)

Tactic:
· simp only [Category.id_comp, Category.assoc, eqToHom_trans_assoc, eqToHom_refl,
        Presheaf.stalkFunctor_map_germ_assoc, Presheaf.stalkFunctor_obj]

Goal state after:
case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 𝓖 : Presheaf C X
f : 𝓕 ⟶ 𝓖
U : Opens ↑X
h : p₀ ∉ U
⊢ f.app (op U) ≫ (⋯ ▸ terminalIsTerminal).from (𝓖.obj (op U)) =
    (⋯ ▸ terminalIsTerminal).from (𝓕.obj (op U)) ≫ (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ U then 𝓕.stalk p₀ else ⊤_ C)
Module: Mathlib.Topology.Sheaves.Alexandrov

Goal state before:
pp: X✝ : Type v
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : Preorder X✝
inst✝⁴ : Topology.IsUpperSet X✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
F✝ : X✝ ⥤ C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
α : Type v
Us : α → Opens ↑X
S : Cone ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F)
m : S.pt ⟶ ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).pt
hm✝ :
  ∀ (j : (ObjectProperty.FullSubcategory fun V ↦ ∃ i, V ≤ Us i)ᵒᵖ),
    m ≫ ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).π.app j = S.π.app j
left✝ : Discrete PUnit.{1}
x : ↑X
f : (fromPUnit (Opposite.op (iSup Us))).obj left✝ ⟶ (principals ↑X).obj x
hm :
  m ≫
      ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).π.app
        (Opposite.op { obj := principalOpen x, property := ⋯ }) =
    S.π.app (Opposite.op { obj := principalOpen x, property := ⋯ })
⊢ S.π.app
        (Opposite.op
          { obj := principalOpen (StructuredArrow.right { left := left✝, right := x, hom := f }), property := ⋯ }) ≫
      limit.π (generator (principalOpen (StructuredArrow.right { left := left✝, right := x, hom := f })) ⋙ F)
        { left := { as := PUnit.unit }, right := StructuredArrow.right { left := left✝, right := x, hom := f },
          hom := 𝟙 (Opposite.op (principalOpen (StructuredArrow.right { left := left✝, right := x, hom := f }))) } =
    m ≫ limit.π (generator (iSup Us) ⋙ F) { left := left✝, right := x, hom := f }

Tactic:
· rw [← hm]
      simp only [Category.assoc]
      congr
      apply limit.lift_π

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

Goal state before:
pp: X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := fun x ↦ unop (StructuredArrow.right ↑x).fst
t : ToType (F.obj.obj (op (iSup f)))
ht : IsGluing F.obj f (fun x ↦ (StructuredArrow.right ↑x).snd) t
right✝ :
  ∀ (y : ToType (F.obj.obj (op (iSup f)))),
    (fun s_1 ↦ IsGluing F.obj f (fun x ↦ (StructuredArrow.right ↑x).snd) s_1) y → y = t
le₁ : iSup f ≤ U
le₂ : ∀ i ∈ c, unop (StructuredArrow.right i).fst ≤ iSup f
i : Under g s
hi : i ∈ c
⊢ (StructuredArrow.mk
          (CategoryOfElements.homMk ⟨op U, s⟩
            ((NatTrans.mapElements (Functor.whiskerRight g.hom (CategoryTheory.forget AddCommGrpCat))).obj
              ⟨op (iSup f), t⟩)
            (homOfLE le₁).op ⋯)).hom ≫
      (NatTrans.mapElements (Functor.whiskerRight g.hom (CategoryTheory.forget AddCommGrpCat))).map
        (CategoryOfElements.homMk
          (StructuredArrow.mk
              (CategoryOfElements.homMk ⟨op U, s⟩
                ((NatTrans.mapElements (Functor.whiskerRight g.hom (CategoryTheory.forget AddCommGrpCat))).obj
                  ⟨op (iSup f), t⟩)
                (homOfLE le₁).op ⋯)).right
          (StructuredArrow.right i) (homOfLE ⋯).op ⋯) =
    StructuredArrow.hom i

Tactic:
by cat_disch

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

Goal state before:
pp: X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : OpenNhds x
⊢ ∀ (V : OpenNhds x) (fU : (y : ↥↑U) → F.stalk ↑y),
    (Sheafify.isLocallyGerm F).pred fU →
      ∀ (fV : (y : ↥↑V) → F.stalk ↑y),
        (Sheafify.isLocallyGerm F).pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)

Tactic:
V

Goal state after:
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
⊢ ∀ (fU : (y : ↥↑U) → F.stalk ↑y),
    (Sheafify.isLocallyGerm F).pred fU →
      ∀ (fV : (y : ↥↑V) → F.stalk ↑y),
        (Sheafify.isLocallyGerm F).pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
Module: Mathlib.Topology.Sheaves.Sheafify

Goal state before:
pp: 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
e : fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩
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')
wV : ∀ (x_1 : ↥V'), (fun x_2 ↦ fV (iV x_2)) x_1 = (ConcreteCategory.hom (F.germ V' ↑x_1 ⋯)) gV
wUx : (fun x_1 ↦ fU (iU x_1)) ⟨x, mU⟩ = (ConcreteCategory.hom (F.germ U' ↑⟨x, mU⟩ ⋯)) gU
⊢ ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)

Tactic:
dsimp at wUx

Goal state after:
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
e : fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩
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')
wV : ∀ (x_1 : ↥V'), (fun x_2 ↦ fV (iV x_2)) x_1 = (ConcreteCategory.hom (F.germ V' ↑x_1 ⋯)) gV
wUx : fU ⟨x, ⋯⟩ = (ConcreteCategory.hom (F.germ U' x ⋯)) gU
⊢ ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
Module: Mathlib.Topology.Sheaves.Flasque

Goal state before:
pp: X : TopCat
U : Opens ↑X
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst✝ : S.X₁.IsFlasque
s : ↑(S.X₃.obj.obj (op U))
t : Under S.g s
ht : ∀ (a : Under S.g s), Nonempty (a ⟶ t) → Nonempty (t ⟶ a)
tle : unop (StructuredArrow.right t).fst ≤ U
tcomp :
  (s |_ unop (StructuredArrow.right t).fst) tle =
    (ConcreteCategory.hom (S.g.hom.app (StructuredArrow.right t).fst)) (StructuredArrow.right t).snd
x : ↑X
hx : x ∈ U
this✝¹ : Presheaf.IsLocallySurjective S.g.hom
W : Opens ↑X
Wle : W ≤ U
hW : x ∈ W
t₁ : ↑(S.X₂.obj.obj (op W))
ht₁ : (ConcreteCategory.hom (S.g.hom.app (op W))) t₁ = (s |_ W) Wle
t₂ : ToType (S.X₂.obj.obj (op (unop (StructuredArrow.right t).fst ⊓ W))) :=
  ((StructuredArrow.right t).snd |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯ -
    (t₁ |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯
this✝ : (ConcreteCategory.hom (S.g.hom.app (op (unop (StructuredArrow.right t).fst ⊓ W)))) t₂ = 0
t₃ : ↑(S.X₁.obj.obj (op (unop (StructuredArrow.right t).fst ⊓ W)))
ht₃ : (ConcreteCategory.hom (S.f.hom.app (op (unop (StructuredArrow.right t).fst ⊓ W)))) t₃ = t₂
t₄ : ↑(S.X₁.obj.obj (op W))
ht₄ : (t₄ |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯ = t₃
f : Fin 2 → Opens ↑X := ![unop (StructuredArrow.right t).fst, W]
sf : (i : Fin 2) → ↑(S.X₂.obj.obj (op (f i))) :=
  fun x ↦
    match x with
    | 0 => (StructuredArrow.right t).snd
    | 1 => t₁ + (ConcreteCategory.hom (S.f.hom.app (op W))) t₄
this : (sf 0 |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯ = (sf 1 |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯
t₅ : ToType (S.X₂.obj.obj (op (iSup f)))
ht₅ : IsGluing S.X₂.obj f sf t₅
right✝ : ∀ (y : ToType (S.X₂.obj.obj (op (iSup f)))), (fun t₅ ↦ IsGluing S.X₂.obj f sf t₅) y → y = t₅
le : iSup f ≤ U
t₆ : Under S.g s :=
  StructuredArrow.mk
    (CategoryOfElements.homMk ⟨op U, s⟩
      ((NatTrans.mapElements (Functor.whiskerRight S.g.hom (CategoryTheory.forget AddCommGrpCat))).obj
        ⟨op (iSup f), t₅⟩)
      (homOfLE le).op ⋯)
⊢ StructuredArrow.hom t₆ ≫
      (NatTrans.mapElements (Functor.whiskerRight S.g.hom (CategoryTheory.forget AddCommGrpCat))).map
        (CategoryOfElements.homMk (StructuredArrow.right t₆) (StructuredArrow.right t) (homOfLE ⋯).op ⋯) =
    StructuredArrow.hom t

Tactic:
by cat_disch

Goal state after:
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✝⁴ : IsTopologicalAddGroup E
inst✝³ : Module ℝ E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
cY : Convex ℝ Y
a : E
b : β
y y' : ↑Y
ha : ∀ x ∈ X, max (f a ↑y) (f a ↑y') ≤ max (f x ↑y) (f x ↑y')
hb : b < max (f a ↑y) (f a ↑y')
z : ↑(segment ℝ ↑y ↑y')
⊢ sublevelLeft X f b ↑z ⊆ sublevelLeft X f b ↑y ∨ sublevelLeft X f b ↑z ⊆ sublevelLeft X f b ↑y'

Tactic:
apply isPreconnected_iff_subset_of_disjoint_closed.mp
    (isPreconnected_sublevelLeft hfy' b ⟨z, cY.segment_subset y.prop y'.prop z.prop⟩)
    _ _ (isClosed_sublevelLeft hfy b y) (isClosed_sublevelLeft hfy b y')
    (sublevelLeft_subset_union hfx' b y y' z)
  simp [(disjoint_sublevelLeft ha hb).inter_eq]

Goal state after:
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, 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 : ∃ᶠ (x : F) in nhdsWithin (↑z) Y, ∃ (h : x ∈ segment ℝ ↑y ↑y'), ⟨x, h⟩ ∈ J
x : ↑X
hx : x ∈ sublevelLeft X f b ↑z
hfx : ∀ᶠ (x' : F) in nhdsWithin (↑z) Y, f (↑x) x' < b'
⊢ ∃ z' ∈ setOfPred_sublevelLeft_subset X Y f b b' y y', x ∈ sublevelLeft X f b' ↑z'

Tactic:
suffices ∀ᶠ z' : F in nhdsWithin z Y,
    (∃ hz' : z' ∈ segment ℝ y.val y'.val,
      (⟨z', hz'⟩ : segment ℝ y.val y'.val) ∈ setOfPred_sublevelLeft_subset X Y f b b' y y') →
      ∃ hz' : z' ∈ segment ℝ y.val y'.val, x ∈ sublevelLeft X f b' z'
        ∧ (⟨z', hz'⟩ : segment ℝ y.val y'.val) ∈ setOfPred_sublevelLeft_subset X Y f b b' y y' by
    obtain ⟨z', hz', hxz'1, hxz'2⟩ := hz.mp this |>.exists
    exact ⟨⟨z', hz'⟩, ⟨hxz'2, hxz'1⟩⟩

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, 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 : ∃ᶠ (x : F) in nhdsWithin (↑z) Y, ∃ (h : x ∈ segment ℝ ↑y ↑y'), ⟨x, h⟩ ∈ J
x : ↑X
hx : x ∈ sublevelLeft X f b ↑z
hfx : ∀ᶠ (x' : F) in nhdsWithin (↑z) Y, f (↑x) x' < b'
⊢ ∀ᶠ (z' : F) in nhdsWithin (↑z) Y,
    (∃ (hz' : z' ∈ segment ℝ ↑y ↑y'), ⟨z', hz'⟩ ∈ setOfPred_sublevelLeft_subset X Y f b b' y y') →
      ∃ (hz' : z' ∈ segment ℝ ↑y ↑y'),
        x ∈ sublevelLeft X f b' z' ∧ ⟨z', hz'⟩ ∈ setOfPred_sublevelLeft_subset X Y f b b' y y'
Module: Mathlib.Topology.Subpath

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
p : Fin 3 → X
F : (k : Fin 2) → Path (p k.castSucc) (p k.succ)
⊢ (concat p F).Homotopic ((F 0).trans (F 1))

Tactic:
by
  simpa [concat_succ] using hcomp ⟨Homotopy.reflTrans _⟩ (refl _)

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : UniformSpace X
inst✝¹ : UniformSpace Y
inst✝ : IsUltraUniformity X
⊢ IsUltraUniformity (SeparationQuotient X)

Tactic:
have := IsUltraUniformity.hasBasis.map
    (Prod.map SeparationQuotient.mk (SeparationQuotient.mk (X := X)))

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : UniformSpace X
inst✝¹ : UniformSpace Y
inst✝ : IsUltraUniformity X
this :
  (map (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (𝓤 X)).HasBasis (fun s ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans)
    fun i ↦ Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
⊢ IsUltraUniformity (SeparationQuotient X)
Module: Mathlib.Topology.Sion

Goal state before:
pp: case insert.inr
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
Y : Set F
f : E → F → β
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
cY : Convex ℝ Y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
s✝ : Set F
t : β
b : F
s : Set F
a✝ : b ∉ s
hs : s.Finite
hrec :
  ∀ {X : Set E},
    X.Nonempty →
      IsCompact X →
        (∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X) →
          (∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y) →
            (∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y) →
              (∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y) →
                Convex ℝ X → s ⊆ Y → (∀ x ∈ X, ∃ y ∈ s, t < f x y) → ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
X : Set 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
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
cX : Convex ℝ X
hsY : insert b s ⊆ Y
ht : ∀ x ∈ X, ∃ y ∈ insert b s, t < f x y
hb : b ∈ Y
X' : Set E := X ∩ (fun x ↦ f x b) ⁻¹' Iic t
X'_ne : X'.Nonempty
hX'X : X' ⊆ X
kX' : IsCompact X'
cX' : Convex ℝ X'
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0

Tactic:
specialize hrec X'_ne kX'
      (fun y hy ↦ LowerSemicontinuousOn.mono (hfy y hy) hX'X)
      (fun y hy ↦ cX'.quasiconvexOn_restrict (hfy' y hy) hX'X)
      (fun x hx' ↦ hfx x (hX'X hx'))
      (fun x hx' ↦ hfx' x (hX'X hx'))
      cX'

Goal state after:
case insert.inr
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
Y : Set F
f : E → F → β
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
cY : Convex ℝ Y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
s✝ : Set F
t : β
b : F
s : Set F
a✝ : b ∉ s
hs : s.Finite
X : Set 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
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
cX : Convex ℝ X
hsY : insert b s ⊆ Y
ht : ∀ x ∈ X, ∃ y ∈ insert b s, t < f x y
hb : b ∈ Y
X' : Set E := X ∩ (fun x ↦ f x b) ⁻¹' Iic t
hrec : s ⊆ Y → (∀ x ∈ X', ∃ y ∈ s, t < f x y) → ∃ y0 ∈ Y, ∀ x ∈ X', t < f x y0
X'_ne : X'.Nonempty
hX'X : X' ⊆ X
kX' : IsCompact X'
cX' : Convex ℝ X'
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0