mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
x : CategoryTheory.Pairwise ι
⊢ 𝟙 ((coneEquiv F U).symm.functor.obj (SheafConditionEqualizerProducts.fork F U)).pt ≫
      (Functor.mapCone F (cocone U).op).π.app (op x) =
    ((coneEquiv F U).symm.functor.obj (SheafConditionEqualizerProducts.fork F U)).π.app (op x)

Tactic:
rcases x with ⟨⟩

Goal state after:
case op.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
a✝ : ι
⊢ 𝟙 ((coneEquiv F U).symm.functor.obj (SheafConditionEqualizerProducts.fork F U)).pt ≫
      (Functor.mapCone F (cocone U).op).π.app (op (single a✝)) =
    ((coneEquiv F U).symm.functor.obj (SheafConditionEqualizerProducts.fork F U)).π.app (op (single a✝))

case op.pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
a✝¹ a✝ : ι
⊢ 𝟙 ((coneEquiv F U).symm.functor.obj (SheafConditionEqualizerProducts.fork F U)).pt ≫
      (Functor.mapCone F (cocone U).op).π.app (op (Pairwise.pair a✝¹ a✝)) =
    ((coneEquiv F U).symm.functor.obj (SheafConditionEqualizerProducts.fork F U)).π.app (op (Pairwise.pair a✝¹ a✝))
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
x : CategoryTheory.Pairwise ι
⊢ 𝟙 (Functor.mapCone F (cocone U).op).pt ≫
      ((coneEquiv F U).symm.functor.obj (SheafConditionEqualizerProducts.fork F U)).π.app (op x) =
    (Functor.mapCone F (cocone U).op).π.app (op x)

Tactic:
rcases x with ⟨⟩

Goal state after:
case op.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
a✝ : ι
⊢ 𝟙 (Functor.mapCone F (cocone U).op).pt ≫
      ((coneEquiv F U).symm.functor.obj (SheafConditionEqualizerProducts.fork F U)).π.app (op (single a✝)) =
    (Functor.mapCone F (cocone U).op).π.app (op (single a✝))

case op.pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
a✝¹ a✝ : ι
⊢ 𝟙 (Functor.mapCone F (cocone U).op).pt ≫
      ((coneEquiv F U).symm.functor.obj (SheafConditionEqualizerProducts.fork F U)).π.app (op (Pairwise.pair a✝¹ a✝)) =
    (Functor.mapCone F (cocone U).op).π.app (op (Pairwise.pair a✝¹ a✝))
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:
← 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
s : Set X
hs : IsCompact s
ho : IsOpen[inst✝] s
⊢ IsOpen[constructibleTopology X] s

Tactic:
apply TopologicalSpace.isOpen_generateFrom_of_mem

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
ho : IsOpen[inst✝] s
⊢ s ∈ constructibleTopologySubbasis X
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact sᶜ
ho : IsClosed[inst✝] s
⊢ IsOpen[constructibleTopology X] s

Tactic:
apply TopologicalSpace.isOpen_generateFrom_of_mem

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact sᶜ
ho : IsClosed[inst✝] s
⊢ s ∈ constructibleTopologySubbasis X
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
s : Set X
hs : s ∈ constructibleTopologySubbasis X
⊢ IsCompact s

Tactic:
obtain (hs | hs) := hs

Goal state after:
case inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
s : Set X
hs : s ∈ {s | IsOpen[inst✝¹] s ∧ IsCompact s}
⊢ IsCompact s

case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
s : Set X
hs : s ∈ {s | IsClosed[inst✝¹] s ∧ IsCompact sᶜ}
⊢ IsCompact s
Module: Mathlib.Topology.UniformSpace.CompareReals

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

Tactic:
ext s
  rw [(AbsoluteValue.hasBasis_uniformity _).mem_iff, Metric.uniformity_basis_dist_rat.mem_iff]
  simp only [Rat.dist_eq, AbsoluteValue.abs_apply, ← Rat.cast_sub, ← Rat.cast_abs, Rat.cast_lt,
    _root_.abs_sub_comm]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝⁵ : Preorder ι
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup G
inst✝² : Lattice G
inst✝¹ : HasSolidNorm G
inst✝ : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h_tendsto : ∀ (x : α), Tendsto (fun x_1 ↦ F x_1 x) atTop (𝓝 (f x))
x✝ : atTop.NeBot
x : α
n m : ι
hnm : m ∈ Set.Ici n
⊢ F n x ≤ F m x

Tactic:
exact hF_mono hnm x

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]
  constructor
  · rintro ⟨V, V_in, V_sub⟩
    rw [IsUltraUniformity.hasBasis.mem_iff'] at V_in
    obtain ⟨U, ⟨U_in, U_sym, U_trans⟩, U_sub⟩ := V_in
    refine ⟨U, U_in, U_sym, U_trans, (UniformSpace.ball_mono U_sub _).trans V_sub⟩
  · rintro ⟨V, V_in, _, _, V_sub⟩
    exact ⟨V, V_in, V_sub⟩

Goal state after:
Module: Mathlib.Topology.Sion

Goal state before:
pp: case right
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
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
cX : Convex ℝ X
ne_Y : Y.Nonempty
η : E → F
η_mem : ∀ x ∈ X, η x ∈ Y
η_max : ∀ x ∈ X, IsMaxOn (f x) Y (η x)
hlsc : LowerSemicontinuousOn (fun x ↦ f x (η x)) X
a : E
ha : a ∈ X
ha' : IsMinOn (fun x ↦ f x (η x)) X a
ξ : F → E
ξ_mem : ∀ y ∈ Y, ξ y ∈ X
ξ_min : ∀ y ∈ Y, IsMinOn (fun x ↦ f x y) X (ξ y)
husc : UpperSemicontinuousOn (fun x ↦ f (ξ x) x) Y
⊢ ∃ b ∈ Y, IsSaddlePointOn X Y f a b

Tactic:
obtain ⟨b, hb, hb'⟩ : ∃ b ∈ Y, IsMaxOn (fun y ↦ f (ξ y) y) Y b := husc.exists_isMaxOn ne_Y kY

Goal state after:
case right
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
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
cX : Convex ℝ X
ne_Y : Y.Nonempty
η : E → F
η_mem : ∀ x ∈ X, η x ∈ Y
η_max : ∀ x ∈ X, IsMaxOn (f x) Y (η x)
hlsc : LowerSemicontinuousOn (fun x ↦ f x (η x)) X
a : E
ha : a ∈ X
ha' : IsMinOn (fun x ↦ f x (η x)) X a
ξ : F → E
ξ_mem : ∀ y ∈ Y, ξ y ∈ X
ξ_min : ∀ y ∈ Y, IsMinOn (fun x ↦ f x y) X (ξ y)
husc : UpperSemicontinuousOn (fun x ↦ f (ξ x) x) Y
b : F
hb : b ∈ Y
hb' : IsMaxOn (fun y ↦ f (ξ y) y) Y b
⊢ ∃ b ∈ Y, IsSaddlePointOn X Y f a b