mathlib-initiative/mathlib-tactics huggingface dataset:
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
ι : Type u_5
𝔸' : Type u_7
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst✝ : DecidableEq ι
x : E
hg : ∀ i ∈ u, HasStrictFDerivAt (g i) (g' i) x
⊢ HasStrictFDerivAt (fun x ↦ ∏ i ∈ u, g i x) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) •> g' i) x

Tactic:
by
  simpa [← Finset.prod_attach u] using .congr_fderiv
    (hasStrictFDerivAt_finsetProd.comp x <| hasStrictFDerivAt_pi.mpr fun i ↦ hg i i.prop)
    (by ext; simp [Finset.prod_erase_attach (g · x), ← u.sum_attach])

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
U : Set 𝕜
s : Set E
f : 𝕜 → E
hfU : AnalyticOnNhd 𝕜 f U
h₂f : ∀ x ∈ U, ¬EventuallyConst f (𝓝 x)
hs : s ∈ codiscreteWithin (f '' U)
⊢ f ⁻¹' s ∈ codiscreteWithin U

Tactic:
mem_codiscreteWithin,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
s : Set E
f : 𝕜 → E
hfU : AnalyticOnNhd 𝕜 f U
h₂f : ∀ x ∈ U, ¬EventuallyConst f (𝓝 x)
hs : ∀ x ∈ f '' U, Disjoint (𝓝[≠] x) (𝓟 (f '' U \ s))
⊢ ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ f ⁻¹' s))
Module: Mathlib.Analysis.Calculus.MeanValue

Goal state before:
pp: 𝕜 : Type u_3
G : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : E → G
hf : Differentiable 𝕜 f
hg : Differentiable 𝕜 g
hf' : ∀ (x : E), fderiv 𝕜 f x = fderiv 𝕜 g x
x : E
hfgx : f x = g x
⊢ f = g

Tactic:
let : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
  let A : NormedSpace ℝ E := .restrictScalars ℝ 𝕜 E
  suffices Set.univ.EqOn f g from funext fun x => this <| mem_univ x
  exact convex_univ.eqOn_of_fderivWithin_eq hf.differentiableOn hg.differentiableOn
    uniqueDiffOn_univ (fun x _ => by simpa using hf' _) (mem_univ _) hfgx

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
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
hf' : f' =o[𝓝[s] x₀] fun x ↦ ‖x - x₀‖ ^ n
⊢ (fun x ↦ f x - f x₀) =o[𝓝[s] x₀] fun x ↦ ‖x - x₀‖ ^ (n + 1)

Tactic:
rw [Asymptotics.isLittleO_iff] at hf' ⊢

Goal state after:
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
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖‖x - x₀‖ ^ n‖
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f x - f x₀‖ ≤ c * ‖‖x - x₀‖ ^ (n + 1)‖
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
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
hf' : f' =o[𝓝[s] x₀] fun x ↦ ‖x - x₀‖ ^ n
⊢ (fun x ↦ f x - f x₀) =o[𝓝[s] x₀] fun x ↦ ‖x - x₀‖ ^ (n + 1)

Tactic:
rw [Asymptotics.isLittleO_iff] at hf' ⊢
  intro c hc
  simp_rw [norm_pow, pow_succ, ← mul_assoc, norm_norm]
  simp_rw [norm_pow, norm_norm] at hf'
  have : ∀ᶠ x in 𝓝[s] x₀, segment ℝ x₀ x ⊆ s ∧ ∀ y ∈ segment ℝ x₀ x, ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n := by
    have h1 : ∀ᶠ x in 𝓝[s] x₀, x ∈ s := eventually_mem_nhdsWithin
    filter_upwards [h1, hs.eventually_nhdsWithin_segment hx₀s (hf' hc)] with x hxs h
    refine ⟨hs.segment_subset hx₀s hxs, fun y hy ↦ (h y hy).trans ?_⟩
    gcongr
    exact norm_sub_le_of_mem_segment hy
  filter_upwards [this] with x ⟨h_segment, h⟩
  convert!
    (convex_segment x₀ x).norm_image_sub_le_of_norm_hasFDerivWithin_le (f := fun x ↦ f x - f x₀)
      (y := x) (x := x₀) (s := segment ℝ x₀ x) ?_ h
      (left_mem_segment ℝ x₀ x)
      (right_mem_segment ℝ x₀ x) using 1
  · simp
  · simp only [hasFDerivWithinAt_sub_const_iff]
    exact fun x hx ↦ (hff' x (h_segment hx)).mono h_segment

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

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → E
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf' : f' =o[𝓝[s] x₀] fun x ↦ (x - x₀) ^ n
h : (fun x ↦ f x - f x₀) =o[𝓝[s] x₀] fun x ↦ ‖x - x₀‖ ^ (n + 1)
⊢ (fun x ↦ f x - f x₀) =o[𝓝[s] x₀] fun x ↦ (x - x₀) ^ (n + 1)

Tactic:
rw [Asymptotics.isLittleO_iff] at h ⊢
    simpa using h

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

Goal state before:
pp: case succ
𝕜 : 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
g : G ≃L[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : G},
    g x ∈ s →
      iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x =
        (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun x ↦ ↑g
x : G
hx : g x ∈ s
m : Fin (i + 1) → G
this :
  fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s)) (⇑g ⁻¹' s) x =
    fderivWithin 𝕜 (⇑(continuousMultilinearMapCongrLeft F fun _x ↦ g) ∘ iteratedFDerivWithin 𝕜 i f s ∘ ⇑g) (⇑g ⁻¹' s) x
⊢ ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s)) (⇑g ⁻¹' s) x) (m 0)) (tail m) =
    ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s (g x)) (g (m 0))) (tail fun i ↦ g (m i))

Tactic:
this,

Goal state after:
case succ
𝕜 : 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
g : G ≃L[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : G},
    g x ∈ s →
      iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x =
        (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun x ↦ ↑g
x : G
hx : g x ∈ s
m : Fin (i + 1) → G
this :
  fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s)) (⇑g ⁻¹' s) x =
    fderivWithin 𝕜 (⇑(continuousMultilinearMapCongrLeft F fun _x ↦ g) ∘ iteratedFDerivWithin 𝕜 i f s ∘ ⇑g) (⇑g ⁻¹' s) x
⊢ ((fderivWithin 𝕜 (⇑(continuousMultilinearMapCongrLeft F fun _x ↦ g) ∘ iteratedFDerivWithin 𝕜 i f s ∘ ⇑g) (⇑g ⁻¹' s) x)
        (m 0))
      (tail m) =
    ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s (g x)) (g (m 0))) (tail fun i ↦ g (m i))
Module: Mathlib.Analysis.Calculus.MeanValue

Goal state before:
pp: case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → E
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf' : f' =o[𝓝[s] x₀] fun x ↦ (x - x₀) ^ n
⊢ (fun x ↦ toSpanSingleton ℝ (f' x)) =o[𝓝[s] x₀] fun x ↦ ‖x - x₀‖ ^ n

Tactic:
rw [Asymptotics.isLittleO_iff] at hf' ⊢

Goal state after:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → E
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖(x - x₀) ^ n‖
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in 𝓝[s] x₀, ‖toSpanSingleton ℝ (f' x)‖ ≤ c * ‖‖x - x₀‖ ^ n‖
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
g : G ≃ₗᵢ[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
x : G
hx : g x ∈ s
i : ℕ
this :
  iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x =
    (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun x ↦ ↑↑g
⊢ ‖iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x‖ = ‖iteratedFDerivWithin 𝕜 i f s (g x)‖

Tactic:
this,

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
g : G ≃ₗᵢ[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
x : G
hx : g x ∈ s
i : ℕ
this :
  iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x =
    (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun x ↦ ↑↑g
⊢ ‖(iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun x ↦ ↑↑g‖ = ‖iteratedFDerivWithin 𝕜 i f s (g x)‖
Module: Mathlib.Analysis.Calculus.ContDiff.Deriv

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 (0 + 1) f s ↔ DifferentiableOn 𝕜 f s ∧ ContinuousOn (derivWithin f s) s

Tactic:
contDiffOn_succ_iff_derivWithin hs

Goal state after:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
hs : UniqueDiffOn 𝕜 s
⊢ DifferentiableOn 𝕜 f s ∧ (0 = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 0 (derivWithin f s) s ↔
    DifferentiableOn 𝕜 f s ∧ ContinuousOn (derivWithin f s) s
Module: Mathlib.Analysis.Calculus.ContDiff.Deriv

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 (∞ + 1) f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (∞ + 1) (derivWithin f s) s

Tactic:
contDiffOn_succ_iff_derivWithin hs

Goal state after:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
hs : UniqueDiffOn 𝕜 s
⊢ DifferentiableOn 𝕜 f s ∧ (∞ = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 ∞ (derivWithin f s) s ↔
    DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (∞ + 1) (derivWithin f s) s
Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft

Goal state before:
pp: case refine_1
𝕜 : 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 : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
a : E
s : Set E
t : Set F
hg : Tendsto g (𝓝[s] a) (𝓝[t] g a)
hf : HasFDerivWithinAt f f' t (g a)
hf' : Topology.IsEmbedding ⇑f'
hh : HasFDerivWithinAt h (f' ∘SL g') s a
hcomp : f ∘ g =ᶠ[𝓝[s] a] h
ha : a ∈ s
⊢ Tendsto (Prod.map g g) (𝓝[s] a ×ˢ pure a) (𝓝[t] g a ×ˢ pure (g a))

pp: case refine_2
𝕜 : 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 : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
a : E
s : Set E
t : Set F
hg : Tendsto g (𝓝[s] a) (𝓝[t] g a)
hf : HasFDerivWithinAt f f' t (g a)
hf' : Topology.IsEmbedding ⇑f'
hh : HasFDerivWithinAt h (f' ∘SL g') s a
hcomp : f ∘ g =ᶠ[𝓝[s] a] h
ha : a ∈ s
⊢ Prod.map (f ∘ g) (f ∘ g) =ᶠ[𝓝[s] a ×ˢ pure a] Prod.map h h

Tactic:
· exact hg.prodMap (by simp)

Goal state after:
case refine_2
𝕜 : 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 : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
a : E
s : Set E
t : Set F
hg : Tendsto g (𝓝[s] a) (𝓝[t] g a)
hf : HasFDerivWithinAt f f' t (g a)
hf' : Topology.IsEmbedding ⇑f'
hh : HasFDerivWithinAt h (f' ∘SL g') s a
hcomp : f ∘ g =ᶠ[𝓝[s] a] h
ha : a ∈ s
⊢ Prod.map (f ∘ g) (f ∘ g) =ᶠ[𝓝[s] a ×ˢ pure a] Prod.map h h
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case inr
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
h : range ((c.extendMiddle i).emb j) = {0}
hij : j ≠ i
⊢ False

Tactic:
· have : (c.extendMiddle i).emb j 0 ∈ range ((c.extendMiddle i).emb j) :=
      mem_range_self 0
    rw [h] at this
    simp only [extendMiddle, hij, ↓reduceDIte, comp_apply, mem_singleton_iff] at this
    exact Fin.succ_ne_zero _ this

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

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞
Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x ↦ iteratedFDerivWithin 𝕜 m f s x) s
Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x ↦ iteratedFDerivWithin 𝕜 m f s x) s
x : E
hx : x ∈ s
m : ℕ
hm : ↑m ≤ n
⊢ ∃ u ∈ 𝓝[s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u

Tactic:
refine ⟨s, self_mem_nhdsWithin, ftaylorSeriesWithin 𝕜 f s, ?_⟩

Goal state after:
𝕜 : 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 : ℕ∞
Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x ↦ iteratedFDerivWithin 𝕜 m f s x) s
Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x ↦ iteratedFDerivWithin 𝕜 m f s x) s
x : E
hx : x ∈ s
m : ℕ
hm : ↑m ≤ n
⊢ HasFTaylorSeriesUpToOn (↑m) f (ftaylorSeriesWithin 𝕜 f s) s
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

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
n✝ : ℕ∞ω
n : ℕ∞
⊢ ContDiffOn 𝕜 (↑n) f univ ↔ ContDiff 𝕜 (↑n) f

Tactic:
constructor
    · intro H
      use ftaylorSeriesWithin 𝕜 f univ
      rw [← hasFTaylorSeriesUpToOn_univ_iff]
      exact H.ftaylorSeriesWithin uniqueDiffOn_univ
    · rintro ⟨p, hp⟩ x _ m hm
      exact ⟨univ, Filter.univ_sets _, p,
        (hp.hasFTaylorSeriesUpToOn univ).of_le (mod_cast hm)⟩

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

Goal state before:
pp: case inl
𝕜 : 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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
⊢ ∃ m y, (if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ y.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ y)).pred ⋯) = x

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
x : Fin n
i : Fin c.length
j : Fin (c.partSize i)
hij : c.emb i j = x.succ
hi : i ≠ c.index 0
⊢ ∃ m y, (if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ y.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ y)).pred ⋯) = x

Tactic:
· refine ⟨c.index 0, ?_⟩
      have j_ne : j ≠ 0 := by
        rintro rfl
        simp only [c.emb_zero] at hij
        exact (Fin.succ_ne_zero _).symm hij
      have je_ne' : (j : ℕ) ≠ 0 := by simpa
      simp only [↓reduceDIte]
      have A : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0) :=
        Nat.sub_add_cancel (c.partSize_pos _)
      have B : update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) =
        c.partSize (c.index 0) - 1 := by simp
      refine ⟨Fin.cast B.symm (pred (Fin.cast A.symm j) ?_), ?_⟩
      · simpa using j_ne
      · have : x = pred (succ x) (succ_ne_zero x) := rfl
        rw [this]
        simp only [pred_inj, ← hij]
        congr 1
        rw [← val_eq_val]
        simp only [val_cast, val_succ, val_pred]
        omega

Goal state after:
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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
x : Fin n
i : Fin c.length
j : Fin (c.partSize i)
hij : c.emb i j = x.succ
hi : i ≠ c.index 0
⊢ ∃ m y, (if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ y.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ y)).pred ⋯) = x
Module: Mathlib.Analysis.Complex.RealDeriv

Goal state before:
pp: e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasDerivAt e e' ↑z
A : HasFDerivAt ofReal ofRealCLM z
⊢ HasDerivAt (fun x ↦ (e ↑x).re) e'.re z

Tactic:
have B :
    HasFDerivAt e ((ContinuousLinearMap.smulRight 1 e' : ℂ →L[ℂ] ℂ).restrictScalars ℝ)
      (ofRealCLM z) :=
    h.hasFDerivAt.restrictScalars ℝ

Goal state after:
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasDerivAt e e' ↑z
A : HasFDerivAt ofReal ofRealCLM z
B : HasFDerivAt e (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (ofRealCLM z)
⊢ HasDerivAt (fun x ↦ (e ↑x).re) e'.re z
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝔸 : Type u_2
inst✝² : Ring 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
⊢ exp 0 = 1

Tactic:
rw [exp]

Goal state after:
𝔸 : Type u_2
inst✝² : Ring 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
⊢ (if h : Nonempty (Algebra ℚ 𝔸) then (expSeries ℚ 𝔸).sum 0 else 1) = 1
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
f g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑n) f s x
hg : ContDiffWithinAt 𝕜 (↑n) g s x
⊢ iteratedDerivWithin n (f + -g) s x = iteratedDerivWithin n f s x + -iteratedDerivWithin n g s x

Tactic:
Pi.neg_def,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
f g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑n) f s x
hg : ContDiffWithinAt 𝕜 (↑n) g s x
⊢ iteratedDerivWithin n (f + fun i ↦ -g i) s x = iteratedDerivWithin n f s x + -iteratedDerivWithin n g s x
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
i : ℕ
f g : E → F
hf : ContDiffAt 𝕜 (↑i) f x
hg : ContDiffAt 𝕜 (↑i) g x
⊢ iteratedFDeriv 𝕜 i (f + g) x = iteratedFDeriv 𝕜 i f x + iteratedFDeriv 𝕜 i g x

Tactic:
simp_rw [← iteratedFDerivWithin_univ]
  exact iteratedFDerivWithin_add_apply hf hg uniqueDiffOn_univ (Set.mem_univ _)

Goal state after:
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: case neg.inl
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
hab : a ≠ b
hab' : a < b
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)

pp: case neg.inr
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
hab : a ≠ b
hba' : b < a
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)

Tactic:
· simp only [hab', uIoo_of_lt, nhdsWithin_Ioo_eq_nhdsGT, nhdsWithin_Ioo_eq_nhdsLT,
      uIcc_of_lt] at ha hb hf ⊢
    exact continuousOn_Icc_extendFrom_Ioo hf ha hb

Goal state after:
case neg.inr
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
hab : a ≠ b
hba' : b < a
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
x : 𝕜
R : Type u_3
inst✝² : DistribSMul R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
n : ℕ
f : 𝕜 → F
h : ContDiffAt 𝕜 (↑n) f x
c : R
⊢ iteratedDeriv n (c • f) x = c • iteratedDeriv n f x

Tactic:
by
  simpa only [iteratedDerivWithin_univ] using
    iteratedDerivWithin_const_smul (Set.mem_univ x) uniqueDiffOn_univ
      c (contDiffWithinAt_univ.mpr h)

Goal state after:
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
this :
  ContinuousOn (f ∘ ⇑OrderDual.ofDual) (⇑OrderDual.ofDual ⁻¹' Ioo a b) →
    Tendsto (f ∘ ⇑OrderDual.ofDual) (𝓝[⇑OrderDual.ofDual ⁻¹' Iio b] OrderDual.toDual b) (𝓝 lb) →
      ContinuousOn (extendFrom (⇑OrderDual.ofDual ⁻¹' Ioo a b) (f ∘ ⇑OrderDual.ofDual)) (⇑OrderDual.ofDual ⁻¹' Ioc a b)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b)

Tactic:
exact this hf hb

Goal state after:
Module: Mathlib.Analysis.Calculus.LocalExtr.Rolle

Goal state before:
pp: case neg
f : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[>] a) (𝓝 l)
hfb : Tendsto f (𝓝[<] b) (𝓝 l)
h : ∃ x ∈ Ioo a b, ¬DifferentiableAt ℝ f x
⊢ ∃ c ∈ Ioo a b, deriv f c = 0

Tactic:
obtain ⟨c, hc, hcdiff⟩ : ∃ x ∈ Ioo a b, ¬DifferentiableAt ℝ f x := h
    exact ⟨c, hc, deriv_zero_of_not_differentiableAt hcdiff⟩

Goal state after: