mathlib-initiative/mathlib-tactics huggingface dataset:
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
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : y ∈ (fun x_1 ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r
r' : ℝ≥0
yr' : edist y 0 < ↑r'
hr' : ↑r' < r
this : Metric.eball 0 ↑r' ∈ 𝓝 y
⊢ ∃ t ∈ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r] y,
    ∀ᶠ (n : ℕ) in atTop, ∀ y ∈ t, ((fun y ↦ f (x + y)) y, (fun n y ↦ p.partialSum n y) n y) ∈ u

Tactic:
refine ⟨(x + ·)⁻¹' (insert x s) ∩ Metric.eball (0 : E) r', ?_, ?_⟩

Goal state after:
case refine_1
𝕜 : 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
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : y ∈ (fun x_1 ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r
r' : ℝ≥0
yr' : edist y 0 < ↑r'
hr' : ↑r' < r
this : Metric.eball 0 ↑r' ∈ 𝓝 y
⊢ (fun x_1 ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 ↑r' ∈ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r] y

case refine_2
𝕜 : 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
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : y ∈ (fun x_1 ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r
r' : ℝ≥0
yr' : edist y 0 < ↑r'
hr' : ↑r' < r
this : Metric.eball 0 ↑r' ∈ 𝓝 y
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ y ∈ (fun x_1 ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 ↑r',
      ((fun y ↦ f (x + y)) y, (fun n y ↦ p.partialSum n y) n y) ∈ u
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
M N : ℕ
z : E
⊢ q.partialSum M (∑ i ∈ Finset.Ico 1 N, (p i) fun _j ↦ z) =
    ∑ i ∈ compPartialSumTarget 0 M N, (q.compAlongComposition p i.snd) fun _j ↦ z

Tactic:
by
  -- we expand the composition, using the multilinearity of `q` to expand along each coordinate.
  suffices H :
    (∑ n ∈ Finset.range M,
        ∑ r ∈ Fintype.piFinset fun i : Fin n => Finset.Ico 1 N,
          q n fun i : Fin n => p (r i) fun _j => z) =
      ∑ i ∈ compPartialSumTarget 0 M N, q.compAlongComposition p i.2 fun _j => z by
    simpa only [FormalMultilinearSeries.partialSum, ContinuousMultilinearMap.map_sum_finset] using H
  -- rewrite the first sum as a big sum over a sigma type, in the finset
  -- `compPartialSumTarget 0 N N`
  rw [Finset.range_eq_Ico, Finset.sum_sigma']
  -- use `compChangeOfVariables_sum`, saying that this change of variables respects sums
  apply compChangeOfVariables_sum 0 M N
  rintro ⟨k, blocks_fun⟩ H
  apply congr _ (compChangeOfVariables_length 0 M N H).symm
  intros
  rw [← compChangeOfVariables_blocksFun 0 M N H, applyComposition, Function.comp_def]

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

Goal state before:
pp: n : ℕ
a : Composition n
b : Composition a.length
i j : ℕ
hi : i < b.length
hj : j < b.blocksFun ⟨i, hi⟩
⊢ a.sizeUpTo (b.sizeUpTo i + j) = (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo j

Tactic:
induction j with
  | zero =>
    change
      sum (take (b.blocks.take i).sum a.blocks) =
        sum (take i (map sum (splitWrtComposition a.blocks b)))
    induction i with
    | zero => rfl
    | succ i IH =>
      have A : i < b.length := Nat.lt_of_succ_lt hi
      have B : i < List.length (map List.sum (splitWrtComposition a.blocks b)) := by simp [A]
      have C : 0 < blocksFun b ⟨i, A⟩ := Composition.blocks_pos' _ _ _
      rw [sum_take_succ _ _ B, ← IH A C]
      have :
        take (sum (take i b.blocks)) a.blocks =
          take (sum (take i b.blocks)) (take (sum (take (i + 1) b.blocks)) a.blocks) := by
        rw [take_take, min_eq_left]
        apply monotone_sum_take _ (Nat.le_succ _)
      rw [this, getElem_map, getElem_splitWrtComposition, ←
        take_append_drop (sum (take i b.blocks)) (take (sum (take (Nat.succ i) b.blocks)) a.blocks),
        sum_append]
      congr
      rw [take_append_drop]
  | succ j IHj =>
    have A : j < blocksFun b ⟨i, hi⟩ := lt_trans (lt_add_one j) hj
    have B : j < length (sigmaCompositionAux a b ⟨i, (length_gather a b).symm ▸ hi⟩) := by
      convert! A; rw [← length_sigmaCompositionAux]
    have C : sizeUpTo b i + j < sizeUpTo b (i + 1) := by
      simp only [sizeUpTo_succ b hi, add_lt_add_iff_left]
      exact A
    have D : sizeUpTo b i + j < length a := lt_of_lt_of_le C (b.sizeUpTo_le _)
    have : sizeUpTo b i + Nat.succ j = (sizeUpTo b i + j).succ := rfl
    rw [this, sizeUpTo_succ _ D, IHj A, sizeUpTo_succ _ B]
    simp only [sigmaCompositionAux, add_assoc]
    rw [getElem_of_eq (getElem_splitWrtComposition _ _ _ _), getElem_drop, getElem_take]

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

Goal state before:

Tactic:
_ ≤ pf.radius / ‖u‖ₑ := by
        gcongr
        exact hf.r_le
      _ ≤ _ := pf.div_le_radius_compContinuousLinearMap _

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

Goal state before:
pp: case empty
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
c : E
s : Set E
h : ∀ n ∈ ∅, AnalyticWithinAt 𝕜 (f n) s c
⊢ AnalyticWithinAt 𝕜 (∑ n ∈ ∅, f n) s c

Tactic:
simp only [Finset.sum_empty]

Goal state after:
case empty
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
c : E
s : Set E
h : ∀ n ∈ ∅, AnalyticWithinAt 𝕜 (f n) s c
⊢ AnalyticWithinAt 𝕜 0 s c
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case empty
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_9
inst✝¹ : NormedCommRing A
inst✝ : NormedAlgebra 𝕜 A
f : α → E → A
c : E
s : Set E
h : ∀ n ∈ ∅, AnalyticWithinAt 𝕜 (f n) s c
⊢ AnalyticWithinAt 𝕜 (fun z ↦ ∏ n ∈ ∅, f n z) s c

Tactic:
simp only [Finset.prod_empty]

Goal state after:
case empty
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_9
inst✝¹ : NormedCommRing A
inst✝ : NormedAlgebra 𝕜 A
f : α → E → A
c : E
s : Set E
h : ∀ n ∈ ∅, AnalyticWithinAt 𝕜 (f n) s c
⊢ AnalyticWithinAt 𝕜 (fun z ↦ 1) s c
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case neg
𝕜 : 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
hf : ¬(Function.mulSupport f).Finite
⊢ AnalyticAt 𝕜 (∏ᶠ (n : α), f n) c

Tactic:
rw [finprod_of_infinite_mulSupport hf]

Goal state after:
case neg
𝕜 : 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
hf : ¬(Function.mulSupport f).Finite
⊢ AnalyticAt 𝕜 1 c
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
f' : E →L[𝕜] F
x : E
s : Set E
a : E
this : map (fun x ↦ a + x) (𝓝[s] x) = 𝓝[a +ᵥ s] (a + x)
⊢ HasFDerivWithinAt (fun x ↦ f (a + x)) f' s x ↔ HasFDerivWithinAt f f' (a +ᵥ s) (a + x)

Tactic:
simp [HasFDerivWithinAt, hasFDerivAtFilter_iff_isLittleOTVS, ← this, Function.comp_def]

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 a : E
⊢ fderiv 𝕜 (fun x ↦ f (x + a)) x = fderiv 𝕜 f (x + a)

Tactic:
by
  simp [← fderivWithin_univ, fderivWithin_comp_add_right]

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
H : DifferentiableOn 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s)
y : F
hy : y ∈ s
⊢ DifferentiableWithinAt 𝕜 f s y

Tactic:
← iso.apply_symm_apply y,

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
H : DifferentiableOn 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s)
y : F
hy : y ∈ s
⊢ DifferentiableWithinAt 𝕜 f s (iso (iso.symm y))
Module: Mathlib.Analysis.Calculus.FDeriv.Prod

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : E →L[𝕜] (i : Fin n.succ) → F' i
l : Filter (E × E)
⊢ (HasFDerivAtFilter (fun x ↦ Fin.cons (φ x) (φs x) 0) (proj 0 ∘SL φ') l ∧
      ∀ (i : Fin n), HasFDerivAtFilter (fun x ↦ Fin.cons (φ x) (φs x) i.succ) (proj i.succ ∘SL φ') l) ↔
    HasFDerivAtFilter φ (proj 0 ∘SL φ') l ∧
      ∀ (i : Fin n), HasFDerivAtFilter (fun x ↦ φs x i) (proj i ∘SL Pi.compRightL 𝕜 F' Fin.succ ∘SL φ') l

Tactic:
dsimp [ContinuousLinearMap.comp, LinearMap.comp, Function.comp_def]

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : E →L[𝕜] (i : Fin n.succ) → F' i
l : Filter (E × E)
⊢ (HasFDerivAtFilter (fun x ↦ Fin.cons (φ x) (φs x) 0)
        { toFun := fun x ↦ φ' x 0, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } l ∧
      ∀ (i : Fin n),
        HasFDerivAtFilter (fun x ↦ Fin.cons (φ x) (φs x) i.succ)
          { toFun := fun x ↦ φ' x i.succ, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } l) ↔
    HasFDerivAtFilter φ { toFun := fun x ↦ φ' x 0, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } l ∧
      ∀ (i : Fin n),
        HasFDerivAtFilter (fun x ↦ φs x i) { toFun := fun x ↦ φ' x i.succ, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } l
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 ∈ 𝓤 ℝ
T : {x | (dist x.1.1 x.1.2, dist x.2.1 x.2.2) ∈ r} ∈ 𝓤 (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α)

Tactic:
simp only [uniformity_prod_eq_prod, mem_prod_iff, Filter.mem_map] at T

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 :
  ∃ t₁ ∈ 𝓤 (Completion α),
    ∃ t₂ ∈ 𝓤 (Completion α),
      t₁ ×ˢ t₂ ⊆ (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' {x | (dist x.1.1 x.1.2, dist x.2.1 x.2.2) ∈ r}
⊢ s ∈ 𝓤 (Completion α)
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
⊢ 𝓤 (Completion α) = ⨅ ε, 𝓟 {p | dist p.1 p.2 < ↑ε}

Tactic:
ext s; rw [mem_iInf_of_directed]
  · simp [Completion.mem_uniformity_dist, subset_def]
  · rintro ⟨r, hr⟩ ⟨p, hp⟩
    use ⟨min r p, lt_min hr hp⟩
    simp +contextual

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

Goal state before:
pp: case e'_12
𝕜 : 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
x : E
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hn : n ≠ 0
hx : x ∈ s
A : ∀ y ∈ s, f y = (continuousMultilinearCurryFin0 𝕜 E F) (p y 0)
this : ↑↑0 < n
e_8✝ : ContinuousMultilinearMap.normedAddCommGroup'.toAddCommGroup = ContinuousMultilinearMap.instAddCommGroup
e_9✝ : ContinuousMultilinearMap.normedSpace'.toModule ≍ ContinuousMultilinearMap.instModule
e_10✝ : PseudoMetricSpace.toUniformSpace.toTopologicalSpace = ContinuousMultilinearMap.instTopologicalSpace
y : E
v : Fin 0 → E
⊢ ((↑↑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘SL (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) y) v =
    ((p x (Nat.succ 0)).curryLeft y) v

Tactic:
change (p x 1) (snoc 0 y) = (p x 1) (cons y v)

Goal state after:
case e'_12
𝕜 : 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
x : E
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hn : n ≠ 0
hx : x ∈ s
A : ∀ y ∈ s, f y = (continuousMultilinearCurryFin0 𝕜 E F) (p y 0)
this : ↑↑0 < n
e_8✝ : ContinuousMultilinearMap.normedAddCommGroup'.toAddCommGroup = ContinuousMultilinearMap.instAddCommGroup
e_9✝ : ContinuousMultilinearMap.normedSpace'.toModule ≍ ContinuousMultilinearMap.instModule
e_10✝ : PseudoMetricSpace.toUniformSpace.toTopologicalSpace = ContinuousMultilinearMap.instTopologicalSpace
y : E
v : Fin 0 → E
⊢ (p x 1) (snoc 0 y) = (p x 1) (cons y v)
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
h :
  (∀ 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
n : ℕ
⊢ (∀ 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 ⟨h.1, h.2.1, (h.2.2).of_le (m := n) (natCast_le_of_coe_top_le_withTop hN n)⟩

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

Goal state before:
pp: case succ
𝕜 : 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
hs : UniqueDiffOn 𝕜 s
n : ℕ
IH :
  ∀ {x : E},
    x ∈ s →
      ∀ (m : Fin (n + 1) → E),
        (iteratedFDerivWithin 𝕜 (n + 1) f s x) m =
          ((iteratedFDerivWithin 𝕜 n (fun y ↦ fderivWithin 𝕜 f s y) s x) (init m)) (m (last n))
x : E
hx : x ∈ s
m : Fin (n + 1 + 1) → E
I : (E [×n]→L[𝕜] E →L[𝕜] F) ≃ₗᵢ[𝕜] E [×n.succ]→L[𝕜] F := (continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm
⊢ (iteratedFDerivWithin 𝕜 (n + 1 + 1) f s x) m =
    ((iteratedFDerivWithin 𝕜 (n + 1) (fun y ↦ fderivWithin 𝕜 f s y) s x) (init m)) (m (last (n + 1)))

Tactic:
have A : ∀ y ∈ s, iteratedFDerivWithin 𝕜 n.succ f s y =
        (I ∘ iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s) y := fun y hy ↦ by
      ext m
      simp [IH hy m, I]

Goal state after:
case succ
𝕜 : 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
hs : UniqueDiffOn 𝕜 s
n : ℕ
IH :
  ∀ {x : E},
    x ∈ s →
      ∀ (m : Fin (n + 1) → E),
        (iteratedFDerivWithin 𝕜 (n + 1) f s x) m =
          ((iteratedFDerivWithin 𝕜 n (fun y ↦ fderivWithin 𝕜 f s y) s x) (init m)) (m (last n))
x : E
hx : x ∈ s
m : Fin (n + 1 + 1) → E
I : (E [×n]→L[𝕜] E →L[𝕜] F) ≃ₗᵢ[𝕜] E [×n.succ]→L[𝕜] F := (continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm
A : ∀ y ∈ s, iteratedFDerivWithin 𝕜 n.succ f s y = (⇑I ∘ iteratedFDerivWithin 𝕜 n (fun y ↦ fderivWithin 𝕜 f s y) s) y
⊢ (iteratedFDerivWithin 𝕜 (n + 1 + 1) f s x) m =
    ((iteratedFDerivWithin 𝕜 (n + 1) (fun y ↦ fderivWithin 𝕜 f s y) s x) (init m)) (m (last (n + 1)))
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
x : E
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
m : ℕ
hmn : ↑m ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ p x m = iteratedFDerivWithin 𝕜 m f s x

Tactic:
induction m generalizing x with

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
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∈ tsupport u
⊢ HasDerivAt (fun x ↦ (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x

pp: case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∉ tsupport u
⊢ HasDerivAt (fun x ↦ (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x

Tactic:
· by_cases hxv : x ∈ tsupport v
    · simpa using (B.hasFDerivAt_of_bilinear (hu hxv).hasFDerivAt (hv hxu).hasFDerivAt).hasDerivAt
    · have hx : x ∉ tsupport fun x ↦ B (u x) (v x) :=
        mt (closure_mono (fun x ↦ mt fun h ↦ by simp [h]) ·) hxv
      convert! HasDerivAt.of_notMem_tsupport hx
      simp [(hv hxu).unique <| .of_notMem_tsupport hxv, image_eq_zero_of_notMem_tsupport hxv]

Goal state after:
case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∉ tsupport u
⊢ HasDerivAt (fun x ↦ (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x
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 ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : IsEmpty ι
l : ℕ
⊢ l + 1 ≠ Fintype.card ι

Tactic:
Fintype.card_eq_zero

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 ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : IsEmpty ι
l : ℕ
⊢ l + 1 ≠ 0
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 ι
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : DecidableEq ι
x : G
f : G → ContinuousMultilinearMap 𝕜 E F
g : (i : ι) → G → E i
f' : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
g' : (i : ι) → G →L[𝕜] E i
hf : HasStrictFDerivAt f f' x
hg : ∀ (i : ι), HasStrictFDerivAt (g i) (g' i) x
⊢ HasStrictFDerivAt (fun x ↦ (f x) fun x_1 ↦ g x_1 x)
    ((apply 𝕜 E F fun x_1 ↦ g x_1 x) ∘SL f' + ∑ i, (f x).toContinuousLinearMap (fun x_1 ↦ g x_1 x) i ∘SL g' i) x

Tactic:
convert!
    ContinuousMultilinearMap.hasStrictFDerivAt_uncurry (f x, (g · x)) |>.comp x
      (hf.prodMk (hasStrictFDerivAt_pi.2 hg))

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 ι
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : DecidableEq ι
x : G
f : G → ContinuousMultilinearMap 𝕜 E F
g : (i : ι) → G → E i
f' : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
g' : (i : ι) → G →L[𝕜] E i
hf : HasStrictFDerivAt f f' x
hg : ∀ (i : ι), HasStrictFDerivAt (g i) (g' i) x
⊢ (apply 𝕜 E F fun x_1 ↦ g x_1 x) ∘SL f' + ∑ i, (f x).toContinuousLinearMap (fun x_1 ↦ g x_1 x) i ∘SL g' i =
    (apply 𝕜 E F (f x, fun x_1 ↦ g x_1 x).2 ∘SL
          ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i) +
        (f x, fun x_1 ↦ g x_1 x).1.linearDeriv (f x, fun x_1 ↦ g x_1 x).2 ∘SL
          ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i)) ∘SL
      f'.prod (ContinuousLinearMap.pi g')
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hx : AccPt x (𝓟 s)
hd : HasDerivWithinAt g g' s x
hg : MonotoneOn g s
⊢ 0 ≤ g'

Tactic:
have : (𝓝[s \ {x}] x).NeBot := accPt_principal_iff_nhdsWithin.mp hx
  have h'g : MonotoneOn g (insert x s) :=
    hg.insert_of_continuousWithinAt hx.clusterPt hd.continuousWithinAt
  have : Tendsto (slope g x) (𝓝[s \ {x}] x) (𝓝 g') := hasDerivWithinAt_iff_tendsto_slope.mp hd
  apply ge_of_tendsto this
  filter_upwards [self_mem_nhdsWithin] with y hy
  simp only [Set.mem_sdiff, mem_singleton_iff] at hy
  exact h'g.slope_nonneg (by simp) (by simp [hy])

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
n : ℕ
hp : HasFPowerSeriesAt f p z₀
⊢ HasFPowerSeriesAt ((swap dslope z₀)^[n] f) (fslope^[n] p) z₀

Tactic:
induction n generalizing f p with
  | zero => exact hp
  | succ n ih => simpa using ih (has_fpower_series_dslope_fslope hp)

Goal state after: