mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Separation.PerfectlyNormal

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (s : Set X), IsClosed[inst✝] s → ∃ f, s = ⇑f ⁻¹' {0} ∧ ∀ (x : X), f x ∈ Icc 0 1
s t : Set X
hs : IsClosed[inst✝] s
ht : IsClosed[inst✝] t
hst : Disjoint s t
f : C(X, ℝ)
hf : s = ⇑f ⁻¹' {0}
hfr : ∀ (x : X), f x ∈ Icc 0 1
g : C(X, ℝ)
hg : t = ⇑g ⁻¹' {0}
hgr : ∀ (x : X), g x ∈ Icc 0 1
hsn : SeparatedNhds {0} {1}
hfg : ∀ (x : X), f x + g x ≠ 0
⊢ SeparatedNhds s t

Tactic:
have hp : s = (fun a => f a / (f a + g a)) ⁻¹' {0} := by simp_all [preimage]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (s : Set X), IsClosed[inst✝] s → ∃ f, s = ⇑f ⁻¹' {0} ∧ ∀ (x : X), f x ∈ Icc 0 1
s t : Set X
hs : IsClosed[inst✝] s
ht : IsClosed[inst✝] t
hst : Disjoint s t
f : C(X, ℝ)
hf : s = ⇑f ⁻¹' {0}
hfr : ∀ (x : X), f x ∈ Icc 0 1
g : C(X, ℝ)
hg : t = ⇑g ⁻¹' {0}
hgr : ∀ (x : X), g x ∈ Icc 0 1
hsn : SeparatedNhds {0} {1}
hfg : ∀ (x : X), f x + g x ≠ 0
hp : s = (fun a ↦ f a / (f a + g a)) ⁻¹' {0}
⊢ SeparatedNhds s t
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
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 y : ↑(s p)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
j' : j = ↑((E q) (Ψ y))
this✝¹ : (F p).snd ((E p) x) ((E p) y) = ⌊ε⁻¹ * dist x y⌋
Ap : (F p).snd ⟨i, hip⟩ ⟨j, hjp⟩ = ⌊ε⁻¹ * dist x y⌋
this✝ : (F q).snd ((E q) (Ψ x)) ((E q) (Ψ y)) = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
Aq : (F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
this : ⌊ε⁻¹ * dist x y⌋ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
I : ε⁻¹ * |dist x y - dist (Ψ x) (Ψ y)| ≤ 1
⊢ |dist x y - dist (Ψ x) (Ψ y)| = ε * (ε⁻¹ * |dist x y - dist (Ψ x) (Ψ y)|)

Tactic:
#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
            (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed
            this goal. It is not yet clear whether this is due to defeq abuse in Mathlib or a
            problem in the new canonicalizer; a minimization would help. The original proof was:
            `grind` -/
            field_simp

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

Goal state before:
pp: 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
⊢ fork F U ≅ (Cone.postcompose (diagram.isoOfIso U α).inv).obj (fork G U)

Tactic:
by
  fapply Fork.ext
  · apply α.app
  · dsimp
    refine Pi.hom_ext _ _ fun b ↦ ?_
    dsimp only [Fork.ι]
    simp [res, diagram.isoOfIso]

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

Goal state before:
pp: case refine_1
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
⊢ ⨅ y, (candidatesBDist X Y) (inl x, inr y) ≤ diam univ + 1 + diam univ

Tactic:
have A : ⨅ y, candidatesBDist X Y (inl x, inr y) ≤ candidatesBDist X Y (inl x, inr default) :=
      ciInf_le (by simpa using HD_below_aux1 0) default

Goal state after:
case refine_1
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)
⊢ ⨅ y, (candidatesBDist X Y) (inl x, inr y) ≤ diam univ + 1 + diam univ
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✝¹ : AddCommGroup F
inst✝ : Module ℝ F
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
b : β
y y' : ↑Y
z : ↑(segment ℝ ↑y ↑y')
x : ↑X
hx : x ∈ sublevelLeft X f b ↑z
⊢ x ∈ sublevelLeft X f b ↑y ∪ sublevelLeft X f b ↑y'

Tactic:
simp only [Set.mem_union, mem_sublevelLeft_iff, ← inf_le_iff]
    specialize hfx' x x.2 (f x y ⊓ f x y')
    rw [convex_iff_segment_subset] at hfx'
    specialize hfx' ⟨y.prop, inf_le_left⟩ ⟨y'.prop, inf_le_right⟩ z.prop
    exact le_trans hfx'.2 hx

Goal state after:
Module: Mathlib.Topology.Subpath

Goal state before:
pp: case right
t₀ t₁ : ↑I
t : ↑(Icc 0 1)
s : ℝ
hs : s ∈ Icc 0 1
hst : (fun θ ↦ (1 - θ) • ↑t₀ + θ • ↑t₁) s = ↑t
⊢ ∃ a, Icc.convexComb t₀ t₁ a = t

Tactic:
use ⟨s, hs⟩

Goal state after:
case h
t₀ t₁ : ↑I
t : ↑(Icc 0 1)
s : ℝ
hs : s ∈ Icc 0 1
hst : (fun θ ↦ (1 - θ) • ↑t₀ + θ • ↑t₁) s = ↑t
⊢ Icc.convexComb t₀ t₁ ⟨s, hs⟩ = t
Module: Mathlib.Topology.Subpath

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ↑I
⊢ range ⇑(γ.subpath t₀ t₁) = ⇑γ '' uIcc t₀ t₁

Tactic:
by
  rw [← range_subpathAux, ← range_comp, subpath, coe_mk', ContinuousMap.coe_mk]

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

Goal state before:
pp: X : Type u_1
inst✝² : UniformSpace X
x : X
V : SetRel X X
inst✝¹ : V.IsSymm
inst✝ : V.IsTrans
h' : V ∈ 𝓤 X
⊢ ∀ x_1 ∈ (ball x V)ᶜ, ∃ V_1 ∈ 𝓤 X, ball x_1 V_1 ⊆ (ball x V)ᶜ

Tactic:
exact fun y hy ↦ ⟨V, h', fun z hyz hxz ↦ hy <| V.trans hxz <| V.symm hyz⟩

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
⊢ (𝓝 x).HasBasis (fun s ↦ x ∈ s ∧ IsClopen s) id

Tactic:
refine (nhds_basis_uniformity' (IsUltraUniformity.hasBasis)).to_hasBasis' ?_ ?_
  · intro V ⟨hV, h_symm, h_trans⟩
    exact ⟨ball x V, ⟨mem_ball_self _ hV,
      isClopen_ball_of_isSymm_of_isTrans_of_mem_uniformity _ hV⟩, le_rfl⟩
  · rintro u ⟨hx, hu⟩
    simp [hu.right.mem_nhds_iff, hx]

Goal state after: