mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ (ConcreteCategory.hom (X.map (intervalEdge j l hjl).op)) (sx.spineToSimplex f) =
    sx.spineToDiagonal (f.interval j l hjl)

Tactic:
dsimp only [spineToDiagonal, SimplicialObject.diagonal]
  rw [← spineToSimplex_interval, ← Functor.map_comp_apply, ← op_comp,
    diag_subinterval_eq]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X Y : SSet
sx : X.StrictSegal
sy : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
⊢ sy.spineToSimplex (f.map σ) = (ConcreteCategory.hom (σ.app (Opposite.op ⦋n + 1⦌))) (sx.spineToSimplex f)

Tactic:
apply sy.spineInjective
  ext k
  dsimp only [spineEquiv, Equiv.coe_fn_mk, spine_arrow]
  rw [← types_comp_apply (σ.app _) (Y.map _), ← σ.naturality, types_comp_apply,
    spineToSimplex_arrow, spineToSimplex_arrow, Path.map_arrow]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a b c : CatEnriched C
f f' : a ⟶ b
α : f = f'
g g' : b ⟶ c
β : g = g'
⊢ hComp (eqToHom α) (eqToHom β) = eqToHom ⋯

Tactic:
cases α

Goal state after:
case refl
C : Type u_1
inst✝ : EnrichedCategory Cat C
a b c : CatEnriched C
f : a ⟶ b
g g' : b ⟶ c
β : g = g'
⊢ hComp (eqToHom ⋯) (eqToHom β) = eqToHom ⋯
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f g : X ⟶ Y
α β : f ⟶ g
H : base α = base β
⊢ α = β

Tactic:
cases α

Goal state after:
case mk'
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f g : X ⟶ Y
β : f ⟶ g
base'✝ : homEquiv f ⟶ homEquiv g
H : { base' := base'✝ }.base = base β
⊢ { base' := base'✝ } = β
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f g : X ⟶ Y
α : f = g
⊢ base (eqToHom α) = eqToHom ⋯

Tactic:
cases α

Goal state after:
case refl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f : X ⟶ Y
⊢ base (eqToHom ⋯) = eqToHom ⋯
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c : CatEnrichedOrdinary C
f f' : a ⟶ b
α : f = f'
g g' : b ⟶ c
β : g = g'
⊢ hComp (eqToHom α) (eqToHom β) = eqToHom ⋯

Tactic:
cases α

Goal state after:
case refl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c : CatEnrichedOrdinary C
f : a ⟶ b
g g' : b ⟶ c
β : g = g'
⊢ hComp (eqToHom ⋯) (eqToHom β) = eqToHom ⋯
Module: Mathlib.CategoryTheory.Functor.FunctorHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
A : C ⥤ Type (max u v v')
φ : A ⟶ F.functorHom G
⊢ (fun x ↦
        { app := fun X ↦ ↾fun a ↦ { app := fun Y f ↦ x.app Y ((ConcreteCategory.hom (A.map f)) a), naturality := ⋯ },
          naturality := ⋯ })
      ((fun φ ↦
          { app := fun X a ↦ ((ConcreteCategory.hom (φ.app X)) a).app X (𝟙 (Opposite.unop (Opposite.op X))),
            naturality := ⋯ })
        φ) =
    φ

Tactic:
ext X a Y f
    exact (HomObj.congr_app (ConcreteCategory.congr_hom (φ.naturality f) a) Y (𝟙 _)).trans
      (congr_arg ((φ.app X a).app Y) (by simp))

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' Y Y' : C
f : X ⟶ X'
g : Y ⟶ Y'
⊢ eHomWhiskerLeft V X' g ≫ eHomWhiskerRight V f Y' = eHomWhiskerRight V f Y ≫ eHomWhiskerLeft V X g

Tactic:
by
  dsimp [eHomWhiskerLeft, eHomWhiskerRight]
  rw [assoc, assoc, assoc, assoc, leftUnitor_inv_naturality_assoc,
    whisker_exchange_assoc, ← e_assoc, leftUnitor_tensor_inv_assoc,
    associator_inv_naturality_left_assoc, Iso.hom_inv_id_assoc,
    ← comp_whiskerRight_assoc, whisker_exchange_assoc,
    MonoidalCategory.whiskerRight_id_assoc, assoc, Iso.inv_hom_id_assoc,
    whisker_exchange_assoc, MonoidalCategory.whiskerRight_id_assoc, Iso.inv_hom_id_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝⁷ : Category.{w, v} V
inst✝⁶ : MonoidalCategory V
C✝ : Type u₁
inst✝⁵ : EnrichedCategory V C✝
W : Type v'
inst✝⁴ : Category.{w', v'} W
inst✝³ : MonoidalCategory W
C : Type u₁
inst✝² : EnrichedCategory W C
D : Type u₂
inst✝¹ : EnrichedCategory W D
E : Type u₃
inst✝ : EnrichedCategory W E
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ForgetEnrichment.homOf W
      (ForgetEnrichment.homTo W (f ≫ g) ≫ F.map (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Z✝)) =
    ForgetEnrichment.homOf W
        (ForgetEnrichment.homTo W f ≫ F.map (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝)) ≫
      ForgetEnrichment.homOf W
        (ForgetEnrichment.homTo W g ≫ F.map (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝))

Tactic:
apply_fun ForgetEnrichment.homTo W
    · simp only [Iso.cancel_iso_inv_left, Category.assoc, ← tensorHom_comp_tensorHom,
        ForgetEnrichment.homTo_homOf, EnrichedFunctor.map_comp, ForgetEnrichment.homTo_comp]
      rfl
    · intro f g w; apply_fun ForgetEnrichment.homOf W at w; simpa using w

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝⁷ : Category.{w, v} V
inst✝⁶ : MonoidalCategory V
C✝ : Type u₁
inst✝⁵ : EnrichedCategory V C✝
W : Type v'
inst✝⁴ : Category.{w', v'} W
inst✝³ : MonoidalCategory W
C : Type u₁
inst✝² : EnrichedCategory W C
D : Type u₂
inst✝¹ : EnrichedCategory W D
E : Type u₃
inst✝ : EnrichedCategory W E
F : EnrichedFunctor W C D
G : EnrichedFunctor W D E
X✝ Y✝ : ForgetEnrichment W C
f : X✝ ⟶ Y✝
⊢ (comp W F G).forget.map f ≫ (Iso.refl ((comp W F G).forget.obj Y✝)).hom =
    (Iso.refl ((comp W F G).forget.obj X✝)).hom ≫ (F.forget ⋙ G.forget).map f

Tactic:
simp [comp, forget]

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : TransportEnrichment F (ForgetEnrichment V D)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ForgetEnrichment.homOf W
      ((λ_ (𝟙_ W)).inv ≫
        𝟙_ W ◁ Functor.LaxMonoidal.ε F ≫
          Functor.LaxMonoidal.ε F ▷ F.obj (𝟙_ V) ≫
            (F.map (ForgetEnrichment.homTo V f) ⊗ₘ F.map (ForgetEnrichment.homTo V g)) ≫
              eComp W (ForgetEnrichment.to V X✝) (ForgetEnrichment.to V Y✝) (ForgetEnrichment.to V Z✝)) =
    ForgetEnrichment.homOf W
      ((λ_ (𝟙_ W)).inv ≫
        (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V f) ⊗ₘ
            Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V g)) ≫
          eComp W X✝ Y✝ Z✝)

Tactic:
← tensorHom_def'_assoc,

Goal state after:
V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : TransportEnrichment F (ForgetEnrichment V D)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ForgetEnrichment.homOf W
      ((λ_ (𝟙_ W)).inv ≫
        (Functor.LaxMonoidal.ε F ⊗ₘ Functor.LaxMonoidal.ε F) ≫
          (F.map (ForgetEnrichment.homTo V f) ⊗ₘ F.map (ForgetEnrichment.homTo V g)) ≫
            eComp W (ForgetEnrichment.to V X✝) (ForgetEnrichment.to V Y✝) (ForgetEnrichment.to V Z✝)) =
    ForgetEnrichment.homOf W
      ((λ_ (𝟙_ W)).inv ≫
        (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V f) ⊗ₘ
            Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V g)) ≫
          eComp W X✝ Y✝ Z✝)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: case mpr
V : Truncated 2
X✝ Y✝ : V.HomotopyCategory
f : X✝ ⟶ Y✝
⊢ (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)).strictMap (quotientFunctor V) f → morphismPropertyHomMk V f

Tactic:
rintro ⟨⟨_, _, e⟩⟩

Goal state after:
case mpr
V : Truncated 2
X✝ Y✝ : V.HomotopyCategory
X Y : Cat.FreeRefl (OneTruncation₂ V)
fst✝¹ fst✝ : OneTruncation₂ V
e : fst✝¹ ⟶ fst✝
⊢ morphismPropertyHomMk V ((quotientFunctor V).map (Cat.FreeRefl.homMk ⟨fst✝¹, ⟨fst✝, e⟩⟩.snd.snd))
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: A : Truncated 2
inst✝ : A.Quasicategory₂
x y z : A.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
⊢ ∀ {X Y : A.HomotopyCategory₂} (f : X ⟶ Y), f ≫ 𝟙 Y = f

Tactic:
rintro _ _ ⟨f⟩
    exact ((compStruct _ _).comp_unique (compId _) .refl .refl).congr_homotopyCategory₂HomMk

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case succ.comp_of.inr.inr
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)),
    P_δ f → ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
x X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
f : x ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
h' : x.len < (mk (n + 1)).len
j : Fin (n + 1)
j' : Fin (n + 2)
h'' : δ k ≫ σ i = σ j ≫ δ j'
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m

Tactic:
obtain ⟨z, e, m, he, hm, fac⟩ := hn j f hf

Goal state after:
case succ.comp_of.inr.inr
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)),
    P_δ f → ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
x X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
f : x ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
h' : x.len < (mk (n + 1)).len
j : Fin (n + 1)
j' : Fin (n + 2)
h'' : δ k ≫ σ i = σ j ≫ δ j'
z : SimplexCategoryGenRel
e : x ⟶ z
m : z ⟶ mk n
he : P_σ e
hm : P_δ m
fac : f ≫ σ j = e ≫ m
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: case neg
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
⊢ 0 = (ConcreteCategory.hom f) i

Tactic:
obtain ⟨j, hj⟩ : ∃ (j : Fin 2), f i = j := ⟨_, rfl⟩

Goal state after:
case neg
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
j : Fin 2
hj : (ConcreteCategory.hom f) i = j
⊢ 0 = (ConcreteCategory.hom f) i
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd

Goal state before:
pp: X₁ X₂ : SSet
d₁ d₂ : ℕ
inst✝¹ : X₁.HasDimensionLT d₁
inst✝ : X₂.HasDimensionLT d₂
n : ℕ
hn : d₁ + d₂ ≤ n + 1
⊢ (X₁ ⊗ X₂).HasDimensionLT n

Tactic:
rw [← hasDimensionLT_subcomplex_top_iff, ← iSup_subcomplexOfSimplex_prod_eq_top]
  simp only [Subcomplex.ofSimplexProd_eq_range, hasDimensionLT_iSup_iff]
  intro x₁ x₂
  have := X₁.dim_lt_of_nonDegenerate ⟨_, x₁.nonDegenerate⟩ d₁
  have := X₂.dim_lt_of_nonDegenerate ⟨_, x₂.nonDegenerate⟩ d₂
  have := (Δ[x₁.dim] ⊗ Δ[x₂.dim]).hasDimensionLT_of_le (x₁.dim + x₂.dim + 1) n
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst✝ : P.IsProper
g : unop (op ⦋(↑c.s).dim⦌) ⟶ ⦋c.dim + 1⦌
h₁ : stdSimplex.objEquiv.symm g ∈ c.horn.obj (op ⦋(↑c.s).dim⦌)
h₂ : (ConcreteCategory.hom (X.map g.op)) ((↑(P.p c.s)).cast ⋯).simplex = (↑c.s).simplex
this : Mono g
⊢ False

Tactic:
obtain rfl := (P.isUniquelyCodimOneFace c.s).unique rfl _ h₂

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst✝ : P.IsProper
h₁ : stdSimplex.objEquiv.symm (SimplexCategory.δ (⋯.index ⋯)) ∈ c.horn.obj (op ⦋(↑c.s).dim⦌)
h₂ : (ConcreteCategory.hom (X.map (SimplexCategory.δ (⋯.index ⋯)).op)) ((↑(P.p c.s)).cast ⋯).simplex = (↑c.s).simplex
this : Mono (SimplexCategory.δ (⋯.index ⋯))
⊢ False
Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : HasPushouts C
A B X Y Z W : C
f : A ⟶ B
g : X ⟶ Y
h : Z ⊗ W ⟶ A
⊢ (α_ Z W X).inv ≫ h ▷ X ≫ f ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g) =
    (α_ Z W X).inv ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g)

Tactic:
← comp_whiskerRight_assoc

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : HasPushouts C
A B X Y Z W : C
f : A ⟶ B
g : X ⟶ Y
h : Z ⊗ W ⟶ A
⊢ (α_ Z W X).inv ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g) =
    (α_ Z W X).inv ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesColimit

Goal state before:
pp: X : SSet
s : Cocone X.functorN
x✝ : (MultispanShape.prod X.N).L
x y u t : X.N
h : t.simplex ∈ u.subcomplex.obj (op ⦋t.dim⦌)
⊢ t ≤ u

Tactic:
rwa [N.le_iff, Subcomplex.ofSimplex_le_iff]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: ⊢ stdSimplex.δ 1 ≫
      (sSetTopAdj.homEquiv Δ[1] TopCat.I)
        (TopCat.isoOfHomeo (⦋1⦌.toTopHomeo.trans (stdSimplexHomeomorphUnitInterval.trans Homeomorph.ulift.symm))).hom =
    SSet.const (TopCat.toSSetObj₀Equiv.symm 0)

Tactic:
← Adjunction.homEquiv_naturality_left,

Goal state after:
⊢ (sSetTopAdj.homEquiv Δ[0] TopCat.I)
      (toTop.map (stdSimplex.δ 1) ≫
        (TopCat.isoOfHomeo (⦋1⦌.toTopHomeo.trans (stdSimplexHomeomorphUnitInterval.trans Homeomorph.ulift.symm))).hom) =
    SSet.const (TopCat.toSSetObj₀Equiv.symm 0)
Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy

Goal state before:
pp: X : TopCat
inst✝ : PathConnectedSpace ↑X
⊢ Nonempty (Unique (ZerothHomotopy ↑X))

Tactic:
rw [unique_iff_subsingleton_and_nonempty]
    constructor <;> infer_instance

Goal state after:
Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy

Goal state before:
pp: X : TopCat
inst✝ : PathConnectedSpace ↑X
⊢ (toSSet.obj X).IsConnected

Tactic:
let : Unique (ZerothHomotopy X) := Nonempty.some (by
    rw [unique_iff_subsingleton_and_nonempty]
    constructor <;> infer_instance)

Goal state after:
X : TopCat
inst✝ : PathConnectedSpace ↑X
this : Unique (ZerothHomotopy ↑X) := ⋯.some
⊢ (toSSet.obj X).IsConnected
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: ⊢ stdSimplex.δ 0 ≫
      (sSetTopAdj.homEquiv Δ[1] TopCat.I)
        (TopCat.isoOfHomeo (⦋1⦌.toTopHomeo.trans (stdSimplexHomeomorphUnitInterval.trans Homeomorph.ulift.symm))).hom =
    SSet.const (TopCat.toSSetObj₀Equiv.symm 1)

Tactic:
← Adjunction.homEquiv_naturality_left,

Goal state after:
⊢ (sSetTopAdj.homEquiv Δ[0] TopCat.I)
      (toTop.map (stdSimplex.δ 0) ≫
        (TopCat.isoOfHomeo (⦋1⦌.toTopHomeo.trans (stdSimplexHomeomorphUnitInterval.trans Homeomorph.ulift.symm))).hom) =
    SSet.const (TopCat.toSSetObj₀Equiv.symm 1)
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) = a
⊢ #α = a

Tactic:
by
  apply le_antisymm
  · apply mk_le_of_countable_eventually_mem ht (fun i ↦ (h'f i).le)
  · obtain ⟨i⟩ : Nonempty ι := nonempty_of_neBot l
    rw [← (h'f i)]
    exact mk_set_le (f i)

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Cardinality

Goal state before:
pp: E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Zero E
inst✝² : MulActionWithZero 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
this : Tendsto (fun n ↦ (c ^ n)⁻¹ • x) atTop (𝓝 (0 • x))
⊢ ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s

Tactic:
rw [zero_smul] at this

Goal state after:
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Zero E
inst✝² : MulActionWithZero 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
this : Tendsto (fun n ↦ (c ^ n)⁻¹ • x) atTop (𝓝 0)
⊢ ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: z : ℂ
m : z ∈ slitPlane
⊢ AnalyticAt ℂ log z

Tactic:
analyticAt_iff_eventually_differentiableAt

Goal state after:
z : ℂ
m : z ∈ slitPlane
⊢ ∀ᶠ (z : ℂ) in 𝓝 z, DifferentiableAt ℂ log z
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ‖ordinaryHypergeometricCoefficient a b c n‖ / ‖ordinaryHypergeometricCoefficient a b c n.succ‖ =
    ‖a + ↑n‖⁻¹ * ‖b + ↑n‖⁻¹ * ‖c + ↑n‖ * ‖1 + ↑n‖

Tactic:
simp only [mul_inv_rev, factorial_succ, cast_mul, cast_add,
    cast_one, ascPochhammer_succ_eval, norm_mul, norm_inv]

Goal state after:
𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ‖↑n !‖⁻¹ * ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖ * ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ *
        ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖⁻¹ /
      (‖↑n !‖⁻¹ * ‖↑n + 1‖⁻¹ * (‖Polynomial.eval a (ascPochhammer 𝕂 n)‖ * ‖a + ↑n‖) *
          (‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ * ‖b + ↑n‖) *
        (‖c + ↑n‖⁻¹ * ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖⁻¹)) =
    ‖a + ↑n‖⁻¹ * ‖b + ↑n‖⁻¹ * ‖c + ↑n‖ * ‖1 + ↑n‖
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | analyticOrderAt f ↑u = ⊤}
x✝¹ : Set ↑U
x✝ : ↑U
| analyticOrderAt f ↑x✝ = ⊤

Tactic:
rw [analyticOrderAt_eq_top, eventually_nhds_iff]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | analyticOrderAt f ↑u = ⊤}
x✝¹ : Set ↑U
x✝ : ↑U
| ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑x✝ ∈ t
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝² : AddCommMonoid R
inst✝¹ : Pow R ℕ
inst✝ : BinomialRing R
r : R
⊢ (ascPochhammer ℕ 0).smeval r = Nat.factorial 0 • r ^ 0

Tactic:
ascPochhammer_zero,

Goal state after:
R : Type u_1
inst✝² : AddCommMonoid R
inst✝¹ : Pow R ℕ
inst✝ : BinomialRing R
r : R
⊢ smeval 1 r = Nat.factorial 0 • r ^ 0
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: ⊢ (ascPochhammer ℕ 0).smeval 0 = (-1) ^ 0 * ↑(Nat.factorial 0)

Tactic:
ascPochhammer_zero,

Goal state after:
⊢ smeval 1 0 = (-1) ^ 0 * ↑(Nat.factorial 0)
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: n : ℕ
⊢ (ascPochhammer ℕ (n + 1)).smeval (-↑(n + 1)) = (-1) ^ (n + 1) * ↑(n + 1).factorial

Tactic:
rw [ascPochhammer_succ_left, smeval_X_mul, smeval_comp, smeval_add, smeval_X, smeval_one,
      pow_zero, pow_one, one_smul, Nat.cast_add, Nat.cast_one, neg_add_rev, neg_add_cancel_comm,
      smeval_ascPochhammer_self_neg n, ← mul_assoc, mul_comm _ ((-1) ^ n),
      show (-1 + -↑n = (-1 : ℤ) * (n + 1)) by lia, ← mul_assoc, pow_add, pow_one,
      Nat.factorial, Nat.cast_mul, ← mul_assoc, Nat.cast_succ]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝¹ : Field R
inst✝ : CharZero R
a : R
n : ℕ
⊢ choose a n = (↑n.factorial)⁻¹ • n.factorial • choose a n

Tactic:
← Nat.cast_smul_eq_nsmul R,

Goal state after:
R : Type u_1
inst✝¹ : Field R
inst✝ : CharZero R
a : R
n : ℕ
⊢ choose a n = (↑n.factorial)⁻¹ • ↑n.factorial • choose a n
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

Goal state before:
pp: case h'
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ AnalyticOn 𝕜 f (s ∩ Metric.eball x r)

Tactic:
apply h.analyticOn.mono
    rw [insert_eq_of_mem hx]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: case e'_5
b : ℝ≥0∞
hb : b < 1
⊢ ⊤ = ⊥ * b.log

Tactic:
EReal.bot_mul_of_neg (log_lt_zero_iff.2 hb)

Goal state after:
case e'_5
b : ℝ≥0∞
hb : b < 1
⊢ ⊤ = ⊤
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
l : Filter α
k : α → β
z : ℕ
⊢ Tendsto (fun a ↦ k a ^ z * 0 a) l (𝓝 0)

Tactic:
simpa only [Pi.zero_apply, mul_zero] using tendsto_const_nhds

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : CommRing β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hf : SuperpolynomialDecay l k f
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
⊢ SuperpolynomialDecay l k g

Tactic:
by
  rw [superpolynomialDecay_iff_abs_tendsto_zero] at hf ⊢
  refine fun z =>
    tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds (hf z)
      (Eventually.of_forall fun x => abs_nonneg _) (hfg.mono fun x hx => ?_)
  calc
    |k x ^ z * g x| = |k x ^ z| * |g x| := abs_mul (k x ^ z) (g x)
    _ ≤ |k x ^ z| * |f x| := by gcongr _ * ?_; exact hx
    _ = |k x ^ z * f x| := (abs_mul (k x ^ z) (f x)).symm

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: v : ℕ → ℕ
h : (linearGrowthInf fun n ↦ ↑(v n)) ≠ 0
⊢ Tendsto v atTop atTop

Tactic:
refine tendsto_atTop.2 fun M ↦ ?_
  have := tendsto_atTop_of_linearGrowthInf_pos (h.lt_of_le' (linearGrowthInf_natCast_nonneg v))
  exact (tendsto_nhds_top_iff_real.1 this M).mono fun n ↦ by exact_mod_cast le_of_lt

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: b : ℝ≥0∞
⊢ limsup (fun n ↦ (b ^ n).log / ↑n) atTop = b.log

Tactic:
← limsup_const (f := atTop (α := ℕ)) (log b)

Goal state after:
b : ℝ≥0∞
⊢ limsup (fun n ↦ (b ^ n).log / ↑n) atTop = limsup (fun x ↦ b.log) atTop
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case pos
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
u_0 : u = ⊥
⊢ linearGrowthInf (u ∘ v) ≤ (linearGrowthSup fun n ↦ ↑(v n)) * linearGrowthInf u

pp: case neg
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
u_0 : ¬u = ⊥
⊢ linearGrowthInf (u ∘ v) ≤ (linearGrowthSup fun n ↦ ↑(v n)) * linearGrowthInf u

Tactic:
· rw [u_0, Pi.bot_comp, linearGrowthInf_bot]; exact bot_le

Goal state after:
case neg
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
u_0 : ¬u = ⊥
⊢ linearGrowthInf (u ∘ v) ≤ (linearGrowthSup fun n ↦ ↑(v n)) * linearGrowthInf u