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

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

Tactic:
refine ⟨⟨?_, r_pos, ?_⟩, fun n _ ↦ hp n⟩

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
x : E
r : ℝ≥0∞
hf : ∀ y ∈ Metric.eball x r, f y = 0
r_pos : 0 < r
hp : ∀ (n : ℕ), p n = 0
⊢ r ≤ p.radius

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
x : E
r : ℝ≥0∞
hf : ∀ y ∈ Metric.eball x r, f y = 0
r_pos : 0 < r
hp : ∀ (n : ℕ), p n = 0
⊢ ∀ {y : E}, y ∈ Metric.eball 0 r → HasSum (fun n ↦ (p n) fun x ↦ y) (f (x + y))
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: case neg.refine_1.refine_2
𝕜 : 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
⊢ Tendsto (fun n ↦ ‖‖‖c (n + 1)‖ * ↑r' ^ (n + 1)‖‖ / ‖‖‖c n‖ * ↑r' ^ n‖‖) atTop (𝓝 ↑(r' * r))

Tactic:
simp_rw [norm_norm]
      exact tendsto_succ_norm_div_norm c hrz hc

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁵ : CommRing 𝕜
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : AddCommGroup F
inst✝¹² : AddCommGroup G
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : Module 𝕜 G
inst✝⁸ : TopologicalSpace E
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousConstSMul 𝕜 E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
v : Fin 1 → E
this : {Composition.ones 1} = Finset.univ
⊢ (q (Composition.ones 1).length) (p.applyComposition (Composition.ones 1) v) = (q 1) fun _i ↦ (p 1) v

Tactic:
refine q.congr (by simp) fun i hi1 hi2 => ?_

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁵ : CommRing 𝕜
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : AddCommGroup F
inst✝¹² : AddCommGroup G
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : Module 𝕜 G
inst✝⁸ : TopologicalSpace E
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousConstSMul 𝕜 E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
v : Fin 1 → E
this : {Composition.ones 1} = Finset.univ
i : ℕ
hi1 : i < (Composition.ones 1).length
hi2 : i < 1
⊢ p.applyComposition (Composition.ones 1) v ⟨i, hi1⟩ = (p 1) 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✝¹⁵ : CommRing 𝕜
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : AddCommGroup F
inst✝¹² : AddCommGroup G
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : Module 𝕜 G
inst✝⁸ : TopologicalSpace E
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousConstSMul 𝕜 E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
⊢ q.comp p.removeZero = q.comp p

Tactic:
ext n; simp [FormalMultilinearSeries.comp]

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

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 : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n
⊢ 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')
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
⊢ ∑ e ∈ (Ico 2 (n + 1)).sigma fun n_1 ↦ Fintype.piFinset fun _i ↦ Ico 1 n, ∏ j, r * (a ^ e.snd j * p (e.snd j)) =
    ∑ j ∈ Ico 2 (n + 1), r ^ j * (∑ k ∈ Ico 1 n, a ^ k * p k) ^ j

Tactic:
← sum_sigma' (Ico 2 (n + 1))
          (fun k : ℕ => (Fintype.piFinset fun _ : Fin k => Ico 1 n : Finset (Fin k → ℕ)))
          (fun n e => ∏ j : Fin n, r * (a ^ e j * p (e j)))

Goal state after:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
⊢ ∑ a_1 ∈ Ico 2 (n + 1), ∑ s ∈ Fintype.piFinset fun x ↦ Ico 1 n, ∏ j, r * (a ^ s j * p (s j)) =
    ∑ j ∈ Ico 2 (n + 1), r ^ j * (∑ k ∈ Ico 1 n, a ^ k * p k) ^ j
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: case pos
𝕜 : 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
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x | (fun x ↦ f x = g x) x}
g' : E → F := u.piecewise g f
y : E
hy : y ∈ insert x s
h'y : y ∈ u
⊢ f y = g' y

pp: case neg
𝕜 : 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
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x | (fun x ↦ f x = g x) x}
g' : E → F := u.piecewise g f
y : E
hy : y ∈ insert x s
h'y : y ∉ u
⊢ f y = g' y

Tactic:
· have : y ∈ u ∩ insert x s := ⟨h'y, hy⟩
        simpa [g', h'y, this] using hu this

Goal state after:
case neg
𝕜 : 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
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x | (fun x ↦ f x = g x) x}
g' : E → F := u.piecewise g f
y : E
hy : y ∈ insert x s
h'y : y ∉ u
⊢ f y = g' y
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✝
f : OpenPartialHomeomorph E✝ F✝
a : E✝
i : E✝ ≃L[𝕜] F✝
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E✝ F✝
h : HasFPowerSeriesAt (↑f) p a
hp : p 1 = (continuousMultilinearCurryFin1 𝕜 E✝ F✝).symm ↑i
A : HasFPowerSeriesAt (↑f.symm ∘ ↑f) ((p.leftInv i a).comp p) a
B : ∀ᶠ (y : E✝) in 𝓝 0, HasSum (fun n ↦ (p.leftInv i a n) fun x ↦ ↑f (a + y) - ↑f a) (↑f.symm (↑f (a + y)))
C : ∀ᶠ (y : E✝) in 𝓝 a, HasSum (fun n ↦ (p.leftInv i a n) fun x ↦ ↑f y - ↑f a) (↑f.symm (↑f y))
D : ∀ᶠ (y : E✝) in 𝓝 (↑f.symm (↑f a)), HasSum (fun n ↦ (p.leftInv i a n) fun x ↦ ↑f y - ↑f a) y
E : ∀ᶠ (z : F✝) in 𝓝 (↑f a), HasSum (fun n ↦ (p.leftInv i a n) fun x ↦ ↑f (↑f.symm z) - ↑f a) (↑f.symm z)
F : ∀ᶠ (z : F✝) in 𝓝 (↑f a), HasSum (fun n ↦ (p.leftInv i a n) fun x ↦ z - ↑f a) (↑f.symm z)
r : ℝ≥0∞
r_pos : r > 0
hr : Metric.eball (↑f a) r ⊆ {x | (fun z ↦ HasSum (fun n ↦ (p.leftInv i a n) fun x ↦ z - ↑f a) (↑f.symm z)) x}
y : F✝
hy : y ∈ Metric.eball 0 (min r (p.leftInv i a).radius)
⊢ HasSum (fun n ↦ (p.leftInv i a n) fun x ↦ y) (↑f.symm (↑f a + y))

Tactic:
have : y + f a ∈ Metric.eball (f a) r := by
    simp only [Metric.mem_eball, edist_eq_enorm_sub, sub_zero, lt_min_iff,
      add_sub_cancel_right] at hy ⊢
    exact hy.1

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✝
f : OpenPartialHomeomorph E✝ F✝
a : E✝
i : E✝ ≃L[𝕜] F✝
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E✝ F✝
h : HasFPowerSeriesAt (↑f) p a
hp : p 1 = (continuousMultilinearCurryFin1 𝕜 E✝ F✝).symm ↑i
A : HasFPowerSeriesAt (↑f.symm ∘ ↑f) ((p.leftInv i a).comp p) a
B : ∀ᶠ (y : E✝) in 𝓝 0, HasSum (fun n ↦ (p.leftInv i a n) fun x ↦ ↑f (a + y) - ↑f a) (↑f.symm (↑f (a + y)))
C : ∀ᶠ (y : E✝) in 𝓝 a, HasSum (fun n ↦ (p.leftInv i a n) fun x ↦ ↑f y - ↑f a) (↑f.symm (↑f y))
D : ∀ᶠ (y : E✝) in 𝓝 (↑f.symm (↑f a)), HasSum (fun n ↦ (p.leftInv i a n) fun x ↦ ↑f y - ↑f a) y
E : ∀ᶠ (z : F✝) in 𝓝 (↑f a), HasSum (fun n ↦ (p.leftInv i a n) fun x ↦ ↑f (↑f.symm z) - ↑f a) (↑f.symm z)
F : ∀ᶠ (z : F✝) in 𝓝 (↑f a), HasSum (fun n ↦ (p.leftInv i a n) fun x ↦ z - ↑f a) (↑f.symm z)
r : ℝ≥0∞
r_pos : r > 0
hr : Metric.eball (↑f a) r ⊆ {x | (fun z ↦ HasSum (fun n ↦ (p.leftInv i a n) fun x ↦ z - ↑f a) (↑f.symm z)) x}
y : F✝
hy : y ∈ Metric.eball 0 (min r (p.leftInv i a).radius)
this : y + ↑f a ∈ Metric.eball (↑f a) r
⊢ HasSum (fun n ↦ (p.leftInv i a n) fun x ↦ y) (↑f.symm (↑f a + y))
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: case neg
𝕜 : 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 : G → E
s : Set G
x : G
hxs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
this : ¬DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x
⊢ fderivWithin 𝕜 (⇑iso ∘ f) s x = ↑iso ∘SL fderivWithin 𝕜 f s x

Tactic:
fderivWithin_zero_of_not_differentiableWithinAt h,

Goal state after:
case neg
𝕜 : 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 : G → E
s : Set G
x : G
hxs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
this : ¬DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x
⊢ fderivWithin 𝕜 (⇑iso ∘ f) s x = ↑iso ∘SL 0
Module: Mathlib.Analysis.Calculus.FDeriv.Add

Goal state before:
pp: case neg
𝕜 : 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
hxs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ fderivWithin 𝕜 (fun y ↦ -f y) s x = -fderivWithin 𝕜 f s x

Tactic:
fderivWithin_zero_of_not_differentiableWithinAt h,

Goal state after:
case neg
𝕜 : 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
hxs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ fderivWithin 𝕜 (fun y ↦ -f y) s x = -0
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: case neg
𝕜 : 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
x : E
hxs : UniqueDiffWithinAt 𝕜 (⇑iso ⁻¹' s) x
h : ¬DifferentiableWithinAt 𝕜 f s (iso x)
this : ¬DifferentiableWithinAt 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) x
⊢ fderivWithin 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) x = fderivWithin 𝕜 f s (iso x) ∘SL ↑iso

Tactic:
fderivWithin_zero_of_not_differentiableWithinAt h,

Goal state after:
case neg
𝕜 : 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
x : E
hxs : UniqueDiffWithinAt 𝕜 (⇑iso ⁻¹' s) x
h : ¬DifferentiableWithinAt 𝕜 f s (iso x)
this : ¬DifferentiableWithinAt 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) x
⊢ fderivWithin 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) x = 0 ∘SL ↑iso
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
L : Filter E
⊢ Tendsto (fun x' ↦ ‖x' - x‖⁻¹ • (f x' - f x - f' (x' - x))) L (𝓝 0) ↔
    Tendsto (fun x' ↦ ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (𝓝 0)

Tactic:
rw [tendsto_iff_norm_sub_tendsto_zero]

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
L : Filter E
⊢ Tendsto (fun e ↦ ‖‖e - x‖⁻¹ • (f e - f x - f' (e - x)) - 0‖) L (𝓝 0) ↔
    Tendsto (fun x' ↦ ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (𝓝 0)
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f : F [⋀^ι]→L[𝕜] G
dg : E →L[𝕜] F
v : ι → E
i : ι
⊢ ‖f‖ * (‖dg (v i)‖ * ∏ i_1 ∈ {i}ᶜ, ‖(Function.update (fun x ↦ g) i dg i_1) (v i_1)‖) ≤
    ‖f‖ * (‖dg‖ * (‖v i‖ * (‖g‖ ^ (Fintype.card ι - 1) * ∏ i ∈ {i}ᶜ, ‖v i‖)))

Tactic:
dg.le_opNorm,

Goal state after:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f : F [⋀^ι]→L[𝕜] G
dg : E →L[𝕜] F
v : ι → E
i : ι
⊢ ‖f‖ * (‖dg‖ * ‖v i‖ * ∏ i_1 ∈ {i}ᶜ, ‖(Function.update (fun x ↦ g) i dg i_1) (v i_1)‖) ≤
    ‖f‖ * (‖dg‖ * (‖v i‖ * (‖g‖ ^ (Fintype.card ι - 1) * ∏ i ∈ {i}ᶜ, ‖v i‖)))
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
f : E → F
m n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
hmn : m ≤ n
⊢ HasFTaylorSeriesUpTo m f p

Tactic:
rw [← hasFTaylorSeriesUpToOn_univ_iff] at h ⊢; exact h.of_le hmn

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

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

Tactic:
← mul_smul _ (-1),

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
c' d' : 𝔸
hc : HasDerivWithinAt c c' univ x
hd : HasDerivWithinAt d d' univ x
⊢ HasDerivWithinAt (c * d) (c' * d x + c x * d') univ x

Tactic:
exact HasDerivWithinAt.mul hc hd

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

Goal state before:
pp: case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (-f) s x = -derivWithin f s x

Tactic:
simp only [derivWithin, fderivWithin_neg hsx, neg_apply]

Goal state after:
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 : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
⊢ 0 ≤ slope f x y

Tactic:
rcases le_total x y with hxy | hxy

Goal state after:
case inl
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 : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
hxy : x ≤ y
⊢ 0 ≤ slope f x y

case inr
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 : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
hxy : y ≤ x
⊢ 0 ≤ slope f x y
Module: Mathlib.Analysis.Analytic.Uniqueness

Goal state before:
pp: case refine_1
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ m < k, ∀ (y : E), ((p m) fun x ↦ y) = 0
z : E
b : ℕ
hb : b ∈ Finset.range (k + 1)
hnb : b ≠ k
⊢ ((p b) fun x ↦ z) = 0

Tactic:
have := Finset.mem_range_succ_iff.mp hb
      simp only [hk b (this.lt_of_ne hnb)]

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

Goal state before:
pp: case inr
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x ↦ (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
⊢ ({x | f x ≤ B x} ∩ Ioc x y).Nonempty

Tactic:
· rcases exists_between (bound x xab hxB) with ⟨r, hfr, hrB⟩
    specialize hf' x xab r hfr
    have HB : ∀ᶠ z in 𝓝[>] x, r < slope B x z :=
      (hasDerivWithinAt_iff_tendsto_slope' <| lt_irrefl x).1 (hB' x xab).Ioi_of_Ici
        (Ioi_mem_nhds hrB)
    obtain ⟨z, hfz, hzB, hz⟩ : ∃ z, slope f x z < r ∧ r < slope B x z ∧ z ∈ Ioc x y :=
      hf'.and_eventually (HB.and (Ioc_mem_nhdsGT hy)) |>.exists
    refine ⟨z, ?_, hz⟩
    have := (hfz.trans hzB).le
    rwa [slope_def_field, slope_def_field, div_le_div_iff_of_pos_right (sub_pos.2 hz.1), hxB,
      sub_le_sub_iff_right] at this

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

Goal state before:
pp: case hB'
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
x✝ : ℝ
hx✝ : x✝ ∈ Icc a b
r : ℝ
hr : r > 0
x : ℝ
hx : x ∈ Ico a b
⊢ HasDerivWithinAt (fun x ↦ B x + r * (x - a)) (?m.110 x) (Ici x) x

Tactic:
exact (hB' x hx).add (((hasDerivWithinAt_id x (Ici x)).sub_const a).const_mul r)

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
n : ℕ∞ω
f : E → F
g : F →L[𝕜] G
hf : ContDiffWithinAt 𝕜 n f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
hi : ↑i ≤ n
⊢ iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x = g.compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x)

Tactic:
rcases hf.contDiffOn' hi (by simp) with ⟨U, hU, hxU, hfU⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
x : E
n : ℕ∞ω
f : E → F
g : F →L[𝕜] G
hf : ContDiffWithinAt 𝕜 n f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
hi : ↑i ≤ n
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hxU : x ∈ U
hfU : ContDiffOn 𝕜 (↑i) f (insert x s ∩ U)
⊢ iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x = g.compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x)
Module: Mathlib.Analysis.Calculus.MeanValue

Goal state before:
pp: case hab
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
f' : E → E →L[𝕜] G
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
h1 : ∀ᶠ (x : E) in 𝓝[s] x₀, x ∈ s
x : E
hxs : x ∈ s
h : ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖y - x₀‖ ^ n
y : E
hy : y ∈ [x₀ -[ℝ] x]
⊢ ‖y - x₀‖ ≤ ‖x - x₀‖

Tactic:
exact norm_sub_le_of_mem_segment hy

Goal state after: