mathlib-initiative/mathlib-tactics huggingface dataset:
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
s : Set E
f : E → F
x : E
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hn : n ≠ 0
hx : x ∈ s
A : ∀ y ∈ s, f y = (continuousMultilinearCurryFin0 𝕜 E F) (p y 0)
this : ↑↑0 < n
⊢ HasFDerivWithinAt (fun x ↦ p x 0)
    (↑↑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘SL (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) s x

Tactic:
convert! h.fderivWithin _ this x hx

Goal state after:
case e'_12
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hn : n ≠ 0
hx : x ∈ s
A : ∀ y ∈ s, f y = (continuousMultilinearCurryFin0 𝕜 E F) (p y 0)
this : ↑↑0 < n
e_8✝ : ContinuousMultilinearMap.normedAddCommGroup'.toAddCommGroup = ContinuousMultilinearMap.instAddCommGroup
e_9✝ : ContinuousMultilinearMap.normedSpace'.toModule ≍ ContinuousMultilinearMap.instModule
e_10✝ : PseudoMetricSpace.toUniformSpace.toTopologicalSpace = ContinuousMultilinearMap.instTopologicalSpace
⊢ ↑↑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘SL (continuousMultilinearCurryFin1 𝕜 E F) (p x 1) =
    (p x (Nat.succ 0)).curryLeft
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
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ HasFTaylorSeriesUpToOn (↑n + 1) f p s →
    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

pp: case mpr
𝕜 : 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 : ℕ
⊢ 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 →
    HasFTaylorSeriesUpToOn (↑n + 1) f p s

Tactic:
· exact fun h ↦ ⟨h.of_le (mod_cast Nat.le_succ n),
      h.fderivWithin _ (mod_cast lt_add_one n), h.cont (n + 1) le_rfl⟩

Goal state after:
case mpr
𝕜 : 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 : ℕ
⊢ 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 →
    HasFTaylorSeriesUpToOn (↑n + 1) f p s
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
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
⊢ HasDerivAt (fun x ↦ (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x

Tactic:
by
  by_cases hxu : x ∈ tsupport u
  · by_cases hxv : x ∈ tsupport v
    · simpa using (B.hasFDerivAt_of_bilinear (hu hxv).hasFDerivAt (hv hxu).hasFDerivAt).hasDerivAt
    · have hx : x ∉ tsupport fun x ↦ B (u x) (v x) :=
        mt (closure_mono (fun x ↦ mt fun h ↦ by simp [h]) ·) hxv
      convert! HasDerivAt.of_notMem_tsupport hx
      simp [(hv hxu).unique <| .of_notMem_tsupport hxv, image_eq_zero_of_notMem_tsupport hxv]
  · have hx : x ∉ tsupport fun x ↦ B (u x) (v x) :=
      mt (closure_mono (fun x ↦ mt fun h ↦ by simp [h]) ·) hxu
    convert! HasDerivAt.of_notMem_tsupport hx
    by_cases hxv : x ∈ tsupport v
    · simp [image_eq_zero_of_notMem_tsupport hxu, (hu hxv).unique <| .of_notMem_tsupport hxu]
    · simp [image_eq_zero_of_notMem_tsupport hxu, image_eq_zero_of_notMem_tsupport hxv]

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
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
f : F
⊢ derivWithin (fun y ↦ c y • f) s x = derivWithin c s x • f

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

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

Goal state before:
pp: 𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
n a : ℕ
⊢ a ∈ Finset.range n → f x ^ (a + (n.pred - a)) = f x ^ (n - 1)

Tactic:
ha

Goal state after:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
n a : ℕ
ha : a ∈ Finset.range n
⊢ f x ^ (a + (n.pred - a)) = f x ^ (n - 1)
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 : 𝕜
⊢ DifferentiableAt 𝕜 (fun x ↦ f (-x)) a ↔ DifferentiableAt 𝕜 f (-a)

Tactic:
by
  refine ⟨fun H ↦ ?_, fun H ↦ H.comp a differentiable_neg.differentiableAt⟩
  convert! ((neg_neg a).symm ▸ H).comp (-a) differentiable_neg.differentiableAt
  ext
  simp only [Function.comp_apply, neg_neg]

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 g : 𝕜 → F
f' g' : F
L : Filter (𝕜 × 𝕜)
hf : HasDerivAtFilter f f' L
hg : HasDerivAtFilter g g' L
⊢ HasDerivAtFilter (f - g) (f' - g') L

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

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

Goal state before:
pp: case inr.refine_3
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
i : ι
⊢ f (Function.update x i (y i)) =
    f fun i_1 ↦ (if (Fintype.equivFinOfCardEq ⋯) i_1 = (Fintype.equivFinOfCardEq ⋯) i then y else x) i_1

Tactic:
(Equiv.injective _).eq_iff,

Goal state after:
case inr.refine_3
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
i : ι
⊢ f (Function.update x i (y i)) = f fun i_1 ↦ (if i_1 = i then y else x) i_1
Module: Mathlib.Analysis.Analytic.Uniqueness

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
y : E
c : ℝ
c_pos : c > 0
t : Set E
t_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
δ : ℝ
δ_pos : δ > 0
δε : Metric.ball 0 δ ⊆ t
n : ℕ
p : E [×n + 1]→L[𝕜] F
ht : ∀ y ∈ t, ‖p fun x ↦ y‖ ≤ c * ‖‖y‖ ^ (n + 1 + 1)‖
hy : 0 < ‖y‖
ε : ℝ
ε_pos : 0 < ε
h₀ : 0 < c * ‖y‖ ^ (n.succ + 1)
k : 𝕜
k_pos : 0 < ‖k‖
k_norm : ‖k‖ < min (δ * ‖y‖⁻¹) (ε * (c * ‖y‖ ^ (n.succ + 1))⁻¹)
h₁ : ‖k • y‖ < δ
h₂ : ‖p fun x ↦ k • y‖ ≤ ‖k‖ ^ n.succ * (‖k‖ * (c * ‖y‖ ^ (n.succ + 1)))
h₃ : ‖k‖ * (c * ‖y‖ ^ (n.succ + 1)) < ε
⊢ ‖1 ^ n.succ‖ * (‖k‖ * (c * ‖y‖ ^ (n.succ + 1))) ≤ 0 + ε

Tactic:
simpa using! h₃.le

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nontrivial E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
x : E
hx : x ∈ univ
r : 𝕜
hr₀ : 0 < ‖r‖
hr : ‖r‖ < 1
c : E
hc : c ≠ 0
A : Tendsto (fun n ↦ x + r ^ n • c) atTop (𝓝 (x + 0 • c))
⊢ AccPt x (𝓟 univ)

Tactic:
have B : Tendsto (fun (n : ℕ) ↦ x + r ^ n • c) atTop (𝓝[univ \ {x}] x) := by
    simp only [zero_smul, add_zero] at A
    simp [tendsto_nhdsWithin_iff, A, hc, norm_pos_iff.mp hr₀]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nontrivial E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
x : E
hx : x ∈ univ
r : 𝕜
hr₀ : 0 < ‖r‖
hr : ‖r‖ < 1
c : E
hc : c ≠ 0
A : Tendsto (fun n ↦ x + r ^ n • c) atTop (𝓝 (x + 0 • c))
B : Tendsto (fun n ↦ x + r ^ n • c) atTop (𝓝[univ \ {x}] x)
⊢ AccPt x (𝓟 univ)
Module: Mathlib.Analysis.Calculus.DSlope

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : 𝕜
f : 𝕜 → E
h : b ≠ a
⊢ dslope (fun x ↦ (x - a) • f x) a b = f b

Tactic:
by
  rw [dslope_of_ne _ h, slope_sub_smul _ h.symm]

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

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
⊢ HasStrictDerivAt Inv.inv (-(x ^ 2)⁻¹) x

Tactic:
suffices
    (fun p : 𝕜 × 𝕜 => (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) =o[𝓝 (x, x)] fun p =>
      (p.1 - p.2) * 1 by
    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
  refine (isBigO_refl (fun p : 𝕜 × 𝕜 => p.1 - p.2) _).mul_isLittleO ((isLittleO_one_iff 𝕜).2 ?_)
  rw [← sub_self (x * x)⁻¹]
  exact tendsto_const_nhds.sub ((continuous_mul.tendsto (x, x)).inv₀ <| mul_ne_zero hx hx)

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

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
f' : 𝕜
hf : HasDerivWithinAt f f' s x
hx : f x = x
hs : MapsTo f s s
n : ℕ
⊢ HasDerivWithinAt f^[n] (f' ^ n) s x

Tactic:
by
  have := HasFDerivWithinAt.iterate hf hx hs n
  rwa [ContinuousLinearMap.toSpanSingleton_pow] at this

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
x : 𝕜
hx : x ∈ U
hx2 : (U \ {x | ¬f x = 0})ᶜ ∉ 𝓝[≠] x
nh : ∀ᶠ (x : 𝕜) in 𝓝[≠] x, ¬(fun z ↦ f z = 0) x
a : 𝕜
⊢ ¬f a = 0 → a ∈ (U \ {x | ¬f x = 0})ᶜ

Tactic:
ha

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
x : 𝕜
hx : x ∈ U
hx2 : (U \ {x | ¬f x = 0})ᶜ ∉ 𝓝[≠] x
nh : ∀ᶠ (x : 𝕜) in 𝓝[≠] x, ¬(fun z ↦ f z = 0) x
a : 𝕜
ha : ¬f a = 0
⊢ a ∈ (U \ {x | ¬f x = 0})ᶜ
Module: Mathlib.Analysis.Calculus.FDeriv.Affine

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
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (⇑f) s x = f.contLinear

Tactic:
DifferentiableAt.fderivWithin f.differentiableAt hxs

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 : E →ᴬ[𝕜] F
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderiv 𝕜 (⇑f) x = f.contLinear
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
f : E → F
x : E
n : ℕ∞ω
g : F →L[𝕜] G
hf : ContDiffWithinAt 𝕜 ω f s x
⊢ ContDiffWithinAt 𝕜 ω (⇑g ∘ f) s x

Tactic:
obtain ⟨u, hu, p, hp, h'p⟩ := hf
    refine ⟨u, hu, _, hp.continuousLinearMap_comp g, fun i ↦ ?_⟩
    change AnalyticOn 𝕜
      (fun x ↦ (ContinuousLinearMap.compContinuousMultilinearMapL 𝕜
      (fun _ : Fin i ↦ E) F G g) (p x i)) u
    apply AnalyticOnNhd.comp_analyticOn _ (h'p i) (Set.mapsTo_univ _ _)
    exact ContinuousLinearMap.analyticOnNhd _ _

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 f₁ : E → F
x : E
n✝ : ℕ∞ω
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
n : ℕ∞
h : ContDiffWithinAt 𝕜 (↑n) f s x
m : ℕ
hm : ↑m ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn (↑m) f p u
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) f₁ p u

Tactic:
exact ⟨{ x ∈ u | f₁ x = f x }, Filter.inter_mem hu (mem_nhdsWithin_insert.2 ⟨hx, h₁⟩), p,
      (H.mono (sep_subset _ _)).congr fun _ ↦ And.right⟩

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 f₁ : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ ContDiffWithinAt 𝕜 n f₁ s x

Tactic:
match n with
  | ω =>
    obtain ⟨u, hu, p, H, H'⟩ := h
    exact ⟨{x ∈ u | f₁ x = f x}, Filter.inter_mem hu (mem_nhdsWithin_insert.2 ⟨hx, h₁⟩), p,
      (H.mono (sep_subset _ _)).congr fun _ ↦ And.right,
      fun i ↦ (H' i).mono (sep_subset _ _)⟩
  | (n : ℕ∞) =>
    intro m hm
    let ⟨u, hu, p, H⟩ := h m hm
    exact ⟨{ x ∈ u | f₁ x = f x }, Filter.inter_mem hu (mem_nhdsWithin_insert.2 ⟨hx, h₁⟩), p,
      (H.mono (sep_subset _ _)).congr fun _ ↦ And.right⟩

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

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

Tactic:
· exact hcomp.prodMap (hcomp.self_of_nhdsWithin ha)

Goal state after:
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
hg : ContinuousAt g a
hf : HasFDerivAt f f' (g a)
hf' : Topology.IsEmbedding ⇑f'
hh : HasFDerivAt h (f' ∘SL g') a
hcomp : f ∘ g =ᶠ[𝓝 a] h
⊢ Tendsto (Prod.map g g) (𝓝 a ×ˢ pure a) (𝓝 (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
hg : ContinuousAt g a
hf : HasFDerivAt f f' (g a)
hf' : Topology.IsEmbedding ⇑f'
hh : HasFDerivAt h (f' ∘SL g') a
hcomp : f ∘ g =ᶠ[𝓝 a] h
⊢ Prod.map (f ∘ g) (f ∘ g) =ᶠ[𝓝 a ×ˢ pure a] Prod.map h h

Tactic:
· exact hg.tendsto.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
hg : ContinuousAt g a
hf : HasFDerivAt f f' (g a)
hf' : Topology.IsEmbedding ⇑f'
hh : HasFDerivAt h (f' ∘SL g') a
hcomp : f ∘ g =ᶠ[𝓝 a] h
⊢ Prod.map (f ∘ g) (f ∘ g) =ᶠ[𝓝 a ×ˢ pure a] Prod.map h h
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 : ℕ∞
f' : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn (↑n) f f' s
⊢ ContDiffOn 𝕜 (↑n) f s

Tactic:
by
  intro x hx m hm
  use s
  simp only [Set.insert_eq_of_mem hx, self_mem_nhdsWithin, true_and]
  exact ⟨f', hf.of_le (mod_cast hm)⟩

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

Goal state before:
pp: n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
⊢ 1 < c.partSize (c.index 0)

Tactic:
by
  have : c.partSize (c.index 0) = Nat.card (range (c.emb (c.index 0))) := by
    rw [Nat.card_range_of_injective (c.emb_strictMono _).injective]; simp
  rw [this]
  rcases eq_or_ne (c.index 0) 0 with h | h
  · rw [← h] at hc
    have : {0} ⊂ range (c.emb (c.index 0)) := by
      apply ssubset_of_subset_of_ne ?_ hc.symm
      simpa only [singleton_subset_iff, mem_range] using ⟨0, emb_zero c⟩
    simpa using Set.Finite.card_lt_card (finite_range _) this
  · apply one_lt_two.trans_le
    have : {c.emb (c.index 0) 0,
        c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, Nat.sub_one_lt_of_lt (c.partSize_pos _)⟩}
          ⊆ range (c.emb (c.index 0)) := by simp [insert_subset]
    simp only [emb_zero] at this
    convert! Nat.card_mono Subtype.finite this
    simp only [Nat.card_eq_fintype_card, Fintype.card_ofFinset, toFinset_singleton]
    apply (Finset.card_pair ?_).symm
    exact ((Fin.zero_le _).trans_lt (c.parts_strictMono ((pos_iff_ne_zero' (c.index 0)).mpr h))).ne

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
f : E → F
x : E
n : ℕ∞ω
⊢ ContDiffWithinAt 𝕜 n f {x}ᶜ x ↔ ContDiffAt 𝕜 n f x

Tactic:
by
  rw [compl_eq_univ_sdiff, contDiffWithinAt_sdiff_singleton, contDiffWithinAt_univ]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
⊢ ContinuousOn exp (Metric.eball 0 (expSeries 𝕂 𝔸).radius)

Tactic:
have := FormalMultilinearSeries.continuousOn (p := expSeries 𝕂 𝔸)
  simpa only [exp_eq_expSeries_sum 𝕂, expSeries_sum_eq_rat] using this

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: case neg
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
h : ¬(expSeries 𝕂 𝔸).radius = 0
⊢ AnalyticAt 𝕂 exp x

Tactic:
have h := pos_iff_ne_zero.mpr h
    exact (hasFPowerSeriesOnBall_exp_of_radius_pos h).analyticAt_of_mem hx

Goal state after:
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 : ℕ
s : Set 𝕜
f : 𝕜 → F
c : 𝕜
⊢ iteratedDerivWithin n (fun z ↦ f (c + z)) s = fun x ↦ iteratedDerivWithin n f (c +ᵥ s) (c + x)

Tactic:
ext x
  simp [iteratedDerivWithin, ← iteratedFDerivWithin_comp_add_left n c x]

Goal state after:
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 : ℕ
s : Set 𝕜
f : 𝕜 → F
c : 𝕜
⊢ iteratedDerivWithin n (fun z ↦ f (z + c)) s = fun x ↦ iteratedDerivWithin n f (c +ᵥ s) (x + c)

Tactic:
by
  ext x
  simp [iteratedDerivWithin, ← iteratedFDerivWithin_comp_add_right n c x]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Exponential

Goal state before:
pp: case e'_12
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : CharZero 𝕂
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
h : 0 < (expSeries 𝕂 𝔸).radius
e_4✝ : inst✝³.toAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup.toAddCommGroup
e_5✝ : (NormedAlgebra.toNormedSpace 𝔸).toModule ≍ (NormedAlgebra.toNormedSpace 𝔸).toModule
x : 𝔸
⊢ 1 x = ((continuousMultilinearCurryFin1 𝕂 𝔸 𝔸) (expSeries 𝕂 𝔸 1)) x

Tactic:
change x = expSeries 𝕂 𝔸 1 fun _ => x

Goal state after:
case e'_12
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : CharZero 𝕂
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
h : 0 < (expSeries 𝕂 𝔸).radius
e_4✝ : inst✝³.toAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup.toAddCommGroup
e_5✝ : (NormedAlgebra.toNormedSpace 𝔸).toModule ≍ (NormedAlgebra.toNormedSpace 𝔸).toModule
x : 𝔸
⊢ x = (expSeries 𝕂 𝔸 1) fun x_1 ↦ x
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case e_6.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
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
e : E
v : Fin m → E
j : Fin c.length
a : ℕ
⊢ ∀ (him : a < update c.partSize j (c.partSize j + 1) j) (hin : a < c.partSize j + 1),
    (cons e v ∘ (fun i ↦ cases 0 (succ ∘ c.emb j) i) ∘ Fin.cast ⋯) ⟨a, him⟩ = cons e (v ∘ c.emb j) ⟨a, hin⟩

Tactic:
ha

Goal state after:
case e_6.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
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
e : E
v : Fin m → E
j : Fin c.length
a : ℕ
ha : a < update c.partSize j (c.partSize j + 1) j
⊢ ∀ (hin : a < c.partSize j + 1),
    (cons e v ∘ (fun i ↦ cases 0 (succ ∘ c.emb j) i) ∘ Fin.cast ⋯) ⟨a, ha⟩ = cons e (v ∘ c.emb j) ⟨a, hin⟩