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 ι
inst✝ : P.IsProper
j : ι
d : ℕ
s : f.sigmaStdSimplex j _⦋d⦌
hs : s ∈ (f.sigmaStdSimplex j).nonDegenerate d
hs' : s ∉ (range (f.m j)).obj (op ⦋d⦌)
⊢ ∃ c, N.mk s hs hs' = Cell.type₁ f c ∨ N.mk s hs hs' = Cell.type₂ f c

Tactic:
obtain ⟨x, s, rfl⟩ := f.ιSigmaStdSimplex_jointly_surjective s

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
d : ℕ
x : f.Cell j
s : Δ[x.dim + 1] _⦋d⦌
hs : (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) s ∈ (f.sigmaStdSimplex j).nonDegenerate d
hs' : (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) s ∉ (range (f.m j)).obj (op ⦋d⦌)
⊢ ∃ c,
    N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) s) hs hs' = Cell.type₁ f c ∨
      N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) s) hs hs' = Cell.type₂ f c
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
X✝ Y✝ Z✝ : ↑h.smallCategoryOfSet.obj
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ h.homEquiv (x✝¹ ≫ x✝) = h.homEquiv x✝¹ ≫ h.homEquiv x✝

Tactic:
rw [SmallCategoryOfSet.comp_def]

Goal state after:
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
X✝ Y✝ Z✝ : ↑h.smallCategoryOfSet.obj
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ h.homEquiv (h.smallCategoryOfSet.comp x✝¹ x✝) = h.homEquiv x✝¹ ≫ h.homEquiv x✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
i : Fin (m + 2)
hi : i ≠ k.castSucc
⊢ i ∈ Set.range ⇑(x.cast ⋯).simplex.1

Tactic:
have := x.notMem

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
i : Fin (m + 2)
hi : i ≠ k.castSucc
this : x.simplex ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋x.dim⦌)
⊢ i ∈ Set.range ⇑(x.cast ⋯).simplex.1
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
i : Fin (n + 1)
⊢ i ∈ Set.range ⇑(x.cast ⋯).simplex.2

Tactic:
have := x.notMem

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
i : Fin (n + 1)
this : x.simplex ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋x.dim⦌)
⊢ i ∈ Set.range ⇑(x.cast ⋯).simplex.2
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]

Goal state after:
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 < (k.castSucc, (x.cast hd).simplex.2 (min x hd))
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)
⊢ ((X₁ □ X₂) □ X₃) ≅ X₁ □ X₂ □ X₃

Tactic:
by
  refine Arrow.isoMk ?_ (α_ _ _ _) ?_
  · refine Iso.mk ?_ ?_ ?_ ?_
    · exact pushout.desc ((α_ _ _ _).hom ≫ _ ◁ pushout.inl _ _ ≫ pushout.inl _ _)
        ((whiskerRightIso _ _).hom.left ≫
          pushout.desc (_ ◁ pushout.inr _ _ ≫ pushout.inl _ _) (pushout.inr _ _)
          (by simp [Limits.pushout.associator_naturality_left_condition]))
        (((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext
          (by simp [Limits.pushout.whiskerLeft_condition_assoc, ← whisker_exchange_assoc,
            ← comp_whiskerRight_assoc])
          (by simp [← whisker_exchange_assoc, Limits.pushout.associator_naturality_left_condition,
            ← comp_whiskerRight_assoc]))
    · exact pushout.desc ((whiskerLeftIso _ _).hom.left ≫
          pushout.desc (pushout.inl _ _) ((pushout.inl _ _ ▷ _) ≫ pushout.inr _ _)
          (by simp [Limits.pushout.associator_inv_naturality_right_condition]))
        ((α_ _ _ _).inv ≫ (pushout.inr _ _) ▷ _ ≫ pushout.inr _ _)
        (((tensorLeft _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext
          (by simp [whisker_exchange_assoc,
            Limits.pushout.associator_inv_naturality_right_condition, ← whiskerLeft_comp_assoc])
          (by simp [whisker_exchange_assoc, Limits.pushout.condition_whiskerRight_assoc,
            ← whiskerLeft_comp_assoc]))
    · apply pushout.hom_ext (by simp)
      apply ((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext <;> simp
    · refine pushout.hom_ext ?_ (by simp)
      apply ((tensorLeft _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext <;> simp
  · apply pushout.hom_ext (by simp [← MonoidalCategory.whiskerLeft_comp])
    · apply ((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext
      · simp [← MonoidalCategory.whiskerLeft_comp, ← MonoidalCategory.comp_whiskerRight_assoc]
      · simp [← MonoidalCategory.comp_whiskerRight_assoc]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
⊢ parallelPair ((sigmaConst.obj R).map (SimplicialObject.δ X 1) - (sigmaConst.obj R).map (SimplicialObject.δ X 0)) 0 ≅
    parallelPair ((X.chainComplex R).d 1 0) 0

Tactic:
refine parallelPair.ext (-Iso.refl _) (Iso.refl _) ?_ (by simp)
    simp [chainComplex, SSet.chainComplexFunctor, sub_eq_neg_add]

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
s : X.PtSimplex n x
Y : SSet
φ : Y ⟶ Δ[n]
inst✝ : Y.HasDimensionLT n
h : Subcomplex.range φ = ⊤
this : IsIso (Subcomplex.range φ).ι
⊢ False

Tactic:
exact stdSimplex.not_hasDimensionLT n
    ((hasDimensionLT_iff_of_iso (asIso (Subcomplex.range φ).ι) n).mp inferInstance)

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

Goal state before:
pp: X : SSet
s : Cocone X.functorN
x : X.N
⊢ x.subcomplex.ι ≫ desc s = s.ι.app x

Tactic:
have : x.subcomplex.ι ≫ (Subcomplex.topIso X).inv =
    ((multicoequalizerDiagram X).multicofork.map Subcomplex.toSSetFunctor).π x := rfl

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
⊢ x.subcomplex.ι ≫ desc s = s.ι.app x
Module: Mathlib.Analysis.Normed.Field.WithAbs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Semiring S
inst✝³ : PartialOrder S
inst✝² : CommRing R
T : Type u_3
inst✝¹ : Field T
inst✝ : Algebra R T
w : AbsoluteValue T ℝ
r : R
⊢ UniformContinuous fun x ↦ (algebraMap R (WithAbs w)) r * x

Tactic:
exact (Ring.uniformContinuousConstSMul _).uniformContinuous_const_smul _

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
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
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
n : ℕ
w : E
hw : dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
⊢ ↑f'symm.nnnorm * dist (f b) y * 1 ≤ ↑f'symm.nnnorm * (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)

Tactic:
rw [mul_one]
        gcongr
        exact mem_closedBall'.1 hy

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
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
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y →
      w ∈ closedBall b ε
n : ℕ
⊢ dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧
    dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y

Tactic:
induction n with

Goal state after:
case succ
𝕜 : 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
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y →
      w ∈ closedBall b ε
n : ℕ
IH :
  dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧
    dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
⊢ dist (f (u (n + 1))) y ≤ (↑c * ↑f'symm.nnnorm) ^ (n + 1) * dist (f b) y ∧
    dist (u (n + 1)) b ≤
      ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ (n + 1)) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ := ⋯.choose
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hg_ne : g z₀ ≠ 0
hm : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ ⋯.choose • g z
hmn : n ≤ ⋯.choose
z : 𝕜
hz : f z = (z - z₀) ^ ⋯.choose • g z
⊢ f z = (z - z₀) ^ n • (z - z₀) ^ (m - n) • g z

Tactic:
by rwa [← mul_smul, ← pow_add, Nat.add_sub_of_le hmn]

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
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst✝¹ : CompleteSpace E
inst✝ : CharZero 𝕜
r : ℕ
h : analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = ↑r
hr : r = 0
⊢ False

Tactic:
rw [hr, ENat.natCast_zero, AnalyticAt.analyticOrderAt_eq_zero (by fun_prop)] at h

Goal state after:
𝕜 : 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 𝕜
r : ℕ
h : f x - f x ≠ 0
hr : r = 0
⊢ False
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case top
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
h : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = f x
⊢ deriv f x = 0

Tactic:
rw [EventuallyEq.deriv_eq h, deriv_const]

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

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

Tactic:
ext n

Goal state after:
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
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: r : ENNReal
hp : HasFPowerSeriesOnBall log (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n) 1 r
this :
  HasFPowerSeriesOnBall log
    (FormalMultilinearSeries.restrictScalars ℝ (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n))
    (ofRealCLM 1) r
⊢ (FormalMultilinearSeries.ofScalars ℝ fun n ↦ -(-1) ^ n / ↑n) =
    reCLM.compFormalMultilinearSeries
      ((FormalMultilinearSeries.restrictScalars ℝ
            (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n)).compContinuousLinearMap
        ofRealCLM)

Tactic:
ext n

Goal state after:
r : ENNReal
hp : HasFPowerSeriesOnBall log (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n) 1 r
this :
  HasFPowerSeriesOnBall log
    (FormalMultilinearSeries.restrictScalars ℝ (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n))
    (ofRealCLM 1) r
n : ℕ
⊢ ((FormalMultilinearSeries.ofScalars ℝ (fun n ↦ -(-1) ^ n / ↑n) n) fun x ↦ 1) =
    (reCLM.compFormalMultilinearSeries
        ((FormalMultilinearSeries.restrictScalars ℝ
              (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n)).compContinuousLinearMap
          ofRealCLM)
        n)
      fun x ↦ 1
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case succ
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
z₀ : 𝕜
n : ℕ
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
IH : analyticOrderAt (deriv f) z₀ = ↑n ↔ (∀ k < n, iteratedDeriv (k + 1) f z₀ = 0) ∧ iteratedDeriv (n + 1) f z₀ ≠ 0
⊢ analyticOrderAt f z₀ = ↑(n + 1) ↔ (∀ k < n + 1, iteratedDeriv k f z₀ = 0) ∧ iteratedDeriv (n + 1) f z₀ ≠ 0

Tactic:
refine ⟨fun ho ↦ ?_, fun ⟨hz, hnz⟩ ↦ ?_⟩

Goal state after:
case succ.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
z₀ : 𝕜
n : ℕ
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
IH : analyticOrderAt (deriv f) z₀ = ↑n ↔ (∀ k < n, iteratedDeriv (k + 1) f z₀ = 0) ∧ iteratedDeriv (n + 1) f z₀ ≠ 0
ho : analyticOrderAt f z₀ = ↑(n + 1)
⊢ (∀ k < n + 1, iteratedDeriv k f z₀ = 0) ∧ iteratedDeriv (n + 1) f z₀ ≠ 0

case succ.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
z₀ : 𝕜
n : ℕ
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
IH : analyticOrderAt (deriv f) z₀ = ↑n ↔ (∀ k < n, iteratedDeriv (k + 1) f z₀ = 0) ∧ iteratedDeriv (n + 1) f z₀ ≠ 0
x✝ : (∀ k < n + 1, iteratedDeriv k f z₀ = 0) ∧ iteratedDeriv (n + 1) f z₀ ≠ 0
hz : ∀ k < n + 1, iteratedDeriv k f z₀ = 0
hnz : iteratedDeriv (n + 1) f z₀ ≠ 0
⊢ analyticOrderAt f z₀ = ↑(n + 1)
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case pos
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_5
F : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ (i : ι), MeromorphicAt (F i) x
h₂f : Function.HasFiniteMulSupport F
⊢ MeromorphicAt (∏ᶠ (i : ι), F i) x

Tactic:
simpa [finprod_eq_prod F h₂f] using prod (by aesop)

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

Goal state before:
pp: case right
𝕜 : 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 : analyticOrderAt f ↑z = ⊤
⊢ ∃ x ⊆ {x | ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑x ∈ t},
    IsOpen[instTopologicalSpaceSubtype] x ∧ z ∈ x

Tactic:
rw [analyticOrderAt_eq_top, eventually_nhds_iff] at hz

Goal state after:
case right
𝕜 : 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 : ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑z ∈ t
⊢ ∃ x ⊆ {x | ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑x ∈ t},
    IsOpen[instTopologicalSpaceSubtype] x ∧ z ∈ x
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
n : ℕ
⊢ MeromorphicAt (f ^ n) x

Tactic:
induction n with

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

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (n + 1) sin = iteratedDeriv n cos

Tactic:
induction n with

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

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (n + 1) cos = -iteratedDeriv n sin

Tactic:
induction n with

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

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (2 * n) sin = (-1) ^ n * sin

Tactic:
induction n with

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

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (2 * n) cos = (-1) ^ n * cos

Tactic:
induction n with

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
inst✝ : CompleteSpace E
n : ℕ
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
⊢ MeromorphicAt (deriv^[n] f) x

Tactic:
induction n with

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Pow S ℕ
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : NatPowAssoc S
x : S
n : ℕ
⊢ (ascPochhammer R n).smeval x = (ascPochhammer ℕ n).smeval x

Tactic:
induction n with

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)
⊢ (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)

Tactic:
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: 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:
induction n with

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

Goal state before:
pp: a : ℂ
⊢ (fun x ↦ Ring.choose a x) = fun n ↦ iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0 / ↑n !

Tactic:
ext n

Goal state after:
a : ℂ
n : ℕ
⊢ Ring.choose a n = iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0 / ↑n !
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: a : ℂ
B : Set ℂ := Metric.ball 0 1
n : ℕ
ih :
  Set.EqOn (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n))
    B
this :
  iteratedDerivWithin (n + 1) (fun x ↦ (1 + x) ^ a) B = derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B
z : ℂ
hz : z ∈ B
⊢ derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B z =
    derivWithin (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n)) B z

Tactic:
rw [derivWithin_congr (fun _ hz ↦ ih hz) (ih hz)]

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

Goal state before:
pp: a : ℂ
n : ℕ
B : Set ℂ := Metric.ball 0 1
⊢ Set.EqOn (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n))
    B

Tactic:
induction n with

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

Goal state before:
pp: a : ℂ
⊢ (binomialSeries ℂ (-a)).compContinuousLinearMap (-1) =
    FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (a + ↑n - 1) n

Tactic:
ext n

Goal state after:
a : ℂ
n : ℕ
⊢ (((binomialSeries ℂ (-a)).compContinuousLinearMap (-1) n) fun x ↦ 1) =
    (FormalMultilinearSeries.ofScalars ℂ (fun n ↦ Ring.choose (a + ↑n - 1) n) n) fun x ↦ 1
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: a : ℕ
z : ℂ
hz : z ≠ 0
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑((a + n).choose a)) ((z⁻¹ • 1) 0) 1
⊢ HasFPowerSeriesOnBall (fun x ↦ 1 / (z - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun n ↦ (z ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)) 0 ‖z‖ₑ

Tactic:
have := this.compContinuousLinearMap

Goal state after:
a : ℕ
z : ℂ
hz : z ≠ 0
this✝ :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑((a + n).choose a)) ((z⁻¹ • 1) 0) 1
this :
  HasFPowerSeriesOnBall ((fun x ↦ 1 / (1 - x) ^ (a + 1)) ∘ ⇑(z⁻¹ • 1))
    ((FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑((a + n).choose a)).compContinuousLinearMap (z⁻¹ • 1)) 0
    (1 / ‖z⁻¹ • 1‖ₑ)
⊢ HasFPowerSeriesOnBall (fun x ↦ 1 / (z - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun n ↦ (z ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)) 0 ‖z‖ₑ
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

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
n : ℕ
f : E [×n]→L[𝕜] F
x : E
v : Fin n → E
g : E →L[𝕜] Fin n → E := ContinuousLinearMap.pi fun i ↦ ContinuousLinearMap.id 𝕜 E
⊢ ((iteratedFDeriv 𝕜 n (⇑f) (g x)).compContinuousLinearMap fun x ↦ g) v =
    ∑ i, f fun i_1 ↦ v (((Equiv.inv (Perm (Fin n))) i) i_1)

Tactic:
f.iteratedFDeriv_eq

Goal state after:
𝕜 : 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
n : ℕ
f : E [×n]→L[𝕜] F
x : E
v : Fin n → E
g : E →L[𝕜] Fin n → E := ContinuousLinearMap.pi fun i ↦ ContinuousLinearMap.id 𝕜 E
⊢ ((f.iteratedFDeriv n (g x)).compContinuousLinearMap fun x ↦ g) v =
    ∑ i, f fun i_1 ↦ v (((Equiv.inv (Perm (Fin n))) i) i_1)