mathlib-initiative/mathlib-tactics huggingface dataset:
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
x✝ : 𝕜
⊢ (∏ i ∈ u, f i) x✝ = ∏ i ∈ u, f i x✝

Tactic:
simp

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

Goal state before:
pp: case e'_11
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
H : DifferentiableAt 𝕜 (fun x ↦ f (b - x)) a
x✝ : 𝕜
⊢ f x✝ = ((fun x ↦ f (b - x)) ∘ HSub.hSub b) x✝

Tactic:
simp

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

Goal state before:
pp: case e'_9
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ
IH : CPolynomialOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm =
    ⇑↑↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: k : Type u_1
E : Type u_2
PE : Type u_3
inst✝⁶ : Field k
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module k E
inst✝³ : AddTorsor E PE
F : Type u_4
PF : Type u_5
inst✝² : AddCommGroup F
inst✝¹ : Module k F
inst✝ : AddTorsor F PF
f : PE →ᵃ[k] PF
g : k → PE
a b : k
⊢ slope (⇑f ∘ g) a b = f.linear (slope g a b)

Tactic:
simp only [slope, (· ∘ ·), f.linear.map_smul, f.linearMap_vsub]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: case inl
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a r : k
⊢ (lineMap (slope f ((lineMap a a) r) a) (slope f a ((lineMap a a) r))) r = slope f a a

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: case inr
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
⊢ (lineMap (slope f ((lineMap a b) r) b) (slope f ((lineMap a b) r) a)) r = slope f b a

Tactic:
slope_comm _ _ b

Goal state after:
case inr
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
⊢ (lineMap (slope f b ((lineMap a b) r)) (slope f ((lineMap a b) r) a)) r = slope f b a
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: 𝕜 : 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 ι
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : DecidableEq ι
x : G
f : G → ContinuousMultilinearMap 𝕜 E F
g : (i : ι) → G → E i
f' : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
g' : (i : ι) → G →L[𝕜] E i
hf : HasStrictFDerivAt f f' x
hg : ∀ (i : ι), HasStrictFDerivAt (g i) (g' i) x
x✝ : G
⊢ ((apply 𝕜 E F fun x_1 ↦ g x_1 x) ∘SL f' + ∑ i, (f x).toContinuousLinearMap (fun x_1 ↦ g x_1 x) i ∘SL g' i) x✝ =
    ((apply 𝕜 E F (f x, fun x_1 ↦ g x_1 x).2 ∘SL
            ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i) +
          (f x, fun x_1 ↦ g x_1 x).1.linearDeriv (f x, fun x_1 ↦ g x_1 x).2 ∘SL
            ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i)) ∘SL
        f'.prod (ContinuousLinearMap.pi g'))
      x✝

Tactic:
simp

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

Goal state before:
pp: 𝕜 : 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 ι
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : DecidableEq ι
x : G
f : G → ContinuousMultilinearMap 𝕜 E F
g : (i : ι) → G → E i
f' : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
g' : (i : ι) → G →L[𝕜] E i
hf : HasStrictFDerivAt f f' x
hg : ∀ (i : ι), HasStrictFDerivAt (g i) (g' i) x
⊢ HasStrictFDerivAt (fun x ↦ (f x) fun x_1 ↦ g x_1 x)
    ((apply 𝕜 E F fun x_1 ↦ g x_1 x) ∘SL f' + ∑ i, (f x).toContinuousLinearMap (fun x_1 ↦ g x_1 x) i ∘SL g' i) x

Tactic:
convert!
    ContinuousMultilinearMap.hasStrictFDerivAt_uncurry (f x, (g · x)) |>.comp x
      (hf.prodMk (hasStrictFDerivAt_pi.2 hg))
  ext
  simp

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

Goal state before:
pp: case e'_12
𝕜 : 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 ι
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : DecidableEq ι
s : Set G
x : G
f : G → ContinuousMultilinearMap 𝕜 E F
g : (i : ι) → G → E i
f' : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
g' : (i : ι) → G →L[𝕜] E i
hf : HasFDerivWithinAt f f' s x
hg : ∀ (i : ι), HasFDerivWithinAt (g i) (g' i) s x
x✝ : G
⊢ ((apply 𝕜 E F fun x_1 ↦ g x_1 x) ∘SL f' + ∑ i, (f x).toContinuousLinearMap (fun x_1 ↦ g x_1 x) i ∘SL g' i) x✝ =
    ((apply 𝕜 E F (f x, fun x_1 ↦ g x_1 x).2 ∘SL
            ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i) +
          (f x, fun x_1 ↦ g x_1 x).1.linearDeriv (f x, fun x_1 ↦ g x_1 x).2 ∘SL
            ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i)) ∘SL
        f'.prod (ContinuousLinearMap.pi g'))
      x✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_4
inst✝ : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
j : Fin (n + 1)
h'k : e j ∈ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
hj : j ≠ 0
⊢ e j = ((Equiv.embeddingFinSucc n ι) e).fst (j.pred hj)

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
L : Filter 𝕜
⊢ ∀ a ∉ {x}ᶜ, slope f x a - (a - x)⁻¹ • (a - x) • f' = 0

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
⊢ 𝓝[≠] x = map (fun t ↦ x + t) (𝓝[≠] 0)

Tactic:
simp

Goal state after:
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 : MonotoneOn g s
this✝ : (𝓝[s \ {x}] x).NeBot
h'g : MonotoneOn g (insert x s)
this : Tendsto (slope g x) (𝓝[s \ {x}] x) (𝓝 g')
y : 𝕜
hy : y ∈ s ∧ ¬y = x
⊢ x ∈ insert x s

Tactic:
simp

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

Goal state before:
pp: case zero
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : 𝕜
f : 𝕜 → E
hf : ∀ k < 0, (swap dslope a)^[k] f a = 0
⊢ (b - a) ^ 0 • (swap dslope a)^[0] f b = f b

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
n : ℕ
x : Fin n → 𝔸
⊢ ∀ (i : Fin (List.finRange n).length), i ∈ Finset.univ ↔ (finCongr ⋯) i ∈ Finset.univ

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
n : ℕ
x : Fin n → 𝔸
⊢ ∀ i ∈ Finset.univ,
    (List.map x (List.take (↑i) (List.finRange n))).prod •>
        (proj (List.finRange n)[i] <• (List.map x (List.drop (↑i).succ (List.finRange n))).prod) =
      (List.map x (List.take (↑((finCongr ⋯) i)) (List.finRange n))).prod •>
        (proj ((finCongr ⋯) i) <• (List.map x (List.drop (↑((finCongr ⋯) i)).succ (List.finRange n))).prod)

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
l : List ι
x : { i // i ∈ l } → 𝔸
⊢ ∀ (i : Fin l.length), i ∈ Finset.univ ↔ (finCongr ⋯) i ∈ Finset.univ

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
l : List ι
x : { i // i ∈ l } → 𝔸
⊢ ∀ i ∈ Finset.univ,
    (List.map x (List.take (↑i) l.attach)).prod •>
        (proj l.attach[Fin.cast ⋯ i] <• (List.map x (List.drop (↑i).succ l.attach)).prod) =
      (List.map x (List.take (↑((finCongr ⋯) i)) l.attach)).prod •>
        (proj l.attach[(finCongr ⋯) i] <• (List.map x (List.drop (↑((finCongr ⋯) i)).succ l.attach)).prod)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap

Goal state before:
pp: c : ℂ
R θ : ℝ
⊢ circleMap c R θ ∈ sphere c |R|

Tactic:
simp

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

Goal state before:
pp: case inl
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
⊢ 0 = -(0 ^ 2)⁻¹

Tactic:
simp

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
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
z : 𝕜
k : ℕ
hk : k < p.order
⊢ (fslope^[k] p).coeff 0 = 0

Tactic:
coeff_iterate_fslope,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
z : 𝕜
k : ℕ
hk : k < p.order
⊢ p.coeff (0 + k) = 0
Module: Mathlib.Analysis.Calculus.Deriv.ZPow

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
k : ℕ
x : 𝕜
⊢ deriv^[k] Inv.inv x = deriv^[k] (fun x ↦ x ^ (-1)) x

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
k : ℕ
x : 𝕜
⊢ ((-1) ^ (Finset.range k).card * ∏ x ∈ Finset.range k, (1 + ↑x)) * x ^ (-(1 + ↑k)) =
    (-1) ^ k * ↑(∏ k ∈ Finset.range (k + 1 - 1), (1 + k)) * x ^ (-(1 + ↑k))

Tactic:
simp

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

Goal state before:
pp: case zero
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
c d : 𝕜
⊢ (deriv^[0] fun x ↦ (c * x + d)⁻¹) = fun x ↦ (-1) ^ 0 * ↑0! * c ^ 0 * (c * x + d) ^ (-1 - ↑0)

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst✝⁶ : NormedRing A
inst✝⁵ : IsDomain A
inst✝⁴ : NormedAlgebra 𝕜 A
B : Type u_4
inst✝³ : NormedAddCommGroup B
inst✝² : NormedSpace 𝕜 B
inst✝¹ : Module A B
inst✝ : IsTorsionFree A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : ¬U = ∅
z : 𝕜
hz : z ∈ U
hU'' : U.Nontrivial
this : ∃ᶠ (w : 𝕜) in 𝓝[≠] z, w ∈ U
w : 𝕜
⊢ w ∈ U → f w = 0 ∨ g w = 0

Tactic:
hw

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst✝⁶ : NormedRing A
inst✝⁵ : IsDomain A
inst✝⁴ : NormedAlgebra 𝕜 A
B : Type u_4
inst✝³ : NormedAddCommGroup B
inst✝² : NormedSpace 𝕜 B
inst✝¹ : Module A B
inst✝ : IsTorsionFree A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : ¬U = ∅
z : 𝕜
hz : z ∈ U
hU'' : U.Nontrivial
this : ∃ᶠ (w : 𝕜) in 𝓝[≠] z, w ∈ U
w : 𝕜
hw : w ∈ U
⊢ f w = 0 ∨ g w = 0
Module: Mathlib.Analysis.Calculus.LogDeriv

Goal state before:
pp: case empty
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ i ∈ ∅, f i x ≠ 0
hd : ∀ i ∈ ∅, DifferentiableAt 𝕜 (f i) x
⊢ logDeriv (fun x ↦ ∏ i ∈ ∅, f i x) x = ∑ i ∈ ∅, logDeriv (f i) x

Tactic:
simp

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

Goal state before:
pp: case inl
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hdf : DifferentiableAt 𝕜 f x
⊢ logDeriv (fun x ↦ f x ^ 0) x = ↑0 * logDeriv f x

Tactic:
simp

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

Goal state before:
pp: case e'_4
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
Hr : ∀ x ∈ Icc a b, ∀ r > 0, f x ≤ B x + r * (x - a)
x : ℝ
hx : x ∈ Icc a b
this : ContinuousWithinAt (fun r ↦ B x + r * (x - a)) (Ioi 0) 0
⊢ B x = B x + 0 * (x - a)

Tactic:
simp

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

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
Hr : ∀ x ∈ Icc a b, ∀ r > 0, f x ≤ B x + r * (x - a)
x : ℝ
hx : x ∈ Icc a b
this : ContinuousWithinAt (fun r ↦ B x + r * (x - a)) (Ioi 0) 0
⊢ 0 ∈ closure (Ioi 0)

Tactic:
simp

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

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
φ : E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x - φ‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : E → G := fun y ↦ f y - φ y
hg : ∀ x ∈ s, HasFDerivWithinAt g (f' x - φ) s x
⊢ ‖f y - f x - φ (y - x)‖ = ‖f y - f x - (φ y - φ x)‖

Tactic:
simp

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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅
hs' : IsPreconnected ∅
hf : DifferentiableOn 𝕜 f ∅
hf' : EqOn (fderiv 𝕜 f) 0 ∅
⊢ ∀ x ∈ ∅, f x = 0

Tactic:
simp

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

Goal state before:
pp: case zero
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
x✝¹ : E
x✝ : Fin 0 → E
⊢ (iteratedFDerivWithin 𝕜 0 0 s x✝¹) x✝ = (0 x✝¹) x✝

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
inst✝ : Subsingleton F
⊢ ContDiff 𝕜 n f

Tactic:
Subsingleton.elim f fun _ => 0

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
inst✝ : Subsingleton F
⊢ ContDiff 𝕜 n fun x ↦ 0
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ∞ω
inst✝ : Subsingleton F
⊢ ContDiffAt 𝕜 n f x

Tactic:
Subsingleton.elim f fun _ => 0

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ∞ω
inst✝ : Subsingleton F
⊢ ContDiffAt 𝕜 n (fun x ↦ 0) x
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
inst✝ : Subsingleton F
⊢ ContDiffWithinAt 𝕜 n f s x

Tactic:
Subsingleton.elim f fun _ => 0

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
inst✝ : Subsingleton F
⊢ ContDiffWithinAt 𝕜 n (fun x ↦ 0) s x
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
inst✝ : Subsingleton F
⊢ ContDiffOn 𝕜 n f s

Tactic:
Subsingleton.elim f fun _ => 0

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
inst✝ : Subsingleton F
⊢ ContDiffOn 𝕜 n (fun x ↦ 0) s
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
c : F
⊢ n + 1 ≠ 0

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ∞ω
⊢ ∀ y ∈ {x}, f y = f x

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
x : E
n : ℕ∞ω
f : E → F
g : F →L[𝕜] G
hf : ContDiffWithinAt 𝕜 n f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
hi : ↑i ≤ n
⊢ ↑i = ∞ → n = ω

Tactic:
simp

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

Tactic:
simp

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

Goal state before:
pp: 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 : ℝ
hc : 0 < c
x : ℝ
⊢ ‖toSpanSingleton ℝ (f' x)‖ ≤ c * ‖‖x - x₀‖ ^ n‖ ↔ ‖f' x‖ ≤ c * ‖(x - x₀) ^ n‖

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_3
G : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f f' : 𝕜 → G
s : Set 𝕜
x✝ y : 𝕜
C : ℝ
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖ ≤ C
hs : Convex ℝ s
xs : x✝ ∈ s
ys : y ∈ s
x : 𝕜
hx : x ∈ s
⊢ ‖toSpanSingleton 𝕜 (f' x)‖ ≤ ‖f' x‖

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_3
G : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f f' : 𝕜 → G
s : Set 𝕜
C : ℝ≥0
hs : Convex ℝ s
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖₊ ≤ C
x : 𝕜
hx : x ∈ s
⊢ ‖toSpanSingleton 𝕜 (f' x)‖₊ ≤ ‖f' x‖₊

Tactic:
simp

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

Goal state before:
pp: case zero
𝕜 : 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
hi : ↑0 ≤ n
x : E
hx : x ∈ s
m : Fin 0 → E
⊢ (iteratedFDerivWithin 𝕜 0 (fun y ↦ (c y) u) s x) m = ((iteratedFDerivWithin 𝕜 0 c s x) m) u

Tactic:
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
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
hi : ↑(i + 1) ≤ n
x : E
hx : x ∈ s
m : Fin (i + 1) → E
⊢ i < i + 1

Tactic:
simp

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
x : E
h : ContDiffWithinAt 𝕜 ω f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : AnalyticOn 𝕜 f u
⊢ x ∈ insert x s

Tactic:
simp

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
x : E
h : ContDiffWithinAt 𝕜 ω f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : AnalyticOn 𝕜 f u
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
have xu : x ∈ u := mem_of_mem_nhdsWithin (by simp) hu

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
x : E
h : ContDiffWithinAt 𝕜 ω f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : AnalyticOn 𝕜 f u
xu : x ∈ u
⊢ AnalyticWithinAt 𝕜 f s 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
⊢ DifferentiableOn 𝕜 f s ∧ (0 = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 0 (derivWithin f s) s ↔
    DifferentiableOn 𝕜 f s ∧ ContinuousOn (derivWithin f s) s

Tactic:
simp

Goal state after: