awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
⊢ y = (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)

Tactic:
simp only [c, hy, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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 :
  (↑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)
⊢ (↑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:
dsimp [c, c']
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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)
⊢ ((↑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
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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)

Tactic:
(h₂ ((extChartAt I (f x)).symm y) ?_).mono ?_

Premises used: ContMDiffWithinAt.mono, extChartAt, PartialEquiv.symm, OpenPartialHomeomorph.toFun', PartialEquiv.toFun
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
refine_2 : (f.symm ≫ₕ c).source ⊆ f.target
⊢ ContMDiffWithinAt I I n (↑f.symm : M' → M) (f.symm ≫ₕ c).source ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y)

Tactic:
refine (h₂ ((extChartAt I (f x)).symm y) ?_).mono ?_

Premises used: ContMDiffWithinAt.mono, extChartAt, PartialEquiv.symm, OpenPartialHomeomorph.toFun', PartialEquiv.toFun
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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)
⊢ (↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y ∈ f.target

Tactic:
simp only [c', hy, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
refine_2₃ refine_2₄ : ∀ ⦃my_y : M'⦄, my_y ∈ f.target ∧ (↑f.symm : M' → M) my_y ∈ c.source → my_y ∈ f.target
⊢ (f.symm ≫ₕ c).source ⊆ f.target

Tactic:
mfld_set_tac
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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)

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
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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)
⊢ (↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y ∈ c'.source

Tactic:
simp only [c', hy, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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)
⊢ (↑(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]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
⊢ (↑f.symm : M' → M) ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y) ∈ c.source

Tactic:
simp only [c', hy, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
⊢ (↑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]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
⊢ 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

Premises used: contMDiffWithinAt_iff_of_mem_source
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
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))
⊢ (↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y ∈ c'.source

Tactic:
rw [contMDiffWithinAt_iff_of_mem_source hy' hy''] at H

Premises used: contMDiffWithinAt_iff_of_mem_source
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
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
⊢ (↑f.symm : M' → M) ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y) ∈ c.source

Tactic:
rw [contMDiffWithinAt_iff_of_mem_source hy' hy''] at H

Premises used: contMDiffWithinAt_iff_of_mem_source