mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Analytic.ChangeOrigin

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : z ∈ Metric.eball 0 (r - ‖y‖ₑ)
⊢ f (x + y + z) = (p.changeOrigin y).sum z

Tactic:
rw [mem_eball_zero_iff, lt_tsub_iff_right, add_comm] at hz

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : ‖y‖ₑ + ‖z‖ₑ < r
⊢ f (x + y + z) = (p.changeOrigin y).sum z
Module: Mathlib.Analysis.Analytic.CPolynomialDef

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : ∀ y ∈ Metric.eball x r, f y = 0
r_pos : 0 < r
hp : ∀ (n : ℕ), p n = 0
⊢ HasFiniteFPowerSeriesOnBall f p x 0 r

Tactic:
by
  refine ⟨⟨?_, r_pos, ?_⟩, fun n _ ↦ hp n⟩
  · rw [p.radius_eq_top_of_forall_image_add_eq_zero 0 (fun n ↦ by rw [add_zero]; exact hp n)]
    exact le_top
  · intro y hy
    rw [hf (x + y)]
    · convert! hasSum_zero
      rw [hp, zero_apply]
    · rwa [Metric.mem_eball, edist_eq_enorm_sub, add_comm, add_sub_cancel_right,
        ← edist_zero_right, ← Metric.mem_eball]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
x y : E
hf : HasFiniteFPowerSeriesOnBall f p x n r
h : ↑‖y‖₊ < r
z : E
hz : z ∈ Metric.eball 0 (r - ↑‖y‖₊)
⊢ f (x + y + z) = (p.changeOrigin y).sum z

Tactic:
rw [mem_eball_zero_iff, lt_tsub_iff_right, add_comm] at hz

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
x y : E
hf : HasFiniteFPowerSeriesOnBall f p x n r
h : ↑‖y‖₊ < r
z : E
hz : ↑‖y‖₊ + ‖z‖ₑ < r
⊢ f (x + y + z) = (p.changeOrigin y).sum z
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0∞
hr : r = ∞
hc' : Tendsto (fun n ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 ∞)
⊢ Tendsto (fun n ↦ ‖c (n + 1).succ‖ / ‖c (n + 1)‖) atTop atTop

Tactic:
refine tendsto_ofReal_nhds_top.mp (Tendsto.congr' ?_ ((tendsto_add_atTop_iff_nat 1).mpr hc'))

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0∞
hr : r = ∞
hc' : Tendsto (fun n ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 ∞)
⊢ (fun n ↦ ENNReal.ofReal ‖c (n + 1).succ‖ / ENNReal.ofReal ‖c (n + 1)‖) =ᶠ[atTop] fun x ↦
    ENNReal.ofReal (‖c (x + 1).succ‖ / ‖c (x + 1)‖)
Module: Mathlib.Analysis.Analytic.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : y ∈ Metric.eball 0 r
h'y : x + y ∈ insert x s
A✝ : Tendsto (fun z ↦ p.partialSum z.1 y) (atTop ×ˢ 𝓝 y) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : ↑r' < r
yr'_2 : ‖y‖ < ↑r'
S : Summable fun n ↦ ‖p n‖ * ↑r' ^ n
k : ℕ
hk : ∑' (n : ℕ), ‖p (n + k)‖ * ↑r' ^ (n + k) < ε / 4
A : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4
B : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, ‖z.2‖₊ < r'
C : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, k ≤ z.1
n : ℕ
z : E
h'z : ‖(n, z).2‖₊ < r'
hkn : k ≤ (n, z).1
hz : ‖p.partialSum k z - p.partialSum k y‖ < ε / 4
w : E
hw : ‖w‖₊ < r'
⊢ ∑ i ∈ Finset.range (n - k), ‖p (i + k)‖ * ‖w‖ ^ (i + k) ≤ ∑ i ∈ Finset.range (n - k), ‖p (i + k)‖ * ↑r' ^ (i + k)

Tactic:
gcongr with i _hi; simpa [← coe_nnnorm] using hw.le

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : C > 0
hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n
y : E
hy : y ∈ Metric.ball 0 ↑r'
n : ℕ
ys : x + y ∈ insert x s
⊢ ‖y‖ < ↑r'

Tactic:
rwa [ball_zero_eq] at hy

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : ↑r' < r
⊢ ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n

Tactic:
simpa using hf.uniform_geometric_approx h

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
hr : ↑r' < r
hr'0 : 0 < r'
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : 0 < C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / ↑r' ^ n
L : E × E → ℝ := fun y ↦ C * (a / ↑r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * (a / (1 - a) ^ 2 + 2 / (1 - a))
y : E × E
hy' : ‖y - (x, x)‖₊ < r'
ys : y ∈ insert x s ×ˢ insert x s
hy : y ∈ Metric.eball x r ×ˢ Metric.eball x r
A : ℕ → F := fun n ↦ ((p n) fun x_1 ↦ y.1 - x) - (p n) fun x_1 ↦ y.2 - x
hA : HasSum (fun n ↦ A (n + 2)) (f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2)
B : ℕ → ℝ := fun n ↦ C * (a / ↑r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * ((↑n + 2) * a ^ n)
hAB : ∀ (n : ℕ), ‖A (n + 2)‖ ≤ B n
hBL : HasSum B (L y)
⊢ ‖f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2‖ ≤ L y

Tactic:
exact hA.norm_le_of_bounded hBL hAB

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
hr : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
⊢ ↑r ≤ (q.comp p).radius

Tactic:
refine
    le_radius_of_bound_nnreal _
      (∑' i : Σ n, Composition n, ‖compAlongComposition q p i.snd‖₊ * r ^ i.fst) fun n => ?_

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
hr : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
n : ℕ
⊢ ‖q.comp p n‖₊ * r ^ n ≤ ∑' (i : (n : ℕ) × Composition n), ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: α : Type u_6
inst✝ : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H : ⟨k, blocks_fun⟩ ∈ compPartialSumSource m M N
k' : ℕ
blocks_fun' : Fin k' → ℕ
H' : ⟨k', blocks_fun'⟩ ∈ compPartialSumSource m M N
heq : compChangeOfVariables m M N ⟨k, blocks_fun⟩ H = compChangeOfVariables m M N ⟨k', blocks_fun'⟩ H'
this : ⟨k, blocks_fun⟩.fst = (compChangeOfVariables m M N ⟨k, blocks_fun⟩ H).snd.length
⊢ k = k'

Tactic:
heq,

Goal state after:
α : Type u_6
inst✝ : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H : ⟨k, blocks_fun⟩ ∈ compPartialSumSource m M N
k' : ℕ
blocks_fun' : Fin k' → ℕ
H' : ⟨k', blocks_fun'⟩ ∈ compPartialSumSource m M N
heq : compChangeOfVariables m M N ⟨k, blocks_fun⟩ H = compChangeOfVariables m M N ⟨k', blocks_fun'⟩ H'
this : ⟨k, blocks_fun⟩.fst = (compChangeOfVariables m M N ⟨k', blocks_fun'⟩ H').snd.length
⊢ k = k'
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case h
⊢ Monotone fun p ↦ compPartialSumTarget 0 p.1 p.2

Tactic:
intro m n hmn a ha

Goal state after:
case h
m n : ℕ × ℕ
hmn : m ≤ n
a : (n : ℕ) × Composition n
ha : a ∈ (fun p ↦ compPartialSumTarget 0 p.1 p.2) m
⊢ a ∈ (fun p ↦ compPartialSumTarget 0 p.1 p.2) n
Module: Mathlib.Analysis.Analytic.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
⊢ TendstoLocallyUniformlyOn (fun n y ↦ p.partialSum n y) (fun y ↦ f (x + y)) atTop (Metric.eball 0 r)

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf
  simpa using hf.tendstoLocallyUniformlyOn

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

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
g : F → G
g' : F →L[𝕜] G
L' : Filter (F × F)
hg : HasFDerivAtFilter g g' L'
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L'
⊢ (fun p ↦ g (f p.1) - g (f p.2) - g' (f p.1 - f p.2)) =o[𝕜; L] fun p ↦ p.1 - p.2

Tactic:
case =>

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

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
g : F → G
g' : F →L[𝕜] G
L' : Filter (F × F)
hg : HasFDerivAtFilter g g' L'
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L'
⊢ (fun p ↦ g' (f p.1 - f p.2 - f' (p.1 - p.2))) =o[𝕜; L] fun p ↦ p.1 - p.2

Tactic:
case =>

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

Goal state before:
pp: case a.left
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < (p.prod q).radius
this : (fun n ↦ ‖p.prod q n‖ * ↑r ^ n) =o[atTop] fun x ↦ 1
⊢ ↑r ≤ p.radius

pp: case a.right
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < (p.prod q).radius
this : (fun n ↦ ‖p.prod q n‖ * ↑r ^ n) =o[atTop] fun x ↦ 1
⊢ ↑r ≤ q.radius

Tactic:
all_goals
      apply FormalMultilinearSeries.le_radius_of_isBigO
      refine (isBigO_of_le _ fun n ↦ ?_).trans this.isBigO
      rw [norm_mul, norm_norm, norm_mul, norm_norm]
      refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
      rw [FormalMultilinearSeries.prod, ContinuousMultilinearMap.opNorm_prod]

Goal state after:
case a.left
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < (p.prod q).radius
this : (fun n ↦ ‖p.prod q n‖ * ↑r ^ n) =o[atTop] fun x ↦ 1
n : ℕ
⊢ ‖p n‖ ≤ max ‖p n‖ ‖q n‖

case a.right
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < (p.prod q).radius
this : (fun n ↦ ‖p.prod q n‖ * ↑r ^ n) =o[atTop] fun x ↦ 1
n : ℕ
⊢ ‖q n‖ ≤ max ‖p n‖ ‖q n‖
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕝 : Type u_8
inst✝¹ : NormedDivisionRing 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
s : Set E
n : ℤ
h₁f : AnalyticWithinAt 𝕜 f s z
h₂f : f z ≠ 0
⊢ AnalyticWithinAt 𝕜 (f ^ n) s z

Tactic:
by_cases hn : 0 ≤ n
  · exact zpow_nonneg h₁f hn
  · rw [(Int.eq_neg_comm.mp rfl : n = -(-n))]
    conv => arg 2; intro x; rw [zpow_neg]
    exact (h₁f.zpow_nonneg (by linarith)).inv (zpow_ne_zero (-n) h₂f)

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕝 : Type u_8
inst✝¹ : NormedDivisionRing 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
n : ℤ
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
⊢ AnalyticAt 𝕜 (f ^ n) z

Tactic:
by_cases hn : 0 ≤ n
  · exact zpow_nonneg h₁f hn
  · rw [(Int.eq_neg_comm.mp rfl : n = -(-n))]
    conv => arg 2; intro x; rw [zpow_neg]
    exact (h₁f.zpow_nonneg (by linarith)).inv (zpow_ne_zero (-n) h₂f)

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
c : F
h : HasFDerivWithinAt f f' s x
hf' : ∃ C, AntilipschitzWith C ⇑f'
⊢ ∀ᶠ (z : E) in 𝓝[s \ {x}] x, f z ≠ c

Tactic:
by
  rw [← eventually_map (m := f) (P := fun z ↦ z ≠ c)]
  apply Eventually.filter_mono (h.tendsto_nhdsWithin_nhdsNE hf')
  rcases eq_or_ne (f x) c with rfl | hc
  · exact eventually_mem_nhdsWithin
  · exact eventually_ne_nhdsWithin hc

Goal state after:
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: case mpr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.1 p.2 < ε}
this : r ∈ 𝓤 ℝ
⊢ s ∈ 𝓤 (Completion α)

Tactic:
have T := uniformContinuous_def.1 (@Completion.uniformContinuous_dist α _) r this

Goal state after:
case mpr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.1 p.2 < ε}
this : r ∈ 𝓤 ℝ
T : {x | (dist x.1.1 x.1.2, dist x.2.1 x.2.2) ∈ r} ∈ 𝓤 (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α)
Module: Mathlib.Analysis.Normed.Group.Completion

Goal state before:
pp: case ih
E : Type u_1
inst✝ : SeminormedAddCommGroup E
a✝ b✝ : E
⊢ dist ↑a✝ ↑b✝ = ‖↑(-a✝) + ↑b✝‖

Tactic:
← Completion.coe_add,

Goal state after:
case ih
E : Type u_1
inst✝ : SeminormedAddCommGroup E
a✝ b✝ : E
⊢ dist ↑a✝ ↑b✝ = ‖↑(-a✝ + b✝)‖
Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
x : E
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
c' : E →L[𝕜] G →L[𝕜] H
u : E → G
u' : E →L[𝕜] G
hc : HasFDerivAt c c' x
hu : HasFDerivAt u u' x
⊢ HasFDerivAt (fun y ↦ (c y) (u y)) (c x ∘SL u' + c'.flip (u x)) x

Tactic:
by
  -- `by exact` to solve unification issues.
  exact (isBoundedBilinearMap_apply.hasFDerivAt (c x, u x)).comp x (hc.prodMk hu)

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case neg
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
h :
  HasFTaylorSeriesUpToOn (↑n) f p s ∧
    (∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y n) (p x n.succ).curryLeft s x) ∧ ContinuousOn (fun x ↦ p x (n + 1)) s
m : ℕ
hm : ↑m < ↑n + 1
h' : ¬m < n
this : m = n
⊢ ∀ x ∈ s, HasFDerivWithinAt (fun x ↦ p x n) (p x n.succ).curryLeft s x

Tactic:
exact h.2.1

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case mpr.cont
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, (p x 0).curry0 = f x
Hfderiv_zero : ∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft s x
Htaylor : HasFTaylorSeriesUpToOn (↑n) (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) s
⊢ ∀ (m : ℕ), ↑m ≤ ↑(n + 1) → ContinuousOn (fun x ↦ p x m) s

Tactic:
intro m (hm : (m : ℕ∞ω) ≤ n.succ)
      rcases m with - | m
      · have : DifferentiableOn 𝕜 (fun x => p x 0) s := fun x hx =>
          (Hfderiv_zero x hx).differentiableWithinAt
        exact this.continuousOn
      · refine (continuousMultilinearCurryRightEquiv' 𝕜 m E F).comp_continuousOn_iff.mp ?_
        refine Htaylor.cont _ ?_
        rw [Nat.cast_le] at hm ⊢
        exact Nat.lt_succ_iff.mp hm

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case succ
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
ih : ∀ (a : 𝕜), iteratedFDerivWithin 𝕜 n (fun x ↦ f (-x)) s a = (-1) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a)
a : 𝕜
ih' : iteratedFDerivWithin 𝕜 n (fun x ↦ f (-x)) s = fun a ↦ (-1) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a)
g : 𝕜 → 𝕜 [×n]→L[𝕜] F := fun a ↦ iteratedFDerivWithin 𝕜 n f (-s) a
⊢ (continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ 𝕜) F).symm
      (fderivWithin 𝕜 (fun a ↦ (-1) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a)) s a) =
    (-1) ^ (n + 1) •
      (continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ 𝕜) F).symm
        (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f (-s)) (-s) (-a))

Tactic:
← Pi.smul_def,

Goal state after:
case succ
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
ih : ∀ (a : 𝕜), iteratedFDerivWithin 𝕜 n (fun x ↦ f (-x)) s a = (-1) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a)
a : 𝕜
ih' : iteratedFDerivWithin 𝕜 n (fun x ↦ f (-x)) s = fun a ↦ (-1) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a)
g : 𝕜 → 𝕜 [×n]→L[𝕜] F := fun a ↦ iteratedFDerivWithin 𝕜 n f (-s) a
⊢ (continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ 𝕜) F).symm
      (fderivWithin 𝕜 ((-1) ^ n • fun a ↦ iteratedFDerivWithin 𝕜 n f (-s) (-a)) s a) =
    (-1) ^ (n + 1) •
      (continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ 𝕜) F).symm
        (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f (-s)) (-s) (-a))
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
x : E
inst✝ : CompleteSpace F
h : AnalyticAt 𝕜 f x
⊢ AnalyticAt 𝕜 (fderiv 𝕜 f) x

Tactic:
rcases h with ⟨p, r, hp⟩
  exact hp.fderiv.analyticAt

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
n : ℕ
IH : AnalyticOnNhd 𝕜 (iteratedFDeriv 𝕜 n f) s
⊢ (E →L[𝕜] E [×n]→L[𝕜] F) →L[𝕜] E [×n + 1]→L[𝕜] F

Tactic:
case =>

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticWithinAt 𝕜 f s x
g : E → F
fg : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
v : Set E
vx : v ∈ 𝓝 x
hv : AnalyticOnNhd 𝕜 g v
i : ℕ
⊢ AnalyticOn 𝕜 (fun x ↦ ftaylorSeries 𝕜 g x i) (insert x s ∩ v)

Tactic:
· exact (hv.iteratedFDeriv i).analyticOn.mono Set.inter_subset_right

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ
IH : CPolynomialOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ (E →L[𝕜] E [×n]→L[𝕜] F) →L[𝕜] E [×n + 1]→L[𝕜] F

Tactic:
case =>

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

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : IsEmpty ι
this : ∀ (l : ℕ), 1 + l ≠ Fintype.card ι
⊢ (∑' (n : ℕ), 0) (Fin.snoc 0 y) = 0

Tactic:
tsum_zero

Goal state after:
case inl
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : IsEmpty ι
this : ∀ (l : ℕ), 1 + l ≠ Fintype.card ι
⊢ 0 (Fin.snoc 0 y) = 0