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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : EDist α
d : ℝ≥0∞
f : β → α
s : Set β
⊢ (∀ x ∈ f '' s, ∀ y ∈ f '' s, x ≠ y → d ≤ edist x y) ↔ ∀ x ∈ s, ∀ y ∈ s, f x ≠ f y → d ≤ edist (f x) (f y)

Tactic:
forall_mem_image

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

Goal state before:
pp: case refine_2
X : Type u
inst✝² : MetricSpace X
inst✝¹ : CompactSpace X
inst✝ : Nonempty X
p : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
Ψ : X → ↥(lp (fun n ↦ ℝ) ∞)
isomΨ : Isometry Ψ
rangeΨ : range Ψ = ↑p
⊢ IsometryRel.setoid p (NonemptyCompacts.kuratowskiEmbedding X)

Tactic:
have f :=
      ((kuratowskiEmbedding.isometry X).isometryEquivOnRange.symm.trans
          isomΨ.isometryEquivOnRange).symm

Goal state after:
case refine_2
X : Type u
inst✝² : MetricSpace X
inst✝¹ : CompactSpace X
inst✝ : Nonempty X
p : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
Ψ : X → ↥(lp (fun n ↦ ℝ) ∞)
isomΨ : Isometry Ψ
rangeΨ : range Ψ = ↑p
f : ↑(range Ψ) ≃ᵢ ↑(range (kuratowskiEmbedding X))
⊢ IsometryRel.setoid p (NonemptyCompacts.kuratowskiEmbedding X)
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x : X
r : ℝ
hr : 0 ≤ r
y : X
⊢ { val := y } ∈ ⇑ofSnowflaking ⁻¹' ball x r ↔ { val := y } ∈ ball (toSnowflaking x) (r ^ α)

Tactic:
simp (disch := positivity) [Real.rpow_lt_rpow_iff]

Goal state after:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : IsLower α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsLower β
inst✝ : OrderBot β
⊢ lower (α × β) ≤ instTopologicalSpaceProd

Tactic:
rw [(IsLower.isTopologicalBasis.prod
      IsLower.isTopologicalBasis).eq_generateFrom, le_generateFrom_iff_subset_isOpen,
      image2_subset_iff]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : IsLower α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsLower β
inst✝ : OrderBot β
⊢ ∀ x ∈ IsLower.lowerBasis α, ∀ y ∈ IsLower.lowerBasis β, x ×ˢ y ∈ {s | IsOpen[lower (α × β)] s}
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: case inr
⊢ ∃ a, Ioi a = Ioi False

Tactic:
use False

Goal state after:
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case refine_1.inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
hq : 0 ≤ q
⊢ IsOpen (⇑some ⁻¹' Ioi ⟨toLex (x, q), ⋯⟩)

Tactic:
convert isOpen_Ioi (a := x)
      ext
      simp [some, Prod.Lex.lt_iff, hq.not_gt]

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

Goal state before:
pp: x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun n ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
this : range Φ = range Ψ
T : (↑(range Ψ) ≃ᵢ y.Rep) = (↑(range Φ) ≃ᵢ y.Rep)
eΨ : ↑(range Φ) ≃ᵢ y.Rep
e : x.Rep ≃ᵢ y.Rep
⊢ Nonempty (x.Rep ≃ᵢ y.Rep)

Tactic:
exact ⟨e⟩

Goal state after:
Module: Mathlib.Topology.Separation.PerfectlyNormal

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h : PerfectlyNormalSpace X
s : Set X
hs : IsClosed[inst✝] s
U : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen[inst✝] (U n)
hu : s = ⋂ n, U n
n : ℕ
⊢ s ⊆ U n

Tactic:
grw [hu, iInter_subset]

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

Goal state before:
pp: X : TopCat
C : Type u
inst✝⁴ : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : Limits.HasColimits C
F : Presheaf C X
inst✝ : Limits.PreservesFilteredColimits (forget C)
U : Opens ↑X
hF_bij : ∀ (x : ↑X) (hx : x ∈ U), Bijective ⇑(ConcreteCategory.hom (F.germ U x hx))
x : ↑X
hx : x ∈ U
⊢ ∀ (x_1 : ↑(base ⁻¹' ↑U)),
    Tendsto (fun s ↦ WithTopology.toTopology ⊥ ((ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ (↑s).germ))) (𝓝 x_1)
      (𝓝 (WithTopology.toTopology ⊥ ((ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ (↑x_1).germ))))

Tactic:
nhds_discrete,

Goal state after:
X : TopCat
C : Type u
inst✝⁴ : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : Limits.HasColimits C
F : Presheaf C X
inst✝ : Limits.PreservesFilteredColimits (forget C)
U : Opens ↑X
hF_bij : ∀ (x : ↑X) (hx : x ∈ U), Bijective ⇑(ConcreteCategory.hom (F.germ U x hx))
x : ↑X
hx : x ∈ U
⊢ ∀ (x_1 : ↑(base ⁻¹' ↑U)),
    Tendsto (fun s ↦ WithTopology.toTopology ⊥ ((ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ (↑s).germ))) (𝓝 x_1)
      (pure (WithTopology.toTopology ⊥ ((ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ (↑x_1).germ))))
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✝
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

Tactic:
exact ⟨V, homOfLE Vle, hV⟩

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ ∀ {X_1 : Opens X},
    ∀ R ∈ (grothendieckTopology X) X_1,
      ∀
        (x_1 :
          { obj := fun U ↦ ULift.{u, 0} (PLift (x ∈ U)), map := fun {X_2 Y} f ↦ ↾fun h ↦ { down := { down := ⋯ } },
                map_id := ⋯, map_comp := ⋯ }.obj
            X_1),
        ∃ Y f,
          ∃ (_ : R.arrows f),
            ∃ y,
              (ConcreteCategory.hom
                    ({ obj := fun U ↦ ULift.{u, 0} (PLift (x ∈ U)),
                          map := fun {X_2 Y} f ↦ ↾fun h ↦ { down := { down := ⋯ } }, map_id := ⋯, map_comp := ⋯ }.map
                      f))
                  y =
                x_1

Tactic:
by
    rintro U R hR ⟨⟨hU⟩⟩
    obtain ⟨V, f, hf, hV⟩ := hR x hU
    exact ⟨_, _, hf, ⟨⟨hV⟩⟩, rfl⟩

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

Goal state before:
pp: case pos
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, ∃ N ≤ K n, ∃ x, p ∈ t → univ ⊆ ⋃ x ∈ s, ball x (u n)

Tactic:
have : Nonempty (Equiv (∅ : Set p.Rep) (Fin 0)) := by
        rw [← Fintype.card_eq, card_empty, Fintype.card_fin]

Goal state after:
case pos
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
this : Nonempty (↑∅ ≃ Fin 0)
⊢ ∃ s, ∃ N ≤ K n, ∃ x, p ∈ t → univ ⊆ ⋃ x ∈ s, ball x (u n)
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
f g : Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ⇑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ⇑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ f x
⊢ ⨆ x, ⨅ y, f (inl x, inr y) ≤ (⨆ x, ⨅ y, g (inl x, inr y)) + dist f g

Tactic:
have Z : (⨆ x, ⨅ y, f (inl x, inr y)) ≤ ⨆ x, ⨅ y, g (inl x, inr y) + dist f g :=
    ciSup_mono (HD_bound_aux1 _ (dist f g)) fun x =>
      ciInf_mono ⟨cf, forall_mem_range.2 fun i => Hcf _⟩ fun y => coe_le_coe_add_dist

Goal state after:
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
f g : Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ⇑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ⇑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ f x
Z : ⨆ x, ⨅ y, f (inl x, inr y) ≤ ⨆ x, ⨅ y, g (inl x, inr y) + dist f g
⊢ ⨆ x, ⨅ y, f (inl x, inr y) ≤ (⨆ x, ⨅ y, g (inl x, inr y)) + dist f g
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
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ ∀ ⦃X_1 Y : (CategoryTheory.Pairwise ι)ᵒᵖ⦄ (f : X_1 ⟶ Y),
    ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f ≫
        Opposite.rec
          (fun x ↦
            Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
              c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
          Y =
      Opposite.rec
          (fun x ↦
            Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
              c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
          X_1 ≫
        ((diagram U).op ⋙ F).map f

Tactic:
by
        intro x y f
        induction x with | op x => ?_
        induction y with | op y => ?_
        have ef : f = f.unop.op := rfl
        revert ef
        generalize f.unop = f'
        rintro rfl
        rcases x with (⟨i⟩ | ⟨⟩) <;> rcases y with (⟨⟩ | ⟨j, j⟩) <;> rcases f' with ⟨⟩
        · dsimp
          rw [F.map_id]
          simp
        · dsimp
          simp only [Category.id_comp, Category.assoc]
          have h := c.π.naturality WalkingParallelPairHom.left
          dsimp [SheafConditionEqualizerProducts.leftRes] at h
          simp only [Category.id_comp] at h
          have h' := h =≫ Pi.π _ (i, j)
          rw [h']
          simp only [Category.assoc, limit.lift_π, Fan.mk_π_app]
          rfl
        · dsimp
          simp only [Category.id_comp, Category.assoc]
          have h := c.π.naturality WalkingParallelPairHom.right
          dsimp [SheafConditionEqualizerProducts.rightRes] at h
          simp only [Category.id_comp] at h
          have h' := h =≫ Pi.π _ (j, i)
          rw [h']
          simp
          rfl
        · dsimp
          rw [F.map_id]
          simp

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

Goal state before:
pp: X : Type u_1
⊢ IsUltraUniformity X

Tactic:
let : UniformSpace X := ⊤
  have := Filter.hasBasis_top (α := (X × X))
  rw [← top_uniformity] at this
  exact mk_of_hasBasis this inferInstance inferInstance

Goal state after:
Module: Mathlib.Topology.Sion

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
Y : Set F
f : E → F → β
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
cY : Convex ℝ Y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
s✝ : Set F
t : β
b : F
s : Set F
a✝ : b ∉ s
hs : s.Finite
X : Set E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
cX : Convex ℝ X
hsY : insert b s ⊆ Y
ht : ∀ x ∈ X, ∃ y ∈ insert b s, t < f x y
hb : b ∈ Y
X' : Set E := X ∩ (fun x ↦ f x b) ⁻¹' Iic t
hrec : s ⊆ Y → (∀ x ∈ X', ∃ y ∈ s, t < f x y) → ∃ y0 ∈ Y, ∀ x ∈ X', t < f x y0
X'_ne : X'.Nonempty
hX'X : X' ⊆ X
kX' : IsCompact X'
cX' : Convex ℝ X'
ht_lt : ∀ x ∈ X', ∃ y ∈ s, t < f x y
⊢ s ⊆ Y

Tactic:
by grw [subset_insert b s, hsY]

Goal state after: