mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Presentable.StrongGenerator

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
⊢ isCardinalPresentable C κ = P.colimitsCardinalClosure κ

Tactic:
by
  refine le_antisymm ?_ (P.colimitsCardinalClosure_le_isCardinalPresentable hS₂)
  have := hS₁.isDense_colimitsCardinalClosure_ι hS₂
  intro X hX
  rw [isCardinalPresentable_iff] at hX
  rw [← (P.colimitsCardinalClosure κ).retractClosure_eq_self]
  obtain ⟨j, φ, hφ⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ
    ((P.colimitsCardinalClosure κ).ι.denseAt X) (𝟙 X)
  exact ⟨_, j.left.2, ⟨{ i := _, r := _, retract := hφ }⟩⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct

Goal state before:
pp: X₁ Y₁ E✝ B✝ : SSet
i : X₁ ⟶ Y₁
p✝ : E✝ ⟶ B✝
inst✝¹ : Mono i
inst✝ : InnerFibration p✝
sq₁₃ : internalHom.PullbackObjObj i p✝
X✝ Y✝ : SSet
g✝ : X✝ ⟶ Y✝
n✝ : ℕ
k : Fin (n✝ + 3)
h0 : 0 < k
hn : k < Fin.last (n✝ + 2)
sq₁₂ : (curriedTensor SSet).PushoutObjObj i Λ[n✝ + 2, k].ι :=
  Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) i Λ[n✝ + 2, k].ι
E B : SSet
p : E ⟶ B
hp : innerFibrations p
sq₁₃' : internalHom.PullbackObjObj Λ[n✝ + 2, k].ι p := Functor.PullbackObjObj.ofHasPullback internalHom Λ[n✝ + 2, k].ι p
X Y : SSet
n : ℕ
⊢ HasLiftingProperty (Λ[n✝ + 2, k].unionProd ∂Δ[n]).ι p

Tactic:
exact prodStdSimplex.innerAnodyneExtensions_unionProd_ι k h0 hn n _ hp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasPushouts C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ : Arrow C
W : C
inst✝³ : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.left)
inst✝² : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.right)
inst✝¹ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.left)
inst✝ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.right)
⊢ ((curriedTensor C).map (Arrow.mk (X₁.right ◁ X₂.hom)).hom).app X₃.left ≫
      pushout.inl (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
        (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom) =
    ((curriedTensor C).obj (Arrow.mk (X₁.right ◁ X₂.hom)).left).map X₃.hom ≫
      pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ▷ X₃.right ≫
        pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
          (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom)

Tactic:
by simp [Limits.pushout.associator_inv_naturality_right_condition]

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

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin m
n : ℕ
s : Type₁ k.succ n
h : (pairingCore k.succ n).index s = 0
this✝ : s.index = 0
hs : IsIndex s.x ⋯ (Fin.succ 0)
i : Fin ((s.x.cast ⋯).dim + 1)
hi : (s.x.cast ⋯).simplex.1 i = 0
this : (fun j ↦ (s.x.cast ⋯).simplex.1 j) 0 ≤ (fun j ↦ (s.x.cast ⋯).simplex.1 j) i
h₁ : (s.x.cast ⋯).simplex.1 (Fin.castSucc 0) = k.succ.castSucc
⊢ False

Tactic:
dsimp only [Fin.castSucc_zero] at h₁

Goal state after:
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin m
n : ℕ
s : Type₁ k.succ n
h : (pairingCore k.succ n).index s = 0
this✝ : s.index = 0
hs : IsIndex s.x ⋯ (Fin.succ 0)
i : Fin ((s.x.cast ⋯).dim + 1)
hi : (s.x.cast ⋯).simplex.1 i = 0
this : (fun j ↦ (s.x.cast ⋯).simplex.1 j) 0 ≤ (fun j ↦ (s.x.cast ⋯).simplex.1 j) i
h₁ : (s.x.cast ⋯).simplex.1 0 = k.succ.castSucc
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
⊢ (↾fun x ↦
        (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1⦌)))
          ↑(prodStdSimplex.nonDegenerateEquiv₁ j)) ≫
      σ Y i.castSucc =
    σ X i ≫
      ↾fun x ↦
        (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1 + 1⦌)))
          ↑(prodStdSimplex.nonDegenerateEquiv₁ j.succ)

Tactic:
ext x
    simp only [TypeCat.Fun.toFun_apply, types_comp_apply, TypeCat.hom_ofHom, TypeCat.Fun.coe_mk,
      ← SSet.σ_naturality_apply]
    dsimp
    apply congr_arg
    ext k : 2
    · simp [SimplexCategory.σ_comp_σ hij, SSet.yonedaEquiv_symm_app_objEquiv_symm.{u}]
      rfl
    · rw [stdSimplex.σ_objMk₁_of_lt _ _ (by simpa)]

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 : g.op.MulStruct f.op fg.op i
j : Fin n
hij : i.rev = j
⊢ stdSimplex.δ j.castSucc.castSucc ≫ yonedaEquiv.symm (opObjEquiv (yonedaEquiv h.map)) = g.map

Tactic:
by
    simp [stdSimplex.δ_comp_yonedaEquiv_symm, δ_opObjEquiv,
      ← stdSimplex.yonedaEquiv_δ_comp, ← hij, Fin.rev_castSucc]

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : MulStruct RelativeMorphism.const f g i
j : Fin (n + 2)
hj : i.castSucc.succ < j
⊢ stdSimplex.δ j ≫ h.map = const x

Tactic:
rw [Fin.succ_castSucc, Fin.castSucc_lt_iff_succ_le] at hj

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : MulStruct RelativeMorphism.const f g i
j : Fin (n + 2)
hj : i.succ.succ ≤ j
⊢ stdSimplex.δ j ≫ h.map = const x
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: 𝕜 : 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
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
z : E
hz : z ∈ closedBall b ε
hgz : g z ∈ closedBall b ε
v : E := f'symm.toFun (y - f z)
⊢ ↑c * ‖z + v - z‖ ≤ ↑c * (↑f'symm.nnnorm * dist (f z) y)

Tactic:
gcongr
        simpa [dist_eq_norm'] using f'symm.bound (y - f z)

Goal state after:
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 : ∃ t, (∀ y ∈ t, g y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ z₀ ∈ t
⊢ ∃ t, (∀ y ∈ t, (f • g) y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ z₀ ∈ t

Tactic:
obtain ⟨t, h₁t, h₂t, h₃t⟩ := hg

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
t : Set 𝕜
h₁t : ∀ y ∈ t, g y = 0
h₂t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
h₃t : z₀ ∈ t
⊢ ∃ t, (∀ y ∈ t, (f • g) y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ z₀ ∈ t
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst✝¹ : CompleteSpace E
inst✝ : CharZero 𝕜
s : ℕ
hrne : s + 1 ≠ 0
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (s + 1) • F z + f x
U : Set 𝕜
hUf : ∀ y ∈ U, f y = (y - x) ^ (s + 1) • F y + f x ∧ AnalyticAt 𝕜 F y
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hUx : x ∈ U
this : ∀ y ∈ U, deriv f y = (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y
y : 𝕜
⊢ (s + 1) • (y - x) ^ s • F y = (y - x) ^ s • (fun z ↦ ↑(s + 1) • F z) y

Tactic:
· simpa only [Nat.cast_smul_eq_nsmul] using smul_comm ..

Goal state after:
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: 𝕜 : 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
f' : E ≃L[𝕜] F
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑f'.symm‖₊⁻¹
⊢ ↑c < ↑‖↑f'.symm‖₊⁻¹

Tactic:
exact hc

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
z₀ : 𝕜
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
hzero : f z₀ = 0
⊢ analyticOrderAt (deriv f) z₀ = ⊤ ↔ analyticOrderAt f z₀ = ⊤

Tactic:
simp_rw [ENat.eq_top_iff_forall_ge, analyticOrderAt_deriv_ge_iff hf hzero]
  exact ⟨fun h m ↦ le_self_add.trans (h m), fun h m ↦ h (m + 1)⟩

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

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬EventuallyConst g (𝓝 z₀)
hf' : analyticOrderAt f (g z₀) = ⊤
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (fun x ↦ g x - g z₀) z₀

Tactic:
rw [hf', analyticOrderAt_eq_top.mpr
      (EventuallyEq.comp_tendsto (analyticOrderAt_eq_top.mp hf') hg.continuousAt), ENat.top_mul]
    rw [AnalyticAt.analyticOrderAt_ne_zero (by fun_prop), sub_eq_zero]

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

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬EventuallyConst g (𝓝 z₀)
hf' : analyticOrderAt f (g z₀) = ⊤
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (fun x ↦ g x - g z₀) z₀

pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬EventuallyConst g (𝓝 z₀)
hf' : ¬analyticOrderAt f (g z₀) = ⊤
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (fun x ↦ g x - g z₀) z₀

Tactic:
· -- If `f` is eventually constant but `g` is not, we have `⊤ = ⊤ * (non-zero thing)`
    rw [hf', analyticOrderAt_eq_top.mpr
      (EventuallyEq.comp_tendsto (analyticOrderAt_eq_top.mp hf') hg.continuousAt), ENat.top_mul]
    rw [AnalyticAt.analyticOrderAt_ne_zero (by fun_prop), sub_eq_zero]

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬EventuallyConst g (𝓝 z₀)
hf' : ¬analyticOrderAt f (g z₀) = ⊤
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (fun x ↦ g x - g z₀) z₀
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
this : Tendsto (fun k ↦ (a + ↑k)⁻¹ * (b + ↑k)⁻¹ * (c + ↑k) * (1 + ↑k)) atTop (𝓝 1)
⊢ 1 = ‖1‖

Tactic:
exact norm_one.symm

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

Goal state before:
pp: case neg
𝕜 : 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 = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
h₁w : ¬w = z
⊢ ¬analyticOrderAt f ↑w = ⊤

Tactic:
rw [(hf _ w.2).analyticOrderAt_eq_zero.2 ((h₁t' w hw) (Subtype.coe_ne_coe.mpr h₁w))]
          exact ENat.zero_ne_top

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : Ring R
inst✝⁴ : Ring S
inst✝³ : BinomialRing R
inst✝² : BinomialRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
a : R
n : ℕ
⊢ f (multichoose a n) = multichoose (f a) n

Tactic:
by
  apply nsmul_right_injective n.factorial_ne_zero
  simp only [← map_nsmul, Ring.factorial_nsmul_multichoose_eq_ascPochhammer,
    ← Polynomial.eval₂_smulOneHom_eq_smeval, Polynomial.hom_eval₂, ← RingHom.coe_coe f]
  congr
  exact Subsingleton.elim _ _

Goal state after:
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)
⊢ (descPochhammer ℤ (n + 1)).smeval r = (ascPochhammer ℕ (n + 1)).smeval (r - ↑(n + 1) + 1)

Tactic:
rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right, smeval_mul, ih,
      ascPochhammer_succ_left, X_mul, smeval_mul_X, smeval_comp, smeval_sub, ← C_eq_natCast,
      smeval_add, smeval_one, smeval_C]

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.smeval r - ↑n • r ^ 0) =
    (ascPochhammer ℕ n).smeval (X.smeval (r - ↑n) + 1 • (r - ↑n) ^ 0) * (r - ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y ↦ ↑y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) (-x)
⊢ HasDerivAt (fun y ↦ ↑(-y) ^ (r + 1)) (-(r + 1) * ↑(-x) ^ r) x

Tactic:
convert! @HasDerivAt.scomp ℝ _ ℂ _ _ x ℝ _ _ _ _ _ _ _ _ this (hasDerivAt_neg x) using 1
      rw [real_smul, ofReal_neg 1, ofReal_one]; ring

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Ring R
r s : R
h : Commute r s
k : ℕ
ih :
  (descPochhammer ℤ k).smeval (r + s) =
    ∑ ij ∈ antidiagonal k, ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)
⊢ (descPochhammer ℤ (k + 1)).smeval (r + s) =
    ∑ ij ∈ antidiagonal (k + 1),
      ↑((k + 1).choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)

Tactic:
rw [descPochhammer_succ_right, mul_comm, smeval_mul, sum_antidiagonal_choose_succ_mul
      fun i j => ((descPochhammer ℤ i).smeval r * (descPochhammer ℤ j).smeval s),
      ← sum_add_distrib, smeval_sub, smeval_X, smeval_natCast, pow_zero, pow_one, ih, mul_sum]

Goal state after:
case succ
R : Type u_1
inst✝ : Ring R
r s : R
h : Commute r s
k : ℕ
ih :
  (descPochhammer ℤ k).smeval (r + s) =
    ∑ ij ∈ antidiagonal k, ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)
⊢ ∑ i ∈ antidiagonal k,
      (r + s - k • 1) * (↑(k.choose i.1) * ((descPochhammer ℤ i.1).smeval r * (descPochhammer ℤ i.2).smeval s)) =
    ∑ x ∈ antidiagonal k,
      (↑(k.choose x.1) * ((descPochhammer ℤ x.1).smeval r * (descPochhammer ℤ (x.2 + 1)).smeval s) +
        ↑(k.choose x.2) * ((descPochhammer ℤ (x.1 + 1)).smeval r * (descPochhammer ℤ x.2).smeval s))
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: p : ℝ
h : ↑0 ≤ p
x : ℝ
⊢ 0 ≤ p

Tactic:
simpa using h

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

Goal state before:
pp: f g : ℝ → ℝ
f' g' x : ℝ
hf : HasDerivWithinAt f f' Set.univ x
hg : HasDerivWithinAt g g' Set.univ x
h : 0 < f x
⊢ HasDerivWithinAt (fun x ↦ f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) Set.univ x

Tactic:
exact hf.rpow hg h

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

Goal state before:
pp: case bot
⊢ ∃ a, a.log = ⊥

Tactic:
| bot =>

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

Goal state before:
pp: b : ℝ≥0∞
hb : 1 < b
⊢ Filter.Tendsto (fun x ↦ ↑x * b.log) Filter.atTop (𝓝 ⊤)

Tactic:
convert! EReal.Tendsto.mul_const tendsto_coe_atTop _ _

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

case convert_2
b : ℝ≥0∞
hb : 1 < b
⊢ ⊤ ≠ 0 ∨ b.log ≠ ⊥

case convert_3
b : ℝ≥0∞
hb : 1 < b
⊢ ⊤ ≠ 0 ∨ b.log ≠ ⊤
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: b : ℝ≥0∞
hb : b < 1
⊢ Filter.Tendsto (fun x ↦ ↑x * b.log) Filter.atTop (𝓝 ⊥)

Tactic:
convert! EReal.Tendsto.mul_const tendsto_coe_atTop _ _

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

case convert_2
b : ℝ≥0∞
hb : b < 1
⊢ ⊤ ≠ 0 ∨ b.log ≠ ⊥

case convert_3
b : ℝ≥0∞
hb : b < 1
⊢ ⊤ ≠ 0 ∨ b.log ≠ ⊤
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

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

Tactic:
EReal.bot_mul_of_pos (zero_lt_log_iff.2 hb)

Goal state after:
case e'_5
b : ℝ≥0∞
hb : 1 < b
⊢ ⊥ = ⊥
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

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

Tactic:
rw [EReal.bot_mul_of_neg (log_lt_zero_iff.2 hb)]

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

Goal state before:
pp: u v : ℕ → EReal
h : linearGrowthSup u ≠ ⊥ ∨ linearGrowthInf v ≠ ⊤
h' : linearGrowthSup u ≠ ⊤ ∨ linearGrowthInf v ≠ ⊥
⊢ linearGrowthInf (u + v) ≤ linearGrowthSup u + linearGrowthInf v

Tactic:
refine (liminf_add_le h h').trans_eq' (liminf_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.LinearGrowth

Goal state before:
pp: case inr
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ (linearGrowthInf v + linearGrowthSup fun x ↦ b) = linearGrowthInf v

Tactic:
rw [linearGrowthSup_const b_bot.ne' hb]

Goal state after:
case inr
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v + 0 = linearGrowthInf v
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v ≠ ⊥ ∨ (linearGrowthSup fun x ↦ b) ≠ ⊤

Tactic:
rw [linearGrowthSup_const b_bot.ne' hb]

Goal state after:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v ≠ ⊥ ∨ 0 ≠ ⊤
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v ≠ ⊤ ∨ (linearGrowthSup fun x ↦ b) ≠ ⊥

Tactic:
rw [linearGrowthSup_const b_bot.ne' hb]

Goal state after:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v ≠ ⊤ ∨ 0 ≠ ⊥
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case inr
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ (linearGrowthSup v + linearGrowthSup fun x ↦ b) = linearGrowthSup v

Tactic:
rw [linearGrowthSup_const b_bot.ne' hb]

Goal state after:
case inr
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthSup v + 0 = linearGrowthSup v
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthSup v ≠ ⊥ ∨ (linearGrowthSup fun x ↦ b) ≠ ⊤

Tactic:
rw [linearGrowthSup_const b_bot.ne' hb]

Goal state after:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthSup v ≠ ⊥ ∨ 0 ≠ ⊤
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthSup v ≠ ⊤ ∨ (linearGrowthSup fun x ↦ b) ≠ ⊥

Tactic:
rw [linearGrowthSup_const b_bot.ne' hb]

Goal state after:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthSup v ≠ ⊤ ∨ 0 ≠ ⊥
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: case pos
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
a'_ne_u : a' ∉ u
c : ι
ct : c ∈ t
b : ι
ba'u : b ∈ insert a' u
hcb : (B c ∩ B b).Nonempty
H : ∃ d ∈ u, (B c ∩ B d).Nonempty
⊢ ∃ c_1 ∈ insert a' u, (B c ∩ B c_1).Nonempty ∧ δ c ≤ τ * δ c_1

Tactic:
rcases H with ⟨d, du, hd⟩
      rcases hu.prop.2.2 c ct d du hd with ⟨d', d'u, hd'⟩
      exact ⟨d', mem_insert_of_mem _ d'u, hd'⟩

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: α : 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 ↦ ball (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (ball (x a) (r a) ∩ ball (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : (ball (x a) (r a) ∩ ball (x b) (r b)).Nonempty
rb : r a ≤ (τ - 1) / 2 * r b
this : dist (x a) (x b) < r a + r b
⊢ ball (x a) (r a) ⊆ ball (x b) (τ * r b)

Tactic:
apply ball_subset_ball'

Goal state after:
α : 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 ι := ⋯
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint fun a ↦ ball (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (ball (x a) (r a) ∩ ball (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : (ball (x a) (r a) ∩ ball (x b) (r b)).Nonempty
rb : r a ≤ (τ - 1) / 2 * r b
this : dist (x a) (x b) < r a + r b
⊢ r a + dist (x a) (x b) ≤ τ * r b
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ∞
hf : IntegrableOn f s μ
⊢ 0 < μ {x | x ∈ s ∧ f x ≤ ⨍ (a : α) in s, f a ∂μ}

Tactic:
refine pos_iff_ne_zero.2 fun H => ?_

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ∞
hf : IntegrableOn f s μ
H : μ {x | x ∈ s ∧ f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0
⊢ False
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ∞
hf : IntegrableOn f s μ
H : (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0
this : Fact (μ s < ∞)
⊢ 0 ≤ᵐ[μ.restrict s] fun x ↦ f x - ⨍ (a : α) in s, f a ∂μ

Tactic:
refine measure_mono_null (fun x hx ↦ ?_) H
    simp only [Pi.zero_apply, sub_nonneg, mem_compl_iff, mem_ofPred_eq, not_le] at hx
    exact hx.le

Goal state after: