-- 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.source) ∧
      (↑f : M → M') ((↑c.symm : H_1 → M) ((↑I.symm : E → H_1) y)) ∈ c'.source) ∧
    y ∈ range (↑I : H_1 → E)
H :
  ContinuousWithinAt (↑f : M → M') (f ≫ₕ c').source ((↑(extChartAt I x).symm : E → M) y) ∧
    ContDiffWithinAt 𝕜 n
      ((↑(extChartAt I ((↑f : M → M') x)) : M' → E) ∘ (↑f : M → M') ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' (f ≫ₕ c').source ∩ range (↑I : H_1 → E))
      ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
hy' : (↑(extChartAt I x).symm : E → M) y ∈ c.source
hy'' : (↑f : M → M') ((↑(extChartAt I 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 x)).target ∩
              (↑I.symm : E → H_1) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H_1 x)) : H_1 → M) ⁻¹' f.source ∩
            (↑I.symm : E → H_1) ⁻¹'
              (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H_1 x)) : H_1 → M) ⁻¹'
                (OpenPartialHomeomorph.toPartialEquiv (chartAt H_1 ((↑f : M → M') x))).source ∩
          range (↑I : H_1 → E) →
      my_y ∈
        (↑(OpenPartialHomeomorph.symm (chartAt H_1 x)) : H_1 → M) ∘ (↑I.symm : E → H_1) ⁻¹' f.source ∩
            (↑(OpenPartialHomeomorph.symm (chartAt H_1 x)) : H_1 → M) ∘ (↑I.symm : E → H_1) ⁻¹'
              (↑f : M → M') ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H_1 ((↑f : M → M') x))).source ∩
          range (↑I : H_1 → E)
⊢ (↑I.symm : E → H_1) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H_1 x)).target ∩
          (↑I.symm : E → H_1) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H_1 x)) : H_1 → M) ⁻¹' f.source ∩
        (↑I.symm : E → H_1) ⁻¹'
          (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H_1 x)) : H_1 → M) ⁻¹'
            (OpenPartialHomeomorph.toPartialEquiv (chartAt H_1 ((↑f : M → M') x))).source ∩
      range (↑I : H_1 → E) ⊆
    (↑(OpenPartialHomeomorph.symm (chartAt H_1 x)) : H_1 → M) ∘ (↑I.symm : E → H_1) ⁻¹' f.source ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H_1 x)) : H_1 → M) ∘ (↑I.symm : E → H_1) ⁻¹'
          (↑f : M → M') ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H_1 ((↑f : M → M') x))).source ∩
      range (↑I : H_1 → E)
have mpr₃ : ∀ ⦃my_y : E⦄,
  (((↑I.symm : E → H_1) my_y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H_1 x)).target ∧
          (↑(OpenPartialHomeomorph.symm (chartAt H_1 x)) : H_1 → M) ((↑I.symm : E → H_1) my_y) ∈ f.source) ∧
        (↑f : M → M') ((↑(OpenPartialHomeomorph.symm (chartAt H_1 x)) : H_1 → M) ((↑I.symm : E → H_1) my_y)) ∈
          (OpenPartialHomeomorph.toPartialEquiv (chartAt H_1 ((↑f : M → M') x))).source) ∧
      my_y ∈ range (↑I : H_1 → E) →
    my_y ∈
      (↑(OpenPartialHomeomorph.symm (chartAt H_1 x)) : H_1 → M) ∘ (↑I.symm : E → H_1) ⁻¹' f.source ∩
          (↑(OpenPartialHomeomorph.symm (chartAt H_1 x)) : H_1 → M) ∘ (↑I.symm : E → H_1) ⁻¹'
            (↑f : M → M') ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H_1 ((↑f : M → M') x))).source ∩
        range (↑I : H_1 → E)
Tactic: mfld_set_tac