mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

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
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ C, ∀ (z : E), ‖z‖ ≤ C * ‖f' z‖
A : (fun z ↦ z - x) =O[𝓝[s] x] fun z ↦ f' (z - x)
this✝ : (fun z ↦ f z - f x) ~[𝓝[s] x] fun z ↦ f' (z - x)
this : ∀ᶠ (x_1 : E) in 𝓝[s] x, x_1 ∈ {x}ᶜ → f x_1 ∈ {f x}ᶜ
⊢ ∀ᶠ (a : E) in 𝓝[s] x ⊓ 𝓟 {x}ᶜ, f a ∈ {f x}ᶜ

Tactic:
eventually_inf_principal

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
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ C, ∀ (z : E), ‖z‖ ≤ C * ‖f' z‖
A : (fun z ↦ z - x) =O[𝓝[s] x] fun z ↦ f' (z - x)
this✝ : (fun z ↦ f z - f x) ~[𝓝[s] x] fun z ↦ f' (z - x)
this : ∀ᶠ (x_1 : E) in 𝓝[s] x, x_1 ∈ {x}ᶜ → f x_1 ∈ {f x}ᶜ
⊢ ∀ᶠ (x_1 : E) in 𝓝[s] x, x_1 ∈ {x}ᶜ → f x_1 ∈ {f x}ᶜ
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: case inl
𝕜 : 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
⊢ 0 • fderivWithin 𝕜 f (0 • univ) (0 • x) = 0 • fderiv 𝕜 f (0 • x)

pp: case inr
𝕜 : 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
c : 𝕜
hc : c ≠ 0
⊢ c • fderivWithin 𝕜 f (c • univ) (c • x) = c • fderiv 𝕜 f (c • x)

Tactic:
<;>

Goal state after:
case inl
𝕜 : 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
⊢ 0 • fderivWithin 𝕜 f (0 • univ) (0 • x) = 0 • fderiv 𝕜 f (0 • x)

case inr
𝕜 : 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
c : 𝕜
hc : c ≠ 0
⊢ c • fderivWithin 𝕜 f (c • univ) (c • x) = c • fderiv 𝕜 f (c • x)
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: case e'_6.e'_1.inr.inr
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : ι → E
a b : ι
heq : v a = v b
hne : a ≠ b
i : ι
hia : i ≠ a
hib : i ≠ b
⊢ (Function.update (fun x ↦ g) b dg i) (v i) =
    ((fun j ↦ (Function.update (fun x ↦ g) a dg j) (v j)) ∘ ⇑(Equiv.swap a b)) i

Tactic:
· simp [Function.update_apply, Equiv.swap_apply_of_ne_of_ne, *]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: case refine_1.refine_1
α : Type u
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ Continuous fun x ↦ dist x.1 x.2.2

pp: case refine_1.refine_2
α : Type u
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ Continuous fun x ↦ dist x.1 x.2.1

pp: case refine_1.refine_3
α : Type u
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ Continuous fun x ↦ dist x.2.1 x.2.2

Tactic:
<;>

Goal state after:
case refine_1.refine_1
α : Type u
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ Continuous fun x ↦ dist x.1 x.2.2

case refine_1.refine_2
α : Type u
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ Continuous fun x ↦ dist x.1 x.2.1

case refine_1.refine_3
α : Type u
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ Continuous fun x ↦ dist x.2.1 x.2.2
Module: Mathlib.Analysis.Normed.Module.Completion

Goal state before:
pp: case hp
𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst✝ : SeminormedRing A
⊢ IsClosed {x | ‖x.1 * x.2‖ ≤ ‖x.1‖ * ‖x.2‖}

Tactic:
apply isClosed_le

Goal state after:
case hp.hf
𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst✝ : SeminormedRing A
⊢ Continuous fun b ↦ ‖b.1 * b.2‖

case hp.hg
𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst✝ : SeminormedRing A
⊢ Continuous fun b ↦ ‖b.1‖ * ‖b.2‖
Module: Mathlib.Analysis.Normed.Module.Completion

Goal state before:
pp: case hp.hf
𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst✝ : SeminormedRing A
⊢ Continuous fun b ↦ ‖b.1 * b.2‖

pp: case hp.hg
𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst✝ : SeminormedRing A
⊢ Continuous fun b ↦ ‖b.1‖ * ‖b.2‖

Tactic:
<;>

Goal state after:
case hp.hf
𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst✝ : SeminormedRing A
⊢ Continuous fun b ↦ ‖b.1 * b.2‖

case hp.hg
𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst✝ : SeminormedRing A
⊢ Continuous fun b ↦ ‖b.1‖ * ‖b.2‖
Module: Mathlib.Analysis.Normed.Module.Completion

Goal state before:
pp: case ih
𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst✝ : SeminormedRing A
x y : A
⊢ ‖↑x * ↑y‖ ≤ ‖↑x‖ * ‖↑y‖

Tactic:
simpa only [← coe_mul, norm_coe] using norm_mul_le x y

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

Goal state before:
pp: case zero_eq
𝕜 : 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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
⊢ ∀ x ∈ ∅, (p x 0).curry0 = f x

pp: case fderivWithin
𝕜 : 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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
⊢ ∀ (m : ℕ), ↑m < n → ∀ x ∈ ∅, HasFDerivWithinAt (fun x ↦ p x m) (p x m.succ).curryLeft ∅ x

pp: case cont
𝕜 : 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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
⊢ ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x ↦ p x m) ∅

Tactic:
<;>

Goal state after:
case zero_eq
𝕜 : 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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
⊢ ∀ x ∈ ∅, (p x 0).curry0 = f x

case fderivWithin
𝕜 : 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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
⊢ ∀ (m : ℕ), ↑m < n → ∀ x ∈ ∅, HasFDerivWithinAt (fun x ↦ p x m) (p x m.succ).curryLeft ∅ x

case cont
𝕜 : 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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
⊢ ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x ↦ p x m) ∅
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

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
hs : UniqueDiffOn 𝕜 s
n : ℕ
IH :
  ∀ {x : E},
    x ∈ s →
      ∀ (m : Fin (n + 1) → E),
        (iteratedFDerivWithin 𝕜 (n + 1) f s x) m =
          ((iteratedFDerivWithin 𝕜 n (fun y ↦ fderivWithin 𝕜 f s y) s x) (init m)) (m (last n))
x : E
hx : x ∈ s
m : Fin (n + 1 + 1) → E
I : (E [×n]→L[𝕜] E →L[𝕜] F) ≃ₗᵢ[𝕜] E [×n.succ]→L[𝕜] F := (continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm
A : ∀ y ∈ s, iteratedFDerivWithin 𝕜 n.succ f s y = (⇑I ∘ iteratedFDerivWithin 𝕜 n (fun y ↦ fderivWithin 𝕜 f s y) s) y
⊢ (((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n (fun y ↦ fderivWithin 𝕜 f s y) s) s x) (m 0)) (init (tail m)))
      (tail m (last n)) =
    ((iteratedFDerivWithin 𝕜 n.succ (fun y ↦ fderivWithin 𝕜 f s y) s x) (init m)) (m (last (n + 1)))

Tactic:
rw [iteratedFDerivWithin_succ_apply_left, tail_init_eq_init_tail]

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
hs : UniqueDiffOn 𝕜 s
n : ℕ
IH :
  ∀ {x : E},
    x ∈ s →
      ∀ (m : Fin (n + 1) → E),
        (iteratedFDerivWithin 𝕜 (n + 1) f s x) m =
          ((iteratedFDerivWithin 𝕜 n (fun y ↦ fderivWithin 𝕜 f s y) s x) (init m)) (m (last n))
x : E
hx : x ∈ s
m : Fin (n + 1 + 1) → E
I : (E [×n]→L[𝕜] E →L[𝕜] F) ≃ₗᵢ[𝕜] E [×n.succ]→L[𝕜] F := (continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm
A : ∀ y ∈ s, iteratedFDerivWithin 𝕜 n.succ f s y = (⇑I ∘ iteratedFDerivWithin 𝕜 n (fun y ↦ fderivWithin 𝕜 f s y) s) y
⊢ (((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n (fun y ↦ fderivWithin 𝕜 f s y) s) s x) (m 0)) (init (tail m)))
      (tail m (last n)) =
    (((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n (fun y ↦ fderivWithin 𝕜 f s y) s) s x) (init m 0)) (init (tail m)))
      (m (last (n + 1)))
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case mp
𝕜 : 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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
⊢ HasFTaylorSeriesUpToOn n f p univ → HasFTaylorSeriesUpTo n f p

pp: case mpr
𝕜 : 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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
⊢ HasFTaylorSeriesUpTo n f p → HasFTaylorSeriesUpToOn n f p univ

Tactic:
<;>

Goal state after:
case mp
𝕜 : 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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
⊢ HasFTaylorSeriesUpToOn n f p univ → HasFTaylorSeriesUpTo n f p

case mpr
𝕜 : 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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
⊢ HasFTaylorSeriesUpTo n f p → HasFTaylorSeriesUpToOn n f p univ
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NormedDivisionRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
⊢ derivWithin (fun y ↦ v y * u) s x = derivWithin v s x * u

Tactic:
by_cases hu : u = 0

Goal state after:
case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NormedDivisionRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
hu : u = 0
⊢ derivWithin (fun y ↦ v y * u) s x = derivWithin v s x * u

case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NormedDivisionRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
hu : ¬u = 0
⊢ derivWithin (fun y ↦ v y * u) s x = derivWithin v s x * u
Module: Mathlib.Analysis.Calculus.Deriv.Polynomial

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
p : 𝕜[X]
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ deriv (fun x ↦ eval x p) x = eval x (derivative p)

Tactic:
exact p.deriv

Goal state after:
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
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
F' : Type u_3 := ⋯
e : F →L[𝕜] F' := ⋯
this : AnalyticOnNhd 𝕜 (⇑e ∘ f) U
⊢ ⇑e ∘ f =ᶠ[𝓝 z₀] 0

Tactic:
filter_upwards [hfz₀] with x hx

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
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
F' : Type u_3 := UniformSpace.Completion F
e : F →L[𝕜] F' := UniformSpace.Completion.toComplL
this : AnalyticOnNhd 𝕜 (⇑e ∘ f) U
x : E
hx : f x = 0 x
⊢ (⇑e ∘ f) x = 0 x
Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars

Goal state before:
pp: case mpr
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' E
inst✝⁴ : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
s : Set E
x : E
hf : DifferentiableWithinAt 𝕜 f s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ (∃ g', restrictScalars 𝕜 g' = fderivWithin 𝕜 f s x) → DifferentiableWithinAt 𝕜' f s x

Tactic:
· rintro ⟨f', hf'⟩
    exact ⟨f', hf.hasFDerivWithinAt.of_restrictScalars 𝕜 hf'⟩

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

Goal state before:
pp: case e'_3.e'_5
𝕜 : 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
n : ℕ
x : E
⊢ n + 1 = (card (Fin (1 + n))).choose n

Tactic:
card_fin,

Goal state after:
case e'_3.e'_5
𝕜 : 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
n : ℕ
x : E
⊢ n + 1 = (1 + n).choose n
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case zero
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
⊢ ∀ {F : Type (max u v)} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r → (0! • (p 0) fun x ↦ y) = (iteratedFDeriv 𝕜 0 f x) fun x ↦ y

pp: case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
n : ℕ
ih :
  ∀ {F : Type (max u v)} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r → (n ! • (p n) fun x ↦ y) = (iteratedFDeriv 𝕜 n f x) fun x ↦ y
⊢ ∀ {F : Type (max u v)} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r → ((n + 1)! • (p (n + 1)) fun x ↦ y) = (iteratedFDeriv 𝕜 (n + 1) f x) fun x ↦ y

Tactic:
<;>

Goal state after:
case zero
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
⊢ ∀ {F : Type (max u v)} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r → (0! • (p 0) fun x ↦ y) = (iteratedFDeriv 𝕜 0 f x) fun x ↦ y

case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
n : ℕ
ih :
  ∀ {F : Type (max u v)} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r → (n ! • (p n) fun x ↦ y) = (iteratedFDeriv 𝕜 n f x) fun x ↦ y
⊢ ∀ {F : Type (max u v)} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r → ((n + 1)! • (p (n + 1)) fun x ↦ y) = (iteratedFDeriv 𝕜 (n + 1) f x) fun x ↦ y
Module: Mathlib.Analysis.Calculus.DSlope

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
b : 𝕜
⊢ (b - b) • dslope f b b = f b - f b

pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
hne : b ≠ a
⊢ (b - a) • dslope f a b = f b - f a

Tactic:
<;>

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
b : 𝕜
⊢ (b - b) • dslope f b b = f b - f b

case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
hne : b ≠ a
⊢ (b - a) • dslope f a b = f b - f a
Module: Mathlib.Analysis.Analytic.IsolatedZeros

Goal state before:
pp: case e'_6
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a : ℕ → E
⊢ a 0 = 0 ^ 0 • a 0

pp: case convert_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a : ℕ → E
b : ℕ
h : b ≠ 0
⊢ 0 ^ b • a b = 0

Tactic:
<;>

Goal state after:
case e'_6
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a : ℕ → E
⊢ a 0 = 0 ^ 0 • a 0

case convert_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a : ℕ → E
b : ℕ
h : b ≠ 0
⊢ 0 ^ b • a b = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap

Goal state before:
pp: case left
a b R : ℝ
c : ℂ
h_R : R ≠ 0
x✝ : |a - b| ≤ 2 * π
x₁✝ : ℝ
left✝¹ : min a b < x₁✝
right✝¹ : x₁✝ ≤ max a b
x₂✝ : ℝ
left✝ : min a b < x₂✝
right✝ : x₂✝ ≤ max a b
h : circleMap c R x₁✝ = circleMap c R x₂✝
⊢ -(2 * π) < x₁✝ - x₂✝

pp: case right
a b R : ℝ
c : ℂ
h_R : R ≠ 0
x✝ : |a - b| ≤ 2 * π
x₁✝ : ℝ
left✝¹ : min a b < x₁✝
right✝¹ : x₁✝ ≤ max a b
x₂✝ : ℝ
left✝ : min a b < x₂✝
right✝ : x₂✝ ≤ max a b
h : circleMap c R x₁✝ = circleMap c R x₂✝
⊢ x₁✝ - x₂✝ < 2 * π

Tactic:
<;>

Goal state after:
case left
a b R : ℝ
c : ℂ
h_R : R ≠ 0
x✝ : |a - b| ≤ 2 * π
x₁✝ : ℝ
left✝¹ : min a b < x₁✝
right✝¹ : x₁✝ ≤ max a b
x₂✝ : ℝ
left✝ : min a b < x₂✝
right✝ : x₂✝ ≤ max a b
h : circleMap c R x₁✝ = circleMap c R x₂✝
⊢ -(2 * π) < x₁✝ - x₂✝

case right
a b R : ℝ
c : ℂ
h_R : R ≠ 0
x✝ : |a - b| ≤ 2 * π
x₁✝ : ℝ
left✝¹ : min a b < x₁✝
right✝¹ : x₁✝ ≤ max a b
x₂✝ : ℝ
left✝ : min a b < x₂✝
right✝ : x₂✝ ≤ max a b
h : circleMap c R x₁✝ = circleMap c R x₂✝
⊢ x₁✝ - x₂✝ < 2 * π
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap

Goal state before:
pp: case left
a b R : ℝ
c : ℂ
h_R : R ≠ 0
x✝ : b - a ≤ 2 * π
x₁✝ : ℝ
left✝¹ : a ≤ x₁✝
right✝¹ : x₁✝ < b
x₂✝ : ℝ
left✝ : a ≤ x₂✝
right✝ : x₂✝ < b
h : circleMap c R x₁✝ = circleMap c R x₂✝
⊢ -(2 * π) < x₁✝ - x₂✝

pp: case right
a b R : ℝ
c : ℂ
h_R : R ≠ 0
x✝ : b - a ≤ 2 * π
x₁✝ : ℝ
left✝¹ : a ≤ x₁✝
right✝¹ : x₁✝ < b
x₂✝ : ℝ
left✝ : a ≤ x₂✝
right✝ : x₂✝ < b
h : circleMap c R x₁✝ = circleMap c R x₂✝
⊢ x₁✝ - x₂✝ < 2 * π

Tactic:
<;>

Goal state after:
case left
a b R : ℝ
c : ℂ
h_R : R ≠ 0
x✝ : b - a ≤ 2 * π
x₁✝ : ℝ
left✝¹ : a ≤ x₁✝
right✝¹ : x₁✝ < b
x₂✝ : ℝ
left✝ : a ≤ x₂✝
right✝ : x₂✝ < b
h : circleMap c R x₁✝ = circleMap c R x₂✝
⊢ -(2 * π) < x₁✝ - x₂✝

case right
a b R : ℝ
c : ℂ
h_R : R ≠ 0
x✝ : b - a ≤ 2 * π
x₁✝ : ℝ
left✝¹ : a ≤ x₁✝
right✝¹ : x₁✝ < b
x₂✝ : ℝ
left✝ : a ≤ x₂✝
right✝ : x₂✝ < b
h : circleMap c R x₁✝ = circleMap c R x₂✝
⊢ x₁✝ - x₂✝ < 2 * π
Module: Mathlib.Analysis.Analytic.IsolatedZeros

Goal state before:
pp: case e'_6
𝕜 : 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
⊢ dslope f z₀ (z₀ + x) = x ^ 0 • p.coeff (0 + 1)

pp: case pos.convert_2
𝕜 : 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
⊢ ∀ (b' : ℕ), b' ≠ 0 → x ^ b' • p.coeff (b' + 1) = 0

Tactic:
<;>

Goal state after:
case e'_6
𝕜 : 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
⊢ dslope f z₀ (z₀ + x) = x ^ 0 • p.coeff (0 + 1)

case pos.convert_2
𝕜 : 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
⊢ ∀ (b' : ℕ), b' ≠ 0 → x ^ b' • p.coeff (b' + 1) = 0
Module: Mathlib.Analysis.Analytic.IsolatedZeros

Goal state before:
pp: case e'_6
𝕜 : 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
⊢ dslope f z₀ (z₀ + x) = x ^ 0 • p.coeff (0 + 1)

pp: case pos.convert_2
𝕜 : 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
b'✝ : ℕ
x✝ : b'✝ ≠ 0
⊢ x ^ b'✝ • p.coeff (b'✝ + 1) = 0

Tactic:
<;>

Goal state after:
case e'_6
𝕜 : 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
⊢ dslope f z₀ (z₀ + x) = x ^ 0 • p.coeff (0 + 1)

case pos.convert_2
𝕜 : 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
b'✝ : ℕ
x✝ : b'✝ ≠ 0
⊢ x ^ b'✝ • p.coeff (b'✝ + 1) = 0