-- Mathlib/Geometry/Manifold/ContMDiff/Basic.lean
/-- If the `ChartedSpace` structure on a manifold `M` is given by an open embedding `e : M → H`,
then `e` is `C^n`. -/
lemma contMDiff_isOpenEmbedding [Nonempty M] :
    haveI := h.singletonChartedSpace; ContMDiff I I n e

Proof state:
case right
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
e : M → H
h : IsOpenEmbedding e
n : WithTop ℕ∞
inst✝ : Nonempty M
this : IsManifold I ω M
x : M
y : H
z : E
hz : z ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (e ⁻¹' (extChartAt I y).source)
⊢ z ∈ range ↑I

Tactic:
apply mem_of_subset_of_mem _ hz.1

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
e : M → H
h : IsOpenEmbedding e
n : WithTop ℕ∞
inst✝ : Nonempty M
this : IsManifold I ω M
x : M
y : H
z : E
hz : z ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (e ⁻¹' (extChartAt I y).source)
⊢ (extChartAt I x).target ⊆ range ↑I

Proof state:
case right
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
e : M → H
h : IsOpenEmbedding e
n : WithTop ℕ∞
inst✝ : Nonempty M
this : IsManifold I ω M
x : M
y : H
z : E
hz : z ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (e ⁻¹' (extChartAt I y).source)
⊢ ↑I (↑I.symm z) = z

Tactic:
rw [I.right_inv]

Result:
case right
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
e : M → H
h : IsOpenEmbedding e
n : WithTop ℕ∞
inst✝ : Nonempty M
this : IsManifold I ω M
x : M
y : H
z : E
hz : z ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (e ⁻¹' (extChartAt I y).source)
⊢ z ∈ range ↑I

Proof state:
case right
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
e : M → H
h : IsOpenEmbedding e
n : WithTop ℕ∞
inst✝ : Nonempty M
this✝¹ : IsManifold I ω M
x : M
y : H
z : E
hz : z ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (e ⁻¹' (extChartAt I y).source)
this✝ : z ∈ ↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I
this : z ∈ ↑I.symm ⁻¹' (chartAt H x).target
⊢ ↑I.symm z ∈ range e

Tactic:
rw [mem_preimage, PartialHomeomorph.singletonChartedSpace_chartAt_eq,
  h.toPartialHomeomorph_target] at this

Result:
case right
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
e : M → H
h : IsOpenEmbedding e
n : WithTop ℕ∞
inst✝ : Nonempty M
this✝¹ : IsManifold I ω M
x : M
y : H
z : E
hz : z ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (e ⁻¹' (extChartAt I y).source)
this✝ : z ∈ ↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I
this : ↑I.symm z ∈ range e
⊢ ↑I.symm z ∈ range e

Proof state:
case right
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
e : M → H
h : IsOpenEmbedding e
n : WithTop ℕ∞
inst✝ : Nonempty M
this : IsManifold I ω M
x : M
y : H
⊢ ContDiffOn 𝕜 n (↑(extChartAt I y) ∘ e ∘ ↑(extChartAt I x).symm)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (e ⁻¹' (extChartAt I y).source))

Tactic:
apply contDiffOn_id.congr

Result:
case right
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
e : M → H
h : IsOpenEmbedding e
n : WithTop ℕ∞
inst✝ : Nonempty M
this : IsManifold I ω M
x : M
y : H
⊢ ∀ x_1 ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (e ⁻¹' (extChartAt I y).source),
    (↑(extChartAt I y) ∘ e ∘ ↑(extChartAt I x).symm) x_1 = id x_1

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
e : M → H
h : IsOpenEmbedding e
n : WithTop ℕ∞
inst✝ : Nonempty M
this : IsManifold I ω M
⊢ ContMDiff I I n e

Tactic:
rw [@contMDiff_iff _ _ _ _ _ _ _ _ _ _ h.singletonChartedSpace]

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
e : M → H
h : IsOpenEmbedding e
n : WithTop ℕ∞
inst✝ : Nonempty M
this : IsManifold I ω M
⊢ Continuous e ∧
    ∀ (x : M) (y : H),
      ContDiffOn 𝕜 n (↑(extChartAt I y) ∘ e ∘ ↑(extChartAt I x).symm)
        ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (e ⁻¹' (extChartAt I y).source))

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
e : M → H
h : IsOpenEmbedding e
n : WithTop ℕ∞
inst✝ : Nonempty M
this : IsManifold I ω M
x : M
y : H
z : E
hz : z ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (e ⁻¹' (extChartAt I y).source)
⊢ (extChartAt I x).target ⊆ range ↑I

Tactic:
exact haveI := h.singletonChartedSpace; extChartAt_target_subset_range (I := I) x

Result:
no goals

Proof state:
case right
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
e : M → H
h : IsOpenEmbedding e
n : WithTop ℕ∞
inst✝ : Nonempty M
this : IsManifold I ω M
x : M
y : H
z : E
hz : z ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (e ⁻¹' (extChartAt I y).source)
⊢ (↑(extChartAt I y) ∘ e ∘ ↑(extChartAt I x).symm) z = id z

Tactic:
simp only [mfld_simps]

Result:
case right
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
e : M → H
h : IsOpenEmbedding e
n : WithTop ℕ∞
inst✝ : Nonempty M
this : IsManifold I ω M
x : M
y : H
z : E
hz : z ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (e ⁻¹' (extChartAt I y).source)
⊢ ↑I (e (↑(IsOpenEmbedding.toPartialHomeomorph e h).symm (↑I.symm z))) = z