awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[s] f x
hW : (MDiffAt[s] fun (x : M) ↦ ⟨x, W x⟩) x
hs : UniqueMDiffWithinAt I s x
V' : (x : E) → TangentSpace 𝓘(𝕜, E) x :=
  mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E))
W' : (x : E) → TangentSpace 𝓘(𝕜, E) x :=
  mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E))
f' : E → 𝕜 := f ∘ (↑(extChartAt I x).symm : E → M)
s' : Set E := (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
A : (x₀ : E) → TangentSpace 𝓘(𝕜, E) x₀ :=
  fun (x₀ : E) ↦
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (((fderivWithin 𝕜 f' s' x₀ : E →L[𝕜] 𝕜) : (a : E) → 𝕜) (V' x₀) : 𝕜) (W' x₀)
B : (x₀ : E) → TangentSpace 𝓘(𝕜, E) x₀ := fun (x₀ : E) ↦ f' x₀ • lieBracketWithin 𝕜 V' W' s' x₀
e_a :
  mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) A x =
    HSMul.hSMul (α := 𝕜)
      ((fromTangentSpace (f x) : (a : TangentSpace 𝓘(𝕜, 𝕜) (f x)) → 𝕜)
          (((mfderivWithin I 𝓘(𝕜, 𝕜) f s x :
                  ContinuousLinearMap.{u_1, u_1, u_3, u_1} (RingHom.id 𝕜) (TangentSpace I x)
                    (TangentSpace 𝓘(𝕜, 𝕜) (f x))) :
                (a : TangentSpace I x) → TangentSpace 𝓘(𝕜, 𝕜) (f x))
              (V x) :
            TangentSpace 𝓘(𝕜, 𝕜) (f x)) :
        𝕜)
      (W x)
e_a₁ :
  mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) B x =
    HSMul.hSMul (β := TangentSpace I x) (f x)
      (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (lieBracketWithin 𝕜 V' W' s') x)
⊢ HAdd.hAdd (α := TangentSpace I x) (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) A x)
      (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) B x) =
    HSMul.hSMul (α := 𝕜)
        ((fromTangentSpace (f x) : (a : TangentSpace 𝓘(𝕜, 𝕜) (f x)) → 𝕜)
            (((mfderivWithin I 𝓘(𝕜, 𝕜) f s x :
                    ContinuousLinearMap.{u_1, u_1, u_3, u_1} (RingHom.id 𝕜) (TangentSpace I x)
                      (TangentSpace 𝓘(𝕜, 𝕜) (f x))) :
                  (a : TangentSpace I x) → TangentSpace 𝓘(𝕜, 𝕜) (f x))
                (V x) :
              TangentSpace 𝓘(𝕜, 𝕜) (f x)) :
          𝕜)
        (W x) +
      HSMul.hSMul (β := TangentSpace I x) (f x)
        (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (lieBracketWithin 𝕜 V' W' s') x)

Tactic:
congr
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[s] f x
hW : (MDiffAt[s] fun (x : M) ↦ ⟨x, W x⟩) x
hs : UniqueMDiffWithinAt I s x
V' : (x : E) → TangentSpace 𝓘(𝕜, E) x :=
  mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E))
W' : (x : E) → TangentSpace 𝓘(𝕜, E) x :=
  mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E))
f' : E → 𝕜 := f ∘ (↑(extChartAt I x).symm : E → M)
s' : Set E := (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
A : (x₀ : E) → TangentSpace 𝓘(𝕜, E) x₀ :=
  fun (x₀ : E) ↦
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (((fderivWithin 𝕜 f' s' x₀ : E →L[𝕜] 𝕜) : (a : E) → 𝕜) (V' x₀) : 𝕜) (W' x₀)
B : (x₀ : E) → TangentSpace 𝓘(𝕜, E) x₀ := fun (x₀ : E) ↦ f' x₀ • lieBracketWithin 𝕜 V' W' s' x₀
⊢ mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) A x =
    HSMul.hSMul (α := 𝕜)
      ((fromTangentSpace (f x) : (a : TangentSpace 𝓘(𝕜, 𝕜) (f x)) → 𝕜)
          (((mfderivWithin I 𝓘(𝕜, 𝕜) f s x :
                  ContinuousLinearMap.{u_1, u_1, u_3, u_1} (RingHom.id 𝕜) (TangentSpace I x)
                    (TangentSpace 𝓘(𝕜, 𝕜) (f x))) :
                (a : TangentSpace I x) → TangentSpace 𝓘(𝕜, 𝕜) (f x))
              (V x) :
            TangentSpace 𝓘(𝕜, 𝕜) (f x)) :
        𝕜)
      (W x)

Tactic:
simpa only [A] using mpullback_mfderivWithin_apply_smul hf

Premises used: VectorField.mpullback_mfderivWithin_apply_smul
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[s] f x
hW : (MDiffAt[s] fun (x : M) ↦ ⟨x, W x⟩) x
hs : UniqueMDiffWithinAt I s x
V' : (x : E) → TangentSpace 𝓘(𝕜, E) x :=
  mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E))
W' : (x : E) → TangentSpace 𝓘(𝕜, E) x :=
  mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E))
f' : E → 𝕜 := f ∘ (↑(extChartAt I x).symm : E → M)
s' : Set E := (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
A : (x₀ : E) → TangentSpace 𝓘(𝕜, E) x₀ :=
  fun (x₀ : E) ↦
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (((fderivWithin 𝕜 f' s' x₀ : E →L[𝕜] 𝕜) : (a : E) → 𝕜) (V' x₀) : 𝕜) (W' x₀)
B : (x₀ : E) → TangentSpace 𝓘(𝕜, E) x₀ := fun (x₀ : E) ↦ f' x₀ • lieBracketWithin 𝕜 V' W' s' x₀
⊢ mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) B x =
    HSMul.hSMul (β := TangentSpace I x) (f x)
      (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (lieBracketWithin 𝕜 V' W' s') x)

Tactic:
simp [B, ← Pi.smul_def', mpullback_smul (V := lieBracketWithin 𝕜 V' W' s'), f']

Premises used: Pi.smul_def', VectorField.mpullback_smul
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
V W : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
f : M → 𝕜
hf : MDiffAt f x
hW : (MDiffAt fun (x : M) ↦ ⟨x, W x⟩) x
⊢ MDiffAt[univ] f x

Tactic:
rw [← mdifferentiableWithinAt_univ] at hf hW

Premises used: mdifferentiableWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
V W : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
f : M → 𝕜
hf : MDiffAt f x
hW : (MDiffAt fun (x : M) ↦ ⟨x, W x⟩) x
hf₁ : MDiffAt[univ] f x
⊢ (MDiffAt[univ] fun (x : M) ↦ ⟨x, W x⟩) x

Tactic:
rw [← mdifferentiableWithinAt_univ] at hf hW

Premises used: mdifferentiableWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
V W : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[univ] f x
hW : (MDiffAt[univ] fun (x : M) ↦ ⟨x, W x⟩) x
rw :
  mlieBracketWithin I V (f • W) univ x =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜)
        (((↑(fromTangentSpace (f x)) : TangentSpace 𝓘(𝕜, 𝕜) (f x) →L[𝕜] 𝕜) ∘SL mfderivWithin I 𝓘(𝕜, 𝕜) f univ x :
              (a : TangentSpace I x) → 𝕜)
            (V x) :
          𝕜)
        (W x) +
      f x • mlieBracket I V W x
⊢ mlieBracket I V (f • W) x =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) ((d% f x : (a : TangentSpace I x) → 𝕜) (V x) : 𝕜) (W x) +
      f x • mlieBracket I V W x

Tactic:
rw [← mlieBracketWithin_univ, mvfderiv, ← mfderivWithin_univ]

Premises used: mvfderiv, mfderivWithin_univ, VectorField.mlieBracketWithin_univ
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
V W : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[univ] f x
hW : (MDiffAt[univ] fun (x : M) ↦ ⟨x, W x⟩) x
⊢ mlieBracketWithin I V (f • W) univ x =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜)
        (((↑(fromTangentSpace (f x)) : TangentSpace 𝓘(𝕜, 𝕜) (f x) →L[𝕜] 𝕜) ∘SL mfderivWithin I 𝓘(𝕜, 𝕜) f univ x :
              (a : TangentSpace I x) → 𝕜)
            (V x) :
          𝕜)
        (W x) +
      f x • mlieBracket I V W x

Tactic:
mlieBracketWithin_smul_right hf hW (uniqueMDiffWithinAt_univ I)

Premises used: VectorField.mlieBracketWithin_smul_right, uniqueMDiffWithinAt_univ, VectorField.mlieBracket
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
V W : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[univ] f x
hW : (MDiffAt[univ] fun (x : M) ↦ ⟨x, W x⟩) x
⊢ mlieBracketWithin I V (f • W) univ x =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜)
        (((↑(fromTangentSpace (f x)) : TangentSpace 𝓘(𝕜, 𝕜) (f x) →L[𝕜] 𝕜) ∘SL mfderivWithin I 𝓘(𝕜, 𝕜) f univ x :
              (a : TangentSpace I x) → 𝕜)
            (V x) :
          𝕜)
        (W x) +
      f x • mlieBracket I V W x

Tactic:
exact mlieBracketWithin_smul_right hf hW (uniqueMDiffWithinAt_univ I)

Premises used: VectorField.mlieBracketWithin_smul_right, uniqueMDiffWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[s] f x
hV : (MDiffAt[s] fun (x : M) ↦ ⟨x, V x⟩) x
hs : UniqueMDiffWithinAt I s x
rw :
  -(HSMul.hSMul (α := 𝕜)
          ((fromTangentSpace (f x) : (a : TangentSpace 𝓘(𝕜, 𝕜) (f x)) → 𝕜)
              (((mfderivWithin I 𝓘(𝕜, 𝕜) f s x :
                      ContinuousLinearMap.{u_1, u_1, u_3, u_1} (RingHom.id 𝕜) (TangentSpace I x)
                        (TangentSpace 𝓘(𝕜, 𝕜) (f x))) :
                    (a : TangentSpace I x) → TangentSpace 𝓘(𝕜, 𝕜) (f x))
                  (W x) :
                TangentSpace 𝓘(𝕜, 𝕜) (f x)) :
            𝕜)
          (V x) +
        f x • (-mlieBracketWithin I V W s) x) =
    HSMul.hSMul (α := 𝕜)
        (-(fromTangentSpace (f x) : (a : TangentSpace 𝓘(𝕜, 𝕜) (f x)) → 𝕜)
              (((mfderivWithin I 𝓘(𝕜, 𝕜) f s x :
                      ContinuousLinearMap.{u_1, u_1, u_3, u_1} (RingHom.id 𝕜) (TangentSpace I x)
                        (TangentSpace 𝓘(𝕜, 𝕜) (f x))) :
                    (a : TangentSpace I x) → TangentSpace 𝓘(𝕜, 𝕜) (f x))
                  (W x) :
                TangentSpace 𝓘(𝕜, 𝕜) (f x)) :
          𝕜)
        (V x) +
      f x • mlieBracketWithin I V W s x
⊢ mlieBracketWithin I (f • V) W s x =
    HSMul.hSMul (α := 𝕜)
        (-(fromTangentSpace (f x) : (a : TangentSpace 𝓘(𝕜, 𝕜) (f x)) → 𝕜)
              (((mfderivWithin I 𝓘(𝕜, 𝕜) f s x :
                      ContinuousLinearMap.{u_1, u_1, u_3, u_1} (RingHom.id 𝕜) (TangentSpace I x)
                        (TangentSpace 𝓘(𝕜, 𝕜) (f x))) :
                    (a : TangentSpace I x) → TangentSpace 𝓘(𝕜, 𝕜) (f x))
                  (W x) :
                TangentSpace 𝓘(𝕜, 𝕜) (f x)) :
          𝕜)
        (V x) +
      f x • mlieBracketWithin I V W s x

Tactic:
rw [mlieBracketWithin_swap, Pi.neg_apply, mlieBracketWithin_smul_right hf hV (V := W) hs,
    mlieBracketWithin_swap]

Premises used: VectorField.mlieBracketWithin_smul_right, Pi.neg_apply, VectorField.mlieBracketWithin_swap
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[s] f x
hV : (MDiffAt[s] fun (x : M) ↦ ⟨x, V x⟩) x
hs : UniqueMDiffWithinAt I s x
simp :
  f x • mlieBracketWithin I V W s x +
      -HSMul.hSMul (α := 𝕜)
          ((fromTangentSpace (f x) : (a : TangentSpace 𝓘(𝕜, 𝕜) (f x)) → 𝕜)
              (((mfderivWithin I 𝓘(𝕜, 𝕜) f s x :
                      ContinuousLinearMap.{u_1, u_1, u_3, u_1} (RingHom.id 𝕜) (TangentSpace I x)
                        (TangentSpace 𝓘(𝕜, 𝕜) (f x))) :
                    (a : TangentSpace I x) → TangentSpace 𝓘(𝕜, 𝕜) (f x))
                  (W x) :
                TangentSpace 𝓘(𝕜, 𝕜) (f x)) :
            𝕜)
          (V x) =
    -HSMul.hSMul (α := 𝕜)
          ((fromTangentSpace (f x) : (a : TangentSpace 𝓘(𝕜, 𝕜) (f x)) → 𝕜)
              (((mfderivWithin I 𝓘(𝕜, 𝕜) f s x :
                      ContinuousLinearMap.{u_1, u_1, u_3, u_1} (RingHom.id 𝕜) (TangentSpace I x)
                        (TangentSpace 𝓘(𝕜, 𝕜) (f x))) :
                    (a : TangentSpace I x) → TangentSpace 𝓘(𝕜, 𝕜) (f x))
                  (W x) :
                TangentSpace 𝓘(𝕜, 𝕜) (f x)) :
            𝕜)
          (V x) +
      f x • mlieBracketWithin I V W s x
⊢ -(HSMul.hSMul (α := 𝕜)
          ((fromTangentSpace (f x) : (a : TangentSpace 𝓘(𝕜, 𝕜) (f x)) → 𝕜)
              (((mfderivWithin I 𝓘(𝕜, 𝕜) f s x :
                      ContinuousLinearMap.{u_1, u_1, u_3, u_1} (RingHom.id 𝕜) (TangentSpace I x)
                        (TangentSpace 𝓘(𝕜, 𝕜) (f x))) :
                    (a : TangentSpace I x) → TangentSpace 𝓘(𝕜, 𝕜) (f x))
                  (W x) :
                TangentSpace 𝓘(𝕜, 𝕜) (f x)) :
            𝕜)
          (V x) +
        f x • (-mlieBracketWithin I V W s) x) =
    HSMul.hSMul (α := 𝕜)
        (-(fromTangentSpace (f x) : (a : TangentSpace 𝓘(𝕜, 𝕜) (f x)) → 𝕜)
              (((mfderivWithin I 𝓘(𝕜, 𝕜) f s x :
                      ContinuousLinearMap.{u_1, u_1, u_3, u_1} (RingHom.id 𝕜) (TangentSpace I x)
                        (TangentSpace 𝓘(𝕜, 𝕜) (f x))) :
                    (a : TangentSpace I x) → TangentSpace 𝓘(𝕜, 𝕜) (f x))
                  (W x) :
                TangentSpace 𝓘(𝕜, 𝕜) (f x)) :
          𝕜)
        (V x) +
      f x • mlieBracketWithin I V W s x

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[s] f x
hV : (MDiffAt[s] fun (x : M) ↦ ⟨x, V x⟩) x
hs : UniqueMDiffWithinAt I s x
⊢ f x • mlieBracketWithin I V W s x +
      -HSMul.hSMul (α := 𝕜)
          ((fromTangentSpace (f x) : (a : TangentSpace 𝓘(𝕜, 𝕜) (f x)) → 𝕜)
              (((mfderivWithin I 𝓘(𝕜, 𝕜) f s x :
                      ContinuousLinearMap.{u_1, u_1, u_3, u_1} (RingHom.id 𝕜) (TangentSpace I x)
                        (TangentSpace 𝓘(𝕜, 𝕜) (f x))) :
                    (a : TangentSpace I x) → TangentSpace 𝓘(𝕜, 𝕜) (f x))
                  (W x) :
                TangentSpace 𝓘(𝕜, 𝕜) (f x)) :
            𝕜)
          (V x) =
    -HSMul.hSMul (α := 𝕜)
          ((fromTangentSpace (f x) : (a : TangentSpace 𝓘(𝕜, 𝕜) (f x)) → 𝕜)
              (((mfderivWithin I 𝓘(𝕜, 𝕜) f s x :
                      ContinuousLinearMap.{u_1, u_1, u_3, u_1} (RingHom.id 𝕜) (TangentSpace I x)
                        (TangentSpace 𝓘(𝕜, 𝕜) (f x))) :
                    (a : TangentSpace I x) → TangentSpace 𝓘(𝕜, 𝕜) (f x))
                  (W x) :
                TangentSpace 𝓘(𝕜, 𝕜) (f x)) :
            𝕜)
          (V x) +
      f x • mlieBracketWithin I V W s x

Tactic:
abel
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
V W : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
f : M → 𝕜
hf : MDiffAt f x
hV : (MDiffAt fun (x : M) ↦ ⟨x, V x⟩) x
⊢ MDiffAt[univ] f x

Tactic:
rw [← mdifferentiableWithinAt_univ] at hf hV

Premises used: mdifferentiableWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
V W : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
f : M → 𝕜
hf : MDiffAt f x
hV : (MDiffAt fun (x : M) ↦ ⟨x, V x⟩) x
hf₁ : MDiffAt[univ] f x
⊢ (MDiffAt[univ] fun (x : M) ↦ ⟨x, V x⟩) x

Tactic:
rw [← mdifferentiableWithinAt_univ] at hf hV

Premises used: mdifferentiableWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
V W : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[univ] f x
hV : (MDiffAt[univ] fun (x : M) ↦ ⟨x, V x⟩) x
rw :
  mlieBracketWithin I (f • V) W univ x =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜)
        (-((↑(fromTangentSpace (f x)) : TangentSpace 𝓘(𝕜, 𝕜) (f x) →L[𝕜] 𝕜) ∘SL mfderivWithin I 𝓘(𝕜, 𝕜) f univ x :
                (a : TangentSpace I x) → 𝕜)
              (W x) :
          𝕜)
        (V x) +
      f x • mlieBracket I V W x
⊢ mlieBracket I (f • V) W x =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (-(d% f x : (a : TangentSpace I x) → 𝕜) (W x) : 𝕜) (V x) +
      f x • mlieBracket I V W x

Tactic:
rw [← mlieBracketWithin_univ, mvfderiv, ← mfderivWithin_univ]

Premises used: mvfderiv, mfderivWithin_univ, VectorField.mlieBracketWithin_univ
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
V W : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[univ] f x
hV : (MDiffAt[univ] fun (x : M) ↦ ⟨x, V x⟩) x
⊢ mlieBracketWithin I (f • V) W univ x =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜)
        (-((↑(fromTangentSpace (f x)) : TangentSpace 𝓘(𝕜, 𝕜) (f x) →L[𝕜] 𝕜) ∘SL mfderivWithin I 𝓘(𝕜, 𝕜) f univ x :
                (a : TangentSpace I x) → 𝕜)
              (W x) :
          𝕜)
        (V x) +
      f x • mlieBracket I V W x

Tactic:
mlieBracketWithin_smul_left hf hV (uniqueMDiffWithinAt_univ I)

Premises used: VectorField.mlieBracketWithin_smul_left, uniqueMDiffWithinAt_univ, VectorField.mlieBracket
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
V W : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[univ] f x
hV : (MDiffAt[univ] fun (x : M) ↦ ⟨x, V x⟩) x
⊢ mlieBracketWithin I (f • V) W univ x =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜)
        (-((↑(fromTangentSpace (f x)) : TangentSpace 𝓘(𝕜, 𝕜) (f x) →L[𝕜] 𝕜) ∘SL mfderivWithin I 𝓘(𝕜, 𝕜) f univ x :
                (a : TangentSpace I x) → 𝕜)
              (W x) :
          𝕜)
        (V x) +
      f x • mlieBracket I V W x

Tactic:
exact mlieBracketWithin_smul_left hf hV (uniqueMDiffWithinAt_univ I)

Premises used: VectorField.mlieBracketWithin_smul_left, uniqueMDiffWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
c : 𝕜
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hV : MDiffAt[s] (T% V) x
hs : UniqueMDiffWithinAt I s x
⊢ mlieBracketWithin I (c • V) W s x = c • mlieBracketWithin I V W s x

Tactic:
simpa [mfderivWithin_const] using
    mlieBracketWithin_smul_left (mdifferentiableWithinAt_const (c := c)) (W := W) hV hs

Premises used: VectorField.mlieBracketWithin_smul_left, mdifferentiableWithinAt_const, mfderivWithin_const
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
V W : (x : M) → TangentSpace I x
c : 𝕜
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hV : MDiffAt (T% V) x
simp : mlieBracketWithin I (c • V) W univ x = c • mlieBracketWithin I V W univ x
⊢ mlieBracket I (c • V) W x = c • mlieBracket I V W x

Tactic:
simp only [← mlieBracketWithin_univ] at hV ⊢

Premises used: VectorField.mlieBracketWithin_univ
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
V W : (x : M) → TangentSpace I x
c : 𝕜
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hV : MDiffAt (T% V) x
⊢ mlieBracketWithin I (c • V) W univ x = c • mlieBracketWithin I V W univ x

Tactic:
mlieBracketWithin_const_smul_left hV (uniqueMDiffWithinAt_univ _)

Premises used: VectorField.mlieBracketWithin_const_smul_left, uniqueMDiffWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
V W : (x : M) → TangentSpace I x
c : 𝕜
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hV : MDiffAt (T% V) x
⊢ mlieBracketWithin I (c • V) W univ x = c • mlieBracketWithin I V W univ x

Tactic:
exact mlieBracketWithin_const_smul_left hV (uniqueMDiffWithinAt_univ _)

Premises used: VectorField.mlieBracketWithin_const_smul_left, uniqueMDiffWithinAt_univ