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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
D s : ℝ≥0
A : Set X
hs : s ≤ r
hA : ∀ ⦃x : X⦄, x ∈ A → ∀ ⦃y : X⦄, y ∈ A → edist x y ≤ ↑D
hf : ∃ C, HolderWith C r (A.domRestrict f)
this : PseudoMetricSpace ↑A := PseudoEMetricSpace.toPseudoMetricSpace ⋯
⊢ ∃ C, HolderWith C s (A.domRestrict f)

Tactic:
have : BoundedSpace A := Metric.boundedSpace_iff_edist.2 ⟨D, fun x y ↦ hA x.2 y.2⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
D s : ℝ≥0
A : Set X
hs : s ≤ r
hA : ∀ ⦃x : X⦄, x ∈ A → ∀ ⦃y : X⦄, y ∈ A → edist x y ≤ ↑D
hf : ∃ C, HolderWith C r (A.domRestrict f)
this✝ : PseudoMetricSpace ↑A := PseudoEMetricSpace.toPseudoMetricSpace ⋯
this : BoundedSpace ↑A
⊢ ∃ C, HolderWith C s (A.domRestrict f)
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case intro
α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
val✝ : Fintype ↑s
w : α × α
hed : s.offDiag.toFinset.inf (uncurry edist) = uncurry edist w
hxy : w ∈ s.offDiag
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.offDiag.toFinset.inf (uncurry edist) = edist x y

Tactic:
exact ⟨w.fst, hxy.1, w.snd, hxy.2.1, hxy.2.2, hed⟩

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
val✝ : Fintype ↑s
hs : s.Nontrivial
⊢ 0 < s.einfsep

Tactic:
rcases hs.einfsep_exists_of_finite with ⟨x, _hx, y, _hy, hxy, hxy'⟩

Goal state after:
case pos
α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
val✝ : Fintype ↑s
hs : s.Nontrivial
x : α
_hx : x ∈ s
y : α
_hy : y ∈ s
hxy : x ≠ y
hxy' : s.einfsep = edist x y
⊢ 0 < s.einfsep
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case intro
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
val✝ : Fintype ↑s
w : α × α
hed : s.offDiag.toFinset.inf' ⋯ (uncurry dist) = uncurry dist w
hxy : w ∈ s.offDiag
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.offDiag.toFinset.inf' ⋯ (uncurry dist) = dist x y

Tactic:
exact ⟨w.fst, hxy.1, w.snd, hxy.2.1, hxy.2.2, hed⟩

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

Goal state before:
pp: case h
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
y : α
r : ℚ
hy₁ : IsSuccPrelimit y → 0 ≤ r
hy₂ : IsPredPrelimit y → r ≤ 0
h : x < y
hx : IsPredPrelimit x
z : α
hz : x < z
hz' : z < y
⊢ ⟨toLex (x, q), ⋯⟩ < some z ∧ some z < ⟨toLex (y, r), ⋯⟩

Tactic:
simp [some, Prod.Lex.lt_iff, hz', hz]

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
⊢ {s | ∃ t, t.Finite ∧ ∃ u, IsOpen[scott α univ] u ∧ u \ ↑(upperClosure t) = s} =
    {c |
      ∃ a ∈ {s | ∃ t, t.Finite ∧ (↑(upperClosure t))ᶜ = s},
        ∃ b ∈ {U | IsOpen[scott α univ] U}, ⇑WithLower.toLower ⁻¹' a ∩ ⇑WithScott.toScott ⁻¹' b = c}

Tactic:
simp_rw [sdiff_eq_compl_inter]

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
⊢ {s | ∃ t, t.Finite ∧ ∃ u, IsOpen[scott α univ] u ∧ (↑(upperClosure t))ᶜ ∩ u = s} =
    {c |
      ∃ a ∈ {s | ∃ t, t.Finite ∧ (↑(upperClosure t))ᶜ = s},
        ∃ b ∈ {U | IsOpen[scott α univ] U}, ⇑WithLower.toLower ⁻¹' a ∩ ⇑WithScott.toScott ⁻¹' b = c}
Module: Mathlib.Topology.Partial

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
r : SetRel Y X
l : Filter Y
x : X
⊢ RTendsto' r l (𝓝 x) ↔ ∀ (s : Set X), IsOpen[inst✝] s → x ∈ s → r.preimage s ∈ l

Tactic:
rw [rtendsto'_def]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
r : SetRel Y X
l : Filter Y
x : X
⊢ (∀ s ∈ 𝓝 x, r.preimage s ∈ l) ↔ ∀ (s : Set X), IsOpen[inst✝] s → x ∈ s → r.preimage s ∈ l
Module: Mathlib.Topology.Sheaves.LocallySurjective

Goal state before:
pp: 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
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))
U : Opens ↑X
t : ToType (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : CC (𝒢.stalk x) := (ConcreteCategory.hom (𝒢.germ U x hxU)) t
ht_x : t_x = (ConcreteCategory.hom (𝒢.germ U x hxU)) t
V : Opens ↑X
hxV : x ∈ V
s : ToType (ℱ.obj (op V))
hs_x : (ConcreteCategory.hom ((stalkFunctor C x).map T)) ((ConcreteCategory.hom (ℱ.germ V x hxV)) s) = t_x
⊢ (ConcreteCategory.hom (𝒢.germ V x hxV)) ((ConcreteCategory.hom (T.app (op V))) s) =
    (ConcreteCategory.hom (𝒢.germ U x hxU)) t

Tactic:
convert! hs_x using 1
      symm
      convert! stalkFunctor_map_germ_apply _ _ _ _ s

Goal state after:
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)
main : ghDist p.Rep q.Rep ≤ ε + ε / 2 + ε
⊢ dist p q ≤ δ

Tactic:
calc
    dist p q = ghDist p.Rep q.Rep := dist_ghDist p q
    _ ≤ ε + ε / 2 + ε := main
    _ = δ := by ring

Goal state after:
Module: Mathlib.Topology.SmallInductiveDimension

Goal state before:
pp: case zero
X : Type u_1
inst✝ : TopologicalSpace X
h : HasSmallInductiveDimensionLT X 0
⊢ smallInductiveDimension X < ↑0

Tactic:
smallInductiveDimension,

Goal state after:
case zero
X : Type u_1
inst✝ : TopologicalSpace X
h : HasSmallInductiveDimensionLT X 0
⊢ sInf {n | ∀ (i : ℕ), n < ↑i → HasSmallInductiveDimensionLT X i} < ↑0