mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.TangentCone.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : SMul 𝕜 E
inst✝ : TopologicalSpace E
s : Set E
x : E
ι : Sort u_3
p : ι → Prop
U : ι → Set E
h : (𝓝 0).HasBasis p U
⊢ tangentConeAt 𝕜 s x = ⋂ i, ⋂ (_ : p i), closure[inst✝] (univ • (U i ∩ (fun x_2 ↦ x + x_2) ⁻¹' s))

Tactic:
ext y
  simp only [tangentConeAt_def, mem_ofPred_eq, mem_iInter₂, ← map₂_smul, ← map_prod_eq_map₂,
    ((nhdsWithin_hasBasis h _).top_prod.map _).clusterPt_iff_forall_mem_closure, image_prod,
    image2_smul]

Goal state after:
Module: Mathlib.Analysis.Calculus.TangentCone.Real

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul ℝ E
s : Set E
x : E
inst✝ : IsTopologicalAddGroup E
conv : Convex ℝ s
hx : x ∈ closure[inst✝²] s
y : E
hy : y ∈ interior s
⊢ y - x ∈ interior (tangentConeAt ℝ s x)

Tactic:
mem_interior_iff_mem_nhds

Goal state after:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul ℝ E
s : Set E
x : E
inst✝ : IsTopologicalAddGroup E
conv : Convex ℝ s
hx : x ∈ closure[inst✝²] s
y : E
hy : y ∈ interior s
⊢ tangentConeAt ℝ s x ∈ 𝓝 (y - x)
Module: Mathlib.Analysis.Calculus.FDeriv.Const

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
x : E
hf : Injective ⇑(fderiv 𝕜 f x)
⊢ DifferentiableAt 𝕜 f x

Tactic:
simp only [← differentiableWithinAt_univ, ← fderivWithin_univ] at hf ⊢

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
x : E
hf : Injective ⇑(fderivWithin 𝕜 f univ x)
⊢ DifferentiableWithinAt 𝕜 f univ x
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
σ σ' : 𝕜 →+* 𝕜
inst✝³ : RingHomIsometric σ
inst✝² : RingHomInvPair σ σ'
F' : Type u_1
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜 F'
L : F →SL[σ] F'
hf : HasDerivAt f f' x
this : RingHomIsometric σ'
R : 𝕜 →SL[σ'] 𝕜 := { toLinearMap := σ'.toSemilinearMap, cont := ⋯ }
hR : ∀ (k : 𝕜), R k = σ' k
⊢ HasDerivAt (⇑L ∘ f ∘ ⇑σ') (L f') (σ x)

Tactic:
rw [hasDerivAt_iff_hasFDerivAt]

Goal state after:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
σ σ' : 𝕜 →+* 𝕜
inst✝³ : RingHomIsometric σ
inst✝² : RingHomInvPair σ σ'
F' : Type u_1
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜 F'
L : F →SL[σ] F'
hf : HasDerivAt f f' x
this : RingHomIsometric σ'
R : 𝕜 →SL[σ'] 𝕜 := { toLinearMap := σ'.toSemilinearMap, cont := ⋯ }
hR : ∀ (k : 𝕜), R k = σ' k
⊢ HasFDerivAt (⇑L ∘ f ∘ ⇑σ') (toSpanSingleton 𝕜 (L f')) (σ x)
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s t : Set E
hs : HasFDerivWithinAt f f' s x
ht : HasFDerivWithinAt f f' t x
⊢ HasFDerivWithinAt f f' (s ∪ t) x

Tactic:
by
  simp only [hasFDerivWithinAt_iff_isLittleOTVS, nhdsWithin_union] at *
  exact hs.sup ht

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

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
hf : HasFDerivAt f f' x₀
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ‖f'‖ ≤ ↑C

Tactic:
refine hf.le_of_lip' C.coe_nonneg ?_
  filter_upwards [hs] with x hx using hlip.norm_sub_le hx (mem_of_mem_nhds hs)

Goal state after:
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
r : ℝ≥0
h : Summable fun n ↦ ↑‖p n‖₊ * ↑r ^ n
⊢ Summable fun n ↦ ‖p n‖₊ * r ^ n

Tactic:
exact mod_cast h

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry

Goal state before:
pp: 𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 Ei G
m : (i : Fin n.succ) → Ei i
⊢ f (snoc (init m) (m (last n))) = f m

Tactic:
snoc_init_self

Goal state after:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 Ei G
m : (i : Fin n.succ) → Ei i
⊢ f m = f m
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 ∈ insert x s ∩ Metric.eball x r
⊢ AnalyticWithinAt 𝕜 f s y

Tactic:
have : (‖y - x‖₊ : ℝ≥0∞) < r := by simpa [edist_eq_enorm_sub] using! h.2
  have := hf.changeOrigin this (by simpa using! h.1)
  rw [add_sub_cancel] at this
  exact this.analyticWithinAt

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

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
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
g : F →L[𝕜] G
h : HasFiniteFPowerSeriesOnBall f p x n r
m : ℕ
hm : n ≤ m
⊢ g.compFormalMultilinearSeries p m = 0

Tactic:
rw [compFormalMultilinearSeries_apply, h.finite m hm]
    ext; exact map_zero g

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

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 →L[𝕜] F
x : E
⊢ ∀ (m : ℕ), 2 ≤ m → f.fpowerSeries x m = 0

Tactic:
by
    intro m hm
    match m with
    | 0 | 1 => linarith
    | n + 2 => simp [fpowerSeries]

Goal state after:
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 ≠ 0
hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
r' : ℝ≥0
hr' : ↑r' < (ofScalars E c).radius
this : 1 < r' * r
⊢ r' ≠ 0

Tactic:
aesop

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

Goal state before:
pp: 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‖

Tactic:
aesop

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

Goal state before:
pp: 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‖

Tactic:
aesop

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

Goal state before:
pp: case ha
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc✝ : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
n : ℕ
hc : 2 * ↑r⁻¹ ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
⊢ ↑r ^ n ≠ 0

Tactic:
aesop

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

Goal state before:
pp: n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
⊢ ∑ k ∈ Ico 2 (n + 1), a ^ k * ∑ c ∈ {c | 1 < c.length}.toFinset, r ^ c.length * ∏ j, p (c.blocksFun j) =
    ∑ k ∈ Ico 2 (n + 1), ∑ c ∈ {c | 1 < c.length}.toFinset, ∏ j, r * (a ^ c.blocksFun j * p (c.blocksFun j))

Tactic:
by
      simp_rw [mul_sum]
      congr! with k _ c
      rw [prod_mul_distrib, prod_mul_distrib, prod_pow_eq_pow_sum, Composition.sum_blocksFun,
        prod_const, card_fin]
      ring

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

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
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
⊢ ContinuousAt (fun y ↦ f (x + y) - f x) 0

Tactic:
apply ContinuousAt.sub _ continuousAt_const

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
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
⊢ ContinuousAt (fun y ↦ f (x + y)) 0
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 : ℕ
i : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
⊢ (ofFn fun j ↦ (i.snd j).length).sum =
    { blocks := (ofFn fun j ↦ (i.snd j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ }.length

Tactic:
dsimp only [Composition.length]

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 : ℕ
i : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
⊢ (ofFn fun j ↦ (i.snd j).blocks.length).sum = (ofFn fun j ↦ (i.snd j).blocks).flatten.length
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
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
⊢ HasFPowerSeriesAt (fun x x_1 ↦ f x_1 x) (FormalMultilinearSeries.pi p) e ↔ ∀ (i : ι), HasFPowerSeriesAt (f i) (p i) e

Tactic:
simp_rw [← hasFPowerSeriesWithinAt_univ]
  exact hasFPowerSeriesWithinAt_pi_iff

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

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
f' : E →L[𝕜] F
x : E
s : Set E
c : F
h : HasFDerivWithinAt f f' s x
hf' : ∃ C, AntilipschitzWith C ⇑f'
hc : f x ≠ c
⊢ ∀ᶠ (x : F) in 𝓝[≠] f x, x ≠ c

Tactic:
· exact eventually_ne_nhdsWithin hc

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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1)) f p s
m : ℕ
hm : ↑m < ↑n
x : E
hx : x ∈ s
A : ↑m.succ < ↑n.succ
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 m.succ → E
⊢ (p x (m + 2)) (cons y (snoc (init v) (v (last m)))) = (p x (m + 2)) (cons y v)

Tactic:
snoc_init_self

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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1)) f p s
m : ℕ
hm : ↑m < ↑n
x : E
hx : x ∈ s
A : ↑m.succ < ↑n.succ
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 m.succ → E
⊢ (p x (m + 2)) (cons y v) = (p x (m + 2)) (cons y v)
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
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
x : E
hx : x ∈ s
m : ℕ
hm : ↑(m + 1) < ↑n.succ
A : ↑m < ↑n
this :
  HasFDerivWithinAt (fun x ↦ p x m.succ)
    (↑↑(continuousMultilinearCurryRightEquiv' 𝕜 m E F).symm ∘SL ((p x).shift m.succ).curryLeft) s x
e_8✝ : ContinuousMultilinearMap.instAddCommGroup = ContinuousMultilinearMap.normedAddCommGroup'.toAddCommGroup
e_9✝ : ContinuousMultilinearMap.instModule ≍ ContinuousMultilinearMap.normedSpace'.toModule
e_10✝ : ContinuousMultilinearMap.instTopologicalSpace = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
y : E
v : Fin (m + 1) → E
⊢ (p x m.succ.succ) (cons y v) = (p x m.succ.succ) (cons y (snoc (init v) (v (last m))))

Tactic:
snoc_init_self

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
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
x : E
hx : x ∈ s
m : ℕ
hm : ↑(m + 1) < ↑n.succ
A : ↑m < ↑n
this :
  HasFDerivWithinAt (fun x ↦ p x m.succ)
    (↑↑(continuousMultilinearCurryRightEquiv' 𝕜 m E F).symm ∘SL ((p x).shift m.succ).curryLeft) s x
e_8✝ : ContinuousMultilinearMap.instAddCommGroup = ContinuousMultilinearMap.normedAddCommGroup'.toAddCommGroup
e_9✝ : ContinuousMultilinearMap.instModule ≍ ContinuousMultilinearMap.normedSpace'.toModule
e_10✝ : ContinuousMultilinearMap.instTopologicalSpace = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
y : E
v : Fin (m + 1) → E
⊢ (p x m.succ.succ) (cons y v) = (p x m.succ.succ) (cons y v)
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
s : Set E
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hs : UniqueDiffOn 𝕜 s
x : E
hmn : ↑0 ≤ n
hx : x ∈ s
⊢ p x 0 = iteratedFDerivWithin 𝕜 0 f s x

Tactic:
rw [h.zero_eq' hx, iteratedFDerivWithin_zero_eq_comp, comp_apply]

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
p : FormalMultilinearSeries 𝕜 E F
x : E
inst✝ : CompleteSpace F
h : ‖x‖ₑ < p.radius
⊢ HasFDerivAt p.sum (p.derivSeries.sum x) x

Tactic:
rw [← FormalMultilinearSeries.fderiv_sum h]

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
inst✝ : CompleteSpace F
h : ‖x‖ₑ < p.radius
⊢ HasFDerivAt p.sum (fderiv 𝕜 p.sum x) x
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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hu : UniqueDiffOn 𝕜 (insert x s)
z : E
hz : z ∈ insert x s ∩ Metric.eball x r
⊢ ↑‖z - x‖₊ < r

pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hu : UniqueDiffOn 𝕜 (insert x s)
z : E
hz : z ∈ insert x s ∩ Metric.eball x r
⊢ x + (z - x) ∈ insert x s

Tactic:
· simpa only [edist_eq_enorm_sub, Metric.mem_eball] using! hz.2

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hu : UniqueDiffOn 𝕜 (insert x s)
z : E
hz : z ∈ insert x s ∩ Metric.eball x r
⊢ x + (z - x) ∈ insert x s
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 : ℕ), (f.toFormalMultilinearSeries.changeOriginSeries 1 n) fun x_1 ↦ x) (Fin.snoc 0 y) = 0

Tactic:
changeOriginSeries_support _ (this _),

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 ι
⊢ (∑' (n : ℕ), 0 fun x_1 ↦ x) (Fin.snoc 0 y) = 0
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
f : k → E
x y : k
⊢ slope (fun t ↦ -f t) x y = -slope f x y

Tactic:
simp only [slope_def_module, neg_sub_neg, ← smul_neg, neg_sub]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: case neg.refine_2
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
hxy : x ≤ y
hxeqy : ¬x = y
h : f x ≤ f y
⊢ 0 ≤ f y -ᵥ f x

Tactic:
rwa [vsub_eq_sub, sub_nonneg]

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
f : 𝕜 → E
z₀ : 𝕜
m n : ℤ
hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z
⊢ m = n

Tactic:
wlog! h_le : n ≤ m generalizing m n

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
m n : ℤ
hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z
this :
  ∀ {m n : ℤ},
    (∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z) →
      (∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z) → n ≤ m → m = n
h_le : m < n
⊢ m = n

𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
m n : ℤ
hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z
h_le : n ≤ m
⊢ m = n
Module: Mathlib.Analysis.Calculus.Deriv.CompMul

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
f : 𝕜 → E
x : 𝕜
⊢ deriv (fun x ↦ f (c * x)) x = c • deriv f (c * x)

Tactic:
by
  simp only [← smul_eq_mul, deriv, fderiv_comp_smul, smul_apply]

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

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
t : Set F
hl : HasFDerivWithinAt l l' t y
hf : HasDerivWithinAt f f' s x
hst : MapsTo f s t
hy : y = f x
⊢ HasDerivWithinAt (l ∘ f) (l' f') s x

Tactic:
by
  rw [hy] at hl; exact hl.comp_hasDerivWithinAt x hf hst

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.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
s : Set E
x : E
g : F ≃ₗᵢ[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
⊢ ‖iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖

Tactic:
have :
    iteratedFDerivWithin 𝕜 i (g ∘ f) s x =
      (g : F →L[𝕜] G).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x) :=
    g.toContinuousLinearEquiv.iteratedFDerivWithin_comp_left f hs hx i
  rw [this]
  apply LinearIsometry.norm_compContinuousMultilinearMap g.toLinearIsometry

Goal state after: