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 : M
hx : x ∈ e.source
⊢ ContinuousAt (↑e : M → H) x ∧
    DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e : M → H)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)

Tactic:
⟨(e.continuousOn x hx).continuousAt (e.open_source.mem_nhds hx), ?_⟩

Premises used: OpenPartialHomeomorph.open_source, OpenPartialHomeomorph.continuousOn, And.intro, IsOpen.mem_nhds, ContinuousWithinAt.continuousAt
-- 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 : M
hx : x ∈ e.source
refine :
  DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e : M → H)) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
⊢ ContinuousAt (↑e : M → H) x ∧
    DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e : M → H)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)

Tactic:
refine ⟨(e.continuousOn x hx).continuousAt (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
inst_6 : IsManifold I 1 M
e : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
x : M
hx : x ∈ e.source
⊢ (↑I : H → E) ((↑(chartAt H x) : M → H) x) ∈
    (↑I.symm : E → H) ⁻¹'
        (OpenPartialHomeomorph.toPartialEquiv (OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e)).source ∩
      range (↑I : H → E)

Tactic:
simp only [hx, mfld_simps]
-- 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 : M
hx : x ∈ e.source
⊢ (↑I : H → E) ((↑(chartAt H x) : M → H) x) ∈
    (↑I.symm : E → H) ⁻¹'
        (OpenPartialHomeomorph.toPartialEquiv (OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e)).source ∩
      range (↑I : H → E)

Tactic:
have mem :
    I ((chartAt H x : M → H) x) ∈ I.symm ⁻¹' ((chartAt H x).symm ≫ₕ e).source ∩ range I := by
    simp only [hx, mfld_simps]
-- 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 : M
hx : x ∈ e.source
mem :
  (↑I : H → E) ((↑(chartAt H x) : M → H) x) ∈
    (↑I.symm : E → H) ⁻¹'
        (OpenPartialHomeomorph.toPartialEquiv (OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e)).source ∩
      range (↑I : H → E)
⊢ OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e ∈ contDiffGroupoid 1 I

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

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

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

Tactic:
rw [inter_comm, differentiableWithinAt_inter] at B

Premises used: differentiableWithinAt_inter, Set.inter_comm
-- 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 : M
hx : x ∈ e.source
mem :
  (↑I : H → E) ((↑(chartAt H x) : M → H) x) ∈
    (↑I.symm : E → H) ⁻¹'
        (OpenPartialHomeomorph.toPartialEquiv (OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e)).source ∩
      range (↑I : H → E)
this : OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e ∈ contDiffGroupoid 1 I
A :
  ContDiffOn 𝕜 1 ((↑I : H → E) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e) : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹'
        (OpenPartialHomeomorph.toPartialEquiv (OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e)).source ∩
      range (↑I : H → E))
B :
  DifferentiableWithinAt 𝕜
    ((↑I : H → E) ∘ ((↑e : M → H) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) ∘ (↑I.symm : E → H))
    (range (↑I : H → E)) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e : M → H)) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
simpa only [mfld_simps]
-- 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 : M
hx : x ∈ e.source
mem :
  (↑I : H → E) ((↑(chartAt H x) : M → H) x) ∈
    (↑I.symm : E → H) ⁻¹'
        (OpenPartialHomeomorph.toPartialEquiv (OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e)).source ∩
      range (↑I : H → E)
this : OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e ∈ contDiffGroupoid 1 I
A :
  ContDiffOn 𝕜 1 ((↑I : H → E) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e) : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹'
        (OpenPartialHomeomorph.toPartialEquiv (OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e)).source ∩
      range (↑I : H → E))
B :
  DifferentiableWithinAt 𝕜
    ((↑I : H → E) ∘ ((↑e : M → H) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) ∘ (↑I.symm : E → H))
    (range (↑I : H → E) ∩
      ((↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
        (↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' e.source))
    ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
⊢ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
      (↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' e.source ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) 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.source] (↑e : M → H)

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

Premises used: MDifferentiableAt.mdifferentiableWithinAt, MDifferentiableOn, mdifferentiableAt_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
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
rw :
  ContinuousAt (↑e.symm : H → M) x ∧
    DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e.symm : H → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : H → E) x)
⊢ MDiffAt (↑e.symm : H → M) x

Tactic:
rw [mdifferentiableAt_iff]

Premises used: mdifferentiableAt_iff
-- 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
⊢ ContinuousAt (↑e.symm : H → M) x ∧
    DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e.symm : H → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : H → E) x)

Tactic:
⟨(e.continuousOn_symm x hx).continuousAt (e.open_target.mem_nhds hx), ?_⟩

Premises used: And.intro, IsOpen.mem_nhds, OpenPartialHomeomorph.continuousOn_symm, OpenPartialHomeomorph.open_target, ContinuousWithinAt.continuousAt
-- 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
refine :
  DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e.symm : H → M)) (range (↑I : H → E))
    ((↑(extChartAt I x) : H → E) x)
⊢ ContinuousAt (↑e.symm : H → M) x ∧
    DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e.symm : H → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : H → E) x)

Tactic:
refine ⟨(e.continuousOn_symm x hx).continuousAt (e.open_target.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
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
⊢ (↑I : H → E) x ∈
    (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x))).source ∩
      range (↑I : H → E)

Tactic:
simp only [hx, mfld_simps]
-- 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
⊢ (↑I : H → E) x ∈
    (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x))).source ∩
      range (↑I : H → E)

Tactic:
have mem : I x ∈ I.symm ⁻¹' (e.symm ≫ₕ chartAt H (e.symm x)).source ∩ range I := by
    simp only [hx, mfld_simps]
-- 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)
⊢ e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x) ∈ contDiffGroupoid 1 I

Tactic:
have : e.symm.trans (chartAt H (e.symm x)) ∈ contDiffGroupoid 1 I :=
    HasGroupoid.compatible h (chart_mem_atlas 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
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
⊢ 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))

Tactic:
have A :
    ContDiffOn 𝕜 1 (I ∘ e.symm.trans (chartAt H (e.symm x)) ∘ I.symm)
      (I.symm ⁻¹' (e.symm.trans (chartAt H (e.symm x))).source ∩ range I) :=
    this.1
-- 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))
⊢ DifferentiableWithinAt 𝕜 ((↑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))
    ((↑I : H → E) x)

Tactic:
have B := A.differentiableOn one_ne_zero (I x) 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
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))
    ((↑I.symm : E → H) ⁻¹' e.target ∩
        (↑I.symm : E → H) ⁻¹'
          (↑e.symm : H → M) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑e.symm : H → M) x))).source ∩
      range (↑I : H → E))
    ((↑I : H → E) x)
rw :
  ∀
    (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 : H → E) x)),
    DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e.symm : H → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : H → E) x)
rw₁ :
  ∀
    (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)
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e.symm : H → M)) (range (↑I : H → E))
    ((↑(extChartAt I x) : H → E) x)

Tactic:
rw [inter_comm, differentiableWithinAt_inter] at B

Premises used: differentiableWithinAt_inter, Set.inter_comm
-- 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 : H → E) x)
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e.symm : H → M)) (range (↑I : H → E))
    ((↑(extChartAt I x) : H → E) x)

Tactic:
simpa only [mfld_simps]