awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
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 :
  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
⊢ HAdd.hAdd (α := F)
      ((iteratedFDerivWithin 𝕜 3 g t (f x) : (a : (i : Fin 3) → E) → F) 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 :
        F)
      (HAdd.hAdd (α := F)
        ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F) fun (j : Fin 2) ↦
            iteratedDerivWithin (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 2 (fun (x : Fin 1) ↦ 1) j) f s x :
          F)
        (HAdd.hAdd (α := F)
          ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F) 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 :
            F)
          (HAdd.hAdd (α := F) (β := F)
            ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F) 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 :
              F)
            ((fderivWithin 𝕜 g t (f x) : (a : E) → F) (iteratedDerivWithin 3 f s x) : F)))) =
    HAdd.hAdd (α := F)
      ((iteratedFDerivWithin 𝕜 3 g t (f x) : (a : (i : Fin 3) → E) → F) fun (x_1 : Fin 3) ↦ derivWithin f s x : F)
      (HAdd.hAdd (α := F)
        ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F)
            ![iteratedDerivWithin 2 f s x, derivWithin f s x] :
          F)
        (HAdd.hAdd (α := F)
          ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F)
              ![derivWithin f s x, iteratedDerivWithin 2 f s x] :
            F)
          (HAdd.hAdd (α := F) (β := F)
            ((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))))
have e_a₁ : (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: congr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
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
⊢ 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
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
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
⊢ (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]
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
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
⊢ (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]
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
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
⊢ 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
have 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, sorry⟩ : Fin 3)))
    f s x_1 =
  derivWithin f s x_1
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
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
⊢ 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
have 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, sorry⟩ : Fin 3)))
    f s x_1 =
  derivWithin f s x_1
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
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
⊢ 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
have 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, sorry⟩ : Fin 3)))
    f s x_1 =
  derivWithin f s x_1
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
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
⊢ 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
have e_a : iteratedDerivWithin
    (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 2 (fun (x : Fin 1) ↦ 1) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))) f s x_1 =
  ![iteratedDerivWithin 2 f s x_1, derivWithin f s x_1] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
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, ⋯⟩)
⊢ 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
have e_a₁ : iteratedDerivWithin
    (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 2 (fun (x : Fin 1) ↦ 1) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))) f s x_1 =
  ![iteratedDerivWithin 2 f s x_1, derivWithin f s x_1] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
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
⊢ 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
have 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, sorry⟩ : Fin 2)))
    f s x_1 =
  ![derivWithin f s x_1, iteratedDerivWithin 2 f s x_1] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
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, ⋯⟩)
⊢ 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
have 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, sorry⟩ : Fin 2)))
    f s x_1 =
  ![derivWithin f s x_1, iteratedDerivWithin 2 f s x_1] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
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 𝕜 3 g (f x)
hf : ContDiffAt 𝕜 3 f x
⊢ iteratedDeriv 3 (g ∘ f) x =
    HAdd.hAdd (β := F)
      (HAdd.hAdd (α := F) (β := F)
          ((iteratedFDeriv 𝕜 3 g (f x) : (a : (i : Fin 3) → E) → F) fun (x_1 : Fin 3) ↦ deriv f x : F)
          ((iteratedFDeriv 𝕜 2 g (f x) : (a : (i : Fin 2) → E) → F) ![iteratedDeriv 2 f x, deriv f x] : F) +
        HSMul.hSMul (α := ℕ) (β := F) 2
          ((iteratedFDeriv 𝕜 2 g (f x) : (a : (i : Fin 2) → E) → F) ![deriv f x, iteratedDeriv 2 f x] : F))
      ((fderiv 𝕜 g (f x) : (a : E) → F) (iteratedDeriv 3 f x) : F)
have simp : iteratedDerivWithin 3 (g ∘ f) univ x =
  HAdd.hAdd (β := F)
    (HAdd.hAdd (α := F) (β := F)
        ((iteratedFDerivWithin 𝕜 3 g univ (f x) : (a : (i : Fin 3) → E) → F) fun (x_1 : Fin 3) ↦ derivWithin f univ x :
          F)
        ((iteratedFDerivWithin 𝕜 2 g univ (f x) : (a : (i : Fin 2) → E) → F)
            ![iteratedDerivWithin 2 f univ x, derivWithin f univ x] :
          F) +
      HSMul.hSMul (α := ℕ) (β := F) 2
        ((iteratedFDerivWithin 𝕜 2 g univ (f x) : (a : (i : Fin 2) → E) → F)
            ![derivWithin f univ x, iteratedDerivWithin 2 f univ x] :
          F))
    ((fderivWithin 𝕜 g univ (f x) : (a : E) → F) (iteratedDerivWithin 3 f univ x) : F)
Tactic: simp only [← iteratedDerivWithin_univ, ← iteratedFDerivWithin_univ,
    ← derivWithin_univ, ← fderivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
s t : Set 𝕜
x : 𝕜
n : ℕ∞ω
i : ℕ
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
hi : (↑i : ℕ∞ω) ≤ n
⊢ iteratedDerivWithin i (g ∘ f) s x =
    ∑ c : OrderedFinpartition i,
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (∏ j : Fin c.length, iteratedDerivWithin (c.partSize j) f s x)
        (iteratedDerivWithin c.length g t (f x))
have rw : Eq.{u_2 + 1} (α := E)
  (∑ c : OrderedFinpartition i,
    (iteratedFDerivWithin 𝕜 c.length g t (f x) : (a : (i : Fin c.length) → 𝕜) → E) fun (j : Fin c.length) ↦
      iteratedDerivWithin (c.partSize j) f s x)
  (∑ c : OrderedFinpartition i,
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (∏ j : Fin c.length, iteratedDerivWithin (c.partSize j) f s x)
      (iteratedDerivWithin c.length g t (f x)))
Tactic: rw [iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition hg hf ht hs hx hst hi]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
x : 𝕜
n : ℕ∞ω
i : ℕ
hg : ContDiffAt 𝕜 n g (f x)
hf : ContDiffAt 𝕜 n f x
hi : (↑i : ℕ∞ω) ≤ n
⊢ iteratedDeriv i (g ∘ f) x =
    ∑ c : OrderedFinpartition i,
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (∏ j : Fin c.length, iteratedDeriv (c.partSize j) f x)
        (iteratedDeriv c.length g (f x))
have rw : Eq.{u_2 + 1} (α := E)
  (∑ c : OrderedFinpartition i,
    (iteratedFDeriv 𝕜 c.length g (f x) : (a : (i : Fin c.length) → 𝕜) → E) fun (j : Fin c.length) ↦
      iteratedDeriv (c.partSize j) f x)
  (∑ c : OrderedFinpartition i,
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (∏ j : Fin c.length, iteratedDeriv (c.partSize j) f x)
      (iteratedDeriv c.length g (f x)))
Tactic: rw [iteratedDeriv_vcomp_eq_sum_orderedFinpartition hg hf hi]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
s t : Set 𝕜
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
⊢ iteratedDerivWithin 2 (g ∘ f) s x =
    HPow.hPow (β := ℕ) (derivWithin f s x) 2 • iteratedDerivWithin 2 g t (f x) +
      iteratedDerivWithin 2 f s x • derivWithin g t (f x)
have rw : HAdd.hAdd (α := E) (β := E)
    ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → 𝕜) → E) fun (x_1 : Fin 2) ↦ derivWithin f s x : E)
    ((fderivWithin 𝕜 g t (f x) : (a : 𝕜) → E) (iteratedDerivWithin 2 f s x) : E) =
  HPow.hPow (β := ℕ) (derivWithin f s x) 2 • iteratedDerivWithin 2 g t (f x) +
    iteratedDerivWithin 2 f s x • derivWithin g t (f x)
Tactic: rw [iteratedDerivWithin_vcomp_two hg hf ht hs hx hst]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
x : 𝕜
hg : ContDiffAt 𝕜 2 g (f x)
hf : ContDiffAt 𝕜 2 f x
⊢ iteratedDeriv 2 (g ∘ f) x =
    HPow.hPow (β := ℕ) (deriv f x) 2 • iteratedDeriv 2 g (f x) + iteratedDeriv 2 f x • deriv g (f x)
have simp : iteratedDerivWithin 2 (g ∘ f) univ x =
  HPow.hPow (β := ℕ) (derivWithin f univ x) 2 • iteratedDerivWithin 2 g univ (f x) +
    iteratedDerivWithin 2 f univ x • derivWithin g univ (f x)
Tactic: simp only [← iteratedDerivWithin_univ, ← derivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
s t : Set 𝕜
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
⊢ iteratedDerivWithin 3 (g ∘ f) s x =
    HPow.hPow (β := ℕ) (derivWithin f s x) 3 • iteratedDerivWithin 3 g t (f x) +
        HSMul.hSMul (α := ℕ) 3 (iteratedDerivWithin 2 f s x • derivWithin f s x • iteratedDerivWithin 2 g t (f x)) +
      iteratedDerivWithin 3 f s x • derivWithin g t (f x)
have rw : HAdd.hAdd (β := E)
    (HAdd.hAdd (α := E) (β := E)
        ((iteratedFDerivWithin 𝕜 3 g t (f x) : (a : (i : Fin 3) → 𝕜) → E) fun (x_1 : Fin 3) ↦ derivWithin f s x : E)
        ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → 𝕜) → E)
            ![iteratedDerivWithin 2 f s x, derivWithin f s x] :
          E) +
      HSMul.hSMul (α := ℕ) (β := E) 2
        ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → 𝕜) → E)
            ![derivWithin f s x, iteratedDerivWithin 2 f s x] :
          E))
    ((fderivWithin 𝕜 g t (f x) : (a : 𝕜) → E) (iteratedDerivWithin 3 f s x) : E) =
  HPow.hPow (β := ℕ) (derivWithin f s x) 3 • iteratedDerivWithin 3 g t (f x) +
      HSMul.hSMul (α := ℕ) 3 (iteratedDerivWithin 2 f s x • derivWithin f s x • iteratedDerivWithin 2 g t (f x)) +
    iteratedDerivWithin 3 f s x • derivWithin g t (f x)
Tactic: rw [iteratedDerivWithin_vcomp_three hg hf ht hs hx hst]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
s t : Set 𝕜
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
⊢ HAdd.hAdd (β := E)
      (HAdd.hAdd (α := E) (β := E)
          ((iteratedFDerivWithin 𝕜 3 g t (f x) : (a : (i : Fin 3) → 𝕜) → E) fun (x_1 : Fin 3) ↦ derivWithin f s x : E)
          ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → 𝕜) → E)
              ![iteratedDerivWithin 2 f s x, derivWithin f s x] :
            E) +
        HSMul.hSMul (α := ℕ) (β := E) 2
          ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → 𝕜) → E)
              ![derivWithin f s x, iteratedDerivWithin 2 f s x] :
            E))
      ((fderivWithin 𝕜 g t (f x) : (a : 𝕜) → E) (iteratedDerivWithin 3 f s x) : E) =
    HPow.hPow (β := ℕ) (derivWithin f s x) 3 • iteratedDerivWithin 3 g t (f x) +
        HSMul.hSMul (α := ℕ) 3 (iteratedDerivWithin 2 f s x • derivWithin f s x • iteratedDerivWithin 2 g t (f x)) +
      iteratedDerivWithin 3 f s x • derivWithin g t (f x)
have simp : HPow.hPow (β := ℕ) (derivWithin f s x) 3 • iteratedDerivWithin 3 g t (f x) +
      derivWithin f s x • iteratedDerivWithin 2 f s x • iteratedDerivWithin 2 g t (f x) +
    HSMul.hSMul (α := ℕ) 2 (derivWithin f s x • iteratedDerivWithin 2 f s x • iteratedDerivWithin 2 g t (f x)) =
  HPow.hPow (β := ℕ) (derivWithin f s x) 3 • iteratedDerivWithin 3 g t (f x) +
    HSMul.hSMul (α := ℕ) 3 (derivWithin f s x • iteratedDerivWithin 2 f s x • iteratedDerivWithin 2 g t (f x))
Tactic: simp [← toSpanSingleton_derivWithin, mul_smul, smul_comm (iteratedDerivWithin 2 f s x),
        iteratedFDerivWithin_apply_eq_iteratedDerivWithin_mul_prod]