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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
𝕜' : Type u_6
c : 𝕜'
inst✝³ : NormedDivisionRing 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : NormSMulClass 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
hc : c ≠ 0
⊢ (c • p).radius = p.radius

Tactic:
apply eq_of_le_of_ge _ radius_le_smul

Goal state after:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
𝕜' : Type u_6
c : 𝕜'
inst✝³ : NormedDivisionRing 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : NormSMulClass 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
hc : c ≠ 0
⊢ (c • p).radius ≤ p.radius
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Nontrivial F
p : FormalMultilinearSeries 𝕜 F G
u : E ≃L[𝕜] F
⊢ (p.compContinuousLinearMap ↑u).radius ≤ ‖↑u.symm‖ₑ * p.radius

Tactic:
have := (p.compContinuousLinearMap u.toContinuousLinearMap).div_le_radius_compContinuousLinearMap
    u.symm.toContinuousLinearMap
  simp only [compContinuousLinearMap_comp, ContinuousLinearEquiv.coe_comp_coe_symm,
    compContinuousLinearMap_id] at this
  rwa [ENNReal.div_le_iff' (by simpa [DFunLike.ext_iff] using exists_ne 0) (by simp)] at this

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
s : Set E
hf : AnalyticOnNhd 𝕜 f s
y x : E
hx : x + -y ∈ s
⊢ AnalyticAt 𝕜 (fun z ↦ f (z - y)) x

Tactic:
show x = (x - y) + y by abel

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
s : Set E
hf : AnalyticOnNhd 𝕜 f s
y x : E
hx : x + -y ∈ s
⊢ AnalyticAt 𝕜 (fun z ↦ f (z - y)) (x - y + y)
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
s : Set E
hf : AnalyticOn 𝕜 f s
y x : E
hx : x + -y ∈ s
⊢ AnalyticWithinAt 𝕜 (fun z ↦ f (z - y)) (s + {y}) x

Tactic:
show x = (x - y) + y by abel

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
s : Set E
hf : AnalyticOn 𝕜 f s
y x : E
hx : x + -y ∈ s
⊢ AnalyticWithinAt 𝕜 (fun z ↦ f (z - y)) (s + {y}) (x - y + y)
Module: Mathlib.Analysis.Analytic.Composition

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
x : E
n : ℕ
⊢ p.compAlongComposition (id 𝕜 E x) (Composition.ones n) = p n

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 ∈ Finset.univ, b ≠ Composition.ones n → p.compAlongComposition (id 𝕜 E x) b = 0

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 : ℕ
⊢ Composition.ones n ∉ Finset.univ → p.compAlongComposition (id 𝕜 E x) (Composition.ones n) = 0

Tactic:
· show compAlongComposition p (id 𝕜 E x) (Composition.ones n) = p n
    ext v
    rw [compAlongComposition_apply]
    apply p.congr (Composition.ones_length n)
    intros
    rw [applyComposition_ones]
    refine congr_arg v ?_
    rw [Fin.ext_iff, Fin.val_castLE, Fin.val_mk]

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 ∈ Finset.univ, b ≠ Composition.ones n → p.compAlongComposition (id 𝕜 E x) b = 0

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 : ℕ
⊢ Composition.ones n ∉ Finset.univ → p.compAlongComposition (id 𝕜 E x) (Composition.ones n) = 0
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 r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
hr : r' < r
⊢ ∃ C,
    ∀ y ∈ insert x s ∩ Metric.eball x r',
      ∀ z ∈ insert x s ∩ Metric.eball x r', ‖f y - f z - (p 1) fun x ↦ y - z‖ ≤ C * max ‖y - x‖ ‖z - x‖ * ‖y - z‖

Tactic:
have := hf.isBigO_image_sub_image_sub_deriv_principal hr

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
s : Set E
x : E
r r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
hr : r' < r
this :
  (fun y ↦ f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2) =O[𝓟 (Metric.eball (x, x) r' ∩ insert x s ×ˢ insert x s)] fun y ↦
    ‖y - (x, x)‖ * ‖y.1 - y.2‖
⊢ ∃ C,
    ∀ y ∈ insert x s ∩ Metric.eball x r',
      ∀ z ∈ insert x s ∩ Metric.eball x r', ‖f y - f z - (p 1) fun x ↦ y - z‖ ≤ C * max ‖y - x‖ ‖z - x‖ * ‖y - z‖
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case refine_2
m M N n : ℕ
c : Composition n
hi : ⟨n, c⟩ ∈ compPartialSumTargetSet m M N
⊢ (ofFn fun a ↦ c.blocks.get a) = c.blocks

Tactic:
conv_rhs => rw [← List.ofFn_get c.blocks]

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
⊢ TendstoUniformlyOn (fun n y ↦ p.partialSum n y) (fun y ↦ f (x + y)) atTop
    ((fun x_1 ↦ x + x_1) ⁻¹' insert x s ∩ Metric.ball 0 ↑r')

Tactic:
obtain ⟨a, ha, C, -, hp⟩ : ∃ a ∈ Ioo (0 : ℝ) 1, ∃ C > 0, ∀ y ∈ Metric.ball (0 : E) r', ∀ n,
    x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n := hf.uniform_geometric_approx h
  refine Metric.tendstoUniformlyOn_iff.2 fun ε εpos => ?_
  have L : Tendsto (fun n => (C : ℝ) * a ^ n) atTop (𝓝 ((C : ℝ) * 0)) :=
    tendsto_const_nhds.mul (tendsto_pow_atTop_nhds_zero_of_lt_one ha.1.le ha.2)
  rw [mul_zero] at L
  refine (L.eventually (gt_mem_nhds εpos)).mono fun n hn y hy => ?_
  rw [dist_eq_norm]
  exact (hp y hy.2 n hy.1).trans_lt hn

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
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
h : 0 < p.radius
y✝ : E
hy : y✝ ∈ Metric.eball 0 p.radius
⊢ HasSum (fun n ↦ (p n) fun x ↦ y✝) (p.sum y✝)

Tactic:
exact p.hasSum hy

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : AnalyticOn 𝕜 f s
x : E
m : x ∈ s
r : ℝ
r0 : r > 0
rs : ball x r ⊆ s
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p s x t
⊢ AnalyticAt 𝕜 f x

Tactic:
exact ⟨p, min (.ofReal r) t,
  { r_pos := lt_min (by positivity) fp.r_pos
    r_le := min_le_of_right_le fp.r_le
    hasSum := by
      intro y ym
      simp only [mem_eball, lt_min_iff, edist_lt_ofReal, dist_zero_right] at ym
      refine fp.hasSum ?_ ym.2
      apply mem_insert_of_mem
      apply rs
      simp only [mem_ball, dist_self_add_left, ym.1] }⟩

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
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
r : FormalMultilinearSeries 𝕜 G H
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : Fin n → E
f : (a : Composition n) × Composition a.length → H :=
  fun c ↦ (r c.snd.length) (q.applyComposition c.snd (p.applyComposition c.fst v))
g : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)) → H :=
  fun c ↦ (r c.fst.length) fun i ↦ (q (c.snd i).length) (p.applyComposition (c.snd i) (v ∘ ⇑(c.fst.embedding i)))
a : Composition n
b : Composition a.length
a✝ : ⟨a, b⟩ ∈ Finset.univ
i : ℕ
hi1 : i < b.length
hi2 : i < (a.gather b).length
j : ℕ
hj1 : j < b.blocksFun ⟨i, hi1⟩
hj2 : j < (a.sigmaCompositionAux b ⟨↑⟨i, hi1⟩, ⋯⟩).length
⊢ (p.applyComposition ⟨a, b⟩.fst v ∘ ⇑(⟨a, b⟩.snd.embedding ⟨i, hi1⟩)) ⟨j, hj1⟩ =
    p.applyComposition (⟨a.gather b, a.sigmaCompositionAux b⟩.snd ⟨i, hi2⟩)
      (v ∘ ⇑(⟨a.gather b, a.sigmaCompositionAux b⟩.fst.embedding ⟨i, hi2⟩)) ⟨j, hj2⟩

Tactic:
apply p.congr (blocksFun_sigmaCompositionAux a b _ _).symm

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
r : FormalMultilinearSeries 𝕜 G H
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : Fin n → E
f : (a : Composition n) × Composition a.length → H := ⋯
g : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)) → H := ⋯
a : Composition n
b : Composition a.length
a✝ : ⟨a, b⟩ ∈ Finset.univ
i : ℕ
hi1 : i < b.length
hi2 : i < (a.gather b).length
j : ℕ
hj1 : j < b.blocksFun ⟨i, hi1⟩
hj2 : j < (a.sigmaCompositionAux b ⟨↑⟨i, hi1⟩, ⋯⟩).length
⊢ ∀ (i_1 : ℕ) (him : i_1 < a.blocksFun ((b.embedding ⟨i, hi1⟩) ⟨j, hj1⟩))
    (hin : i_1 < (a.sigmaCompositionAux b ⟨↑⟨i, hi1⟩, ⋯⟩).blocksFun ⟨↑⟨j, hj1⟩, ⋯⟩),
    (v ∘ ⇑(⟨a, b⟩.fst.embedding ((⟨a, b⟩.snd.embedding ⟨i, hi1⟩) ⟨j, hj1⟩))) ⟨i_1, him⟩ =
      ((v ∘ ⇑(⟨a.gather b, a.sigmaCompositionAux b⟩.fst.embedding ⟨i, hi2⟩)) ∘
          ⇑((⟨a.gather b, a.sigmaCompositionAux b⟩.snd ⟨i, hi2⟩).embedding ⟨j, hj2⟩))
        ⟨i_1, hin⟩
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_9
A : Type u_10
inst✝¹ : NormedCommRing A
inst✝ : NormedAlgebra 𝕜 A
f : α → E → A
c : E
h : ∀ (a : α), AnalyticAt 𝕜 (f a) c
⊢ AnalyticAt 𝕜 (∏ᶠ (n : α), f n) c

Tactic:
by_cases hf : (Function.mulSupport f).Finite
  · simp_all [finprod_eq_prod _ hf, Finset.analyticAt_prod]
  · rw [finprod_of_infinite_mulSupport hf]
    apply analyticAt_const

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

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
x : E
s : Set E
R : Type u_4
inst✝⁴ : Monoid R
inst✝³ : DistribMulAction R F
inst✝² : SMulCommClass 𝕜 R F
inst✝¹ : ContinuousConstSMul R F
c : R
inst✝ : Invertible c
⊢ DifferentiableWithinAt 𝕜 (c • f) s x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.const_smul c⟩
  apply (h.const_smul ⅟c).congr_of_eventuallyEq ?_ (by simp)
  filter_upwards with x using by simp

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

Goal state before:
pp: case inr
𝕜 : 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
x : E
s : Set E
R : Type u_4
inst✝³ : DivisionSemiring R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
c : R
hs : UniqueDiffWithinAt 𝕜 s x
ha : c ≠ 0
⊢ fderivWithin 𝕜 (c • f) s x = c • fderivWithin 𝕜 f s x

Tactic:
have : Invertible c := invertibleOfNonzero ha
    simp [fderivWithin_const_smul_of_invertible c hs]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Completion

Goal state before:
pp: case ih
𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst✝ : SeminormedRing A
x y : A
⊢ ‖↑x * ↑y‖ ≤ ‖↑x‖ * ‖↑y‖

Tactic:
| ih x y =>

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

Goal state before:
pp: case ih
α : Type u
β : Type v
inst✝⁷ : PseudoMetricSpace α
inst✝⁶ : Ring α
inst✝⁵ : IsTopologicalRing α
inst✝⁴ : IsUniformAddGroup α
inst✝³ : Ring β
inst✝² : PseudoMetricSpace β
inst✝¹ : IsUniformAddGroup β
inst✝ : IsTopologicalRing β
f : α →+* β
h : Isometry ⇑f
x y : α
⊢ dist (h.mapRingHom ↑x) (h.mapRingHom ↑y) = dist ↑x ↑y

Tactic:
| ih x y =>

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

Goal state before:
pp: α : Type u
β : Type v
inst✝⁷ : PseudoMetricSpace α
inst✝⁶ : Ring α
inst✝⁵ : IsTopologicalRing α
inst✝⁴ : IsUniformAddGroup α
inst✝³ : Ring β
inst✝² : PseudoMetricSpace β
inst✝¹ : IsUniformAddGroup β
inst✝ : IsTopologicalRing β
f : α →+* β
h : Isometry ⇑f
x y : Completion α
⊢ dist (h.mapRingHom x) (h.mapRingHom y) = dist x y

Tactic:
induction x, y using induction_on₂ with
    | hp => exact isClosed_eq (continuous_dist.comp₂ (continuous_map.comp continuous_fst)
        (continuous_map.comp continuous_snd)) (by fun_prop)
    | ih x y => simp only [Completion.dist_eq, mapRingHom_coe, h.dist_eq]

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
n : ℕ
⊢ HasFTaylorSeriesUpToOn (↑n + 1) f p s ↔
    (∀ x ∈ s, (p x 0).curry0 = f x) ∧
      (∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft s x) ∧
        HasFTaylorSeriesUpToOn (↑n) (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) s

Tactic:
exact hasFTaylorSeriesUpToOn_succ_nat_iff_right

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

Goal state before:
pp: case zero
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
⊢ tsupport (iteratedFDeriv 𝕜 0 f) ⊆ tsupport f

Tactic:
iteratedFDeriv_zero_eq_comp

Goal state after:
case zero
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
⊢ tsupport (⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f) ⊆ tsupport f
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case zero
𝕜 : 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
⊢ AnalyticOnNhd 𝕜 (iteratedFDeriv 𝕜 0 f) s

Tactic:
iteratedFDeriv_zero_eq_comp

Goal state after:
case zero
𝕜 : 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
⊢ AnalyticOnNhd 𝕜 (⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f) s
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case zero
𝕜 : 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 : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
⊢ AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 0 f s) s

Tactic:
rw [iteratedFDerivWithin_zero_eq_comp]

Goal state after:
case zero
𝕜 : 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 : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
⊢ AnalyticOn 𝕜 (⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f) s
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case zero
𝕜 : 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
⊢ CPolynomialOn 𝕜 (_root_.iteratedFDeriv 𝕜 0 f) s

Tactic:
iteratedFDeriv_zero_eq_comp

Goal state after:
case zero
𝕜 : 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
⊢ CPolynomialOn 𝕜 (⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f) s
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
u : 𝕜 → F
hc : DifferentiableWithinAt 𝕜 c s x
hu : DifferentiableWithinAt 𝕜 u s x
⊢ derivWithin (fun y ↦ (c y) (u y)) s x = (derivWithin c s x) (u x) + (c x) (derivWithin u s x)

Tactic:
by
  by_cases hsx : UniqueDiffWithinAt 𝕜 s x
  · exact (hc.hasDerivWithinAt.clm_apply hu.hasDerivWithinAt).derivWithin hsx
  · simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

Goal state after:
Module: Mathlib.Analysis.Calculus.DSlope

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a : 𝕜
⊢ ContinuousAt (dslope f a) a ↔ DifferentiableAt 𝕜 f a

Tactic:
simp only [dslope, continuousAt_update_same, ← hasDerivAt_deriv_iff, hasDerivAt_iff_tendsto_slope]

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
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasStrictFDerivAt (fun x ↦ f i x) (f' i) x
m : E
⊢ ∑ i,
      ((List.take (↑i) (List.map (fun i ↦ f (l.get i) x) (List.finRange l.length))).prod •>
          (proj i <• (List.drop (↑i).succ (List.map (fun i ↦ f (l.get i) x) (List.finRange l.length))).prod))
        ((pi fun i ↦ f' (l.get i)) m) =
    ∑ i,
      ((List.take (↑i) (List.map ((fun x_1 ↦ f x_1 x) ∘ l.get) (List.finRange l.length))).prod •>
          (f' (l.get i) <•
            (List.drop (↑i).succ (List.map ((fun x_1 ↦ f x_1 x) ∘ l.get) (List.finRange l.length))).prod))
        m

Tactic:
smul_apply,

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasStrictFDerivAt (fun x ↦ f i x) (f' i) x
m : E
⊢ ∑ x_1,
      (List.take (↑x_1) (List.map (fun i ↦ f (l.get i) x) (List.finRange l.length))).prod •>
        ((proj x_1) ((pi fun i ↦ f' (l.get i)) m) <•
          (List.drop (↑x_1).succ (List.map (fun i ↦ f (l.get i) x) (List.finRange l.length))).prod) =
    ∑ x_1,
      (List.take (↑x_1) (List.map ((fun x_2 ↦ f x_2 x) ∘ l.get) (List.finRange l.length))).prod •>
        ((f' (l.get x_1)) m <•
          (List.drop (↑x_1).succ (List.map ((fun x_2 ↦ f x_2 x) ∘ l.get) (List.finRange l.length))).prod)
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
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasFDerivAt (fun x ↦ f i x) (f' i) x
m : E
⊢ ∑ i,
      ((List.take (↑i) (List.map (fun i ↦ f (l.get i) x) (List.finRange l.length))).prod •>
          (proj i <• (List.drop (↑i).succ (List.map (fun i ↦ f (l.get i) x) (List.finRange l.length))).prod))
        ((pi fun i ↦ f' (l.get i)) m) =
    ∑ i,
      ((List.take (↑i) (List.map ((fun x_1 ↦ f x_1 x) ∘ l.get) (List.finRange l.length))).prod •>
          (f' (l.get i) <•
            (List.drop (↑i).succ (List.map ((fun x_1 ↦ f x_1 x) ∘ l.get) (List.finRange l.length))).prod))
        m

Tactic:
smul_apply,

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasFDerivAt (fun x ↦ f i x) (f' i) x
m : E
⊢ ∑ x_1,
      (List.take (↑x_1) (List.map (fun i ↦ f (l.get i) x) (List.finRange l.length))).prod •>
        ((proj x_1) ((pi fun i ↦ f' (l.get i)) m) <•
          (List.drop (↑x_1).succ (List.map (fun i ↦ f (l.get i) x) (List.finRange l.length))).prod) =
    ∑ x_1,
      (List.take (↑x_1) (List.map ((fun x_2 ↦ f x_2 x) ∘ l.get) (List.finRange l.length))).prod •>
        ((f' (l.get x_1)) m <•
          (List.drop (↑x_1).succ (List.map ((fun x_2 ↦ f x_2 x) ∘ l.get) (List.finRange l.length))).prod)