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
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
⊢ LiftSourceTargetPropertyAt I J n f x (ImmersionAtProp h.complement I J M N)

Tactic:
h.isImmersionAtOfComplement_complement.property

Premises used: Manifold.IsImmersionAt.isImmersionAtOfComplement_complement, Manifold.IsImmersionAtOfComplement.property
-- 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
⊢ (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 ⊆
    (h.codChart.extend J).target

Tactic:
h.isImmersionAtOfComplement_complement.map_target_subset_target

Premises used: Manifold.IsImmersionAt.domChart, Manifold.IsImmersionAtOfComplement.map_target_subset_target, Manifold.IsImmersionAt.isImmersionAtOfComplement_complement, Manifold.IsImmersionAt.codChart
-- 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.extend I).target ⊆
    (comp (β := Prod.{u_2, u} E h.complement) (⇑h.equiv : (a : E × h.complement) → E'') fun (x_1 : E) ↦ (x_1, 0)) ⁻¹'
      (h.codChart.extend J).target

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

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

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

Premises used: Manifold.IsImmersionAt.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
x : M
hf : IsImmersionAt I J n f x
hfg : f =ᶠ[𝓝 x] g
⊢ IsImmersionAtOfComplement hf.complement I J n g x

Tactic:
hf.isImmersionAtOfComplement_complement.congr_of_eventuallyEq hfg

Premises used: Manifold.IsImmersionAt.isImmersionAtOfComplement_complement, Manifold.IsImmersionAtOfComplement.congr_of_eventuallyEq
-- 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
x : M
hf : IsImmersionAt I J n f x
hfg : f =ᶠ[𝓝 x] g
⊢ IsImmersionAtOfComplement hf.complement I J n g x

Tactic:
exact hf.isImmersionAtOfComplement_complement.congr_of_eventuallyEq hfg

Premises used: Manifold.IsImmersionAt.isImmersionAtOfComplement_complement, Manifold.IsImmersionAtOfComplement.congr_of_eventuallyEq
-- 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
x : M
hfg : f =ᶠ[𝓝 x] g
⊢ IsImmersionAt I J n f x ↔ IsImmersionAt I J n g x

Tactic:
⟨fun h ↦ h.congr_of_eventuallyEq hfg, fun h ↦ h.congr_of_eventuallyEq hfg.symm⟩

Premises used: Iff.intro, Manifold.IsImmersionAt.congr_of_eventuallyEq, Filter.EventuallyEq.symm
-- 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
rw :
  ∀ (x : M),
    Membership.mem (γ := Set M) {x : M | IsImmersionAt I J n f x} x →
      ∃ t ⊆ {x : M | IsImmersionAt I J n f x}, IsOpen[inst_7] t ∧ x ∈ t
⊢ IsOpen[inst_7] {x : M | IsImmersionAt I J n f x}

Tactic:
rw [isOpen_iff_forall_mem_open]

Premises used: isOpen_iff_forall_mem_open
-- 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
hx : Membership.mem (γ := Set M) {x : M | IsImmersionAt I J n f x} x
⊢ Membership.mem (γ := Set M) {x_1 : M | IsImmersionAtOfComplement (complement hx) I J n f x_1} x

Tactic:
simp [hx.isImmersionAtOfComplement_complement]

Premises used: 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),
    Membership.mem (γ := Set M) {x : M | IsImmersionAt I J n f x} x →
      ∃ t ⊆ {x : M | IsImmersionAt I J n f x}, IsOpen[inst_7] t ∧ x ∈ t

Tactic:
exact fun x hx ↦ ⟨{x | IsImmersionAtOfComplement hx.complement I J n f x },
    fun y hy ↦ hy.isImmersionAt, .isImmersionAtOfComplement,
    by simp [hx.isImmersionAtOfComplement_complement]⟩
-- 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 : ℕ∞ω
x : M
f : M → N
g : M' → N'
x' : M'
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 : IsImmersionAt I J n f x
hg : IsImmersionAt I' J' n g x'
⊢ IsImmersionAt (I.prod I') (J.prod J') n (Prod.map f g) (x, x')

Tactic:
hf.isImmersionAtOfComplement_complement.prodMap hg.isImmersionAtOfComplement_complement
    |>.isImmersionAt

Premises used: Manifold.IsImmersionAtOfComplement.prodMap, Manifold.IsImmersionAtOfComplement.isImmersionAt, Manifold.IsImmersionAt.isImmersionAtOfComplement_complement
-- 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 : ℕ∞ω
x : M
inst_6 : IsManifold I n M
s : TopologicalSpace.Opens M
hx : x ∈ s
⊢ 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 : ℕ∞ω
x : M
inst_6 : IsManifold I n M
s : TopologicalSpace.Opens M
hx : x ∈ s
⊢ 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 : ℕ∞ω
x : M
inst_6 : IsManifold I n M
s : TopologicalSpace.Opens M
hx : x ∈ s
h :
  IsImmersionAtOfComplement PUnit.{u_2 + 1} I I n (Subtype.val (p := fun (x : M) ↦ x ∈ s))
    (Subtype.mk (p := fun (x : M) ↦ x ∈ s) x hx)
⊢ IsImmersionAt I I n (Subtype.val (p := fun (x : M) ↦ x ∈ s)) (Subtype.mk (p := fun (x : M) ↦ x ∈ s) x hx)

Tactic:
use PUnit, by infer_instance, by infer_instance

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 : ℕ∞ω
x : M
inst_6 : IsManifold I n M
s : TopologicalSpace.Opens M
hx : x ∈ s
⊢ IsImmersionAtOfComplement PUnit.{u_2 + 1} I I n (Subtype.val (p := fun (x : M) ↦ x ∈ s))
    (Subtype.mk (p := fun (x : M) ↦ x ∈ s) x hx)

Tactic:
apply Manifold.IsImmersionAtOfComplement.of_opens

Premises used: Manifold.IsImmersionAtOfComplement.of_opens
-- 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
x : M
⊢ IsImmersionAtOfComplement F I J n f x

Tactic:
h x
-- 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
h : IsImmersionOfComplement F I J n f
heq : f = g
⊢ IsImmersionOfComplement F 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
F : Type u_5
F' : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup E''
inst_4 : NormedSpace 𝕜 E''
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜 F'
H : Type u_7
inst_9 : TopologicalSpace H
G : Type u_9
inst_10 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
N : Type u_13
inst_13 : TopologicalSpace N
inst_14 : ChartedSpace G N
n : ℕ∞ω
f : M → N
h : IsImmersionOfComplement F I J n f
e : F ≃L[𝕜] F'
⊢ IsImmersionOfComplement F' I J n f

Tactic:
fun x ↦ (h x).trans_F e

Premises used: Manifold.IsImmersionAtOfComplement.trans_F, Manifold.IsImmersionOfComplement
-- Module: Mathlib.Geometry.Manifold.Immersion
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
F : Type u_5
F' : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup E''
inst_4 : NormedSpace 𝕜 E''
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜 F'
H : Type u_7
inst_9 : TopologicalSpace H
G : Type u_9
inst_10 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
N : Type u_13
inst_13 : TopologicalSpace N
inst_14 : ChartedSpace G N
n : ℕ∞ω
f : M → N
e : F ≃L[𝕜] F'
⊢ IsImmersionOfComplement F I J n f ↔ IsImmersionOfComplement F' I J n f

Tactic:
⟨fun h ↦ trans_F (e := e) h, fun h ↦ trans_F (e := e.symm) h⟩

Premises used: ContinuousLinearEquiv.symm, Manifold.IsImmersionOfComplement.trans_F, Iff.intro
-- 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
F : Type u_5
F' : Type u_6
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'''
inst_9 : NormedAddCommGroup F
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedAddCommGroup F'
inst_12 : NormedSpace 𝕜 F'
H : Type u_7
inst_13 : TopologicalSpace H
H' : Type u_8
inst_14 : TopologicalSpace H'
G : Type u_9
inst_15 : TopologicalSpace G
G' : Type u_10
inst_16 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
inst_17 : TopologicalSpace M
inst_18 : ChartedSpace H M
M' : Type u_12
inst_19 : TopologicalSpace M'
inst_20 : ChartedSpace H' M'
N : Type u_13
inst_21 : TopologicalSpace N
inst_22 : ChartedSpace G N
N' : Type u_14
inst_23 : TopologicalSpace N'
inst_24 : ChartedSpace G' N'
n : ℕ∞ω
f : M → N
g : M' → N'
inst_25 : IsManifold I n M
inst_26 : IsManifold I' n M'
inst_27 : IsManifold J n N
inst_28 : IsManifold J' n N'
h : IsImmersionOfComplement F I J n f
h' : IsImmersionOfComplement F' I' J' n g
⊢ IsImmersionOfComplement (F × F') (I.prod I') (J.prod J') n (Prod.map f g)

Tactic:
fun ⟨x, x'⟩ ↦ (h x).prodMap (h' x')

Premises used: Manifold.IsImmersionAtOfComplement.prodMap, Manifold.IsImmersionAtOfComplement, Prod.map, _private.0.Manifold.IsImmersionOfComplement.prodMap.match_1, Manifold.IsImmersionOfComplement, Prod, ModelWithCorners.prod
-- 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
pos : ∀ (hM : IsEmpty M), IsImmersion I J n f
neg : ∀ (hM : Nonempty M), IsImmersion I J n f
⊢ IsImmersion I J n f

Tactic:
by_cases! hM : IsEmpty M

Premises used: IsEmpty
-- 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 : IsEmpty M
⊢ NormedAddCommGroup PUnit.{u + 1}

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 : IsEmpty M
⊢ NormedSpace 𝕜 PUnit.{u + 1}

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 : IsEmpty M
h₁ : IsImmersionOfComplement PUnit.{u + 1} I J n f
⊢ ∃ (F : Type u) (x : NormedAddCommGroup F) (x_1 : NormedSpace 𝕜 F), IsImmersionOfComplement F I J n f

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
E'' : Type u
F : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup E''
inst_4 : NormedSpace 𝕜 E''
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_7
inst_7 : TopologicalSpace H
G : Type u_9
inst_8 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace H M
N : Type u_13
inst_11 : TopologicalSpace N
inst_12 : ChartedSpace G N
n : ℕ∞ω
f : M → N
h : IsImmersionOfComplement F I J n f
hM : IsEmpty M
⊢ IsImmersionOfComplement PUnit.{u + 1} I J n f

Tactic:
fun x ↦ (IsEmpty.false x).elim

Premises used: False.elim, IsEmpty.false, Manifold.IsImmersionOfComplement
-- 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 : IsEmpty M
⊢ IsImmersionOfComplement PUnit.{u + 1} I J n f

Tactic:
exact fun x ↦ (IsEmpty.false x).elim

Premises used: False.elim, IsEmpty.false
-- 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
neg : ∀ (inhabited_h : Inhabited M), IsImmersion I J n f
⊢ IsImmersion I J n f

Tactic:
inhabit M