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 g : M → N
x : M
hfg : f =ᶠ[𝓝 x] g
⊢ IsImmersionAtOfComplement F I J n f x ↔ IsImmersionAtOfComplement F I J n g x

Tactic:
LiftSourceTargetPropertyAt.congr_iff_of_eventuallyEq
      isLocalSourceTargetProperty_immersionAtProp hfg

Premises used: Manifold.IsImmersionAtOfComplement, Manifold.LiftSourceTargetPropertyAt.congr_iff_of_eventuallyEq, Manifold.isLocalSourceTargetProperty_immersionAtProp
-- 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 : IsImmersionAtOfComplement F I J n f x
⊢ Small.{u, u_5} F

Tactic:
small_of_injective <| hf.equiv.injective.comp (Prod.mk_right_injective 0)

Premises used: small_of_injective, ContinuousLinearEquiv.injective, Function.Injective.comp, Prod.mk_right_injective, Manifold.IsImmersionAtOfComplement.equiv, OfNat.ofNat
-- 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
x : M
h : IsImmersionAtOfComplement F I J n f x
e : F ≃L[𝕜] F'
⊢ IsImmersionAtOfComplement F' I J n f x

Tactic:
⟨h.domChart, h.codChart, h.mem_domChart_source, h.mem_codChart_source,
    h.domChart_mem_maximalAtlas, h.codChart_mem_maximalAtlas, h.source_subset_preimage_source, ?_⟩

Premises used: Manifold.LocalPresentationAt.mk, Manifold.IsImmersionAtOfComplement, Manifold.IsImmersionAtOfComplement.mem_domChart_source, Manifold.IsImmersionAtOfComplement.source_subset_preimage_source, Nonempty.intro, Manifold.LiftSourceTargetPropertyAt, Manifold.IsImmersionAtOfComplement.domChart_mem_maximalAtlas, Manifold.IsImmersionAtOfComplement.mem_codChart_source, Manifold.IsImmersionAtOfComplement.codChart, Manifold.IsImmersionAtOfComplement.domChart, Manifold.IsImmersionAtOfComplement.codChart_mem_maximalAtlas
-- 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
x : M
h : IsImmersionAtOfComplement F I J n f x
e : F ≃L[𝕜] F'
refine : ImmersionAtProp F' I J M N f h.domChart h.codChart
⊢ IsImmersionAtOfComplement F' I J n f x

Tactic:
refine ⟨h.domChart, h.codChart, h.mem_domChart_source, h.mem_codChart_source,
    h.domChart_mem_maximalAtlas, h.codChart_mem_maximalAtlas, 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
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
x : M
h : IsImmersionAtOfComplement F I J n f x
e : F ≃L[𝕜] F'
h₁ :
  EqOn ((↑(h.codChart.extend J) : N → E'') ∘ f ∘ (↑(h.domChart.extend I).symm : E → M))
    (comp (β := E × F')
      (⇑(ContinuousLinearEquiv.trans (ContinuousLinearEquiv.prodCongr (ContinuousLinearEquiv.refl 𝕜 E) e.symm)
            h.equiv) :
        (a : E × F') → E'')
      fun (x : E) ↦ (x, 0))
    (h.domChart.extend I).target
⊢ ImmersionAtProp F' I J M N f h.domChart h.codChart

Tactic:
use ((ContinuousLinearEquiv.refl 𝕜 E).prodCongr e.symm).trans h.equiv

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearEquiv.trans, ContinuousLinearEquiv.refl, Manifold.IsImmersionAtOfComplement.equiv, ContinuousLinearEquiv.prodCongr
-- 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
x : M
h : IsImmersionAtOfComplement F I J n f x
e : F ≃L[𝕜] F'
h₁ :
  EqOn.{u_2, u} (β := E'') (comp (β := E × F) (⇑h.equiv : (a : E × F) → E'') fun (x : E) ↦ (x, 0))
    (comp (β := E × F')
      (⇑(ContinuousLinearEquiv.trans (ContinuousLinearEquiv.prodCongr (ContinuousLinearEquiv.refl 𝕜 E) e.symm)
            h.equiv) :
        (a : E × F') → E'')
      fun (x : E) ↦ (x, 0))
    (h.domChart.extend I).target
⊢ EqOn ((↑(h.codChart.extend J) : N → E'') ∘ f ∘ (↑(h.domChart.extend I).symm : E → M))
    (comp (β := E × F')
      (⇑(ContinuousLinearEquiv.trans (ContinuousLinearEquiv.prodCongr (ContinuousLinearEquiv.refl 𝕜 E) e.symm)
            h.equiv) :
        (a : E × F') → E'')
      fun (x : E) ↦ (x, 0))
    (h.domChart.extend I).target

Tactic:
apply Set.EqOn.trans h.writtenInCharts

Premises used: Set.EqOn.trans, Manifold.IsImmersionAtOfComplement.writtenInCharts
-- 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
x_1 : M
h : IsImmersionAtOfComplement F I J n f x_1
e : F ≃L[𝕜] F'
x : E
hx : x ∈ (h.domChart.extend I).target
⊢ Eq.{u + 1} (α := E'') (comp (β := E × F) (⇑h.equiv : (a : E × F) → E'') (fun (x : E) ↦ (x, 0)) x)
    (comp (β := E × F')
      (⇑(ContinuousLinearEquiv.trans (ContinuousLinearEquiv.prodCongr (ContinuousLinearEquiv.refl 𝕜 E) e.symm)
            h.equiv) :
        (a : E × F') → E'')
      (fun (x : E) ↦ (x, 0)) x)

Tactic:
simp
-- 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
x : M
e : F ≃L[𝕜] F'
⊢ IsImmersionAtOfComplement F I J n f x ↔ IsImmersionAtOfComplement F' I J n f x

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

Premises used: ContinuousLinearEquiv.symm, Manifold.IsImmersionAtOfComplement.trans_F, Iff.intro
-- 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
⊢ IsOpen[inst_9] {x : M | IsImmersionAtOfComplement F I J n f x}

Tactic:
IsOpen.liftSourceTargetPropertyAt

Premises used: IsOpen.liftSourceTargetPropertyAt, Manifold.IsImmersionAtOfComplement, setOf
-- 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 : ℕ∞ω
x : M
f : M → N
g : M' → N'
x' : M'
inst_25 : IsManifold I n M
inst_26 : IsManifold I' n M'
inst_27 : IsManifold J n N
inst_28 : IsManifold J' n N'
hf : IsImmersionAtOfComplement F I J n f x
hg : IsImmersionAtOfComplement F' I' J' n g x'
apply :
  ∀ {f : M → N} {φ₁ : OpenPartialHomeomorph M H} {ψ₁ : OpenPartialHomeomorph N G} {g : M' → N'}
    {φ₂ : OpenPartialHomeomorph M' H'} {ψ₂ : OpenPartialHomeomorph N' G'},
    ImmersionAtProp F I J M N f φ₁ ψ₁ →
      ImmersionAtProp F' I' J' M' N' g φ₂ ψ₂ →
        ImmersionAtProp (F × F') (I.prod I') (J.prod J') (M × M') (N × N') (Prod.map f g) (φ₁.prod φ₂) (ψ₁.prod ψ₂)
⊢ IsImmersionAtOfComplement (F × F') (I.prod I') (J.prod J') n (Prod.map f g) (x, x')

Tactic:
apply LiftSourceTargetPropertyAt.prodMap hf.property hg.property

Premises used: Manifold.IsImmersionAtOfComplement.property, Manifold.LiftSourceTargetPropertyAt.prodMap
-- 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 : ℕ∞ω
x : M
f_1 : M → N
g_1 : M' → N'
x' : M'
inst_25 : IsManifold I n M
inst_26 : IsManifold I' n M'
inst_27 : IsManifold J n N
inst_28 : IsManifold J' n N'
hf : IsImmersionAtOfComplement F I J n f_1 x
hg : IsImmersionAtOfComplement F' I' J' n g_1 x'
f : M → N
φ₁ : OpenPartialHomeomorph M H
ψ₁ : OpenPartialHomeomorph N G
g : M' → N'
φ₂ : OpenPartialHomeomorph M' H'
ψ₂ : OpenPartialHomeomorph N' G'
equiv₁ : (E × F) ≃L[𝕜] E''
hfprop :
  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
equiv₂ : (E' × F') ≃L[𝕜] E'''
hgprop :
  EqOn ((↑(ψ₂.extend J') : N' → E''') ∘ g ∘ (↑(φ₂.extend I').symm : E' → M'))
    (comp (β := E' × F') (⇑equiv₂ : (a : E' × F') → E''') fun (x : E') ↦ (x, 0)) (φ₂.extend I').target
h :
  EqOn
    ((↑((ψ₁.prod ψ₂).extend (J.prod J')) : N × N' → E'' × E''') ∘
      Prod.map f g ∘ (↑((φ₁.prod φ₂).extend (I.prod I')).symm : E × E' → M × M'))
    (comp (β := (E × E') × F × F')
      (⇑(ContinuousLinearEquiv.trans (ContinuousLinearEquiv.prodProdProdComm 𝕜 E E' F F') (equiv₁.prodCongr equiv₂)) :
        (a : (E × E') × F × F') → E'' × E''')
      fun (x : E × E') ↦ (x, 0))
    ((φ₁.prod φ₂).extend (I.prod I')).target
⊢ ImmersionAtProp (F × F') (I.prod I') (J.prod J') (M × M') (N × N') (Prod.map f g) (φ₁.prod φ₂) (ψ₁.prod ψ₂)

Tactic:
use (ContinuousLinearEquiv.prodProdProdComm 𝕜 E E' F F').trans (equiv₁.prodCongr equiv₂)

Premises used: ContinuousLinearEquiv.trans, ContinuousLinearEquiv.prodProdProdComm, ContinuousLinearEquiv.prodCongr
-- 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 : ℕ∞ω
x_1 : M
f_1 : M → N
g_1 : M' → N'
x' : M'
inst_25 : IsManifold I n M
inst_26 : IsManifold I' n M'
inst_27 : IsManifold J n N
inst_28 : IsManifold J' n N'
hf : IsImmersionAtOfComplement F I J n f_1 x_1
hg : IsImmersionAtOfComplement F' I' J' n g_1 x'
f : M → N
φ₁ : OpenPartialHomeomorph M H
ψ₁ : OpenPartialHomeomorph N G
g : M' → N'
φ₂ : OpenPartialHomeomorph M' H'
ψ₂ : OpenPartialHomeomorph N' G'
equiv₁ : (E × F) ≃L[𝕜] E''
hfprop :
  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
equiv₂ : (E' × F') ≃L[𝕜] E'''
hgprop :
  EqOn ((↑(ψ₂.extend J') : N' → E''') ∘ g ∘ (↑(φ₂.extend I').symm : E' → M'))
    (comp (β := E' × F') (⇑equiv₂ : (a : E' × F') → E''') fun (x : E') ↦ (x, 0)) (φ₂.extend I').target
x : E × E'
h : x ∈ (φ₁.extend I).target ×ˢ (φ₂.extend I').target
hx : x.1 ∈ (φ₁.extend I).target
hx' : x.2 ∈ (φ₂.extend I').target
⊢ (Prod.fst ∘
        (↑((ψ₁.extend J).prod (ψ₂.extend J')) : N × N' → E'' × E''') ∘
          Prod.map f g ∘ (↑((φ₁.extend I).prod (φ₂.extend I')).symm : E × E' → M × M'))
      x =
    comp (β := E'' × E''') Prod.fst
      (comp (β := (E × E') × F × F')
        (⇑(ContinuousLinearEquiv.trans (ContinuousLinearEquiv.prodProdProdComm 𝕜 E E' F F') (equiv₁.prodCongr equiv₂)) :
          (a : (E × E') × F × F') → E'' × E''')
        fun (x : E × E') ↦ (x, 0))
      x

Tactic:
simpa using hfprop hx
-- 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 : ℕ∞ω
x_1 : M
f_1 : M → N
g_1 : M' → N'
x' : M'
inst_25 : IsManifold I n M
inst_26 : IsManifold I' n M'
inst_27 : IsManifold J n N
inst_28 : IsManifold J' n N'
hf : IsImmersionAtOfComplement F I J n f_1 x_1
hg : IsImmersionAtOfComplement F' I' J' n g_1 x'
f : M → N
φ₁ : OpenPartialHomeomorph M H
ψ₁ : OpenPartialHomeomorph N G
g : M' → N'
φ₂ : OpenPartialHomeomorph M' H'
ψ₂ : OpenPartialHomeomorph N' G'
equiv₁ : (E × F) ≃L[𝕜] E''
hfprop :
  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
equiv₂ : (E' × F') ≃L[𝕜] E'''
hgprop :
  EqOn ((↑(ψ₂.extend J') : N' → E''') ∘ g ∘ (↑(φ₂.extend I').symm : E' → M'))
    (comp (β := E' × F') (⇑equiv₂ : (a : E' × F') → E''') fun (x : E') ↦ (x, 0)) (φ₂.extend I').target
x : E × E'
h : x ∈ (φ₁.extend I).target ×ˢ (φ₂.extend I').target
hx : x.1 ∈ (φ₁.extend I).target
hx' : x.2 ∈ (φ₂.extend I').target
⊢ (Prod.snd ∘
        (↑((ψ₁.extend J).prod (ψ₂.extend J')) : N × N' → E'' × E''') ∘
          Prod.map f g ∘ (↑((φ₁.extend I).prod (φ₂.extend I')).symm : E × E' → M × M'))
      x =
    comp (β := E'' × E''') Prod.snd
      (comp (β := (E × E') × F × F')
        (⇑(ContinuousLinearEquiv.trans (ContinuousLinearEquiv.prodProdProdComm 𝕜 E E' F F') (equiv₁.prodCongr equiv₂)) :
          (a : (E × E') × F × F') → E'' × E''')
        fun (x : E × E') ↦ (x, 0))
      x

Tactic:
simpa using hgprop hx'
-- 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 : ℕ∞ω
x : M
f_1 : M → N
g_1 : M' → N'
x' : M'
inst_25 : IsManifold I n M
inst_26 : IsManifold I' n M'
inst_27 : IsManifold J n N
inst_28 : IsManifold J' n N'
hf : IsImmersionAtOfComplement F I J n f_1 x
hg : IsImmersionAtOfComplement F' I' J' n g_1 x'
f : M → N
φ₁ : OpenPartialHomeomorph M H
ψ₁ : OpenPartialHomeomorph N G
g : M' → N'
φ₂ : OpenPartialHomeomorph M' H'
ψ₂ : OpenPartialHomeomorph N' G'
equiv₁ : (E × F) ≃L[𝕜] E''
hfprop :
  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
equiv₂ : (E' × F') ≃L[𝕜] E'''
hgprop :
  EqOn ((↑(ψ₂.extend J') : N' → E''') ∘ g ∘ (↑(φ₂.extend I').symm : E' → M'))
    (comp (β := E' × F') (⇑equiv₂ : (a : E' × F') → E''') fun (x : E') ↦ (x, 0)) (φ₂.extend I').target
⊢ EqOn
      (Prod.fst ∘
        (↑((ψ₁.extend J).prod (ψ₂.extend J')) : N × N' → E'' × E''') ∘
          Prod.map f g ∘ (↑((φ₁.extend I).prod (φ₂.extend I')).symm : E × E' → M × M'))
      (comp (β := E'' × E''') Prod.fst
        (comp (β := (E × E') × F × F')
          (⇑(ContinuousLinearEquiv.trans (ContinuousLinearEquiv.prodProdProdComm 𝕜 E E' F F')
                (equiv₁.prodCongr equiv₂)) :
            (a : (E × E') × F × F') → E'' × E''')
          fun (x : E × E') ↦ (x, 0)))
      ((φ₁.extend I).target ×ˢ (φ₂.extend I').target) ∧
    EqOn
      (Prod.snd ∘
        (↑((ψ₁.extend J).prod (ψ₂.extend J')) : N × N' → E'' × E''') ∘
          Prod.map f g ∘ (↑((φ₁.extend I).prod (φ₂.extend I')).symm : E × E' → M × M'))
      (comp (β := E'' × E''') Prod.snd
        (comp (β := (E × E') × F × F')
          (⇑(ContinuousLinearEquiv.trans (ContinuousLinearEquiv.prodProdProdComm 𝕜 E E' F F')
                (equiv₁.prodCongr equiv₂)) :
            (a : (E × E') × F × F') → E'' × E''')
          fun (x : E × E') ↦ (x, 0)))
      ((φ₁.extend I).target ×ˢ (φ₂.extend I').target)

Tactic:
exact ⟨fun x ⟨hx, hx'⟩ ↦ by simpa using hfprop hx, fun x ⟨hx, hx'⟩ ↦ by simpa using hgprop hx'⟩
-- 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
⊢ NormedAddCommGroup h.smallComplement

Tactic:
infer_instance