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

Goal state before:
pp: case refine_2
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
T : ℱ ⟶ 𝒢
h :
  ∀ (U : Opens ↑X) (t : ToType (𝒢.obj (op U))),
    ∀ x ∈ U, ∃ V, ∃ (x_1 : V ≤ U), (∃ s, (ConcreteCategory.hom (T.app (op V))) s = (t |_ V) x_1) ∧ x ∈ V
U✝ : Opens ↑X
s : ToType (𝒢.obj (op U✝))
x : ↑X
hx : x ∈ U✝
⊢ ∃ U f, (Presheaf.imageSieve T s).arrows f ∧ x ∈ U

Tactic:
obtain ⟨V, Vle, hV⟩ := h _ s x hx

Goal state after:
case refine_2
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
T : ℱ ⟶ 𝒢
h :
  ∀ (U : Opens ↑X) (t : ToType (𝒢.obj (op U))),
    ∀ x ∈ U, ∃ V, ∃ (x_1 : V ≤ U), (∃ s, (ConcreteCategory.hom (T.app (op V))) s = (t |_ V) x_1) ∧ x ∈ V
U✝ : Opens ↑X
s : ToType (𝒢.obj (op U✝))
x : ↑X
hx : x ∈ U✝
V : Opens ↑X
Vle : V ≤ U✝
hV : (∃ s_1, (ConcreteCategory.hom (T.app (op V))) s_1 = (s |_ V) Vle) ∧ x ∈ V
⊢ ∃ U f, (Presheaf.imageSieve T s).arrows f ∧ x ∈ U
Module: Mathlib.Topology.Sheaves.MayerVietoris

Goal state before:
pp: case refine_1
T : Type u
inst✝ : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
s : PullbackCone sq.f₂₄ sq.f₃₄
⊢ s.pt ⟶ sq.X₁

Tactic:
apply homOfLE

Goal state after:
case refine_1
T : Type u
inst✝ : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
s : PullbackCone sq.f₂₄ sq.f₃₄
⊢ s.pt ≤ sq.X₁
Module: Mathlib.Topology.Sheaves.MayerVietoris

Goal state before:
pp: case refine_2
T : Type u
inst✝ : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
s✝ : PullbackCone sq.f₂₄ sq.f₃₄
⊢ homOfLE ⋯ ≫ sq.f₁₂ = s✝.fst

Tactic:
apply Subsingleton.elim

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

Goal state before:
pp: case refine_3
T : Type u
inst✝ : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
s✝ : PullbackCone sq.f₂₄ sq.f₃₄
⊢ homOfLE ⋯ ≫ sq.f₁₃ = s✝.snd

Tactic:
apply Subsingleton.elim

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

Goal state before:
pp: case refine_4
T : Type u
inst✝ : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
s✝ : PullbackCone sq.f₂₄ sq.f₃₄
m✝ : s✝.pt ⟶ sq.X₁
x✝¹ : m✝ ≫ sq.f₁₂ = s✝.fst
x✝ : m✝ ≫ sq.f₁₃ = s✝.snd
⊢ m✝ = homOfLE ⋯

Tactic:
apply Subsingleton.elim

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

Goal state before:
pp: case neg
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 ≤ ε
p : GHSpace
hp : ¬p ∉ t
s : Set p.Rep
scover : univ ⊆ ⋃ x ∈ s, ball x (u n)
N : ℕ
scard : ↑N ≤ ↑(K n)
hN : #↑s = ↑N
⊢ ∃ s, ∃ N ≤ K n, ∃ x, p ∈ t → univ ⊆ ⋃ x ∈ s, ball x (u n)

Tactic:
Nat.cast_le

Goal state after:
case neg
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 ≤ ε
p : GHSpace
hp : ¬p ∉ t
s : Set p.Rep
scover : univ ⊆ ⋃ x ∈ s, ball x (u n)
N : ℕ
scard : N ≤ K n
hN : #↑s = ↑N
⊢ ∃ s, ∃ N ≤ K n, ∃ x, p ∈ t → univ ⊆ ⋃ x ∈ s, ball x (u n)
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: 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
c c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
i j : ι
⊢ f.hom ≫ c'.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j) =
    c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j)

Tactic:
← f.w WalkingParallelPair.one,

Goal state after:
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
c c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
i j : ι
⊢ f.hom ≫ c'.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j) =
    (f.hom ≫ c'.π.app WalkingParallelPair.one) ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j)
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: 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

Tactic:
exact dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _)

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

Goal state before:
pp: 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

Tactic:
exact dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _)

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

Goal state before:
pp: 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

Tactic:
exact dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _)

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

Goal state before:
pp: 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

Tactic:
exact dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _)

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

Goal state before:
pp: X : Type u_1
s : SetRel X X
t u v : Set X
inst✝ : s.IsTrans
htu : t ×ˢ u ⊆ s
huv : u ×ˢ v ⊆ s
hu : u.Nonempty
⊢ t ×ˢ v ⊆ s

Tactic:
rintro ⟨a, b⟩ hab

Goal state after:
X : Type u_1
s : SetRel X X
t u v : Set X
inst✝ : s.IsTrans
htu : t ×ˢ u ⊆ s
huv : u ×ˢ v ⊆ s
hu : u.Nonempty
a b : X
hab : (a, b) ∈ t ×ˢ v
⊢ (a, b) ∈ s