-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (goal)
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'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') 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)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) ((↑c.symm : H → M) ⁻¹' f.source ∩ e.source)
hex : (↑c : M → H) x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
hc' : ContMDiffOn I I n (↑c'.symm : H → M') (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).target
he'' : ContMDiffOn I I n (↑e : H → H) e.source
hc : ContMDiffOn I I n (↑c : M → H) (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
mfld_set_tac mfld_set_tac₁ mfld_set_tac₂ :
  ∀ ⦃my_y : M⦄,
    my_y ∈
        f.source ∩ (↑f : M → M') ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).source ∩
          ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' e.source ∩
            (↑e : H → H) ∘ (↑(chartAt H x) : M → H) ⁻¹'
              (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).target) →
      my_y ∈
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' e.source ∩
          (↑e : H → H) ∘ (↑(chartAt H x) : M → H) ⁻¹'
            (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).target
⊢ f.source ∩ (↑f : M → M') ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).source ∩
      ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' e.source ∩
        (↑e : H → H) ∘ (↑(chartAt H x) : M → H) ⁻¹'
          (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).target) ⊆
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' e.source ∩
      (↑e : H → H) ∘ (↑(chartAt H x) : M → H) ⁻¹'
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).target
have mfld_set_tac₃ : ∀ ⦃my_y : M⦄,
  (my_y ∈ f.source ∧ (↑f : M → M') my_y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).source) ∧
      (my_y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∧ (↑(chartAt H x) : M → H) my_y ∈ e.source) ∧
        (↑e : H → H) ((↑(chartAt H x) : M → H) my_y) ∈
          (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).target →
    my_y ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' e.source ∩
        (↑e : H → H) ∘ (↑(chartAt H x) : M → H) ⁻¹'
          (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).target
Tactic: mfld_set_tac