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
e : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
x : H
hx : x ∈ e.target
mem :
  (↑I : H → E) x ∈
    (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x))).source ∩
      range (↑I : H → E)
this : e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x) ∈ contDiffGroupoid 1 I
A :
  ContDiffOn 𝕜 1 ((↑I : H → E) ∘ (↑(e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x)) : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x))).source ∩
      range (↑I : H → E))
B :
  DifferentiableWithinAt 𝕜
    ((↑I : H → E) ∘ ((↑(chartAt H ((↑e.symm : H → M) x)) : M → H) ∘ (↑e.symm : H → M)) ∘ (↑I.symm : E → H))
    (range (↑I : H → E) ∩
      ((↑I.symm : E → H) ⁻¹' e.target ∩
        (↑I.symm : E → H) ⁻¹'
          (↑e.symm : H → M) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑e.symm : H → M) x))).source))
    ((↑I : H → E) x)
⊢ (↑I.symm : E → H) ⁻¹' e.target ∩
      (↑I.symm : E → H) ⁻¹'
        (↑e.symm : H → M) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑e.symm : H → M) x))).source ∈
    𝓝 ((↑I : H → E) x)

Tactic:
apply IsOpen.mem_nhds ((OpenPartialHomeomorph.open_source _).preimage I.continuous_symm) mem.1

Premises used: OpenPartialHomeomorph.open_source, ModelWithCorners.continuous_symm, And.left, IsOpen.mem_nhds, IsOpen.preimage
-- 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
e : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
⊢ MDiff[e.target] (↑e.symm : H → M)

Tactic:
fun _x hx => (mdifferentiableAt_atlas_symm h hx).mdifferentiableWithinAt

Premises used: MDifferentiableAt.mdifferentiableWithinAt, MDifferentiableOn, 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
e : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
⊢ OpenPartialHomeomorph.MDifferentiable I I e

Tactic:
⟨mdifferentiableOn_atlas h, mdifferentiableOn_atlas_symm h⟩

Premises used: mdifferentiableOn_atlas, And.intro, OpenPartialHomeomorph.MDifferentiable, mdifferentiableOn_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
⊢ OpenPartialHomeomorph.MDifferentiable I I (chartAt H x)

Tactic:
mdifferentiable_of_mem_atlas (chart_mem_atlas _ _)

Premises used: chart_mem_atlas, mdifferentiable_of_mem_atlas
-- 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 : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
⊢ MDifferentiable I' I e.symm

Tactic:
he.symm

Premises used: PartialEquiv.symm, OpenPartialHomeomorph.MDifferentiable, And.symm, OpenPartialHomeomorph.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
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 : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
⊢ MDiffAt (↑e : M → M') x

Tactic:
(he.1 x hx).mdifferentiableAt (e.open_source.mem_nhds hx)

Premises used: OpenPartialHomeomorph.open_source, MDifferentiableWithinAt.mdifferentiableAt, And.left, IsOpen.mem_nhds
-- 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 : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
x : M'
hx : x ∈ e.target
⊢ MDiffAt (↑e.symm : M' → M) x

Tactic:
(he.2 x hx).mdifferentiableAt (e.open_target.mem_nhds hx)

Premises used: And.right, MDifferentiableWithinAt.mdifferentiableAt, IsOpen.mem_nhds, OpenPartialHomeomorph.open_target
-- 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 : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
⊢ Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (((↑e.symm : M' → M) ∘ (↑e : M → M')) x))
    (mfderiv% ((↑e.symm : M' → M) ∘ (↑e : M → M')) x)
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' ((↑e : M → M') x)) (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x))
      (mfderiv% (↑e : M → M') x))

Tactic:
have : mfderiv% (e.symm ∘ e) x = (mfderiv% e.symm (e x)).comp (mfderiv% e x) :=
    mfderiv_comp x (he.mdifferentiableAt_symm (e.map_source hx)) (he.mdifferentiableAt 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
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 : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
this :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (((↑e.symm : M' → M) ∘ (↑e : M → M')) x))
    (mfderiv% ((↑e.symm : M' → M) ∘ (↑e : M → M')) x)
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' ((↑e : M → M') x)) (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x))
      (mfderiv% (↑e : M → M') x))
rw :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))
    (mfderiv% ((↑e.symm : M' → M) ∘ (↑e : M → M')) x) (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
⊢ Eq (α := TangentSpace I x →L[𝕜] TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' ((↑e : M → M') x)) (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x))
      (mfderiv% (↑e : M → M') x))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I x))

Tactic:
rw [← this]
-- 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 : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
this :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (((↑e.symm : M' → M) ∘ (↑e : M → M')) x))
    (mfderiv% ((↑e.symm : M' → M) ∘ (↑e : M → M')) x)
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' ((↑e : M → M') x)) (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x))
      (mfderiv% (↑e : M → M') x))
⊢ Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (id x)) (mfderiv% id x) (ContinuousLinearMap.id 𝕜 (TangentSpace I x))

Tactic:
have : mfderiv% (_root_.id : M → M) x = ContinuousLinearMap.id _ _ := mfderiv_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
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 : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
this_1 :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (((↑e.symm : M' → M) ∘ (↑e : M → M')) x))
    (mfderiv% ((↑e.symm : M' → M) ∘ (↑e : M → M')) x)
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' ((↑e : M → M') x)) (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x))
      (mfderiv% (↑e : M → M') x))
this :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (id x)) (mfderiv% id x) (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
rw :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))
    (mfderiv% ((↑e.symm : M' → M) ∘ (↑e : M → M')) x) (mfderiv% id x)
⊢ Eq (α := TangentSpace I x →L[𝕜] TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))
    (mfderiv% ((↑e.symm : M' → M) ∘ (↑e : M → M')) x) (ContinuousLinearMap.id 𝕜 (TangentSpace I x))

Tactic:
rw [← this]
-- 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 : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
this_1 :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (((↑e.symm : M' → M) ∘ (↑e : M → M')) x))
    (mfderiv% ((↑e.symm : M' → M) ∘ (↑e : M → M')) x)
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' ((↑e : M → M') x)) (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x))
      (mfderiv% (↑e : M → M') x))
this :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (id x)) (mfderiv% id x) (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
hL : (↑e.symm : M' → M) ∘ (↑e : M → M') =ᶠ[𝓝 x] id
⊢ Eq (α := TangentSpace I x →L[𝕜] TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))
    (mfderiv% ((↑e.symm : M' → M) ∘ (↑e : M → M')) x) (mfderiv% id x)

Tactic:
apply Filter.EventuallyEq.mfderiv_eq

Premises used: Filter.EventuallyEq.mfderiv_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
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 : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
this_1 :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (((↑e.symm : M' → M) ∘ (↑e : M → M')) x))
    (mfderiv% ((↑e.symm : M' → M) ∘ (↑e : M → M')) x)
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' ((↑e : M → M') x)) (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x))
      (mfderiv% (↑e : M → M') x))
this :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (id x)) (mfderiv% id x) (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
⊢ e.source ∈ 𝓝 x

Tactic:
have : e.source ∈ 𝓝 x := e.open_source.mem_nhds 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
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 : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
this_1 :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (((↑e.symm : M' → M) ∘ (↑e : M → M')) x))
    (mfderiv% ((↑e.symm : M' → M) ∘ (↑e : M → M')) x)
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' ((↑e : M → M') x)) (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x))
      (mfderiv% (↑e : M → M') x))
this_2 :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (id x)) (mfderiv% id x) (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
this : e.source ∈ 𝓝 x
mfld_set_tac mfld_set_tac₁ mfld_set_tac₂ mfld_set_tac₃ mfld_set_tac₄ :
  ∀ ⦃my_y : M⦄,
    my_y ∈ e.source →
      Membership.mem (γ := Set M) {x : M | (fun (x : M) ↦ ((↑e.symm : M' → M) ∘ (↑e : M → M')) x = id x) x} my_y
⊢ e.source ⊆ {x : M | (fun (x : M) ↦ ((↑e.symm : M' → M) ∘ (↑e : M → M')) x = id x) x}

Tactic:
mfld_set_tac
-- 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 : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
this_1 :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (((↑e.symm : M' → M) ∘ (↑e : M → M')) x))
    (mfderiv% ((↑e.symm : M' → M) ∘ (↑e : M → M')) x)
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' ((↑e : M → M') x)) (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x))
      (mfderiv% (↑e : M → M') x))
this_2 :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (id x)) (mfderiv% id x) (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
this : e.source ∈ 𝓝 x
⊢ (↑e.symm : M' → M) ∘ (↑e : M → M') =ᶠ[𝓝 x] id

Tactic:
exact Filter.mem_of_superset this (by mfld_set_tac)

Premises used: Filter.mem_of_superset
-- 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 : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
x : M'
hx : x ∈ e.target
⊢ Eq (α := TangentSpace I' x →L[𝕜] TangentSpace I' ((↑e : M → M') ((↑e.symm : M' → M) x)))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I ((↑e.symm : M' → M) x))
      (mfderiv% (↑e : M → M') ((↑e.symm : M' → M) x)) (mfderiv% (↑e.symm : M' → M) x))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I' x))

Tactic:
he.symm.symm_comp_deriv hx

Premises used: PartialEquiv.symm, TangentSpace, OpenPartialHomeomorph.MDifferentiable.symm_comp_deriv, OpenPartialHomeomorph.symm, 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
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_1 : MDifferentiable I I' e
e' : OpenPartialHomeomorph M' M''
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
y : TangentSpace I x
⊢ (ContinuousLinearMap.id 𝕜 (TangentSpace I x) : (a : TangentSpace I x) → TangentSpace I x) y = y

Tactic:
have : (ContinuousLinearMap.id _ _ : TangentSpace I x →L[𝕜] TangentSpace I x) y = y := rfl
-- 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_1 : MDifferentiable I I' e
e' : OpenPartialHomeomorph M' M''
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
y : TangentSpace I x
this : (ContinuousLinearMap.id 𝕜 (TangentSpace I x) : (a : TangentSpace I x) → TangentSpace I x) y = y
rw :
  (((ContinuousLinearMap.comp (M₂ := TangentSpace I' ((↑e : M → M') x)) (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x))
            (mfderiv% (↑e : M → M') x) :
          TangentSpace I x →L[𝕜] TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x))) :
        (a : TangentSpace I x) → TangentSpace I x)
      y :
    TangentSpace I x)
| y

Tactic:
rw [← this, ← he.symm_comp_deriv hx]

Premises used: OpenPartialHomeomorph.MDifferentiable.symm_comp_deriv
-- 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_1 : MDifferentiable I I' e
e' : OpenPartialHomeomorph M' M''
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
y : TangentSpace I x
this : (ContinuousLinearMap.id 𝕜 (TangentSpace I x) : (a : TangentSpace I x) → TangentSpace I x) y = y
conv_rhs :
  Eq.{u_2 + 1} (α := TangentSpace I x)
    (((mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x) :
            ContinuousLinearMap.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (TangentSpace I' ((↑e : M → M') x))
              (TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))) :
          (a : TangentSpace I' ((↑e : M → M') x)) → TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))
        (AddHom.toFun
          (LinearMap.toAddHom (↑(mfderiv% (↑e : M → M') x) : TangentSpace I x →ₗ[𝕜] TangentSpace I' ((↑e : M → M') x)))
          y) :
      TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))
    (((ContinuousLinearMap.comp (M₂ := TangentSpace I' ((↑e : M → M') x))
              (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x)) (mfderiv% (↑e : M → M') x) :
            TangentSpace I x →L[𝕜] TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x))) :
          (a : TangentSpace I x) → TangentSpace I x)
        y :
      TangentSpace I x)
⊢ ((mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x) :
          ContinuousLinearMap.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (TangentSpace I' ((↑e : M → M') x))
            (TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))) :
        (a : TangentSpace I' ((↑e : M → M') x)) → TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))
      (AddHom.toFun
        (LinearMap.toAddHom (↑(mfderiv% (↑e : M → M') x) : TangentSpace I x →ₗ[𝕜] TangentSpace I' ((↑e : M → M') x)))
        y) =
    y

Tactic:
conv_rhs => rw [← this, ← he.symm_comp_deriv hx]

Premises used: OpenPartialHomeomorph.MDifferentiable.symm_comp_deriv
-- 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_1 : MDifferentiable I I' e
e' : OpenPartialHomeomorph M' M''
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
y : TangentSpace I x
this : (ContinuousLinearMap.id 𝕜 (TangentSpace I x) : (a : TangentSpace I x) → TangentSpace I x) y = y
⊢ Eq.{u_2 + 1} (α := TangentSpace I x)
    (((mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x) :
            ContinuousLinearMap.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (TangentSpace I' ((↑e : M → M') x))
              (TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))) :
          (a : TangentSpace I' ((↑e : M → M') x)) → TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))
        (AddHom.toFun
          (LinearMap.toAddHom (↑(mfderiv% (↑e : M → M') x) : TangentSpace I x →ₗ[𝕜] TangentSpace I' ((↑e : M → M') x)))
          y) :
      TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))
    (((ContinuousLinearMap.comp (M₂ := TangentSpace I' ((↑e : M → M') x))
              (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x)) (mfderiv% (↑e : M → M') x) :
            TangentSpace I x →L[𝕜] TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x))) :
          (a : TangentSpace I x) → TangentSpace I x)
        y :
      TangentSpace I x)

Tactic:
rfl