mathlib-initiative/mathlib-tactics huggingface dataset:
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
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∈ tsupport u
⊢ HasDerivAt (fun x ↦ (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x

Tactic:
by_cases hxv : x ∈ tsupport v

Goal state after:
case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∈ tsupport u
hxv : x ∈ tsupport v
⊢ HasDerivAt (fun x ↦ (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x

case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∈ tsupport u
hxv : x ∉ tsupport v
⊢ HasDerivAt (fun x ↦ (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x
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
hxu : x ∉ tsupport u
hx : x ∉ tsupport fun x ↦ (B (u x)) (v x)
⊢ (B (u x)) v' + (B u') (v x) = 0

Tactic:
by_cases hxv : x ∈ tsupport v

Goal state after:
case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∉ tsupport u
hx : x ∉ tsupport fun x ↦ (B (u x)) (v x)
hxv : x ∈ tsupport v
⊢ (B (u x)) v' + (B u') (v x) = 0

case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∉ tsupport u
hx : x ∉ tsupport fun x ↦ (B (u x)) (v x)
hxv : x ∉ tsupport v
⊢ (B (u x)) v' + (B u') (v x) = 0
Module: Mathlib.Analysis.Calculus.FDeriv.Pow

Goal state before:
pp: 𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing 𝔸
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
n : ℕ
⊢ HasFDerivWithinAt (f ^ 0) (∑ i ∈ Finset.range 0, f x ^ (Nat.pred 0 - i) •> f' <• f x ^ i) s x

Tactic:
by simpa using! hasFDerivWithinAt_const 1 x s

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

Goal state before:
pp: case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (-f) s x = -derivWithin f s x

pp: case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (-f) s x = -derivWithin f s x

Tactic:
· simp only [derivWithin, fderivWithin_neg hsx, neg_apply]

Goal state after:
case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (-f) s x = -derivWithin f s x
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
𝔸' : Type u_3
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hd : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x
⊢ DifferentiableWithinAt 𝕜 (fun x ↦ ∏ i ∈ u, f i x) s x

Tactic:
classical
  exact (HasDerivWithinAt.fun_finsetProd (fun i hi ↦
    DifferentiableWithinAt.hasDerivWithinAt (hd i hi))).differentiableWithinAt

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

Goal state before:
pp: case inr
𝕜 : 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 ι
⊢ ∀ (b' : ℕ), b' ≠ Fintype.card ι - 1 → ((f.toFormalMultilinearSeries.changeOriginSeries 1 b') fun x_1 ↦ x) = 0

pp: case inr
𝕜 : 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 ι
⊢ ((∑ s, f.toFormalMultilinearSeries.changeOriginSeriesTerm 1 (Fintype.card ι - 1) ↑s ⋯) fun x_1 ↦ x) (Fin.snoc 0 y) =
    ∑ i, f (Function.update x i (y i))

Tactic:
· intro m hm
    rw [Ne, eq_tsub_iff_add_eq_of_le (by exact Fintype.card_pos), add_comm] at hm
    rw [f.changeOriginSeries_support hm, _root_.zero_apply]

Goal state after:
case inr
𝕜 : 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 ι
⊢ ((∑ s, f.toFormalMultilinearSeries.changeOriginSeriesTerm 1 (Fintype.card ι - 1) ↑s ⋯) fun x_1 ↦ x) (Fin.snoc 0 y) =
    ∑ i, f (Function.update x i (y i))
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‖ < δ
⊢ c * ‖k • y‖ ^ (n.succ + 1) = ‖k‖ ^ n.succ * (‖k‖ * (c * ‖y‖ ^ (n.succ + 1)))

Tactic:
simp only [norm_smul, mul_pow]
          ring

Goal state after:
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
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
F' : Type u_3 := UniformSpace.Completion F
e : F →L[𝕜] F' := UniformSpace.Completion.toComplL
this : AnalyticOnNhd 𝕜 (⇑e ∘ f) U
⊢ EqOn f 0 U

Tactic:
have A : EqOn (e ∘ f) 0 U := by
    apply eqOn_zero_of_preconnected_of_eventuallyEq_zero_aux this hU h₀
    filter_upwards [hfz₀] with x hx
    simp only [hx, Function.comp_apply, Pi.zero_apply, map_zero]

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
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
F' : Type u_3 := UniformSpace.Completion F
e : F →L[𝕜] F' := UniformSpace.Completion.toComplL
this : AnalyticOnNhd 𝕜 (⇑e ∘ f) U
A : EqOn (⇑e ∘ f) 0 U
⊢ EqOn f 0 U
Module: Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalSpace Z
proj : Z → B
h : IsHomeomorphicTrivialFiberBundle F proj
⊢ Continuous[inst✝, inst✝²] proj

Tactic:
by
  obtain ⟨e, rfl⟩ := h.proj_eq; exact continuous_fst.comp e.continuous

Goal state after:
Module: Mathlib.Analysis.Complex.ReImTopology

Goal state before:
pp: a : ℝ
⊢ frontier {z | a ≤ z.im} = {z | z.im = a}

Tactic:
simpa only [frontier_Ici] using! frontier_preimage_im (Ici a)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
f : 𝕜 → E
s : Set 𝕜
x : 𝕜
⊢ derivWithin (fun x ↦ f (c * x)) s x = c • derivWithin f (c • s) (c * x)

Tactic:
by
  simp only [← smul_eq_mul]
  rw [← derivWithin_const_smul_field, derivWithin, derivWithin,
    fderivWithin_comp_smul_eq_fderivWithin_smul, Pi.smul_def]

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

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

Tactic:
exact (hasDerivAt_zpow m x H).deriv

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

Goal state before:
pp: case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
s : Set E
hfx : AnalyticAt 𝕜 f x
hs : s ∈ 𝓝[≠] f x
this : ∀ᶠ (z : 𝕜) in 𝓝 x, f z ∈ insert (f x) s
h : ¬f ⁻¹' s ∈ 𝓝[≠] x
z : 𝕜
h₁z : f z ∈ s → False
h₂z : f z ∈ insert (f x) s
⊢ f z = f x

Tactic:
Set.mem_insert_iff

Goal state after:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
s : Set E
hfx : AnalyticAt 𝕜 f x
hs : s ∈ 𝓝[≠] f x
this : ∀ᶠ (z : 𝕜) in 𝓝 x, f z ∈ insert (f x) s
h : ¬f ⁻¹' s ∈ 𝓝[≠] x
z : 𝕜
h₁z : f z ∈ s → False
h₂z : f z = f x ∨ f z ∈ s
⊢ f z = f x
Module: Mathlib.Analysis.Calculus.LogDeriv

Goal state before:
pp: case inr.inr
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hdf : DifferentiableAt 𝕜 f x
n : ℤ
hn : n ≠ 0
hf : f x ≠ 0
⊢ deriv (fun x ↦ x ^ n) (f x) * deriv f x / f x ^ n = ↑n * logDeriv f x

Tactic:
deriv_zpow,

Goal state after:
case inr.inr
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hdf : DifferentiableAt 𝕜 f x
n : ℤ
hn : n ≠ 0
hf : f x ≠ 0
⊢ ↑n * f x ^ (n - 1) * deriv f x / f x ^ n = ↑n * logDeriv f x
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' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖‖x - x₀‖ ^ n‖
c : ℝ
hc : 0 < c
⊢ ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f x - f x₀‖ ≤ c * ‖‖x - x₀‖ ^ (n + 1)‖

Tactic:
norm_pow,

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 : ℝ
hc : 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' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖‖x - x₀‖ ^ n‖
c : ℝ
hc : 0 < c
⊢ ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f x - f x₀‖ ≤ c * ‖x - x₀‖ ^ n * ‖x - x₀‖

Tactic:
norm_pow,

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
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖‖x - x₀‖‖ ^ n
⊢ ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f x - f x₀‖ ≤ c * ‖x - x₀‖ ^ n * ‖x - x₀‖
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

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
s : Set E
f : E → F
n : ℕ∞ω
x : G
g : G →L[𝕜] E
u : Set E
hu : u ∈ 𝓝[insert (g x) s] g x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u
⊢ ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ (p (g x) i).compContinuousLinearMap fun x ↦ g) (⇑g ⁻¹' u)

Tactic:
· intro i
      change AnalyticOn 𝕜 (fun x ↦
        ContinuousMultilinearMap.compContinuousLinearMapL (fun _ ↦ g) (p (g x) i)) (⇑g ⁻¹' u)
      apply AnalyticOn.comp _ _ (Set.mapsTo_univ _ _)
      · exact ContinuousLinearMap.analyticOn _ _
      · exact (h'p i).comp (g.analyticOn _) (mapsTo_preimage _ _)

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

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
n : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ↑i ≤ n →
    ∀ {x : E},
      x ∈ s →
        ∀ {m : Fin i → E}, (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s x) m = ((iteratedFDerivWithin 𝕜 i c s x) m) u
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : ↑i < n
h_deriv_apply : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s) s
h_deriv : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i c s) s
⊢ ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s) s x) (m 0)) (Fin.tail m) =
    (((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x) (m 0)) (Fin.tail m)) u

Tactic:
← fderivWithin_continuousMultilinear_apply_const_apply (hs x hx) (h_deriv_apply x hx)

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
n : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ↑i ≤ n →
    ∀ {x : E},
      x ∈ s →
        ∀ {m : Fin i → E}, (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s x) m = ((iteratedFDerivWithin 𝕜 i c s x) m) u
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : ↑i < n
h_deriv_apply : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s) s
h_deriv : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i c s) s
⊢ (fderivWithin 𝕜 (fun y ↦ (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s y) (Fin.tail m)) s x) (m 0) =
    (((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x) (m 0)) (Fin.tail m)) u
Module: Mathlib.Analysis.Calculus.ContDiff.Comp

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
s : Set E
n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun x ↦ (x, g x)) '' s] (x₀, g x₀)
v : Set (E × F)
hv : v ∈ 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀)
hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)
f_an : n = ω → AnalyticOn 𝕜 (uncurry f) v
f' : E × F → E × F →L[𝕜] G
hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x
hf' : ContDiffWithinAt 𝕜 n f' (insert x₀ s ×ˢ t) (x₀, g x₀)
this : (x₀, g x₀) ∈ v
⊢ (fun z ↦ (z, g z)) ⁻¹' v ∈ 𝓝[s] x₀

Tactic:
refine (continuousWithinAt_id.prodMk hg.continuousWithinAt).preimage_mem_nhdsWithin' ?_

Goal state after:
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
s : Set E
n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun x ↦ (x, g x)) '' s] (x₀, g x₀)
v : Set (E × F)
hv : v ∈ 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀)
hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)
f_an : n = ω → AnalyticOn 𝕜 (uncurry f) v
f' : E × F → E × F →L[𝕜] G
hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x
hf' : ContDiffWithinAt 𝕜 n f' (insert x₀ s ×ˢ t) (x₀, g x₀)
this : (x₀, g x₀) ∈ v
⊢ v ∈ 𝓝[(fun x ↦ (id x, g x)) '' s] (id x₀, g x₀)
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
x : E
n : ℕ∞ω
y : E
⊢ ContDiffWithinAt 𝕜 n f (insert y s) x ↔ ContDiffWithinAt 𝕜 n f s x

Tactic:
by
  rcases eq_or_ne x y with (rfl | hx)
  · exact contDiffWithinAt_insert_self
  refine ⟨fun h ↦ h.mono (subset_insert _ _), fun h ↦ ?_⟩
  apply h.mono_of_mem_nhdsWithin
  simp [nhdsWithin_insert_of_ne hx, self_mem_nhdsWithin]

Goal state after:
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
⊢ ContDiff 𝕜 ∞ f ↔ Differentiable 𝕜 f ∧ ContDiff 𝕜 ∞ (deriv f)

Tactic:
show (∞ : ℕ∞ω) = ∞ + 1 from rfl,

Goal state after:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
⊢ ContDiff 𝕜 (∞ + 1) f ↔ Differentiable 𝕜 f ∧ ContDiff 𝕜 (∞ + 1) (deriv f)
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
s : Set E
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hf : ContDiffWithinAt 𝕜 n (uncurry f) (s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 m g s x₀
ht : UniqueDiffOn 𝕜 t
hmn : m + 1 ≤ n
hx₀ : x₀ ∈ s
hst : s ⊆ g ⁻¹' t
⊢ ContDiffWithinAt 𝕜 m (fun x ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀

Tactic:
← insert_eq_self.mpr hx₀

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
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hf : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 m g s x₀
ht : UniqueDiffOn 𝕜 t
hmn : m + 1 ≤ n
hx₀ : x₀ ∈ s
hst : s ⊆ g ⁻¹' t
⊢ ContDiffWithinAt 𝕜 m (fun x ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
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
x : E
n : ℕ∞ω
hn : n ≠ ∞
⊢ ContDiffWithinAt 𝕜 n f s x ↔ ∃ u ∈ 𝓝[insert x s] x, ContDiffOn 𝕜 n f u

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

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
x : E
n : ℕ∞ω
hn : n ≠ ∞
h : ContDiffWithinAt 𝕜 n f s x
⊢ ∃ u ∈ 𝓝[insert x s] x, ContDiffOn 𝕜 n f u

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 ≠ ∞
h : ∃ u ∈ 𝓝[insert x s] x, ContDiffOn 𝕜 n f u
⊢ ContDiffWithinAt 𝕜 n f s x
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
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
n : ℕ∞ω
hn : n ≠ ∞
h :
  ∀ x ∈ s,
    ∃ u ∈ 𝓝[insert x s] x,
      (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 (n + 1) f s x

Tactic:
contDiffWithinAt_succ_iff_hasFDerivWithinAt hn

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
n : ℕ∞ω
hn : n ≠ ∞
h :
  ∀ x ∈ s,
    ∃ u ∈ 𝓝[insert x s] x,
      (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u
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