awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_7
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
inst_6 : IsManifold I n M
s : TopologicalSpace.Opens M
y : ↥s
x : E
hx : x ∈ (OpenPartialHomeomorph.extend (chartAt H y) I).target
⊢ ((↑(OpenPartialHomeomorph.extend (chartAt H (↑y : M)) I) : M → E) ∘
        Subtype.val (p := fun (x : M) ↦ x ∈ s) ∘ (↑(OpenPartialHomeomorph.extend (chartAt H y) I).symm : E → ↥s))
      x =
    comp (β := E × PUnit.{u_15 + 1})
      (⇑(ContinuousLinearEquiv.prodUnique 𝕜 E PUnit.{u_15 + 1}) : (a : E × PUnit.{u_15 + 1}) → E) (fun (x : E) ↦ (x, 0))
      x
have suffices : (↑I : H → E)
    ((↑(chartAt H y) : ↥s → H) ((↑(OpenPartialHomeomorph.symm (chartAt H y)) : H → ↥s) ((↑I.symm : E → H) x))) =
  x
Tactic: suffices I ((chartAt H ↑y) ((chartAt H y).symm (I.symm x))) = x by simpa +contextual
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
F : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup E''
inst_4 : NormedSpace 𝕜 E''
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_7
inst_7 : TopologicalSpace H
G : Type u_9
inst_8 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace H M
N : Type u_13
inst_11 : TopologicalSpace N
inst_12 : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
equiv : (E × F) ≃L[𝕜] E''
domChart : OpenPartialHomeomorph M H
codChart : OpenPartialHomeomorph N G
hx : x ∈ domChart.source
hfx : f x ∈ codChart.source
hdomChart : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (IsManifold.maximalAtlas I n M) domChart
hcodChart : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (IsManifold.maximalAtlas J n N) codChart
hsource : domChart.source ⊆ f ⁻¹' codChart.source
hwrittenInExtend :
  EqOn ((↑(codChart.extend J) : N → E'') ∘ f ∘ (↑(domChart.extend I).symm : E → M))
    (comp (β := E × F) (⇑equiv : (a : E × F) → E'') fun (x : E) ↦ (x, 0)) (domChart.extend I).target
⊢ IsImmersionAt I J n f x
have aux : IsImmersionAtOfComplement F I J n f x
Tactic: have aux : IsImmersionAtOfComplement F I J n f x := by
    apply IsImmersionAtOfComplement.mk_of_charts <;> assumption
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
F : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup E''
inst_4 : NormedSpace 𝕜 E''
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_7
inst_7 : TopologicalSpace H
G : Type u_9
inst_8 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace H M
N : Type u_13
inst_11 : TopologicalSpace N
inst_12 : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
equiv : (E × F) ≃L[𝕜] E''
domChart : OpenPartialHomeomorph M H
codChart : OpenPartialHomeomorph N G
hx : x ∈ domChart.source
hfx : f x ∈ codChart.source
hdomChart : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (IsManifold.maximalAtlas I n M) domChart
hcodChart : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (IsManifold.maximalAtlas J n N) codChart
hsource : domChart.source ⊆ f ⁻¹' codChart.source
hwrittenInExtend :
  EqOn ((↑(codChart.extend J) : N → E'') ∘ f ∘ (↑(domChart.extend I).symm : E → M))
    (comp (β := E × F) (⇑equiv : (a : E × F) → E'') fun (x : E) ↦ (x, 0)) (domChart.extend I).target
aux : IsImmersionAtOfComplement F I J n f x
⊢ IsImmersionAt I J n f x
have h : IsImmersionAtOfComplement aux.smallComplement I J n f x
Tactic: use aux.smallComplement, by infer_instance, by infer_instance
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
F : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup E''
inst_4 : NormedSpace 𝕜 E''
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_7
inst_7 : TopologicalSpace H
G : Type u_9
inst_8 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace H M
N : Type u_13
inst_11 : TopologicalSpace N
inst_12 : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
hf : ContinuousAt f x
equiv : (E × F) ≃L[𝕜] E''
domChart : OpenPartialHomeomorph M H
codChart : OpenPartialHomeomorph N G
hx : x ∈ domChart.source
hfx : f x ∈ codChart.source
hdomChart : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (IsManifold.maximalAtlas I n M) domChart
hcodChart : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (IsManifold.maximalAtlas J n N) codChart
hwrittenInExtend :
  EqOn ((↑(codChart.extend J) : N → E'') ∘ f ∘ (↑(domChart.extend I).symm : E → M))
    (comp (β := E × F) (⇑equiv : (a : E × F) → E'') fun (x : E) ↦ (x, 0)) (domChart.extend I).target
⊢ IsImmersionAt I J n f x
have aux : IsImmersionAtOfComplement F I J n f x
Tactic: have aux : IsImmersionAtOfComplement F I J n f x := by
    apply IsImmersionAtOfComplement.mk_of_continuousAt <;> assumption
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
F : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup E''
inst_4 : NormedSpace 𝕜 E''
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_7
inst_7 : TopologicalSpace H
G : Type u_9
inst_8 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace H M
N : Type u_13
inst_11 : TopologicalSpace N
inst_12 : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
hf : ContinuousAt f x
equiv : (E × F) ≃L[𝕜] E''
domChart : OpenPartialHomeomorph M H
codChart : OpenPartialHomeomorph N G
hx : x ∈ domChart.source
hfx : f x ∈ codChart.source
hdomChart : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (IsManifold.maximalAtlas I n M) domChart
hcodChart : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (IsManifold.maximalAtlas J n N) codChart
hwrittenInExtend :
  EqOn ((↑(codChart.extend J) : N → E'') ∘ f ∘ (↑(domChart.extend I).symm : E → M))
    (comp (β := E × F) (⇑equiv : (a : E × F) → E'') fun (x : E) ↦ (x, 0)) (domChart.extend I).target
aux : IsImmersionAtOfComplement F I J n f x
⊢ IsImmersionAt I J n f x
have h : IsImmersionAtOfComplement aux.smallComplement I J n f x
Tactic: use aux.smallComplement, by infer_instance, by infer_instance
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup E''
inst_4 : NormedSpace 𝕜 E''
H : Type u_7
inst_5 : TopologicalSpace H
G : Type u_9
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_13
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
f g : M → N
x : M
hf : IsImmersionAt I J n f x
hfg : f =ᶠ[𝓝 x] g
⊢ IsImmersionAt I J n g x
have h : IsImmersionAtOfComplement hf.complement I J n g x
Tactic: use hf.complement, by infer_instance, by infer_instance
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup E''
inst_4 : NormedSpace 𝕜 E''
H : Type u_7
inst_5 : TopologicalSpace H
G : Type u_9
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_13
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
f : M → N
⊢ IsOpen[inst_7] {x : M | IsImmersionAt I J n f x}
have rw : ∀ (x : M),
  Membership.mem (γ := Set M) {x : M | IsImmersionAt I J n f x} x →
    ∃ t ⊆ {x : M | IsImmersionAt I J n f x}, IsOpen[inst_7] t ∧ x ∈ t
Tactic: rw [isOpen_iff_forall_mem_open]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_7
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
x : M
inst_6 : IsManifold I n M
s : TopologicalSpace.Opens M
hx : x ∈ s
⊢ IsImmersionAt I I n (Subtype.val (p := fun (x : M) ↦ x ∈ s)) (Subtype.mk (p := fun (x : M) ↦ x ∈ s) x hx)
have h : IsImmersionAtOfComplement PUnit.{u_2 + 1} I I n (Subtype.val (p := fun (x : M) ↦ x ∈ s))
  (Subtype.mk (p := fun (x : M) ↦ x ∈ s) x hx)
Tactic: use PUnit, by infer_instance, by infer_instance
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
F : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup E''
inst_4 : NormedSpace 𝕜 E''
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_7
inst_7 : TopologicalSpace H
G : Type u_9
inst_8 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace H M
N : Type u_13
inst_11 : TopologicalSpace N
inst_12 : ChartedSpace G N
n : ℕ∞ω
f : M → N
h : IsImmersionOfComplement F I J n f
⊢ IsImmersion I J n f
have pos : ∀ (hM : IsEmpty M), IsImmersion I J n f
Tactic: by_cases! hM : IsEmpty M
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
F : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup E''
inst_4 : NormedSpace 𝕜 E''
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_7
inst_7 : TopologicalSpace H
G : Type u_9
inst_8 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace H M
N : Type u_13
inst_11 : TopologicalSpace N
inst_12 : ChartedSpace G N
n : ℕ∞ω
f : M → N
h : IsImmersionOfComplement F I J n f
pos : ∀ (hM : IsEmpty M), IsImmersion I J n f
⊢ IsImmersion I J n f
have neg : ∀ (hM : Nonempty M), IsImmersion I J n f
Tactic: by_cases! hM : IsEmpty M
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
F : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup E''
inst_4 : NormedSpace 𝕜 E''
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_7
inst_7 : TopologicalSpace H
G : Type u_9
inst_8 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace H M
N : Type u_13
inst_11 : TopologicalSpace N
inst_12 : ChartedSpace G N
n : ℕ∞ω
f : M → N
h : IsImmersionOfComplement F I J n f
hM : IsEmpty M
⊢ ∃ (F : Type u) (x : NormedAddCommGroup F) (x_1 : NormedSpace 𝕜 F), IsImmersionOfComplement F I J n f
have h₁ : IsImmersionOfComplement PUnit.{u + 1} I J n f
Tactic: use PUnit, by infer_instance, by infer_instance
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
F : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup E''
inst_4 : NormedSpace 𝕜 E''
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_7
inst_7 : TopologicalSpace H
G : Type u_9
inst_8 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace H M
N : Type u_13
inst_11 : TopologicalSpace N
inst_12 : ChartedSpace G N
n : ℕ∞ω
f : M → N
h : IsImmersionOfComplement F I J n f
hM : Nonempty M
⊢ IsImmersion I J n f
have neg : ∀ (inhabited_h : Inhabited M), IsImmersion I J n f
Tactic: inhabit M
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
F : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup E''
inst_4 : NormedSpace 𝕜 E''
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_7
inst_7 : TopologicalSpace H
G : Type u_9
inst_8 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace H M
N : Type u_13
inst_11 : TopologicalSpace N
inst_12 : ChartedSpace G N
n : ℕ∞ω
f : M → N
h : IsImmersionOfComplement F I J n f
hM : Nonempty M
inhabited_h : Inhabited M
x : M := default
⊢ IsImmersion I J n f
have h₁ : IsImmersionOfComplement sorry.smallComplement I J n f
Tactic: use (h x).smallComplement, by infer_instance, by infer_instance
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_7
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
inst_6 : IsManifold I n M
x : M
⊢ IsImmersionAtOfComplement PUnit.{u_15 + 1} I I n id x
have apply : EqOn
  ((↑(OpenPartialHomeomorph.extend (chartAt H x) I) : M → E) ∘
    id ∘ (↑(OpenPartialHomeomorph.extend (chartAt H x) I).symm : E → M))
  (comp (β := E × PUnit.{u_15 + 1})
    (⇑(ContinuousLinearEquiv.prodUnique 𝕜 E PUnit.{u_15 + 1}) : (a : E × PUnit.{u_15 + 1}) → E) fun (x : E) ↦ (x, 0))
  (OpenPartialHomeomorph.extend (chartAt H x) I).target
Tactic: apply IsImmersionAtOfComplement.mk_of_continuousAt (continuousAt_id) (.prodUnique 𝕜 E _)
    (chartAt H x) (chartAt H x) (mem_chart_source H x) (mem_chart_source H x)
    (chart_mem_maximalAtlas x) (chart_mem_maximalAtlas x)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_7
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
inst_6 : IsManifold I n M
x : M
y : E
hy : y ∈ (OpenPartialHomeomorph.extend (chartAt H x) I).target
⊢ (↑I : H → E)
      ((↑(chartAt H x) : M → H) ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) y))) =
    y
have rw : (↑I : H → E) ((↑I.symm : E → H) y) = y
Tactic: rw [(chartAt H x).right_inv (by simp_all), I.right_inv (by simp_all)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_7
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
inst_6 : IsManifold I n M
x : M
y : E
hy : y ∈ (OpenPartialHomeomorph.extend (chartAt H x) I).target
rw : (↑I : H → E) ((↑I.symm : E → H) y) = y
⊢ (↑I : H → E)
      ((↑(chartAt H x) : M → H) ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) y))) =
    y
have rw₁ : y = y
Tactic: rw [(chartAt H x).right_inv (by simp_all), I.right_inv (by simp_all)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_7
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
inst_6 : IsManifold I n M
x : M
y : E
hy : y ∈ (OpenPartialHomeomorph.extend (chartAt H x) I).target
⊢ ((↑(OpenPartialHomeomorph.extend (chartAt H x) I) : M → E) ∘
        id ∘ (↑(OpenPartialHomeomorph.extend (chartAt H x) I).symm : E → M))
      y =
    comp (β := E × PUnit.{u_15 + 1})
      (⇑(ContinuousLinearEquiv.prodUnique 𝕜 E PUnit.{u_15 + 1}) : (a : E × PUnit.{u_15 + 1}) → E) (fun (x : E) ↦ (x, 0))
      y
have this : (↑I : H → E) ((↑(chartAt H x) : M → H) ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) y))) =
  y
Tactic: have : I ((chartAt H x) ((chartAt H x).symm (I.symm y))) = y := by
    rw [(chartAt H x).right_inv (by simp_all), I.right_inv (by simp_all)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup E''
inst_4 : NormedSpace 𝕜 E''
H : Type u_7
inst_5 : TopologicalSpace H
G : Type u_9
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_13
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
f : M → N
h : IsImmersion I J n f
x : M
⊢ ∃ (F : Type u) (x_1 : NormedAddCommGroup F) (x_2 : NormedSpace 𝕜 F), IsImmersionAtOfComplement F I J n f x
have h₁ : IsImmersionAtOfComplement h.complement I J n f x
Tactic: use h.complement, by infer_instance, by infer_instance
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_7
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
inst_6 : IsManifold I n M
⊢ IsImmersion.{u_2, u_1, u_2, u_7, u_7, u_11, u_11} I I (M := M) n id
have h : IsImmersionOfComplement.{u_2, u_1, u_2, u_2, u_7, u_7, u_11, u_11} PUnit.{u_2 + 1} I I (M := M) n id
Tactic: use PUnit, by infer_instance, by infer_instance
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_7
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
inst_6 : IsManifold I n M
s : TopologicalSpace.Opens M
⊢ IsImmersion.{u_2, u_1, u_2, u_7, u_7, u_11, u_11} I I (M := ↥s) n (Subtype.val (p := fun (x : M) ↦ x ∈ s))
have h : IsImmersionOfComplement.{u_2, u_1, u_2, u_2, u_7, u_7, u_11, u_11} PUnit.{u_2 + 1} I I (M := ↥s) n
  (Subtype.val (p := fun (x : M) ↦ x ∈ s))
Tactic: use PUnit, by infer_instance, by infer_instance
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
⊢ ContMDiffAt (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) 𝓘(ℝ, ℝ) (M' := ℝ) n
    (fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) z
have rw : ContinuousAt (Y := ℝ) (fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) z ∧
  ContDiffWithinAt ℝ (E := EuclideanSpace ℝ (Fin 1)) n
    ((↑(extChartAt 𝓘(ℝ, ℝ) (↑z : ℝ)) : ℝ → ℝ) ∘
      (fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) ∘
        (↑(PartialEquiv.symm (extChartAt (H := EuclideanHalfSpace 1) (𝓡∂ 1) z)) :
          EuclideanSpace ℝ (Fin 1) → (↑(Icc x y) : Type)))
    (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))
    ((↑(extChartAt (H := EuclideanHalfSpace 1) (𝓡∂ 1) z) : (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) z)
Tactic: rw [contMDiffAt_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
⊢ ContinuousAt (Y := ℝ) (fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) z ∧
    ContDiffWithinAt ℝ (E := EuclideanSpace ℝ (Fin 1)) n
      ((↑(extChartAt 𝓘(ℝ, ℝ) (↑z : ℝ)) : ℝ → ℝ) ∘
        (fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) ∘
          (↑(PartialEquiv.symm (extChartAt (H := EuclideanHalfSpace 1) (𝓡∂ 1) z)) :
            EuclideanSpace ℝ (Fin 1) → (↑(Icc x y) : Type)))
      (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))
      ((↑(extChartAt (H := EuclideanHalfSpace 1) (𝓡∂ 1) z) : (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) z)
have refine : ContDiffWithinAt ℝ (E := EuclideanSpace ℝ (Fin 1)) n
  ((↑(extChartAt 𝓘(ℝ, ℝ) (↑z : ℝ)) : ℝ → ℝ) ∘
    (fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) ∘
      (↑(PartialEquiv.symm (extChartAt (H := EuclideanHalfSpace 1) (𝓡∂ 1) z)) :
        EuclideanSpace ℝ (Fin 1) → (↑(Icc x y) : Type)))
  (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))
  ((↑(extChartAt (H := EuclideanHalfSpace 1) (𝓡∂ 1) z) : (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) z)
Tactic: refine ⟨by fun_prop, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
⊢ ContDiffWithinAt ℝ (F := ℝ) n
    ((fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) ∘
      (↑(if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y).symm :
          EuclideanHalfSpace 1 → (↑(Icc x y) : Type)) ∘
        (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
    (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))
    ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
      ((↑(if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1)
        z))
have pos : ∀ (hz : (↑z : ℝ) < y),
  ContDiffWithinAt ℝ (F := ℝ) n
    ((fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) ∘
      (↑(IccLeftChart x y).symm : EuclideanHalfSpace 1 → (↑(Icc x y) : Type)) ∘
        (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
    (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))
    ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
      ((↑(IccLeftChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1) z))
Tactic: split_ifs with hz
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
pos :
  ∀ (hz : (↑z : ℝ) < y),
    ContDiffWithinAt ℝ (F := ℝ) n
      ((fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) ∘
        (↑(IccLeftChart x y).symm : EuclideanHalfSpace 1 → (↑(Icc x y) : Type)) ∘
          (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
      (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        ((↑(IccLeftChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1) z))
⊢ ContDiffWithinAt ℝ (F := ℝ) n
    ((fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) ∘
      (↑(if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y).symm :
          EuclideanHalfSpace 1 → (↑(Icc x y) : Type)) ∘
        (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
    (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))
    ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
      ((↑(if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1)
        z))
have neg : ∀ (hz : ¬(↑z : ℝ) < y),
  ContDiffWithinAt ℝ (F := ℝ) n
    ((fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) ∘
      (↑(IccRightChart x y).symm : EuclideanHalfSpace 1 → (↑(Icc x y) : Type)) ∘
        (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
    (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))
    ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
      ((↑(IccRightChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1) z))
Tactic: split_ifs with hz