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 : 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
mpr : (contDiffPregroupoid n I).property (↑((c.symm ≫ₕ f) ≫ₕ c') : H → H) ((c.symm ≫ₕ f) ≫ₕ c').source
mpr₁ : (contDiffPregroupoid n I).property (↑((c.symm ≫ₕ f) ≫ₕ c').symm : H → H) ((c.symm ≫ₕ f) ≫ₕ c').target
⊢ ∃ e ∈ contDiffGroupoid n I,
    EqOn
        ((↑(chartAt H ((↑f : M → M') x)) : M' → H) ∘
          (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        (↑e.toPartialEquiv : H → H) ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source ∩ e.source) ∧
      (↑(chartAt H x) : M → H) x ∈ e.source
have mpr₂ : 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)
Tactic: refine ⟨(c.symm.trans f).trans c', ⟨?_, ?_⟩, (?_ : EqOn (c' ∘ f ∘ c.symm) _ _), ?_⟩
-- 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
mpr : (contDiffPregroupoid n I).property (↑((c.symm ≫ₕ f) ≫ₕ c') : H → H) ((c.symm ≫ₕ f) ≫ₕ c').source
mpr₁ : (contDiffPregroupoid n I).property (↑((c.symm ≫ₕ f) ≫ₕ c').symm : H → H) ((c.symm ≫ₕ f) ≫ₕ c').target
mpr₂ :
  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)
⊢ ∃ e ∈ contDiffGroupoid n I,
    EqOn
        ((↑(chartAt H ((↑f : M → M') x)) : M' → H) ∘
          (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        (↑e.toPartialEquiv : H → H) ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source ∩ e.source) ∧
      (↑(chartAt H x) : M → H) x ∈ e.source
have mpr₃ : (↑(chartAt H x) : M → H) x ∈ ((c.symm ≫ₕ f) ≫ₕ c').source
Tactic: refine ⟨(c.symm.trans f).trans c', ⟨?_, ?_⟩, (?_ : EqOn (c' ∘ f ∘ c.symm) _ _), ?_⟩
-- 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').source ∩ range (↑I : H → E)
⊢ ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑((c.symm ≫ₕ f) ≫ₕ c') : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').source ∩ range (↑I : H → E)) y
have hy₁ : (((↑I.symm : E → H) y ∈ c.target ∧ (↑c.symm : H → M) ((↑I.symm : E → H) y) ∈ f.source) ∧
    (↑f : 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.source) ∧
      (↑f : M → M') ((↑c.symm : H → M) ((↑I.symm : E → H) y)) ∈ c'.source) ∧
    y ∈ range (↑I : H → E)
⊢ ContMDiffWithinAt I I n (↑f : M → M') (f ≫ₕ c').source ((↑(extChartAt I x).symm : E → M) y)
have refine_1 : (↑(extChartAt I x).symm : E → M) y ∈ f.source
Tactic: refine (h₁ ((extChartAt I 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.source) ∧
      (↑f : M → M') ((↑c.symm : H → M) ((↑I.symm : E → H) y)) ∈ c'.source) ∧
    y ∈ range (↑I : H → E)
refine_1 : (↑(extChartAt I x).symm : E → M) y ∈ f.source
⊢ ContMDiffWithinAt I I n (↑f : M → M') (f ≫ₕ c').source ((↑(extChartAt I x).symm : E → M) y)
have refine_2 : (f ≫ₕ c').source ⊆ f.source
Tactic: refine (h₁ ((extChartAt I 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.source) ∧
      (↑f : M → M') ((↑c.symm : H → M) ((↑I.symm : E → H) y)) ∈ c'.source) ∧
    y ∈ range (↑I : H → E)
⊢ (f ≫ₕ c').source ⊆ f.source
have refine_2 : ∀ ⦃my_y : M⦄, my_y ∈ (f ≫ₕ c').source → my_y ∈ f.source
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.source) ∧
      (↑f : 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 ≫ₕ c').source → my_y ∈ f.source
⊢ (f ≫ₕ c').source ⊆ f.source
have refine_2₃ : ∀ ⦃my_y : M⦄, my_y ∈ f.source ∧ (↑f : M → M') my_y ∈ c'.source → my_y ∈ f.source
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.source) ∧
      (↑f : 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') : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').source ∩ range (↑I : H → E)) y
have H₁ : ContMDiffWithinAt I I n (↑f : M → M') (f ≫ₕ c').source ((↑(extChartAt I x).symm : E → M) y)
Tactic: have H : ContMDiffWithinAt I I n f (f ≫ₕ c').source ((extChartAt I x).symm y) := by
        refine (h₁ ((extChartAt I 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.source) ∧
      (↑f : 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 : M → M') (f ≫ₕ c').source ((↑(extChartAt I x).symm : E → M) y)
⊢ ContDiffWithinAt 𝕜 n ((↑I : H_1 → E) ∘ (↑((c.symm ≫ₕ f) ≫ₕ c') : H_1 → H_1) ∘ (↑I.symm : E → H_1))
    ((↑I.symm : E → H_1) ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').source ∩ range (↑I : H_1 → E)) y
have hy' : (↑(extChartAt I x).symm : E → M) y ∈ c.source
Tactic: have hy' : (extChartAt I 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.source) ∧
      (↑f : 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 : M → M') (f ≫ₕ c').source ((↑(extChartAt I x).symm : E → M) y)
hy' : (↑(extChartAt I x).symm : E → M) y ∈ c.source
⊢ ContDiffWithinAt 𝕜 n ((↑I : H_1 → E) ∘ (↑((c.symm ≫ₕ f) ≫ₕ c') : H_1 → H_1) ∘ (↑I.symm : E → H_1))
    ((↑I.symm : E → H_1) ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').source ∩ range (↑I : H_1 → E)) y
have hy'' : (↑f : M → M') ((↑(extChartAt I x).symm : E → M) y) ∈ c'.source
Tactic: have hy'' : f ((extChartAt I 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.source) ∧
      (↑f : 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 : M → M') (f ≫ₕ c').source ((↑(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
⊢ ContDiffWithinAt 𝕜 n ((↑I : H_1 → E) ∘ (↑((c.symm ≫ₕ f) ≫ₕ c') : H_1 → H_1) ∘ (↑I.symm : E → H_1))
    ((↑I.symm : E → H_1) ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').source ∩ range (↑I : H_1 → E)) y
have 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))
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.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
⊢ ContDiffWithinAt 𝕜 n ((↑I : H_1 → E) ∘ (↑((c.symm ≫ₕ f) ≫ₕ c') : H_1 → H_1) ∘ (↑I.symm : E → H_1))
    ((↑I.symm : E → H_1) ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').source ∩ range (↑I : H_1 → E)) y
have h : y = (↑(extChartAt I x) : M → E) ((↑(extChartAt I 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.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
h : y = (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)
⊢ ContDiffWithinAt 𝕜 n ((↑I : H_1 → E) ∘ (↑((c.symm ≫ₕ f) ≫ₕ c') : H_1 → H_1) ∘ (↑I.symm : E → H_1))
    ((↑I.symm : E → H_1) ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').source ∩ range (↑I : H_1 → E)) y
have mpr : (↑I.symm : E → H_1) ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').source ∩ range (↑I : H_1 → E) ⊆
  (↑(extChartAt I x).symm : E → M) ⁻¹' (f ≫ₕ 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.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) ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').source ∩ range (↑I : H_1 → E) ⊆
    (↑(extChartAt I x).symm : E → M) ⁻¹' (f ≫ₕ c').source ∩ range (↑I : H_1 → E)
have mpr : (↑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)
Tactic: dsimp [c, c']