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 : ‖y‖ₑ + ‖z‖ₑ < r
⊢ f (x + y + z) = (p.changeOrigin y).sum z

Tactic:
p.changeOrigin_eval (hz.trans_le hf.r_le),

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.sum (y + 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
n : ℕ
r : ℝ≥0∞
finite : ∀ (m : ℕ), n ≤ m → p m = 0
pos : 0 < r
sum_eq : ∀ y ∈ Metric.eball 0 r, (∑ i ∈ Finset.range n, (p i) fun x ↦ y) = f (x + y)
y✝ : E
hy : y✝ ∈ Metric.eball 0 r
m : ℕ
hm : m ∉ Finset.range n
⊢ ((p m) fun x ↦ y✝) = 0

Tactic:
Finset.mem_range,

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
x : E
n : ℕ
r : ℝ≥0∞
finite : ∀ (m : ℕ), n ≤ m → p m = 0
pos : 0 < r
sum_eq : ∀ y ∈ Metric.eball 0 r, (∑ i ∈ Finset.range n, (p i) fun x ↦ y) = f (x + y)
y✝ : E
hy : y✝ ∈ Metric.eball 0 r
m : ℕ
hm : ¬m < n
⊢ ((p m) fun x ↦ y✝) = 0
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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x : E
m : ℕ
hm : m ∉ Finset.range n
⊢ ((p m) fun x_1 ↦ x) = 0

Tactic:
Finset.mem_range,

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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x : E
m : ℕ
hm : ¬m < n
⊢ ((p m) fun x_1 ↦ x) = 0
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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
x : E
x✝ : Fin k → E
m : ℕ
hm : m ∉ Finset.range (n - k)
⊢ ((p.changeOriginSeries k m) fun x_1 ↦ x) = 0

Tactic:
Finset.mem_range,

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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
x : E
x✝ : Fin k → E
m : ℕ
hm : ¬m < n - k
⊢ ((p.changeOriginSeries k m) fun x_1 ↦ x) = 0
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: case neg.refine_1.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
r' : ℝ≥0
hr' : r' * r < 1
hrz : ¬r' = 0
⊢ ∀ᶠ (n : ℕ) in atTop, ‖‖c n‖ * ↑r' ^ n‖ ≠ 0

Tactic:
refine (hc.eventually_ne (NNReal.coe_ne_zero.mpr hr)).mp (Eventually.of_forall ?_)

Goal state after:
case neg.refine_1.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
r' : ℝ≥0
hr' : r' * r < 1
hrz : ¬r' = 0
⊢ ∀ (x : ℕ), ‖c x.succ‖ / ‖c x‖ ≠ 0 → ‖‖c x‖ * ↑r' ^ x‖ ≠ 0
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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
finsupp : (Function.support f).Finite
hfkl : ∀ (k l : ℕ), HasSum (fun x ↦ f ⟨k, ⟨l, x⟩⟩) (((p.changeOriginSeries k l) fun x_1 ↦ x) fun x ↦ y)
k m : ℕ
hm : m ∉ Finset.range n
⊢ ((p.changeOriginSeries k m) fun x_1 ↦ x) = 0

Tactic:
Finset.mem_range,

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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
finsupp : (Function.support f).Finite
hfkl : ∀ (k l : ℕ), HasSum (fun x ↦ f ⟨k, ⟨l, x⟩⟩) (((p.changeOriginSeries k l) fun x_1 ↦ x) fun x ↦ y)
k m : ℕ
hm : ¬m < n
⊢ ((p.changeOriginSeries k m) fun x_1 ↦ x) = 0
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 < (ofScalars E c).radius
this : 0 < r
hc : ∀ᶠ (x : ℕ) in atTop, ‖‖ofScalars E c x‖ * ↑r ^ x‖ = 0
n : ℕ
hc' : ‖c n‖ = 0 ∨ ‖↑r ^ n‖ = 0
⊢ 0 = ‖c n.succ‖ / ‖c n‖

Tactic:
cases hc'

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
hc : ∀ᶠ (x : ℕ) in atTop, ‖‖ofScalars E c x‖ * ↑r ^ x‖ = 0
n : ℕ
h✝ : ‖c n‖ = 0
⊢ 0 = ‖c n.succ‖ / ‖c n‖

case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
hc : ∀ᶠ (x : ℕ) in atTop, ‖‖ofScalars E c x‖ * ↑r ^ x‖ = 0
n : ℕ
h✝ : ‖↑r ^ n‖ = 0
⊢ 0 = ‖c n.succ‖ / ‖c n‖
Module: Mathlib.Analysis.Analytic.Basic

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
f : E → F
s : Set E
g : F →L[𝕜] G
h : AnalyticOnNhd 𝕜 f s
⊢ AnalyticOnNhd 𝕜 (⇑g ∘ f) s

Tactic:
by
  rintro x hx
  rcases h x hx with ⟨p, r, hp⟩
  exact ⟨g.compFormalMultilinearSeries p, r, g.comp_hasFPowerSeriesOnBall hp⟩

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

Goal state before:
pp: case h₀
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
b : Composition n
a✝ : b ∈ Finset.univ
hb : b ≠ Composition.ones n
k : ℕ
hk : k ∈ b.blocks
lt_k : 1 < k
i : Fin b.blocks.length
hi : b.blocks[i] = k
j : Fin b.length := ⟨↑i, ⋯⟩
A : 1 < b.blocksFun j
v : Fin n → E
⊢ (p.compAlongComposition (id 𝕜 E x) b) v = 0 v

Tactic:
compAlongComposition_apply,

Goal state after:
case h₀
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
b : Composition n
a✝ : b ∈ Finset.univ
hb : b ≠ Composition.ones n
k : ℕ
hk : k ∈ b.blocks
lt_k : 1 < k
i : Fin b.blocks.length
hi : b.blocks[i] = k
j : Fin b.length := ⟨↑i, ⋯⟩
A : 1 < b.blocksFun j
v : Fin n → E
⊢ (p b.length) ((id 𝕜 E x).applyComposition b v) = 0 v
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case inr
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
v : Fin n → E
⊢ ((id 𝕜 F ((p 0) v0)).compAlongComposition p (Composition.single n n_pos)) v = (p n) v

Tactic:
compAlongComposition_apply,

Goal state after:
case inr
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
v : Fin n → E
⊢ (id 𝕜 F ((p 0) v0) (Composition.single n n_pos).length) (p.applyComposition (Composition.single n n_pos) v) = (p n) v
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case inr.h₀
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
b : Composition n
a✝ : b ∈ Finset.univ
hb : b ≠ Composition.single n n_pos
A : 1 < b.length
v : Fin n → E
⊢ ((id 𝕜 F ((p 0) v0)).compAlongComposition p b) v = 0 v

Tactic:
compAlongComposition_apply,

Goal state after:
case inr.h₀
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
b : Composition n
a✝ : b ∈ Finset.univ
hb : b ≠ Composition.single n n_pos
A : 1 < b.length
v : Fin n → E
⊢ (id 𝕜 F ((p 0) v0) b.length) (p.applyComposition b v) = 0 v
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
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFPowerSeriesAt g q (f x)
hf : HasFPowerSeriesAt f p x
⊢ HasFPowerSeriesAt (g ∘ f) (q.comp p) x

Tactic:
rw [← hasFPowerSeriesWithinAt_univ] at hf hg ⊢
  apply hg.comp hf (by simp)

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

Goal state before:
pp: case zero.succ
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
IH :
  ∀ (hi : i < b.length),
    0 < b.blocksFun ⟨i, hi⟩ →
      (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
hi : i + 1 < b.length
hj : 0 < b.blocksFun ⟨i + 1, hi⟩
A : i < b.length
B : i < (List.map sum (a.blocks.splitWrtComposition b)).length
C : 0 < b.blocksFun ⟨i, A⟩
⊢ (take (take (i + 1) b.blocks).sum a.blocks).sum = (take (i + 1) (List.map sum (a.blocks.splitWrtComposition b))).sum

Tactic:
rw [sum_take_succ _ _ B, ← IH A C]

Goal state after:
case zero.succ
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
IH :
  ∀ (hi : i < b.length),
    0 < b.blocksFun ⟨i, hi⟩ →
      (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
hi : i + 1 < b.length
hj : 0 < b.blocksFun ⟨i + 1, hi⟩
A : i < b.length
B : i < (List.map sum (a.blocks.splitWrtComposition b)).length
C : 0 < b.blocksFun ⟨i, A⟩
⊢ (take (take (i + 1) b.blocks).sum a.blocks).sum =
    (take (take i b.blocks).sum a.blocks).sum + (List.map sum (a.blocks.splitWrtComposition b))[i]
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
n✝ n : ℕ
a : Composition n
b : Composition a.length
B : (a.gather b).length = b.blocks.length
| b.blocks

Tactic:
← ofFn_getElem (xs := b.blocks)

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
n✝ n : ℕ
a : Composition n
b : Composition a.length
B : (a.gather b).length = b.blocks.length
| ofFn fun i ↦ b.blocks[↑i]
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
A : Type u_7
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ 1 ≤ (formalMultilinearSeries_geometric 𝕜 A).radius

Tactic:
by
  convert!
    formalMultilinearSeries_geometric_eq_ofScalars 𝕜 A ▸
      FormalMultilinearSeries.inv_le_ofScalars_radius_of_tendsto A _ one_ne_zero (by simp)
  simp

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
𝕝 : Type u_8
inst✝¹ : NormedDivisionRing 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
z : 𝕝
hz : z ≠ 0
⊢ AnalyticAt 𝕜 Inv.inv z

Tactic:
by
  convert! analyticAt_inverse (𝕜 := 𝕜) (Units.mk0 _ hz)
  exact Ring.inverse_eq_inv'.symm

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
s : Set E
n : ℤ
h₁f : AnalyticWithinAt 𝕜 f s z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
| AnalyticWithinAt 𝕜 (f ^ (- -n)) s z

Tactic:
arg 2; intro x; rw [zpow_neg]

Goal state after:
𝕜 : 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
hn : ¬0 ≤ n
x : E
| (f ^ (-n))⁻¹ x
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
hn : ¬0 ≤ n
| AnalyticAt 𝕜 (f ^ (- -n)) z

Tactic:
arg 2; intro x; rw [zpow_neg]

Goal state after:
𝕜 : 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
hn : ¬0 ≤ n
x : E
| (f ^ (-n))⁻¹ x
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 g : E → 𝕝
z : E
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
⊢ AnalyticAt 𝕜 g z ↔ AnalyticAt 𝕜 (f * g) z

Tactic:
by
  simp_rw [← smul_eq_mul]
  exact analyticAt_iff_analytic_smul h₁f h₂f

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

Goal state before:
pp: 𝕜 : 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
⊢ HasFTaylorSeriesUpToOn 0 f p s ↔ ContinuousOn f s ∧ ∀ x ∈ s, (p x 0).curry0 = f x

Tactic:
by
  refine ⟨fun H => ⟨H.continuousOn, H.zero_eq⟩, fun H =>
      ⟨H.2, fun m hm => False.elim (not_le.2 hm bot_le), fun m hm ↦ ?_⟩⟩
  obtain rfl : m = 0 := mod_cast hm.antisymm zero_le
  have : EqOn (p · 0) ((continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f) s := fun x hx ↦
    (continuousMultilinearCurryFin0 𝕜 E F).eq_symm_apply.2 (H.2 x hx)
  rw [continuousOn_congr this, LinearIsometryEquiv.comp_continuousOn_iff]
  exact H.1

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

Goal state before:
pp: 𝕜 : 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
N : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
k : ℕ
⊢ HasFTaylorSeriesUpToOn N f p s ↔ ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + k)) f p s

Tactic:
by
  constructor
  · intro H n
    apply H.of_le (natCast_le_of_coe_top_le_withTop hN _)
  · intro H
    constructor
    · exact (H 0).zero_eq
    · intro m _
      apply (H m.succ).fderivWithin m (by norm_cast; lia)
    · intro m _
      apply (H m).cont m (by simp)

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 : 𝕜
⊢ iteratedFDerivWithin 𝕜 (n + 1) (fun x ↦ f (-x)) s a = (-1) ^ (n + 1) • iteratedFDerivWithin 𝕜 (n + 1) f (-s) (-a)

Tactic:
have ih' : iteratedFDerivWithin 𝕜 n (fun x => f (-x)) s
        = fun a ↦ (-1 : 𝕜) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a) := by
      ext b
      rw [ih b]
    set g := fun a ↦ iteratedFDerivWithin 𝕜 n f (-s) a
    rw [iteratedFDerivWithin_succ_eq_comp_left, iteratedFDerivWithin_succ_eq_comp_left,
      Function.comp_apply, Function.comp_apply, ih', ← Pi.smul_def,
      fderivWithin_const_smul_field' ((-1 : 𝕜) ^ n) (f := fun a ↦ g (-a)),
      fderivWithin_comp_neg (f := g), ← neg_one_smul 𝕜 (fderivWithin 𝕜 _ (-s) (-a)),
      ← mul_smul _ (-1), ← pow_succ (-1) n, map_smul]

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: case pos
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hf : DifferentiableWithinAt 𝕜 f s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x

Tactic:
exact (hc.hasDerivWithinAt.smul hf.hasDerivWithinAt).derivWithin hsx

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

Goal state before:
pp: 𝕜 : 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 ι
inst✝ : DecidableEq ι
fa : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)
f : ContinuousMultilinearMap 𝕜 (fun x ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) F :=
  (ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F)).continuousMultilinearMapOption
⊢ HasStrictFDerivAt (fun fx ↦ fx.1 fx.2)
    (apply 𝕜 E F fa.2 ∘SL ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i) +
      fa.1.linearDeriv fa.2 ∘SL ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i))
    fa

Tactic:
have Hf := (f.hasStrictFDerivAt (fun _ ↦ fa)).comp (f := fun fx _ ↦ fx) fa
    (hasStrictFDerivAt_pi.2 fun _ ↦ hasStrictFDerivAt_id _)

Goal state after:
𝕜 : 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 ι
inst✝ : DecidableEq ι
fa : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)
f : ContinuousMultilinearMap 𝕜 (fun x ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) F :=
  (ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F)).continuousMultilinearMapOption
Hf :
  HasStrictFDerivAt (fun x ↦ f fun x_1 ↦ x)
    ((f.linearDeriv fun x ↦ fa) ∘SL
      ContinuousLinearMap.pi fun x ↦ ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    fa
⊢ HasStrictFDerivAt (fun fx ↦ fx.1 fx.2)
    (apply 𝕜 E F fa.2 ∘SL ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i) +
      fa.1.linearDeriv fa.2 ∘SL ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i))
    fa
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module k E
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : PartialOrder E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : PosSMulMono k E
f : k → E
x y : k
s : Set k
hf : StrictAntiOn f s
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
⊢ slope f x y < 0

Tactic:
by
  simpa using hf.neg.slope_pos hx hy hxy

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
hs : x ∉ s
⊢ HasDerivWithinAt f f' s x ↔ Tendsto (slope f x) (𝓝[s] x) (𝓝 f')

Tactic:
by
  rw [hasDerivWithinAt_iff_tendsto_slope, sdiff_singleton_eq_self hs]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
hd : HasStrictFDerivAt d d' x
⊢ HasStrictFDerivAt (c * d) (c x •> d' + d x •> c') x

Tactic:
convert! hc.mul' hd

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
hd : HasStrictFDerivAt d d' x
⊢ HSMul.hSMul (d x) = HSMul.hSMul (MulOpposite.op (d x))
Module: Mathlib.Analysis.Calculus.FDeriv.Mul

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
s : Set E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
hd : HasFDerivWithinAt d d' s x
⊢ HasFDerivWithinAt (c * d) (c x •> d' + d x •> c') s x

Tactic:
convert! hc.mul' hd

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
s : Set E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
hd : HasFDerivWithinAt d d' s x
⊢ HSMul.hSMul (d x) = HSMul.hSMul (MulOpposite.op (d x))