-- Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean
lemma isInvertible_mfderiv_extChartAt {y : M} (hy : y ∈ (extChartAt I x).source) :
    (mfderiv I 𝓘(𝕜, E) (extChartAt I x) y).IsInvertible

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
h'y : ↑(extChartAt I x) y ∈ (extChartAt I x).target
Z : (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) (↑(extChartAt I x).symm (↑(extChartAt I x) y))).IsInvertible
this : ↑(extChartAt I x).symm (↑(extChartAt I x) y) = y
⊢ (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) y).IsInvertible

Tactic:
rwa [this] at Z

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
h'y : ↑(extChartAt I x) y ∈ (extChartAt I x).target
Z : (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) (↑(extChartAt I x).symm (↑(extChartAt I x) y))).IsInvertible
⊢ (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) y).IsInvertible

Tactic:
have : (extChartAt I x).symm ((extChartAt I x) y) = y := (extChartAt I x).left_inv hy

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
h'y : ↑(extChartAt I x) y ∈ (extChartAt I x).target
Z : (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) (↑(extChartAt I x).symm (↑(extChartAt I x) y))).IsInvertible
this : ↑(extChartAt I x).symm (↑(extChartAt I x) y) = y
⊢ (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) y).IsInvertible

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
⊢ (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) y).IsInvertible

Tactic:
have h'y : extChartAt I x y ∈ (extChartAt I x).target := (extChartAt I x).map_source hy

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
h'y : ↑(extChartAt I x) y ∈ (extChartAt I x).target
⊢ (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) y).IsInvertible

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
h'y : ↑(extChartAt I x) y ∈ (extChartAt I x).target
⊢ (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) y).IsInvertible

Tactic:
have Z := ContinuousLinearMap.IsInvertible.of_inverse
  (mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm h'y)
  (mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt h'y)

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
h'y : ↑(extChartAt I x) y ∈ (extChartAt I x).target
Z : (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) (↑(extChartAt I x).symm (↑(extChartAt I x) y))).IsInvertible
⊢ (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) y).IsInvertible