mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.UniformSpace.Ultra.Constructions

Goal state before:
pp: X : Type u_1
Y : Type u_2
u : UniformSpace Y
h : IsUltraUniformity Y
f : X → Y
⊢ IsUltraUniformity X

Tactic:
by
  let := u.comap f
  refine .mk_of_hasBasis (h.hasBasis.comap (Prod.map f f)) ?_ ?_ <;>
  · dsimp
    rintro _ ⟨_, _, _⟩
    infer_instance

Goal state after: