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
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
rw : mlieBracketWithin I V₁ W₁ univ x = mlieBracket I V W x
rw₁ : mlieBracketWithin I V₁ W₁ univ x = mlieBracketWithin I V W univ x
⊢ mlieBracket I V₁ W₁ x = mlieBracket I V W x
have rw₂ : mlieBracketWithin I V W univ x = mlieBracketWithin I V W univ x
Tactic: rw [← mlieBracketWithin_univ, ← mlieBracketWithin_univ,
    hV.mlieBracketWithin_vectorField_eq_nhds 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 V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
⊢ mlieBracket I V₁ W₁ =ᶠ[𝓝 x] mlieBracket I V W
have h : ∀ (y : M) (hVy : V₁ =ᶠ[𝓝 y] V) (hWy : W₁ =ᶠ[𝓝 y] W), mlieBracket I V₁ W₁ y = mlieBracket I V W y
Tactic: filter_upwards [hV.eventuallyEq_nhds, hW.eventuallyEq_nhds] with y hVy hWy
-- 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 : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hV : (MDiffAt[s] fun (x : M) ↦ ⟨x, V x⟩) x
⊢ DifferentiableWithinAt 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)))
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
have a : MDiffAt[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)]
    (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)))
  ((↑(extChartAt I x) : M → E) x)
Tactic: apply MDifferentiableWithinAt.differentiableWithinAt
-- 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
s : Set M
x : M
V : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hV : (MDiffAt[s] fun (x : M) ↦ ⟨x, V x⟩) x
⊢ MDiffAt[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)]
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)))
    ((↑(extChartAt I x) : M → E) x)
have this : (MDiffAt[range (↑I : H → E) ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s] fun (x_1 : E) ↦
    ⟨x_1, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) x_1⟩)
  ((↑(extChartAt I x) : M → E) x)
Tactic: have := MDifferentiableWithinAt.mpullbackWithin_vectorField_inter_of_eq hV
    (contMDiffWithinAt_extChartAt_symm_range x (mem_extChartAt_target x))
    (isInvertible_mfderivWithin_extChartAt_symm (mem_extChartAt_target x)) (mem_range_self _)
    I.uniqueMDiffOn le_rfl (extChartAt_to_inv x).symm
-- 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 : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hV : (MDiffAt[s] fun (x : M) ↦ ⟨x, V x⟩) x
this :
  (MDiffAt[range (↑I : H → E) ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s] fun (x_1 : E) ↦
      ⟨x_1, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) x_1⟩)
    ((↑(extChartAt I x) : M → E) x)
⊢ MDiffAt[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)]
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)))
    ((↑(extChartAt I x) : M → E) x)
have a : MDiffAt[range (↑I : H → E) ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s]
    (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)))
  ((↑(extChartAt I x) : M → E) x)
Tactic: rw [inter_comm]
-- 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
inst_6 : IsManifold I 2 M
Y : TangentSpace I x
φ : PartialEquiv M E := extChartAt I x
⊢ (ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(𝕜, E) ((↑φ : M → E) x))
          (ContinuousLinearMap.inverse (mfderiv% (↑φ : M → E) x))
          (ContinuousLinearMap.inverse
            (mfderivWithin 𝓘(𝕜, E) I (↑φ.symm : E → M) (range (↑I : H → E)) ((↑φ : M → E) x))) :
        (a : TangentSpace I ((↑φ.symm : E → M) ((↑φ : M → E) x))) → TangentSpace I x)
      Y =
    Y
have trans : Eq (α := TangentSpace I x)
  ((ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(𝕜, E) ((↑φ : M → E) x))
          (ContinuousLinearMap.inverse (mfderiv% (↑φ : M → E) x))
          (ContinuousLinearMap.inverse
            (mfderivWithin 𝓘(𝕜, E) I (↑φ.symm : E → M) (range (↑I : H → E)) ((↑φ : M → E) x))) :
        (a : TangentSpace I ((↑φ.symm : E → M) ((↑φ : M → E) x))) → TangentSpace I x)
      Y :
    TangentSpace I x)
  ((ContinuousLinearMap.id 𝕜 (TangentSpace I x) : (a : TangentSpace I x) → TangentSpace I x) Y : TangentSpace I x)
Tactic: trans (ContinuousLinearMap.id 𝕜 _) Y
-- 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
inst_6 : IsManifold I 2 M
Y : TangentSpace I x
φ : PartialEquiv M E := extChartAt I x
trans :
  Eq (α := TangentSpace I x)
    ((ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(𝕜, E) ((↑φ : M → E) x))
            (ContinuousLinearMap.inverse (mfderiv% (↑φ : M → E) x))
            (ContinuousLinearMap.inverse
              (mfderivWithin 𝓘(𝕜, E) I (↑φ.symm : E → M) (range (↑I : H → E)) ((↑φ : M → E) x))) :
          (a : TangentSpace I ((↑φ.symm : E → M) ((↑φ : M → E) x))) → TangentSpace I x)
        Y :
      TangentSpace I x)
    ((ContinuousLinearMap.id 𝕜 (TangentSpace I x) : (a : TangentSpace I x) → TangentSpace I x) Y : TangentSpace I x)
⊢ (ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(𝕜, E) ((↑φ : M → E) x))
          (ContinuousLinearMap.inverse (mfderiv% (↑φ : M → E) x))
          (ContinuousLinearMap.inverse
            (mfderivWithin 𝓘(𝕜, E) I (↑φ.symm : E → M) (range (↑I : H → E)) ((↑φ : M → E) x))) :
        (a : TangentSpace I ((↑φ.symm : E → M) ((↑φ : M → E) x))) → TangentSpace I x)
      Y =
    Y
have trans₁ : (ContinuousLinearMap.id 𝕜 (TangentSpace I x) : (a : TangentSpace I x) → TangentSpace I x) Y = Y
Tactic: trans (ContinuousLinearMap.id 𝕜 _) Y
-- 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
inst_6 : IsManifold I 2 M
Y : TangentSpace I x
φ : PartialEquiv M E := extChartAt I x
⊢ Eq (α := TangentSpace I x)
    ((ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(𝕜, E) ((↑φ : M → E) x))
            (ContinuousLinearMap.inverse (mfderiv% (↑φ : M → E) x))
            (ContinuousLinearMap.inverse
              (mfderivWithin 𝓘(𝕜, E) I (↑φ.symm : E → M) (range (↑I : H → E)) ((↑φ : M → E) x))) :
          (a : TangentSpace I ((↑φ.symm : E → M) ((↑φ : M → E) x))) → TangentSpace I x)
        Y :
      TangentSpace I x)
    ((ContinuousLinearMap.id 𝕜 (TangentSpace I x) : (a : TangentSpace I x) → TangentSpace I x) Y : TangentSpace I x)
have rw : ContinuousLinearMap.IsInvertible (M := TangentSpace 𝓘(𝕜, E) ((↑φ : M → E) x)) (M₂ := TangentSpace I x)
  (mfderivWithin 𝓘(𝕜, E) I (↑φ.symm : E → M) (range (↑I : H → E)) ((↑φ : M → E) x) :
    TangentSpace 𝓘(𝕜, E) ((↑φ : M → E) x) →L[𝕜] TangentSpace I ((↑φ.symm : E → M) ((↑φ : M → E) x)))
Tactic: rw [extChartAt_to_inv x, ← ContinuousLinearMap.IsInvertible.inverse_comp_of_left,
    ← ContinuousLinearMap.inverse_id,
    mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt' (mem_extChartAt_source x)]
-- 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
W : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
⊢ (ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
          (ContinuousLinearMap.inverse (mfderiv% (↑(extChartAt I x) : M → E) x))
          (ContinuousLinearMap.inverse
            (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E))
              ((↑(extChartAt I x) : M → E) x))) :
        (a : TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) → TangentSpace I x)
      (W ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) =
    W x
have rw : W ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)) = W x
Tactic: rw [mfderiv_extChartAt_inverse_comp_mfderivWithin_extChartAT_symm, extChartAt_to_inv]
-- 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
W : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
rw : W ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)) = W x
⊢ (ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
          (ContinuousLinearMap.inverse (mfderiv% (↑(extChartAt I x) : M → E) x))
          (ContinuousLinearMap.inverse
            (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E))
              ((↑(extChartAt I x) : M → E) x))) :
        (a : TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) → TangentSpace I x)
      (W ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) =
    W x
have rw₁ : W x = W x
Tactic: rw [mfderiv_extChartAt_inverse_comp_mfderivWithin_extChartAT_symm, extChartAt_to_inv]
-- 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
f : M → 𝕜
hf : MDiffAt[s] f x
⊢ (ContinuousLinearMap.inverse
          (if MDiffAt[range (↑I : H → E)] (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) then
            fderivWithin 𝕜
              (writtenInExtChartAt 𝓘(𝕜, E) I ((↑(extChartAt I x) : M → E) x) (↑(extChartAt I x).symm : E → M))
              ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)).symm : E → E) ⁻¹' range (↑I : H → E) ∩
                range (↑𝓘(𝕜, E) : E → E))
              ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) : E → E) ((↑(extChartAt I x) : M → E) x))
          else 0) :
        (a : TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) →
          TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
      (V ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) =
    V x
have e_a : (ContinuousLinearMap.inverse
        (if MDiffAt[range (↑I : H → E)] (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) then
          fderivWithin 𝕜
            (writtenInExtChartAt 𝓘(𝕜, E) I ((↑(extChartAt I x) : M → E) x) (↑(extChartAt I x).symm : E → M))
            ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)).symm : E → E) ⁻¹' range (↑I : H → E) ∩
              range (↑𝓘(𝕜, E) : E → E))
            ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) : E → E) ((↑(extChartAt I x) : M → E) x))
        else 0) :
      (a : TangentSpace I x) → TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
    (V x) =
  V x
Tactic: rw [extChartAt_to_inv]
-- 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
⊢ mlieBracketWithin I V (f • 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))
                (V x) :
              TangentSpace 𝓘(𝕜, 𝕜) (f x)) :
          𝕜)
        (W x) +
      f x • mlieBracketWithin I V W s x
have simp : mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
    (lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)))
      (HSMul.hSMul (β := (x : E) → TangentSpace 𝓘(𝕜, E) x) (f ∘ (↑(extChartAt I x).symm : E → M))
        (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)))
    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 𝕜 (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)))
        x)
Tactic: simp only [mlieBracketWithin, mpullbackWithin_smul]
-- 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) (lieBracketWithin 𝕜 V' (f' • 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))
                (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 trans : Eq (α := TangentSpace I x) (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (lieBracketWithin 𝕜 V' (f' • W') s') x)
  (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (fun (y : E) ↦ A y + B y) x)
Tactic: trans mpullback I 𝓘(𝕜, E) ((extChartAt I x)) (fun y ↦ A y + B y) x
-- 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₀
trans :
  Eq (α := TangentSpace I x) (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (lieBracketWithin 𝕜 V' (f' • W') s') x)
    (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (fun (y : E) ↦ A y + B y) x)
⊢ mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (lieBracketWithin 𝕜 V' (f' • 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))
                (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 trans₁ : 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)
Tactic: trans mpullback I 𝓘(𝕜, E) ((extChartAt I x)) (fun y ↦ A y + B y) x
-- 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) (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (lieBracketWithin 𝕜 V' (f' • W') s') x)
    (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (fun (y : E) ↦ A y + B y) x)
have simp : 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)
Tactic: simp only [mpullback_apply]