mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM

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
x : E
s : Set E
ι : Type u_5
c : E → F [⋀^ι]→L[𝕜] G
inst✝ : Finite ι
hxs : UniqueDiffWithinAt 𝕜 s x
hc : DifferentiableWithinAt 𝕜 c s x
u : ι → F
m : E
⊢ (fderivWithin 𝕜 (fun y ↦ (c y) u) s x) m = ((fderivWithin 𝕜 c s x) m) u

Tactic:
have := Fintype.ofFinite ι
  simp [fderivWithin_continuousAlternatingMap_apply_const hxs hc]

Goal state after:
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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
this : ContinuousOn (fun x ↦ (continuousMultilinearCurryFin0 𝕜 E F).symm (f x)) s
⊢ ContinuousOn f s

Tactic:
rwa [← (continuousMultilinearCurryFin0 𝕜 E F).symm.comp_continuousOn_iff]

Goal state after:
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 f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝[s] x] f
⊢ ftaylorSeriesWithin 𝕜 f₁ s =ᶠ[𝓝[s] x] ftaylorSeriesWithin 𝕜 f s

Tactic:
filter_upwards [eventually_eventually_nhdsWithin.2 h, self_mem_nhdsWithin] with x₁ h₁x₁ h₂x₁

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 f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝[s] x] f
x₁ : E
h₁x₁ : ∀ᶠ (x : E) in 𝓝[s] x₁, f₁ x = f x
h₂x₁ : x₁ ∈ s
⊢ ftaylorSeriesWithin 𝕜 f₁ s x₁ = ftaylorSeriesWithin 𝕜 f s x₁
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
⊢ ‖iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x‖ = ‖iteratedFDeriv 𝕜 (n + 1) f x‖

Tactic:
iteratedFDeriv_succ_eq_comp_right,

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
f : E → F
x : E
n : ℕ
⊢ ‖iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x‖ =
    ‖(⇑(continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm ∘ iteratedFDeriv 𝕜 n fun y ↦ fderiv 𝕜 f y) x‖
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 x ↦ c + f x) s x = derivWithin f s x

Tactic:
by
  simp only [derivWithin, fderivWithin_const_add]

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
c : F
⊢ (derivWithin fun x ↦ c + f x) = derivWithin f

Tactic:
by
  ext
  apply derivWithin_const_add

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 : 𝕜
⊢ DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun x ↦ f (-x)) (-a)

Tactic:
by
  simp_rw [← differentiableAt_comp_neg, neg_neg]

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

Goal state before:
pp: case inl.refine_1
𝕜 : 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
h : HasFiniteFPowerSeriesOnBall f p x 0 r
y : E
hy : y ∈ Metric.eball x r
⊢ fderiv 𝕜 f y = 0

Tactic:
Filter.EventuallyEq.fderiv_eq (f := fun _ ↦ 0)

Goal state after:
case inl.refine_1
𝕜 : 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
h : HasFiniteFPowerSeriesOnBall f p x 0 r
y : E
hy : y ∈ Metric.eball x r
⊢ fderiv 𝕜 (fun x ↦ 0) y = 0

case inl.refine_1
𝕜 : 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
h : HasFiniteFPowerSeriesOnBall f p x 0 r
y : E
hy : y ∈ Metric.eball x r
⊢ f =ᶠ[𝓝 y] fun x ↦ 0
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hx : AccPt x (𝓟 s)
hd : HasDerivWithinAt g g' s x
hg : AntitoneOn g s
⊢ g' ≤ 0

Tactic:
have : MonotoneOn (-g) s := fun x hx y hy hxy ↦ by simpa using hg hx hy hxy
  simpa using hd.neg.nonneg_of_monotoneOn hx this

Goal state after:
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
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
𝕜' : Type u_5
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
c' : E →L[𝕜] 𝕜'
hc : HasFDerivWithinAt c c' s x
hf : HasFDerivWithinAt f f' s x
⊢ HasFDerivWithinAt (c • f) (c x • f' + c'.smulRight (f x)) s x

Tactic:
exact (isBoundedBilinearMap_smul.hasFDerivAt (𝕜 := 𝕜) (c x, f x)).comp_hasFDerivWithinAt x <|
    hc.prodMk hf

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivWithinAt c c' univ x
hd : HasDerivWithinAt d d' univ x
hx : d x ≠ 0
⊢ HasDerivWithinAt (fun y ↦ c y / d y) ((c' * d x - c x * d') / d x ^ 2) univ x

Tactic:
exact hc.div hd hx

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
R : Type u_5
inst✝² : NormedRing R
inst✝¹ : HasSummableGeomSeries R
inst✝ : NormedAlgebra 𝕜 R
x : Rˣ
⊢ HasFDerivAt Ring.inverse (-((mulLeftRight 𝕜 R) ↑x⁻¹) ↑x⁻¹) ↑x

Tactic:
have : (fun t : R => Ring.inverse (↑x + t) - ↑x⁻¹ + ↑x⁻¹ * t * ↑x⁻¹) =o[𝓝 0] id :=
    (inverse_add_norm_diff_second_order x).trans_isLittleO (isLittleO_norm_pow_id one_lt_two)

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
R : Type u_5
inst✝² : NormedRing R
inst✝¹ : HasSummableGeomSeries R
inst✝ : NormedAlgebra 𝕜 R
x : Rˣ
this : (fun t ↦ (↑x + t)⁻¹ʳ - ↑x⁻¹ + ↑x⁻¹ * t * ↑x⁻¹) =o[𝓝 0] id
⊢ HasFDerivAt Ring.inverse (-((mulLeftRight 𝕜 R) ↑x⁻¹) ↑x⁻¹) ↑x
Module: Mathlib.Analysis.Calculus.Deriv.Comp

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasDerivAt h₂ h₂' (h x)
hh : HasDerivAt h h' x
hy : y = h x
⊢ HasDerivAt (h₂ ∘ h) (h₂' * h') x

Tactic:
exact hh₂.comp x hh

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasStrictDerivAt h₂ h₂' (h x)
hh : HasStrictDerivAt h h' x
hy : y = h x
⊢ HasStrictDerivAt (h₂ ∘ h) (h₂' * h') x

Tactic:
exact hh₂.comp x hh

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

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m✝ : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m✝
m : ℕ
hm : 0 < ↑m
⊢ HasStrictDerivAt (fun x ↦ x ^ m) (↑m * x ^ (↑m - 1)) x

Tactic:
convert hasStrictDerivAt_pow m x

Goal state after:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m✝ : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m✝
m : ℕ
hm : 0 < ↑m
⊢ x ^ (↑m - 1) = x ^ (m - 1)
Module: Mathlib.Analysis.Calculus.Deriv.ZPow

Goal state before:
pp: case neg
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
H : ¬(x ≠ 0 ∨ 0 ≤ m)
⊢ deriv (fun x ↦ x ^ m) x = ↑m * x ^ (m - 1)

Tactic:
rw [deriv_zero_of_not_differentiableAt (mt differentiableAt_zpow.1 H)]

Goal state after:
case neg
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
H : ¬(x ≠ 0 ∨ 0 ≤ m)
⊢ 0 = ↑m * x ^ (m - 1)
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
L : Filter (E × E)
⊢ HasFDerivAtFilter (⇑f) f.contLinear L

Tactic:
by
  refine .of_isLittleOTVS <| .congr_left (.zero _ _) ?_
  simp [(vsub_eq_sub _ _).symm.trans (f.contLinear_map_vsub _ _).symm]

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

Goal state before:
pp: case cons.hdf
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (∀ i ∈ s, f i x ≠ 0) →
    (∀ i ∈ s, DifferentiableAt 𝕜 (f i) x) → logDeriv (fun x ↦ ∏ i ∈ s, f i x) x = ∑ i ∈ s, logDeriv (f i) x
hf : f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0
hd : DifferentiableAt 𝕜 (f a) x ∧ ∀ x_1 ∈ s, DifferentiableAt 𝕜 (f x_1) x
⊢ DifferentiableAt 𝕜 (f a) x

pp: case cons.hdg
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (∀ i ∈ s, f i x ≠ 0) →
    (∀ i ∈ s, DifferentiableAt 𝕜 (f i) x) → logDeriv (fun x ↦ ∏ i ∈ s, f i x) x = ∑ i ∈ s, logDeriv (f i) x
hf : f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0
hd : DifferentiableAt 𝕜 (f a) x ∧ ∀ x_1 ∈ s, DifferentiableAt 𝕜 (f x_1) x
⊢ DifferentiableAt 𝕜 (fun x ↦ ∏ i ∈ s, f i x) x

Tactic:
· exact hd.1

Goal state after:
case cons.hdg
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (∀ i ∈ s, f i x ≠ 0) →
    (∀ i ∈ s, DifferentiableAt 𝕜 (f i) x) → logDeriv (fun x ↦ ∏ i ∈ s, f i x) x = ∑ i ∈ s, logDeriv (f i) x
hf : f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0
hd : DifferentiableAt 𝕜 (f a) x ∧ ∀ x_1 ∈ s, DifferentiableAt 𝕜 (f x_1) x
⊢ DifferentiableAt 𝕜 (fun x ↦ ∏ i ∈ s, f i x) x
Module: Mathlib.Analysis.Calculus.MeanValue

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt f 0 (Ici x) x
⊢ ∀ x ∈ Icc a b, f x = f a

Tactic:
have : ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ 0 * (x - a) := fun x hx =>
    norm_image_sub_le_of_norm_deriv_right_le_segment hcont hderiv (fun _ _ => norm_zero.le) x hx

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt f 0 (Ici x) x
this : ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ 0 * (x - a)
⊢ ∀ x ∈ Icc a b, f x = f a
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' ⊢
    convert! hf' using 4 with c hc x
    simp

Goal state after:
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
y : F
x : E
hg : ContDiffWithinAt 𝕜 n g t y
hf : ContDiffWithinAt 𝕜 n f s x
st : MapsTo f s t
hy : f x = y
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x

Tactic:
subst hy; exact hg.comp x hf st

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage

Goal state before:
pp: case left
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s s' : Set X
hss' : e.source ∩ interior s = e.source ∩ interior s'
⊢ (e.restr s).source = (e.restr s').source

pp: case right
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s s' : Set X
hss' : e.source ∩ interior s = e.source ∩ interior s'
⊢ EqOn (↑(e.restr s)) (↑(e.restr s')) (e.restr s).source

Tactic:
· simpa [e.restr_source]

Goal state after:
case right
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s s' : Set X
hss' : e.source ∩ interior s = e.source ∩ interior s'
⊢ EqOn (↑(e.restr s)) (↑(e.restr s')) (e.restr s).source
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case refine_2
𝕜 : 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 : ℕ∞ω
hn : n ≠ ∞
⊢ (∃ u ∈ 𝓝[insert x s] x,
      u ⊆ insert x s ∧
        (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) s x) ∧ ContDiffWithinAt 𝕜 n f' s x) →
    ContDiffWithinAt 𝕜 (n + 1) f (insert ?m.343 s) x

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 : ℕ∞ω
hn : n ≠ ∞
⊢ E

Tactic:
contDiffWithinAt_succ_iff_hasFDerivWithinAt hn,

Goal state after:
case refine_2
𝕜 : 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 : ℕ∞ω
hn : n ≠ ∞
⊢ (∃ u ∈ 𝓝[insert x s] x,
      u ⊆ insert x s ∧
        (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) s x) ∧ ContDiffWithinAt 𝕜 n f' s x) →
    ∃ u ∈ 𝓝[insert x (insert ?m.343 s)] x,
      (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 n f' u x

𝕜 : 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 : ℕ∞ω
hn : n ≠ ∞
⊢ E
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
c : F
x : 𝕜
⊢ iteratedDeriv n (fun x ↦ c) x = if n = 0 then c else 0

Tactic:
induction n generalizing c with

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
c : F
s : Set 𝕜
x : 𝕜
⊢ iteratedDerivWithin n (fun x ↦ c) s x = if n = 0 then c else 0

Tactic:
induction n generalizing c with

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

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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ c : OrderedFinpartition n
i : Fin c.length
hi : i ∈ univ
j : Fin c.length
hj : j ∈ univ
hij h : i ≠ j
this : ∀ (a' : Fin (c.partSize i)) (b' : Fin (c.partSize j + 1)), (c.emb i a').succ ≠ cases 0 (succ ∘ c.emb j) b'
⊢ ∀ (a : Fin (update c.partSize j (c.partSize j + 1) i)) (a_1 : Fin (update c.partSize j (c.partSize j + 1) j)),
    ¬(c.emb i (Fin.cast ⋯ a)).succ = cases 0 (succ ∘ c.emb j) (Fin.cast ⋯ a_1)

Tactic:
intro a b

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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ c : OrderedFinpartition n
i : Fin c.length
hi : i ∈ univ
j : Fin c.length
hj : j ∈ univ
hij h : i ≠ j
this : ∀ (a' : Fin (c.partSize i)) (b' : Fin (c.partSize j + 1)), (c.emb i a').succ ≠ cases 0 (succ ∘ c.emb j) b'
a : Fin (update c.partSize j (c.partSize j + 1) i)
b : Fin (update c.partSize j (c.partSize j + 1) j)
⊢ ¬(c.emb i (Fin.cast ⋯ a)).succ = cases 0 (succ ∘ c.emb j) (Fin.cast ⋯ b)
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
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✝ c : OrderedFinpartition n
k i : Fin c.length
hi : i ∈ univ
j : Fin c.length
hj✝ : j ∈ univ
hij : i ≠ j
h : i ≠ k
hj : j ≠ k
⊢ ∀ (a : Fin (update c.partSize k (c.partSize k + 1) i)) (a_1 : Fin (update c.partSize k (c.partSize k + 1) j)),
    ¬c.emb i (Fin.cast ⋯ a) = c.emb j (Fin.cast ⋯ a_1)

Tactic:
intro a b

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✝ c : OrderedFinpartition n
k i : Fin c.length
hi : i ∈ univ
j : Fin c.length
hj✝ : j ∈ univ
hij : i ≠ j
h : i ≠ k
hj : j ≠ k
a : Fin (update c.partSize k (c.partSize k + 1) i)
b : Fin (update c.partSize k (c.partSize k + 1) j)
⊢ ¬c.emb i (Fin.cast ⋯ a) = c.emb j (Fin.cast ⋯ b)
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

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
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}
i : Fin (c.length - 1)
x✝¹ : i ∈ univ
j : Fin (c.length - 1)
x✝ : j ∈ univ
hij : i ≠ j
⊢ ∀ (a : Fin (c.partSize (Fin.cast ⋯ i.succ))) (a_1 : Fin (c.partSize (Fin.cast ⋯ j.succ))),
    ¬c.emb (Fin.cast ⋯ i.succ) a = c.emb (Fin.cast ⋯ j.succ) a_1

Tactic:
intro a b

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
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}
i : Fin (c.length - 1)
x✝¹ : i ∈ univ
j : Fin (c.length - 1)
x✝ : j ∈ univ
hij : i ≠ j
a : Fin (c.partSize (Fin.cast ⋯ i.succ))
b : Fin (c.partSize (Fin.cast ⋯ j.succ))
⊢ ¬c.emb (Fin.cast ⋯ i.succ) a = c.emb (Fin.cast ⋯ j.succ) b
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 : ℕ∞ω
h : ∀ (m : ℕ), AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 ω f s x

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

Goal state after:
case refine_1
𝕜 : 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 : ℕ∞ω
h : ∀ (m : ℕ), AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s
x : E
hx : x ∈ s
⊢ HasFTaylorSeriesUpToOn ω f (ftaylorSeriesWithin 𝕜 f s) (insert x s)

case refine_2
𝕜 : 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 : ℕ∞ω
h : ∀ (m : ℕ), AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s
x : E
hx : x ∈ s
⊢ ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ ftaylorSeriesWithin 𝕜 f s x i) (insert x s)
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case pos.refine_2
𝕜 : 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}
i : Fin c.length
j : Fin (update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)
h : i = c.index 0
⊢ c.emb i (Fin.cast ⋯ j.succ) ≠ 0

Tactic:
have : 0 ≤ c.emb i 0 := Fin.zero_le _

Goal state after:
case pos.refine_2
𝕜 : 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}
i : Fin c.length
j : Fin (update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)
h : i = c.index 0
this : 0 ≤ c.emb i 0
⊢ c.emb i (Fin.cast ⋯ j.succ) ≠ 0
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case inr
𝕜 : 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 : ℕ∞ω
hf : DifferentiableOn 𝕜 f s
h' : n = ω → AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 n (fun y ↦ fderivWithin 𝕜 f s y) s
hn : n ≠ ∞
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 (n + 1) f s x

Tactic:
contDiffWithinAt_succ_iff_hasFDerivWithinAt hn,

Goal state after:
case inr
𝕜 : 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 : ℕ∞ω
hf : DifferentiableOn 𝕜 f s
h' : n = ω → AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 n (fun y ↦ fderivWithin 𝕜 f s y) s
hn : n ≠ ∞
x : E
hx : x ∈ s
⊢ ∃ u ∈ 𝓝[insert x s] x,
    (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 n f' u x