-- 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
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiffOn I s
hf : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
A : (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀) = x₀
hfi :
  ¬ContinuousLinearMap.IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
neg :
  Eq (α := E)
    (((ContinuousLinearMap.inverse
              (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x₀).symm : E → M) (range (↑I : H → E))
                ((↑(extChartAt I x₀) : M → E) x₀)) :
            TangentSpace I x₀ →L[𝕜] TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x₀) : M → E) x₀)) :
          (a : TangentSpace I x₀) → TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x₀) : M → E) x₀))
        (((0 : ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f x₀)) (TangentSpace I x₀)) :
            (a : TangentSpace I' (f x₀)) → TangentSpace I x₀)
          (V (f x₀))) :
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x₀) : M → E) x₀))
    (0 : E)
⊢ Eq (α := E)
    ((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₀))
        (((ContinuousLinearMap.inverse
                (mfderivWithin I I' f s ((↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀))) :
              ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜)
                (TangentSpace I' (f ((↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀))))
                (TangentSpace I ((↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀)))) :
            (a : TangentSpace I' (f ((↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀)))) →
              TangentSpace I ((↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀)))
          (V (f ((↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀))))) :
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x₀) : M → E) x₀))
    (0 : E)

Tactic:
rw [A, ContinuousLinearMap.inverse_of_not_isInvertible hfi]

Premises used: ContinuousLinearMap.inverse_of_not_isInvertible