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
x : M
h : IsImmersionAtOfComplement F I J n f x
⊢ NormedSpace.{u_1, u} 𝕜 h.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
x : M
h : IsImmersionAtOfComplement F I J n f x
h₁ : IsImmersionAtOfComplement h.smallComplement I J n f x
⊢ IsImmersionAt I J n f x

Tactic:
use h.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
x : M
h : IsImmersionAtOfComplement F I J n f x
⊢ IsImmersionAtOfComplement h.smallComplement I J n f x

Tactic:
(IsImmersionAtOfComplement.congr_F h.smallEquiv).mp h

Premises used: Manifold.IsImmersionAtOfComplement.congr_F, Manifold.IsImmersionAtOfComplement.smallEquiv, Iff.mp
-- 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
x : M
h : IsImmersionAtOfComplement F I J n f x
⊢ IsImmersionAtOfComplement h.smallComplement I J n f x

Tactic:
exact (IsImmersionAtOfComplement.congr_F h.smallEquiv).mp h

Premises used: Manifold.IsImmersionAtOfComplement.congr_F, Manifold.IsImmersionAtOfComplement.smallEquiv, Iff.mp
-- 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
y : ↥s
⊢ ContinuousAt (Subtype.val (p := fun (x : M) ↦ x ∈ s)) y

Tactic:
fun_prop
-- 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
y : ↥s
apply :
  EqOn
    ((↑(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))
    (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 y) I).target
⊢ IsImmersionAtOfComplement PUnit.{u_15 + 1} I I n (Subtype.val (p := fun (x : M) ↦ x ∈ s)) y

Tactic:
apply IsImmersionAtOfComplement.mk_of_continuousAt (by fun_prop) (.prodUnique 𝕜 E _)
    (chartAt H y) (chartAt H y.val) (mem_chart_source H y) (mem_chart_source H y.val)
    (chart_mem_maximalAtlas y) (chart_mem_maximalAtlas y.val)

Premises used: mem_chart_source, ContinuousLinearEquiv.prodUnique, chartAt, IsManifold.chart_mem_maximalAtlas, Manifold.IsImmersionAtOfComplement.mk_of_continuousAt, Subtype.val
-- 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
y : ↥s
x : E
hx : x ∈ (OpenPartialHomeomorph.extend (chartAt H y) I).target
this :
  (↑I : H → E)
      ((↑(chartAt H y) : ↥s → H) ((↑(OpenPartialHomeomorph.symm (chartAt H y)) : H → ↥s) ((↑I.symm : E → H) x))) =
    x
⊢ ((↑(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

Tactic:
simpa +contextual
-- 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
y : ↥s
x : E
hx : x ∈ (OpenPartialHomeomorph.extend (chartAt H y) I).target
suffices :
  (↑I : H → E)
      ((↑(chartAt H y) : ↥s → H) ((↑(OpenPartialHomeomorph.symm (chartAt H y)) : H → ↥s) ((↑I.symm : E → H) x))) =
    x
⊢ ((↑(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

Tactic:
suffices I ((chartAt H ↑y) ((chartAt H y).symm (I.symm x))) = x by simpa +contextual
-- 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
y : ↥s
x : E
hx : x ∈ (OpenPartialHomeomorph.extend (chartAt H y) I).target
⊢ (↑I : H → E)
      ((↑(chartAt H y) : ↥s → H) ((↑(OpenPartialHomeomorph.symm (chartAt H y)) : H → ↥s) ((↑I.symm : E → H) x))) =
    x

Tactic:
simp_all
-- 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
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
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
equiv₁ : (E × F) ≃L[𝕜] E''
domChart₁ : OpenPartialHomeomorph M H
codChart₁ : OpenPartialHomeomorph N G
⊢ IsImmersionAtOfComplement F I J n f x

Tactic:
apply IsImmersionAtOfComplement.mk_of_charts

Premises used: Manifold.IsImmersionAtOfComplement.mk_of_charts
-- 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
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
⊢ x ∈ domChart.source

Tactic:
assumption
-- 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
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
⊢ f x ∈ codChart.source

Tactic:
assumption
-- 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
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
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (IsManifold.maximalAtlas I n M) domChart

Tactic:
assumption
-- 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
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
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (IsManifold.maximalAtlas J n N) codChart

Tactic:
assumption
-- 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
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
⊢ domChart.source ⊆ f ⁻¹' codChart.source

Tactic:
assumption
-- 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
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
⊢ 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

Tactic:
assumption
-- 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
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
⊢ IsImmersionAtOfComplement F I J n f x

Tactic:
have aux : IsImmersionAtOfComplement F I J n f x := by
    apply IsImmersionAtOfComplement.mk_of_charts <;> assumption
-- 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
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
⊢ NormedAddCommGroup aux.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
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
⊢ NormedSpace.{u_1, u} 𝕜 aux.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
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
h : IsImmersionAtOfComplement aux.smallComplement I J n f x
⊢ IsImmersionAt I J n f x

Tactic:
use aux.smallComplement, by infer_instance, by infer_instance

Premises used: Manifold.IsImmersionAtOfComplement.smallComplement