awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source
h''y : (↑(extChartAt I x).symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y)
this :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y))
⊢ (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y) = y

Tactic:
PartialEquiv.right_inv (extChartAt I x) hy

Premises used: extChartAt, PartialEquiv.right_inv
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source
h''y : (↑(extChartAt I x).symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y)
this :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y))
⊢ (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y) = y

Tactic:
exact PartialEquiv.right_inv (extChartAt I x) hy

Premises used: extChartAt, PartialEquiv.right_inv
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source
h''y : (↑(extChartAt I x).symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y)
this :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y))
rw :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I I ((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) (extChartAt I x).source
        ((↑(extChartAt I x).symm : E → M) y) :
      TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
        TangentSpace I
          (((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderivWithin I I id (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y))
⊢ Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I I ((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) (extChartAt I x).source
        ((↑(extChartAt I x).symm : E → M) y) :
      TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
        TangentSpace I
          (((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) ((↑(extChartAt I x).symm : E → M) y)))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I ((↑(extChartAt I x).symm : E → M) y)))

Tactic:
rw [← mfderivWithin_id U']

Premises used: mfderivWithin_id
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source
h''y : (↑(extChartAt I x).symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y)
this :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y))
hL :
  (↑(extChartAt I x).symm : E → M) ∘
      (↑(extChartAt I x) : M → E) =ᶠ[𝓝[(extChartAt I x).source] (↑(extChartAt I x).symm : E → M) y]
    id
hx :
  ((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) ((↑(extChartAt I x).symm : E → M) y) =
    id ((↑(extChartAt I x).symm : E → M) y)
⊢ Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I I ((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) (extChartAt I x).source
        ((↑(extChartAt I x).symm : E → M) y) :
      TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
        TangentSpace I
          (((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderivWithin I I id (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y))

Tactic:
apply Filter.EventuallyEq.mfderivWithin_eq

Premises used: Filter.EventuallyEq.mfderivWithin_eq
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source
h''y : (↑(extChartAt I x).symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y)
this :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y))
h :
  ∀ (z : M) (hz : z ∈ (extChartAt I x).source),
    ((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) z = id z
⊢ (↑(extChartAt I x).symm : E → M) ∘
      (↑(extChartAt I x) : M → E) =ᶠ[𝓝[(extChartAt I x).source] (↑(extChartAt I x).symm : E → M) y]
    id

Tactic:
filter_upwards [extChartAt_source_mem_nhdsWithin' h'y] with z hz

Premises used: extChartAt_source_mem_nhdsWithin'
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source
h''y : (↑(extChartAt I x).symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y)
this :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y))
z : M
hz : z ∈ (extChartAt I x).source
⊢ ((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) z = id z

Tactic:
simp only [Function.comp_def, PartialEquiv.left_inv (extChartAt I x) hz, id_eq]

Premises used: extChartAt, Function.comp_def, PartialEquiv.left_inv, id_eq
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source
h''y : (↑(extChartAt I x).symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y)
this :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y))
⊢ ((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) ((↑(extChartAt I x).symm : E → M) y) =
    id ((↑(extChartAt I x).symm : E → M) y)

Tactic:
simp only [Function.comp_def, PartialEquiv.right_inv (extChartAt I x) hy, id_eq]

Premises used: extChartAt, PartialEquiv.right_inv, Function.comp_def, id_eq
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
this : y = (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)
⊢ Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)) →L[𝕜]
      TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)))
    (ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) y))
        (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))) :
      TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)) →L[𝕜]
        TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))) :
      TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)) →L[𝕜]
        TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)))

Tactic:
mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt ((extChartAt I x).map_source hy)

Premises used: extChartAt, PartialEquiv.map_source, mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
this : y = (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)
⊢ Eq (α := TangentSpace I y →L[𝕜] TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)))
    (ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) y))
      (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) y))
      (mfderiv% (↑(extChartAt I x) : M → E) y))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I y))

Tactic:
convert! mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt ((extChartAt I x).map_source hy)

Premises used: extChartAt, PartialEquiv.map_source, mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
⊢ ContinuousLinearMap.IsInvertible (M := TangentSpace 𝓘(𝕜, E) y) (M₂ :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y)

Tactic:
ContinuousLinearMap.IsInvertible.of_inverse
    (mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt hy)
    (mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm hy)

Premises used: mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm, mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt, ContinuousLinearMap.IsInvertible.of_inverse
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
⊢ (↑(extChartAt I x) : M → E) y ∈ (extChartAt I x).target

Tactic:
have h'y : extChartAt I x y ∈ (extChartAt I x).target := (extChartAt I x).map_source hy
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
h'y : (↑(extChartAt I x) : M → E) y ∈ (extChartAt I x).target
⊢ ContinuousLinearMap.IsInvertible (M :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))) (M₂ :=
    TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) y))
    (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)) :
      TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)) →L[𝕜]
        TangentSpace 𝓘(𝕜, E)
          ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))))

Tactic:
have Z := ContinuousLinearMap.IsInvertible.of_inverse
    (mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm h'y)
    (mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt h'y)
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
h'y : (↑(extChartAt I x) : M → E) y ∈ (extChartAt I x).target
Z :
  ContinuousLinearMap.IsInvertible (M :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))) (M₂ :=
    TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) y))
    (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)) :
      TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)) →L[𝕜]
        TangentSpace 𝓘(𝕜, E)
          ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))))
⊢ (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y) = y

Tactic:
have : (extChartAt I x).symm ((extChartAt I x) y) = y := (extChartAt I x).left_inv hy
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
h'y : (↑(extChartAt I x) : M → E) y ∈ (extChartAt I x).target
Z :
  ContinuousLinearMap.IsInvertible (M :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))) (M₂ :=
    TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) y))
    (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)) :
      TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)) →L[𝕜]
        TangentSpace 𝓘(𝕜, E)
          ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))))
this : (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y) = y
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (Z :
      ContinuousLinearMap.IsInvertible (M := TangentSpace I y) (M₂ :=
        TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) y)) (mfderiv% (↑(extChartAt I x) : M → E) y))
    (this : (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y) = y),
    ContinuousLinearMap.IsInvertible (M := TangentSpace I y) (M₂ :=
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) y)) (mfderiv% (↑(extChartAt I x) : M → E) y)
⊢ ContinuousLinearMap.IsInvertible (M := TangentSpace I y) (M₂ := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) y))
    (mfderiv% (↑(extChartAt I x) : M → E) y)

Tactic:
rwa [this] at Z
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x₀ x : M
hx : x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x₀)).source
⊢ MDiffAt (↑(extChartAt I x₀) : M → E) x

Tactic:
have : MDiffAt (extChartAt I x₀) x := mdifferentiableAt_extChartAt hx
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x₀ x : M
hx : x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x₀)).source
this : MDiffAt ((↑I : H → E) ∘ (↑(chartAt H x₀) : M → H)) x
⊢ Eq (α := TangentSpace I x →L[𝕜] E)
    (Trivialization.continuousLinearMapAt 𝕜 (E := TangentSpace I) (trivializationAt E (TangentSpace I) x₀) x)
    (mfderiv% (↑(extChartAt I x₀) : M → E) x)

Tactic:
simp [hx, mfderiv, this]

Premises used: mfderiv
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x₀ x : M
hx : x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x₀)).source
⊢ (↑I : H → E) ((↑(chartAt H x₀) : M → H) x) ∈ (extChartAt I x₀).target

Tactic:
simp [hx]
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x₀ x : M
hx : x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x₀)).source
⊢ MDiffAt[range (↑I : H → E)] ((↑(OpenPartialHomeomorph.symm (chartAt H x₀)) : H → M) ∘ (↑I.symm : E → H))
    ((↑I : H → E) ((↑(chartAt H x₀) : M → H) x))

Tactic:
simpa using mdifferentiableWithinAt_extChartAt_symm (by simp [hx])

Premises used: mdifferentiableWithinAt_extChartAt_symm
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x₀ x : M
hx : x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x₀)).source
⊢ MDiffAt[range (↑I : H → E)] ((↑(OpenPartialHomeomorph.symm (chartAt H x₀)) : H → M) ∘ (↑I.symm : E → H))
    ((↑I : H → E) ((↑(chartAt H x₀) : M → H) x))

Tactic:
have : MDiffAt[range I] ((chartAt H x₀).symm ∘ I.symm) (I (chartAt H x₀ x)) := by
    simpa using mdifferentiableWithinAt_extChartAt_symm (by simp [hx])
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x₀ x : M
hx : x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x₀)).source
this :
  MDiffAt[range (↑I : H → E)] ((↑(OpenPartialHomeomorph.symm (chartAt H x₀)) : H → M) ∘ (↑I.symm : E → H))
    ((↑I : H → E) ((↑(chartAt H x₀) : M → H) x))
⊢ Eq (α := E →L[𝕜] TangentSpace I x)
    (Trivialization.symmL 𝕜 (E := TangentSpace I) (trivializationAt E (TangentSpace I) x₀) x)
    (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x₀).symm : E → M) (range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x))

Tactic:
simp [hx, mfderivWithin, this]

Premises used: mfderivWithin
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
set :
  let φ := extChartAt I x;
  Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 ((↑φ : M → E) ∘ (↑φ.symm : E → M)) (range (↑I : H → E)) ((↑φ : M → E) x))
    (ContinuousLinearMap.id 𝕜 E)
⊢ Eq (α := E →L[𝕜] E)
    (fderivWithin 𝕜 ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x))
    (ContinuousLinearMap.id 𝕜 E)

Tactic:
set φ := extChartAt I x

Premises used: extChartAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
φ : PartialEquiv M E := extChartAt I x
⊢ (↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M) =ᶠ[𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x]
    id

Tactic:
have eq_nhd : ((extChartAt I x) ∘ (extChartAt I x).symm) =ᶠ[𝓝[range I] (extChartAt I x x)] id :=
    Filter.eventuallyEq_of_mem (extChartAt_target_mem_nhdsWithin x)
      (fun _ ↦ (extChartAt I x).right_inv)