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 : 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
⊢ ∃ 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

Tactic:
⟨(c.symm.trans f).trans c', ⟨?_, ?_⟩, (?_ : EqOn (c' ∘ f ∘ c.symm) _ _), ?_⟩

Premises used: OpenPartialHomeomorph.trans, And.intro, Exists.intro, OpenPartialHomeomorph.symm
-- 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
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)
mpr₃ : (↑(chartAt H x) : M → H) x ∈ ((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

Tactic:
refine ⟨(c.symm.trans f).trans c', ⟨?_, ?_⟩, (?_ : EqOn (c' ∘ f ∘ c.symm) _ _), ?_⟩
-- 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').source ∩ range (↑I : H → E)
⊢ (((↑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
-- 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.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)

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

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

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

Premises used: ContMDiffWithinAt.mono, extChartAt, PartialEquiv.symm, 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.source) ∧
      (↑f : M → M') ((↑c.symm : H → M) ((↑I.symm : E → H) y)) ∈ c'.source) ∧
    y ∈ range (↑I : H → E)
⊢ (↑(extChartAt I x).symm : E → M) y ∈ f.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 : 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
refine_2₃ refine_2₄ : ∀ ⦃my_y : M⦄, my_y ∈ f.source ∧ (↑f : M → M') my_y ∈ c'.source → my_y ∈ f.source
⊢ (f ≫ₕ c').source ⊆ f.source

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.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)

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
-- 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 : ContMDiffWithinAt I I n (↑f : M → M') (f ≫ₕ c').source ((↑(extChartAt I x).symm : E → M) y)
⊢ (↑(extChartAt I 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.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)
⊢ (↑(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]
-- 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 : 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
⊢ (↑f : M → M') ((↑(extChartAt I 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.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
⊢ (↑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]
-- 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 : 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
⊢ 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

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.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
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))
⊢ (↑(extChartAt I 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.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
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
⊢ (↑f : M → M') ((↑(extChartAt I 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.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 ((↑(extChartAt I ((↑f : M → M') x)) : M' → E) ∘ (↑f : M → M') ∘ (↑(extChartAt I x).symm : E → M))
    ((↑I.symm : E → H_1) ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').source ∩ range (↑I : H_1 → E))
    ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))

Tactic:
H.2.mono _

Premises used: And.right, ContDiffWithinAt.mono
-- 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
h : y = (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)
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)
⊢ 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

Tactic:
convert! H.2.mono _

Premises used: And.right, ContDiffWithinAt.mono