mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
Comm : toGlueL hΦ hΨ ∘ optimalGHInjr X Y = toGlueR hΦ hΨ ∘ optimalGHInjl Y Z
⊢ hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) +
      hausdorffDist (range (optimalGHInjl Y Z)) (range (optimalGHInjr Y Z)) =
    dist (toGHSpace X) (toGHSpace Y) + dist (toGHSpace Y) (toGHSpace Z)

Tactic:
rw [hausdorffDist_optimal, hausdorffDist_optimal, ghDist, ghDist]

Goal state after:
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
y : ↑X
h : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ (skyscraperPresheafCoconeOfSpecializes p₀ A h).ι.app U ≫ eqToHom ⋯ ≫ c.ι.app (op ⊤) = c.ι.app U

Tactic:
dsimp
    rw [← c.w (homOfLE <| (le_top : unop U ≤ _)).op]
    change _ ≫ _ ≫ dite _ _ _ ≫ _ = _
    rw [dif_pos]
    · simp only [eqToHom_trans_assoc,
        eqToHom_refl, Category.id_comp, op_unop]
    · exact h.mem_open U.unop.1.2 U.unop.2

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case zero.one.right
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
b : ι × ι
⊢ (rightRes F U ≫ (Pi.mapIso fun x ↦ α.app (op (U x.1 ⊓ U x.2))).hom) ≫ Pi.π (fun p ↦ G.obj (op (U p.1 ⊓ U p.2))) b =
    ((Pi.mapIso fun x ↦ α.app (op (U x))).hom ≫ rightRes G U) ≫ Pi.π (fun p ↦ G.obj (op (U p.1 ⊓ U p.2))) b

Tactic:
simp [rightRes]

Goal state after:
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
⊢ (Sheafify.isLocallyGerm F).pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)

Tactic:
hV

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
⊢ fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
Module: Mathlib.Topology.Sheaves.Flasque

Goal state before:
pp: case neg
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
h1 : p₀ ∉ unop U
⊢ Epi ((skyscraperSheaf p₀ A).obj.map r)

Tactic:
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 mpr
X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsTopologicalBasis {s | IsClopen s} → HasSmallInductiveDimensionLT X 1

Tactic:
· exact fun h ↦ .succ 0 _ h fun _ hU ↦ hU.frontier_eq ▸ .zero

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
a b : X
hab : a ∈ t ∧ b ∈ v
⊢ (a, b) ∈ s

Tactic:
obtain ⟨x, hx⟩ := hu

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
a b : X
hab : a ∈ t ∧ b ∈ v
x : X
hx : x ∈ u
⊢ (a, b) ∈ s
Module: Mathlib.Topology.UniformSpace.Ultra.Basic

Goal state before:
pp: case refine_2
X : Type u_1
inst✝¹ : UniformSpace X
inst✝ : IsUltraUniformity X
x : X
⊢ ∀ (i' : Set X), x ∈ i' ∧ IsClopen i' → id i' ∈ 𝓝 x

Tactic:
rintro u ⟨hx, hu⟩
    simp [hu.right.mem_nhds_iff, hx]

Goal state after: