-- Module: Mathlib.Geometry.Manifold.ContMDiff.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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
X : M'
hX : X ∈ f.symm.source
x : M := (↑f.symm : M' → M) X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H X
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt
    ((↑(chartAt H ((↑f : M → M') x)) : M' → H) ∘ (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x)
h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source
h1 : c' = chartAt H ((↑f : M → M') x)
h2 : (↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M) = (↑(c.symm ≫ₕ f ≫ₕ c') : H → H)
hcx : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source
rw :
  ∀
    (hxf :
      (↑(chartAt H x) : M → H) x ∈ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source →
        ∃ e ∈ contDiffGroupoid n I,
          e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source ∧
            EqOn (↑(c.symm ≫ₕ f ≫ₕ c') : H → H) (↑e : H → H) e.source ∧ (↑(chartAt H x) : M → H) x ∈ e.source)
    (h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source)
    (h1 : c' = chartAt H ((↑f : M → M') x))
    (h2 : (↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M) = (↑(c.symm ≫ₕ f ≫ₕ c') : H → H))
    (hcx : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source),
    ∃ e ∈ contDiffGroupoid n I,
      e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source ∧
        EqOn (↑(c.symm ≫ₕ f ≫ₕ c') : H → H) (↑e : H → H) e.source ∧ (↑c : M → H) x ∈ e.source
hs :
  ∀
    (hxf :
      (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑(c.symm ≫ₕ f ≫ₕ c') : H → H)
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x))
    (h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source)
    (h1 : c' = chartAt H ((↑f : M → M') x))
    (h2 : (↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M) = (↑(c.symm ≫ₕ f ≫ₕ c') : H → H))
    (hcx : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source),
    (c.symm ≫ₕ f ≫ₕ c').source ⊆ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source
hx₁ :
  ∀
    (hxf :
      (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑(c.symm ≫ₕ f ≫ₕ c') : H → H)
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x))
    (h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source)
    (h1 : c' = chartAt H ((↑f : M → M') x))
    (h2 : (↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M) = (↑(c.symm ≫ₕ f ≫ₕ c') : H → H))
    (hcx : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source),
    (↑(chartAt H x) : M → H) x ∈
      (c.symm ≫ₕ f ≫ₕ c').source ∪ ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source)ᶜ
⊢ ∃ e ∈ contDiffGroupoid n I,
    e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source ∧
      EqOn (↑(c.symm ≫ₕ f ≫ₕ c') : H → H) (↑e : H → H) e.source ∧ (↑c : M → H) x ∈ e.source

Tactic:
rw [← h1, h2, OpenPartialHomeomorph.isLocalStructomorphWithinAt_iff'] at hxf

Premises used: OpenPartialHomeomorph.isLocalStructomorphWithinAt_iff'