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 <;> fin_cases x

Goal state after:
case e_a.e_6.«_@»._internal._hyg.0.«0»
𝕜 : 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
⊢ iteratedDerivWithin (Fin.cons 1 (Fin.cons 1 fun x ↦ 1) ((fun i ↦ i) ⟨0, ⋯⟩)) f s x = derivWithin f s x

case e_a.e_6.«_@»._internal._hyg.0.«1»
𝕜 : 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
⊢ iteratedDerivWithin (Fin.cons 1 (Fin.cons 1 fun x ↦ 1) ((fun i ↦ i) ⟨1, ⋯⟩)) f s x = derivWithin f s x

case e_a.e_6.«_@»._internal._hyg.0.«2»
𝕜 : 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
⊢ iteratedDerivWithin (Fin.cons 1 (Fin.cons 1 fun x ↦ 1) ((fun i ↦ i) ⟨2, ⋯⟩)) f s x = derivWithin f s x

case e_a.e_a.e_6.«_@»._internal._hyg.0.«0»
𝕜 : 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
⊢ iteratedDerivWithin (Fin.cons 2 (fun x ↦ 1) ((fun i ↦ i) ⟨0, ⋯⟩)) f s x =
    ![iteratedDerivWithin 2 f s x, derivWithin f s x] ((fun i ↦ i) ⟨0, ⋯⟩)

case e_a.e_a.e_6.«_@»._internal._hyg.0.«1»
𝕜 : 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
⊢ iteratedDerivWithin (Fin.cons 2 (fun x ↦ 1) ((fun i ↦ i) ⟨1, ⋯⟩)) f s x =
    ![iteratedDerivWithin 2 f s x, derivWithin f s x] ((fun i ↦ i) ⟨1, ⋯⟩)

case e_a.e_a.e_a.e_6.«_@»._internal._hyg.0.«0»
𝕜 : 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
⊢ iteratedDerivWithin (update (Fin.cons 1 fun x ↦ 1) 1 2 ((fun i ↦ i) ⟨0, ⋯⟩)) f s x =
    ![derivWithin f s x, iteratedDerivWithin 2 f s x] ((fun i ↦ i) ⟨0, ⋯⟩)

case e_a.e_a.e_a.e_6.«_@»._internal._hyg.0.«1»
𝕜 : 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
⊢ iteratedDerivWithin (update (Fin.cons 1 fun x ↦ 1) 1 2 ((fun i ↦ i) ⟨1, ⋯⟩)) f s x =
    ![derivWithin f s x, iteratedDerivWithin 2 f s x] ((fun i ↦ i) ⟨1, ⋯⟩)

case e_a.e_a.e_a.e_a.e_6.«_@»._internal._hyg.0.«0»
𝕜 : 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
⊢ iteratedDerivWithin (update (Fin.cons 1 fun x ↦ 1) 1 2 ((fun i ↦ i) ⟨0, ⋯⟩)) f s x =
    ![derivWithin f s x, iteratedDerivWithin 2 f s x] ((fun i ↦ i) ⟨0, ⋯⟩)

case e_a.e_a.e_a.e_a.e_6.«_@»._internal._hyg.0.«1»
𝕜 : 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
⊢ iteratedDerivWithin (update (Fin.cons 1 fun x ↦ 1) 1 2 ((fun i ↦ i) ⟨1, ⋯⟩)) f s x =
    ![derivWithin f s x, iteratedDerivWithin 2 f s x] ((fun i ↦ i) ⟨1, ⋯⟩)