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
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)
⊢ 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

Tactic:
simp only [mlieBracketWithin, mpullbackWithin_smul]

Premises used: VectorField.mpullbackWithin_smul, VectorField.mlieBracketWithin
-- 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))
set :
  let W' : (x : E) → TangentSpace 𝓘(𝕜, E) x :=
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E));
  mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
      (lieBracketWithin 𝕜 V' (f ∘ (↑(extChartAt I x).symm : E → M) • W')
        ((↑(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 𝕜 V' W' ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))) x)
⊢ mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
      (lieBracketWithin 𝕜 V'
        (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 𝕜 V' (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:
set W' := mpullbackWithin 𝓘(𝕜, E) I (extChartAt I x).symm W (range I)

Premises used: extChartAt, VectorField.mpullbackWithin, PartialEquiv.symm, ModelWithCorners.toFun', modelWithCornersSelf, Set.range, PartialEquiv.toFun
-- 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))
set :
  let f' := f ∘ (↑(extChartAt I x).symm : E → M);
  mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
      (lieBracketWithin 𝕜 V' (f' • W') ((↑(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 𝕜 V' W' ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))) x)
⊢ mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
      (lieBracketWithin 𝕜 V' (f ∘ (↑(extChartAt I x).symm : E → M) • W')
        ((↑(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 𝕜 V' W' ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))) x)

Tactic:
set f' := f ∘ (extChartAt I x).symm

Premises used: extChartAt, PartialEquiv.symm
-- 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)
set :
  let s' := (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E);
  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)
⊢ mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
      (lieBracketWithin 𝕜 V' (f' • W') ((↑(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 𝕜 V' W' ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))) x)

Tactic:
set s' := (extChartAt I x).symm ⁻¹' s ∩ range I

Premises used: extChartAt, PartialEquiv.symm, ModelWithCorners.toFun', Set.range
-- 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₀
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)
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)
⊢ 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)

Tactic:
trans mpullback I 𝓘(𝕜, E) ((extChartAt I x)) (fun y ↦ A y + B y) x

Premises used: extChartAt, VectorField.mpullback, HAdd.hAdd, modelWithCornersSelf, PartialEquiv.toFun
-- 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₀
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)
⊢ 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:
simp only [mpullback_apply]

Premises used: VectorField.mpullback_apply
-- 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₀
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))
⊢ 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:
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₀
⊢ 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:
lieBracketWithin_smul_right (V := V') hf.differentiableWithinAt_comp_extChartAt_symm
      hW.differentiableWithinAt_mpullbackWithin_vectorField hs

Premises used: MDifferentiableWithinAt.differentiableWithinAt_mpullbackWithin_vectorField, TangentSpace, VectorField.lieBracketWithin_smul_right, MDifferentiableWithinAt.differentiableWithinAt_comp_extChartAt_symm
-- 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₀
⊢ 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:
exact lieBracketWithin_smul_right (V := V') hf.differentiableWithinAt_comp_extChartAt_symm
      hW.differentiableWithinAt_mpullbackWithin_vectorField hs

Premises used: MDifferentiableWithinAt.differentiableWithinAt_mpullbackWithin_vectorField, VectorField.lieBracketWithin_smul_right, MDifferentiableWithinAt.differentiableWithinAt_comp_extChartAt_symm
-- 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₀
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)
⊢ 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:
rw [← Pi.add_def, mpullback_add_apply]

Premises used: VectorField.mpullback_add_apply, Pi.add_def