-- Mathlib/Geometry/Manifold/ContMDiff/Basic.lean
/-- If the `ChartedSpace` structure on a manifold `M` is given by an open embedding `e : M → H`,
then the inverse of `e` is `C^n`. -/
lemma contMDiffOn_isOpenEmbedding_symm [Nonempty M] :
    haveI := h.singletonChartedSpace; ContMDiffOn I I
      n (IsOpenEmbedding.toPartialHomeomorph e h).symm (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
z✝ : H
hz✝ : M
z : E
hz :
  z ∈
    (extChartAt I z✝).target ∩
      ↑(extChartAt I z✝).symm ⁻¹'
        (range e ∩ ↑(IsOpenEmbedding.toPartialHomeomorph e h).symm ⁻¹' (extChartAt I hz✝).source)
this : ↑I.symm z ∈ range e
⊢ z ∈ range ↑I

Tactic:
exact mem_of_subset_of_mem (extChartAt_target_subset_range _) hz.1

Result:
no goals

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
z✝ : H
hz✝ : M
z : E
hz :
  z ∈
    (extChartAt I z✝).target ∩
      ↑(extChartAt I z✝).symm ⁻¹'
        (range e ∩ ↑(IsOpenEmbedding.toPartialHomeomorph e h).symm ⁻¹' (extChartAt I hz✝).source)
⊢ ↑I.symm z ∈ range e

Tactic:
rw [ModelWithCorners.symm, ← mem_preimage]

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
z✝ : H
hz✝ : M
z : E
hz :
  z ∈
    (extChartAt I z✝).target ∩
      ↑(extChartAt I z✝).symm ⁻¹'
        (range e ∩ ↑(IsOpenEmbedding.toPartialHomeomorph e h).symm ⁻¹' (extChartAt I hz✝).source)
⊢ z ∈ ↑I.symm ⁻¹' 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
z✝ : H
hz✝ : M
z : E
hz :
  z ∈
    (extChartAt I z✝).target ∩
      ↑(extChartAt I z✝).symm ⁻¹'
        (range e ∩ ↑(IsOpenEmbedding.toPartialHomeomorph e h).symm ⁻¹' (extChartAt I hz✝).source)
⊢ (↑(extChartAt I hz✝) ∘ ↑(IsOpenEmbedding.toPartialHomeomorph e h).symm ∘ ↑(extChartAt I z✝).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
z✝ : H
hz✝ : M
z : E
hz :
  z ∈
    (extChartAt I z✝).target ∩
      ↑(extChartAt I z✝).symm ⁻¹'
        (range e ∩ ↑(IsOpenEmbedding.toPartialHomeomorph e h).symm ⁻¹' (extChartAt I hz✝).source)
⊢ ↑I (e (↑(IsOpenEmbedding.toPartialHomeomorph e h).symm (↑I.symm z))) = z

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
z✝ : H
hz✝ : M
z : E
hz :
  z ∈
    (extChartAt I z✝).target ∩
      ↑(extChartAt I z✝).symm ⁻¹'
        (range e ∩ ↑(IsOpenEmbedding.toPartialHomeomorph e h).symm ⁻¹' (extChartAt I hz✝).source)
this : ↑I.symm z ∈ range e
⊢ ↑I (↑I.symm z) = z

Tactic:
apply 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
z✝ : H
hz✝ : M
z : E
hz :
  z ∈
    (extChartAt I z✝).target ∩
      ↑(extChartAt I z✝).symm ⁻¹'
        (range e ∩ ↑(IsOpenEmbedding.toPartialHomeomorph e h).symm ⁻¹' (extChartAt I hz✝).source)
this : ↑I.symm z ∈ range e
⊢ z ∈ range ↑I

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
⊢ ContinuousOn (↑(IsOpenEmbedding.toPartialHomeomorph e h).symm) (range e) ∧
    ∀ (x : H) (y : M),
      ContDiffOn 𝕜 n (↑(extChartAt I y) ∘ ↑(IsOpenEmbedding.toPartialHomeomorph e h).symm ∘ ↑(extChartAt I x).symm)
        ((extChartAt I x).target ∩
          ↑(extChartAt I x).symm ⁻¹'
            (range e ∩ ↑(IsOpenEmbedding.toPartialHomeomorph e h).symm ⁻¹' (extChartAt I y).source))

Tactic:
constructor

Result:
case left
𝕜 : 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
⊢ ContinuousOn (↑(IsOpenEmbedding.toPartialHomeomorph e h).symm) (range e)

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 : H) (y : M),
    ContDiffOn 𝕜 n (↑(extChartAt I y) ∘ ↑(IsOpenEmbedding.toPartialHomeomorph e h).symm ∘ ↑(extChartAt I x).symm)
      ((extChartAt I x).target ∩
        ↑(extChartAt I x).symm ⁻¹'
          (range e ∩ ↑(IsOpenEmbedding.toPartialHomeomorph e h).symm ⁻¹' (extChartAt I y).source))

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
z : H
hz : M
⊢ ContDiffOn 𝕜 n (↑(extChartAt I hz) ∘ ↑(IsOpenEmbedding.toPartialHomeomorph e h).symm ∘ ↑(extChartAt I z).symm)
    ((extChartAt I z).target ∩
      ↑(extChartAt I z).symm ⁻¹'
        (range e ∩ ↑(IsOpenEmbedding.toPartialHomeomorph e h).symm ⁻¹' (extChartAt I hz).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
z : H
hz : M
⊢ ∀
    x ∈
      (extChartAt I z).target ∩
        ↑(extChartAt I z).symm ⁻¹'
          (range e ∩ ↑(IsOpenEmbedding.toPartialHomeomorph e h).symm ⁻¹' (extChartAt I hz).source),
    (↑(extChartAt I hz) ∘ ↑(IsOpenEmbedding.toPartialHomeomorph e h).symm ∘ ↑(extChartAt I z).symm) x = id x