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
U : UniqueMDiffWithinAt 𝓘(𝕜, E) (range (↑I : H → E)) y
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
⊢ ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) y = id 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
⊢ y = (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)

Tactic:
have : y = (extChartAt I x).symm (extChartAt I x y) := ((extChartAt I x).left_inv hy).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 y : M
hy : y ∈ (extChartAt I x).source
this : y = (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)
⊢ Eq (α :=
    TangentSpace 𝓘(𝕜, E) ((↑(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))))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)))
      (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) ((↑(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)))
    (ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) y)))

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

Premises used: extChartAt, PartialEquiv.map_source, mfderiv_extChartAt_comp_mfderivWithin_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 y : M
hy : y ∈ (extChartAt I x).source
this : y = (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)
⊢ Eq (α :=
    TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) y) →L[𝕜] TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) y))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I y) (mfderiv% (↑(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)))
    (ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) y)))

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

Premises used: extChartAt, PartialEquiv.map_source, mfderiv_extChartAt_comp_mfderivWithin_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 : M
y : E
hy : y ∈ (extChartAt I x).target
⊢ (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source

Tactic:
have h'y : (extChartAt I x).symm y ∈ (extChartAt I x).source := (extChartAt I x).map_target 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 : M
y : E
hy : y ∈ (extChartAt I x).target
h'y rwa rwa₁ rwa₂ rwa₃ : (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source
⊢ (↑(extChartAt I x).symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source

Tactic:
rwa [← extChartAt_source (I := I)]

Premises used: extChartAt_source
-- 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
⊢ (↑(extChartAt I x).symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source

Tactic:
have h''y : (extChartAt I x).symm y ∈ (chartAt H x).source := by
    rwa [← extChartAt_source (I := I)]
-- 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
⊢ UniqueMDiffWithinAt I (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y)

Tactic:
have U' : UniqueMDiffWithinAt I (extChartAt I x).source ((extChartAt I x).symm y) :=
    (isOpen_extChartAt_source x).uniqueMDiffWithinAt 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 : 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)
rw : MDiffAt (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)
⊢ 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))

Tactic:
rw [mfderivWithin_eq_mfderiv U']

Premises used: mfderivWithin_eq_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 : 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)
⊢ MDiffAt (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)

Tactic:
mdifferentiableAt_extChartAt h''y

Premises used: mdifferentiableAt_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
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)
⊢ MDiffAt (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)

Tactic:
exact mdifferentiableAt_extChartAt h''y

Premises used: mdifferentiableAt_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
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)
⊢ 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))

Tactic:
have : mfderiv% (extChartAt I x) ((extChartAt I x).symm y)
      = mfderiv[(extChartAt I x).source] (extChartAt I x) ((extChartAt I x).symm y) := by
    rw [mfderivWithin_eq_mfderiv U']
    exact mdifferentiableAt_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 : 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)))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I ((↑(extChartAt I x).symm : E → M) y)))
hg : MDiffAt[range (↑I : H → E)] (↑(extChartAt I x).symm : E → M) y
hf : MDiffAt[(extChartAt I x).source] (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)
h : (extChartAt I x).source ⊆ (↑(extChartAt I x) : M → E) ⁻¹' range (↑I : H → E)
hxs : UniqueMDiffWithinAt I (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y)
hy₁ : (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y) = y
⊢ Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
    (ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(𝕜, E) y)
      (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y)
      (mfderiv% (↑(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 [this, ← mfderivWithin_comp_of_eq]

Premises used: mfderivWithin_comp_of_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))
⊢ MDiffAt[range (↑I : H → E)] (↑(extChartAt I x).symm : E → M) y

Tactic:
mdifferentiableWithinAt_extChartAt_symm hy

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 : 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))
⊢ MDiffAt[range (↑I : H → E)] (↑(extChartAt I x).symm : E → M) y

Tactic:
exact mdifferentiableWithinAt_extChartAt_symm hy

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 : 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))
⊢ MDiffAt[(extChartAt I x).source] (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)

Tactic:
(mdifferentiableAt_extChartAt h''y).mdifferentiableWithinAt

Premises used: MDifferentiableAt.mdifferentiableWithinAt, mdifferentiableAt_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
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))
⊢ MDiffAt[(extChartAt I x).source] (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)

Tactic:
exact (mdifferentiableAt_extChartAt h''y).mdifferentiableWithinAt

Premises used: MDifferentiableAt.mdifferentiableWithinAt, mdifferentiableAt_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
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
h : (↑(extChartAt I x) : M → E) z ∈ (extChartAt I x).target
⊢ z ∈ (↑(extChartAt I x) : M → E) ⁻¹' range (↑I : H → E)

Tactic:
apply extChartAt_target_subset_range x

Premises used: extChartAt_target_subset_range
-- 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) : M → E) z ∈ (extChartAt I x).target

Tactic:
PartialEquiv.map_source (extChartAt I x) hz

Premises used: extChartAt, PartialEquiv.map_source
-- 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) : M → E) z ∈ (extChartAt I x).target

Tactic:
exact PartialEquiv.map_source (extChartAt I x) hz

Premises used: extChartAt, PartialEquiv.map_source
-- 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))
⊢ UniqueMDiffWithinAt I (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y)

Tactic:
U'
-- 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))
⊢ UniqueMDiffWithinAt I (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y)

Tactic:
exact U'