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

Goal state before:
pp: case inl.refine_2
𝕜 : 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
r : ℝ≥0∞
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x 0 r
n : ℕ
a : Fin n → E
⊢ (continuousMultilinearCurryFin1 𝕜 E F) (0 a) = 0

Tactic:
]

Goal state after:
case inl.refine_2
𝕜 : 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
r : ℝ≥0∞
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x 0 r
n : ℕ
a : Fin n → E
⊢ (continuousMultilinearCurryFin1 𝕜 E F) (0 a) = 0
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case inl.refine_2
𝕜 : 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
r : ℝ≥0∞
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x 0 r
n : ℕ
⊢ p.derivSeries n = 0

Tactic:
· apply ContinuousMultilinearMap.ext; intro a
      change (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOriginSeries 1 n a) = 0
      rw [p.changeOriginSeries_finite_of_finite h.finite 1 (Nat.zero_le _)]
      exact map_zero _

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

Goal state before:
pp: case inr
𝕜 : 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
r : ℝ≥0∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x n.pred.succ r
hn : n ≠ 0
⊢ HasFiniteFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x (n - 1) r

Tactic:
]

Goal state after:
case inr
𝕜 : 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
r : ℝ≥0∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x n.pred.succ r
hn : n ≠ 0
⊢ HasFiniteFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x (n - 1) r
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:
]

Goal state after:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
p : 𝕜[X]
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ deriv (fun x ↦ eval x p) x = eval x (derivative p)
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
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
⊢ CPolynomialOn 𝕜 (⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f) s

Tactic:
]

Goal state after:
case zero
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
⊢ CPolynomialOn 𝕜 (⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f) s
Module: Mathlib.Analysis.Calculus.Deriv.Mul

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
x : 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
d' : E →L[𝕜] F
hc : HasDerivWithinAt c c' univ x
hd : HasDerivWithinAt d d' univ x
⊢ HasDerivWithinAt (fun y ↦ c y ∘SL d y) (c' ∘SL d x + c x ∘SL d') univ x

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
d' : E →L[𝕜] F
hc : HasDerivWithinAt c c' univ x
hd : HasDerivWithinAt d d' univ x
⊢ HasDerivWithinAt (fun y ↦ c y ∘SL d y) (c' ∘SL d x + c x ∘SL d') univ x
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ
IH : CPolynomialOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ CPolynomialOn 𝕜
    (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm ∘ _root_.fderiv 𝕜 (_root_.iteratedFDeriv 𝕜 n f)) s

Tactic:
]

Goal state after:
case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ
IH : CPolynomialOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ CPolynomialOn 𝕜
    (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm ∘ _root_.fderiv 𝕜 (_root_.iteratedFDeriv 𝕜 n f)) s
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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
⊢ (∑' (n : ℕ), (f.toFormalMultilinearSeries.changeOriginSeries 1 n) fun x_1 ↦ x) (Fin.snoc 0 y) =
    ∑ i, f (Function.update x i (y i))

Tactic:
]

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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
⊢ (∑' (n : ℕ), (f.toFormalMultilinearSeries.changeOriginSeries 1 n) fun x_1 ↦ x) (Fin.snoc 0 y) =
    ∑ i, f (Function.update x i (y i))
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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : IsEmpty ι
l : ℕ
⊢ l + 1 ≠ 0

Tactic:
]

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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : IsEmpty ι
l : ℕ
⊢ l + 1 ≠ 0
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case inr
𝕜 : 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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
⊢ ((∑ s, f.toFormalMultilinearSeries.changeOriginSeriesTerm 1 (Fintype.card ι - 1) ↑s ⋯) fun x_1 ↦ x) (Fin.snoc 0 y) =
    ∑ i, f (Function.update x i (y i))

pp: case inr
𝕜 : 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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
⊢ ∀ (b' : ℕ), b' ≠ Fintype.card ι - 1 → ((f.toFormalMultilinearSeries.changeOriginSeries 1 b') fun x_1 ↦ x) = 0

Tactic:
]

Goal state after:
case inr
𝕜 : 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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
⊢ ((∑ s, f.toFormalMultilinearSeries.changeOriginSeriesTerm 1 (Fintype.card ι - 1) ↑s ⋯) fun x_1 ↦ x) (Fin.snoc 0 y) =
    ∑ i, f (Function.update x i (y i))

case inr
𝕜 : 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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
⊢ ∀ (b' : ℕ), b' ≠ Fintype.card ι - 1 → ((f.toFormalMultilinearSeries.changeOriginSeries 1 b') fun x_1 ↦ x) = 0
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case inr
𝕜 : 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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
m : ℕ
hm : ¬1 + m = Fintype.card ι
⊢ ((f.toFormalMultilinearSeries.changeOriginSeries 1 m) fun x_1 ↦ x) = 0

Tactic:
]

Goal state after:
case inr
𝕜 : 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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
m : ℕ
hm : ¬1 + m = Fintype.card ι
⊢ ((f.toFormalMultilinearSeries.changeOriginSeries 1 m) fun x_1 ↦ x) = 0
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case inr
𝕜 : 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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
m : ℕ
hm : ¬1 + m = Fintype.card ι
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case inr
𝕜 : 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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
⊢ (∑ i, ((f.toFormalMultilinearSeries.changeOriginSeriesTerm 1 (Fintype.card ι - 1) ↑i ⋯) fun x_1 ↦ x) fun x ↦ y) =
    ∑ i, f (Function.update x i (y i))

Tactic:
]

Goal state after:
case inr
𝕜 : 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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
⊢ (∑ i, ((f.toFormalMultilinearSeries.changeOriginSeriesTerm 1 (Fintype.card ι - 1) ↑i ⋯) fun x_1 ↦ x) fun x ↦ y) =
    ∑ i, f (Function.update x i (y i))
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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
x✝ : Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))
⊢ Fintype.card ι - 1 = Fintype.card ι - 1

Tactic:
]

Goal state after:
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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
s : Finset (Fin (1 + (Fintype.card ι - 1)))
hs : #s = Fintype.card ι - 1
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case inr.refine_3
𝕜 : 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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
i : ι
⊢ f (Function.update x i (y i)) =
    (domDomCongr (Fintype.equivFinOfCardEq ⋯) (f.compContinuousLinearMap ContinuousLinearMap.proj))
      (Function.update (fun x_1 ↦ x) ((Fintype.equivFinOfCardEq ⋯) i) y)

Tactic:
]

Goal state after:
case inr.refine_3
𝕜 : 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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
i : ι
⊢ f (Function.update x i (y i)) =
    (domDomCongr (Fintype.equivFinOfCardEq ⋯) (f.compContinuousLinearMap ContinuousLinearMap.proj))
      (Function.update (fun x_1 ↦ x) ((Fintype.equivFinOfCardEq ⋯) i) y)
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
x : (i : ι) → E i
inst✝ : DecidableEq ι
⊢ HasStrictFDerivAt (⇑f)
    ((continuousMultilinearCurryFin1 𝕜 ((i : ι) → E i) F) (f.toFormalMultilinearSeries.changeOrigin x 1)) x

Tactic:
]

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
x : (i : ι) → E i
inst✝ : DecidableEq ι
⊢ HasStrictFDerivAt (⇑f)
    ((continuousMultilinearCurryFin1 𝕜 ((i : ι) → E i) F) (f.toFormalMultilinearSeries.changeOrigin x 1)) x
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case e'_13
𝕜 : 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
x : (i : ι) → E i
inst✝ : DecidableEq ι
⊢ x = x

Tactic:
]

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

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : NormedSpace ℝ E
x : E
h : DiffContOnCl 𝕜 f (ball x 0)
⊢ ContinuousOn f {x}

Tactic:
]

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : NormedSpace ℝ E
x : E
h : DiffContOnCl 𝕜 f (ball x 0)
⊢ ContinuousOn f {x}
Module: Mathlib.Analysis.Calculus.DiffContOnCl

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
h : DiffContOnCl 𝕜 f (ball x r)
hr : r ≠ 0
⊢ ContinuousOn f (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r))

Tactic:
]

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
h : DiffContOnCl 𝕜 f (ball x r)
hr : r ≠ 0
⊢ ContinuousOn f (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r))
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a : k
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: case inl
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a : k
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: case inr
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
hne : a ≠ b
⊢ f b -ᵥ f a = f b -ᵥ f a

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
⊢ f b = f b

Tactic:
]

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
y : E
c : ℝ
c_pos : c > 0
t : Set E
t_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
δ : ℝ
δ_pos : δ > 0
δε : Metric.ball 0 δ ⊆ t
n : ℕ
p : E [×n + 1]→L[𝕜] F
ht : ∀ y ∈ t, ‖p fun x ↦ y‖ ≤ c * ‖‖y‖ ^ (n + 1 + 1)‖
hy : 0 < ‖y‖
ε : ℝ
ε_pos : 0 < ε
h₀ : 0 < c * ‖y‖ ^ (n.succ + 1)
k : 𝕜
k_pos : 0 < ‖k‖
k_norm : ‖k‖ < min (δ * ‖y‖⁻¹) (ε * (c * ‖y‖ ^ (n.succ + 1))⁻¹)
⊢ ‖k‖ * ‖y‖ < δ

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
y : E
c : ℝ
c_pos : c > 0
t : Set E
t_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
δ : ℝ
δ_pos : δ > 0
δε : Metric.ball 0 δ ⊆ t
n : ℕ
p : E [×n + 1]→L[𝕜] F
ht : ∀ y ∈ t, ‖p fun x ↦ y‖ ≤ c * ‖‖y‖ ^ (n + 1 + 1)‖
hy : 0 < ‖y‖
ε : ℝ
ε_pos : 0 < ε
h₀ : 0 < c * ‖y‖ ^ (n.succ + 1)
k : 𝕜
k_pos : 0 < ‖k‖
k_norm : ‖k‖ < min (δ * ‖y‖⁻¹) (ε * (c * ‖y‖ ^ (n.succ + 1))⁻¹)
⊢ ‖k‖ * ‖y‖ < δ
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
h : slope f a b = 0
⊢ f a = f a

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
⊢ (a - b)⁻¹ • (f a -ᵥ f b) = (a - b)⁻¹ • (f a -ᵥ f b)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: case pos
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a c : k
⊢ ((c - a) / (c - a)) • slope f a c = slope f a c

Tactic:
]

Goal state after:
case pos
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a c : k
⊢ ((c - a) / (c - a)) • slope f a c = slope f a c
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: case neg
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a c : k
hac : ¬a = c
⊢ slope f a c = slope f a c

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: case neg
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b c : k
hab : ¬a = b
hbc : ¬b = c
⊢ ((c - b) / (c - a)) • slope f b c + ((b - a) / (c - a)) • slope f a b = slope f a c

Tactic:
]

Goal state after:
case neg
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b c : k
hab : ¬a = b
hbc : ¬b = c
⊢ ((c - b) / (c - a)) • slope f b c + ((b - a) / (c - a)) • slope f a b = slope f a c
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: case inr
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
⊢ (lineMap (slope f b ((lineMap a b) r)) (slope f ((lineMap a b) r) a)) r = slope f b a

Tactic:
]

Goal state after:
case inr
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
⊢ (lineMap (slope f b ((lineMap a b) r)) (slope f ((lineMap a b) r) a)) r = slope f b a
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
y : E
c : ℝ
c_pos : c > 0
t : Set E
t_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
δ : ℝ
δ_pos : δ > 0
δε : Metric.ball 0 δ ⊆ t
n : ℕ
p : E [×n + 1]→L[𝕜] F
ht : ∀ y ∈ t, ‖p fun x ↦ y‖ ≤ c * ‖‖y‖ ^ (n + 1 + 1)‖
hy : 0 < ‖y‖
ε : ℝ
ε_pos : 0 < ε
h₀ : 0 < c * ‖y‖ ^ (n.succ + 1)
k : 𝕜
k_pos : 0 < ‖k‖
k_norm : ‖k‖ < min (δ * ‖y‖⁻¹) (ε * (c * ‖y‖ ^ (n.succ + 1))⁻¹)
h₁ : ‖k • y‖ < δ
h₂ : ‖p fun x ↦ k • y‖ ≤ ‖k‖ ^ n.succ * (‖k‖ * (c * ‖y‖ ^ (n.succ + 1)))
h₃ : ‖k‖ * (c * ‖y‖ ^ (n.succ + 1)) < ε
⊢ ‖k⁻¹ ^ n.succ‖ * ‖k‖ ^ n.succ * (‖k‖ * (c * ‖y‖ ^ (n.succ + 1))) =
    ‖(k⁻¹ * k) ^ n.succ‖ * (‖k‖ * (c * ‖y‖ ^ (n.succ + 1)))

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
y : E
c : ℝ
c_pos : c > 0
t : Set E
t_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
δ : ℝ
δ_pos : δ > 0
δε : Metric.ball 0 δ ⊆ t
n : ℕ
p : E [×n + 1]→L[𝕜] F
ht : ∀ y ∈ t, ‖p fun x ↦ y‖ ≤ c * ‖‖y‖ ^ (n + 1 + 1)‖
hy : 0 < ‖y‖
ε : ℝ
ε_pos : 0 < ε
h₀ : 0 < c * ‖y‖ ^ (n.succ + 1)
k : 𝕜
k_pos : 0 < ‖k‖
k_norm : ‖k‖ < min (δ * ‖y‖⁻¹) (ε * (c * ‖y‖ ^ (n.succ + 1))⁻¹)
h₁ : ‖k • y‖ < δ
h₂ : ‖p fun x ↦ k • y‖ ≤ ‖k‖ ^ n.succ * (‖k‖ * (c * ‖y‖ ^ (n.succ + 1)))
h₃ : ‖k‖ * (c * ‖y‖ ^ (n.succ + 1)) < ε
⊢ ‖k⁻¹ ^ n.succ‖ * ‖k‖ ^ n.succ * (‖k‖ * (c * ‖y‖ ^ (n.succ + 1))) =
    ‖(k⁻¹ * k) ^ n.succ‖ * (‖k‖ * (c * ‖y‖ ^ (n.succ + 1)))