awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
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₀
⊢ Eq (α := TangentSpace I x)
    ((ContinuousLinearMap.inverse (mfderiv% (↑(extChartAt I x) : M → E) x) :
          (a : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) → TangentSpace I x)
        (lieBracketWithin 𝕜 V' (f' • W') s' ((↑(extChartAt I x) : M → E) x)) :
      TangentSpace I x)
    ((ContinuousLinearMap.inverse (mfderiv% (↑(extChartAt I x) : M → E) x) :
          (a : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) → TangentSpace I x)
        (HAdd.hAdd (α := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) (A ((↑(extChartAt I x) : M → E) x))
          (B ((↑(extChartAt I x) : M → E) x))) :
      TangentSpace I x)
have h : lieBracketWithin 𝕜 V' (f' • W') s' ((↑(extChartAt I x) : M → E) x) =
  HAdd.hAdd (α := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) (A ((↑(extChartAt I x) : M → E) x))
    (B ((↑(extChartAt I x) : M → E) x))
Tactic: congr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
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) (fun (y : E) ↦ A y + B y) 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)
have rw : 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: rw [← Pi.add_def, mpullback_add_apply]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
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₀
⊢ 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)
have 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)
Tactic: congr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
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)
⊢ 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)
have 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)
Tactic: congr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (hypothesis)
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
⊢ 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
have hf₁ : MDiffAt[univ] f x
Tactic: rw [← mdifferentiableWithinAt_univ] at hf hW
Cleared hypotheses: hf, hW
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (hypothesis)
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
⊢ 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
have hW₁ : (MDiffAt[univ] fun (x : M) ↦ ⟨x, W x⟩) x
Tactic: rw [← mdifferentiableWithinAt_univ] at hf hW
Cleared hypotheses: hf, hW
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
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
⊢ 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
have 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
Tactic: rw [← mlieBracketWithin_univ, mvfderiv, ← mfderivWithin_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
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
⊢ 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
have 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
Tactic: rw [mlieBracketWithin_swap, Pi.neg_apply, mlieBracketWithin_smul_right hf hV (V := W) hs,
    mlieBracketWithin_swap]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
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
⊢ -(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
have 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
Tactic: simp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (hypothesis)
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
⊢ 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
have hf₁ : MDiffAt[univ] f x
Tactic: rw [← mdifferentiableWithinAt_univ] at hf hV
Cleared hypotheses: hf, hV
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (hypothesis)
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
⊢ 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
have hV₁ : (MDiffAt[univ] fun (x : M) ↦ ⟨x, V x⟩) x
Tactic: rw [← mdifferentiableWithinAt_univ] at hf hV
Cleared hypotheses: hf, hV
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
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
⊢ 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
have 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
Tactic: rw [← mlieBracketWithin_univ, mvfderiv, ← mfderivWithin_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
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
⊢ mlieBracket I (c • V) W x = c • mlieBracket I V W x
have simp : mlieBracketWithin I (c • V) W univ x = c • mlieBracketWithin I V W univ x
Tactic: simp only [← mlieBracketWithin_univ] at hV ⊢
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
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
hW : MDiffAt (T% W) x
⊢ mlieBracket I V (c • W) x = c • mlieBracket I V W x
have simp : mlieBracketWithin I V (c • W) univ x = c • mlieBracketWithin I V W univ x
Tactic: simp only [← mlieBracketWithin_univ] at hW ⊢
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
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 V₁ : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hV : MDiffAt[s] (T% V) x
hV₁ : MDiffAt[s] (T% V₁) x
hs : UniqueMDiffWithinAt I s x
⊢ mlieBracketWithin I (V + V₁) W s x = mlieBracketWithin I V W s x + mlieBracketWithin I V₁ W s x
have simp : (ContinuousLinearMap.inverse (mfderiv% (↑(extChartAt I x) : M → E) x) :
      (a : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) → TangentSpace I x)
    (lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (V + V₁) (range (↑I : H → E)))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E)))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)) =
  HAdd.hAdd (α := TangentSpace I x) (β := TangentSpace I x)
    ((ContinuousLinearMap.inverse (mfderiv% (↑(extChartAt I x) : M → E) x) :
          (a : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) → TangentSpace I x)
        (lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)))
          (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E)))
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)) :
      TangentSpace I x)
    ((ContinuousLinearMap.inverse (mfderiv% (↑(extChartAt I x) : M → E) x) :
          (a : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) → TangentSpace I x)
        (lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V₁ (range (↑I : H → E)))
          (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E)))
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)) :
      TangentSpace I x)
Tactic: simp only [mlieBracketWithin_apply]