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

Goal state before:
pp: case mpr
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))
⊢ ∀ {U : Opens ↑X} (s : ToType (𝒢.obj (op U))), Presheaf.imageSieve T s ∈ (Opens.grothendieckTopology ↑X) U

Tactic:
intro U t x hxU

Goal state after:
case mpr
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))
U : Opens ↑X
t : ToType (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
⊢ ∃ U_1 f, (Presheaf.imageSieve T t).arrows f ∧ x ∈ U_1
Module: Mathlib.Topology.Sheaves.Points

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x✝¹ x y : X
x✝ : pointGrothendieckTopology x ⟶ pointGrothendieckTopology y
⊢ (fun s ↦ { hom := { app := fun U ↦ ↾fun hU ↦ { down := { down := ⋯ } }, naturality := ⋯ } }) ⋯ = x✝

Tactic:
by subsingleton

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 → β
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')
⊢ sublevelLeft X f b ↑y ∩ sublevelLeft X f b ↑y' ⊆ ∅

Tactic:
rintro ⟨x, hx⟩ ⟨hx1, hx2⟩

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 → β
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')
x : E
hx : x ∈ X
hx1 : ⟨x, hx⟩ ∈ sublevelLeft X f b ↑y
hx2 : ⟨x, hx⟩ ∈ sublevelLeft X f b ↑y'
⊢ ⟨x, hx⟩ ∈ ∅
Module: Mathlib.Topology.Sheaves.Flasque

Goal state before:
pp: X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : C
inst✝¹ : HasTerminal C
inst✝ : Epi (terminalIsTerminal.from A)
U V : (Opens ↑X)ᵒᵖ
r : U ⟶ V
⊢ Epi ((skyscraperSheaf p₀ A).obj.map r)

Tactic:
by_cases h1 : p₀ ∈ unop U
    · by_cases h2 : p₀ ∈ unop V
      · simp_all only [skyscraperSheaf_obj_obj, skyscraperSheaf_obj_map, ↓reduceDIte]
        infer_instance
      · simp
        grind
    · have h2 : p₀ ∉ unop V := fun hV => h1 (r.unop.le hV)
      have := isIso_of_isTerminal (isTerminalSkyscraperSheafObjObjOfNotMem h1)
        (isTerminalSkyscraperSheafObjObjOfNotMem h2) ((skyscraperSheaf p₀ A).obj.map r)
      infer_instance

Goal state after:
Module: Mathlib.Topology.SmallInductiveDimension

Goal state before:
pp: case succ.succ
m : ℕ
IH :
  ∀ {X : Type u_1} [inst : TopologicalSpace X] {m_1 : ℕ},
    m_1 ≤ m → HasSmallInductiveDimensionLT X m_1 → HasSmallInductiveDimensionLT X m
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set (Set X)
hs : IsTopologicalBasis s
h : ∀ U ∈ s, HasSmallInductiveDimensionLT (↑(frontier U)) n
hmn : n + 1 ≤ m + 1
⊢ HasSmallInductiveDimensionLT X (m + 1)

Tactic:
refine .succ _ s hs fun U hU ↦ IH ?_ (h U hU)
      rwa [add_le_add_iff_right] at hmn

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 : ClusterPt z (𝓟 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:
clusterPt_principal_subtype_iff_frequently (cY.segment_subset y.prop y'.prop)

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' ∈ setOfPred_sublevelLeft_subset X Y f b b' y y', x ∈ sublevelLeft X f b' ↑z'
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 = ∅}
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 : ¬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 = ∅
hY₁B : insert Y₁ B ∉ 𝒮
⊢ insert Y₂ B ∉ 𝒮

Tactic:
intro hY₂B

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 = ∅}
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 : ¬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 = ∅
hY₁B : insert Y₁ B ∉ 𝒮
hY₂B : insert Y₂ B ∈ 𝒮
⊢ False
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 : ι
⊢ ∀ᶠ (c : ι) in atTop, F n x ≤ F c x

Tactic:
filter_upwards [Ici_mem_atTop n] with m hnm

Goal state after:
ι : 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
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
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
t : β
hinfi_le : ∀ y0 ∈ Y, ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 y2 : { x // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x ↑y1) (f x ↑y2)
ha' : IsMinOn (fun x ↦ max (f x ↑y1) (f x ↑y2)) X a
ht' : t' < max (f a ↑y1) (f a ↑y2)
J1 : Set ↑(segment ℝ ↑y1 ↑y2) := setOfPred_sublevelLeft_subset X Y f t t' y1 y2
mem_J1_iff : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), z ∈ J1 ↔ sublevelLeft X f t ↑z ⊆ sublevelLeft X f t' ↑y1
φ : ↑(segment ℝ ↑y1 ↑y2) ≃ₜ ↑(segment ℝ ↑y2 ↑y1) := Homeomorph.setCongr ⋯
J2 : Set ↑(segment ℝ ↑y1 ↑y2) := ⇑φ ⁻¹' setOfPred_sublevelLeft_subset X Y f t t' y2 y1
mem_J2_iff : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), z ∈ J2 ↔ sublevelLeft X f t ↑z ⊆ sublevelLeft X f t' ↑y2
h_mem_Y : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), ↑z ∈ Y
hJ1J2 : J1 ∩ J2 = ∅
hJ1_union_J2 : Subtype.val '' (J1 ∪ J2) = segment ℝ ↑y1 ↑y2
this : IsPreconnected univ
hJ1 : IsClosed J1
hJ2 : IsClosed J2
⊢ Subtype.val '' univ ⊆ Subtype.val '' (J1 ∪ J2)

Tactic:
simp [hJ1_union_J2]

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

Goal state before:
pp: γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
𝓝Δ : Filter (γ × γ) := ⋯
F : Filter (γ × γ) := ⋯
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : (y, y) ∈ (interior V)ᶜ
h : Inseparable x y
⊢ (y, y) ∈ interior V

Tactic:
mem_interior_iff_mem_nhds

Goal state after:
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun s ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : (y, y) ∈ (interior V)ᶜ
h : Inseparable x y
⊢ V ∈ 𝓝 (y, y)
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
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
cX : Convex ℝ X
sup_y : E → β
hsup_y : ∀ x ∈ X, IsLUB {x_1 | ∃ y ∈ Y, f x y = x_1} (sup_y x)
inf_sup : β
hinf_sup : IsGLB {x | ∃ x_1 ∈ X, sup_y x_1 = x} inf_sup
inf_x : F → β
hinf_x : ∀ y ∈ Y, IsGLB {x | ∃ x_1 ∈ X, f x_1 y = x} (inf_x y)
sup_inf : β
hsup_inf : IsLUB {x | ∃ y ∈ Y, inf_x y = x} sup_inf
ne_Y : Y.Nonempty
t : β
x : E
hx : x ∈ X
hx' : ∀ i ∈ Y, f x i ≤ t
c : β
htc : t < c
hc : ∀ a ∈ X, c ≤ sup_y a
⊢ ∀ x_1 ∈ {x_2 | ∃ y ∈ Y, f x y = x_2}, x_1 ≤ t

Tactic:
aesop

Goal state after: