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

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

Tactic:
rw [nhdsWithin_inter_of_mem']
    · exact inter_mem_nhdsWithin _ this
    · apply mem_nhdsWithin_of_mem_nhds
      apply Filter.mem_of_superset this (Metric.eball_subset_eball hr'.le)

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✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' ↑r
y : E
h'y : x + y ∈ insert x s
hy : y ∈ Metric.eball 0 (min rf' ↑r)
y_mem : y ∈ Metric.eball 0 rf
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
A : Tendsto (fun n ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a) fun x ↦ y)) atTop (atTop ×ˢ 𝓝 (f (x + y) - f x))
B : Tendsto (fun n ↦ q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a) fun _b ↦ y)) atTop (𝓝 (g (f (x + y))))
C :
  Tendsto (fun n ↦ ∑ i ∈ compPartialSumTarget 0 n n, (q.compAlongComposition p i.snd) fun _j ↦ y) atTop
    (𝓝 (g (f (x + y))))
⊢ ∀ (i : (n : ℕ) × Composition n),
    ‖(q.compAlongComposition p i.snd) fun _j ↦ y‖ ≤ ‖q.compAlongComposition p i.snd‖ * ↑r ^ i.fst

Tactic:
rintro ⟨n, c⟩

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
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' ↑r
y : E
h'y : x + y ∈ insert x s
hy : y ∈ Metric.eball 0 (min rf' ↑r)
y_mem : y ∈ Metric.eball 0 rf
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
A : Tendsto (fun n ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a) fun x ↦ y)) atTop (atTop ×ˢ 𝓝 (f (x + y) - f x))
B : Tendsto (fun n ↦ q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a) fun _b ↦ y)) atTop (𝓝 (g (f (x + y))))
C :
  Tendsto (fun n ↦ ∑ i ∈ compPartialSumTarget 0 n n, (q.compAlongComposition p i.snd) fun _j ↦ y) atTop
    (𝓝 (g (f (x + y))))
n : ℕ
c : Composition n
⊢ ‖(q.compAlongComposition p ⟨n, c⟩.snd) fun _j ↦ y‖ ≤ ‖q.compAlongComposition p ⟨n, c⟩.snd‖ * ↑r ^ ⟨n, c⟩.fst
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: case mpr.a
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
g : E → F
hfg : EqOn f g (insert x s ∩ eball x r)
hg : HasFPowerSeriesOnBall g p x r
y : E
ys : x + y ∈ insert x s
lt : y ∈ eball 0 r
⊢ x + y ∈ insert x s ∩ eball x r

Tactic:
refine ⟨ys, ?_⟩
      simpa only [mem_eball, edist_eq_enorm_sub, add_sub_cancel_left, sub_zero] using lt

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 → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r1 ^ i.fst
r : ℝ≥0∞ := min r0 ↑r1
this : Metric.eball 0 r ∈ 𝓝 0
y : E
hy : y ∈ Metric.eball 0 r
hy0 : y ∈ Metric.eball 0 r0
⊢ ∀ (i : (n : ℕ) × Composition n),
    ‖(q.compAlongComposition p i.snd) fun _j ↦ y‖ ≤ ‖q.compAlongComposition p i.snd‖ * ↑r1 ^ i.fst

Tactic:
rintro ⟨n, c⟩

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 → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r1 ^ i.fst
r : ℝ≥0∞ := min r0 ↑r1
this : Metric.eball 0 r ∈ 𝓝 0
y : E
hy : y ∈ Metric.eball 0 r
hy0 : y ∈ Metric.eball 0 r0
n : ℕ
c : Composition n
⊢ ‖(q.compAlongComposition p ⟨n, c⟩.snd) fun _j ↦ y‖ ≤ ‖q.compAlongComposition p ⟨n, c⟩.snd‖ * ↑r1 ^ ⟨n, c⟩.fst
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
x : E
q : FormalMultilinearSeries 𝕜 F G
m : ℕ
hm : HasFiniteFPowerSeriesAt g q (f x) m
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : HasFiniteFPowerSeriesAt f p x n
⊢ CPolynomialAt 𝕜 (g ∘ f) x

Tactic:
refine ⟨q.comp p, m * (n + 1), ?_⟩

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
g : F → G
f : E → F
x : E
q : FormalMultilinearSeries 𝕜 F G
m : ℕ
hm : HasFiniteFPowerSeriesAt g q (f x) m
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : HasFiniteFPowerSeriesAt f p x n
⊢ HasFiniteFPowerSeriesAt (g ∘ f) (q.comp p) x (m * (n + 1))
Module: Mathlib.Analysis.Analytic.Composition

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

Tactic:
← ofFn_get (splitWrtComposition a.blocks b)

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
n✝ n : ℕ
a : Composition n
b : Composition a.length
| (ofFn (a.blocks.splitWrtComposition b).get).flatten
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕝 : Type u_8
inst✝¹ : NormedDivisionRing 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
s : Set E
n : ℤ
h₁f : AnalyticWithinAt 𝕜 f s z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
| AnalyticWithinAt 𝕜 (f ^ (- -n)) s z

Tactic:
conv =>

Goal state after:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕝 : Type u_8
inst✝¹ : NormedDivisionRing 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
s : Set E
n : ℤ
h₁f : AnalyticWithinAt 𝕜 f s z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
x : E
| (f ^ (-n))⁻¹ x
Module: Mathlib.Analysis.Analytic.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
⊢ HasFPowerSeriesAt (↑f.symm) (p.leftInv i a) (↑f a)

Tactic:
have B : ∀ᶠ (y : E) in 𝓝 0, HasSum (fun n ↦ (p.leftInv i a n) fun _ ↦ f (a + y) - f a)
      (f.symm (f (a + y))) := by
    simpa using! A.eventually_hasSum_of_comp h (radius_leftInv_pos_of_radius_pos h.radius_pos hp)

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)))
⊢ HasFPowerSeriesAt (↑f.symm) (p.leftInv i a) (↑f a)
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕝 : Type u_8
inst✝¹ : NormedDivisionRing 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
n : ℤ
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
| AnalyticAt 𝕜 (f ^ (- -n)) z

Tactic:
conv =>

Goal state after:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕝 : Type u_8
inst✝¹ : NormedDivisionRing 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
n : ℤ
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
x : E
| (f ^ (-n))⁻¹ x
Module: Mathlib.Analysis.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
c : F
⊢ DifferentiableWithinAt 𝕜 (fun y ↦ c - f y) s x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
by
  simp [sub_eq_add_neg]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Alternating.Topology

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F✝ : Type u_3
ι : Type u_4
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : AddCommGroup E
inst✝¹² : Module 𝕜 E
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : AddCommGroup F✝
inst✝⁹ : Module 𝕜 F✝
inst✝⁸ : UniformSpace F✝
inst✝⁷ : IsUniformAddGroup F✝
inst✝⁶ : ContinuousSMul 𝕜 E
h : IsCoherentWith {s | IsVonNBounded 𝕜 s}
F : Type u_3
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : UniformSpace F
inst✝² : IsUniformAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
hF : T2Space F
this : CompleteSpace (ContinuousMultilinearMap 𝕜 (fun i ↦ E) F)
⊢ CompleteSpace (E [⋀^ι]→L[𝕜] F)

Tactic:
completeSpace_iff_isComplete_range
    isUniformEmbedding_toContinuousMultilinearMap.isUniformInducing

Goal state after:
𝕜 : Type u_1
E : Type u_2
F✝ : Type u_3
ι : Type u_4
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : AddCommGroup E
inst✝¹² : Module 𝕜 E
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : AddCommGroup F✝
inst✝⁹ : Module 𝕜 F✝
inst✝⁸ : UniformSpace F✝
inst✝⁷ : IsUniformAddGroup F✝
inst✝⁶ : ContinuousSMul 𝕜 E
h : IsCoherentWith {s | IsVonNBounded 𝕜 s}
F : Type u_3
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : UniformSpace F
inst✝² : IsUniformAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
hF : T2Space F
this : CompleteSpace (ContinuousMultilinearMap 𝕜 (fun i ↦ E) F)
⊢ IsComplete (range toContinuousMultilinearMap)
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: case hp
α : Type u
β : Type v
inst✝⁵ : PseudoMetricSpace α
M : Type u_1
inst✝⁴ : Zero M
inst✝³ : Zero α
inst✝² : SMul M α
inst✝¹ : PseudoMetricSpace M
inst✝ : IsBoundedSMul M α
c : M
⊢ IsClosed {x | dist (c • x.1) (c • x.2) ≤ dist c 0 * dist x.1 x.2}

Tactic:
exact isClosed_le (by fun_prop) (by fun_prop)

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

Goal state before:
pp: case hp
α : Type u
β : Type v
inst✝⁵ : PseudoMetricSpace α
M : Type u_1
inst✝⁴ : Zero M
inst✝³ : Zero α
inst✝² : SMul M α
inst✝¹ : PseudoMetricSpace M
inst✝ : IsBoundedSMul M α
c₁ c₂ : M
⊢ IsClosed {a | dist (c₁ • a) (c₂ • a) ≤ dist c₁ c₂ * dist a 0}

Tactic:
exact isClosed_le (by fun_prop) (by fun_prop)

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
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ HasFPowerSeriesWithinOnBall (fderivWithin 𝕜 f s) p.derivSeries s x r

Tactic:
have : insert x s = s := insert_eq_of_mem hx
  rw [← this] at hu
  convert! h.fderivWithin hu
  exact this.symm

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

Goal state before:
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
hx : x ∉ tsupport fun x ↦ (B (u x)) (v x)
hxv : x ∉ tsupport v
⊢ (B (u x)) v' + (B u') (v x) = 0

Tactic:
simp [image_eq_zero_of_notMem_tsupport hxu, image_eq_zero_of_notMem_tsupport hxv]

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
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticWithinAt 𝕜 f s x
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn n f p u ∧ ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u

Tactic:
by
  rcases h.exists_analyticAt with ⟨g, -, fg, hg⟩
  rcases hg.exists_mem_nhds_analyticOnNhd with ⟨v, vx, hv⟩
  refine ⟨insert x s ∩ v, inter_mem_nhdsWithin _ vx, ftaylorSeries 𝕜 g, ?_, fun i ↦ ?_⟩
  · suffices HasFTaylorSeriesUpToOn n g (ftaylorSeries 𝕜 g) (insert x s ∩ v) from
      this.congr (fun y hy ↦ fg hy.1)
    exact AnalyticOnNhd.hasFTaylorSeriesUpToOn _ (hv.mono Set.inter_subset_right)
  · exact (hv.iteratedFDeriv i).analyticOn.mono Set.inter_subset_right

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

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x c : 𝕜
⊢ HasDerivAt (fun x ↦ x * c) c x

Tactic:
by
  simpa only [one_mul] using (hasDerivAt_id' x).mul_const c

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

Goal state before:
pp: k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
⊢ (-(b - a))⁻¹ • (f a -ᵥ f b) = (a - b)⁻¹ • (f a -ᵥ f b)

Tactic:
neg_sub

Goal state after:
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
⊢ (a - b)⁻¹ • (f a -ᵥ f b) = (a - b)⁻¹ • (f a -ᵥ f b)
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: case pos
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b c : k
hab : ¬a = b
hbc : b = c
⊢ ((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c

Tactic:
subst hbc

Goal state after:
case pos
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
hab : ¬a = b
⊢ ((b - a) / (b - a)) • slope f a b + ((b - b) / (b - a)) • slope f b b = slope f a b
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
inst✝² : DecidableEq ι
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : (i : ι) → G → E i
g' : (i : ι) → G →L[𝕜] E i
s : Set G
x : G
hg : ∀ (i : ι), HasFDerivWithinAt (g i) (g' i) s x
⊢ HasFDerivWithinAt (fun x ↦ f fun i ↦ g i x) (∑ i, f.toContinuousLinearMap (fun j ↦ g j x) i ∘SL g' i) s x

Tactic:
by
  simpa using (hasFDerivWithinAt_const f x s).continuousMultilinearMap_apply hg

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x : (i : ι) → E i
H :
  (f.iteratedFDeriv n.succ x).curryLeft =
    ∑ e,
      (f.iteratedFDerivComponent e.toEquivRange).linearDeriv ((Pi.compRightL 𝕜 E Subtype.val) x) ∘SL
        Pi.compRightL 𝕜 E Subtype.val
⊢ HasFDerivAt (fun y ↦ f.iteratedFDeriv n y) (f.iteratedFDeriv n.succ x).curryLeft x

Tactic:
have A : HasFDerivAt (f.iteratedFDeriv n) (∑ e : Fin n ↪ ι,
          ((iteratedFDerivComponent f e.toEquivRange).linearDeriv (Pi.compRightL 𝕜 _ Subtype.val x))
            ∘L (Pi.compRightL 𝕜 _ Subtype.val)) x := by
        apply HasFDerivAt.fun_sum (fun s _hs ↦ ?_)
        exact (ContinuousMultilinearMap.hasFDerivAt _ _).comp x (ContinuousLinearMap.hasFDerivAt _)

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
n : ℕ
x : (i : ι) → E i
H :
  (f.iteratedFDeriv n.succ x).curryLeft =
    ∑ e,
      (f.iteratedFDerivComponent e.toEquivRange).linearDeriv ((Pi.compRightL 𝕜 E Subtype.val) x) ∘SL
        Pi.compRightL 𝕜 E Subtype.val
A :
  HasFDerivAt (f.iteratedFDeriv n)
    (∑ e,
      (f.iteratedFDerivComponent e.toEquivRange).linearDeriv ((Pi.compRightL 𝕜 E Subtype.val) x) ∘SL
        Pi.compRightL 𝕜 E Subtype.val)
    x
⊢ HasFDerivAt (fun y ↦ f.iteratedFDeriv n y) (f.iteratedFDeriv n.succ x).curryLeft x
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case cont
𝕜 : 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
n : ℕ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun x ↦ f.iteratedFDeriv n x

Tactic:
apply continuous_finsetSum _ (fun e _ ↦ ?_)

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
n : ℕ
e : Fin n ↪ ι
x✝ : e ∈ Finset.univ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun a ↦
    (f.iteratedFDerivComponent e.toEquivRange) ((Pi.compRightL 𝕜 E Subtype.val) a)
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
t : Set 𝕜
h : Dense t
⊢ univ ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (univ ∩ t)

Tactic:
simp [dense_iff_closure_eq.1 h]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap

Goal state before:
pp: a b R : ℝ
c : ℂ
h_R : R ≠ 0
x✝ : |a - b| ≤ 2 * π
x₁✝ : ℝ
left✝¹ : min a b < x₁✝
right✝¹ : x₁✝ ≤ max a b
x₂✝ : ℝ
left✝ : min a b < x₂✝
right✝ : x₂✝ ≤ max a b
h : circleMap c R x₁✝ = circleMap c R x₂✝
⊢ |x₁✝ - x₂✝| < 2 * π

Tactic:
rw [abs_lt]

Goal state after:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
x✝ : |a - b| ≤ 2 * π
x₁✝ : ℝ
left✝¹ : min a b < x₁✝
right✝¹ : x₁✝ ≤ max a b
x₂✝ : ℝ
left✝ : min a b < x₂✝
right✝ : x₂✝ ≤ max a b
h : circleMap c R x₁✝ = circleMap c R x₂✝
⊢ -(2 * π) < x₁✝ - x₂✝ ∧ x₁✝ - x₂✝ < 2 * π
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap

Goal state before:
pp: a b R : ℝ
c : ℂ
h_R : R ≠ 0
x✝ : b - a ≤ 2 * π
x₁✝ : ℝ
left✝¹ : a ≤ x₁✝
right✝¹ : x₁✝ < b
x₂✝ : ℝ
left✝ : a ≤ x₂✝
right✝ : x₂✝ < b
h : circleMap c R x₁✝ = circleMap c R x₂✝
⊢ |x₁✝ - x₂✝| < 2 * π

Tactic:
rw [abs_lt]

Goal state after:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
x✝ : b - a ≤ 2 * π
x₁✝ : ℝ
left✝¹ : a ≤ x₁✝
right✝¹ : x₁✝ < b
x₂✝ : ℝ
left✝ : a ≤ x₂✝
right✝ : x₂✝ < b
h : circleMap c R x₁✝ = circleMap c R x₂✝
⊢ -(2 * π) < x₁✝ - x₂✝ ∧ x₁✝ - x₂✝ < 2 * π
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
s : Set E
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasFDerivWithinAt (fun x ↦ f i x) (f' i) s x
⊢ HasFDerivWithinAt (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) l).prod)
    (∑ i,
      (List.map (fun x_1 ↦ f x_1 x) (List.take (↑i) l)).prod •>
        (f' l[i] <• (List.map (fun x_1 ↦ f x_1 x) (List.drop (↑i).succ l)).prod))
    s x

Tactic:
simp_rw [Fin.getElem_fin, ← l.get_eq_getElem, ← List.map_get_finRange l, List.map_map]
  refine .congr_fderiv (hasFDerivAt_list_prod_finRange'.comp_hasFDerivWithinAt x
    (hasFDerivWithinAt_pi.mpr fun i ↦ h (l.get i) (l.get_mem i)) :) ?_
  ext m
  simp_rw [List.map_take, List.map_drop, List.map_map, comp_apply, sum_apply, smul_apply,
    proj_apply, pi_apply, Function.comp_def]

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

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
this : (fun p ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) =o[𝓝 (x, x)] fun p ↦ (p.1 - p.2) * 1
⊢ HasStrictDerivAt Inv.inv (-(x ^ 2)⁻¹) x

Tactic:
refine .of_isLittleO <| this.congr' ?_ (Eventually.of_forall fun _ => mul_one _)
    refine Eventually.mono ((isOpen_ne.prod isOpen_ne).mem_nhds ⟨hx, hx⟩) ?_
    rintro ⟨y, z⟩ ⟨hy, hz⟩
    simp only [mem_ofPred_eq] at hy hz
    simp [field]
    ring

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
x : 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
y : 𝕜'
hg : DifferentiableAt 𝕜' g₁ y
hh : DifferentiableAt 𝕜 h x
hy : y = h x
⊢ deriv (g₁ ∘ h) x = deriv h x • deriv g₁ (h x)

Tactic:
by
  rw [hy] at hg; exact deriv.scomp x hg hh

Goal state after: