Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno

Goal state before:
pp: 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✝

pp: 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

pp: 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

pp: 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

Tactic:
<;>

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