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

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
x : 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
u : 𝕜 → F
u' : F
hc : HasDerivAt c c' x
hu : HasDerivAt u u' x
⊢ HasDerivAt (fun y ↦ (c y) (u y)) (c' (u x) + (c x) u') x

Tactic:
simpa using

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
x : 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
u : 𝕜 → F
u' : F
hc : HasDerivAt c c' x
hu : HasDerivAt u u' x
⊢ HasDerivAt (fun y ↦ (c y) (u y)) (c' (u x) + (c x) u') x
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 ι
f : ContinuousMultilinearMap 𝕜 E F
inst✝² : DecidableEq ι
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : (i : ι) → G → E i
g' : (i : ι) → G →L[𝕜] E i
s : Set G
x : G
hg : ∀ (i : ι), HasFDerivWithinAt (g i) (g' i) s x
⊢ HasFDerivWithinAt (fun x ↦ f fun i ↦ g i x) (∑ i, f.toContinuousLinearMap (fun j ↦ g j x) i ∘SL g' i) s x

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
inst✝² : DecidableEq ι
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : (i : ι) → G → E i
g' : (i : ι) → G →L[𝕜] E i
s : Set G
x : G
hg : ∀ (i : ι), HasFDerivWithinAt (g i) (g' i) s x
⊢ HasFDerivWithinAt (fun x ↦ f fun i ↦ g i x) (∑ i, f.toContinuousLinearMap (fun j ↦ g j x) i ∘SL g' i) s x
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 ι
f : ContinuousMultilinearMap 𝕜 E F
inst✝² : DecidableEq ι
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : (i : ι) → G → E i
g' : (i : ι) → G →L[𝕜] E i
x : G
hg : ∀ (i : ι), HasFDerivAt (g i) (g' i) x
⊢ HasFDerivAt (fun x ↦ f fun i ↦ g i x) (∑ i, f.toContinuousLinearMap (fun j ↦ g j x) i ∘SL g' i) x

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
inst✝² : DecidableEq ι
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : (i : ι) → G → E i
g' : (i : ι) → G →L[𝕜] E i
x : G
hg : ∀ (i : ι), HasFDerivAt (g i) (g' i) x
⊢ HasFDerivAt (fun x ↦ f fun i ↦ g i x) (∑ i, f.toContinuousLinearMap (fun j ↦ g j x) i ∘SL g' i) x
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module k E
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : PartialOrder E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : PosSMulMono k E
f : k → E
x y : k
hxy : x ≤ y
⊢ slope f x y ≤ 0 ↔ f y ≤ f x

Tactic:
simpa using

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module k E
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : PartialOrder E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : PosSMulMono k E
f : k → E
x y : k
hxy : x ≤ y
⊢ slope f x y ≤ 0 ↔ f y ≤ f x
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module k E
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : PartialOrder E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : PosSMulMono k E
f : k → E
x y : k
s : Set k
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
⊢ slope f x y ≤ 0

Tactic:
simpa using

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module k E
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : PartialOrder E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : PosSMulMono k E
f : k → E
x y : k
s : Set k
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
⊢ slope f x y ≤ 0
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module k E
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : PartialOrder E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : PosSMulMono k E
f : k → E
x y : k
hxy : x ≤ y
⊢ slope f x y < 0 ↔ f y < f x

Tactic:
simpa using

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module k E
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : PartialOrder E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : PosSMulMono k E
f : k → E
x y : k
hxy : x ≤ y
⊢ slope f x y < 0 ↔ f y < f x
Module: Mathlib.Analysis.Analytic.Uniqueness

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p₁ p₂ : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
x : 𝕜
h₁ : HasFPowerSeriesAt f p₁ x
h₂ : HasFPowerSeriesAt f p₂ x
⊢ HasFPowerSeriesAt 0 (p₁ - p₂) x

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p₁ p₂ : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
x : 𝕜
h₁ : HasFPowerSeriesAt f p₁ x
h₂ : HasFPowerSeriesAt f p₂ x
⊢ HasFPowerSeriesAt 0 (p₁ - p₂) x
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module k E
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : PartialOrder E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : PosSMulMono k E
f : k → E
x y : k
s : Set k
hf : StrictAntiOn f s
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
⊢ slope f x y < 0

Tactic:
simpa using

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module k E
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : PartialOrder E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : PosSMulMono k E
f : k → E
x y : k
s : Set k
hf : StrictAntiOn f s
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
⊢ slope f x y < 0
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case fderiv
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x : (i : ι) → E i
⊢ (f.iteratedFDeriv n.succ x).curryLeft =
    ∑ e,
      (f.iteratedFDerivComponent e.toEquivRange).linearDeriv ((Pi.compRightL 𝕜 E Subtype.val) x) ∘SL
        Pi.compRightL 𝕜 E Subtype.val

Tactic:
ext v m

Goal state after:
case fderiv
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x v : (i : ι) → E i
m : Fin n → (i : ι) → E i
⊢ ((f.iteratedFDeriv n.succ x).curryLeft v) m =
    ((∑ e,
          (f.iteratedFDerivComponent e.toEquivRange).linearDeriv ((Pi.compRightL 𝕜 E Subtype.val) x) ∘SL
            Pi.compRightL 𝕜 E Subtype.val)
        v)
      m
Module: Mathlib.Analysis.Analytic.Uniqueness

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x | f =ᶠ[𝓝 x] 0}
main : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∩ U ⊆ u
Uu : U ⊆ u
z : E
hz : z ∈ U
⊢ f z = 0 z

Tactic:
simpa using

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
inst✝ : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x | f =ᶠ[𝓝 x] 0}
main : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∩ U ⊆ u
Uu : U ⊆ u
z : E
hz : z ∈ U
⊢ f z = 0
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 ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x v : (i : ι) → E i
m : Fin n → (i : ι) → E i
e : Fin n.succ ↪ ι
j : Fin n.succ
hkf : e j ∉ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
⊢ e j = e 0

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x v : (i : ι) → E i
m : Fin n → (i : ι) → E i
e : Fin n.succ ↪ ι
j : Fin n.succ
hkf : e j ∉ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
⊢ j = 0
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 𝕜
⊢ Tendsto (fun y ↦ slope f x y - f') (L ⊓ 𝓟 {x}ᶜ) (𝓝 0) ↔ Tendsto (slope f x) (L ⊓ 𝓟 {x}ᶜ) (𝓝 f')

Tactic:
rw [← nhds_translation_sub f', tendsto_comap_iff]

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
L : Filter 𝕜
⊢ Tendsto (fun y ↦ slope f x y - f') (L ⊓ 𝓟 {x}ᶜ) (𝓝 0) ↔ Tendsto ((fun x ↦ x - f') ∘ slope f x) (L ⊓ 𝓟 {x}ᶜ) (𝓝 0)
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin f s x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(Submodule.span 𝕜 (f '' t))

Tactic:
simpa using

Goal state after:
case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : ¬UniqueDiffWithinAt 𝕜 s x
⊢ 0 ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(Submodule.span 𝕜 (f '' t))
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
x✝ : Fin 0 → E
⊢ (iteratedFDeriv 𝕜 0 f x) x✝ = (p 0) x✝

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
x✝ : Fin 0 → E
⊢ f x = (p 0) x✝
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 : AntitoneOn g s
x : 𝕜
hx : x ∈ s
y : 𝕜
hy : y ∈ s
hxy : x ≤ y
⊢ (-g) x ≤ (-g) y

Tactic:
simpa using

Goal state after:
𝕜 : 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 : AntitoneOn g s
x : 𝕜
hx : x ∈ s
y : 𝕜
hy : y ∈ s
hxy : x ≤ y
⊢ g y ≤ g x
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 : AntitoneOn g s
this : MonotoneOn (-g) s
⊢ g' ≤ 0

Tactic:
simpa using

Goal state after:
𝕜 : 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 : AntitoneOn g s
this : MonotoneOn (-g) s
⊢ g' ≤ 0
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
g : 𝕜 → 𝕜
hg : AntitoneOn g s
⊢ derivWithin g s x ≤ 0

Tactic:
simpa using

Goal state after:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
g : 𝕜 → 𝕜
hg : AntitoneOn g s
⊢ derivWithin g s x ≤ 0
Module: Mathlib.Analysis.Calculus.DSlope

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : ContinuousWithinAt (dslope f a) s b
this : ContinuousWithinAt (fun x ↦ (x - a) • dslope f a x + f a) s b
⊢ ContinuousWithinAt f s b

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : ContinuousWithinAt (dslope f a) s b
this : ContinuousWithinAt (fun x ↦ (x - a) • dslope f a x + f a) s b
⊢ ContinuousWithinAt f s b
Module: Mathlib.Analysis.Calculus.DSlope

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
⊢ ContinuousWithinAt (dslope f a) s b ↔ ContinuousWithinAt f s b

Tactic:
refine ⟨ContinuousWithinAt.of_dslope, fun hc => ?_⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hc : ContinuousWithinAt f s b
⊢ ContinuousWithinAt (dslope f a) s b
Module: Mathlib.Analysis.Calculus.DSlope

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : DifferentiableWithinAt 𝕜 (dslope f a) s b
⊢ DifferentiableWithinAt 𝕜 f s b

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : DifferentiableWithinAt 𝕜 (dslope f a) s b
⊢ DifferentiableWithinAt 𝕜 f s b
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap

Goal state before:
pp: c : ℂ
R : ℝ
hR : 0 ≤ R
θ : ℝ
⊢ circleMap c R θ ∈ sphere c R

Tactic:
simpa using

Goal state after:
c : ℂ
R : ℝ
hR : 0 ≤ R
θ : ℝ
⊢ circleMap c R θ ∈ sphere c R
Module: Mathlib.Analysis.Calculus.FDeriv.Mul

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst✝³ : NormedCommRing 𝔸'
inst✝² : NormedAlgebra 𝕜 𝔸'
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
u : Multiset ι
x : ι → 𝔸'
this : Fintype ι
l : List ι
⊢ HasStrictFDerivAt (fun x ↦ (Multiset.map x ⟦l⟧).prod)
    (Multiset.map (fun i ↦ (Multiset.map x (Multiset.erase ⟦l⟧ i)).prod •> proj i) ⟦l⟧).sum x

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst✝³ : NormedCommRing 𝔸'
inst✝² : NormedAlgebra 𝕜 𝔸'
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
u : Multiset ι
x : ι → 𝔸'
this : Fintype ι
l : List ι
⊢ HasStrictFDerivAt (fun x ↦ (List.map x l).prod) (List.map (fun i ↦ (List.map x (l.erase i)).prod •> proj i) l).sum x
Module: Mathlib.Analysis.Analytic.IsolatedZeros

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : z = 0
⊢ HasSum (fun m ↦ z ^ m • a m) 0

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : z = 0
⊢ HasSum (fun m ↦ 0 ^ m • a m) 0
Module: Mathlib.Analysis.Analytic.IsolatedZeros

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : z = 0
this : s = 0
⊢ HasSum (fun m ↦ z ^ m • a (m + n)) (a n)

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : z = 0
this : s = 0
⊢ HasSum (fun m ↦ 0 ^ m • a (m + n)) (a n)
Module: Mathlib.Analysis.Analytic.IsolatedZeros

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
h1 : ∑ i ∈ Finset.range n, z ^ i • a i = 0
⊢ HasSum (fun m ↦ z ^ (m + n) • a (m + n)) s

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
h1 : ∑ i ∈ Finset.range n, z ^ i • a i = 0
⊢ HasSum (fun m ↦ z ^ (m + n) • a (m + n)) s
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₀ : 𝕜
hpd : deriv f z₀ = p.coeff 1
hp0 : p.coeff 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n ↦ z ^ n • p.coeff n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n ↦ x ^ n • p.coeff n) (f (z₀ + x))
h : ¬x = 0
hxx : ∀ (n : ℕ), x⁻¹ * x ^ (n + 1) = x ^ n
this : HasSum (fun n ↦ x⁻¹ • x ^ (n + 1) • p.coeff (n + 1)) (x⁻¹ • (f (z₀ + x) - f z₀))
⊢ HasSum (fun n ↦ x ^ n • p.coeff (n + 1)) (dslope f z₀ (z₀ + x))

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hpd : deriv f z₀ = p.coeff 1
hp0 : p.coeff 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n ↦ z ^ n • p.coeff n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n ↦ x ^ n • p.coeff n) (f (z₀ + x))
h : ¬x = 0
hxx : ∀ (n : ℕ), x⁻¹ * x ^ (n + 1) = x ^ n
this : HasSum (fun n ↦ x⁻¹ • x ^ (n + 1) • p.coeff (n + 1)) (x⁻¹ • (f (z₀ + x) - f z₀))
⊢ HasSum (fun n ↦ x ^ n • p.coeff (n + 1)) (x⁻¹ • (f (z₀ + x) - f z₀))
Module: Mathlib.Analysis.Calculus.Deriv.Comp

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
L : Filter (𝕜 × 𝕜)
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
L' : Filter (𝕜' × 𝕜')
hg : HasDerivAtFilter g₁ g₁' L'
hh : HasDerivAtFilter h h' L
hL : Tendsto (Prod.map h h) L L'
⊢ HasDerivAtFilter (g₁ ∘ h) (h' • g₁') L

Tactic:
simpa using

Goal state after:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
L : Filter (𝕜 × 𝕜)
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
L' : Filter (𝕜' × 𝕜')
hg : HasDerivAtFilter g₁ g₁' L'
hh : HasDerivAtFilter h h' L
hL : Tendsto (Prod.map h h) L L'
⊢ HasDerivAtFilter (g₁ ∘ h) (h' • g₁') L
Module: Mathlib.Analysis.Analytic.IsolatedZeros

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hpd : deriv f z₀ = p.coeff 1
hp0 : p.coeff 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n ↦ z ^ n • p.coeff n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n ↦ x ^ n • p.coeff n) (f (z₀ + x))
h : ¬x = 0
hxx : ∀ (n : ℕ), x⁻¹ * x ^ (n + 1) = x ^ n
⊢ HasSum (fun n ↦ x⁻¹ • x ^ (n + 1) • p.coeff (n + 1)) (x⁻¹ • (f (z₀ + x) - f z₀))

Tactic:
simpa using

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hpd : deriv f z₀ = p.coeff 1
hp0 : p.coeff 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n ↦ z ^ n • p.coeff n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n ↦ x ^ n • p.coeff n) (f (z₀ + x))
h : ¬x = 0
hxx : ∀ (n : ℕ), x⁻¹ * x ^ (n + 1) = x ^ n
⊢ HasSum (fun n ↦ x⁻¹ • x ^ (n + 1) • p.coeff (n + 1)) (x⁻¹ • (f (z₀ + x) - f z₀))
Module: Mathlib.Analysis.Analytic.IsolatedZeros

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
z₀ : 𝕜
n : ℕ
ih :
  ∀ {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E},
    HasFPowerSeriesAt f p z₀ → HasFPowerSeriesAt ((swap dslope z₀)^[n] f) (fslope^[n] p) z₀
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
hp : HasFPowerSeriesAt f p z₀
⊢ HasFPowerSeriesAt ((swap dslope z₀)^[n + 1] f) (fslope^[n + 1] p) z₀

Tactic:
simpa using

Goal state after:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
z₀ : 𝕜
n : ℕ
ih :
  ∀ {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E},
    HasFPowerSeriesAt f p z₀ → HasFPowerSeriesAt ((swap dslope z₀)^[n] f) (fslope^[n] p) z₀
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
hp : HasFPowerSeriesAt f p z₀
⊢ HasFPowerSeriesAt ((swap dslope z₀)^[n] (swap dslope z₀ f)) (fslope^[n] p.fslope) z₀
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₀
h : p ≠ 0
⊢ (fslope^[p.order] p 0) 1 ≠ 0

Tactic:
simpa using

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₀
h : p ≠ 0
⊢ ¬p p.order = 0