mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.Deriv.Comp

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
f : 𝕜 → F
f' : F
x : 𝕜
l : F → E
l' : F →L[𝕜] E
t : Set F
hl : HasFDerivWithinAt l l' t (f x)
hf : HasDerivAt f f' x
ht : ∀ᶠ (x' : 𝕜) in 𝓝 x, f x' ∈ t
⊢ HasDerivAt (l ∘ f) (l' f') x

Tactic:
by

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

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

Tactic:
by

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

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
f : 𝕜 → F
f' : F
x : 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
t : Set F
hl : HasFDerivWithinAt l l' t y
hf : HasDerivAt f f' x
ht : ∀ᶠ (x' : 𝕜) in 𝓝 x, f x' ∈ t
hy : y = f x
⊢ HasDerivAt (l ∘ f) (l' f') x

Tactic:
by

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
f : 𝕜 → E
z₀ : 𝕜
m n : ℤ
hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z
h_le : n ≤ m
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
left✝ : g z₀ ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
j : 𝕜 → E
hj_an : AnalyticAt 𝕜 j z₀
hj_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • j z
hj_ne : m ≠ n
⊢ ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, j z = (z - z₀) ^ (m - n) • g z

Tactic:
by

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

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
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
hl : HasFDerivAt l l' y
hf : HasDerivWithinAt f f' s x
hy : y = f x
⊢ HasDerivWithinAt (l ∘ f) (l' f') s x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
⊢ deriv (fun x ↦ x ^ m) x = ↑m * x ^ (m - 1)

Tactic:
by

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

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
f : 𝕜 → F
f' : F
x : 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
hl : HasFDerivAt l l' y
hf : HasDerivAt f f' x
hy : y = f x
⊢ HasDerivAt (l ∘ f) (l' f') x

Tactic:
by

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

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
f : 𝕜 → F
f' : F
x : 𝕜
l : F → E
l' : F →L[𝕜] E
hl : HasStrictFDerivAt l l' (f x)
hf : HasStrictDerivAt f f' x
⊢ HasStrictDerivAt (l ∘ f) (l' f') x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
k : ℕ
⊢ (deriv^[k] fun x ↦ x ^ m) = fun x ↦ (∏ i ∈ Finset.range k, (↑m - ↑i)) * x ^ (m - ↑k)

Tactic:
by

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

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
f : 𝕜 → F
f' : F
x : 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
hl : HasStrictFDerivAt l l' y
hf : HasStrictDerivAt f f' x
hy : y = f x
⊢ HasStrictDerivAt (l ∘ f) (l' f') x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
k : ℕ
⊢ deriv^[k] (fun x ↦ x ^ n) x = (∏ i ∈ Finset.range k, (↑n - ↑i)) * x ^ (n - k)

Tactic:
by

Goal state after:
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:
by

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

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
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
l : F → E
t : Set F
hl : DifferentiableWithinAt 𝕜 l t (f x)
hf : DifferentiableWithinAt 𝕜 f s x
hs : MapsTo f s t
⊢ derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x)) (derivWithin f s x)

Tactic:
by

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

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

Tactic:
by

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

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
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
l : F → E
y : F
t : Set F
hl : DifferentiableWithinAt 𝕜 l t y
hf : DifferentiableWithinAt 𝕜 f s x
hs : MapsTo f s t
hy : y = f x
⊢ derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x)) (derivWithin f s x)

Tactic:
by

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

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
f : 𝕜 → F
x : 𝕜
l : F → E
y : F
hl : DifferentiableAt 𝕜 l y
hf : DifferentiableAt 𝕜 f x
hy : y = f x
⊢ deriv (l ∘ f) x = (fderiv 𝕜 l (f x)) (deriv f x)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
c d : 𝕜
k : ℕ
ihk : (deriv^[k] fun x ↦ (c * x + d)⁻¹) = fun x ↦ (-1) ^ k * ↑k ! * c ^ k * (c * x + d) ^ (-1 - ↑k)
z : 𝕜
hd : ¬c = 0
this : deriv (fun x ↦ (c * (x + d / c)) ^ (-1 - ↑k)) z = deriv (fun x ↦ (c * x) ^ (-1 - ↑k)) (z + d / c)
⊢ (fun x ↦ (c * (x + d / c)) ^ (-1 - ↑k)) = fun x ↦ (c * x + d) ^ (-1 - ↑k)

Tactic:
by

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

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

Tactic:
by

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
f : 𝕜 → E
z₀ : 𝕜
m n : ℤ
hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z
⊢ m = n

Tactic:
by

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

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

Tactic:
by

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
f : 𝕜 → E
z₀ : 𝕜
m n : ℕ
hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ m • g z
hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
⊢ m = n

Tactic:
by

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
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ (∃ n g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) ↔ ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0

Tactic:
by

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
f : 𝕜 → E
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
⊢ EqOn f 0 U ∨ ∀ᶠ (x : 𝕜) in codiscreteWithin U, f x ≠ 0

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
L : Filter (𝕜 × 𝕜)
⊢ HasDerivAtFilter (⇑f) (f.linear 1) L

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : E
x : 𝕜
⊢ HasStrictDerivAt (⇑(lineMap a b)) (b - a) x

Tactic:
by

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
f g : 𝕜 → E
z₀ : 𝕜
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
h₀ : z₀ ∈ U
hfg : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = g z
z : 𝕜
h : f z = g z
⊢ (f - g) z = 0

Tactic:
by

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
f g : 𝕜 → E
z₀ : 𝕜
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
h₀ : z₀ ∈ U
hfg : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = g z
⊢ EqOn f g U

Tactic:
by

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
f g : 𝕜 → E
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
⊢ (∀ᶠ (x : 𝕜) in codiscreteWithin U, (f - g) x ≠ 0) → ∀ᶠ (x : 𝕜) in codiscreteWithin U, f x ≠ g x

Tactic:
by

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
⊢ ∀ᶠ (x : 𝕜) in 𝓝[≠] z, x ∈ U → f x = 0 ∨ g x = 0

Tactic:
by

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
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

Tactic:
by

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
x : 𝕜
f : 𝕜 → E
s : Set E
hfx : AnalyticAt 𝕜 f x
h₂f : ¬EventuallyConst f (𝓝 x)
hs : s ∈ 𝓝[≠] f x
⊢ ∀ᶠ (z : 𝕜) in 𝓝 x, f z ∈ insert (f x) s

Tactic:
by

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
x : 𝕜
f : 𝕜 → E
s : Set E
hfx : AnalyticAt 𝕜 f x
h₂f : ¬EventuallyConst f (𝓝 x)
hs : s ∈ 𝓝[≠] f x
⊢ f ⁻¹' s ∈ 𝓝[≠] x

Tactic:
by

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
U : Set 𝕜
s : Set E
f : 𝕜 → E
hfU : AnalyticOnNhd 𝕜 f U
h₂f : ∀ x ∈ U, ¬EventuallyConst f (𝓝 x)
hs : ∀ x ∈ f '' U, s ∪ (f '' U)ᶜ ∈ 𝓝[≠] x
x : 𝕜
hx : x ∈ U
⊢ f x ∈ f '' U

Tactic:
by

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
U : Set 𝕜
s : Set E
f : 𝕜 → E
hfU : AnalyticOnNhd 𝕜 f U
h₂f : ∀ x ∈ U, ¬EventuallyConst f (𝓝 x)
hs : s ∈ codiscreteWithin (f '' U)
⊢ f ⁻¹' s ∈ codiscreteWithin U

Tactic:
by

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

Goal state before:
pp: n : WithTop ℕ∞
𝕂 : Type u_1
inst✝⁴ : RCLike 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
f' : E' →L[𝕂] F'
x : E'
hf : ContDiffAt 𝕂 n f x
hf' : HasFDerivAt f f' x
hn : n ≠ 0
⊢ HasStrictFDerivAt f f' x

Tactic:
by

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

Goal state before:
pp: E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
p : E → FormalMultilinearSeries ℝ E F
s : Set E
x : E
hf : HasFTaylorSeriesUpToOn 1 f p (insert x s)
hs : Convex ℝ s
K : ℝ≥0
hK : ‖p x 1‖₊ < K
f' : E → E →L[ℝ] F := fun y ↦ (continuousMultilinearCurryFin1 ℝ E F) (p y 1)
hder : ∀ y ∈ s, HasFDerivWithinAt f (f' y) s y
hcont : ContinuousWithinAt f' s x
⊢ ‖f' x‖₊ < K

Tactic:
by

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

Goal state before:
pp: E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
p : E → FormalMultilinearSeries ℝ E F
s : Set E
x : E
hf : HasFTaylorSeriesUpToOn 1 f p (insert x s)
hs : Convex ℝ s
K : ℝ≥0
hK : ‖p x 1‖₊ < K
⊢ ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
by

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

Goal state before:
pp: E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
by

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

Goal state before:
pp: E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
hs : Convex ℝ s
hf : ContDiffOn ℝ 1 f s
⊢ LocallyLipschitzOn s f

Tactic:
by

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

Goal state before:
pp: 𝕂 : Type u_1
inst✝⁴ : RCLike 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
hf : ContDiff 𝕂 1 f
⊢ LocallyLipschitz f

Tactic:
by

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

Goal state before:
pp: E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
f : E → F
n : WithTop ℕ∞
hf : ContDiffOn ℝ n f s
hn : n ≠ 0
hs : Convex ℝ s
hs' : IsCompact s
⊢ ∃ K, LipschitzOnWith K f s

Tactic:
by

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

Goal state before:
pp: n : ℕ∞ω
𝕂 : Type u_1
inst✝⁴ : RCLike 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
hf : HasCompactSupport f
h'f : ContDiff 𝕂 n f
hn : n ≠ 0
⊢ ∃ C, LipschitzWith C f

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E →ᴬ[𝕜] F
L : Filter (E × E)
⊢ HasFDerivAtFilter (⇑f) f.contLinear L

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E →ᴬ[𝕜] F
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (⇑f) s x = f.contLinear

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
h : ¬DifferentiableAt 𝕜 f x
⊢ logDeriv f x = 0

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f g : 𝕜 → 𝕜'
U : Set 𝕜
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
h : f =ᶠ[codiscreteWithin U] g
⊢ logDeriv f =ᶠ[codiscreteWithin U] logDeriv g

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ logDeriv id x = 1 / x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
a : 𝕜'
⊢ (logDeriv fun x ↦ a) = 0

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f g : 𝕜 → 𝕜'
x : 𝕜
hf : f x ≠ 0
hg : g x ≠ 0
hdf : DifferentiableAt 𝕜 f x
hdg : DifferentiableAt 𝕜 g x
⊢ logDeriv (fun z ↦ f z * g z) x = logDeriv f x + logDeriv g x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f g : 𝕜 → 𝕜'
x : 𝕜
hf : f x ≠ 0
hg : g x ≠ 0
hdf : DifferentiableAt 𝕜 f x
hdg : DifferentiableAt 𝕜 g x
⊢ logDeriv (fun z ↦ f z / g z) x = logDeriv f x - logDeriv g x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
a : 𝕜'
ha : a ≠ 0
⊢ logDeriv (fun z ↦ f z * a) x = logDeriv f x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
a : 𝕜'
ha : a ≠ 0
⊢ logDeriv (fun z ↦ a * f z) x = logDeriv f x

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
⊢ DifferentiableAt 𝕜 (fun x ↦ x) x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
⊢ logDeriv (fun x ↦ x ^ n) x = ↑n / x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ logDeriv (fun x ↦ x⁻¹) x = -1 / x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜' → 𝕜'
g : 𝕜 → 𝕜'
x : 𝕜
hf : DifferentiableAt 𝕜' f (g x)
hg : DifferentiableAt 𝕜 g x
⊢ logDeriv (f ∘ g) x = logDeriv f (g x) * deriv g x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : IsRCLikeNormedField 𝕜
f g : 𝕜 → 𝕜'
s : Set 𝕜
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsc : IsPreconnected s
hgn : ∀ x ∈ s, g x ≠ 0
hfn : ∀ x ∈ s, f x ≠ 0
t : 𝕜
ht : t ∈ s
h : EqOn (logDeriv f) (logDeriv g) s
⊢ f t * (g t)⁻¹ ≠ 0

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : IsRCLikeNormedField 𝕜
f g : 𝕜 → 𝕜'
s : Set 𝕜
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsc : IsPreconnected s
hgn : ∀ x ∈ s, g x ≠ 0
hfn : ∀ x ∈ s, f x ≠ 0
t : 𝕜
ht : t ∈ s
h : EqOn (logDeriv f) (logDeriv g) s
y : 𝕜
hy : y ∈ s
⊢ EqOn (deriv (f * g⁻¹)) (deriv f * g⁻¹ - f * deriv g / g ^ 2) s

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : IsRCLikeNormedField 𝕜
f g : 𝕜 → 𝕜'
s : Set 𝕜
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsc : IsPreconnected s
hgn : ∀ x ∈ s, g x ≠ 0
hfn : ∀ x ∈ s, f x ≠ 0
t : 𝕜
ht : t ∈ s
h : EqOn (logDeriv f) (logDeriv g) s
y : 𝕜
hy : y ∈ s
hderiv : EqOn (deriv (f * g⁻¹)) (deriv f * g⁻¹ - f * deriv g / g ^ 2) s
z : 𝕜
hz : z ∈ s
⊢ (deriv f * g⁻¹ - f * deriv g / g ^ 2) z = 0 z

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : IsRCLikeNormedField 𝕜
f g : 𝕜 → 𝕜'
s : Set 𝕜
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsc : IsPreconnected s
hgn : ∀ x ∈ s, g x ≠ 0
hfn : ∀ x ∈ s, f x ≠ 0
⊢ EqOn (logDeriv f) (logDeriv g) s ↔ ∃ z, z ≠ 0 ∧ EqOn f (z • g) s

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : AnalyticAt 𝕜 f x
hfx : f x = 0
hf' : deriv f x ≠ 0
⊢ Tendsto (fun w ↦ (w - x) * logDeriv f w) (𝓝[≠] x) (𝓝 1)

Tactic:
by

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

Goal state before:
pp: f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
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, f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x ↦ (f x, B x)) (Icc a b)
⊢ IsClosed s

Tactic:
by

Goal state after: