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
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 h h₁ h₂ h₃ : IsImmersionAtOfComplement F I J n f x
⊢ IsImmersionAtOfComplement aux.smallComplement I J n f x

Tactic:
rwa [← IsImmersionAtOfComplement.congr_F aux.smallEquiv]

Premises used: Manifold.IsImmersionAtOfComplement.congr_F, Manifold.IsImmersionAtOfComplement.smallEquiv
-- 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
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
hf₁ : ContinuousAt f x
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
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_continuousAt

Premises used: Manifold.IsImmersionAtOfComplement.mk_of_continuousAt
-- 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
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
⊢ ContinuousAt f x

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

Tactic:
have aux : IsImmersionAtOfComplement F I J n f x := by
    apply IsImmersionAtOfComplement.mk_of_continuousAt <;> 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
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
⊢ 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
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
⊢ 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
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
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
-- 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
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 h h₁ h₂ h₃ : IsImmersionAtOfComplement F I J n f x
⊢ IsImmersionAtOfComplement aux.smallComplement I J n f x

Tactic:
rwa [← IsImmersionAtOfComplement.congr_F aux.smallEquiv]

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

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

Premises used: Manifold.IsImmersionAt.complement, Classical.choose_spec
-- 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
x : M
h : IsImmersionAt I J n f x
⊢ x ∈ h.domChart.source

Tactic:
h.isImmersionAtOfComplement_complement.mem_domChart_source

Premises used: Set.Mem, Manifold.IsImmersionAtOfComplement.mem_domChart_source, Manifold.IsImmersionAt.isImmersionAtOfComplement_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
x : M
h : IsImmersionAt I J n f x
⊢ f x ∈ h.codChart.source

Tactic:
h.isImmersionAtOfComplement_complement.mem_codChart_source

Premises used: Set.Mem, Manifold.IsImmersionAt.isImmersionAtOfComplement_complement, Manifold.IsImmersionAtOfComplement.mem_codChart_source
-- 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
x : M
h : IsImmersionAt I J n f x
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (IsManifold.maximalAtlas I n M) h.domChart

Tactic:
h.isImmersionAtOfComplement_complement.domChart_mem_maximalAtlas

Premises used: Manifold.IsImmersionAt.domChart, Set.Mem, Manifold.IsImmersionAtOfComplement.domChart_mem_maximalAtlas, Manifold.IsImmersionAt.isImmersionAtOfComplement_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
x : M
h : IsImmersionAt I J n f x
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (IsManifold.maximalAtlas J n N) h.codChart

Tactic:
h.isImmersionAtOfComplement_complement.codChart_mem_maximalAtlas

Premises used: Set.Mem, Manifold.IsImmersionAt.isImmersionAtOfComplement_complement, Manifold.IsImmersionAt.codChart, Manifold.IsImmersionAtOfComplement.codChart_mem_maximalAtlas
-- 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
x : M
h : IsImmersionAt I J n f x
⊢ h.domChart.source ⊆ f ⁻¹' h.codChart.source

Tactic:
h.isImmersionAtOfComplement_complement.source_subset_preimage_source

Premises used: Manifold.IsImmersionAtOfComplement.source_subset_preimage_source, Manifold.IsImmersionAt.isImmersionAtOfComplement_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
x : M
h : IsImmersionAt I J n f x
⊢ EqOn ((↑(h.codChart.extend J) : N → E'') ∘ f ∘ (↑(h.domChart.extend I).symm : E → M))
    (comp (β := Prod.{u_2, u} E h.complement) (⇑h.equiv : (a : E × h.complement) → E'') fun (x_1 : E) ↦ (x_1, 0))
    (h.domChart.extend I).target

Tactic:
h.isImmersionAtOfComplement_complement.writtenInCharts

Premises used: Manifold.IsImmersionAt.domChart, Manifold.IsImmersionAt.isImmersionAtOfComplement_complement, Manifold.IsImmersionAtOfComplement.writtenInCharts