mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

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

Tactic:
hx

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞
Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x ↦ iteratedFDerivWithin 𝕜 m f s x) s
Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x ↦ iteratedFDerivWithin 𝕜 m f s x) s
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 (↑n) f 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
n : ℕ∞ω
h : ∀ (m : ℕ), AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s
x : E
⊢ x ∈ s → ContDiffWithinAt 𝕜 ω f s x

Tactic:
hx

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h : ∀ (m : ℕ), AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 ω f 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
n : ℕ∞ω
m : ℕ
h : ContDiffOn 𝕜 n f s
hmn : ↑m < n
hs : UniqueDiffOn 𝕜 s
x : E
⊢ x ∈ s → DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f s) s x

Tactic:
hx

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
m : ℕ
h : ContDiffOn 𝕜 n f s
hmn : ↑m < n
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
⊢ DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f s) 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
n : ℕ∞ω
m : ℕ
h : ContDiffOn 𝕜 n f s
hmn : ↑m < n
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
this : ↑(m + 1) ≤ n
⊢ DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f s) s x

Tactic:
apply (((h.of_le this).ftaylorSeriesWithin hs).fderivWithin m ?_ x hx).differentiableWithinAt

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
m : ℕ
h : ContDiffOn 𝕜 n f s
hmn : ↑m < n
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
this : ↑(m + 1) ≤ n
⊢ ↑m < ↑(m + 1)
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case inl
𝕜 : 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
hf : DifferentiableOn 𝕜 f s
h' : ∞ = ω → AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 ∞ (fun y ↦ fderivWithin 𝕜 f s y) s
m : ℕ
x : E
⊢ x ∈ s → ContDiffWithinAt 𝕜 (↑m) f s x

Tactic:
hx

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

Tactic:
hx

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
⊢ ContDiffWithinAt 𝕜 (n + 1) f s x
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
H : ContDiffOn 𝕜 ω f univ
⊢ HasFTaylorSeriesUpTo ω f (ftaylorSeriesWithin 𝕜 f univ) ∧
    ∀ (i : ℕ), AnalyticOnNhd 𝕜 (fun x ↦ ftaylorSeriesWithin 𝕜 f univ x i) univ

Tactic:
rw [← hasFTaylorSeriesUpToOn_univ_iff]

Goal state after:
case h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
H : ContDiffOn 𝕜 ω f univ
⊢ HasFTaylorSeriesUpToOn ω f (ftaylorSeriesWithin 𝕜 f univ) univ ∧
    ∀ (i : ℕ), AnalyticOnNhd 𝕜 (fun x ↦ ftaylorSeriesWithin 𝕜 f univ x i) univ
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n✝ : ℕ∞ω
n : ℕ∞
H : ContDiffOn 𝕜 (↑n) f univ
⊢ HasFTaylorSeriesUpTo (↑n) f (ftaylorSeriesWithin 𝕜 f univ)

Tactic:
rw [← hasFTaylorSeriesUpToOn_univ_iff]

Goal state after:
case h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n✝ : ℕ∞ω
n : ℕ∞
H : ContDiffOn 𝕜 (↑n) f univ
⊢ HasFTaylorSeriesUpToOn (↑n) f (ftaylorSeriesWithin 𝕜 f univ) univ
Module: Mathlib.Analysis.Complex.RealDeriv

Goal state before:
pp: e : ℂ → ℂ
e' : ℂ
z : ℝ
hf : HasDerivAt e e' ↑z
⊢ HasDerivAt (fun y ↦ e ↑y) e' z

Tactic:
simpa only [ofRealCLM_apply, ofReal_one, mul_one] using! hf.comp z ofRealCLM.hasDerivAt

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

Goal state before:
pp: case refine_3
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
φ : (i : ι) → E → F' i
p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)
n : ℕ∞ω
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
L : (m : ℕ) → ((i : ι) → E [×m]→L[𝕜] F' i) ≃ₗᵢ[𝕜] E [×m]→L[𝕜] (i : ι) → F' i :=
  fun m ↦ ContinuousMultilinearMap.piₗᵢ 𝕜 fun _i ↦ E
h : ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s
m : ℕ
hm : ↑m < n
x : E
⊢ x ∈ s →
    HasFDerivWithinAt (fun x ↦ ContinuousMultilinearMap.pi fun i ↦ p' i x m)
      (ContinuousMultilinearMap.pi fun i ↦ p' i x m.succ).curryLeft s x

Tactic:
hx

Goal state after:
case refine_3
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
φ : (i : ι) → E → F' i
p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)
n : ℕ∞ω
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
L : (m : ℕ) → ((i : ι) → E [×m]→L[𝕜] F' i) ≃ₗᵢ[𝕜] E [×m]→L[𝕜] (i : ι) → F' i :=
  fun m ↦ ContinuousMultilinearMap.piₗᵢ 𝕜 fun _i ↦ E
h : ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (fun x ↦ ContinuousMultilinearMap.pi fun i ↦ p' i x m)
    (ContinuousMultilinearMap.pi fun i ↦ p' i x m.succ).curryLeft s x
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case zero_eq
𝕜 : 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 : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
x : E
⊢ x ∈ s → ((q (f x)).taylorComp (p x) 0).curry0 = (g ∘ f) x

Tactic:
hx

Goal state after:
case zero_eq
𝕜 : 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 : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
x : E
hx : x ∈ s
⊢ ((q (f x)).taylorComp (p x) 0).curry0 = (g ∘ f) x
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case fderivWithin
𝕜 : 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 : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
m : ℕ
hm : ↑m < n
x : E
⊢ x ∈ s → HasFDerivWithinAt (fun x ↦ (q (f x)).taylorComp (p x) m) ((q (f x)).taylorComp (p x) m.succ).curryLeft s x

Tactic:
hx

Goal state after:
case fderivWithin
𝕜 : 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 : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (fun x ↦ (q (f x)).taylorComp (p x) m) ((q (f x)).taylorComp (p x) m.succ).curryLeft s x
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
x : E
i : ℕ
f g : E → F
hf : ContDiffWithinAt 𝕜 (↑i) f s x
hg : ContDiffWithinAt 𝕜 (↑i) g s x
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
this : ∀ᶠ (x : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 (↑i) f s x ∧ ContDiffWithinAt 𝕜 (↑i) g s x
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
h : t ∩ insert x s ⊆ {x | (fun x ↦ ContDiffWithinAt 𝕜 (↑i) f s x ∧ ContDiffWithinAt 𝕜 (↑i) g s x) x}
hft : ContDiffOn 𝕜 (↑i) f (s ∩ t)
hgt : ContDiffOn 𝕜 (↑i) g (s ∩ t)
hut : UniqueDiffOn 𝕜 (s ∩ t)
H : s ∩ t =ᶠ[𝓝 x] s
⊢ iteratedFDerivWithin 𝕜 i (f + g) s x = iteratedFDerivWithin 𝕜 i f s x + iteratedFDerivWithin 𝕜 i g s x

Tactic:
← iteratedFDerivWithin_congr_set H,

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
x : E
i : ℕ
f g : E → F
hf : ContDiffWithinAt 𝕜 (↑i) f s x
hg : ContDiffWithinAt 𝕜 (↑i) g s x
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
this : ∀ᶠ (x : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 (↑i) f s x ∧ ContDiffWithinAt 𝕜 (↑i) g s x
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
h : t ∩ insert x s ⊆ {x | (fun x ↦ ContDiffWithinAt 𝕜 (↑i) f s x ∧ ContDiffWithinAt 𝕜 (↑i) g s x) x}
hft : ContDiffOn 𝕜 (↑i) f (s ∩ t)
hgt : ContDiffOn 𝕜 (↑i) g (s ∩ t)
hut : UniqueDiffOn 𝕜 (s ∩ t)
H : s ∩ t =ᶠ[𝓝 x] s
⊢ iteratedFDerivWithin 𝕜 i (f + g) (s ∩ t) x = iteratedFDerivWithin 𝕜 i f s x + iteratedFDerivWithin 𝕜 i g s x
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
x : E
i : ℕ
f g : E → F
hf : ContDiffWithinAt 𝕜 (↑i) f s x
hg : ContDiffWithinAt 𝕜 (↑i) g s x
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
this : ∀ᶠ (x : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 (↑i) f s x ∧ ContDiffWithinAt 𝕜 (↑i) g s x
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
h : t ∩ insert x s ⊆ {x | (fun x ↦ ContDiffWithinAt 𝕜 (↑i) f s x ∧ ContDiffWithinAt 𝕜 (↑i) g s x) x}
hft : ContDiffOn 𝕜 (↑i) f (s ∩ t)
hgt : ContDiffOn 𝕜 (↑i) g (s ∩ t)
hut : UniqueDiffOn 𝕜 (s ∩ t)
H : s ∩ t =ᶠ[𝓝 x] s
⊢ iteratedFDerivWithin 𝕜 i (f + g) (s ∩ t) x = iteratedFDerivWithin 𝕜 i f s x + iteratedFDerivWithin 𝕜 i g s x

Tactic:
← iteratedFDerivWithin_congr_set H,

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
x : E
i : ℕ
f g : E → F
hf : ContDiffWithinAt 𝕜 (↑i) f s x
hg : ContDiffWithinAt 𝕜 (↑i) g s x
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
this : ∀ᶠ (x : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 (↑i) f s x ∧ ContDiffWithinAt 𝕜 (↑i) g s x
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
h : t ∩ insert x s ⊆ {x | (fun x ↦ ContDiffWithinAt 𝕜 (↑i) f s x ∧ ContDiffWithinAt 𝕜 (↑i) g s x) x}
hft : ContDiffOn 𝕜 (↑i) f (s ∩ t)
hgt : ContDiffOn 𝕜 (↑i) g (s ∩ t)
hut : UniqueDiffOn 𝕜 (s ∩ t)
H : s ∩ t =ᶠ[𝓝 x] s
⊢ iteratedFDerivWithin 𝕜 i (f + g) (s ∩ t) x = iteratedFDerivWithin 𝕜 i f (s ∩ t) x + iteratedFDerivWithin 𝕜 i g s x
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 : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
c : OrderedFinpartition m
B : (F [×c.length]→L[𝕜] G) →L[𝕜] (E [×c.partSize i]→L[𝕜] F) [×c.length]→L[𝕜] E [×m]→L[𝕜] G :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
cm : ↑c.length ≤ ↑m
cp : ∀ (i : Fin c.length), ↑(c.partSize i) ≤ ↑m
I : ∀ (i : Fin c.length), HasFDerivWithinAt (fun x ↦ p x (c.partSize i)) (p x (c.partSize i).succ).curryLeft s x
J : HasFDerivWithinAt (fun x ↦ q x c.length) (q (f x) c.length.succ).curryLeft t (f x)
K : HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) s x
⊢ HasFDerivWithinAt (fun y ↦ (B (q (f y) c.length)) fun i ↦ p y (c.partSize i))
    (∑ i, ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft) s x

Tactic:
convert! HasFDerivWithinAt.linear_multilinear_comp (J.comp x K h) I B

Goal state after:
case e'_12
𝕜 : 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 : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
c : OrderedFinpartition m
B : (F [×c.length]→L[𝕜] G) →L[𝕜] (E [×c.partSize i]→L[𝕜] F) [×c.length]→L[𝕜] E [×m]→L[𝕜] G := ⋯
cm : ↑c.length ≤ ↑m
cp : ∀ (i : Fin c.length), ↑(c.partSize i) ≤ ↑m
I : ∀ (i : Fin c.length), HasFDerivWithinAt (fun x ↦ p x (c.partSize i)) (p x (c.partSize i).succ).curryLeft s x
J : HasFDerivWithinAt (fun x ↦ q x c.length) (q (f x) c.length.succ).curryLeft t (f x)
K : HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) s x
e_8✝ : ContinuousMultilinearMap.instAddCommGroup = ContinuousMultilinearMap.normedAddCommGroup'.toAddCommGroup
e_9✝ : ContinuousMultilinearMap.instModule ≍ ContinuousMultilinearMap.normedSpace'.toModule
e_10✝ : ContinuousMultilinearMap.instTopologicalSpace = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
⊢ ∑ i, ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft =
    (B.flipMultilinear fun i ↦ p x (c.partSize i)) ∘SL
        (q (f x) c.length.succ).curryLeft ∘SL (continuousMultilinearCurryFin1 𝕜 E F) (p x 1) +
      ∑ i,
        (B (((fun x ↦ q x c.length) ∘ f) x)).toContinuousLinearMap (fun j ↦ p x (c.partSize j)) i ∘SL
          (p x (c.partSize i).succ).curryLeft
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
f : 𝕜 → F
hn : 0 < n
c : F
⊢ iteratedDeriv n (fun z ↦ c - f z) x = iteratedDeriv n (-f) x

Tactic:
simpa only [← iteratedDerivWithin_univ] using! iteratedDerivWithin_const_sub hn c

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

Goal state before:
pp: case h.refine_3
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n✝ : ℕ∞ω
inst✝ : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑f.symm a)
n : ℕ
IH : ContDiffAt 𝕜 (↑↑n) (↑f) (↑f.symm a) → ContDiffAt 𝕜 (↑↑n) (↑f.symm) a
hf : ContDiffAt 𝕜 (↑↑n.succ) (↑f) (↑f.symm a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑f.symm a)
u : Set E
hu : u ∈ 𝓝 (↑f.symm a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑f.symm a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑f.symm a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
htf : ↑f.symm a ∈ t
x : F
⊢ x ∈ f.target ∩ ↑f.symm ⁻¹' t → HasFDerivAt (↑f.symm) ((inverse ∘ f' ∘ ↑f.symm) x) x

Tactic:
hx

Goal state after:
case h.refine_3
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n✝ : ℕ∞ω
inst✝ : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑f.symm a)
n : ℕ
IH : ContDiffAt 𝕜 (↑↑n) (↑f) (↑f.symm a) → ContDiffAt 𝕜 (↑↑n) (↑f.symm) a
hf : ContDiffAt 𝕜 (↑↑n.succ) (↑f) (↑f.symm a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑f.symm a)
u : Set E
hu : u ∈ 𝓝 (↑f.symm a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑f.symm a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑f.symm a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
htf : ↑f.symm a ∈ t
x : F
hx : x ∈ f.target ∩ ↑f.symm ⁻¹' t
⊢ HasFDerivAt (↑f.symm) ((inverse ∘ f' ∘ ↑f.symm) x) x
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : ℝ → ℝ := fun x ↦ (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
hhb : Tendsto h (𝓝[<] b) (𝓝 (lgb * lfa - lfb * lga))
h' : ℝ → ℝ := fun x ↦ (lgb - lga) * f' x - (lfb - lfa) * g' x
x : ℝ
⊢ x ∈ Ioo a b → HasDerivAt h (h' x) x

Tactic:
hx

Goal state after:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : ℝ → ℝ := fun x ↦ (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
hhb : Tendsto h (𝓝[<] b) (𝓝 (lgb * lfa - lfb * lga))
h' : ℝ → ℝ := fun x ↦ (lgb - lga) * f' x - (lfb - lfa) * g' x
x : ℝ
hx : x ∈ Ioo a b
⊢ HasDerivAt h (h' x) x
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[>] a) atTop
x : ℝ
⊢ x ∈ Ioi a → deriv f x = derivWithin f (Ioi a) x

Tactic:
hx

Goal state after:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[>] a) atTop
x : ℝ
hx : x ∈ Ioi a
⊢ deriv f x = derivWithin f (Ioi a) x
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_gt : ∀ x ∈ interior D, C < deriv f x
x : ℝ
⊢ x ∈ D → ∀ y ∈ D, x < y → C * (y - x) < f y - f x

Tactic:
hx

Goal state after:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_gt : ∀ x ∈ interior D, C < deriv f x
x : ℝ
hx : x ∈ D
⊢ ∀ y ∈ D, x < y → C * (y - x) < f y - f x
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x
x : ℝ
⊢ x ∈ D → ∀ y ∈ D, x ≤ y → C * (y - x) ≤ f y - f x

Tactic:
hx

Goal state after:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x
x : ℝ
hx : x ∈ D
⊢ ∀ y ∈ D, x ≤ y → C * (y - x) ≤ f y - f x
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, 0 < deriv f x
x : ℝ
⊢ x ∈ D → ∀ ⦃b : ℝ⦄, b ∈ D → x < b → f x < f b

Tactic:
hx

Goal state after:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, 0 < deriv f x
x : ℝ
hx : x ∈ D
⊢ ∀ ⦃b : ℝ⦄, b ∈ D → x < b → f x < f b
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: 𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid O
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R O
f : M →ₗ[R] N
C : ConvexCone R N
x : M
hx : x ∈ ⇑f ⁻¹' ↑C
y : M
hy : y ∈ ⇑f ⁻¹' ↑C
⊢ f x + f y ∈ ↑C

Tactic:
exact add_mem hx hy

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: n : ℕ∞ω
x : ℝ
⊢ x ∈ {0}ᶜ → ContDiffWithinAt ℝ n log {0}ᶜ x

Tactic:
hx

Goal state after:
n : ℕ∞ω
x : ℝ
hx : x ∈ {0}ᶜ
⊢ ContDiffWithinAt ℝ n log {0}ᶜ x