awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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'
inst_11 : T2Space M
inst_12 : One M'
n : ℕ∞ω
U : Opens M
f : ↥U → M'
supp : HasCompactMulSupport f
diff : ContMDiff I I' n f
x_1 x : M
h : x ∈ mulTSupport (extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1)
⊢ ContMDiffAt I I' n (extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1) x
have lift : ∀ (x : ↥U) (h : (↑x : M) ∈ mulTSupport (extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1)),
  ContMDiffAt I I' n (extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1) (↑x : M)
Tactic: lift x to U using Subtype.coe_image_subset _ _
    (supp.mulTSupport_extend_one_subset continuous_subtype_val h)
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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'
inst_11 : T2Space M
inst_12 : One M'
n : ℕ∞ω
U : Opens M
f : ↥U → M'
supp : HasCompactMulSupport f
diff : ContMDiff I I' n f
x_1 : M
x : ↥U
h : (↑x : M) ∈ mulTSupport (extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1)
⊢ ContMDiffAt I I' n (extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1) (↑x : M)
have rw : ContMDiffAt.{u_1, u_2, u_3, u_4, u_5, u_6, u_7} I I' (M' := M') n
  (fun (x : ↥U) ↦ extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1 (↑x : M)) x
Tactic: rw [← contMDiffAt_subtype_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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'
inst_11 : T2Space M
inst_12 : One M'
n : ℕ∞ω
U : Opens M
f : ↥U → M'
supp : HasCompactMulSupport f
diff : ContMDiff I I' n f
x_1 : M
x : ↥U
h : (↑x : M) ∈ mulTSupport (extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1)
⊢ ContMDiffAt.{u_1, u_2, u_3, u_4, u_5, u_6, u_7} I I' (M' := M') n
    (fun (x : ↥U) ↦ extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1 (↑x : M)) x
have simp_rw : ContMDiffAt I I' n (extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1 ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) x
Tactic: simp_rw [← comp_def]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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'
inst_11 : T2Space M
inst_12 : One M'
n : ℕ∞ω
U : Opens M
f : ↥U → M'
supp : HasCompactMulSupport f
diff : ContMDiff I I' n f
x_1 : M
x : ↥U
h : (↑x : M) ∈ mulTSupport (extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1)
⊢ ContMDiffAt I I' n (extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1 ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) x
have rw : ContMDiffAt I I' n f x
Tactic: rw [extend_comp Subtype.val_injective]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ ContMDiffAt I I' ∞ (Subtype.val (p := fun (x : M') ↦ x ∈ U) ∘ f) x ↔ ContMDiffAt I I' ∞ f x
have rw : ContMDiffWithinAt I I' ∞ (Subtype.val (p := fun (x : M') ↦ x ∈ U) ∘ f) univ x ↔ ContMDiffAt I I' ∞ f x
Tactic: rw [ContMDiffAt, ContMDiffAt, ContMDiffWithinAt.subtypeVal_comp_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ ContMDiffAt I I' ∞ (Subtype.val (p := fun (x : M') ↦ x ∈ U) ∘ f) x ↔ ContMDiffAt I I' ∞ f x
have rw₁ : ContMDiffWithinAt I I' ∞ (Subtype.val (p := fun (x : M') ↦ x ∈ U) ∘ f) univ x ↔ ContMDiffWithinAt I I' ∞ f univ x
Tactic: rw [ContMDiffAt, ContMDiffAt, ContMDiffWithinAt.subtypeVal_comp_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ ContMDiffAt I I' ∞ (Subtype.val (p := fun (x : M') ↦ x ∈ U) ∘ f) x ↔ ContMDiffAt I I' ∞ f x
have rw₂ : ContMDiffWithinAt I I' ∞ f univ x ↔ ContMDiffWithinAt I I' ∞ f univ x
Tactic: rw [ContMDiffAt, ContMDiffAt, ContMDiffWithinAt.subtypeVal_comp_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (hypothesis)
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
⊢ ContMDiff I I n e
have this : IsManifold I ω M
Tactic: haveI := h.isManifold_singleton (I := I) (n := ω)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ ContMDiff I I n e
have 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)
Tactic: rw [@contMDiff_iff _ _ _ _ _ _ _ _ _ _ h.singletonChartedSpace]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ 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)
have 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)
Tactic: use h.continuous
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ 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)
have 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
Tactic: apply contDiffOn_id.congr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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 y) : H → E) ∘ e ∘ (↑(extChartAt I x).symm : E → M)) z = id z
have right : (↑I : H → E) (e ((↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ((↑I.symm : E → H) z))) = z
Tactic: simp only [mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ (↑I : H → E) (e ((↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ((↑I.symm : E → H) z))) = z
have right : (↑I : H → E) ((↑I.symm : E → H) z) = z
Tactic: rw [h.toOpenPartialHomeomorph_right_inv]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ (↑I : H → E) (e ((↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ((↑I.symm : E → H) z))) = z
have right₁ : (↑I.symm : E → H) z ∈ range e
Tactic: rw [h.toOpenPartialHomeomorph_right_inv]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ (↑I : H → E) ((↑I.symm : E → H) z) = z
have right : z ∈ range (↑I : H → E)
Tactic: rw [I.right_inv]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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 ∈ range (↑I : H → E)
have apply : (extChartAt I x).target ⊆ range (↑I : H → E)
Tactic: apply mem_of_subset_of_mem _ hz.1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (hypothesis)
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
⊢ (↑I.symm : E → H) z ∈ range e
have this₁ : z ∈ (extChartAt I x).target
Tactic: have := hz.1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (hypothesis)
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
⊢ (↑I.symm : E → H) z ∈ range e
have this₁ : z ∈ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E)
Tactic: rw [@extChartAt_target _ _ _ _ _ _ _ _ _ _ h.singletonChartedSpace] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (hypothesis)
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)
⊢ (↑I.symm : E → H) z ∈ range e
have this₁ : z ∈ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target
Tactic: have := this.1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (hypothesis)
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
⊢ ContMDiffOn I I n (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) (range e)
have this : IsManifold I ω M
Tactic: haveI := h.isManifold_singleton (I := I) (n := ω)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ ContMDiffOn I I n (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) (range e)
have 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))
Tactic: rw [@contMDiffOn_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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) (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))
have left : ContinuousOn (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) (range e)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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)
⊢ 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))
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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) (range e)
have left : ContinuousOn (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M)
  (IsOpenEmbedding.toOpenPartialHomeomorph e h).target
Tactic: rw [← h.toOpenPartialHomeomorph_target]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ 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))
have 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
Tactic: apply contDiffOn_id.congr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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)
⊢ ((↑(extChartAt I hz_1) : M → E) ∘
        (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ∘ (↑(extChartAt I z_1).symm : E → H))
      z =
    id z
have right : (↑I : H → E) (e ((↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ((↑I.symm : E → H) z))) = z
Tactic: simp only [mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
have rw : z ∈ (↑I.symm : E → H) ⁻¹' range e
Tactic: rw [ModelWithCorners.symm, ← mem_preimage]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (hypothesis)
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 : H → E) (e ((↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ((↑I.symm : E → H) z))) = z
have this₁ : (↑I.symm : E → H) z ∈ range e
Tactic: have : I.symm z ∈ range e := by
      rw [ModelWithCorners.symm, ← mem_preimage]
      exact hz.2.1