Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
s : Set 𝕜
t : Set E
x : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x)
hf : ContDiffWithinAt 𝕜 3 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
this : ∀ (j : Fin (2 + 1)), Fin.cons 1 (Fin.cons 1 fun x ↦ 1) j = 1
⊢ ((iteratedFDerivWithin 𝕜 3 g t (f x)) fun j ↦ iteratedDerivWithin (Fin.cons 1 (Fin.cons 1 fun x ↦ 1) j) f s x) +
      (((iteratedFDerivWithin 𝕜 2 g t (f x)) fun j ↦ iteratedDerivWithin (Fin.cons 2 (fun x ↦ 1) j) f s x) +
        (((iteratedFDerivWithin 𝕜 2 g t (f x)) fun j ↦
            iteratedDerivWithin (update (Fin.cons 1 fun x ↦ 1) 1 2 j) f s x) +
          (((iteratedFDerivWithin 𝕜 2 g t (f x)) fun j ↦
              iteratedDerivWithin (update (Fin.cons 1 fun x ↦ 1) 1 2 j) f s x) +
            (fderivWithin 𝕜 g t (f x)) (iteratedDerivWithin 3 f s x)))) =
    ((iteratedFDerivWithin 𝕜 3 g t (f x)) fun x_1 ↦ derivWithin f s x) +
      ((iteratedFDerivWithin 𝕜 2 g t (f x)) ![iteratedDerivWithin 2 f s x, derivWithin f s x] +
        ((iteratedFDerivWithin 𝕜 2 g t (f x)) ![derivWithin f s x, iteratedDerivWithin 2 f s x] +
          ((iteratedFDerivWithin 𝕜 2 g t (f x)) ![derivWithin f s x, iteratedDerivWithin 2 f s x] +
            (fderivWithin 𝕜 g t (f x)) (iteratedDerivWithin 3 f s x))))

Tactic:
congr <;> ext x

Goal state after:
case e_a.e_6
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
s : Set 𝕜
t : Set E
x✝ : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x✝)
hf : ContDiffWithinAt 𝕜 3 f s x✝
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x✝ ∈ s
hst : MapsTo f s t
this : ∀ (j : Fin (2 + 1)), Fin.cons 1 (Fin.cons 1 fun x ↦ 1) j = 1
x : Fin 3
⊢ iteratedDerivWithin (Fin.cons 1 (Fin.cons 1 fun x ↦ 1) x) f s x✝ = derivWithin f s x✝

case e_a.e_a.e_6
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
s : Set 𝕜
t : Set E
x✝ : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x✝)
hf : ContDiffWithinAt 𝕜 3 f s x✝
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x✝ ∈ s
hst : MapsTo f s t
this : ∀ (j : Fin (2 + 1)), Fin.cons 1 (Fin.cons 1 fun x ↦ 1) j = 1
x : Fin 2
⊢ iteratedDerivWithin (Fin.cons 2 (fun x ↦ 1) x) f s x✝ = ![iteratedDerivWithin 2 f s x✝, derivWithin f s x✝] x

case e_a.e_a.e_a.e_6
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
s : Set 𝕜
t : Set E
x✝ : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x✝)
hf : ContDiffWithinAt 𝕜 3 f s x✝
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x✝ ∈ s
hst : MapsTo f s t
this : ∀ (j : Fin (2 + 1)), Fin.cons 1 (Fin.cons 1 fun x ↦ 1) j = 1
x : Fin 2
⊢ iteratedDerivWithin (update (Fin.cons 1 fun x ↦ 1) 1 2 x) f s x✝ =
    ![derivWithin f s x✝, iteratedDerivWithin 2 f s x✝] x

case e_a.e_a.e_a.e_a.e_6
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
s : Set 𝕜
t : Set E
x✝ : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x✝)
hf : ContDiffWithinAt 𝕜 3 f s x✝
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x✝ ∈ s
hst : MapsTo f s t
this : ∀ (j : Fin (2 + 1)), Fin.cons 1 (Fin.cons 1 fun x ↦ 1) j = 1
x : Fin 2
⊢ iteratedDerivWithin (update (Fin.cons 1 fun x ↦ 1) 1 2 x) f s x✝ =
    ![derivWithin f s x✝, iteratedDerivWithin 2 f s x✝] x