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
N : Type u_13
inst_10 : TopologicalSpace N
f : M → N
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
s : Set M
hs : IsOpen[inst_9] s
h : ImmersionAtProp F I J M N f φ ψ
equiv : (E × F) ≃L[𝕜] E''
hf :
  EqOn ((↑(ψ.extend J) : N → E'') ∘ f ∘ (↑(φ.extend I).symm : E → M))
    (comp (β := E × F) (⇑equiv : (a : E × F) → E'') fun (x : E) ↦ (x, 0)) (φ.extend I).target
simp :
  range (↑I : H → E) ∩ ((↑I.symm : E → H) ⁻¹' φ.target ∩ (↑I.symm : E → H) ⁻¹' (↑φ.symm : H → M) ⁻¹' interior s) ⊆
    (↑I.symm : E → H) ⁻¹' φ.target
⊢ ((φ.restr s).extend I).target ⊆ (φ.extend I).target

Tactic:
simp
-- 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
N : Type u_13
inst_10 : TopologicalSpace N
f : M → N
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
s : Set M
hs : IsOpen[inst_9] s
h : ImmersionAtProp F I J M N f φ ψ
equiv : (E × F) ≃L[𝕜] E''
hf :
  EqOn ((↑(ψ.extend J) : N → E'') ∘ f ∘ (↑(φ.extend I).symm : E → M))
    (comp (β := E × F) (⇑equiv : (a : E × F) → E'') fun (x : E) ↦ (x, 0)) (φ.extend I).target
⊢ range (↑I : H → E) ∩ ((↑I.symm : E → H) ⁻¹' φ.target ∩ (↑I.symm : E → H) ⁻¹' (↑φ.symm : H → M) ⁻¹' interior s) ⊆
    (↑I.symm : E → H) ⁻¹' φ.target

Tactic:
grind
-- 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
N : Type u_13
inst_10 : TopologicalSpace N
f g : M → N
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
hfg : EqOn f g φ.source
equiv : (E × F) ≃L[𝕜] E''
hf :
  EqOn ((↑(ψ.extend J) : N → E'') ∘ f ∘ (↑(φ.extend I).symm : E → M))
    (comp (β := E × F) (⇑equiv : (a : E × F) → E'') fun (x : E) ↦ (x, 0)) (φ.extend I).target
⊢ (φ.extend I).target ⊆ (φ.extend I).target

Tactic:
simp
-- 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
N : Type u_13
inst_10 : TopologicalSpace N
f g : M → N
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
hfg : EqOn f g φ.source
equiv : (E × F) ≃L[𝕜] E''
hf :
  EqOn ((↑(ψ.extend J) : N → E'') ∘ f ∘ (↑(φ.extend I).symm : E → M))
    (comp (β := E × F) (⇑equiv : (a : E × F) → E'') fun (x : E) ↦ (x, 0)) (φ.extend I).target
refine :
  ∀ (x : E) (hx : x ∈ (φ.extend I).target),
    ((↑(ψ.extend J) : N → E'') ∘ g ∘ (↑(φ.extend I).symm : E → M)) x =
      ((↑(ψ.extend J) : N → E'') ∘ f ∘ (↑(φ.extend I).symm : E → M)) x
⊢ ImmersionAtProp F I J M N g φ ψ

Tactic:
refine ⟨equiv, EqOn.trans (fun x hx ↦ ?_) (hf.mono (by simp))⟩
-- 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
N : Type u_13
inst_10 : TopologicalSpace N
f g : M → N
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
hfg : EqOn f g φ.source
equiv : (E × F) ≃L[𝕜] E''
hf :
  EqOn ((↑(ψ.extend J) : N → E'') ∘ f ∘ (↑(φ.extend I).symm : E → M))
    (comp (β := E × F) (⇑equiv : (a : E × F) → E'') fun (x : E) ↦ (x, 0)) (φ.extend I).target
x : E
hx : x ∈ (φ.extend I).target
⊢ (↑(φ.extend I).symm : E → M) x ∈ φ.source

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
N : Type u_13
inst_10 : TopologicalSpace N
f g : M → N
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
hfg : EqOn f g φ.source
equiv : (E × F) ≃L[𝕜] E''
hf :
  EqOn ((↑(ψ.extend J) : N → E'') ∘ f ∘ (↑(φ.extend I).symm : E → M))
    (comp (β := E × F) (⇑equiv : (a : E × F) → E'') fun (x : E) ↦ (x, 0)) (φ.extend I).target
x : E
hx : x ∈ (φ.extend I).target
⊢ (↑(φ.extend I).symm : E → M) x ∈ φ.source

Tactic:
have : ((φ.extend I).symm) x ∈ φ.source := by 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
N : Type u_13
inst_10 : TopologicalSpace N
f g : M → N
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
hfg : EqOn f g φ.source
equiv : (E × F) ≃L[𝕜] E''
hf :
  EqOn ((↑(ψ.extend J) : N → E'') ∘ f ∘ (↑(φ.extend I).symm : E → M))
    (comp (β := E × F) (⇑equiv : (a : E × F) → E'') fun (x : E) ↦ (x, 0)) (φ.extend I).target
x : E
hx : x ∈ (φ.extend I).target
this : (↑(φ.extend I).symm : E → M) x ∈ φ.source
⊢ ((↑(ψ.extend J) : N → E'') ∘ g ∘ (↑(φ.extend I).symm : E → M)) x =
    ((↑(ψ.extend J) : N → E'') ∘ f ∘ (↑(φ.extend I).symm : E → M)) x

Tactic:
grind
-- 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
property : ImmersionAtProp F I J M N f domChart codChart
⊢ IsImmersionAtOfComplement F I J n f x

Tactic:
use domChart, codChart
-- 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
w : (E × F) ≃L[𝕜] E''
h :
  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
⊢ ImmersionAtProp F I J M N f domChart codChart

Tactic:
use equiv
-- 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:
LiftSourceTargetPropertyAt.mk_of_continuousAt hf isLocalSourceTargetProperty_immersionAtProp
    _ _ hx hfx hdomChart hcodChart ⟨equiv, hwrittenInExtend⟩

Premises used: Manifold.IsImmersionAtOfComplement, Manifold.isLocalSourceTargetProperty_immersionAtProp, Exists.intro, Manifold.LiftSourceTargetPropertyAt.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
h : IsImmersionAtOfComplement F I J n f x
⊢ x ∈ h.domChart.source

Tactic:
LiftSourceTargetPropertyAt.mem_domChart_source h

Premises used: Manifold.LiftSourceTargetPropertyAt.mem_domChart_source, Set.Mem
-- 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
⊢ f x ∈ h.codChart.source

Tactic:
LiftSourceTargetPropertyAt.mem_codChart_source h

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

Tactic:
LiftSourceTargetPropertyAt.domChart_mem_maximalAtlas h

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

Tactic:
LiftSourceTargetPropertyAt.codChart_mem_maximalAtlas h

Premises used: Set.Mem, Manifold.LiftSourceTargetPropertyAt.codChart_mem_maximalAtlas, Manifold.IsImmersionAtOfComplement.codChart
-- 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.domChart.source ⊆ f ⁻¹' h.codChart.source

Tactic:
LiftSourceTargetPropertyAt.source_subset_preimage_source h

Premises used: Manifold.LiftSourceTargetPropertyAt.source_subset_preimage_source
-- 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
⊢ EqOn ((↑(h.codChart.extend J) : N → E'') ∘ f ∘ (↑(h.domChart.extend I).symm : E → M))
    (comp (β := E × F) (⇑h.equiv : (a : E × F) → E'') fun (x : E) ↦ (x, 0)) (h.domChart.extend I).target

Tactic:
Classical.choose_spec <| LiftSourceTargetPropertyAt.property h

Premises used: Classical.choose_spec, Manifold.LiftSourceTargetPropertyAt.property, Manifold.IsImmersionAtOfComplement.domChart
-- 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
⊢ LiftSourceTargetPropertyAt I J n f x (ImmersionAtProp F I J M N)

Tactic:
h

Premises used: Manifold.IsImmersionAtOfComplement
-- 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
rw :
  (↑(h.codChart.extend J) : N → E'') '' f '' h.domChart.source ⊆
    (↑(h.codChart.extend J) : N → E'') '' (h.codChart.extend J).source
⊢ (comp (β := E × F) (⇑h.equiv : (a : E × F) → E'') fun (x : E) ↦ (x, 0)) '' (h.domChart.extend I).target ⊆
    (h.codChart.extend J).target

Tactic:
rw [← h.writtenInCharts.image_eq, Set.image_comp, Set.image_comp,
    PartialEquiv.symm_image_target_eq_source, OpenPartialHomeomorph.extend_source,
    ← PartialEquiv.image_source_eq_target]

Premises used: PartialEquiv.symm_image_target_eq_source, PartialEquiv.image_source_eq_target, Set.EqOn.image_eq, OpenPartialHomeomorph.extend_source, Manifold.IsImmersionAtOfComplement.writtenInCharts, Set.image_comp
-- 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
⊢ f '' h.domChart.source ⊆ h.codChart.source

Tactic:
simp [h.source_subset_preimage_source]

Premises used: Manifold.IsImmersionAtOfComplement.source_subset_preimage_source
-- 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
⊢ f '' h.domChart.source ⊆ h.codChart.source

Tactic:
have : f '' h.domChart.source ⊆ h.codChart.source := by
    simp [h.source_subset_preimage_source]
-- 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
this : f '' h.domChart.source ⊆ h.codChart.source
grw :
  (↑(h.codChart.extend J) : N → E'') '' h.codChart.source ⊆
    (↑(h.codChart.extend J) : N → E'') '' (h.codChart.extend J).source
grw₁ grw₂ :
  (↑(h.codChart.extend J) : N → E'') '' h.codChart.source ⊆ (↑(h.codChart.extend J) : N → E'') '' h.codChart.source
⊢ (↑(h.codChart.extend J) : N → E'') '' f '' h.domChart.source ⊆
    (↑(h.codChart.extend J) : N → E'') '' (h.codChart.extend J).source

Tactic:
grw [this, OpenPartialHomeomorph.extend_source]

Premises used: OpenPartialHomeomorph.extend_source
-- 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.domChart.extend I).target ⊆
    (comp (β := E × F) (⇑h.equiv : (a : E × F) → E'') fun (x : E) ↦ (x, 0)) ⁻¹' (h.codChart.extend J).target

Tactic:
fun _x hx ↦ h.map_target_subset_target (mem_image_of_mem _ hx)

Premises used: Set.Mem, Manifold.IsImmersionAtOfComplement.map_target_subset_target, setOf, Function.comp, Prod.mk, Set.inter, Set.Subset, Set.preimage, Set.mem_image_of_mem, Manifold.IsImmersionAtOfComplement.equiv, OfNat.ofNat, DFunLike.coe
-- 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 g : M → N
x : M
hf : IsImmersionAtOfComplement F I J n f x
hfg : f =ᶠ[𝓝 x] g
⊢ IsImmersionAtOfComplement F I J n g x

Tactic:
LiftSourceTargetPropertyAt.congr_of_eventuallyEq
    isLocalSourceTargetProperty_immersionAtProp hf.property hfg

Premises used: Manifold.IsImmersionAtOfComplement, Manifold.isLocalSourceTargetProperty_immersionAtProp, Manifold.LiftSourceTargetPropertyAt.congr_of_eventuallyEq, Manifold.IsImmersionAtOfComplement.property