mathlib-initiative/mathlib-tactics huggingface dataset:
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 ι
j : ι
c : f.Cell j
i : ι
h : j < i
⊢ (↑(P.p c.s)).subcomplex ≤ f.filtration i

Tactic:
refine le_trans ?_ le_sup_right
  refine le_trans ?_ (le_iSup _ j)
  refine le_trans ?_ (le_iSup _ h)
  exact le_trans (by rfl) (le_iSup _ c)

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

Goal state before:
pp: case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
s : X.N
⊢ s.subcomplex ≤ c.horn.image c.map → s.subcomplex ≤ f.filtration j

Tactic:
hs

Goal state after:
case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
s : X.N
hs : s.subcomplex ≤ c.horn.image c.map
⊢ s.subcomplex ≤ f.filtration j
Module: Mathlib.CategoryTheory.Presentable.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
H :
  ∀ {k k' : K} (φ : k ⟶ k'),
    ∃ j f,
      (ConcreteCategory.hom ((X ⋙ F.obj k').map f)) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
        (ConcreteCategory.hom ((X ⋙ F.obj k').map f)) (z k')
j : {k k' : K} → (k ⟶ k') → J := fun {k k'} φ ↦ ⋯.choose
g : {k k' : K} → (φ : k ⟶ k') → j₀ ⟶ j φ := fun {k k'} φ ↦ ⋯.choose
hg :
  ∀ {k k' : K} (φ : k ⟶ k'),
    (ConcreteCategory.hom ((F.obj k').map (X.map (g φ)))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
      (ConcreteCategory.hom ((F.obj k').map (X.map (g φ)))) (z k')
j'' : Arrow K → J := fun f ↦ j f.hom
ψ : Arrow K → (j₀ ⟶ IsCardinalFiltered.max j'' hK) := fun f ↦ g f.hom ≫ IsCardinalFiltered.toMax j'' hK f
k k' : K
φ : k ⟶ k'
⊢ IsCardinalFiltered.toCoeq ψ hK =
    g φ ≫ (fun k k' φ ↦ IsCardinalFiltered.toMax j'' hK (Arrow.mk φ) ≫ IsCardinalFiltered.coeqHom ψ hK) k k' φ

Tactic:
simpa [ψ] using! (IsCardinalFiltered.coeq_condition ψ hK (Arrow.mk φ)).symm

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
H :
  ∀ {k k' : K} (φ : k ⟶ k'),
    ∃ j f,
      (ConcreteCategory.hom ((X ⋙ F.obj k').map f)) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
        (ConcreteCategory.hom ((X ⋙ F.obj k').map f)) (z k')
j : {k k' : K} → (k ⟶ k') → J := fun {k k'} φ ↦ ⋯.choose
g : {k k' : K} → (φ : k ⟶ k') → j₀ ⟶ j φ := fun {k k'} φ ↦ ⋯.choose
hg :
  ∀ {k k' : K} (φ : k ⟶ k'),
    (ConcreteCategory.hom ((F.obj k').map (X.map (g φ)))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
      (ConcreteCategory.hom ((F.obj k').map (X.map (g φ)))) (z k')
j₁ : J
α : j₀ ⟶ j₁
β : ⦃k k' : K⦄ → (φ : k ⟶ k') → j φ ⟶ j₁
hα : ∀ ⦃k k' : K⦄ (φ : k ⟶ k'), α = g φ ≫ β φ
k k' : K
φ : k ⟶ k'
⊢ (ConcreteCategory.hom ((F.obj k').map (X.map α))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
    (ConcreteCategory.hom ((F.obj k').map (X.map α))) (z k')

Tactic:
by simp [hα φ, hg]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
j₁ : J
α : j₀ ⟶ j₁
hα :
  ∀ ⦃k k' : K⦄ (φ : k ⟶ k'),
    (ConcreteCategory.hom ((F.obj k').map (X.map α))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
      (ConcreteCategory.hom ((F.obj k').map (X.map α))) (z k')
s : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j₁)).sections := ⋯
⊢ (Types.isLimitEquivSections (hc cX.pt)) x =
    (Types.isLimitEquivSections (hc cX.pt))
      ((ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app j₁)) ((Types.isLimitEquivSections (hc (X.obj j₁))).symm s))

Tactic:
← hy,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
j₁ : J
α : j₀ ⟶ j₁
hα :
  ∀ ⦃k k' : K⦄ (φ : k ⟶ k'),
    (ConcreteCategory.hom ((F.obj k').map (X.map α))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
      (ConcreteCategory.hom ((F.obj k').map (X.map α))) (z k')
s : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j₁)).sections :=
  ⟨fun k ↦ (ConcreteCategory.hom ((F.obj k).map (X.map α))) (z k), ⋯⟩
⊢ (Types.isLimitEquivSections (hc cX.pt)) ((Types.isLimitEquivSections (hc cX.pt)).symm y) =
    (Types.isLimitEquivSections (hc cX.pt))
      ((ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app j₁)) ((Types.isLimitEquivSections (hc (X.obj j₁))).symm s))
Module: Mathlib.AlgebraicTopology.SimplicialSet.PushoutProduct

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ ⋯.isoPushout.hom ≫ (Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) (Arrow.mk S.ι).hom (Arrow.mk T.ι).hom).ι =
    (S.unionProd T).ι ≫ (Iso.refl (X ⊗ Y)).hom

Tactic:
apply (unionProd.isPushout S T).hom_ext

Goal state after:
case h₀
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ ι₁ S T ≫
      ⋯.isoPushout.hom ≫
        (Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) (Arrow.mk S.ι).hom (Arrow.mk T.ι).hom).ι =
    ι₁ S T ≫ (S.unionProd T).ι ≫ (Iso.refl (X ⊗ Y)).hom

case h₁
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ ι₂ S T ≫
      ⋯.isoPushout.hom ≫
        (Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) (Arrow.mk S.ι).hom (Arrow.mk T.ι).hom).ι =
    ι₂ S T ≫ (S.unionProd T).ι ≫ (Iso.refl (X ⊗ Y)).hom
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case inl.inr
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin d
hi✝ : i.succ ≤ min x hd
hi : i.succ = min x hd
⊢ (objEquiv (x.cast hd).simplex) i.castSucc < φ x hd i.castSucc.succ

Tactic:
rw [← Fin.castSucc_succ, hi, φ_castSucc]
      refine lt_of_le_of_ne ⟨?_, ?_⟩ ?_
      · dsimp
        rw [simplex_fst_le_castSucc_iff]
        grind
      · exact stdSimplex.monotone_apply _
          (by dsimp; rw [← hi]; exact Fin.castSucc_le_succ i)
      · intro h
        rw [Prod.ext_iff] at h
        dsimp at h
        obtain ⟨h₁, h₂⟩ := h
        apply hx _ hd i.succ
        rw [isIndex_succ]
        refine ⟨h₁, ?_, by aesop⟩
        have := φ_succAbove x hd (min x hd)
        rw [Fin.succAbove_castSucc_self] at this
        rw [← φ_succ_fst x hd, this, hi]
        dsimp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ j.castSucc.succ.rev ≫ h.map))) =
    yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ i.castSucc.succ ≫ h.map)))

Tactic:
Fin.rev_succ,

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ j.castSucc.rev.castSucc ≫ h.map))) =
    yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ i.castSucc.succ ≫ h.map)))
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ j.succ.succ.rev ≫ h.map))) =
    yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ i.castSucc.castSucc ≫ h.map)))

Tactic:
Fin.rev_succ,

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ j.succ.rev.castSucc ≫ h.map))) =
    yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ i.castSucc.castSucc ≫ h.map)))
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ j.succ.rev.castSucc ≫ h.map))) =
    yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ i.castSucc.castSucc ≫ h.map)))

Tactic:
Fin.rev_succ,

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ j.rev.castSucc.castSucc ≫ h.map))) =
    yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ i.castSucc.castSucc ≫ h.map)))
Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy

Goal state before:
pp: X : TopCat
x : ZerothHomotopy ↑X
⊢ SSet.π₀.lift (ZerothHomotopy.mk ∘ ⇑toSSetObj₀Equiv) ⋯ (ZerothHomotopy.lift (SSet.π₀.mk ∘ ⇑toSSetObj₀Equiv.symm) ⋯ x) =
    x

Tactic:
induction x; simp

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

Goal state before:
pp: X : TopCat
x : (toSSet.obj X).π₀
⊢ ZerothHomotopy.lift (SSet.π₀.mk ∘ ⇑toSSetObj₀Equiv.symm) ⋯ (SSet.π₀.lift (ZerothHomotopy.mk ∘ ⇑toSSetObj₀Equiv) ⋯ x) =
    x

Tactic:
induction x; simp

Goal state after:
Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hr : 0 < (FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial).radius
⊢ AnalyticOn 𝕜 f
      (Metric.eball x (FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial).radius) →
    HasFPowerSeriesOnBall f (FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial) x
      (FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial).radius

Tactic:
hs

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hr : 0 < (FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial).radius
hs :
  AnalyticOn 𝕜 f
    (Metric.eball x (FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial).radius)
⊢ HasFPowerSeriesOnBall f (FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial) x
    (FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial).radius
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hg : analyticOrderAt g z₀ = ⊤
⊢ analyticOrderAt (f • g) z₀ = ⊤

Tactic:
by
  rw [analyticOrderAt_eq_top, eventually_nhds_iff] at *
  obtain ⟨t, h₁t, h₂t, h₃t⟩ := hg
  exact ⟨t, fun y hy ↦ by simp [h₁t y hy], h₂t, h₃t⟩

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: case convert_7
this :
  (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n) =
    FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n log 1 / ↑n.factorial
⊢ AnalyticAt ℂ log 1

Tactic:
exact analyticAt_clog (by simp)

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
n : ℕ
h : AnalyticAt 𝕜 (fun z ↦ (z - z₀) ^ n • f z) z₀
h₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, (z - z₀) ^ n • f z ≠ 0
⊢ (∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0

Tactic:
right
    filter_upwards [h₂, self_mem_nhdsWithin] with y h₁y h₂y
    exact (smul_ne_zero_iff.1 h₁y).2

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ r * (ascPochhammer ℕ k).smeval (r + 1) +
      (↑k • (ascPochhammer ℕ k).smeval (r + 1) + 1 * (ascPochhammer ℕ k).smeval (r + 1)) =
    k.succ • (ascPochhammer ℕ k).smeval (r + 1) + r * (ascPochhammer ℕ k).smeval (r + 1)

Tactic:
@add_rotate',

Goal state after:
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ ↑k • (ascPochhammer ℕ k).smeval (r + 1) +
      (1 * (ascPochhammer ℕ k).smeval (r + 1) + r * (ascPochhammer ℕ k).smeval (r + 1)) =
    k.succ • (ascPochhammer ℕ k).smeval (r + 1) + r * (ascPochhammer ℕ k).smeval (r + 1)
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case succ
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
n : ℕ
ih : (descPochhammer ℤ n).smeval r = (ascPochhammer ℕ n).smeval (r - ↑n + 1)
⊢ (ascPochhammer ℕ n).smeval (r - ↑n + 1) * (X - ↑n).smeval r = ((ascPochhammer ℕ n).comp (X + 1) * X).smeval (r - ↑n)

Tactic:
smeval_mul_X,

Goal state after:
case succ
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
n : ℕ
ih : (descPochhammer ℤ n).smeval r = (ascPochhammer ℕ n).smeval (r - ↑n + 1)
⊢ (ascPochhammer ℕ n).smeval (r - ↑n + 1) * (X - ↑n).smeval r =
    ((ascPochhammer ℕ n).comp (X + 1)).smeval (r - ↑n) * (r - ↑n)
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h₂ : EqOn f g Uᶜ
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x | f x = g x})ᶜ ∈ 𝓝[≠] x
a : 𝕜
ha : a ∈ (U \ {x | f x = g x})ᶜ
⊢ f a = g a

Tactic:
simp at ha

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h₂ : EqOn f g Uᶜ
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x | f x = g x})ᶜ ∈ 𝓝[≠] x
a : 𝕜
ha : a ∈ U → f a = g a
⊢ f a = g a
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
f' g' : StrongDual ℂ E
x : E
hf : HasFDerivAt f f' x
hg : HasFDerivAt g g' x
h0 : f x ∈ slitPlane
⊢ HasFDerivAt (fun x ↦ f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') x

Tactic:
by
  convert! (@Complex.hasFDerivAt_cpow ((fun x => (f x, g x)) x) h0).comp x (hf.prodMk hg)

Goal state after:
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: 𝕂 : Type u
inst✝⁵ : Field 𝕂
inst✝⁴ : CharZero 𝕂
𝔸 : Type v
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b : 𝕂
h : ∀ (k : ℕ), ↑k ≠ -b
n : ℕ
⊢ Ring.choose a n = (-1) ^ n * ordinaryHypergeometricCoefficient (-a) b b n

Tactic:
ordinaryHypergeometricCoefficient,

Goal state after:
𝕂 : Type u
inst✝⁵ : Field 𝕂
inst✝⁴ : CharZero 𝕂
𝔸 : Type v
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b : 𝕂
h : ∀ (k : ℕ), ↑k ≠ -b
n : ℕ
⊢ Ring.choose a n =
    (-1) ^ n *
      ((↑n !)⁻¹ * Polynomial.eval (-a) (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval b (ascPochhammer 𝕂 n))⁻¹)
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case refine_2
w x : ℂ
hw : w ≠ x
⊢ HasFPowerSeriesOnBall (fun z ↦ 1 / w ^ 2) (FormalMultilinearSeries.ofScalars ℂ fun i ↦ Nat.casesOn i (w ^ (-2)) 0) x
    ‖w - x‖ₑ

Tactic:
convert! hasFPowerSeriesOnBall_const.mono _ le_top
    · ext (_ | _) <;> simp [zpow_ofNat]
    · simpa [sub_eq_zero]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case succ
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x ↦ x ^ p
p : ℝ
h : ↑n ≤ p - 1
h1 : 1 ≤ p
⊢ (Differentiable ℝ fun x ↦ x ^ p) ∧
    (↑n = ⊤ → AnalyticOn ℝ (fun x ↦ x ^ p) Set.univ) ∧ ContDiff ℝ ↑n fun x ↦ p * x ^ (p - 1)

Tactic:
simp only [WithTop.natCast_ne_top, analyticOn_univ, IsEmpty.forall_iff, true_and]

Goal state after:
case succ
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x ↦ x ^ p
p : ℝ
h : ↑n ≤ p - 1
h1 : 1 ≤ p
⊢ (Differentiable ℝ fun x ↦ x ^ p) ∧ ContDiff ℝ ↑n fun x ↦ p * x ^ (p - 1)
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
⊢ linearGrowthSup u + linearGrowthInf v ≤ linearGrowthSup (u + v)

Tactic:
refine le_limsup_add.trans_eq (limsup_congr (Eventually.of_forall fun n ↦ ?_))
  rw [Pi.add_apply, Pi.add_apply, add_div_of_nonneg_right n.cast_nonneg']

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

Goal state before:
pp: u : ℕ → ℝ≥0∞
a : EReal
⊢ expGrowthInf u ≤ a ↔ ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ (b * ↑n).exp

Tactic:
rw [expGrowthInf, liminf_le_iff']

Goal state after:
u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y > a, ∃ᶠ (a : ℕ) in atTop, (u a).log / ↑a ≤ y) ↔ ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ (b * ↑n).exp
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝³ : NormedField β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
⊢ f =O[l] fun a ↦ k a ^ z

Tactic:
refine isBigO_of_div_tendsto_nhds (hk0.mono fun x hx hxz ↦ absurd hxz (zpow_ne_zero _ hx)) 0 ?_

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝³ : NormedField β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
⊢ Tendsto (f / fun a ↦ k a ^ z) l (𝓝 0)
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: b : ℝ≥0∞
n : ℕ
n_1 : 1 ≤ n
⊢ (b ^ n).log / ↑n = b.log

Tactic:
rw [EReal.div_eq_iff (natCast_ne_bot n) (natCast_ne_top n)
    (zero_lt_one.trans_le (Nat.one_le_cast.2 n_1)).ne.symm, log_pow, mul_comm]

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEMeasurableOrder

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p ↦ ⋂ q ∈ s ∩ Ioi p, u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x ↦ ⨅ i, (u' ↑i).piecewise (fun x ↦ ↑i) (fun x ↦ ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ p, ⋃ q, u' ↑p ∩ v ↑p ↑q
μt : μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, x ∉ t
x : α
hx : x ∉ t
q : β
⊢ f x < q → ∃ i, (u' ↑i).piecewise (fun x ↦ ↑i) (fun x ↦ ⊤) x < q

Tactic:
hq

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p ↦ ⋂ q ∈ s ∩ Ioi p, u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x ↦ ⨅ i, (u' ↑i).piecewise (fun x ↦ ↑i) (fun x ↦ ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ p, ⋃ q, u' ↑p ∩ v ↑p ↑q
μt : μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, x ∉ t
x : α
hx : x ∉ t
q : β
hq : f x < q
⊢ ∃ i, (u' ↑i).piecewise (fun x ↦ ↑i) (fun x ↦ ⊤) x < q
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case neg
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun n ↦ ↑(v n) / ↑n) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : 0 < liminf (fun n ↦ ↑(v n) / ↑n) atTop
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
h' : ∀ᶠ (x : ℕ) in atTop, 0 < u x
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf u

Tactic:
replace h' := h'.mono fun _ hn ↦ hn.le

Goal state after:
case neg
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun n ↦ ↑(v n) / ↑n) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : 0 < liminf (fun n ↦ ↑(v n) / ↑n) atTop
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
h' : ∀ᶠ (x : ℕ) in atTop, 0 ≤ u x
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf u
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: case neg.inr
α : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h✝ : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint fun a ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
A : ∀ a ∈ t', ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
a : ι
ha : a ∈ t
h'a : r a < 0
⊢ ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Tactic:
· rcases ht with ⟨b, rb⟩
    rcases A b ⟨rb.1, rb.2⟩ with ⟨c, cu, _⟩
    exact ⟨c, cu, by simp only [closedBall_eq_empty.2 h'a, empty_subset]⟩

Goal state after: