mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case neg
𝕜 : 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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
h :
  HasFTaylorSeriesUpToOn (↑n) f p s ∧
    (∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y n) (p x n.succ).curryLeft s x) ∧ ContinuousOn (fun x ↦ p x (n + 1)) s
m : ℕ
hm : ↑m ≤ ↑n + 1
h' : ¬m ≤ n
this : m = n + 1
⊢ ContinuousOn (fun x ↦ p x m) s

Tactic:
this

Goal state after:
case neg
𝕜 : 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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
h :
  HasFTaylorSeriesUpToOn (↑n) f p s ∧
    (∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y n) (p x n.succ).curryLeft s x) ∧ ContinuousOn (fun x ↦ p x (n + 1)) s
m : ℕ
hm : ↑m ≤ ↑n + 1
h' : ¬m ≤ n
this : m = n + 1
⊢ ContinuousOn (fun x ↦ p x (n + 1)) s
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case fderivWithin.succ
𝕜 : 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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, (p x 0).curry0 = f x
Hfderiv_zero : ∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft s x
Htaylor : HasFTaylorSeriesUpToOn (↑n) (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) s
x : E
hx : x ∈ s
m : ℕ
hm : ↑(m + 1) < ↑n.succ
A : ↑m < ↑n
this :
  HasFDerivWithinAt (⇑(continuousMultilinearCurryRightEquiv' 𝕜 m E F) ∘ fun x ↦ p x m.succ)
    ((p x).shift m.succ).curryLeft s x
⊢ HasFDerivWithinAt (fun x ↦ p x (m + 1)) (p x (m + 1).succ).curryLeft s x

Tactic:
rw [LinearIsometryEquiv.comp_hasFDerivWithinAt_iff'
            (f' := ((p x).shift m.succ).curryLeft)] at this

Goal state after:
case fderivWithin.succ
𝕜 : 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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, (p x 0).curry0 = f x
Hfderiv_zero : ∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft s x
Htaylor : HasFTaylorSeriesUpToOn (↑n) (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) s
x : E
hx : x ∈ s
m : ℕ
hm : ↑(m + 1) < ↑n.succ
A : ↑m < ↑n
this :
  HasFDerivWithinAt (fun x ↦ p x m.succ)
    (↑↑(continuousMultilinearCurryRightEquiv' 𝕜 m E F).symm ∘SL ((p x).shift m.succ).curryLeft) s x
⊢ HasFDerivWithinAt (fun x ↦ p x (m + 1)) (p x (m + 1).succ).curryLeft s x
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case succ
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝[s] x] f
ht : t ⊆ s
n : ℕ
ihn : iteratedFDerivWithin 𝕜 n f₁ t =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 n f t
this : fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f₁ t) t =ᶠ[𝓝[s] x] fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f t) t
y : E
hy : fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f₁ t) t y = fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f t) t y
⊢ iteratedFDerivWithin 𝕜 (n + 1) f₁ t y = iteratedFDerivWithin 𝕜 (n + 1) f t y

Tactic:
simp only [iteratedFDerivWithin_succ_eq_comp_left, hy, (· ∘ ·)]

Goal state after:
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
n : ℕ
a : E
⊢ iteratedFDerivWithin 𝕜 n (fun z ↦ f (a + z)) s = fun x ↦ iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)

Tactic:
induction n with
  | zero => simp [iteratedFDerivWithin]
  | succ n IH =>
    ext v
    simp [iteratedFDerivWithin_succ_eq_comp_left, IH, fderivWithin_comp_add_left]

Goal state after:
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
f : E → F
x : E
n : ℕ
m : Fin (n + 1) → E
⊢ (iteratedFDeriv 𝕜 (n + 1) f x) m = ((iteratedFDeriv 𝕜 n (fun y ↦ fderiv 𝕜 f y) x) (init m)) (m (last n))

Tactic:
rw [← iteratedFDerivWithin_univ, ← iteratedFDerivWithin_univ, ← fderivWithin_univ]

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
f : E → F
x : E
n : ℕ
m : Fin (n + 1) → E
⊢ (iteratedFDerivWithin 𝕜 (n + 1) f univ x) m =
    ((iteratedFDerivWithin 𝕜 n (fun y ↦ fderivWithin 𝕜 f univ y) univ x) (init m)) (m (last n))
Module: Mathlib.Analysis.Calculus.FDeriv.Pow

Goal state before:
pp: 𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing 𝔸
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
n : ℕ
⊢ ∑ x_1 ∈ Finset.range (n + 1), f x •> (f x ^ (n - x_1) •> f' <• f x ^ x_1) + f' <• f x ^ (n + 1) =
    ∑ x_1 ∈ Finset.range (n + 1), f x ^ (n + 1 - x_1) •> f' <• f x ^ x_1 + f' <• f x ^ (n + 1)

Tactic:
[

Goal state after:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing 𝔸
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
n : ℕ
⊢ ∑ x_1 ∈ Finset.range (n + 1), f x •> (f x ^ (n - x_1) •> f' <• f x ^ x_1) + f' <• f x ^ (n + 1) =
    ∑ x_1 ∈ Finset.range (n + 1), f x ^ (n + 1 - x_1) •> f' <• f x ^ x_1 + f' <• f x ^ (n + 1)
Module: Mathlib.Analysis.Calculus.FDeriv.Pow

Goal state before:
pp: 𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing 𝔸
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
h : HasStrictFDerivAt f f' x
n✝ n : ℕ
this :
  HasStrictFDerivAt (f * f ^ (n + 1))
    (f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• (f ^ (n + 1)) x) x
⊢ HasStrictFDerivAt (f ^ (n + 1 + 1)) (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) x

Tactic:
[

Goal state after:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing 𝔸
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
h : HasStrictFDerivAt f f' x
n✝ n : ℕ
this :
  HasStrictFDerivAt (f * f ^ (n + 1))
    (f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• (f ^ (n + 1)) x) x
⊢ HasStrictFDerivAt (f ^ (n + 1 + 1)) (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) x
Module: Mathlib.Analysis.Calculus.FDeriv.Pow

Goal state before:
pp: 𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing 𝔸
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
n✝ n : ℕ
this :
  HasFDerivWithinAt (f * f ^ (n + 1))
    (f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• (f ^ (n + 1)) x) s x
⊢ HasFDerivWithinAt (f ^ (n + 1 + 1)) (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) s
    x

Tactic:
[

Goal state after:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing 𝔸
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
n✝ n : ℕ
this :
  HasFDerivWithinAt (f * f ^ (n + 1))
    (f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• (f ^ (n + 1)) x) s x
⊢ HasFDerivWithinAt (f ^ (n + 1 + 1)) (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) s
    x
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
r : ℝ≥0∞
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinOnBall f p s x r
f' : E →L[𝕜] F
y : E
hy : ↑‖y‖₊ < r
h'y : x + y ∈ insert x s
hf' : HasFDerivWithinAt f f' (insert x s) (x + y)
hu : UniqueDiffOn 𝕜 (insert x s)
F' : Type v := UniformSpace.Completion F
a : F →L[𝕜] F' := UniformSpace.Completion.toComplL
b : (E →L[𝕜] F) →ₗᵢ[𝕜] E →L[𝕜] F' := UniformSpace.Completion.toComplₗᵢ.postcomp
this✝ : HasFPowerSeriesWithinOnBall (⇑a ∘ f) (a.compFormalMultilinearSeries p) s x r
Z :
  HasSum (fun n ↦ ((a.compFormalMultilinearSeries p).derivSeries n) fun x ↦ y)
    (fderivWithin 𝕜 (⇑a ∘ f) (insert x s) (x + y))
this : fderivWithin 𝕜 (⇑a ∘ f) (insert x s) (x + y) = a ∘SL f'
⊢ HasSum (⇑b ∘ fun n ↦ (p.derivSeries n) fun x ↦ y) (b f')

Tactic:
this

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
r : ℝ≥0∞
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinOnBall f p s x r
f' : E →L[𝕜] F
y : E
hy : ↑‖y‖₊ < r
h'y : x + y ∈ insert x s
hf' : HasFDerivWithinAt f f' (insert x s) (x + y)
hu : UniqueDiffOn 𝕜 (insert x s)
F' : Type v := UniformSpace.Completion F
a : F →L[𝕜] F' := UniformSpace.Completion.toComplL
b : (E →L[𝕜] F) →ₗᵢ[𝕜] E →L[𝕜] F' := UniformSpace.Completion.toComplₗᵢ.postcomp
this✝ : HasFPowerSeriesWithinOnBall (⇑a ∘ f) (a.compFormalMultilinearSeries p) s x r
Z : HasSum (fun n ↦ ((a.compFormalMultilinearSeries p).derivSeries n) fun x ↦ y) (a ∘SL f')
this : fderivWithin 𝕜 (⇑a ∘ f) (insert x s) (x + y) = a ∘SL f'
⊢ HasSum (⇑b ∘ fun n ↦ (p.derivSeries n) fun x ↦ y) (b f')
Module: Mathlib.Analysis.Calculus.FDeriv.Pow

Goal state before:
pp: 𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing 𝔸
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
h : HasFDerivAt f f' x
n✝ n : ℕ
this :
  HasFDerivAt (f * f ^ (n + 1))
    (f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• (f ^ (n + 1)) x) x
⊢ HasFDerivAt (f ^ (n + 1 + 1)) (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) x

Tactic:
[

Goal state after:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing 𝔸
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
h : HasFDerivAt f f' x
n✝ n : ℕ
this :
  HasFDerivAt (f * f ^ (n + 1))
    (f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• (f ^ (n + 1)) x) x
⊢ HasFDerivAt (f ^ (n + 1 + 1)) (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) x
Module: Mathlib.Analysis.Calculus.FDeriv.Pow

Goal state before:
pp: 𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
n : ℕ
⊢ ∑ i ∈ Finset.range n, MulOpposite.op (f x ^ i) • f x ^ (n.pred - i) • f' = (n • f x ^ (n - 1)) • f'

Tactic:
[

Goal state after:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
n : ℕ
⊢ ∑ i ∈ Finset.range n, MulOpposite.op (f x ^ i) • f x ^ (n.pred - i) • f' = (n • f x ^ (n - 1)) • f'
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
f : OpenPartialHomeomorph E F
a : F
i : E ≃L[𝕜] F
h0 : a ∈ f.target
h : AnalyticAt 𝕜 (↑f) (↑f.symm a)
h' : fderiv 𝕜 (↑f) (↑f.symm a) = ↑i
this : a = ↑f (↑f.symm a)
⊢ AnalyticAt 𝕜 (↑f.symm) a

Tactic:
this

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
f : OpenPartialHomeomorph E F
a : F
i : E ≃L[𝕜] F
h0 : a ∈ f.target
h : AnalyticAt 𝕜 (↑f) (↑f.symm a)
h' : fderiv 𝕜 (↑f) (↑f.symm a) = ↑i
this : a = ↑f (↑f.symm a)
⊢ AnalyticAt 𝕜 (↑f.symm) (↑f (↑f.symm a))
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
inst✝² : DecidableEq ι
𝔸' : Type u_3
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
f' : ι → 𝔸'
hf : ∀ i ∈ u, HasDerivWithinAt (f i) (f' i) s x
⊢ HasDerivWithinAt (∏ i ∈ u, f i) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) s x

Tactic:
convert! HasDerivWithinAt.fun_finsetProd hf

Goal state after:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
inst✝² : DecidableEq ι
𝔸' : Type u_3
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
f' : ι → 𝔸'
hf : ∀ i ∈ u, HasDerivWithinAt (f i) (f' i) s x
x✝ : 𝕜
⊢ (∏ i ∈ u, f i) x✝ = ∏ i ∈ u, f i x✝
Module: Mathlib.Analysis.Calculus.Deriv.Add

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
⊢ DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun x ↦ f (-x)) (-a)

Tactic:
[

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
⊢ DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun x ↦ f (-x)) (-a)
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
k l : ℕ
h : k + l ≠ Fintype.card ι
x✝¹ : { s // s.card = l }
x✝ : x✝¹ ∈ Finset.univ
⊢ f.toFormalMultilinearSeries.changeOriginSeriesTerm k l ↑x✝¹ ⋯ = 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
k l : ℕ
h : k + l ≠ Fintype.card ι
x✝¹ : { s // s.card = l }
x✝ : x✝¹ ∈ Finset.univ
⊢ f.toFormalMultilinearSeries.changeOriginSeriesTerm k l ↑x✝¹ ⋯ = 0
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case inl
𝕜 : 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 ι
this : ∀ (l : ℕ), 1 + l ≠ Fintype.card ι
⊢ (∑' (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:
case inl
𝕜 : 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 ι
this : ∀ (l : ℕ), 1 + l ≠ Fintype.card ι
⊢ (∑' (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: 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: 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.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 b c : k
hab : a = b
⊢ ((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c

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
⊢ ((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c

Tactic:
· subst hab
    rw [sub_self, zero_div, zero_smul, zero_add]
    by_cases hac : a = c
    · simp [hac]
    · rw [div_self (sub_ne_zero.2 <| Ne.symm hac), one_smul]

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
⊢ ((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b 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 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 neg.refine_1
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
hxeqy : ¬x = y
h : 0 ≤ slope f x y
⊢ f x ≤ f y

pp: case neg.refine_2
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
hxeqy : ¬x = y
h : f x ≤ f y
⊢ 0 ≤ f y -ᵥ f x

Tactic:
· have := smul_nonneg (sub_nonneg.2 hxy) h
    rwa [slope, ← mul_smul, mul_inv_cancel₀ (mt sub_eq_zero.1 (Ne.symm hxeqy)), one_smul,
      vsub_eq_sub, sub_nonneg] at this

Goal state after:
case neg.refine_2
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
hxeqy : ¬x = y
h : f x ≤ f 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
hxy : x ≤ y
⊢ 0 < slope f x y ↔ f x < f y

Tactic:
[

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
⊢ 0 < slope f x y ↔ f x < f y
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: ι : Type u_4
inst✝ : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
j : Fin (n + 1)
h'k : e j ∈ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
hj : j ≠ 0
this : e j = ((Equiv.embeddingFinSucc n ι) e).fst (j.pred hj)
⊢ (((Equiv.embeddingFinSucc n ι) e).fst.toEquivRange.symm ⟨e j, h'k⟩).succ = j

Tactic:
[

Goal state after:
ι : Type u_4
inst✝ : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
j : Fin (n + 1)
h'k : e j ∈ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
hj : j ≠ 0
this : e j = ((Equiv.embeddingFinSucc n ι) e).fst (j.pred hj)
⊢ (((Equiv.embeddingFinSucc n ι) e).fst.toEquivRange.symm ⟨e j, h'k⟩).succ = j
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: ι : Type u_4
inst✝ : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
j : Fin (n + 1)
h'k : e j ∈ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
hj : j ≠ 0
this : e j = ((Equiv.embeddingFinSucc n ι) e).fst (j.pred hj)
⊢ (((Equiv.embeddingFinSucc n ι) e).fst.toEquivRange.symm ⟨e j, h'k⟩).succ = j

Tactic:
this

Goal state after:
ι : Type u_4
inst✝ : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
j : Fin (n + 1)
h'k : e j ∈ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
hj : j ≠ 0
this : e j = ((Equiv.embeddingFinSucc n ι) e).fst (j.pred hj)
⊢ (((Equiv.embeddingFinSucc n ι) e).fst.toEquivRange.symm ⟨((Equiv.embeddingFinSucc n ι) e).fst (j.pred hj), ⋯⟩).succ =
    j