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 V₁ W₁ : (x : M) → TangentSpace I x
hV : EqOn V₁ V s
hVx : V₁ x = V x
hW : EqOn W₁ W s
hWx : W₁ x = W x
⊢ mlieBracketWithin I V₁ W₁ s x = mlieBracketWithin I V W s x

Tactic:
(hV.eventuallyEq.filter_mono inf_le_right).mlieBracketWithin_vectorField_eq hVx
    (hW.eventuallyEq.filter_mono inf_le_right) hWx

Premises used: Filter.EventuallyEq.filter_mono, Set.EqOn.eventuallyEq, inf_le_right, Filter.EventuallyEq.mlieBracketWithin_vectorField_eq
-- 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 V₁ W₁ : (x : M) → TangentSpace I x
hV : EqOn V₁ V s
hW : EqOn W₁ W s
hx : x ∈ s
⊢ mlieBracketWithin I V₁ W₁ s x = mlieBracketWithin I V W s x

Tactic:
mlieBracketWithin_congr hV (hV hx) hW (hW hx)

Premises used: VectorField.mlieBracketWithin_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
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
rw₂ rw₃ : mlieBracketWithin I V W univ x = mlieBracketWithin I V W univ x
⊢ mlieBracket I V₁ W₁ x = mlieBracket I V W x

Tactic:
rw [← mlieBracketWithin_univ, ← mlieBracketWithin_univ,
    hV.mlieBracketWithin_vectorField_eq_nhds hW]

Premises used: VectorField.mlieBracketWithin_univ, Filter.EventuallyEq.mlieBracketWithin_vectorField_eq_nhds
-- 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 V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
h : ∀ (y : M) (hVy : V₁ =ᶠ[𝓝 y] V) (hWy : W₁ =ᶠ[𝓝 y] W), mlieBracket I V₁ W₁ y = mlieBracket I V W y
⊢ mlieBracket I V₁ W₁ =ᶠ[𝓝 x] mlieBracket I V W

Tactic:
filter_upwards [hV.eventuallyEq_nhds, hW.eventuallyEq_nhds] with y hVy hWy

Premises used: Filter.EventuallyEq.eventuallyEq_nhds
-- 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 V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
y : M
hVy : V₁ =ᶠ[𝓝 y] V
hWy : W₁ =ᶠ[𝓝 y] W
⊢ mlieBracket I V₁ W₁ y = mlieBracket I V W y

Tactic:
hVy.mlieBracket_vectorField_eq hWy

Premises used: Filter.EventuallyEq.mlieBracket_vectorField_eq, TangentSpace
-- 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 V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
y : M
hVy : V₁ =ᶠ[𝓝 y] V
hWy : W₁ =ᶠ[𝓝 y] W
⊢ mlieBracket I V₁ W₁ y = mlieBracket I V W y

Tactic:
exact hVy.mlieBracket_vectorField_eq hWy

Premises used: Filter.EventuallyEq.mlieBracket_vectorField_eq
-- 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 : (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
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)
⊢ 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)

Tactic:
apply MDifferentiableWithinAt.differentiableWithinAt

Premises used: MDifferentiableWithinAt.differentiableWithinAt
-- 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 : (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[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
-- 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 : (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)
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)
⊢ 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:
rw [inter_comm]

Premises used: Set.inter_comm
-- 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 : (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[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:
(contMDiff_snd_tangentBundle_modelSpace E 𝓘(𝕜, E)).contMDiffAt.mdifferentiableAt one_ne_zero
    |>.comp_mdifferentiableWithinAt _ this

Premises used: MDifferentiableAt.comp_mdifferentiableWithinAt, ContMDiffAt.mdifferentiableAt, VectorField.mpullbackWithin, modelWithCornersSelf, ContMDiff.contMDiffAt, one_ne_zero, contMDiff_snd_tangentBundle_modelSpace
-- 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 : (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[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:
exact (contMDiff_snd_tangentBundle_modelSpace E 𝓘(𝕜, E)).contMDiffAt.mdifferentiableAt one_ne_zero
    |>.comp_mdifferentiableWithinAt _ this

Premises used: MDifferentiableAt.comp_mdifferentiableWithinAt, ContMDiffAt.mdifferentiableAt, modelWithCornersSelf, ContMDiff.contMDiffAt, one_ne_zero, contMDiff_snd_tangentBundle_modelSpace
-- 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
inst_6 : IsManifold I 2 M
Y : TangentSpace I x
set :
  let φ := 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
⊢ (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)
      Y =
    Y

Tactic:
set φ := extChartAt I x

Premises used: extChartAt
-- 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
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)
trans₁ : (ContinuousLinearMap.id 𝕜 (TangentSpace I x) : (a : TangentSpace I x) → TangentSpace I x) Y = Y
⊢ (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

Tactic:
trans (ContinuousLinearMap.id 𝕜 _) Y

Premises used: ContinuousLinearMap.id, DFunLike.coe
-- 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
inst_6 : IsManifold I 2 M
Y : TangentSpace I x
φ : PartialEquiv M E := extChartAt I x
⊢ (ContinuousLinearMap.id 𝕜 (TangentSpace I x) : (a : TangentSpace I x) → TangentSpace I x) Y = Y

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
x : M
inst_6 : IsManifold I 2 M
Y : TangentSpace I x
φ : PartialEquiv M E := extChartAt I x
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)))
⊢ 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:
rw [extChartAt_to_inv x, ← ContinuousLinearMap.IsInvertible.inverse_comp_of_left,
    ← ContinuousLinearMap.inverse_id,
    mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt' (mem_extChartAt_source x)]

Premises used: extChartAt_to_inv, ContinuousLinearMap.IsInvertible.inverse_comp_of_left, mem_extChartAt_source, mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt', ContinuousLinearMap.inverse_id
-- 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
inst_6 : IsManifold I 2 M
Y : TangentSpace I x
φ : PartialEquiv M E := extChartAt I x
⊢ 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:
isInvertible_mfderivWithin_extChartAt_symm (mem_extChartAt_target x)

Premises used: mem_extChartAt_target, instModuleTangentSpace._aux_1, TangentSpace, instTopologicalSpaceTangentSpace._aux_1, isInvertible_mfderivWithin_extChartAt_symm, instAddCommGroupTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_4
-- 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
inst_6 : IsManifold I 2 M
Y : TangentSpace I x
φ : PartialEquiv M E := extChartAt I x
⊢ 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:
exact isInvertible_mfderivWithin_extChartAt_symm (mem_extChartAt_target x)

Premises used: mem_extChartAt_target, isInvertible_mfderivWithin_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
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
rw₁ rw₂ : W 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

Tactic:
rw [mfderiv_extChartAt_inverse_comp_mfderivWithin_extChartAT_symm, extChartAt_to_inv]

Premises used: extChartAt_to_inv, VectorField.mfderiv_extChartAt_inverse_comp_mfderivWithin_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
f : M → 𝕜
hf : MDiffAt[s] f x
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
⊢ (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

Tactic:
rw [extChartAt_to_inv]

Premises used: extChartAt_to_inv
-- 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
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 x) → TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
      (V x) =
    V x

Tactic:
mfderivWithin_extChartAt_symm_inverse_apply (v := V x)

Premises used: mfderivWithin, mfderivWithin_extChartAt_symm_inverse_apply, instModuleTangentSpace._aux_1, TangentSpace, instTopologicalSpaceTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_4
-- 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
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 x) → TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
      (V x) =
    V x

Tactic:
exact mfderivWithin_extChartAt_symm_inverse_apply (v := V x)

Premises used: mfderivWithin_extChartAt_symm_inverse_apply