awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
U : TopologicalSpace.Opens M'
f : M → ↥U
s : Set M
x : M
⊢ ContMDiffWithinAt I I' ∞ (Subtype.val (p := fun (x : M') ↦ x ∈ U) ∘ f) s x ↔ ContMDiffWithinAt I I' ∞ f s x

Tactic:
ChartedSpace.liftPropWithinAt_subtypeVal_comp_iff ..

Premises used: ContMDiffWithinAt, ChartedSpace.liftPropWithinAt_subtypeVal_comp_iff
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
U : TopologicalSpace.Opens M'
f : M → ↥U
x : M
rw : ContMDiffWithinAt I I' ∞ (Subtype.val (p := fun (x : M') ↦ x ∈ U) ∘ f) univ x ↔ ContMDiffAt I I' ∞ f x
rw₁ : ContMDiffWithinAt I I' ∞ (Subtype.val (p := fun (x : M') ↦ x ∈ U) ∘ f) univ x ↔ ContMDiffWithinAt I I' ∞ f univ x
rw₂ rw₃ : ContMDiffWithinAt I I' ∞ f univ x ↔ ContMDiffWithinAt I I' ∞ f univ x
⊢ ContMDiffAt I I' ∞ (Subtype.val (p := fun (x : M') ↦ x ∈ U) ∘ f) x ↔ ContMDiffAt I I' ∞ f x

Tactic:
rw [ContMDiffAt, ContMDiffAt, ContMDiffWithinAt.subtypeVal_comp_iff]

Premises used: ContMDiffWithinAt.subtypeVal_comp_iff, ContMDiffAt
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
⊢ IsManifold I ω M

Tactic:
haveI := h.isManifold_singleton (I := I) (n := ω)
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this : IsManifold I ω M
rw :
  Continuous[inst_4, inst_3] e ∧
    ∀ (x : M) (y : H),
      ContDiffOn 𝕜 n ((↑(extChartAt I y) : H → E) ∘ e ∘ (↑(extChartAt I x).symm : E → M))
        ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' e ⁻¹' (extChartAt I y).source)
⊢ ContMDiff I I n e

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

Premises used: contMDiff_iff
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this : IsManifold I ω M
right :
  ∀ (x : M) (y : H),
    ContDiffOn 𝕜 n ((↑(extChartAt I y) : H → E) ∘ e ∘ (↑(extChartAt I x).symm : E → M))
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' e ⁻¹' (extChartAt I y).source)
⊢ Continuous[inst_4, inst_3] e ∧
    ∀ (x : M) (y : H),
      ContDiffOn 𝕜 n ((↑(extChartAt I y) : H → E) ∘ e ∘ (↑(extChartAt I x).symm : E → M))
        ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' e ⁻¹' (extChartAt I y).source)

Tactic:
use h.continuous

Premises used: Topology.IsOpenEmbedding.continuous
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this : IsManifold I ω M
x : M
y : H
right :
  ∀ x_1 ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' e ⁻¹' (extChartAt I y).source,
    ((↑(extChartAt I y) : H → E) ∘ e ∘ (↑(extChartAt I x).symm : E → M)) x_1 = id x_1
⊢ ContDiffOn 𝕜 n ((↑(extChartAt I y) : H → E) ∘ e ∘ (↑(extChartAt I x).symm : E → M))
    ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' e ⁻¹' (extChartAt I y).source)

Tactic:
apply contDiffOn_id.congr

Premises used: ContDiffOn.congr, contDiffOn_id
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this : IsManifold I ω M
x : M
y : H
z : E
hz : z ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' e ⁻¹' (extChartAt I y).source
right : (↑I : H → E) (e ((↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ((↑I.symm : E → H) z))) = z
⊢ ((↑(extChartAt I y) : H → E) ∘ e ∘ (↑(extChartAt I x).symm : E → M)) z = id z

Tactic:
simp only [mfld_simps]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this : IsManifold I ω M
x : M
y : H
z : E
hz : z ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' e ⁻¹' (extChartAt I y).source
right : (↑I : H → E) ((↑I.symm : E → H) z) = z
right₁ : (↑I.symm : E → H) z ∈ range e
⊢ (↑I : H → E) (e ((↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ((↑I.symm : E → H) z))) = z

Tactic:
rw [h.toOpenPartialHomeomorph_right_inv]

Premises used: Topology.IsOpenEmbedding.toOpenPartialHomeomorph_right_inv
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this : IsManifold I ω M
x : M
y : H
z : E
hz : z ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' e ⁻¹' (extChartAt I y).source
right : z ∈ range (↑I : H → E)
⊢ (↑I : H → E) ((↑I.symm : E → H) z) = z

Tactic:
rw [I.right_inv]

Premises used: ModelWithCorners.right_inv
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this : IsManifold I ω M
x : M
y : H
z : E
hz : z ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' e ⁻¹' (extChartAt I y).source
apply : (extChartAt I x).target ⊆ range (↑I : H → E)
⊢ z ∈ range (↑I : H → E)

Tactic:
apply mem_of_subset_of_mem _ hz.1

Premises used: Set.mem_of_subset_of_mem, And.left
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this : IsManifold I ω M
x : M
y : H
z : E
hz : z ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' e ⁻¹' (extChartAt I y).source
⊢ (extChartAt I x).target ⊆ range (↑I : H → E)

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

Premises used: extChartAt_target_subset_range
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this : IsManifold I ω M
x : M
y : H
z : E
hz : z ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' e ⁻¹' (extChartAt I y).source
⊢ (extChartAt I x).target ⊆ range (↑I : H → E)

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

Premises used: extChartAt_target_subset_range
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this : IsManifold I ω M
x : M
y : H
z : E
hz : z ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' e ⁻¹' (extChartAt I y).source
⊢ z ∈ (extChartAt I x).target

Tactic:
have := hz.1
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this_1 : IsManifold I ω M
x : M
y : H
z : E
hz : z ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' e ⁻¹' (extChartAt I y).source
this : z ∈ (extChartAt I x).target
⊢ z ∈ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E)

Tactic:
rw [@extChartAt_target _ _ _ _ _ _ _ _ _ _ h.singletonChartedSpace] at this

Premises used: extChartAt_target
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this_1 : IsManifold I ω M
x : M
y : H
z : E
hz : z ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' e ⁻¹' (extChartAt I y).source
this : z ∈ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E)
⊢ z ∈ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target

Tactic:
have := this.1
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this_1 : IsManifold I ω M
x : M
y : H
z : E
hz : z ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' e ⁻¹' (extChartAt I y).source
this_2 : z ∈ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E)
this : z ∈ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target
⊢ (↑I.symm : E → H) z ∈ range e

Tactic:
rw [mem_preimage, OpenPartialHomeomorph.singletonChartedSpace_chartAt_eq,
      h.toOpenPartialHomeomorph_target] at this

Premises used: Topology.IsOpenEmbedding.toOpenPartialHomeomorph_target, OpenPartialHomeomorph.singletonChartedSpace_chartAt_eq, Set.mem_preimage
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this_1 : IsManifold I ω M
x : M
y : H
z : E
hz : z ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' e ⁻¹' (extChartAt I y).source
this_2 : z ∈ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E)
this : (↑I.symm : E → H) z ∈ range e
⊢ (↑I.symm : E → H) z ∈ range e

Tactic:
this
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this_1 : IsManifold I ω M
x : M
y : H
z : E
hz : z ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' e ⁻¹' (extChartAt I y).source
this_2 : z ∈ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E)
this : (↑I.symm : E → H) z ∈ range e
⊢ (↑I.symm : E → H) z ∈ range e

Tactic:
exact this
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this : IsManifold I ω M
rw :
  ContinuousOn (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) (range e) ∧
    ∀ (x : H) (y : M),
      ContDiffOn 𝕜 n
        ((↑(extChartAt I y) : M → E) ∘
          (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ∘ (↑(extChartAt I x).symm : E → H))
        ((extChartAt I x).target ∩
          (↑(extChartAt I x).symm : E → H) ⁻¹'
            (range e ∩ (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ⁻¹' (extChartAt I y).source))
⊢ ContMDiffOn I I n (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) (range e)

Tactic:
rw [@contMDiffOn_iff]

Premises used: contMDiffOn_iff
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this : IsManifold I ω M
left : ContinuousOn (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) (range e)
right :
  ∀ (x : H) (y : M),
    ContDiffOn 𝕜 n
      ((↑(extChartAt I y) : M → E) ∘
        (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ∘ (↑(extChartAt I x).symm : E → H))
      ((extChartAt I x).target ∩
        (↑(extChartAt I x).symm : E → H) ⁻¹'
          (range e ∩ (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ⁻¹' (extChartAt I y).source))
⊢ ContinuousOn (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) (range e) ∧
    ∀ (x : H) (y : M),
      ContDiffOn 𝕜 n
        ((↑(extChartAt I y) : M → E) ∘
          (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ∘ (↑(extChartAt I x).symm : E → H))
        ((extChartAt I x).target ∩
          (↑(extChartAt I x).symm : E → H) ⁻¹'
            (range e ∩ (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ⁻¹' (extChartAt I y).source))

Tactic:
constructor
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this : IsManifold I ω M
left :
  ContinuousOn (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M)
    (IsOpenEmbedding.toOpenPartialHomeomorph e h).target
⊢ ContinuousOn (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) (range e)

Tactic:
rw [← h.toOpenPartialHomeomorph_target]

Premises used: Topology.IsOpenEmbedding.toOpenPartialHomeomorph_target
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this : IsManifold I ω M
⊢ ContinuousOn (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M)
    (IsOpenEmbedding.toOpenPartialHomeomorph e h).target

Tactic:
(h.toOpenPartialHomeomorph e).continuousOn_symm

Premises used: Topology.IsOpenEmbedding.toOpenPartialHomeomorph, OpenPartialHomeomorph.continuousOn_symm
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this : IsManifold I ω M
⊢ ContinuousOn (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M)
    (IsOpenEmbedding.toOpenPartialHomeomorph e h).target

Tactic:
exact (h.toOpenPartialHomeomorph e).continuousOn_symm

Premises used: Topology.IsOpenEmbedding.toOpenPartialHomeomorph, OpenPartialHomeomorph.continuousOn_symm
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this : IsManifold I ω M
z : H
hz : M
right :
  ∀
    x ∈
      (extChartAt I z).target ∩
        (↑(extChartAt I z).symm : E → H) ⁻¹'
          (range e ∩ (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ⁻¹' (extChartAt I hz).source),
    ((↑(extChartAt I hz) : M → E) ∘
          (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ∘ (↑(extChartAt I z).symm : E → H))
        x =
      id x
⊢ ContDiffOn 𝕜 n
    ((↑(extChartAt I hz) : M → E) ∘
      (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ∘ (↑(extChartAt I z).symm : E → H))
    ((extChartAt I z).target ∩
      (↑(extChartAt I z).symm : E → H) ⁻¹'
        (range e ∩ (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ⁻¹' (extChartAt I hz).source))

Tactic:
apply contDiffOn_id.congr

Premises used: ContDiffOn.congr, contDiffOn_id
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this : IsManifold I ω M
z_1 : H
hz_1 : M
z : E
hz :
  z ∈
    (extChartAt I z_1).target ∩
      (↑(extChartAt I z_1).symm : E → H) ⁻¹'
        (range e ∩ (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ⁻¹' (extChartAt I hz_1).source)
right : (↑I : H → E) (e ((↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ((↑I.symm : E → H) z))) = z
⊢ ((↑(extChartAt I hz_1) : M → E) ∘
        (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ∘ (↑(extChartAt I z_1).symm : E → H))
      z =
    id z

Tactic:
simp only [mfld_simps]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this : IsManifold I ω M
z_1 : H
hz_1 : M
z : E
hz :
  z ∈
    (extChartAt I z_1).target ∩
      (↑(extChartAt I z_1).symm : E → H) ⁻¹'
        (range e ∩ (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ⁻¹' (extChartAt I hz_1).source)
rw : z ∈ (↑I.symm : E → H) ⁻¹' range e
⊢ (↑I.symm : E → H) z ∈ range e

Tactic:
rw [ModelWithCorners.symm, ← mem_preimage]

Premises used: ModelWithCorners.symm, Set.mem_preimage
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this : IsManifold I ω M
z_1 : H
hz_1 : M
z : E
hz :
  z ∈
    (extChartAt I z_1).target ∩
      (↑(extChartAt I z_1).symm : E → H) ⁻¹'
        (range e ∩ (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ⁻¹' (extChartAt I hz_1).source)
⊢ z ∈ (↑I.symm : E → H) ⁻¹' range e

Tactic:
hz.2.1

Premises used: Set.Mem, setOf, And.right, Set.preimage, And.left, Set.range
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this : IsManifold I ω M
z_1 : H
hz_1 : M
z : E
hz :
  z ∈
    (extChartAt I z_1).target ∩
      (↑(extChartAt I z_1).symm : E → H) ⁻¹'
        (range e ∩ (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ⁻¹' (extChartAt I hz_1).source)
⊢ z ∈ (↑I.symm : E → H) ⁻¹' range e

Tactic:
exact hz.2.1

Premises used: And.right, And.left
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this : IsManifold I ω M
z_1 : H
hz_1 : M
z : E
hz :
  z ∈
    (extChartAt I z_1).target ∩
      (↑(extChartAt I z_1).symm : E → H) ⁻¹'
        (range e ∩ (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ⁻¹' (extChartAt I hz_1).source)
⊢ (↑I.symm : E → H) z ∈ range e

Tactic:
have : I.symm z ∈ range e := by
      rw [ModelWithCorners.symm, ← mem_preimage]
      exact hz.2.1
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this_1 : IsManifold I ω M
z_1 : H
hz_1 : M
z : E
hz :
  z ∈
    (extChartAt I z_1).target ∩
      (↑(extChartAt I z_1).symm : E → H) ⁻¹'
        (range e ∩ (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ⁻¹' (extChartAt I hz_1).source)
this : (↑I.symm : E → H) z ∈ range e
right : (↑I : H → E) ((↑I.symm : E → H) z) = z
⊢ (↑I : H → E) (e ((↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ((↑I.symm : E → H) z))) = z

Tactic:
rw [h.toOpenPartialHomeomorph_right_inv e this]

Premises used: Topology.IsOpenEmbedding.toOpenPartialHomeomorph_right_inv
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this_1 : IsManifold I ω M
z_1 : H
hz_1 : M
z : E
hz :
  z ∈
    (extChartAt I z_1).target ∩
      (↑(extChartAt I z_1).symm : E → H) ⁻¹'
        (range e ∩ (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ⁻¹' (extChartAt I hz_1).source)
this : (↑I.symm : E → H) z ∈ range e
right : z ∈ range (↑I : H → E)
⊢ (↑I : H → E) ((↑I.symm : E → H) z) = z

Tactic:
apply I.right_inv

Premises used: ModelWithCorners.right_inv