mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ∃ ub, ∀ a ∈ c, Nonempty (ub ⟶ a)

Tactic:
have le₂ : ∀ i, i ∈ c → unop i.right.1 ≤ iSup f := fun i hi ↦ le_iSup f ⟨i, hi⟩

Goal state after:
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
⊢ ∃ ub, ∀ a ∈ c, Nonempty (ub ⟶ a)
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ autoParam
    ((α.app (op (iSup U))).hom ≫ Fork.ι ((Cone.postcompose (diagram.isoOfIso U α).inv).obj (fork G U)) = (fork F U).ι)
    Fork.ext._auto_1

Tactic:
dsimp
    refine Pi.hom_ext _ _ fun b ↦ ?_
    dsimp only [Fork.ι]
    simp [res, diagram.isoOfIso]

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

Goal state before:
pp: case h
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
ihi_eq : ⟨i, hi⟩ = (E q) ⟨y, ys⟩
hiq : i < N q
hip : i < N p
z : ↑(s p) := (E p).symm ⟨i, hip⟩
C1 : (E p) z = ⟨i, hip⟩
C2 : Fin.cast Npq ⟨i, hip⟩ = ⟨i, hi⟩
C3 : (E q).symm ⟨i, hi⟩ = ⟨y, ys⟩
this : Φ z = y
⊢ dist x y ≤ ε

Tactic:
exact le_trans (le_of_lt hy) u_le_ε

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:
| succ n s hs h =>

Goal state after: