mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
⊢ ∀ (f : X✝ ⟶ Y✝), generators.multiplicativeClosure' f → P f

Tactic:
f

Goal state after:
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f✝ : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
⊢ generators.multiplicativeClosure' f → P f
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: case mk
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
b : SimplexCategory
hb : b.len ≤ d
a : ℕ
ha : { len := a }.len ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := b, property := hb }
⊢ W f

Tactic:
induction b using SimplexCategory.rec with

Goal state after:
case mk.mk
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
a : ℕ
ha : { len := a }.len ≤ d
b : ℕ
hb : { len := b }.len ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
⊢ W f
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : LE α
⊢ (IsRelUpperSet s fun x ↦ True) ↔ IsUpperSet s

Tactic:
by
  grind [IsUpperSet, IsRelUpperSet]

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

Goal state before:
pp: X Y : SSet
T : Type u_1
inst✝ : PartialOrder T
⊢ ∀ {n : ℕ} (x : ↑((nerve T).nonDegenerate n)), Mono (yonedaEquiv.symm ↑x)

Tactic:
by
    intro n ⟨x, hx⟩
    rw [PartialOrder.mem_nerve_nonDegenerate_iff_injective] at hx
    simp only [NatTrans.mono_iff_mono_app, mono_iff_injective]
    intro ⟨⟨k⟩⟩ i j hij
    ext l : 1
    exact hx (Functor.congr_obj hij l)

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

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n + 1⦌
hx : x ∈ X.nonDegenerate (n + 1)
i j : Fin (n + 2)
hij : (ConcreteCategory.hom (SimplicialObject.δ X i)) x = (ConcreteCategory.hom (SimplicialObject.δ X j)) x
this : Mono (yonedaEquiv.symm x)
⊢ stdSimplex.objEquiv.symm (SimplexCategory.δ i) = stdSimplex.objEquiv.symm (SimplexCategory.δ j)

Tactic:
exact injective_of_mono ((yonedaEquiv.symm x).app _) hij

Goal state after:
Module: Mathlib.CategoryTheory.Generator.StrongGenerator

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝¹ : P.IsStrongGenerator
hS₁ : P.IsSeparating
hS₂ : ∀ ⦃X : C⦄ (A : Subobject X), (∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f) → A = ⊤
X Y : C
i : X ⟶ Y
x✝ : Mono i
h : ∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i
G : C
hG : P G
g : G ⟶ Y
⊢ (Subobject.mk i).Factors g

Tactic:
Subobject.mk_factors_iff

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝¹ : P.IsStrongGenerator
hS₁ : P.IsSeparating
hS₂ : ∀ ⦃X : C⦄ (A : Subobject X), (∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f) → A = ⊤
X Y : C
i : X ⟶ Y
x✝ : Mono i
h : ∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i
G : C
hG : P G
g : G ⟶ Y
⊢ (MonoOver.mk i).Factors g
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: X : SSet
A : X.Subcomplex
left✝ : Mono A.ι
P₁ : (Subcomplex.range A.ι).Pairing
w✝ : P₁.IsRegular
P₂ : P₁.IsInner
⊢ ∃ B P, ∃ (h : P.IsRegular), P.IsInner ∧ B = A

Tactic:
exact ⟨_, P₁, inferInstance, ⟨P₂, by simp⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst✝ : HasPushout f g
Q : C
⊢ Q ◁ pushout.inl f g ≫ Q ◁ hP.isoPushout.inv = Q ◁ inl

Tactic:
simp [← MonoidalCategory.whiskerLeft_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst✝ : HasPushout f g
Q : C
⊢ Q ◁ pushout.inr f g ≫ Q ◁ hP.isoPushout.inv = Q ◁ inr

Tactic:
simp [← MonoidalCategory.whiskerLeft_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst✝ : HasPushout f g
Q : C
⊢ Q ◁ inl ≫ Q ◁ hP.isoPushout.hom = Q ◁ pushout.inl f g

Tactic:
simp [← MonoidalCategory.whiskerLeft_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst✝ : HasPushout f g
Q : C
⊢ Q ◁ inr ≫ Q ◁ hP.isoPushout.hom = Q ◁ pushout.inr f g

Tactic:
simp [← MonoidalCategory.whiskerLeft_comp]

Goal state after:
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
Q X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ Q ◁ pushout.inl f g ≫ Q ◁ (pushoutSymmetry f g).hom = Q ◁ pushout.inr g f

Tactic:
simp [← MonoidalCategory.whiskerLeft_comp]

Goal state after:
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
Q X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ Q ◁ pushout.inr f g ≫ Q ◁ (pushoutSymmetry f g).hom = Q ◁ pushout.inl g f

Tactic:
simp [← MonoidalCategory.whiskerLeft_comp]

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 : ℕ
hd : x.dim = d
l : Fin d
hl : IsIndex x hd l.succ
i : Fin (d + 1)
⊢ (x.cast hd).simplex.1 i ≤ k.castSucc ↔ i < l.succ

Tactic:
rw [Fin.le_castSucc_iff, ← not_le, hl.succ_le_simplex_fst_iff, not_le]

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)
⊢ HasLiftingProperty Λ[n✝ + 2, k].ι sq₁₃.π

Tactic:
let sq₁₂ := Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) i Λ[_, k].ι

Goal state after:
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].ι
⊢ HasLiftingProperty Λ[n✝ + 2, k].ι sq₁₃.π
Module: Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
x : WalkingIso
⊢ WalkingIso.rec (motive := fun {x_1} ↦ (x_1 ⟶ x) → (WalkingIso.rec X Y x_1 ⟶ WalkingIso.rec X Y x))
      (fun x_1 ↦
        WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y)) (fun x ↦ 𝟙 X)
          (fun x ↦ e.hom) x x_1)
      (fun x_1 ↦
        WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y)) (fun x ↦ e.inv)
          (fun x ↦ 𝟙 Y) x x_1)
      x (𝟙 x) =
    𝟙 (WalkingIso.rec X Y x)

Tactic:
by induction x <;> rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
X Y : WalkingIso
⊢ ∀ (f : X ⟶ Y),
    ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).map f =
      eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

Tactic:
f

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
X Y : WalkingIso
f : X ⟶ Y
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesColimit

Goal state before:
pp: X : SSet
s : Cocone X.functorN
x : X.N
this :
  x.subcomplex.ι ≫ (Subcomplex.topIso X).inv =
    ((CompleteLattice.MulticoequalizerDiagram.multicofork ⋯).map Subcomplex.toSSetFunctor).π x
⊢ x.subcomplex.ι ≫ desc s = s.ι.app x

Tactic:
rw [reassoc_of% this]

Goal state after:
X : SSet
s : Cocone X.functorN
x : X.N
this :
  x.subcomplex.ι ≫ (Subcomplex.topIso X).inv =
    ((CompleteLattice.MulticoequalizerDiagram.multicofork ⋯).map Subcomplex.toSSetFunctor).π x
⊢ ((CompleteLattice.MulticoequalizerDiagram.multicofork ⋯).map Subcomplex.toSSetFunctor).π x ≫
      Multicofork.IsColimit.desc ⋯.isColimit (fun x ↦ s.ι.app x) ⋯ =
    s.ι.app x
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‖
⊢ #↑s = #E

Tactic:
have cn_ne : ∀ n, c ^ n ≠ 0 := by
    intro n
    apply pow_ne_zero
    rintro rfl
    simp only [norm_zero] at hc
    exact lt_irrefl _ (hc.trans zero_lt_one)

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
⊢ #↑s = #E
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
⊢ v.IsEquiv w ↔
    IsEmbedding ⇑(WithAbs.congr v w (RingEquiv.refl F)) ∧ Function.Surjective ⇑(WithAbs.congr v w (RingEquiv.refl F))

Tactic:
refine ⟨fun h ↦ ⟨h.isEmbedding_equivWithAbs, RingEquiv.surjective _⟩, fun ⟨hi, _⟩ ↦ ?_⟩

Goal state after:
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
x✝ : IsEmbedding ⇑(WithAbs.congr v w (RingEquiv.refl F)) ∧ Function.Surjective ⇑(WithAbs.congr v w (RingEquiv.refl F))
hi : IsEmbedding ⇑(WithAbs.congr v w (RingEquiv.refl F))
right✝ : Function.Surjective ⇑(WithAbs.congr v w (RingEquiv.refl F))
⊢ v.IsEquiv w
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

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

Tactic:
simp only [FormalMultilinearSeries.apply_eq_prod_smul_coeff, Finset.prod_const_one,
    FormalMultilinearSeries.coeff_ofScalars, smul_eq_mul, one_mul]

Goal state after:
n : ℕ
⊢ -(-1) ^ n / ↑n = iteratedDeriv n log 1 / ↑n.factorial
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
c : 𝕜
⊢ analyticOrderAt (fun x ↦ x - c) c = 1

Tactic:
by
  have := analyticOrderAt_centeredMonomial (n := 1) (z₀ := c)
  simp_all [pow_one]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
this :
  ∀ y ∈ B ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ‖f y - f x - (f' y - f' x)‖ ≤ ε * ‖y - x‖
y : E
hy : y ∈ ball x δ ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ y ∈ {x_1 | (fun x_2 ↦ ‖f x_2 - f x - f' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}

Tactic:
by simpa using this y hy

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
hf : MeromorphicAt f x
⊢ MeromorphicAt (-f) x

Tactic:
by
  convert (MeromorphicAt.const (-1 : 𝕜) x).smul hf
  ext1 z
  simp only [Pi.neg_apply, Pi.smul_apply', neg_smul, one_smul]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hg : MeromorphicAt g x
⊢ MeromorphicAt (f - g) x ↔ MeromorphicAt f x

Tactic:
exact ⟨fun h ↦ by simpa using h.add hg, fun _ ↦ by fun_prop⟩

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

Goal state before:
pp: n✝ n : ℕ
⊢ Differentiable ℂ (iteratedDeriv (n + 2) sin)

Tactic:
simp [differentiable_iteratedDeriv_sin]

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

Goal state before:
pp: n✝ n : ℕ
⊢ Differentiable ℝ (iteratedDeriv (n + 2) sin)

Tactic:
simp [differentiable_iteratedDeriv_sin]

Goal state after:
Module: Mathlib.RingTheory.Binomial

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

Tactic:
factorial_nsmul_multichoose_eq_ascPochhammer,

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

Goal state before:
pp: R : Type u_1
inst✝² : AddCommMonoid R
inst✝¹ : Pow R ℕ
inst✝ : BinomialRing R
r : R
⊢ Nat.factorial 1 • multichoose r 1 = Nat.factorial 1 • r ^ 1

Tactic:
factorial_nsmul_multichoose_eq_ascPochhammer,

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

Goal state before:
pp: R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
k : ℕ
⊢ (k + 1).factorial • multichoose 0 (k + 1) = (k + 1).factorial • 0

Tactic:
factorial_nsmul_multichoose_eq_ascPochhammer,

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

Goal state before:
pp: case succ
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
n : ℕ
ih : multichoose 1 n = 1
⊢ multichoose 1 n = 1

Tactic:
ih

Goal state after:
case succ
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
n : ℕ
ih : multichoose 1 n = 1
⊢ 1 = 1
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hr : AnalyticAt 𝕜' (fun z ↦ (z - g x) ^ r • f z) (g x)
hg' : ¬analyticOrderAt (fun x_1 ↦ g x_1 - g x) x = ⊤
⊢ MeromorphicAt (f ∘ g) x

Tactic:
obtain ⟨n, hn⟩ := WithTop.ne_top_iff_exists.mp hg'

Goal state after:
case neg
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hr : AnalyticAt 𝕜' (fun z ↦ (z - g x) ^ r • f z) (g x)
hg' : ¬analyticOrderAt (fun x_1 ↦ g x_1 - g x) x = ⊤
n : ℕ
hn : ↑n = analyticOrderAt (fun x_1 ↦ g x_1 - g x) x
⊢ MeromorphicAt (f ∘ g) x
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hg' : ¬analyticOrderAt (fun x_1 ↦ g x_1 - g x) x = ⊤
n : ℕ
hn : ↑n = analyticOrderAt (fun x_1 ↦ g x_1 - g x) x
h : 𝕜 → 𝕜'
han : AnalyticAt 𝕜 h x
hne : h x ≠ 0
heq : ∀ᶠ (z : 𝕜) in 𝓝 x, g z - g x = (z - x) ^ n • h z
j : 𝕜' → F := fun z ↦ (z - g x) ^ r • f z
hr : AnalyticAt 𝕜' j (g x)
this : AnalyticAt 𝕜 (fun i ↦ (h i)⁻¹ ^ r • j (g i)) x
z : 𝕜
hz : g z - g x = (z - x) ^ n • h z
hzne : h z ≠ 0
⊢ ((z - x) ^ n • h z) ^ r • f (g z) = (z - x) ^ (n * r) • h z ^ r • f (g z)

Tactic:
← smul_assoc,

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hg' : ¬analyticOrderAt (fun x_1 ↦ g x_1 - g x) x = ⊤
n : ℕ
hn : ↑n = analyticOrderAt (fun x_1 ↦ g x_1 - g x) x
h : 𝕜 → 𝕜'
han : AnalyticAt 𝕜 h x
hne : h x ≠ 0
heq : ∀ᶠ (z : 𝕜) in 𝓝 x, g z - g x = (z - x) ^ n • h z
j : 𝕜' → F := fun z ↦ (z - g x) ^ r • f z
hr : AnalyticAt 𝕜' j (g x)
this : AnalyticAt 𝕜 (fun i ↦ (h i)⁻¹ ^ r • j (g i)) x
z : 𝕜
hz : g z - g x = (z - x) ^ n • h z
hzne : h z ≠ 0
⊢ ((z - x) ^ n • h z) ^ r • f (g z) = ((z - x) ^ (n * r) • h z ^ r) • f (g z)
Module: Mathlib.RingTheory.Binomial

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

Tactic:
by
  induction n with
  | zero => simp only [descPochhammer_zero, ascPochhammer_zero, smeval_one, npow_zero]
  | succ n ih =>
    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]
    simp only [smeval_X, npow_one, npow_zero, zsmul_one, Int.cast_natCast, one_smul]

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
k : ℕ
ih : (ascPochhammer ℕ k).smeval (-r) = (↑k).negOnePow • (descPochhammer ℤ k).smeval r
h : (X + ↑k).smeval (-r) = -(X + -↑k).smeval r
⊢ -(↑(↑k).negOnePow • (descPochhammer ℤ k).smeval r) * (X + -↑k).smeval r =
    -(↑(↑k).negOnePow • ((descPochhammer ℤ k).smeval r * (X + -↑k).smeval r))

Tactic:
← smul_mul_assoc,

Goal state after:
case succ
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
ih : (ascPochhammer ℕ k).smeval (-r) = (↑k).negOnePow • (descPochhammer ℤ k).smeval r
h : (X + ↑k).smeval (-r) = -(X + -↑k).smeval r
⊢ -(↑(↑k).negOnePow • (descPochhammer ℤ k).smeval r) * (X + -↑k).smeval r =
    -(↑(↑k).negOnePow • (descPochhammer ℤ k).smeval r * (X + -↑k).smeval r)
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: n : ℕ
⊢ Nat.factorial ?m.25 • multichoose (-↑n) n = Nat.factorial ?m.25 • (-1) ^ n

pp: n : ℕ
⊢ ℕ

Tactic:
factorial_nsmul_multichoose_eq_ascPochhammer,

Goal state after:
n : ℕ
⊢ (ascPochhammer ℕ n).smeval (-↑n) = n.factorial • (-1) ^ n
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: n : ℕ
⊢ Nat.factorial ?m.25 • multichoose (-↑n) (n + 1) = Nat.factorial ?m.25 • 0

pp: n : ℕ
⊢ ℕ

Tactic:
factorial_nsmul_multichoose_eq_ascPochhammer,

Goal state after:
n : ℕ
⊢ (ascPochhammer ℕ (n + 1)).smeval (-↑n) = (n + 1).factorial • 0
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: n k : ℕ
⊢ (n + k + 1).factorial • multichoose (-↑n) (n + k + 1) = (n + k + 1).factorial • 0

Tactic:
factorial_nsmul_multichoose_eq_ascPochhammer,

Goal state after:
n k : ℕ
⊢ (ascPochhammer ℕ (n + k + 1)).smeval (-↑n) = (n + k + 1).factorial • 0
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: n k : ℕ
h : n < k
⊢ k.factorial • multichoose (-↑n) k = k.factorial • 0

Tactic:
factorial_nsmul_multichoose_eq_ascPochhammer,

Goal state after:
n k : ℕ
h : n < k
⊢ (ascPochhammer ℕ k).smeval (-↑n) = k.factorial • 0
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
n : ℕ
⊢ (n + 1).factorial • multichoose (-↑n) (n + 1) = 0

Tactic:
factorial_nsmul_multichoose_eq_ascPochhammer,

Goal state after:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
n : ℕ
⊢ (ascPochhammer ℕ (n + 1)).smeval (-↑n) = 0
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ (descPochhammer ℤ n).smeval r = n.factorial • multichoose (r - ↑n + 1) n

Tactic:
factorial_nsmul_multichoose_eq_ascPochhammer,

Goal state after:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ (descPochhammer ℤ n).smeval r = (ascPochhammer ℕ n).smeval (r - ↑n + 1)
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n k : ℕ
hkn : k ≤ n
⊢ n.choose k • choose r n = choose r k * choose (r - ↑k) (n - k)

Tactic:
← nsmul_right_inj (Nat.factorial_ne_zero n),

Goal state after:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n k : ℕ
hkn : k ≤ n
⊢ n.factorial • n.choose k • choose r n = n.factorial • (choose r k * choose (r - ↑k) (n - k))
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)⁻¹ • (descPochhammer ℤ n).smeval a

Tactic:
Ring.descPochhammer_eq_factorial_smul_choose,

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.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case neg
x p : ℝ
h : p ≠ 0
h' : x = 0 ∧ p < 1
⊢ deriv (fun x ↦ x ^ p) x = p * x ^ (p - 1)

Tactic:
have h'' := deriv_zero_of_not_differentiableAt (not_differentiableAt_rpow_const_zero h'.2 h ·)

Goal state after:
case neg
x p : ℝ
h : p ≠ 0
h' : x = 0 ∧ p < 1
h'' : deriv (fun x ↦ x ^ p) 0 = 0
⊢ deriv (fun x ↦ x ^ p) x = p * x ^ (p - 1)
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: r : ℝ
hr : r ≠ 0
⊢ HasFPowerSeriesOnBall (fun x ↦ 1 / (r - x)) (FormalMultilinearSeries.ofScalars ℝ fun n ↦ (r ^ (n + 1))⁻¹) 0 ‖r‖ₑ

Tactic:
by
  simpa using one_div_sub_pow_hasFPowerSeriesOnBall_zero (a := 0) hr

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

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

Tactic:
use 0; simp

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

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
⊢ ENNReal.ofReal (Real.exp (a✝¹ + a✝)) = ENNReal.ofReal (Real.exp a✝¹) * ENNReal.ofReal (Real.exp a✝)

Tactic:
rw [← ENNReal.ofReal_mul (Real.exp_nonneg _), Real.exp_add]

Goal state after: