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 V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_7, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
_I2 : NormedSpace.{u_1, u_3} 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) := inst_3
⊢ 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]
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E))
have h : {x_1 : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x) |
    (fun (x_2 : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) ↦
        Eq (α := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
          (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V₁ (range (↑I : H → E)) x_2 :
            TangentSpace 𝓘(𝕜, E) x_2)
          (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) x_2))
      x_1} ∈
  𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s] (↑(extChartAt I x) : M → E) x
Tactic: apply nhdsWithin_mono _ inter_subset_left
-- 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₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_7, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
_I2 : NormedSpace.{u_1, u_3} 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) := inst_3
⊢ {x_1 : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x) |
      (fun (x_2 : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) ↦
          Eq (α := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
            (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V₁ (range (↑I : H → E)) x_2 :
              TangentSpace 𝓘(𝕜, E) x_2)
            (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) x_2))
        x_1} ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s] (↑(extChartAt I x) : M → E) x
have h : ∀ (y : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
  (hy :
    y ∈ (↑(extChartAt I x).symm : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x) → M) ⁻¹' {x : M | V₁ x = V x}),
  Eq (α := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
    (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V₁ (range (↑I : H → E)) y : TangentSpace 𝓘(𝕜, E) y)
    (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) y)
Tactic: filter_upwards [(continuousAt_extChartAt_symm x).continuousWithinAt.preimage_mem_nhdsWithin''
      hV (by simp)] with y hy
-- 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₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_7, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
_I2 : NormedSpace.{u_1, u_3} 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) := inst_3
⊢ Eq (α := TangentSpace 𝓘(𝕜, E) ((↑(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 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
      (V₁ ((↑(extChartAt I x).symm : E → M) ((↑(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 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
      (V ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))))
have h : Eq.{u_3 + 1} (α := TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
  (V₁ ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
  (V ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
Tactic: congr 1
-- 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₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_7, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
_I2 : NormedSpace.{u_1, u_3} 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) := inst_3
⊢ Eq.{u_3 + 1} (α := TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
    (V₁ ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
    (V ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
have h : (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) = x
Tactic: convert! hxV
-- 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₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_7, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
_I2 : NormedSpace.{u_1, u_3} 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) := inst_3
h : (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) = x
⊢ Eq.{u_3 + 1} (α := TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
    (V₁ ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
    (V ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
have h₁ : TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)) = TangentSpace I x →
  (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) = x
Tactic: convert! hxV
-- 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₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_7, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
_I2 : NormedSpace.{u_1, u_3} 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) := inst_3
⊢ 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]
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E))
have h : {x_1 : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x) |
    (fun (x_2 : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) ↦
        Eq (α := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
          (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W₁ (range (↑I : H → E)) x_2 :
            TangentSpace 𝓘(𝕜, E) x_2)
          (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E)) x_2))
      x_1} ∈
  𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s] (↑(extChartAt I x) : M → E) x
Tactic: apply nhdsWithin_mono _ inter_subset_left
-- 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₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_7, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
_I2 : NormedSpace.{u_1, u_3} 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) := inst_3
⊢ {x_1 : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x) |
      (fun (x_2 : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) ↦
          Eq (α := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
            (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W₁ (range (↑I : H → E)) x_2 :
              TangentSpace 𝓘(𝕜, E) x_2)
            (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E)) x_2))
        x_1} ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s] (↑(extChartAt I x) : M → E) x
have h : ∀ (y : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
  (hy :
    y ∈ (↑(extChartAt I x).symm : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x) → M) ⁻¹' {x : M | W₁ x = W x}),
  Eq (α := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
    (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W₁ (range (↑I : H → E)) y : TangentSpace 𝓘(𝕜, E) y)
    (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E)) y)
Tactic: filter_upwards [(continuousAt_extChartAt_symm x).continuousWithinAt.preimage_mem_nhdsWithin''
      hW (by simp)] with y hy
-- 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₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_7, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
_I2 : NormedSpace.{u_1, u_3} 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) := inst_3
⊢ Eq (α := TangentSpace 𝓘(𝕜, E) ((↑(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 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
      (W₁ ((↑(extChartAt I x).symm : E → M) ((↑(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 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
      (W ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))))
have h : Eq.{u_3 + 1} (α := TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
  (W₁ ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
  (W ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
Tactic: congr 1
-- 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₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_7, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
_I2 : NormedSpace.{u_1, u_3} 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) := inst_3
⊢ Eq.{u_3 + 1} (α := TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
    (W₁ ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
    (W ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
have h : (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) = x
Tactic: convert! hxW
-- 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₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_7, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
_I2 : NormedSpace.{u_1, u_3} 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) := inst_3
h : (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) = x
⊢ Eq.{u_3 + 1} (α := TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
    (W₁ ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
    (W ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
have h₁ : TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)) = TangentSpace I x →
  (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) = x
Tactic: convert! hxW
-- 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 t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
⊢ mlieBracketWithin I V₁ W₁ t =ᶠ[𝓝[s] x] mlieBracketWithin I V W t
have h : ∀ (y : M) (hVy : V₁ y = V y) (hWy : W₁ y = W y) (hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x)
  (hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x), mlieBracketWithin I V₁ W₁ t y = mlieBracketWithin I V W t y
Tactic: filter_upwards [hV, hW, eventually_eventually_nhdsWithin.2 hV,
    eventually_eventually_nhdsWithin.2 hW] with y hVy hWy 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 t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
⊢ mlieBracketWithin I V₁ W₁ t y = mlieBracketWithin I V W t y
have h : V₁ =ᶠ[𝓝[t] y] V
Tactic: apply Filter.EventuallyEq.mlieBracketWithin_vectorField_eq
-- 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 t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
h : V₁ =ᶠ[𝓝[t] y] V
⊢ mlieBracketWithin I V₁ W₁ t y = mlieBracketWithin I V W t y
have h₁ : V₁ y = V y
Tactic: apply Filter.EventuallyEq.mlieBracketWithin_vectorField_eq
-- 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 t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
h : V₁ =ᶠ[𝓝[t] y] V
h₁ : V₁ y = V y
⊢ mlieBracketWithin I V₁ W₁ t y = mlieBracketWithin I V W t y
have h₂ : W₁ =ᶠ[𝓝[t] y] W
Tactic: apply Filter.EventuallyEq.mlieBracketWithin_vectorField_eq
-- 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 t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
h : V₁ =ᶠ[𝓝[t] y] V
h₁ : V₁ y = V y
h₂ : W₁ =ᶠ[𝓝[t] y] W
⊢ mlieBracketWithin I V₁ W₁ t y = mlieBracketWithin I V W t y
have h₃ : W₁ y = W y
Tactic: apply Filter.EventuallyEq.mlieBracketWithin_vectorField_eq
-- 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 t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
⊢ V₁ =ᶠ[𝓝[t] y] V
have h : {x : M | (fun (x : M) ↦ V₁ x = V x) x} ∈ 𝓝[s] y
Tactic: apply nhdsWithin_mono _ ht
-- 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 t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
⊢ W₁ =ᶠ[𝓝[t] y] W
have h : {x : M | (fun (x : M) ↦ W₁ x = W x) x} ∈ 𝓝[s] y
Tactic: apply nhdsWithin_mono _ ht
-- 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 x
have rw : mlieBracketWithin I V₁ W₁ univ x = mlieBracket I V W 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
rw : mlieBracketWithin I V₁ W₁ univ x = mlieBracket I V W 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]