awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
s : Set 𝕜
t : Set E
x : 𝕜
hg : ContDiffWithinAt 𝕜 2 g t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
rw :
  (∑ c : OrderedFinpartition 2,
      (iteratedFDerivWithin 𝕜 c.length g t (f x) : (a : (i : Fin c.length) → E) → F) fun (j : Fin c.length) ↦
        iteratedDerivWithin (c.partSize j) f s x) =
    HAdd.hAdd (α := F) (β := F)
      ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F) fun (x_1 : Fin 2) ↦ derivWithin f s x : F)
      ((fderivWithin 𝕜 g t (f x) : (a : E) → F) (iteratedDerivWithin 2 f s x) : F)
⊢ iteratedDerivWithin 2 (g ∘ f) s x =
    HAdd.hAdd (α := F) (β := F)
      ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F) fun (x_1 : Fin 2) ↦ derivWithin f s x : F)
      ((fderivWithin 𝕜 g t (f x) : (a : E) → F) (iteratedDerivWithin 2 f s x) : F)

Tactic:
rw [iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition hg hf ht hs hx hst le_rfl]

Premises used: le_rfl, iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
s : Set 𝕜
t : Set E
x : 𝕜
hg : ContDiffWithinAt 𝕜 2 g t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
⊢ Eq (α := (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) → ℕ) (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1)
    fun (x : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ 1

Tactic:
have : (Fin.cons 1 (fun _ ↦ 1) : Fin 2 → ℕ) = fun _ ↦ 1 :=
    funext <| Fin.forall_fin_two.mpr ⟨rfl, rfl⟩
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
x : 𝕜
hg : ContDiffAt 𝕜 2 g (f x)
hf : ContDiffAt 𝕜 2 f x
simp :
  iteratedDerivWithin 2 (g ∘ f) univ x =
    HAdd.hAdd (α := F) (β := F)
      ((iteratedFDerivWithin 𝕜 2 g univ (f x) : (a : (i : Fin 2) → E) → F) fun (x_1 : Fin 2) ↦ derivWithin f univ x : F)
      ((fderivWithin 𝕜 g univ (f x) : (a : E) → F) (iteratedDerivWithin 2 f univ x) : F)
⊢ iteratedDeriv 2 (g ∘ f) x =
    HAdd.hAdd (α := F) (β := F)
      ((iteratedFDeriv 𝕜 2 g (f x) : (a : (i : Fin 2) → E) → F) fun (x_1 : Fin 2) ↦ deriv f x : F)
      ((fderiv 𝕜 g (f x) : (a : E) → F) (iteratedDeriv 2 f x) : F)

Tactic:
simp only [← iteratedDerivWithin_univ, ← iteratedFDerivWithin_univ,
    ← derivWithin_univ, ← fderivWithin_univ]

Premises used: derivWithin_univ, fderivWithin_univ, iteratedDerivWithin_univ, iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
x : 𝕜
hg : ContDiffAt 𝕜 2 g (f x)
hf : ContDiffAt 𝕜 2 f x
⊢ iteratedDerivWithin 2 (g ∘ f) univ x =
    HAdd.hAdd (α := F) (β := F)
      ((iteratedFDerivWithin 𝕜 2 g univ (f x) : (a : (i : Fin 2) → E) → F) fun (x_1 : Fin 2) ↦ derivWithin f univ x : F)
      ((fderivWithin 𝕜 g univ (f x) : (a : E) → F) (iteratedDerivWithin 2 f univ x) : F)

Tactic:
iteratedDerivWithin_vcomp_two hg hf uniqueDiffOn_univ
    uniqueDiffOn_univ (mem_univ x) (mapsTo_univ f _)

Premises used: iteratedDerivWithin_vcomp_two, Set.mapsTo_univ, uniqueDiffOn_univ, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
x : 𝕜
hg : ContDiffAt 𝕜 2 g (f x)
hf : ContDiffAt 𝕜 2 f x
⊢ iteratedDerivWithin 2 (g ∘ f) univ x =
    HAdd.hAdd (α := F) (β := F)
      ((iteratedFDerivWithin 𝕜 2 g univ (f x) : (a : (i : Fin 2) → E) → F) fun (x_1 : Fin 2) ↦ derivWithin f univ x : F)
      ((fderivWithin 𝕜 g univ (f x) : (a : E) → F) (iteratedDerivWithin 2 f univ x) : F)

Tactic:
exact iteratedDerivWithin_vcomp_two hg hf uniqueDiffOn_univ
    uniqueDiffOn_univ (mem_univ x) (mapsTo_univ f _)

Premises used: iteratedDerivWithin_vcomp_two, Set.mapsTo_univ, uniqueDiffOn_univ, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : 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
rw :
  (∑ c : OrderedFinpartition 3,
      (iteratedFDerivWithin 𝕜 c.length g t (f x) : (a : (i : Fin c.length) → E) → F) fun (j : Fin c.length) ↦
        iteratedDerivWithin (c.partSize j) f s x) =
    HAdd.hAdd (β := F)
      (HAdd.hAdd (α := F) (β := F)
          ((iteratedFDerivWithin 𝕜 3 g t (f x) : (a : (i : Fin 3) → E) → F) fun (x_1 : Fin 3) ↦ derivWithin f s x : F)
          ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F)
              ![iteratedDerivWithin 2 f s x, derivWithin f s x] :
            F) +
        HSMul.hSMul (α := ℕ) (β := F) 2
          ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F)
              ![derivWithin f s x, iteratedDerivWithin 2 f s x] :
            F))
      ((fderivWithin 𝕜 g t (f x) : (a : E) → F) (iteratedDerivWithin 3 f s x) : F)
⊢ iteratedDerivWithin 3 (g ∘ f) s x =
    HAdd.hAdd (β := F)
      (HAdd.hAdd (α := F) (β := F)
          ((iteratedFDerivWithin 𝕜 3 g t (f x) : (a : (i : Fin 3) → E) → F) fun (x_1 : Fin 3) ↦ derivWithin f s x : F)
          ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F)
              ![iteratedDerivWithin 2 f s x, derivWithin f s x] :
            F) +
        HSMul.hSMul (α := ℕ) (β := F) 2
          ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F)
              ![derivWithin f s x, iteratedDerivWithin 2 f s x] :
            F))
      ((fderivWithin 𝕜 g t (f x) : (a : E) → F) (iteratedDerivWithin 3 f s x) : F)

Tactic:
rw [iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition hg hf ht hs hx hst le_rfl]

Premises used: le_rfl, iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : 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
j : Fin (HAdd.hAdd (α := ℕ) 2 1)
0 :
  Eq (α := ℕ)
    (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩) :
      ℕ)
    (1 : ℕ)
1 :
  Eq (α := ℕ)
    (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩) :
      ℕ)
    (1 : ℕ)
2 :
  Eq (α := ℕ)
    (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩) :
      ℕ)
    (1 : ℕ)
⊢ Eq (α := ℕ) (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) j : ℕ)
    1

Tactic:
fin_cases j
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : 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
⊢ Eq (α := ℕ)
    (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩) :
      ℕ)
    (1 : ℕ)

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : 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
⊢ Eq (α := ℕ)
    (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩) :
      ℕ)
    (1 : ℕ)

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : 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
⊢ Eq (α := ℕ)
    (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩) :
      ℕ)
    (1 : ℕ)

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : 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
⊢ ∀ (j : Fin (HAdd.hAdd (α := ℕ) 2 1)),
    Eq (α := ℕ)
      (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) j : ℕ) 1

Tactic:
have (j : _) : (Fin.cons 1 (Fin.cons 1 fun _ ↦ 1) : Fin 3 → ℕ) j = 1 := by
    fin_cases j <;> rfl
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : 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 (HAdd.hAdd (α := ℕ) 2 1)),
    Eq (α := ℕ)
      (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) j : ℕ) 1
e_a :
  ∀ (x_1 : Fin 3),
    iteratedDerivWithin
        (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) x_1) f s x =
      derivWithin f s x
⊢ Eq.{u_2 + 1} (α := (i : Fin 3) → E)
    (fun (j : Fin 3) ↦
      iteratedDerivWithin
        (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) j) f s x)
    fun (x_1 : Fin 3) ↦ derivWithin f s x

Tactic:
ext x
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : 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 (HAdd.hAdd (α := ℕ) 2 1)),
    Eq (α := ℕ)
      (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) j : ℕ) 1
e_a :
  ∀ (x_1 : Fin 2),
    iteratedDerivWithin (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 2 (fun (x : Fin 1) ↦ 1) x_1) f s x =
      ![iteratedDerivWithin 2 f s x, derivWithin f s x] x_1
⊢ (fun (j : Fin 2) ↦ iteratedDerivWithin (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 2 (fun (x : Fin 1) ↦ 1) j) f s x) =
    ![iteratedDerivWithin 2 f s x, derivWithin f s x]

Tactic:
ext x
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : 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 (HAdd.hAdd (α := ℕ) 2 1)),
    Eq (α := ℕ)
      (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) j : ℕ) 1
e_a :
  ∀ (x_1 : Fin 2),
    iteratedDerivWithin
        (update (β := fun (a : Fin 2) ↦ ℕ) (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) 1 2 x_1) f s x =
      ![derivWithin f s x, iteratedDerivWithin 2 f s x] x_1
⊢ (fun (j : Fin 2) ↦
      iteratedDerivWithin
        (update (β := fun (a : Fin 2) ↦ ℕ) (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) 1 2 j) f s x) =
    ![derivWithin f s x, iteratedDerivWithin 2 f s x]

Tactic:
ext x
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
s : Set 𝕜
t : Set E
x_1 : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x_1)
hf : ContDiffWithinAt 𝕜 3 f s x_1
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x_1 ∈ s
hst : MapsTo f s t
this :
  ∀ (j : Fin (HAdd.hAdd (α := ℕ) 2 1)),
    Eq (α := ℕ)
      (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) j : ℕ) 1
x : Fin 3
e_a :
  iteratedDerivWithin
      (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1)
        ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)))
      f s x_1 =
    derivWithin f s x_1
e_a₁ :
  iteratedDerivWithin
      (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1)
        ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)))
      f s x_1 =
    derivWithin f s x_1
e_a₂ :
  iteratedDerivWithin
      (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1)
        ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)))
      f s x_1 =
    derivWithin f s x_1
⊢ iteratedDerivWithin
      (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) x) f s x_1 =
    derivWithin f s x_1

Tactic:
fin_cases x
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
s : Set 𝕜
t : Set E
x_1 : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x_1)
hf : ContDiffWithinAt 𝕜 3 f s x_1
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x_1 ∈ s
hst : MapsTo f s t
this :
  ∀ (j : Fin (HAdd.hAdd (α := ℕ) 2 1)),
    Eq (α := ℕ)
      (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) j : ℕ) 1
x : Fin 2
e_a :
  iteratedDerivWithin
      (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 2 (fun (x : Fin 1) ↦ 1) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))) f s x_1 =
    ![iteratedDerivWithin 2 f s x_1, derivWithin f s x_1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
e_a₁ :
  iteratedDerivWithin
      (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 2 (fun (x : Fin 1) ↦ 1) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))) f s x_1 =
    ![iteratedDerivWithin 2 f s x_1, derivWithin f s x_1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ iteratedDerivWithin (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 2 (fun (x : Fin 1) ↦ 1) x) f s x_1 =
    ![iteratedDerivWithin 2 f s x_1, derivWithin f s x_1] x

Tactic:
fin_cases x
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
s : Set 𝕜
t : Set E
x_1 : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x_1)
hf : ContDiffWithinAt 𝕜 3 f s x_1
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x_1 ∈ s
hst : MapsTo f s t
this :
  ∀ (j : Fin (HAdd.hAdd (α := ℕ) 2 1)),
    Eq (α := ℕ)
      (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) j : ℕ) 1
x : Fin 2
e_a :
  iteratedDerivWithin
      (update (β := fun (a : Fin 2) ↦ ℕ) (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) 1 2
        ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)))
      f s x_1 =
    ![derivWithin f s x_1, iteratedDerivWithin 2 f s x_1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
e_a₁ :
  iteratedDerivWithin
      (update (β := fun (a : Fin 2) ↦ ℕ) (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) 1 2
        ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)))
      f s x_1 =
    ![derivWithin f s x_1, iteratedDerivWithin 2 f s x_1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ iteratedDerivWithin
      (update (β := fun (a : Fin 2) ↦ ℕ) (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) 1 2 x) f s x_1 =
    ![derivWithin f s x_1, iteratedDerivWithin 2 f s x_1] x

Tactic:
fin_cases x
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : 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 (HAdd.hAdd (α := ℕ) 2 1)),
    Eq (α := ℕ)
      (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) j : ℕ) 1
⊢ iteratedDerivWithin
      (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1)
        ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)))
      f s x =
    derivWithin f s x

Tactic:
simp [this]
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : 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 (HAdd.hAdd (α := ℕ) 2 1)),
    Eq (α := ℕ)
      (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) j : ℕ) 1
⊢ iteratedDerivWithin
      (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1)
        ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)))
      f s x =
    derivWithin f s x

Tactic:
simp [this]
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : 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 (HAdd.hAdd (α := ℕ) 2 1)),
    Eq (α := ℕ)
      (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) j : ℕ) 1
⊢ iteratedDerivWithin
      (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1)
        ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)))
      f s x =
    derivWithin f s x

Tactic:
simp [this]
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : 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 (HAdd.hAdd (α := ℕ) 2 1)),
    Eq (α := ℕ)
      (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) j : ℕ) 1
⊢ iteratedDerivWithin
      (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 2 (fun (x : Fin 1) ↦ 1) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))) f s x =
    ![iteratedDerivWithin 2 f s x, derivWithin f s x] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [this]
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : 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 (HAdd.hAdd (α := ℕ) 2 1)),
    Eq (α := ℕ)
      (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) j : ℕ) 1
⊢ iteratedDerivWithin
      (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 2 (fun (x : Fin 1) ↦ 1) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))) f s x =
    ![iteratedDerivWithin 2 f s x, derivWithin f s x] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [this]
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : 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 (HAdd.hAdd (α := ℕ) 2 1)),
    Eq (α := ℕ)
      (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) j : ℕ) 1
⊢ iteratedDerivWithin
      (update (β := fun (a : Fin 2) ↦ ℕ) (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) 1 2
        ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)))
      f s x =
    ![derivWithin f s x, iteratedDerivWithin 2 f s x] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [this]
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : 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 (HAdd.hAdd (α := ℕ) 2 1)),
    Eq (α := ℕ)
      (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) j : ℕ) 1
⊢ iteratedDerivWithin
      (update (β := fun (a : Fin 2) ↦ ℕ) (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) 1 2
        ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)))
      f s x =
    ![derivWithin f s x, iteratedDerivWithin 2 f s x] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [this]