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
s t : Set E
x : E
h : AnalyticWithinAt 𝕜 f s x
hst : s =ᶠ[𝓝 x] t
⊢ AnalyticWithinAt 𝕜 f t x

Tactic:
refine h.mono_of_mem_nhdsWithin ?_

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s t : Set E
x : E
h : AnalyticWithinAt 𝕜 f s x
hst : s =ᶠ[𝓝 x] t
⊢ s ∈ 𝓝[t] x
Module: Mathlib.Analysis.Analytic.Basic

Goal state before:

Tactic:
‖(p n) fun _ : Fin n => y‖
    _ ≤ ‖p n‖ * ∏ _i : Fin n, ‖y‖ := ContinuousMultilinearMap.le_opNorm _ _
    _ = ‖p n‖ * (r' : ℝ) ^ n * (‖y‖ / r') ^ n := by simp [field, div_pow]
    _ ≤ C * a ^ n * (‖y‖ / r') ^ n := by gcongr ?_ * _; apply hp
    _ ≤ C * (a * (‖y‖ / r')) ^ n := by rw [mul_pow, mul_assoc]

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

Goal state before:
pp: case hf
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
x : (i : ℕ) × Composition i
a✝¹ : x ∈ compPartialSumTarget 2 (n + 1) n
a✝ : x ∉ (Ico 2 (n + 1)).sigma fun k ↦ {c | 1 < c.length}.toFinset
⊢ 0 ≤ ∏ j, r * (a ^ x.snd.blocksFun j * p (x.snd.blocksFun j))

Tactic:
exact prod_nonneg fun j _ ↦ (by positivity [ha, hp (x.snd.blocksFun j)])

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
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
⊢ a * I + ∑ k ∈ Ico 2 (n + 1), a ^ k * ‖p.rightInv i x k‖ =
    a * I +
      ∑ k ∈ Ico 2 (n + 1),
        a ^ k *
          ‖(↑i.symm).compContinuousMultilinearMap
              (∑ c ∈ {c | 1 < c.length}.toFinset, p.compAlongComposition (p.rightInv i x) c)‖

Tactic:
by
      congr! 2 with j hj
      rw [rightInv_coeff _ _ _ _ (mem_Ico.1 hj).1, norm_neg]

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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
⊢ ∃ a, ∃ (_ : 0 < a), 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1 ∧ r * (I + 1) * a ≤ 1 / 2

Tactic:
have :
      Tendsto (fun a => 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a) (𝓝 0)
        (𝓝 (2 * I * C * r ^ 2 * (I + 1) ^ 2 * 0)) :=
      tendsto_const_nhds.mul tendsto_id

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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
this : Tendsto (fun a ↦ 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a) (𝓝 0) (𝓝 (2 * I * C * r ^ 2 * (I + 1) ^ 2 * 0))
⊢ ∃ a, ∃ (_ : 0 < a), 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1 ∧ r * (I + 1) * a ≤ 1 / 2
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: case succ
𝕜 : 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
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : ℕ → ℝ := fun n ↦ ∑ k ∈ Ico 1 n, a ^ k * ‖p.rightInv i x k‖
n : ℕ
⊢ 1 ≤ n → S n ≤ (I + 1) * a → S (n + 1) ≤ (I + 1) * a

Tactic:
one_le_n

Goal state after:
case succ
𝕜 : 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
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : ℕ → ℝ := fun n ↦ ∑ k ∈ Ico 1 n, a ^ k * ‖p.rightInv i x k‖
n : ℕ
one_le_n : 1 ≤ n
⊢ S n ≤ (I + 1) * a → S (n + 1) ≤ (I + 1) * a
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))
⊢ Tendsto (fun n ↦ q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a) fun _b ↦ y)) atTop (𝓝 (g (f (x + y))))

Tactic:
have : Tendsto (fun (z : ℕ × F) ↦ q.partialSum z.1 z.2)
        (atTop ×ˢ 𝓝 (f (x + y) - f x)) (𝓝 (g (f x + (f (x + y) - f x)))) := by
      apply Hg.tendsto_partialSum_prod (y := f (x + y) - f x)
      · simpa [edist_eq_enorm_sub] using! fy_mem.2
      · simpa using! fy_mem.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
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))
this : Tendsto (fun z ↦ q.partialSum z.1 z.2) (atTop ×ˢ 𝓝 (f (x + y) - f x)) (𝓝 (g (f x + (f (x + y) - f x))))
⊢ Tendsto (fun n ↦ q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a) fun _b ↦ y)) atTop (𝓝 (g (f (x + y))))
Module: Mathlib.Analysis.Calculus.FDeriv.Comp

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
f' : E →L[𝕜] F
x : E
g : F → G
g' : F →L[𝕜] G
t : Set F
hf : HasFDerivAt f f' x
ht : ∀ᶠ (x' : E) in 𝓝 x, f x' ∈ t
hg : HasFDerivWithinAt g g' t (f x)
⊢ HasFDerivAt (g ∘ f) (g' ∘SL f') x

Tactic:
exact hg.comp_hasFDerivAt x hf ht

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
this : ∀ᶠ (y : E) in 𝓝 0, f (x + y) - f x ∈ Metric.eball 0 q.radius
y : E
hy : Tendsto (fun a ↦ q.partialSum a.1 (p.partialSum a.2 y - (p 0) fun x ↦ 0)) atTop (𝓝 ((g ∘ f) (x + y)))
h'y : Tendsto (fun n ↦ p.partialSum n y) atTop (𝓝 (f (x + y)))
⊢ f (x + y) - f x ∈ Metric.eball 0 q.radius → HasSum (fun n ↦ (q n) fun x_1 ↦ f (x + y) - f x) (g (f (x + y)))

Tactic:
h''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
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
this : ∀ᶠ (y : E) in 𝓝 0, f (x + y) - f x ∈ Metric.eball 0 q.radius
y : E
hy : Tendsto (fun a ↦ q.partialSum a.1 (p.partialSum a.2 y - (p 0) fun x ↦ 0)) atTop (𝓝 ((g ∘ f) (x + y)))
h'y : Tendsto (fun n ↦ p.partialSum n y) atTop (𝓝 (f (x + y)))
h''y : f (x + y) - f x ∈ Metric.eball 0 q.radius
⊢ HasSum (fun n ↦ (q n) fun x_1 ↦ f (x + y) - f x) (g (f (x + y)))
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 j : ι
hj : j ∈ {i}ᶜ
⊢ ?m.434 ≠ ?m.435

Tactic:
simpa using hj

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

Goal state before:
pp: case mp
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α) → ∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s

pp: case mpr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ (∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s) → s ∈ 𝓤 (Completion α)

Tactic:
· /- Start from an entourage `s`. It contains a closed entourage `t`. Its pullback in `α` is an
      entourage, so it contains an `ε`-neighborhood of the diagonal by definition of the entourages
      in metric spaces. Then `t` contains an `ε`-neighborhood of the diagonal in `Completion α`, as
      closed properties pass to the completion. -/
    intro hs
    rcases mem_uniformity_isClosed hs with ⟨t, ht, ⟨tclosed, ts⟩⟩
    have A : { x : α × α | (↑x.1, ↑x.2) ∈ t } ∈ uniformity α :=
      uniformContinuous_def.1 (uniformContinuous_coe α) t ht
    rcases mem_uniformity_dist.1 A with ⟨ε, εpos, hε⟩
    refine ⟨ε, εpos, @fun x y hxy ↦ ?_⟩
    have : ε ≤ dist x y ∨ (x, y) ∈ t := by
      refine induction_on₂ x y ?_ ?_
      · have : { x : Completion α × Completion α | ε ≤ dist x.fst x.snd ∨ (x.fst, x.snd) ∈ t } =
               { p : Completion α × Completion α | ε ≤ dist p.1 p.2 } ∪ t := by ext; simp
        rw [this]
        apply IsClosed.union _ tclosed
        exact isClosed_le continuous_const Completion.uniformContinuous_dist.continuous
      · intro x y
        rw [Completion.dist_eq]
        by_cases! h : ε ≤ dist x y
        · exact Or.inl h
        · have Z := hε h
          simp only [Set.mem_ofPred_eq] at Z
          exact Or.inr Z
    simp only [not_le.mpr hxy, false_or] at this
    exact ts this

Goal state after:
case mpr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ (∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s) → s ∈ 𝓤 (Completion α)
Module: Mathlib.Topology.MetricSpace.Completion

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

Tactic:
simpa [iInf_subtype] using @Completion.uniformity_dist' α _

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

Goal state before:
pp: case pos
𝕜 : 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) f p s ∧
    (∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y n) (p x n.succ).curryLeft s x) ∧ ContinuousOn (fun x ↦ p x (n + 1)) s
m : ℕ
hm : ↑m ≤ ↑n + 1
h' : m ≤ n
⊢ ContinuousOn (fun x ↦ p x m) s

pp: case neg
𝕜 : 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) f p s ∧
    (∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y n) (p x n.succ).curryLeft s x) ∧ ContinuousOn (fun x ↦ p x (n + 1)) s
m : ℕ
hm : ↑m ≤ ↑n + 1
h' : ¬m ≤ n
⊢ ContinuousOn (fun x ↦ p x m) s

Tactic:
· apply h.1.cont m (mod_cast h')

Goal state after:
case neg
𝕜 : 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) f p s ∧
    (∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y n) (p x n.succ).curryLeft s x) ∧ ContinuousOn (fun x ↦ p x (n + 1)) s
m : ℕ
hm : ↑m ≤ ↑n + 1
h' : ¬m ≤ n
⊢ ContinuousOn (fun x ↦ p x m) s
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case mp
𝕜 : 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn n f p univ
⊢ ∀ (m : ℕ), ↑m < n → ∀ (x : E), HasFDerivAt (fun y ↦ p y m) (p x m.succ).curryLeft x

Tactic:
simpa using H.fderivWithin

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
s : Set E
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
⊢ AnalyticOn 𝕜 (fderivWithin 𝕜 f s) s

Tactic:
intro x hx
  rcases h x hx with ⟨p, r, hr⟩
  refine ⟨p.derivSeries, r, hr.fderivWithin_of_mem_of_analyticOn h hu hx⟩

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
c : F
⊢ derivWithin (fun y ↦ f y - c) s x = derivWithin f s x

Tactic:
simp only [derivWithin, fderivWithin_sub_const]

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
c : F
⊢ deriv (fun x ↦ c - f x) x = -deriv f x

Tactic:
simp only [← derivWithin_univ, derivWithin_const_sub]

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
⊢ DifferentiableAt 𝕜 (fun x ↦ f (x - b)) a ↔ DifferentiableAt 𝕜 f (a - b)

Tactic:
by
  simp [sub_eq_add_neg, differentiableAt_comp_add_const]

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
⊢ DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun x ↦ f (x - b)) (a + b)

Tactic:
by
  simp [sub_eq_add_neg, differentiableAt_comp_add_const]

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R 𝕜
q : R[X]
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun x ↦ (aeval x) q) s x = (aeval x) (derivative q)

Tactic:
simpa only [aeval_def, eval₂_eq_eval_map, derivative_map] using
    (q.map (algebraMap R 𝕜)).derivWithin hxs

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
x : 𝕜
s : Set 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c y ∘SL d y) s x = derivWithin c s x ∘SL d x + c x ∘SL derivWithin d s x

Tactic:
exact (hc.hasDerivWithinAt.clm_comp hd.hasDerivWithinAt).derivWithin hsx

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

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
x : 𝕜
s : Set 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
⊢ derivWithin (fun y ↦ c y ∘SL d y) s x = derivWithin c s x ∘SL d x + c x ∘SL derivWithin d s x

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

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hpd : deriv f z₀ = p.coeff 1
hp0 : p.coeff 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n ↦ z ^ n • p.coeff n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n ↦ x ^ n • p.coeff n) (f (z₀ + x))
h : ¬x = 0
hxx : ∀ (n : ℕ), x⁻¹ * x ^ (n + 1) = x ^ n
⊢ HasSum (fun n ↦ x ^ n • p.coeff (n + 1)) (dslope f z₀ (z₀ + x))

Tactic:
suffices HasSum (fun n => x⁻¹ • x ^ (n + 1) • p.coeff (n + 1)) (x⁻¹ • (f (z₀ + x) - f z₀)) by
      simpa [dslope, slope, h, smul_smul, hxx] using this

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hpd : deriv f z₀ = p.coeff 1
hp0 : p.coeff 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n ↦ z ^ n • p.coeff n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n ↦ x ^ n • p.coeff n) (f (z₀ + x))
h : ¬x = 0
hxx : ∀ (n : ℕ), x⁻¹ * x ^ (n + 1) = x ^ n
⊢ HasSum (fun n ↦ x⁻¹ • x ^ (n + 1) • p.coeff (n + 1)) (x⁻¹ • (f (z₀ + x) - f z₀))
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
x : 𝕜
l : F → E
y : F
hl : DifferentiableAt 𝕜 l (f x)
hf : DifferentiableAt 𝕜 f x
hy : y = f x
⊢ deriv (l ∘ f) x = (fderiv 𝕜 l (f x)) (deriv f x)

Tactic:
exact fderiv_comp_deriv x hl hf

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

Goal state before:
pp: 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
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
φ : E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x - φ‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : E → G := fun y ↦ f y - φ y
hg : ∀ x ∈ s, HasFDerivWithinAt g (f' x - φ) s x
⊢ ‖f y - f x - φ (y - x)‖ ≤ C * ‖y - x‖

Tactic:
calc
    ‖f y - f x - φ (y - x)‖ = ‖f y - f x - (φ y - φ x)‖ := by simp
    _ = ‖f y - φ y - (f x - φ x)‖ := by congr 1; abel
    _ = ‖g y - g x‖ := by simp [g]
    _ ≤ C * ‖y - x‖ := Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le hg bound hs xs ys

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
f : E → F
x : E
n : ℕ∞ω
e : G ≃L[𝕜] E
⊢ ContDiffAt 𝕜 n (f ∘ ⇑e) (e.symm x) ↔ ContDiffAt 𝕜 n f x

Tactic:
rw [← contDiffWithinAt_univ, ← contDiffWithinAt_univ, ← preimage_univ]

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
f : E → F
x : E
n : ℕ∞ω
e : G ≃L[𝕜] E
⊢ ContDiffWithinAt 𝕜 n (f ∘ ⇑e) (?m.94 ⁻¹' univ) (e.symm x) ↔ ContDiffWithinAt 𝕜 n f univ x

𝕜 : 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
x : E
n : ℕ∞ω
e : G ≃L[𝕜] E
⊢ Type ?u.73

𝕜 : 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
x : E
n : ℕ∞ω
e : G ≃L[𝕜] E
⊢ G → ?m.93
Module: Mathlib.Analysis.Calculus.ContDiff.Comp

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
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
st : MapsTo f s t
hf : ContDiffWithinAt 𝕜 ω f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u
v : Set F
hv : v ∈ 𝓝[insert (f x) t] f x
q : F → FormalMultilinearSeries 𝕜 F G
hq : HasFTaylorSeriesUpToOn ω g q v
h'q : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ q x i) v
w : Set E := insert x s ∩ (u ∩ f ⁻¹' v)
wv : w ⊆ f ⁻¹' v
wu : w ⊆ u
⊢ AnalyticOn 𝕜 f w

Tactic:
have : AnalyticOn 𝕜 (fun y ↦ (continuousMultilinearCurryFin0 𝕜 E F).symm (f y)) w :=
          ((h'p 0).mono wu).congr fun y hy ↦ (hp.zero_eq' (wu hy)).symm

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
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
st : MapsTo f s t
hf : ContDiffWithinAt 𝕜 ω f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u
v : Set F
hv : v ∈ 𝓝[insert (f x) t] f x
q : F → FormalMultilinearSeries 𝕜 F G
hq : HasFTaylorSeriesUpToOn ω g q v
h'q : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ q x i) v
w : Set E := insert x s ∩ (u ∩ f ⁻¹' v)
wv : w ⊆ f ⁻¹' v
wu : w ⊆ u
this : AnalyticOn 𝕜 (fun y ↦ (continuousMultilinearCurryFin0 𝕜 E F).symm (f y)) w
⊢ AnalyticOn 𝕜 f w