mathlib-initiative/mathlib-tactics huggingface dataset:
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 δ
key : ∀ p ∈ (B ∩ s) ×ˢ (B ∩ s), ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖
u v : E
uv_in : (u, v) ∈ closure[instTopologicalSpaceProd] ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt (f - ⇑f') s y
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
⊢ u ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ∧
    v ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
simpa using

Goal state after:
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 δ
key : ∀ p ∈ (B ∩ s) ×ˢ (B ∩ s), ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖
u v : E
uv_in : (u, v) ∈ closure[instTopologicalSpaceProd] ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt (f - ⇑f') s y
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
⊢ u ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ∧
    v ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
hU : IsConnected U
this : ConnectedSpace ↑U
v : ↑U
⊢ (∀ (u : ↑U), analyticOrderAt f ↑u ≠ ⊤) ∨ ∀ (u : ↑U), analyticOrderAt f ↑u = ⊤

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
hU : IsConnected U
this : ConnectedSpace ↑U
v : ↑U
⊢ (∀ a ∈ U, ¬analyticOrderAt f a = ⊤) ∨ ∀ a ∈ U, analyticOrderAt f a = ⊤
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
h : MeromorphicAt f⁻¹ x
⊢ MeromorphicAt f x

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
h : MeromorphicAt f⁻¹ x
⊢ MeromorphicAt f x
Module: Mathlib.Analysis.Meromorphic.Basic

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

Tactic:
simpa using

Goal state after:
case ofNat
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
m : ℕ
⊢ MeromorphicAt (f ^ m) x
Module: Mathlib.Analysis.Meromorphic.Basic

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

Tactic:
simpa using

Goal state after:
case negSucc
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
m : ℕ
⊢ MeromorphicAt (f ^ (m + 1)) x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: n : ℕ
x : ℝ
⊢ |iteratedDeriv 0 sin x| ≤ 1

Tactic:
simpa using

Goal state after:
n : ℕ
x : ℝ
⊢ |sin x| ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: n : ℕ
x : ℝ
⊢ |iteratedDeriv 1 sin x| ≤ 1

Tactic:
simpa using

Goal state after:
n : ℕ
x : ℝ
⊢ |cos x| ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: n✝ : ℕ
x : ℝ
n : ℕ
⊢ |iteratedDeriv (n + 2) sin x| ≤ 1

Tactic:
simpa using

Goal state after:
n✝ : ℕ
x : ℝ
n : ℕ
⊢ |iteratedDeriv n sin x| ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: n : ℕ
x : ℝ
⊢ |iteratedDeriv 0 cos x| ≤ 1

Tactic:
simpa using

Goal state after:
n : ℕ
x : ℝ
⊢ |cos x| ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: n : ℕ
x : ℝ
⊢ |iteratedDeriv 1 cos x| ≤ 1

Tactic:
simpa using

Goal state after:
n : ℕ
x : ℝ
⊢ |sin x| ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: n✝ : ℕ
x : ℝ
n : ℕ
⊢ |iteratedDeriv (n + 2) cos x| ≤ 1

Tactic:
simpa using

Goal state after:
n✝ : ℕ
x : ℝ
n : ℕ
⊢ |iteratedDeriv n cos x| ≤ 1
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
n : ℕ
IH : MeromorphicAt (deriv^[n] f) x
⊢ MeromorphicAt (deriv^[n + 1] f) x

Tactic:
simpa using

Goal state after:
case succ
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
n : ℕ
IH : MeromorphicAt (deriv^[n] f) x
⊢ MeromorphicAt (deriv (deriv^[n] f)) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: f g : ℂ → ℂ
f' g' x : ℂ
hf : HasStrictDerivAt f f' x
hg : HasStrictDerivAt g g' x
h0 : f x ∈ slitPlane
⊢ HasStrictDerivAt (fun x ↦ f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') x

Tactic:
simpa using

Goal state after:
f g : ℂ → ℂ
f' g' x : ℂ
hf : HasStrictDerivAt f f' x
hg : HasStrictDerivAt g g' x
h0 : f x ∈ slitPlane
⊢ HasStrictDerivAt (fun x ↦ f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: f g : ℂ → ℂ
f' g' x : ℂ
hf : HasDerivAt f f' x
hg : HasDerivAt g g' x
h0 : f x ∈ slitPlane
⊢ HasDerivAt (fun x ↦ f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') x

Tactic:
simpa using

Goal state after:
f g : ℂ → ℂ
f' g' x : ℂ
hf : HasDerivAt f f' x
hg : HasDerivAt g g' x
h0 : f x ∈ slitPlane
⊢ HasDerivAt (fun x ↦ f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') x
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
U : Set 𝕜
h : MeromorphicOn (-f) U
⊢ MeromorphicOn f U

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h : MeromorphicOn (-f) U
⊢ MeromorphicOn f U
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
s : 𝕜 → 𝕜'
U : Set 𝕜
h : MeromorphicOn s⁻¹ U
⊢ MeromorphicOn s U

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
s : 𝕜 → 𝕜'
U : Set 𝕜
h : MeromorphicOn s⁻¹ U
⊢ MeromorphicOn s U
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: f g : ℂ → ℂ
s : Set ℂ
f' g' x : ℂ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
h0 : f x ∈ slitPlane
⊢ HasDerivWithinAt (fun x ↦ f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') s x

Tactic:
simpa using

Goal state after:
f g : ℂ → ℂ
s : Set ℂ
f' g' x : ℂ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
h0 : f x ∈ slitPlane
⊢ HasDerivWithinAt (fun x ↦ f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') s x
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
c : 𝕜
U : Set 𝕜
h : MeromorphicOn (f ∘ fun x ↦ x + c) U
y x : 𝕜
h₁x : x ∈ U
h₂x : x + c = y
⊢ MeromorphicAt f y

Tactic:
simpa using

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
c : 𝕜
U : Set 𝕜
h : MeromorphicOn (f ∘ fun x ↦ x + c) U
y x : 𝕜
h₁x : x ∈ U
h₂x : x + c = y
⊢ MeromorphicAt (f ∘ fun x ↦ x + c) x
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
inst✝¹ : SecondCountableTopology 𝕜
inst✝ : CompleteSpace E
h : Meromorphic f
⊢ {z | AnalyticAt 𝕜 f z}ᶜ.Countable

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
inst✝¹ : SecondCountableTopology 𝕜
inst✝ : CompleteSpace E
h : Meromorphic f
⊢ {z | AnalyticAt 𝕜 f z}ᶜ.Countable
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
inst✝⁵ : MeasurableSpace 𝕜
inst✝⁴ : SecondCountableTopology 𝕜
inst✝³ : BorelSpace 𝕜
inst✝² : MeasurableSpace E
inst✝¹ : CompleteSpace E
inst✝ : BorelSpace E
h : Meromorphic f
s : Set 𝕜 := {z | AnalyticAt 𝕜 f z}
⊢ sᶜ.Countable

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
f : 𝕜 → E
inst✝⁵ : MeasurableSpace 𝕜
inst✝⁴ : SecondCountableTopology 𝕜
inst✝³ : BorelSpace 𝕜
inst✝² : MeasurableSpace E
inst✝¹ : CompleteSpace E
inst✝ : BorelSpace E
h : Meromorphic f
s : Set 𝕜 := {z | AnalyticAt 𝕜 f z}
⊢ sᶜ.Countable
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case convert_7
a : ℂ
this : binomialSeries ℂ a = FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0 / ↑n !
z : ℂ
hz : z ∈ Metric.ball 0 1
⊢ ‖(fun x ↦ x) z‖ < 1

Tactic:
simpa using

Goal state after:
case convert_7
a : ℂ
this : binomialSeries ℂ a = FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0 / ↑n !
z : ℂ
hz : z ∈ Metric.ball 0 1
⊢ ‖z‖ < 1
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case ha
R : Type u_1
inst✝¹ : Field R
inst✝ : CharZero R
a : R
n : ℕ
⊢ ↑n.factorial ≠ 0

Tactic:
simpa using

Goal state after:
case ha
R : Type u_1
inst✝¹ : Field R
inst✝ : CharZero R
a : R
n : ℕ
⊢ ¬n.factorial = 0
Module: Mathlib.Analysis.Analytic.Binomial

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

Tactic:
simpa using

Goal state after:
a : ℂ
n : ℕ
B : Set ℂ := ⋯
this : iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0 = (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n)) 0
⊢ iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0 = (descPochhammer ℤ n).smeval a
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
B : HasDerivWithinAt f (g x) (Iic x) x
⊢ HasDerivAt f (g x) x

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
B : HasDerivWithinAt f (g x) (Iic x) x
⊢ HasDerivAt f (g x) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: x : ℝ
hx : x ≠ 0
r : ℂ
hr : r ≠ 0
this : HasDerivAt (fun y ↦ r * (↑y ^ (r - 1 + 1) / (r - 1 + 1))) (r * ↑x ^ (r - 1)) x
⊢ HasDerivAt (fun y ↦ ↑y ^ r) (r * ↑x ^ (r - 1)) x

Tactic:
simpa using

Goal state after:
x : ℝ
hx : x ≠ 0
r : ℂ
hr : r ≠ 0
this : HasDerivAt (fun y ↦ r * (↑y ^ (r - 1 + 1) / (r - 1 + 1))) (r * ↑x ^ (r - 1)) x
⊢ HasDerivAt (fun y ↦ ↑y ^ r) (r * ↑x ^ (r - 1)) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case inl
⊢ (deriv fun x ↦ 1) =O[atTop] fun x ↦ x ^ (re 0 - 1)

Tactic:
deriv_const',

Goal state after:
case inl
⊢ (fun x ↦ 0) =O[atTop] fun x ↦ x ^ (re 0 - 1)
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case succ
a : ℂ
B : Set ℂ := ⋯
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
this :
  Set.EqOn (derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B)
    (derivWithin (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n)) B) B
z : ℂ
hz : z ∈ B
⊢ ‖z‖ < 1

Tactic:
simpa using

Goal state after:
case succ
a : ℂ
B : Set ℂ := ⋯
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
this :
  Set.EqOn (derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B)
    (derivWithin (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n)) B) B
z : ℂ
hz : z ∈ B
⊢ ‖z‖ < 1
Module: Mathlib.Analysis.Analytic.Binomial

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

Tactic:
simpa using

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

Goal state before:
pp: a : ℂ
H :
  (binomialSeries ℂ (-a)).compContinuousLinearMap (-1) =
    FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (a + ↑n - 1) n
this : HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ (-a)) (binomialSeries ℂ (-a)) (-0) 1
⊢ HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ a)
    (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (a + ↑n - 1) n) 0 1

Tactic:
simpa using

Goal state after:
a : ℂ
H :
  (binomialSeries ℂ (-a)).compContinuousLinearMap (-1) =
    FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (a + ↑n - 1) n
this : HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ (-a)) (binomialSeries ℂ (-a)) (-0) 1
⊢ HasFPowerSeriesOnBall (fun x ↦ ((1 - x) ^ a)⁻¹)
    (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (a + ↑n - 1) n) 0 1
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : BinomialRing R
r s : R
k : ℕ
h : Commute r s
x : ℕ × ℕ
hx : x ∈ antidiagonal k
⊢ ↑(k.choose x.1) * ((descPochhammer ℤ x.1).smeval r * (descPochhammer ℤ x.2).smeval s) =
    ↑(k.choose x.1) * ↑x.1.factorial * (choose r x.1 * (↑x.2.factorial * choose s x.2))

Tactic:
← nsmul_eq_mul x.2.factorial

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : BinomialRing R
r s : R
k : ℕ
h : Commute r s
x : ℕ × ℕ
hx : x ∈ antidiagonal k
⊢ ↑(k.choose x.1) * ((descPochhammer ℤ x.1).smeval r * (descPochhammer ℤ x.2).smeval s) =
    ↑(k.choose x.1) * ↑x.1.factorial * (choose r x.1 * x.2.factorial • choose s x.2)
Module: Mathlib.Analysis.Analytic.Polynomial

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CommSemiring A
z : E
s : Set E
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f s z
p : A[X]
k : A
⊢ AnalyticWithinAt 𝕜 (fun x ↦ (algebraMap A B) k) s z

Tactic:
apply analyticWithinAt_const

Goal state after:
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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
⊢ AnalyticOn 𝕜 f s

Tactic:
simpa using

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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
⊢ AnalyticOn 𝕜 f s
Module: Mathlib.Analysis.Analytic.Binomial

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

Tactic:
simpa using

Goal state after:
z : ℂ
hz : z ≠ 0
⊢ HasFPowerSeriesOnBall (fun x ↦ (z - x)⁻¹) (FormalMultilinearSeries.ofScalars ℂ fun n ↦ (z ^ (n + 1))⁻¹) 0 ‖z‖ₑ
Module: Mathlib.Analysis.Analytic.Binomial

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

Tactic:
simpa using

Goal state after:
z : ℂ
hz : z ≠ 0
⊢ HasFPowerSeriesOnBall (fun x ↦ ((z - x) ^ 2)⁻¹)
    (FormalMultilinearSeries.ofScalars ℂ fun n ↦ (z ^ (n + 2))⁻¹ * (↑n + 1)) 0 ‖z‖ₑ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case inr
x : ℝ
hx✝ : x ≠ 0
p : ℝ
hx : 0 < x
⊢ HasStrictDerivAt (fun x ↦ x ^ p) (p * x ^ (p - 1)) x

Tactic:
simpa using

Goal state after:
case inr
x : ℝ
hx✝ : x ≠ 0
p : ℝ
hx : 0 < x
⊢ HasStrictDerivAt (fun x ↦ x ^ p) (p * x ^ (p - 1)) x
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: ⊢ HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ 2) (FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑n + 1) 0 1

Tactic:
simpa using

Goal state after:
⊢ HasFPowerSeriesOnBall (fun x ↦ ((1 - x) ^ 2)⁻¹) (FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑n + 1) 0 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: a : ℝ
ha : 0 < a
x : ℝ
⊢ HasStrictDerivAt (fun x ↦ a ^ x) (a ^ x * log a) x

Tactic:
simpa using

Goal state after:
a : ℝ
ha : 0 < a
x : ℝ
⊢ HasStrictDerivAt (fun x ↦ a ^ x) (a ^ x * log a) x
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case refine_1
w x : ℂ
hw : w ≠ x
⊢ HasFPowerSeriesOnBall (fun z ↦ 1 / (z - w) ^ 2)
    (FormalMultilinearSeries.ofScalars ℂ fun i ↦ (↑i + 1) * (w - x) ^ (-↑(i + 2))) x ‖w - x‖ₑ

Tactic:
simpa using

Goal state after:
case refine_1
w x : ℂ
hw : w ≠ x
⊢ HasFPowerSeriesOnBall (fun z ↦ 1 / (z - w) ^ 2)
    (FormalMultilinearSeries.ofScalars ℂ fun i ↦ (↑i + 1) * ((w - x) ^ (i + 2))⁻¹) x ‖w - x‖ₑ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

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

Tactic:
simpa using

Goal state after:
p : ℝ
h : ↑0 ≤ p
x : ℝ
⊢ 0 ≤ p
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: a : ℝ
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ ↑a)
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n))
    0 1
⊢ HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ a)
    (FormalMultilinearSeries.ofScalars ℝ fun n ↦ Ring.choose (a + ↑n - 1) n) 0 1

Tactic:
rw [← Complex.ofRealCLM.map_zero] at this

Goal state after:
a : ℝ
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ ↑a)
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n))
    (Complex.ofRealCLM 0) 1
⊢ HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ a)
    (FormalMultilinearSeries.ofScalars ℝ fun n ↦ Ring.choose (a + ↑n - 1) n) 0 1
Module: Mathlib.Analysis.Analytic.RadiusLiminf

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
p : FormalMultilinearSeries 𝕜 E F
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : ↑r < liminf (fun n ↦ 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop
n : ℕ
hn : ↑r < 1 / ↑(‖p n‖₊ ^ (1 / ↑n))
hn₀ : 0 < n
⊢ ‖‖p n‖ * ↑r ^ n‖ ≤ 1

Tactic:
simpa using

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
p : FormalMultilinearSeries 𝕜 E F
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : ↑r < liminf (fun n ↦ 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop
n : ℕ
hn : ↑r < 1 / ↑(‖p n‖₊ ^ (1 / ↑n))
hn₀ : 0 < n
⊢ ‖p n‖ * ↑r ^ n ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x : E
p : ℝ
m : ℕ
hf : ContDiffAt ℝ (↑m) f x
h : ↑m ≤ p
⊢ ContDiffAt ℝ (↑m) (fun x ↦ f x ^ p) x

Tactic:
rw [← contDiffWithinAt_univ] at *; exact hf.rpow_const_of_le h

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

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
p : FormalMultilinearSeries 𝕜 E F
⊢ p.radius⁻¹ = limsup (fun n ↦ ↑(‖p n‖₊ ^ (1 / ↑n))) atTop

Tactic:
simpa using

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
p : FormalMultilinearSeries 𝕜 E F
⊢ p.radius⁻¹ = limsup (fun n ↦ ↑(‖p n‖₊ ^ (↑n)⁻¹)) atTop
Module: Mathlib.Analysis.Analytic.Binomial

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

Tactic:
rw [← Complex.ofRealCLM.map_zero] at this

Goal state after:
a : ℕ
r : ℝ
hr : r ≠ 0
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (↑r - x) ^ (a + 1))
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ (↑r ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)))
    (Complex.ofRealCLM 0) ‖↑r‖ₑ
⊢ HasFPowerSeriesOnBall (fun x ↦ 1 / (r - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℝ fun n ↦ (r ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)) 0 ‖r‖ₑ