awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.VectorField
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
n : ℕ
x : E
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 2) → E → E
hω : DifferentiableAt 𝕜 ω x
hV : ∀ (i : Fin (n + 2)), DifferentiableAt 𝕜 (V i) x
simp :
  ∀ (hω : DifferentiableWithinAt 𝕜 ω Set.univ x) (hV : ∀ (i : Fin (n + 2)), DifferentiableWithinAt 𝕜 (V i) Set.univ x),
    ((extDerivWithin ω Set.univ x : (a : Fin (n + 1 + 1) → E) → F) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x) =
      HSub.hSub (α := F)
        (∑ x_1 : Fin (n + 2),
          HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑x_1 : ℕ))
            ((fderivWithin 𝕜
                    (fun (x : E) ↦
                      (ω x : (a : Fin (n + 1) → E) → F)
                        (x_1.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_2 : Fin (n + 1 + 1)) ↦ V x_2 x :
                          (i : Fin (n + 1)) → E))
                    Set.univ x :
                  (a : E) → F)
                (V x_1 x) :
              F))
        (∑ x_1 : Fin (n + 1),
          ∑ x_2 ∈ Ici x_1,
            HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) ((↑x_1 : ℕ) + (↑x_2 : ℕ)))
              ((ω x : (a : Fin (n + 1) → E) → F)
                  (Matrix.vecCons (lieBracketWithin 𝕜 (V x_1.castSucc) (V x_2.succ) Set.univ x)
                    (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) x_2
                      (x_1.castSucc.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_3 : Fin (n + 1 + 1)) ↦
                          V x_3 x :
                        (i : Fin (n + 1)) → E))) :
                F))
⊢ ((extDeriv ω x : (a : Fin (n + 1 + 1) → E) → F) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x) =
    HSub.hSub (α := F)
      (∑ i : Fin (n + 2),
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
          ((fderiv 𝕜
                  (fun (x : E) ↦
                    (ω x : (a : Fin (n + 1) → E) → F)
                      (i.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
                        (i : Fin (n + 1)) → E))
                  x :
                (a : E) → F)
              (V i x) :
            F))
      (∑ i : Fin (n + 1),
        ∑ j ∈ Ici i,
          HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ)))
            ((ω x : (a : Fin (n + 1) → E) → F)
                (Matrix.vecCons (lieBracket 𝕜 (V i.castSucc) (V j.succ) x)
                  (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) j
                    (i.castSucc.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
                      (i : Fin (n + 1)) → E))) :
              F))

Tactic:
simp only [← differentiableWithinAt_univ, ← extDerivWithin_univ, ← fderivWithin_univ,
    ← lieBracketWithin_univ] at *

Premises used: VectorField.lieBracketWithin_univ, fderivWithin_univ, extDerivWithin_univ, differentiableWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.VectorField
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
n : ℕ
x : E
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 2) → E → E
hω : DifferentiableWithinAt 𝕜 ω Set.univ x
hV : ∀ (i : Fin (n + 2)), DifferentiableWithinAt 𝕜 (V i) Set.univ x
⊢ UniqueDiffWithinAt 𝕜 Set.univ x

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.VectorField
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
n : ℕ
x : E
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 2) → E → E
hω : DifferentiableWithinAt 𝕜 ω Set.univ x
hV : ∀ (i : Fin (n + 2)), DifferentiableWithinAt 𝕜 (V i) Set.univ x
⊢ ((extDerivWithin ω Set.univ x : (a : Fin (n + 1 + 1) → E) → F) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x) =
    HSub.hSub (α := F)
      (∑ x_1 : Fin (n + 2),
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑x_1 : ℕ))
          ((fderivWithin 𝕜
                  (fun (x : E) ↦
                    (ω x : (a : Fin (n + 1) → E) → F)
                      (x_1.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_2 : Fin (n + 1 + 1)) ↦ V x_2 x :
                        (i : Fin (n + 1)) → E))
                  Set.univ x :
                (a : E) → F)
              (V x_1 x) :
            F))
      (∑ x_1 : Fin (n + 1),
        ∑ x_2 ∈ Ici x_1,
          HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) ((↑x_1 : ℕ) + (↑x_2 : ℕ)))
            ((ω x : (a : Fin (n + 1) → E) → F)
                (Matrix.vecCons (lieBracketWithin 𝕜 (V x_1.castSucc) (V x_2.succ) Set.univ x)
                  (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) x_2
                    (x_1.castSucc.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_3 : Fin (n + 1 + 1)) ↦ V x_3 x :
                      (i : Fin (n + 1)) → E))) :
              F))

Tactic:
exact extDerivWithin_apply_vectorField hω hV (by simp)

Premises used: extDerivWithin_apply_vectorField
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.VectorField
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
s : Set E
x : E
hsx : UniqueDiffWithinAt 𝕜 s x
ω : E → E [⋀^Fin 0]→L[𝕜] F
V : Fin (HAdd.hAdd (α := ℕ) 0 1) → E → E
hω : DifferentiableWithinAt 𝕜 ω s x
hV : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)), DifferentiableWithinAt 𝕜 (V i) s x
hcomm : Pairwise fun (i j : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ lieBracketWithin 𝕜 (V i) (V j) s x = 0
⊢ Eq.{u_3 + 1} (α := F)
    ((extDerivWithin ω s x : (a : Fin (0 + 1) → E) → F) fun (x_1 : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ V x_1 x : F)
    (∑ i : Fin (0 + 1),
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
          ((fderivWithin 𝕜
                  (fun (x : E) ↦
                    (ω x : (a : Fin 0 → E) → F)
                      (i.removeNth (α := fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E)
                          fun (x_1 : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ V x_1 x :
                        (i : Fin 0) → E))
                  s x :
                (a : E) → F)
              (V i x) :
            F) :
      F)

Tactic:
simp [extDerivWithin_apply, fderivWithin_continuousAlternatingMap_apply_const_apply,
      fderivWithin_continuousAlternatingMap_apply_apply, *]

Premises used: fderivWithin_continuousAlternatingMap_apply_const_apply, fderivWithin_continuousAlternatingMap_apply_apply, extDerivWithin_apply
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.VectorField
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
s : Set E
x : E
hsx : UniqueDiffWithinAt 𝕜 s x
n : ℕ
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 1 + 1) → E → E
hω : DifferentiableWithinAt 𝕜 ω s x
hV : ∀ (i : Fin (n + 1 + 1)), DifferentiableWithinAt 𝕜 (V i) s x
hcomm : Pairwise fun (i j : Fin (n + 1 + 1)) ↦ lieBracketWithin 𝕜 (V i) (V j) s x = 0
succ :
  Eq.{u_3 + 1} (α := F)
    (∑ i : Fin (n + 1),
      ∑ j ∈ Ici i,
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ)))
          ((ω x : (a : Fin (n + 1) → E) → F)
              (Matrix.vecCons (lieBracketWithin 𝕜 (V i.castSucc) (V j.succ) s x)
                (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) j
                  (i.castSucc.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
                    (i : Fin (n + 1)) → E))) :
            F))
    0
⊢ Eq.{u_3 + 1} (α := F)
    ((extDerivWithin ω s x : (a : Fin (n + 1 + 1) → E) → F) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x : F)
    (∑ i : Fin (n + 1 + 1),
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
          ((fderivWithin 𝕜
                  (fun (x : E) ↦
                    (ω x : (a : Fin (n + 1) → E) → F)
                      (i.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
                        (i : Fin (n + 1)) → E))
                  s x :
                (a : E) → F)
              (V i x) :
            F) :
      F)

Tactic:
rw [extDerivWithin_apply_vectorField hω hV hsx, sub_eq_self]

Premises used: sub_eq_self, extDerivWithin_apply_vectorField
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.VectorField
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
s : Set E
x : E
hsx : UniqueDiffWithinAt 𝕜 s x
n : ℕ
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 1 + 1) → E → E
hω : DifferentiableWithinAt 𝕜 ω s x
hV : ∀ (i : Fin (n + 1 + 1)), DifferentiableWithinAt 𝕜 (V i) s x
hcomm : Pairwise fun (i j : Fin (n + 1 + 1)) ↦ lieBracketWithin 𝕜 (V i) (V j) s x = 0
⊢ Eq.{u_3 + 1} (α := F)
    (∑ i : Fin (n + 1),
      ∑ j ∈ Ici i,
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ)))
          ((ω x : (a : Fin (n + 1) → E) → F)
              (Matrix.vecCons (lieBracketWithin 𝕜 (V i.castSucc) (V j.succ) s x)
                (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) j
                  (i.castSucc.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
                    (i : Fin (n + 1)) → E))) :
            F))
    0

Tactic:
Fintype.sum_eq_zero _ fun i ↦ sum_eq_zero fun j hj ↦ ?_

Premises used: Fintype.sum_eq_zero, Finset.sum_eq_zero
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.VectorField
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
s : Set E
x : E
hsx : UniqueDiffWithinAt 𝕜 s x
n : ℕ
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 1 + 1) → E → E
hω : DifferentiableWithinAt 𝕜 ω s x
hV : ∀ (i : Fin (n + 1 + 1)), DifferentiableWithinAt 𝕜 (V i) s x
hcomm : Pairwise fun (i j : Fin (n + 1 + 1)) ↦ lieBracketWithin 𝕜 (V i) (V j) s x = 0
succ :
  ∀ (i j : Fin (n + 1)) (hj : j ∈ Ici i),
    HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ)))
        ((ω x : (a : Fin (n + 1) → E) → F)
            (Matrix.vecCons (lieBracketWithin 𝕜 (V i.castSucc) (V j.succ) s x)
              (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) j
                (i.castSucc.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
                  (i : Fin (n + 1)) → E))) :
          F) =
      0
⊢ Eq.{u_3 + 1} (α := F)
    (∑ i : Fin (n + 1),
      ∑ j ∈ Ici i,
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ)))
          ((ω x : (a : Fin (n + 1) → E) → F)
              (Matrix.vecCons (lieBracketWithin 𝕜 (V i.castSucc) (V j.succ) s x)
                (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) j
                  (i.castSucc.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
                    (i : Fin (n + 1)) → E))) :
            F))
    0

Tactic:
refine Fintype.sum_eq_zero _ fun i ↦ sum_eq_zero fun j hj ↦ ?_

Premises used: Fintype.sum_eq_zero, Finset.sum_eq_zero
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.VectorField
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
s : Set E
x : E
hsx : UniqueDiffWithinAt 𝕜 s x
n : ℕ
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 1 + 1) → E → E
hω : DifferentiableWithinAt 𝕜 ω s x
hV : ∀ (i : Fin (n + 1 + 1)), DifferentiableWithinAt 𝕜 (V i) s x
hcomm : Pairwise fun (i j : Fin (n + 1 + 1)) ↦ lieBracketWithin 𝕜 (V i) (V j) s x = 0
i j : Fin (n + 1)
hj : j ∈ Ici i
⊢ i.castSucc < j.succ

Tactic:
simpa using hj
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.VectorField
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
s : Set E
x : E
hsx : UniqueDiffWithinAt 𝕜 s x
n : ℕ
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 1 + 1) → E → E
hω : DifferentiableWithinAt 𝕜 ω s x
hV : ∀ (i : Fin (n + 1 + 1)), DifferentiableWithinAt 𝕜 (V i) s x
hcomm : Pairwise fun (i j : Fin (n + 1 + 1)) ↦ lieBracketWithin 𝕜 (V i) (V j) s x = 0
i j : Fin (n + 1)
hj : j ∈ Ici i
succ : HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ))) 0 = 0
succ₁ :
  Eq.{u_2 + 1} (α := E)
    (Matrix.vecCons (n := n) 0
      (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) j
        (i.castSucc.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
          (i : Fin (n + 1)) → E))
      0)
    0
⊢ HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ)))
      ((ω x : (a : Fin (n + 1) → E) → F)
          (Matrix.vecCons (lieBracketWithin 𝕜 (V i.castSucc) (V j.succ) s x)
            (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) j
              (i.castSucc.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
                (i : Fin (n + 1)) → E))) :
        F) =
    0

Tactic:
rw [hcomm (ne_of_lt <| by simpa using hj), (ω x).map_coord_zero 0]

Premises used: ContinuousAlternatingMap.map_coord_zero, OfNat.ofNat, ne_of_lt
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.VectorField
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
s : Set E
x : E
hsx : UniqueDiffWithinAt 𝕜 s x
n : ℕ
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 1 + 1) → E → E
hω : DifferentiableWithinAt 𝕜 ω s x
hV : ∀ (i : Fin (n + 1 + 1)), DifferentiableWithinAt 𝕜 (V i) s x
hcomm : Pairwise fun (i j : Fin (n + 1 + 1)) ↦ lieBracketWithin 𝕜 (V i) (V j) s x = 0
i j : Fin (n + 1)
hj : j ∈ Ici i
⊢ HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ))) 0 = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.VectorField
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
s : Set E
x : E
hsx : UniqueDiffWithinAt 𝕜 s x
n : ℕ
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 1 + 1) → E → E
hω : DifferentiableWithinAt 𝕜 ω s x
hV : ∀ (i : Fin (n + 1 + 1)), DifferentiableWithinAt 𝕜 (V i) s x
hcomm : Pairwise fun (i j : Fin (n + 1 + 1)) ↦ lieBracketWithin 𝕜 (V i) (V j) s x = 0
i j : Fin (n + 1)
hj : j ∈ Ici i
⊢ Eq.{u_2 + 1} (α := E)
    (Matrix.vecCons (n := n) 0
      (Fin.removeNth.{u_2 + 1} (α := fun (i : Fin (n + 1)) ↦ E) j
        (i.castSucc.removeNth (α := fun (x : Fin (n + 1 + 1)) ↦ E) fun (x_1 : Fin (n + 1 + 1)) ↦ V x_1 x :
          (i : Fin (n + 1)) → E))
      0)
    0

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.VectorField
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
n : ℕ
x : E
ω : E → E [⋀^Fin n]→L[𝕜] F
V : Fin (n + 1) → E → E
hω : DifferentiableAt 𝕜 ω x
hV : ∀ (i : Fin (n + 1)), DifferentiableAt 𝕜 (V i) x
hcomm : Pairwise fun (i j : Fin (n + 1)) ↦ lieBracket 𝕜 (V i) (V j) x = 0
simp :
  ∀ (hω : DifferentiableWithinAt 𝕜 ω Set.univ x) (hV : ∀ (i : Fin (n + 1)), DifferentiableWithinAt 𝕜 (V i) Set.univ x)
    (hcomm : Pairwise fun (i j : Fin (n + 1)) ↦ lieBracketWithin 𝕜 (V i) (V j) Set.univ x = 0),
    Eq.{u_3 + 1} (α := F)
      ((extDerivWithin ω Set.univ x : (a : Fin (n + 1) → E) → F) fun (x_1 : Fin (n + 1)) ↦ V x_1 x : F)
      (∑ x_1 : Fin (n + 1),
          HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑x_1 : ℕ))
            ((fderivWithin 𝕜
                    (fun (x : E) ↦
                      (ω x : (a : Fin n → E) → F)
                        (x_1.removeNth (α := fun (x : Fin (n + 1)) ↦ E) fun (x_2 : Fin (n + 1)) ↦ V x_2 x :
                          (i : Fin n) → E))
                    Set.univ x :
                  (a : E) → F)
                (V x_1 x) :
              F) :
        F)
⊢ Eq.{u_3 + 1} (α := F) ((extDeriv ω x : (a : Fin (n + 1) → E) → F) fun (x_1 : Fin (n + 1)) ↦ V x_1 x : F)
    (∑ i : Fin (n + 1),
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
          ((fderiv 𝕜
                  (fun (x : E) ↦
                    (ω x : (a : Fin n → E) → F)
                      (i.removeNth (α := fun (x : Fin (n + 1)) ↦ E) fun (x_1 : Fin (n + 1)) ↦ V x_1 x :
                        (i : Fin n) → E))
                  x :
                (a : E) → F)
              (V i x) :
            F) :
      F)

Tactic:
simp only [← differentiableWithinAt_univ, ← lieBracketWithin_univ, ← extDerivWithin_univ,
    ← fderivWithin_univ] at *

Premises used: VectorField.lieBracketWithin_univ, fderivWithin_univ, extDerivWithin_univ, differentiableWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.VectorField
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
n : ℕ
x : E
ω : E → E [⋀^Fin n]→L[𝕜] F
V : Fin (n + 1) → E → E
hω : DifferentiableWithinAt 𝕜 ω Set.univ x
hV : ∀ (i : Fin (n + 1)), DifferentiableWithinAt 𝕜 (V i) Set.univ x
hcomm : Pairwise fun (i j : Fin (n + 1)) ↦ lieBracketWithin 𝕜 (V i) (V j) Set.univ x = 0
⊢ UniqueDiffWithinAt 𝕜 Set.univ x

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.DifferentialForm.VectorField
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
n : ℕ
x : E
ω : E → E [⋀^Fin n]→L[𝕜] F
V : Fin (n + 1) → E → E
hω : DifferentiableWithinAt 𝕜 ω Set.univ x
hV : ∀ (i : Fin (n + 1)), DifferentiableWithinAt 𝕜 (V i) Set.univ x
hcomm : Pairwise fun (i j : Fin (n + 1)) ↦ lieBracketWithin 𝕜 (V i) (V j) Set.univ x = 0
⊢ Eq.{u_3 + 1} (α := F)
    ((extDerivWithin ω Set.univ x : (a : Fin (n + 1) → E) → F) fun (x_1 : Fin (n + 1)) ↦ V x_1 x : F)
    (∑ x_1 : Fin (n + 1),
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑x_1 : ℕ))
          ((fderivWithin 𝕜
                  (fun (x : E) ↦
                    (ω x : (a : Fin n → E) → F)
                      (x_1.removeNth (α := fun (x : Fin (n + 1)) ↦ E) fun (x_2 : Fin (n + 1)) ↦ V x_2 x :
                        (i : Fin n) → E))
                  Set.univ x :
                (a : E) → F)
              (V x_1 x) :
            F) :
      F)

Tactic:
exact extDerivWithin_apply_vectorField_of_pairwise_commute hω hV (by simp) hcomm

Premises used: extDerivWithin_apply_vectorField_of_pairwise_commute
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
h : HasFDerivAtFilter f f' L
c : R
⊢ HasFDerivAtFilter (c • f) (c • f') L

Tactic:
(c • (1 : F →L[𝕜] F)).hasFDerivAtFilter.comp h tendsto_map

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.hasFDerivAtFilter, HasFDerivAtFilter.comp, Filter.tendsto_map, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
h : HasStrictFDerivAt f f' x
c : R
⊢ HasStrictFDerivAt (c • f) (c • f') x

Tactic:
HasFDerivAtFilter.const_smul h c

Premises used: HasFDerivAtFilter.const_smul, HasStrictFDerivAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
h : HasFDerivWithinAt f f' s x
c : R
⊢ HasFDerivWithinAt (c • f) (c • f') s x

Tactic:
HasFDerivAtFilter.const_smul h c

Premises used: HasFDerivWithinAt, HasFDerivAtFilter.const_smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
h : HasFDerivAt f f' x
c : R
⊢ HasFDerivAt (c • f) (c • f') x

Tactic:
HasFDerivAtFilter.const_smul h c

Premises used: HasFDerivAt, HasFDerivAtFilter.const_smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
h : DifferentiableWithinAt 𝕜 f s x
c : R
⊢ DifferentiableWithinAt 𝕜 (c • f) s x

Tactic:
(h.hasFDerivWithinAt.const_smul c).differentiableWithinAt

Premises used: HasFDerivWithinAt.const_smul, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
h : DifferentiableAt 𝕜 f x
c : R
⊢ DifferentiableAt 𝕜 (c • f) x

Tactic:
(h.hasFDerivAt.const_smul c).differentiableAt

Premises used: HasFDerivAt.const_smul, DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
h : DifferentiableOn 𝕜 f s
c : R
⊢ DifferentiableOn 𝕜 (c • f) s

Tactic:
fun x hx => (h x hx).const_smul c

Premises used: DifferentiableWithinAt.const_smul, DifferentiableOn
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
h : Differentiable 𝕜 f
c : R
⊢ Differentiable 𝕜 (c • f)

Tactic:
fun x => (h x).const_smul c

Premises used: Differentiable, DifferentiableAt.const_smul