awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ (↑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⦄,
  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)
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (hypothesis)
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₁ : 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 := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') x)
hx' : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source
y : E
hy : y ∈ (↑I.symm : E → H) ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').target ∩ range (↑I : H → E)
⊢ ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑((c.symm ≫ₕ f) ≫ₕ c').symm : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').target ∩ range (↑I : H → E)) y
have hy₁ : ((↑I.symm : E → H) y ∈ c'.target ∧
    (↑c'.symm : H → M') ((↑I.symm : E → H) y) ∈ f.target ∧
      (↑f.symm : M' → M) ((↑c'.symm : H → M') ((↑I.symm : E → H) y)) ∈ c.source) ∧
  y ∈ range (↑I : H → E)
Tactic: simp only [mfld_simps] at hy
Cleared hypotheses: hy
-- 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'
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 := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') x)
hx' : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source
y : E
hy :
  ((↑I.symm : E → H) y ∈ c'.target ∧
      (↑c'.symm : H → M') ((↑I.symm : E → H) y) ∈ f.target ∧
        (↑f.symm : M' → M) ((↑c'.symm : H → M') ((↑I.symm : E → H) y)) ∈ c.source) ∧
    y ∈ range (↑I : H → E)
⊢ ContMDiffWithinAt I I n (↑f.symm : M' → M) (f.symm ≫ₕ c).source ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y)
have refine_1 : (↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y ∈ f.target
Tactic: refine (h₂ ((extChartAt I (f x)).symm y) ?_).mono ?_
-- 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'
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 := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') x)
hx' : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source
y : E
hy :
  ((↑I.symm : E → H) y ∈ c'.target ∧
      (↑c'.symm : H → M') ((↑I.symm : E → H) y) ∈ f.target ∧
        (↑f.symm : M' → M) ((↑c'.symm : H → M') ((↑I.symm : E → H) y)) ∈ c.source) ∧
    y ∈ range (↑I : H → E)
refine_1 : (↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y ∈ f.target
⊢ ContMDiffWithinAt I I n (↑f.symm : M' → M) (f.symm ≫ₕ c).source ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y)
have refine_2 : (f.symm ≫ₕ c).source ⊆ f.target
Tactic: refine (h₂ ((extChartAt I (f x)).symm y) ?_).mono ?_
-- 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'
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 := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') x)
hx' : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source
y : E
hy :
  ((↑I.symm : E → H) y ∈ c'.target ∧
      (↑c'.symm : H → M') ((↑I.symm : E → H) y) ∈ f.target ∧
        (↑f.symm : M' → M) ((↑c'.symm : H → M') ((↑I.symm : E → H) y)) ∈ c.source) ∧
    y ∈ range (↑I : H → E)
⊢ (f.symm ≫ₕ c).source ⊆ f.target
have refine_2 : ∀ ⦃my_y : M'⦄, my_y ∈ (f.symm ≫ₕ c).source → my_y ∈ f.target
Tactic: mfld_set_tac
-- 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'
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 := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') x)
hx' : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source
y : E
hy :
  ((↑I.symm : E → H) y ∈ c'.target ∧
      (↑c'.symm : H → M') ((↑I.symm : E → H) y) ∈ f.target ∧
        (↑f.symm : M' → M) ((↑c'.symm : H → M') ((↑I.symm : E → H) y)) ∈ c.source) ∧
    y ∈ range (↑I : H → E)
refine_2 refine_2₁ refine_2₂ : ∀ ⦃my_y : M'⦄, my_y ∈ (f.symm ≫ₕ c).source → my_y ∈ f.target
⊢ (f.symm ≫ₕ c).source ⊆ f.target
have refine_2₃ : ∀ ⦃my_y : M'⦄, my_y ∈ f.target ∧ (↑f.symm : M' → M) my_y ∈ c.source → my_y ∈ f.target
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (hypothesis)
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₁ : 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 := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') x)
hx' : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source
y : E
hy :
  ((↑I.symm : E → H) y ∈ c'.target ∧
      (↑c'.symm : H → M') ((↑I.symm : E → H) y) ∈ f.target ∧
        (↑f.symm : M' → M) ((↑c'.symm : H → M') ((↑I.symm : E → H) y)) ∈ c.source) ∧
    y ∈ range (↑I : H → E)
⊢ ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑((c.symm ≫ₕ f) ≫ₕ c').symm : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').target ∩ range (↑I : H → E)) y
have H₁ : ContMDiffWithinAt I I n (↑f.symm : M' → M) (f.symm ≫ₕ c).source ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y)
Tactic: have H : ContMDiffWithinAt I I n f.symm (f.symm ≫ₕ c).source
          ((extChartAt I (f x)).symm y) := by
        refine (h₂ ((extChartAt I (f x)).symm y) ?_).mono ?_
        · simp only [c', hy, mfld_simps]
        · mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (hypothesis)
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 :
  ContMDiffWithinAt I I n (↑f.symm : M' → M) (f.symm ≫ₕ c).source ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y)
⊢ ContDiffWithinAt 𝕜 n ((↑I : H_1 → E) ∘ (↑((c.symm ≫ₕ f) ≫ₕ c').symm : H_1 → H_1) ∘ (↑I.symm : E → H_1))
    ((↑I.symm : E → H_1) ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').target ∩ range (↑I : H_1 → E)) y
have hy' : (↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y ∈ c'.source
Tactic: have hy' : (extChartAt I (f x)).symm y ∈ c'.source := by simp only [c', hy, mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (hypothesis)
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 :
  ContMDiffWithinAt I I n (↑f.symm : M' → M) (f.symm ≫ₕ c).source ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y)
hy' : (↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y ∈ c'.source
⊢ ContDiffWithinAt 𝕜 n ((↑I : H_1 → E) ∘ (↑((c.symm ≫ₕ f) ≫ₕ c').symm : H_1 → H_1) ∘ (↑I.symm : E → H_1))
    ((↑I.symm : E → H_1) ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').target ∩ range (↑I : H_1 → E)) y
have hy'' : (↑f.symm : M' → M) ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y) ∈ c.source
Tactic: have hy'' : f.symm ((extChartAt I (f x)).symm y) ∈ c.source := by
        simp only [c', hy, mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (hypothesis)
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 :
  ContMDiffWithinAt I I n (↑f.symm : M' → M) (f.symm ≫ₕ c).source ((↑(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
⊢ ContDiffWithinAt 𝕜 n ((↑I : H_1 → E) ∘ (↑((c.symm ≫ₕ f) ≫ₕ c').symm : H_1 → H_1) ∘ (↑I.symm : E → H_1))
    ((↑I.symm : E → H_1) ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').target ∩ range (↑I : H_1 → E)) y
have 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))
Tactic: rw [contMDiffWithinAt_iff_of_mem_source hy' hy''] at H
Cleared hypotheses: H, hy', hy''
-- 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
⊢ ContDiffWithinAt 𝕜 n ((↑I : H_1 → E) ∘ (↑((c.symm ≫ₕ f) ≫ₕ c').symm : H_1 → H_1) ∘ (↑I.symm : E → H_1))
    ((↑I.symm : E → H_1) ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').target ∩ range (↑I : H_1 → E)) y
have h : y = (↑(extChartAt I ((↑f : M → M') x)) : M' → E) ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y)
Tactic: convert! H.2.mono _
-- 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
h : y = (↑(extChartAt I ((↑f : M → M') x)) : M' → E) ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y)
⊢ ContDiffWithinAt 𝕜 n ((↑I : H_1 → E) ∘ (↑((c.symm ≫ₕ f) ≫ₕ c').symm : H_1 → H_1) ∘ (↑I.symm : E → H_1))
    ((↑I.symm : E → H_1) ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').target ∩ range (↑I : H_1 → E)) y
have mpr : (↑I.symm : E → H_1) ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').target ∩ range (↑I : H_1 → E) ⊆
  (↑(extChartAt I ((↑f : M → M') x)).symm : E → M') ⁻¹' (f.symm ≫ₕ c).source ∩ range (↑I : H_1 → E)
Tactic: convert! H.2.mono _
-- 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
⊢ (↑I.symm : E → H_1) ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').target ∩ range (↑I : H_1 → E) ⊆
    (↑(extChartAt I ((↑f : M → M') x)).symm : E → M') ⁻¹' (f.symm ≫ₕ c).source ∩ range (↑I : H_1 → E)
have mpr : (↑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)
Tactic: dsimp [c, c']
-- 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'
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 := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') x)
hx' : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source
⊢ EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑((c.symm ≫ₕ f) ≫ₕ c').toPartialEquiv : H → H)
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source ∩ ((c.symm ≫ₕ f) ≫ₕ c').source)
have mpr : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M))
  ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source ∩
    (c.target ∩ (↑c.symm : H → M) ⁻¹' f.source ∩ (↑f : M → M') ∘ (↑c.symm : H → M) ⁻¹' c'.source))
Tactic: simp only [mfld_simps]