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

Goal state before:
pp: case pos.refine_2
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : MemHolder r f
x₁ x₂ : X
⊢ edist ((c • f) x₁) ((c • f) x₂) ≤ ↑(nnHolderNorm r (c • f)) * edist x₁ x₂ ^ ↑r

Tactic:
exact hf.smul.holderWith x₁ x₂

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

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
x : Snowflaking X α hα₀ hα₁
⊢ edist x x = 0

Tactic:
by simp [edist_def, hα₀]

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

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
x : Snowflaking X α hα₀ hα₁
d : ℝ≥0∞
⊢ ⇑toSnowflaking ⁻¹' closedEBall x d = closedEBall (ofSnowflaking x) (d ^ α⁻¹)

Tactic:
preimage_toSnowflaking_closedEBall

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
x : Snowflaking X α hα₀ hα₁
d : ℝ≥0∞
⊢ closedEBall (ofSnowflaking x) (d ^ α⁻¹) = closedEBall (ofSnowflaking x) (d ^ α⁻¹)
Module: Mathlib.Topology.NatEmbedding

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
U : ℕ → Set X
hUi : ∀ (n : ℕ), (U n).Infinite
hUo : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hd : Pairwise (Disjoint on U)
⊢ ∃ f, IsEmbedding f

Tactic:
choose f hf using fun n ↦ (hUi n).nonempty

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
U : ℕ → Set X
hUi : ∀ (n : ℕ), (U n).Infinite
hUo : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hd : Pairwise (Disjoint on U)
f : ℕ → X
hf : ∀ (n : ℕ), f n ∈ U n
⊢ ∃ f, IsEmbedding f
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: case pos
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕.stalk p₀ ⟶ c
U V : (Opens ↑X)ᵒᵖ
inc : U ⟶ V
hV : p₀ ∈ unop V
hU : p₀ ∈ unop U
⊢ 𝓕.germ (unop U) p₀ ⋯ ≫ f ≫ eqToHom ⋯ = 𝓕.germ (unop U) p₀ hU ≫ f ≫ eqToHom ⋯ ≫ eqToHom ⋯

Tactic:
eqToHom_trans

Goal state after:
case pos
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕.stalk p₀ ⟶ c
U V : (Opens ↑X)ᵒᵖ
inc : U ⟶ V
hV : p₀ ∈ unop V
hU : p₀ ∈ unop U
⊢ 𝓕.germ (unop U) p₀ ⋯ ≫ f ≫ eqToHom ⋯ = 𝓕.germ (unop U) p₀ hU ≫ f ≫ eqToHom ⋯
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: case pos
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕.stalk p₀ ⟶ c
U V : (Opens ↑X)ᵒᵖ
inc : U ⟶ V
hV : p₀ ∈ unop V
⊢ (𝓕.map inc ≫
      if h : p₀ ∈ unop V then 𝓕.germ (unop V) p₀ h ≫ f ≫ eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (𝓕.obj V)) =
    (if h : p₀ ∈ unop U then 𝓕.germ (unop U) p₀ h ≫ f ≫ eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (𝓕.obj U)) ≫
      if h : p₀ ∈ unop V then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then c else ⊤_ C)

pp: case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕.stalk p₀ ⟶ c
U V : (Opens ↑X)ᵒᵖ
inc : U ⟶ V
hV : p₀ ∉ unop V
⊢ (𝓕.map inc ≫
      if h : p₀ ∈ unop V then 𝓕.germ (unop V) p₀ h ≫ f ≫ eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (𝓕.obj V)) =
    (if h : p₀ ∈ unop U then 𝓕.germ (unop U) p₀ h ≫ f ≫ eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (𝓕.obj U)) ≫
      if h : p₀ ∈ unop V then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then c else ⊤_ C)

Tactic:
· have hU : p₀ ∈ U.unop := leOfHom inc.unop hV
      split_ifs
      rw [← Category.assoc, 𝓕.germ_res' inc, Category.assoc, Category.assoc, eqToHom_trans]

Goal state after:
case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕.stalk p₀ ⟶ c
U V : (Opens ↑X)ᵒᵖ
inc : U ⟶ V
hV : p₀ ∉ unop V
⊢ (𝓕.map inc ≫
      if h : p₀ ∈ unop V then 𝓕.germ (unop V) p₀ h ≫ f ≫ eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (𝓕.obj V)) =
    (if h : p₀ ∈ unop U then 𝓕.germ (unop U) p₀ h ≫ f ≫ eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (𝓕.obj U)) ≫
      if h : p₀ ∈ unop V then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then c else ⊤_ C)
Module: Mathlib.Topology.Sheaves.Flasque

Goal state before:
pp: X : TopCat
U : Opens ↑X
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst✝ : S.X₁.IsFlasque
s : ↑(S.X₃.obj.obj (op U))
t : Under S.g s
ht : ∀ (a : Under S.g s), Nonempty (a ⟶ t) → Nonempty (t ⟶ a)
tle : unop (StructuredArrow.right t).fst ≤ U
tcomp :
  (s |_ unop (StructuredArrow.right t).fst) tle =
    (ConcreteCategory.hom (S.g.hom.app (StructuredArrow.right t).fst)) (StructuredArrow.right t).snd
x : ↑X
hx : x ∈ U
this✝¹ : Presheaf.IsLocallySurjective S.g.hom
W : Opens ↑X
Wle : W ≤ U
hW : x ∈ W
t₁ : ↑(S.X₂.obj.obj (op W))
ht₁ : (ConcreteCategory.hom (S.g.hom.app (op W))) t₁ = (s |_ W) Wle
t₂ : ToType (S.X₂.obj.obj (op (unop (StructuredArrow.right t).fst ⊓ W))) :=
  ((StructuredArrow.right t).snd |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯ -
    (t₁ |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯
this✝ : (ConcreteCategory.hom (S.g.hom.app (op (unop (StructuredArrow.right t).fst ⊓ W)))) t₂ = 0
t₃ : ↑(S.X₁.obj.obj (op (unop (StructuredArrow.right t).fst ⊓ W)))
ht₃ : (ConcreteCategory.hom (S.f.hom.app (op (unop (StructuredArrow.right t).fst ⊓ W)))) t₃ = t₂
t₄ : ↑(S.X₁.obj.obj (op W))
ht₄ : (t₄ |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯ = t₃
f : Fin 2 → Opens ↑X := ![unop (StructuredArrow.right t).fst, W]
sf : (i : Fin 2) → ↑(S.X₂.obj.obj (op (f i))) :=
  fun x ↦
    match x with
    | 0 => (StructuredArrow.right t).snd
    | 1 => t₁ + (ConcreteCategory.hom (S.f.hom.app (op W))) t₄
this : (sf 0 |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯ = (sf 1 |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯
t₅ : ToType (S.X₂.obj.obj (op (iSup f)))
ht₅ : IsGluing S.X₂.obj f sf t₅
right✝ : ∀ (y : ToType (S.X₂.obj.obj (op (iSup f)))), (fun t₅ ↦ IsGluing S.X₂.obj f sf t₅) y → y = t₅
le : iSup f ≤ U
⊢ (ConcreteCategory.hom ((S.X₃.obj ⋙ CategoryTheory.forget AddCommGrpCat).map (homOfLE le).op)) ⟨op U, s⟩.snd =
    ((NatTrans.mapElements (Functor.whiskerRight S.g.hom (CategoryTheory.forget AddCommGrpCat))).obj
        ⟨op (iSup f), t₅⟩).snd

Tactic:
by
          refine (eq_app_of_locally_eq ht₅ (by rw [Fin.forall_fin_two]; exact ⟨tle, Wle⟩) ?_).symm
          rw [Fin.forall_fin_two]
          refine ⟨tcomp.symm, ?_⟩
          simp only [Fin.isValue, map_add, homOfLE_leOfHom, sf, f]
          have : (S.f.hom.app (op W) ≫ S.g.hom.app (op W)) = 0 := by
            rw [← NatTrans.comp_app, ← ObjectProperty.FullSubcategory.comp_hom, S.zero]
            rfl
          simp [← CategoryTheory.comp_apply, this, ht₁]
          rfl

Goal state after:
Module: Mathlib.Topology.UniformSpace.OfCompactT2

Goal state before:
pp: case a
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x : γ
| ⨆ i, ⨆ (_ : Inseparable x i), comap (fun x_2 ↦ x) (𝓝 i) ⊓ 𝓝 i

Tactic:
enter [

Goal state after:
case a
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x : γ
| ⨆ i, ⨆ (_ : Inseparable x i), comap (fun x_2 ↦ x) (𝓝 i) ⊓ 𝓝 i
Module: Mathlib.Topology.UniformSpace.OfCompactT2

Goal state before:
pp: case a
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x : γ
| ⨆ i, ⨆ (_ : ¬Inseparable x i), comap (fun x_2 ↦ x) (𝓝 i) ⊓ 𝓝 i

Tactic:
enter [

Goal state after:
case a
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x : γ
| ⨆ i, ⨆ (_ : ¬Inseparable x i), comap (fun x_2 ↦ x) (𝓝 i) ⊓ 𝓝 i
Module: Mathlib.Topology.UniformSpace.OfCompactT2

Goal state before:
pp: γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x : γ
⊢ 𝓝 x = (⨆ i, ⨆ (_ : Inseparable x i), ⊤ ⊓ 𝓝 x) ⊔ ⨆ i, ⨆ (_ : ¬Inseparable x i), ⊥ ⊓ 𝓝 i

Tactic:
iSup_subtype',

Goal state after:
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x : γ
⊢ 𝓝 x = (⨆ x_1, ⊤ ⊓ 𝓝 x) ⊔ ⨆ i, ⨆ (_ : ¬Inseparable x i), ⊥ ⊓ 𝓝 i