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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
e : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
e' : OpenPartialHomeomorph M' M''
he' : MDifferentiable I' I'' e'
x : M''
hx : x ∈ e'.target ∧ (↑e'.symm : M'' → M') x ∈ e.target
⊢ MDiffAt[(e ≫ₕ e').target] (↑(e ≫ₕ e').symm : M'' → M) x

Tactic:
exact
      ((he.symm.mdifferentiableAt hx.2).comp _
          (he'.symm.mdifferentiableAt hx.1)).mdifferentiableWithinAt

Premises used: MDifferentiableAt.mdifferentiableWithinAt, And.right, And.left, OpenPartialHomeomorph.MDifferentiable.mdifferentiableAt, MDifferentiableAt.comp, OpenPartialHomeomorph.MDifferentiable.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
h : y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
⊢ HasMFDerivAt I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) y (mfderiv% (↑(chartAt H x) : M → H) y)

Tactic:
I.hasMFDerivAt.comp y ((mdifferentiable_chart x).mdifferentiableAt h).hasMFDerivAt

Premises used: ContinuousLinearMap.comp, mfderiv, mdifferentiable_chart, ModelWithCorners.hasMFDerivAt, MDifferentiableAt.hasMFDerivAt, ModelWithCorners.ofTargetUniv, ModelWithCorners.toFun', instModuleTangentSpace._aux_1, TangentSpace, instTopologicalSpaceTangentSpace._aux_1, OpenPartialHomeomorph.MDifferentiable.mdifferentiableAt, modelWithCornersSelf, HasMFDerivAt.comp, instAddCommGroupTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_4, ite
-- 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
s : Set M
x y : M
h : y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
⊢ HasMFDerivWithinAt I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) s y (mfderiv% (↑(chartAt H x) : M → H) y)

Tactic:
(hasMFDerivAt_extChartAt h).hasMFDerivWithinAt

Premises used: hasMFDerivAt_extChartAt, HasMFDerivAt.hasMFDerivWithinAt
-- 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
h : y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
⊢ MDiffAt (↑(extChartAt I x) : M → E) y

Tactic:
(hasMFDerivAt_extChartAt h).mdifferentiableAt

Premises used: hasMFDerivAt_extChartAt, HasMFDerivAt.mdifferentiableAt
-- 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
⊢ MDiff[(OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source] (↑(extChartAt I x) : M → E)

Tactic:
fun _y hy ↦ (hasMFDerivWithinAt_extChartAt hy).mdifferentiableWithinAt

Premises used: hasMFDerivWithinAt_extChartAt, HasMFDerivWithinAt.mdifferentiableWithinAt, MDifferentiableOn
-- 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
z : E
h : z ∈ (extChartAt I x).target
⊢ MDiffAt[range (↑I : H → E)] (↑I.symm : E → H) z

Tactic:
have Z := I.mdifferentiableWithinAt_symm (extChartAt_target_subset_range x h)
-- 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
z : E
h : z ∈ (extChartAt I x).target
Z : MDiffAt[range (↑I : H → E)] (↑I.symm : E → H) z
apply : MDiffAt (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).2 ((↑I.symm : E → H) z)
⊢ MDiffAt[range (↑I : H → E)] (↑(extChartAt I x).symm : E → M) z

Tactic:
apply MDifferentiableAt.comp_mdifferentiableWithinAt (I' := I) _ _ Z

Premises used: MDifferentiableAt.comp_mdifferentiableWithinAt
-- 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
z : E
h : z ∈ (extChartAt I x).target
Z : MDiffAt[range (↑I : H → E)] (↑I.symm : E → H) z
apply :
  Membership.mem (γ := Set H) (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (ChartedSpace.chartAt x)))
    ((↑I.symm : E → H) z)
⊢ MDiffAt (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).2 ((↑I.symm : E → H) z)

Tactic:
apply mdifferentiableAt_atlas_symm (ChartedSpace.chart_mem_atlas x)

Premises used: ChartedSpace.chart_mem_atlas, mdifferentiableAt_atlas_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
z : E
h : z ∈ (extChartAt I x).target
Z : MDiffAt[range (↑I : H → E)] (↑I.symm : E → H) z
⊢ (∃ (y : H), (↑I : H → E) y = z) ∧ (↑I.symm : E → H) z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target

Tactic:
simp only [extChartAt, OpenPartialHomeomorph.extend, PartialEquiv.trans_target,
    ModelWithCorners.target_eq, ModelWithCorners.toPartialEquiv_coe_symm, mem_inter_iff, mem_range,
    mem_preimage] at h

Premises used: Set.mem_range, extChartAt, Set.mem_inter_iff, ModelWithCorners.target_eq, PartialEquiv.trans_target, Set.mem_preimage, OpenPartialHomeomorph.extend, ModelWithCorners.toPartialEquiv_coe_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
z : E
Z : MDiffAt[range (↑I : H → E)] (↑I.symm : E → H) z
h : (∃ (y : H), (↑I : H → E) y = z) ∧ (↑I.symm : E → H) z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target
⊢ Membership.mem (γ := Set H) (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (ChartedSpace.chartAt x)))
    ((↑I.symm : E → H) z)

Tactic:
h.2

Premises used: Set.Mem, And.right
-- 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
z : E
Z : MDiffAt[range (↑I : H → E)] (↑I.symm : E → H) z
h : (∃ (y : H), (↑I : H → E) y = z) ∧ (↑I.symm : E → H) z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target
⊢ Membership.mem (γ := Set H) (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (ChartedSpace.chartAt x)))
    ((↑I.symm : E → H) z)

Tactic:
exact h.2

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

Tactic:
(mdifferentiableWithinAt_extChartAt_symm hy).mono (extChartAt_target_subset_range x)

Premises used: MDifferentiableWithinAt.mono, extChartAt_target_subset_range, 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
⊢ MDiffAt[(extChartAt I x).target] (↑(extChartAt I x).symm : E → M) y

Tactic:
exact (mdifferentiableWithinAt_extChartAt_symm hy).mono (extChartAt_target_subset_range x)

Premises used: MDifferentiableWithinAt.mono, extChartAt_target_subset_range, 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
a : y ∈ range (↑I : H → E)
⊢ UniqueMDiffWithinAt 𝓘(𝕜, E) (range (↑I : H → E)) y

Tactic:
apply I.uniqueMDiffOn

Premises used: ModelWithCorners.uniqueMDiffOn
-- 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
⊢ y ∈ range (↑I : H → E)

Tactic:
extChartAt_target_subset_range x hy

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
⊢ y ∈ range (↑I : H → E)

Tactic:
exact extChartAt_target_subset_range x hy

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
⊢ UniqueMDiffWithinAt 𝓘(𝕜, E) (range (↑I : H → E)) y

Tactic:
have U : UniqueMDiffWithinAt 𝓘(𝕜, E) (range ↑I) y := by
    apply I.uniqueMDiffOn
    exact extChartAt_target_subset_range x 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
U : UniqueMDiffWithinAt 𝓘(𝕜, E) (range (↑I : H → E)) y
⊢ (↑(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
U : UniqueMDiffWithinAt 𝓘(𝕜, E) (range (↑I : H → E)) y
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
U : UniqueMDiffWithinAt 𝓘(𝕜, E) (range (↑I : H → E)) y
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
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
rw :
  Eq (α :=
    TangentSpace 𝓘(𝕜, E) y →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      y)
    (ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) y))
hg : MDiffAt (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)
hf : MDiffAt[range (↑I : H → E)] (↑(extChartAt I x).symm : E → M) y
hxs : UniqueMDiffWithinAt 𝓘(𝕜, E) (range (↑I : H → E)) y
⊢ Eq (α :=
    TangentSpace 𝓘(𝕜, E) y →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
      (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
      (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y))
    (ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) y))

Tactic:
rw [← mfderiv_comp_mfderivWithin]

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

Tactic:
apply 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
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
⊢ 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
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
⊢ 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
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
⊢ UniqueMDiffWithinAt 𝓘(𝕜, E) (range (↑I : H → E)) 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
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
⊢ UniqueMDiffWithinAt 𝓘(𝕜, E) (range (↑I : H → E)) y

Tactic:
exact 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
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
rw :
  Eq (α :=
    TangentSpace 𝓘(𝕜, E) y →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      y)
    (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E) id (range (↑I : H → E)) y)
⊢ Eq (α :=
    TangentSpace 𝓘(𝕜, E) y →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      y)
    (ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) 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
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
hL : (↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M) =ᶠ[𝓝[range (↑I : H → E)] y] id
hx : ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) y = id y
⊢ Eq (α :=
    TangentSpace 𝓘(𝕜, E) y →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      y)
    (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E) id (range (↑I : H → E)) 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
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
h :
  ∀ (z : E) (hz : z ∈ (extChartAt I x).target),
    ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) z = id z
⊢ (↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M) =ᶠ[𝓝[range (↑I : H → E)] y] id

Tactic:
filter_upwards [extChartAt_target_mem_nhdsWithin_of_mem hy] with z hz

Premises used: extChartAt_target_mem_nhdsWithin_of_mem
-- 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
z : E
hz : z ∈ (extChartAt I x).target
⊢ ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) z = id z

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

Premises used: extChartAt, PartialEquiv.right_inv, Function.comp_def, id_eq