-- 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_1 : Type u_3
inst_3 : TopologicalSpace H_1
I : ModelWithCorners 𝕜 E H_1
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H_1 M
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H_1 M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h₁ : ContMDiffOn I I n (↑f : M → M') f.source
h₂ : ContMDiffOn I I n (↑f.symm : M' → M) f.target
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H_1 := chartAt H_1 x
c' : OpenPartialHomeomorph M' H_1 := chartAt H_1 ((↑f : M → M') x)
hx' : (↑c : M → H_1) x ∈ (↑c.symm : H_1 → M) ⁻¹' f.source
y : E
hy :
  ((↑I.symm : E → H_1) y ∈ c'.target ∧
      (↑c'.symm : H_1 → M') ((↑I.symm : E → H_1) y) ∈ f.target ∧
        (↑f.symm : M' → M) ((↑c'.symm : H_1 → M') ((↑I.symm : E → H_1) y)) ∈ c.source) ∧
    y ∈ range (↑I : H_1 → E)
H :
  ContinuousWithinAt (↑f.symm : M' → M) (f.symm ≫ₕ c).source ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y) ∧
    ContDiffWithinAt 𝕜 n
      ((↑(extChartAt I x) : M → E) ∘ (↑f.symm : M' → M) ∘ (↑(extChartAt I ((↑f : M → M') x)).symm : E → M'))
      ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') ⁻¹' (f.symm ≫ₕ c).source ∩ range (↑I : H_1 → E))
      ((↑(extChartAt I ((↑f : M → M') x)) : M' → E) ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y))
hy' : (↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y ∈ c'.source
hy'' : (↑f.symm : M' → M) ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y) ∈ c.source
mpr mpr₁ mpr₂ :
  ∀ ⦃my_y : E⦄,
    my_y ∈
        (↑I.symm : E → H_1) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H_1 ((↑f : M → M') x))).target ∩
            ((↑I.symm : E → H_1) ⁻¹'
                (↑(OpenPartialHomeomorph.symm (chartAt H_1 ((↑f : M → M') x))) : H_1 → M') ⁻¹' f.target ∩
              (↑I.symm : E → H_1) ⁻¹'
                (↑(OpenPartialHomeomorph.symm (chartAt H_1 ((↑f : M → M') x))) : H_1 → M') ⁻¹'
                  (↑f.symm : M' → M) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H_1 x)).source) ∩
          range (↑I : H_1 → E) →
      my_y ∈
        (↑(OpenPartialHomeomorph.symm (chartAt H_1 ((↑f : M → M') x))) : H_1 → M') ∘ (↑I.symm : E → H_1) ⁻¹' f.target ∩
            (↑(OpenPartialHomeomorph.symm (chartAt H_1 ((↑f : M → M') x))) : H_1 → M') ∘ (↑I.symm : E → H_1) ⁻¹'
              (↑f.symm : M' → M) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H_1 x)).source ∩
          range (↑I : H_1 → E)
⊢ (↑I.symm : E → H_1) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H_1 ((↑f : M → M') x))).target ∩
        ((↑I.symm : E → H_1) ⁻¹'
            (↑(OpenPartialHomeomorph.symm (chartAt H_1 ((↑f : M → M') x))) : H_1 → M') ⁻¹' f.target ∩
          (↑I.symm : E → H_1) ⁻¹'
            (↑(OpenPartialHomeomorph.symm (chartAt H_1 ((↑f : M → M') x))) : H_1 → M') ⁻¹'
              (↑f.symm : M' → M) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H_1 x)).source) ∩
      range (↑I : H_1 → E) ⊆
    (↑(OpenPartialHomeomorph.symm (chartAt H_1 ((↑f : M → M') x))) : H_1 → M') ∘ (↑I.symm : E → H_1) ⁻¹' f.target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H_1 ((↑f : M → M') x))) : H_1 → M') ∘ (↑I.symm : E → H_1) ⁻¹'
          (↑f.symm : M' → M) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H_1 x)).source ∩
      range (↑I : H_1 → E)
have mpr₃ : ∀ ⦃my_y : E⦄,
  ((↑I.symm : E → H_1) my_y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H_1 ((↑f : M → M') x))).target ∧
        (↑(OpenPartialHomeomorph.symm (chartAt H_1 ((↑f : M → M') x))) : H_1 → M') ((↑I.symm : E → H_1) my_y) ∈
            f.target ∧
          (↑f.symm : M' → M)
              ((↑(OpenPartialHomeomorph.symm (chartAt H_1 ((↑f : M → M') x))) : H_1 → M') ((↑I.symm : E → H_1) my_y)) ∈
            (OpenPartialHomeomorph.toPartialEquiv (chartAt H_1 x)).source) ∧
      my_y ∈ range (↑I : H_1 → E) →
    my_y ∈
      (↑(OpenPartialHomeomorph.symm (chartAt H_1 ((↑f : M → M') x))) : H_1 → M') ∘ (↑I.symm : E → H_1) ⁻¹' f.target ∩
          (↑(OpenPartialHomeomorph.symm (chartAt H_1 ((↑f : M → M') x))) : H_1 → M') ∘ (↑I.symm : E → H_1) ⁻¹'
            (↑f.symm : M' → M) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H_1 x)).source ∩
        range (↑I : H_1 → E)
Tactic: mfld_set_tac