awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Immersion
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
⊢ NormedAddCommGroup ⋯.smallComplement

Tactic:
infer_instance
-- Module: Mathlib.Geometry.Manifold.Immersion
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
⊢ NormedSpace.{u_1, u} 𝕜 ⋯.smallComplement

Tactic:
infer_instance
-- Module: Mathlib.Geometry.Manifold.Immersion
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
h₁ : IsImmersionOfComplement ⋯.smallComplement I J n f
⊢ IsImmersion I J n f

Tactic:
use (h x).smallComplement, by infer_instance, by infer_instance

Premises used: Manifold.IsImmersionAtOfComplement.smallComplement
-- Module: Mathlib.Geometry.Manifold.Immersion
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
⊢ IsImmersionOfComplement ⋯.smallComplement I J n f

Tactic:
(IsImmersionOfComplement.congr_F (h x).smallEquiv).mp h

Premises used: Manifold.IsImmersionAtOfComplement.smallEquiv, Iff.mp, Manifold.IsImmersionOfComplement.congr_F
-- Module: Mathlib.Geometry.Manifold.Immersion
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
⊢ IsImmersionOfComplement ⋯.smallComplement I J n f

Tactic:
exact (IsImmersionOfComplement.congr_F (h x).smallEquiv).mp h

Premises used: Manifold.IsImmersionAtOfComplement.smallEquiv, Iff.mp, Manifold.IsImmersionOfComplement.congr_F
-- Module: Mathlib.Geometry.Manifold.Immersion
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
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
⊢ IsImmersionAtOfComplement PUnit.{u_15 + 1} I I n id x

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)

Premises used: mem_chart_source, ContinuousLinearEquiv.prodUnique, chartAt, IsManifold.chart_mem_maximalAtlas, Manifold.IsImmersionAtOfComplement.mk_of_continuousAt, continuousAt_id
-- Module: Mathlib.Geometry.Manifold.Immersion
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.symm : E → H) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target

Tactic:
simp_all
-- Module: Mathlib.Geometry.Manifold.Immersion
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
⊢ y ∈ range (↑I : H → E)

Tactic:
simp_all
-- Module: Mathlib.Geometry.Manifold.Immersion
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
rw₁ rw₂ : y = y
⊢ (↑I : H → E)
      ((↑(chartAt H x) : M → H) ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) y))) =
    y

Tactic:
rw [(chartAt H x).right_inv (by simp_all), I.right_inv (by simp_all)]

Premises used: chartAt, ModelWithCorners.right_inv, OpenPartialHomeomorph.right_inv
-- Module: Mathlib.Geometry.Manifold.Immersion
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

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)]
-- Module: Mathlib.Geometry.Manifold.Immersion
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
this :
  (↑I : H → E)
      ((↑(chartAt H x) : M → H) ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) y))) =
    y
⊢ ((↑(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

Tactic:
simpa
-- Module: Mathlib.Geometry.Manifold.Immersion
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
⊢ IsImmersionOfComplement.{u_2, u_1, u_2, u_15, u_7, u_7, u_11, u_11} PUnit.{u_15 + 1} I I (M := ↥s) n
    (Subtype.val (p := fun (x : M) ↦ x ∈ s))

Tactic:
fun y ↦ IsImmersionAtOfComplement.of_opens s y

Premises used: Manifold.IsImmersionAtOfComplement.of_opens, Manifold.IsImmersionOfComplement
-- Module: Mathlib.Geometry.Manifold.Immersion
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
⊢ IsImmersionOfComplement h.complement I J n f

Tactic:
Classical.choose_spec <| Classical.choose_spec <| Classical.choose_spec h

Premises used: Classical.choose_spec, Manifold.IsImmersion.complement
-- Module: Mathlib.Geometry.Manifold.Immersion
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
⊢ NormedAddCommGroup h.complement

Tactic:
infer_instance
-- Module: Mathlib.Geometry.Manifold.Immersion
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
⊢ NormedSpace.{u_1, u} 𝕜 h.complement

Tactic:
infer_instance
-- Module: Mathlib.Geometry.Manifold.Immersion
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
h₁ : IsImmersionAtOfComplement h.complement I J n f x
⊢ ∃ (F : Type u) (x_1 : NormedAddCommGroup F) (x_2 : NormedSpace 𝕜 F), IsImmersionAtOfComplement F I J n f x

Tactic:
use h.complement, by infer_instance, by infer_instance

Premises used: Manifold.IsImmersion.complement
-- Module: Mathlib.Geometry.Manifold.Immersion
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
⊢ IsImmersionAtOfComplement h.complement I J n f x

Tactic:
h.isImmersionOfComplement_complement x

Premises used: Manifold.IsImmersion.isImmersionOfComplement_complement
-- Module: Mathlib.Geometry.Manifold.Immersion
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
⊢ IsImmersionAtOfComplement h.complement I J n f x

Tactic:
exact h.isImmersionOfComplement_complement x

Premises used: Manifold.IsImmersion.isImmersionOfComplement_complement
-- Module: Mathlib.Geometry.Manifold.Immersion
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
h : IsImmersion I J n f
heq : f = g
⊢ IsImmersion I J n g

Tactic:
heq ▸ h

Premises used: Eq.rec
-- Module: Mathlib.Geometry.Manifold.Immersion
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
E' : Type u_3
E''' : Type u_4
E'' : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
inst_5 : NormedAddCommGroup E''
inst_6 : NormedSpace 𝕜 E''
inst_7 : NormedAddCommGroup E'''
inst_8 : NormedSpace 𝕜 E'''
H : Type u_7
inst_9 : TopologicalSpace H
H' : Type u_8
inst_10 : TopologicalSpace H'
G : Type u_9
inst_11 : TopologicalSpace G
G' : Type u_10
inst_12 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
inst_13 : TopologicalSpace M
inst_14 : ChartedSpace H M
M' : Type u_12
inst_15 : TopologicalSpace M'
inst_16 : ChartedSpace H' M'
N : Type u_13
inst_17 : TopologicalSpace N
inst_18 : ChartedSpace G N
N' : Type u_14
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
n : ℕ∞ω
f : M → N
g : M' → N'
inst_21 : IsManifold I n M
inst_22 : IsManifold I' n M'
inst_23 : IsManifold J n N
inst_24 : IsManifold J' n N'
hf : IsImmersion I J n f
hg : IsImmersion I' J' n g
⊢ IsImmersion (I.prod I') (J.prod J') n (Prod.map f g)

Tactic:
(hf.isImmersionOfComplement_complement.prodMap hg.isImmersionOfComplement_complement).isImmersion

Premises used: Manifold.IsImmersionOfComplement.prodMap, Manifold.IsImmersion.isImmersionOfComplement_complement, Manifold.IsImmersionOfComplement.isImmersion
-- Module: Mathlib.Geometry.Manifold.Immersion
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
⊢ NormedAddCommGroup PUnit.{u_2 + 1}

Tactic:
infer_instance
-- Module: Mathlib.Geometry.Manifold.Immersion
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
⊢ NormedSpace 𝕜 PUnit.{u_2 + 1}

Tactic:
infer_instance
-- Module: Mathlib.Geometry.Manifold.Immersion
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
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
⊢ IsImmersion.{u_2, u_1, u_2, u_7, u_7, u_11, u_11} I I (M := M) n id

Tactic:
use PUnit, by infer_instance, by infer_instance

Premises used: PUnit
-- Module: Mathlib.Geometry.Manifold.Immersion
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
⊢ 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:
IsImmersionOfComplement.id

Premises used: Manifold.IsImmersionOfComplement.id
-- Module: Mathlib.Geometry.Manifold.Immersion
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
⊢ 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:
exact IsImmersionOfComplement.id

Premises used: Manifold.IsImmersionOfComplement.id
-- Module: Mathlib.Geometry.Manifold.Immersion
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
⊢ NormedAddCommGroup PUnit.{u_2 + 1}

Tactic:
infer_instance
-- Module: Mathlib.Geometry.Manifold.Immersion
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
⊢ NormedSpace 𝕜 PUnit.{u_2 + 1}

Tactic:
infer_instance
-- Module: Mathlib.Geometry.Manifold.Immersion
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
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))
⊢ 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))

Tactic:
use PUnit, by infer_instance, by infer_instance

Premises used: PUnit
-- Module: Mathlib.Geometry.Manifold.Immersion
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
⊢ 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:
IsImmersionOfComplement.of_opens s

Premises used: Manifold.IsImmersionOfComplement.of_opens
-- Module: Mathlib.Geometry.Manifold.Immersion
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
⊢ 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:
exact IsImmersionOfComplement.of_opens s

Premises used: Manifold.IsImmersionOfComplement.of_opens
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
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)
⊢ ContMDiffAt (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) 𝓘(ℝ, ℝ) (M' := ℝ) n
    (fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) z

Tactic:
rw [contMDiffAt_iff]

Premises used: contMDiffAt_iff
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
⊢ ContinuousAt (Y := ℝ) (fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) z

Tactic:
fun_prop
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
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)
⊢ 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:
refine ⟨by fun_prop, ?_⟩