mathlib-initiative/mathlib-tactics huggingface dataset:
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
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
⊢ ∃ F,
    AnalyticAt 𝕜 F 0 ∧ ∀ (z : 𝕜), f z = ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 + z ^ n • F z

Tactic:
by

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

Goal state before:
pp: D X : SSet
H : ∀ (m : ℕ), IsIso (prodComparison hoFunctor D Δ[m])
⊢ IsIso (prodComparison hoFunctor D X)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
⊢ ordinaryHypergeometricSeries 𝔸 a b c = ordinaryHypergeometricSeries 𝔸 b a c

Tactic:
by

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
n : ℕ
h : ∀ i < n + 1, iteratedDeriv i f z₀ = 0
k : ℕ
hk : k < n
⊢ k + 1 < n + 1

Tactic:
by

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
n : ℕ
h : ∀ i < n, iteratedDeriv (i + 1) f z₀ = 0
k : ℕ
hk : k + 1 < n + 1
⊢ k < n

Tactic:
by

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
n : ℕ
⊢ ↑n ≤ analyticOrderAt (deriv f) z₀ ↔ ↑n + 1 ≤ analyticOrderAt f z₀

Tactic:
by

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:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
habc : ↑k = -a ∨ ↑k = -b ∨ ↑k = -c
hk : k < n
⊢ ordinaryHypergeometricSeries 𝔸 a b c n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
b c : 𝕂
k n : ℕ
⊢ ↑?m.51 = - -↑k ∨ ↑?m.51 = -b ∨ ↑?m.51 = -c

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
b c : 𝕂
k n : ℕ
⊢ k < n + (1 + k)

Tactic:
by

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
n✝ m : ℕ
n : ℕ∞
⊢ n = ↑m ↔ ↑m ≤ n ∧ ¬↑m + 1 ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
b c : 𝕂
k : ℕ
⊢ (ordinaryHypergeometricSeries 𝔸 (-↑k) b c).radius = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a c : 𝕂
k : ℕ
⊢ (ordinaryHypergeometricSeries 𝔸 a (-↑k) c).radius = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b : 𝕂
k n : ℕ
⊢ ↑?m.51 = -a ∨ ↑?m.51 = -b ∨ ↑?m.51 = - -↑k

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b : 𝕂
k n : ℕ
⊢ k < n + (1 + k)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b : 𝕂
k : ℕ
⊢ (ordinaryHypergeometricSeries 𝔸 a b (-↑k)).radius = ⊤

Tactic:
by

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

Goal state before:
pp: X Y : SSet
m : ℕ
this : IsIso (prodComparison hoFunctor Δ[m] X)
⊢ IsIso
    (hoFunctor.map (prod.braiding X Δ[m]).hom ≫
      prodComparison hoFunctor Δ[m] X ≫ (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)).hom)

Tactic:
by

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
n : ℕ
⊢ analyticOrderAt f z₀ = ↑n + 1 ↔ analyticOrderAt (deriv f) z₀ = ↑n

Tactic:
by

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

Goal state before:
pp: X Y : SSet
m : ℕ
⊢ IsIso (prodComparison hoFunctor X Δ[m])

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
n : ℕ
h : Polynomial.eval a (ascPochhammer 𝕂 n) = 0
kn : ℕ
hkn : kn < n
hn : ↑kn = -a
⊢ ↑kn = -a ∨ ↑kn = -b ∨ ↑kn = -c

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
n : ℕ
h : Polynomial.eval b (ascPochhammer 𝕂 n) = 0
kn : ℕ
hkn : kn < n
hn : ↑kn = -b
⊢ ↑kn = -a ∨ ↑kn = -b ∨ ↑kn = -c

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
n : ℕ
h : Polynomial.eval c (ascPochhammer 𝕂 n) = 0
kn : ℕ
hkn : kn < n
hn : ↑kn = -c
⊢ ↑kn = -a ∨ ↑kn = -b ∨ ↑kn = -c

Tactic:
by

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₀ : 𝕜
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)
h_zero : ∀ k < n, iteratedDeriv (k + 1) f z₀ = 0
h_nz : iteratedDeriv (n + 1) f z₀ ≠ 0
k✝ k : ℕ
hk : k + 1 < n + 1
⊢ k < n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
n : ℕ
⊢ ordinaryHypergeometricSeries 𝔸 a b c n = 0 ↔ ∃ k < n, ↑k = -a ∨ ↑k = -b ∨ ↑k = -c

Tactic:
by

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₀ : 𝕜
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
⊢ 0 < n + 1

Tactic:
by

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₀ : 𝕜
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
⊢ f z₀ = 0

Tactic:
by

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 < ε
⊢ ∃ δ > 0, ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε

Tactic:
by

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₀ : 𝕜
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
j : ℕ
x✝ : j < n
⊢ j + 1 < n + 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

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

Tactic:
by

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₀
n : ℕ
⊢ analyticOrderAt f z₀ = ↑n ↔ (∀ k < n, iteratedDeriv k f z₀ = 0) ∧ iteratedDeriv n f z₀ ≠ 0

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
n : ℕ
⊢ AnalyticAt 𝕜 ((fun x ↦ x - z₀) ^ n) z₀

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
n : ℕ
⊢ AnalyticAt 𝕜 1 z₀ ∧ 1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, ((fun x ↦ x - z₀) ^ n) z = (z - z₀) ^ n • 1 z

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
n : ℕ
⊢ analyticOrderAt ((fun x ↦ x - z₀) ^ n) z₀ = ↑n

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
hf' : analyticOrderAt f z₀ ≠ ⊤
hg' : analyticOrderAt g z₀ ≠ ⊤
⊢ analyticOrderNatAt (f * g) z₀ = analyticOrderNatAt f z₀ + analyticOrderNatAt g z₀

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ analyticOrderAt (f ^ 0) z₀ = 0 • analyticOrderAt f z₀

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
⊢ analyticOrderAt (f ^ (n + 1)) z₀ = (n + 1) • analyticOrderAt f z₀

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
⊢ analyticOrderNatAt (f ^ n) z₀ = n • analyticOrderNatAt f z₀

Tactic:
by

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

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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬EventuallyConst g (𝓝 z₀)
hf' : analyticOrderAt f (g z₀) = ⊤
⊢ AnalyticAt 𝕜 (fun x ↦ g x - g z₀) z₀

Tactic:
by

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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r s : ℕ
hs : analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ↑s
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F (g z₀)
hFne : F (g z₀) ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z
⊢ AnalyticAt 𝕜 (fun x ↦ g x - g z₀) z₀

Tactic:
by

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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r s : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F (g z₀)
hFne : F (g z₀) ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z
G : 𝕜 → 𝕜
hGa : AnalyticAt 𝕜 G z₀
hGne : G z₀ ≠ 0
hgG : ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z - g z₀ = (z - z₀) ^ s • G z
⊢ AnalyticAt 𝕜 (fun z ↦ G z ^ r • F (g z)) z₀

Tactic:
by

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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r s : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F (g z₀)
hFne : F (g z₀) ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z
G : 𝕜 → 𝕜
hGa : AnalyticAt 𝕜 G z₀
hGne : G z₀ ≠ 0
hgG : ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z - g z₀ = (z - z₀) ^ s • G z
⊢ (fun z ↦ G z ^ r • F (g z)) z₀ ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
kn : ℕ
hkn : kn < n
⊢ ↑kn ≠ -c

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
kn : ℕ
hkn : kn < n
⊢ ↑kn ≠ -b

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
kn : ℕ
hkn : kn < n
⊢ ↑kn ≠ -a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

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

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

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

Tactic:
by

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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (fun x ↦ g x - g z₀) z₀

Tactic:
by

Goal state after:
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)
⊢ Tendsto (fun n ↦ ‖ordinaryHypergeometricCoefficient a b c n‖ / ‖ordinaryHypergeometricCoefficient a b c n.succ‖) atTop
    (𝓝 ↑1)

Tactic:
by

Goal state after:
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
k : ℕ
⊢ (a + ↑k)⁻¹ * (b + ↑k)⁻¹ * (c + ↑k) * (1 + ↑k) = (c + ↑k) / (a + ↑k) * ((1 + ↑k) / (b + ↑k))

Tactic:
by

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 :
  ∀ p ∈ closure[instTopologicalSpaceProd] ((B ∩ s) ×ˢ (B ∩ s)), ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖
⊢ ∀ y ∈ B ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ‖f y - f x - (f' y - f' x)‖ ≤ ε * ‖y - x‖

Tactic:
by

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
g : 𝕜 → 𝕜
z₀ : 𝕜
hg : AnalyticAt 𝕜 g z₀
hg' : deriv g z₀ ≠ 0
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀)

Tactic:
by

Goal state after:
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
⊢ (ordinaryHypergeometricSeries 𝔸 a b c).radius = 1

Tactic:
by

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
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
⊢ AnalyticAt 𝕜 (fun z ↦ (z - x) ^ 0 • f z) x

Tactic:
by

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
f : 𝕜 → E
z₀ : 𝕜
hf : MeromorphicAt f z₀
⊢ (∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0

Tactic:
by

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
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • g z) x
⊢ (fun z ↦ (z - x) ^ max m n • (f + g) z) = fun z ↦
    (z - x) ^ (max m n - m) • (z - x) ^ m • f z + (z - x) ^ (max m n - n) • (z - x) ^ n • g z

Tactic:
by

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
hf : MeromorphicAt f x
hg : MeromorphicAt g x
⊢ MeromorphicAt (f + g) x

Tactic:
by

Goal state after: