Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
n✝ : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
𝔸 : Type u_5
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕜 𝔸
inst✝² : Module 𝔸 F
inst✝¹ : IsBoundedSMul 𝔸 F
inst✝ : IsScalarTower 𝕜 𝔸 F
n : ℕ
IH :
  ∀ {f : 𝕜 → 𝔸} {g : 𝕜 → F},
    ContDiffWithinAt 𝕜 (↑n) f s x →
      ContDiffWithinAt 𝕜 (↑n) g s x →
        iteratedDerivWithin n (f • g) s x =
          ∑ i ∈ Finset.range (n + 1), n.choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n - i) g s x
f : 𝕜 → 𝔸
g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑(n + 1)) f s x
hg : ContDiffWithinAt 𝕜 (↑(n + 1)) g s x
U : Set 𝕜
hU : U ∈ 𝓝[insert x s] x
H : ∀ y ∈ U, ContDiffWithinAt 𝕜 (↑(n + 1)) f s y ∧ ContDiffWithinAt 𝕜 (↑(n + 1)) g s y
y : 𝕜
hfy : ContDiffWithinAt 𝕜 (↑(n + 1)) f s y
hgy : ContDiffWithinAt 𝕜 (↑(n + 1)) g s y
⊢ f y • derivWithin g s y + derivWithin f s y • g y = (f • derivWithin g s + derivWithin f s • g) y

pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
n✝ : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
𝔸 : Type u_5
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕜 𝔸
inst✝² : Module 𝔸 F
inst✝¹ : IsBoundedSMul 𝔸 F
inst✝ : IsScalarTower 𝕜 𝔸 F
n : ℕ
IH :
  ∀ {f : 𝕜 → 𝔸} {g : 𝕜 → F},
    ContDiffWithinAt 𝕜 (↑n) f s x →
      ContDiffWithinAt 𝕜 (↑n) g s x →
        iteratedDerivWithin n (f • g) s x =
          ∑ i ∈ Finset.range (n + 1), n.choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n - i) g s x
f : 𝕜 → 𝔸
g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑(n + 1)) f s x
hg : ContDiffWithinAt 𝕜 (↑(n + 1)) g s x
U : Set 𝕜
hU : U ∈ 𝓝[insert x s] x
H : ∀ y ∈ U, ContDiffWithinAt 𝕜 (↑(n + 1)) f s y ∧ ContDiffWithinAt 𝕜 (↑(n + 1)) g s y
y : 𝕜
hfy : ContDiffWithinAt 𝕜 (↑(n + 1)) f s y
hgy : ContDiffWithinAt 𝕜 (↑(n + 1)) g s y
⊢ ↑(n + 1) ≠ 0

pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
n✝ : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
𝔸 : Type u_5
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕜 𝔸
inst✝² : Module 𝔸 F
inst✝¹ : IsBoundedSMul 𝔸 F
inst✝ : IsScalarTower 𝕜 𝔸 F
n : ℕ
IH :
  ∀ {f : 𝕜 → 𝔸} {g : 𝕜 → F},
    ContDiffWithinAt 𝕜 (↑n) f s x →
      ContDiffWithinAt 𝕜 (↑n) g s x →
        iteratedDerivWithin n (f • g) s x =
          ∑ i ∈ Finset.range (n + 1), n.choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n - i) g s x
f : 𝕜 → 𝔸
g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑(n + 1)) f s x
hg : ContDiffWithinAt 𝕜 (↑(n + 1)) g s x
U : Set 𝕜
hU : U ∈ 𝓝[insert x s] x
H : ∀ y ∈ U, ContDiffWithinAt 𝕜 (↑(n + 1)) f s y ∧ ContDiffWithinAt 𝕜 (↑(n + 1)) g s y
y : 𝕜
hfy : ContDiffWithinAt 𝕜 (↑(n + 1)) f s y
hgy : ContDiffWithinAt 𝕜 (↑(n + 1)) g s y
⊢ ↑(n + 1) ≠ 0

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
n✝ : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
𝔸 : Type u_5
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕜 𝔸
inst✝² : Module 𝔸 F
inst✝¹ : IsBoundedSMul 𝔸 F
inst✝ : IsScalarTower 𝕜 𝔸 F
n : ℕ
IH :
  ∀ {f : 𝕜 → 𝔸} {g : 𝕜 → F},
    ContDiffWithinAt 𝕜 (↑n) f s x →
      ContDiffWithinAt 𝕜 (↑n) g s x →
        iteratedDerivWithin n (f • g) s x =
          ∑ i ∈ Finset.range (n + 1), n.choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n - i) g s x
f : 𝕜 → 𝔸
g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑(n + 1)) f s x
hg : ContDiffWithinAt 𝕜 (↑(n + 1)) g s x
U : Set 𝕜
hU : U ∈ 𝓝[insert x s] x
H : ∀ y ∈ U, ContDiffWithinAt 𝕜 (↑(n + 1)) f s y ∧ ContDiffWithinAt 𝕜 (↑(n + 1)) g s y
y : 𝕜
hfy : ContDiffWithinAt 𝕜 (↑(n + 1)) f s y
hgy : ContDiffWithinAt 𝕜 (↑(n + 1)) g s y
⊢ f y • derivWithin g s y + derivWithin f s y • g y = (f • derivWithin g s + derivWithin f s • g) y

𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
n✝ : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
𝔸 : Type u_5
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕜 𝔸
inst✝² : Module 𝔸 F
inst✝¹ : IsBoundedSMul 𝔸 F
inst✝ : IsScalarTower 𝕜 𝔸 F
n : ℕ
IH :
  ∀ {f : 𝕜 → 𝔸} {g : 𝕜 → F},
    ContDiffWithinAt 𝕜 (↑n) f s x →
      ContDiffWithinAt 𝕜 (↑n) g s x →
        iteratedDerivWithin n (f • g) s x =
          ∑ i ∈ Finset.range (n + 1), n.choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n - i) g s x
f : 𝕜 → 𝔸
g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑(n + 1)) f s x
hg : ContDiffWithinAt 𝕜 (↑(n + 1)) g s x
U : Set 𝕜
hU : U ∈ 𝓝[insert x s] x
H : ∀ y ∈ U, ContDiffWithinAt 𝕜 (↑(n + 1)) f s y ∧ ContDiffWithinAt 𝕜 (↑(n + 1)) g s y
y : 𝕜
hfy : ContDiffWithinAt 𝕜 (↑(n + 1)) f s y
hgy : ContDiffWithinAt 𝕜 (↑(n + 1)) g s y
⊢ ↑(n + 1) ≠ 0

𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
n✝ : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
𝔸 : Type u_5
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕜 𝔸
inst✝² : Module 𝔸 F
inst✝¹ : IsBoundedSMul 𝔸 F
inst✝ : IsScalarTower 𝕜 𝔸 F
n : ℕ
IH :
  ∀ {f : 𝕜 → 𝔸} {g : 𝕜 → F},
    ContDiffWithinAt 𝕜 (↑n) f s x →
      ContDiffWithinAt 𝕜 (↑n) g s x →
        iteratedDerivWithin n (f • g) s x =
          ∑ i ∈ Finset.range (n + 1), n.choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n - i) g s x
f : 𝕜 → 𝔸
g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑(n + 1)) f s x
hg : ContDiffWithinAt 𝕜 (↑(n + 1)) g s x
U : Set 𝕜
hU : U ∈ 𝓝[insert x s] x
H : ∀ y ∈ U, ContDiffWithinAt 𝕜 (↑(n + 1)) f s y ∧ ContDiffWithinAt 𝕜 (↑(n + 1)) g s y
y : 𝕜
hfy : ContDiffWithinAt 𝕜 (↑(n + 1)) f s y
hgy : ContDiffWithinAt 𝕜 (↑(n + 1)) g s y
⊢ ↑(n + 1) ≠ 0