mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
n : ℕ
⊢ iteratedDerivWithin n (fun x ↦ 1) s x = if n + 1 = 0 then x else if n + 1 = 1 then 1 else 0

pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
n : ℕ
⊢ Set.EqOn (derivWithin id s) (fun x ↦ 1) s

Tactic:
]

Goal state after:
case succ
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
n : ℕ
⊢ iteratedDerivWithin n (fun x ↦ 1) s x = if n + 1 = 0 then x else if n + 1 = 1 then 1 else 0

𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
n : ℕ
⊢ Set.EqOn (derivWithin id s) (fun x ↦ 1) s
Module: Mathlib.Analysis.SpecialFunctions.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
this :
  (fun h ↦ exp x * (exp (0 + h) - exp 0 - (ContinuousLinearMap.id 𝕂 𝔸) h)) =ᶠ[𝓝 0] fun h ↦
    exp (x + h) - exp x - exp x • (ContinuousLinearMap.id 𝕂 𝔸) h
⊢ HasFDerivAt exp (ContinuousLinearMap.id 𝕂 𝔸) 0

Tactic:
]

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
this :
  (fun h ↦ exp x * (exp (0 + h) - exp 0 - (ContinuousLinearMap.id 𝕂 𝔸) h)) =ᶠ[𝓝 0] fun h ↦
    exp (x + h) - exp x - exp x • (ContinuousLinearMap.id 𝕂 𝔸) h
⊢ HasFDerivAt exp (ContinuousLinearMap.id 𝕂 𝔸) 0
Module: Mathlib.Analysis.SpecialFunctions.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
this : ∀ᶠ (h : 𝔸) in 𝓝 0, h ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
a✝ : 𝔸
hh : a✝ ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ exp x * (exp a✝ - 1 - a✝) = exp x * exp a✝ - exp x - exp x * a✝

Tactic:
]

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
this : ∀ᶠ (h : 𝔸) in 𝓝 0, h ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
a✝ : 𝔸
hh : a✝ ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ exp x * (exp a✝ - 1 - a✝) = exp x * exp a✝ - exp x - exp x * a✝
Module: Mathlib.Analysis.SpecialFunctions.Exponential

Goal state before:
pp: x : ℂ
⊢ (exp' x).lim = (fun x ↦ ∑' (n : ℕ), x ^ n / ↑n !) x

Tactic:
]

Goal state after:
x : ℂ
⊢ (exp' x).lim = (fun x ↦ ∑' (n : ℕ), x ^ n / ↑n !) x
Module: Mathlib.Analysis.SpecialFunctions.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ (fun h ↦ exp ((t + h) • x) - exp (t • x) - (exp (t • x) • ContinuousLinearMap.smulRight 1 x) h) =o[𝓝 0] fun h ↦ h

Tactic:
]

Goal state after:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ (fun h ↦ exp ((t + h) • x) - exp (t • x) - (exp (t • x) • ContinuousLinearMap.smulRight 1 x) h) =o[𝓝 0] fun h ↦ h
Module: Mathlib.Analysis.SpecialFunctions.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
this :
  (fun h ↦ exp (t • x) * (exp ((0 + h) • x) - exp (0 • x) - (ContinuousLinearMap.smulRight 1 x) h)) =ᶠ[𝓝 0] fun h ↦
    exp ((t + h) • x) - exp (t • x) - (exp (t • x) • ContinuousLinearMap.smulRight 1 x) h
⊢ HasFDerivAt (fun u ↦ exp (u • x)) (ContinuousLinearMap.smulRight 1 x) 0

Tactic:
]

Goal state after:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
this :
  (fun h ↦ exp (t • x) * (exp ((0 + h) • x) - exp (0 • x) - (ContinuousLinearMap.smulRight 1 x) h)) =ᶠ[𝓝 0] fun h ↦
    exp ((t + h) • x) - exp (t • x) - (exp (t • x) • ContinuousLinearMap.smulRight 1 x) h
⊢ HasFDerivAt (fun u ↦ exp (u • x)) (ContinuousLinearMap.smulRight 1 x) 0
Module: Mathlib.Analysis.SpecialFunctions.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
this :
  (fun h ↦ exp (t • x) * (exp ((0 + h) • x) - exp (0 • x) - (ContinuousLinearMap.smulRight 1 x) h)) =ᶠ[𝓝 0] fun h ↦
    exp ((t + h) • x) - exp (t • x) - (exp (t • x) • ContinuousLinearMap.smulRight 1 x) h
⊢ HasFDerivAt exp 1 0

Tactic:
]

Goal state after:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
this :
  (fun h ↦ exp (t • x) * (exp ((0 + h) • x) - exp (0 • x) - (ContinuousLinearMap.smulRight 1 x) h)) =ᶠ[𝓝 0] fun h ↦
    exp ((t + h) • x) - exp (t • x) - (exp (t • x) • ContinuousLinearMap.smulRight 1 x) h
⊢ HasFDerivAt exp 1 0
Module: Mathlib.Analysis.SpecialFunctions.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ Tendsto (fun h ↦ h • x) (𝓝 0) (𝓝 (0 • x))

Tactic:
]

Goal state after:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ Tendsto (fun h ↦ h • x) (𝓝 0) (𝓝 (0 • x))
Module: Mathlib.Analysis.SpecialFunctions.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
this✝¹ : Tendsto (fun h ↦ h • x) (𝓝 0) (𝓝 0)
this✝ : ∀ᶠ (h : 𝕊) in 𝓝 0, h • x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
h : 𝕊
hh : h • x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
this : Commute (t • x) (h • x)
⊢ exp (t • x) * exp (h • x) - exp (t • x) - exp (t • x) * h • x =
    exp (t • x) * exp (h • x) - exp (t • x) - exp (t • x) * h • x

Tactic:
]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_3
inst✝³ : Fintype ι
F' : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (F' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (F' i)
inst✝ : DecidableEq ι
k : ℕ∞ω
x : (i : ι) → F' i
i : ι
⊢ ∀ (i_1 : ι), ContDiff 𝕜 k fun x_1 ↦ update x i x_1 i_1

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_3
inst✝³ : Fintype ι
F' : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (F' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (F' i)
inst✝ : DecidableEq ι
k : ℕ∞ω
x : (i : ι) → F' i
i : ι
⊢ ∀ (i_1 : ι), ContDiff 𝕜 k fun x_1 ↦ update x i x_1 i_1
Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv

Goal state before:
pp: ⊢ AnalyticOnNhd ℂ NormedSpace.exp univ

Tactic:
]

Goal state after:
⊢ AnalyticOnNhd ℂ NormedSpace.exp univ
Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv

Goal state before:
pp: x : ℂ
⊢ (fun h ↦ cexp (x + h) - cexp x - h • cexp x) =o[𝓝 0] fun h ↦ h

Tactic:
]

Goal state after:
x : ℂ
⊢ (fun h ↦ cexp (x + h) - cexp x - h • cexp x) =o[𝓝 0] fun h ↦ h
Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv

Goal state before:
pp: n : ℕ
⊢ cexp = cexp

Tactic:
]

Goal state after:
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
x : E
n : ℕ∞ω
f g : E → F
hf : ContDiffWithinAt 𝕜 n f univ x
hg : ContDiffWithinAt 𝕜 n g univ x
⊢ ContDiffWithinAt 𝕜 n (fun x ↦ f x + g x) univ x

Tactic:
]

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
x : E
n : ℕ∞ω
f g : E → F
hf : ContDiffWithinAt 𝕜 n f univ x
hg : ContDiffWithinAt 𝕜 n g univ x
⊢ ContDiffWithinAt 𝕜 n (fun x ↦ f x + g x) univ x
Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv

Goal state before:
pp: n : ℕ
c : ℂ
⊢ (fun x ↦ c ^ n * cexp (c * x)) = fun s ↦ c ^ n * cexp (c * s)

Tactic:
]

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

Goal state before:
pp: ⊢ AnalyticOnNhd ℝ NormedSpace.exp univ

Tactic:
]

Goal state after:
⊢ AnalyticOnNhd ℝ NormedSpace.exp univ
Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv

Goal state before:
pp: n : ℕ
⊢ rexp = rexp

Tactic:
]

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

Goal state before:
pp: n : ℕ
c : ℝ
⊢ (fun x ↦ c ^ n * rexp (c * x)) = fun s ↦ c ^ n * rexp (c * s)

Tactic:
]

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

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x y : E
h : (𝓝[>] 0 ⊓ 𝓟 {x_1 | x + ↑x_1 • y ∈ s}).NeBot
⊢ y ∈ posTangentConeAt s x

Tactic:
]

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x y : E
h : (𝓝[>] 0 ⊓ 𝓟 {x_1 | x + ↑x_1 • y ∈ s}).NeBot
⊢ y ∈ posTangentConeAt s x
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
hy : y ∈ posTangentConeAt s a
ι : Type u
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
hd : Tendsto (fun n ↦ a + d n) l (𝓝[s] a)
⊢ ∀ᶠ (n : ι) in l, c n • (f (a + d n) - f a) ≤ 0

Tactic:
]

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
hy : y ∈ posTangentConeAt s a
ι : Type u
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
hd : Tendsto (fun n ↦ a + d n) l (𝓝[s] a)
⊢ ∀ᶠ (n : ι) in l, c n • (f (a + d n) - f a) ≤ 0
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hy : y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ 0 y ≤ 0

Tactic:
]

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hy : y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ 0 y ≤ 0
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ 0 y = 0

Tactic:
]

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ 0 y = 0
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 ∩ t) x + iteratedFDerivWithin 𝕜 i g (s ∩ t) x

Tactic:
]

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 ∩ t) x
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMinOn f s a
hy : y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ 0 ≤ 0 y

Tactic:
]

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMinOn f s a
hy : y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ 0 ≤ 0 y
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
x : E
n : ℕ∞ω
f : E → F
hf : ContDiffWithinAt 𝕜 n f univ x
⊢ ContDiffWithinAt 𝕜 n (fun x ↦ -f x) univ x

Tactic:
]

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
x : E
n : ℕ∞ω
f : E → F
hf : ContDiffWithinAt 𝕜 n f univ x
⊢ ContDiffWithinAt 𝕜 n (fun x ↦ -f x) univ x
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMinOn f s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ 0 y = 0

Tactic:
]

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMinOn f s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ 0 y = 0
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: case hy
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
a : E
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ y ∈ univ

Tactic:
]

Goal state after:
case hy
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
a : E
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ y ∈ univ
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
f : E → F
hu : UniqueDiffOn 𝕜 s
i : ℕ
hi : ∀ {x : E}, x ∈ s → iteratedFDerivWithin 𝕜 i (-f) s x = -iteratedFDerivWithin 𝕜 i f s x
x : E
hx : x ∈ s
h : Fin (i + 1) → E
⊢ ((fderivWithin 𝕜 (fun x ↦ -iteratedFDerivWithin 𝕜 i f s x) s x) (h 0)) (tail h) =
    ((fderivWithin 𝕜 (fun i_1 ↦ -iteratedFDerivWithin 𝕜 i f s i_1) s x) (h 0)) (tail h)

Tactic:
]

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

Goal state before:
pp: case hy'
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
a : E
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ -y ∈ univ

Tactic:
]

Goal state after:
case hy'
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
a : E
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ -y ∈ univ
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
f : E → F
hu : UniqueDiffOn 𝕜 s
i : ℕ
hi : ∀ {x : E}, x ∈ s → iteratedFDerivWithin 𝕜 i (-f) s x = -iteratedFDerivWithin 𝕜 i f s x
x : E
hx : x ∈ s
h : Fin (i + 1) → E
⊢ -((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x) (h 0)) (tail h) =
    -((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x) (h 0)) (tail h)

Tactic:
]

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 : 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
A :
  ∀ (c : OrderedFinpartition m),
    HasFDerivWithinAt (fun x ↦ (q (f x)).compAlongOrderedFinpartition (p x) c)
      (∑ i, ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft) s x
B :
  HasFDerivWithinAt (fun x ↦ (q (f x)).taylorComp (p x) m)
    (∑ c, ∑ i, ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft) s x
this : ∑ c, ∑ i, (q (f x)).compAlongOrderedFinpartition (p x) (c.extend i) = (q (f x)).taylorComp (p x) (m + 1)
⊢ HasFDerivWithinAt (fun x ↦ (q (f x)).taylorComp (p x) m)
    (∑ c, ∑ i, (q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft s x

Tactic:
]

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 : 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
A :
  ∀ (c : OrderedFinpartition m),
    HasFDerivWithinAt (fun x ↦ (q (f x)).compAlongOrderedFinpartition (p x) c)
      (∑ i, ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft) s x
B :
  HasFDerivWithinAt (fun x ↦ (q (f x)).taylorComp (p x) m)
    (∑ c, ∑ i, ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft) s x
this : ∑ c, ∑ i, (q (f x)).compAlongOrderedFinpartition (p x) (c.extend i) = (q (f x)).taylorComp (p x) (m + 1)
⊢ HasFDerivWithinAt (fun x ↦ (q (f x)).taylorComp (p x) m)
    (∑ c, ∑ i, (q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft s x
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: case mpr
s : Set ℝ
a : ℝ
h : ∃ᶠ (a_1 : ℝ) in 𝓝 0, a + a_1 ∈ Ioi a ∩ s
⊢ ∃ᶠ (t : ℝ) in 𝓝[>] 0, a + t • 1 ∈ s

Tactic:
]

Goal state after:
case mpr
s : Set ℝ
a : ℝ
h : ∃ᶠ (a_1 : ℝ) in 𝓝 0, a + a_1 ∈ Ioi a ∩ s
⊢ ∃ᶠ (t : ℝ) in 𝓝[>] 0, a + t • 1 ∈ s
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun x ↦ x ^ i) s x = ↑(i.descFactorial k) * x ^ (i - k)
k : ℕ
⊢ (i + 1) * i.descFactorial k = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun x ↦ x ^ i) s x = ↑(i.descFactorial k) * x ^ (i - k)
k : ℕ
⊢ (i + 1) * i.descFactorial k = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: s : Set ℝ
a : ℝ
⊢ (∃ᶠ (x : ℝ) in 𝓝 a, x ∈ s ∩ Ioi a) ↔ ∃ᶠ (x : ℝ) in 𝓝 a, x ∈ s ∧ x ∈ Ioi a

Tactic:
]

Goal state after:
s : Set ℝ
a : ℝ
⊢ (∃ᶠ (x : ℝ) in 𝓝 a, x ∈ s ∩ Ioi a) ↔ ∃ᶠ (x : ℝ) in 𝓝 a, x ∈ s ∧ x ∈ Ioi a
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
⊢ iteratedFDerivWithin 𝕜 i f s x + -iteratedFDerivWithin 𝕜 i g s x =
    iteratedFDerivWithin 𝕜 i f s x + -iteratedFDerivWithin 𝕜 i g s x

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
⊢ ContDiffWithinAt 𝕜 (↑i) (-g) s x

Tactic:
]

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
⊢ ContDiffWithinAt 𝕜 (↑i) (-g) s x