awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (hypothesis)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
hs : Nonempty.{u_2 + 1} (↑e.source : Type u_2)
inst_3 : HasGroupoid M G
inst_4 : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc'_1 : Membership.mem (γ := Set (OpenPartialHomeomorph (↥t) H)) (atlas H ↥t) c'
this : Nonempty.{u + 1} ↥t
x : ↥t
hc' : c' = subtypeRestr (chartAt H (↑x : H)) this
goal : OpenPartialHomeomorph.{u_2, u} (↑e.source : Type u_2) H :=
  e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ t.openPartialHomeomorphSubtypeCoe this
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (maximalAtlas (↥s) G)
    (e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ t.openPartialHomeomorphSubtypeCoe this)
have this₁ : goal ≈ e.subtypeRestr hs
Tactic: have : goal ≈ e.subtypeRestr (s := s) hs :=
    (goal.eqOnSource_iff (e.subtypeRestr (s := s) hs)).mpr
      ⟨by
        simp only [trans_toPartialEquiv, PartialEquiv.trans_source,
          Homeomorph.toOpenPartialHomeomorph_source, toFun_eq_coe,
          Homeomorph.toOpenPartialHomeomorph_apply, Opens.openPartialHomeomorphSubtypeCoe_source,
          preimage_univ, inter_self, subtypeRestr_source, goal, s]
        exact Subtype.coe_preimage_self _ |>.symm, by intro _ _; rfl⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
inst_7 : HasGroupoid M G
inst_8 : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
⊢ Structomorph.{u, u_2, u} G ↥s ↥t
have pos : (h : Nonempty.{u_2 + 1} (↑e.source : Type u_2)) → Structomorph.{u, u_2, u} G ↥s ↥t
Tactic: by_cases! h : Nonempty e.source
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
inst_7 : HasGroupoid M G
inst_8 : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
pos : (h : Nonempty.{u_2 + 1} (↑e.source : Type u_2)) → Structomorph.{u, u_2, u} G ↥s ↥t
⊢ Structomorph.{u, u_2, u} G ↥s ↥t
have neg : (h : IsEmpty.{u_2 + 1} (↑e.source : Type u_2)) → Structomorph.{u, u_2, u} G ↥s ↥t
Tactic: by_cases! h : Nonempty e.source
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (hypothesis)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
inst_7 : HasGroupoid M G
inst_8 : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
h : IsEmpty.{u_2 + 1} (↑e.source : Type u_2)
⊢ Structomorph.{u, u_2, u} G ↥s ↥t
have this : IsEmpty.{u + 1} ↥t
Tactic: have : IsEmpty t := isEmpty_coe_sort.mpr
      (by convert! e.image_source_eq_target ▸ image_eq_empty.mpr (isEmpty_coe_sort.mp h))
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
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
⊢ ((φ.restr s).extend I).target ⊆ (φ.extend I).target
have simp : range (↑I : H → E) ∩ ((↑I.symm : E → H) ⁻¹' φ.target ∩ (↑I.symm : E → H) ⁻¹' (↑φ.symm : H → M) ⁻¹' interior s) ⊆
  (↑I.symm : E → H) ⁻¹' φ.target
Tactic: simp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
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
⊢ ImmersionAtProp F I J M N g φ ψ
have 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
Tactic: refine ⟨equiv, EqOn.trans (fun x hx ↦ ?_) (hf.mono (by simp))⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (hypothesis)
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 J) : N → E'') ∘ g ∘ (↑(φ.extend I).symm : E → M)) x =
    ((↑(ψ.extend J) : N → E'') ∘ f ∘ (↑(φ.extend I).symm : E → M)) x
have this : (↑(φ.extend I).symm : E → M) x ∈ φ.source
Tactic: have : ((φ.extend I).symm) x ∈ φ.source := by simp_all
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
F : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup E''
inst_4 : NormedSpace 𝕜 E''
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_7
inst_7 : TopologicalSpace H
G : Type u_9
inst_8 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace H M
N : Type u_13
inst_11 : TopologicalSpace N
inst_12 : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
equiv : (E × F) ≃L[𝕜] E''
domChart : OpenPartialHomeomorph M H
codChart : OpenPartialHomeomorph N G
hx : x ∈ domChart.source
hfx : f x ∈ codChart.source
hdomChart : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (IsManifold.maximalAtlas I n M) domChart
hcodChart : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (IsManifold.maximalAtlas J n N) codChart
hsource : domChart.source ⊆ f ⁻¹' codChart.source
hwrittenInExtend :
  EqOn ((↑(codChart.extend J) : N → E'') ∘ f ∘ (↑(domChart.extend I).symm : E → M))
    (comp (β := E × F) (⇑equiv : (a : E × F) → E'') fun (x : E) ↦ (x, 0)) (domChart.extend I).target
⊢ IsImmersionAtOfComplement F I J n f x
have property : ImmersionAtProp F I J M N f domChart codChart
Tactic: use domChart, codChart
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
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
⊢ (comp (β := E × F) (⇑h.equiv : (a : E × F) → E'') fun (x : E) ↦ (x, 0)) '' (h.domChart.extend I).target ⊆
    (h.codChart.extend J).target
have rw : (↑(h.codChart.extend J) : N → E'') '' f '' h.domChart.source ⊆
  (↑(h.codChart.extend J) : N → E'') '' (h.codChart.extend J).source
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (hypothesis)
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.codChart.extend J) : N → E'') '' f '' h.domChart.source ⊆
    (↑(h.codChart.extend J) : N → E'') '' (h.codChart.extend J).source
have this : f '' h.domChart.source ⊆ h.codChart.source
Tactic: have : f '' h.domChart.source ⊆ h.codChart.source := by
    simp [h.source_subset_preimage_source]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
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
⊢ (↑(h.codChart.extend J) : N → E'') '' f '' h.domChart.source ⊆
    (↑(h.codChart.extend J) : N → E'') '' (h.codChart.extend J).source
have grw : (↑(h.codChart.extend J) : N → E'') '' h.codChart.source ⊆
  (↑(h.codChart.extend J) : N → E'') '' (h.codChart.extend J).source
Tactic: grw [this, OpenPartialHomeomorph.extend_source]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
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
⊢ (↑(h.codChart.extend J) : N → E'') '' f '' h.domChart.source ⊆
    (↑(h.codChart.extend J) : N → E'') '' (h.codChart.extend J).source
have grw₁ : (↑(h.codChart.extend J) : N → E'') '' h.codChart.source ⊆ (↑(h.codChart.extend J) : N → E'') '' h.codChart.source
Tactic: grw [this, OpenPartialHomeomorph.extend_source]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
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
have refine : ImmersionAtProp F' I J M N f h.domChart h.codChart
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, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
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'
⊢ ImmersionAtProp F' I J M N f h.domChart h.codChart
have 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
Tactic: use ((ContinuousLinearEquiv.refl 𝕜 E).prodCongr e.symm).trans h.equiv
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
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'
⊢ 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
have 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
Tactic: apply Set.EqOn.trans h.writtenInCharts
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
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'
⊢ IsImmersionAtOfComplement (F × F') (I.prod I') (J.prod J') n (Prod.map f g) (x, x')
have 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 ψ₂)
Tactic: apply LiftSourceTargetPropertyAt.prodMap hf.property hg.property
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
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
⊢ ImmersionAtProp (F × F') (I.prod I') (J.prod J') (M × M') (N × N') (Prod.map f g) (φ₁.prod φ₂) (ψ₁.prod ψ₂)
have 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
Tactic: use (ContinuousLinearEquiv.prodProdProdComm 𝕜 E E' F F').trans (equiv₁.prodCongr equiv₂)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
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
⊢ IsImmersionAt I J n f x
have h₁ : IsImmersionAtOfComplement h.smallComplement I J n f x
Tactic: use h.smallComplement, by infer_instance, by infer_instance
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Immersion (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_7
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
inst_6 : IsManifold I n M
s : TopologicalSpace.Opens M
y : ↥s
⊢ IsImmersionAtOfComplement PUnit.{u_15 + 1} I I n (Subtype.val (p := fun (x : M) ↦ x ∈ s)) y
have apply : EqOn
  ((↑(OpenPartialHomeomorph.extend (chartAt H (↑y : M)) I) : M → E) ∘
    Subtype.val (p := fun (x : M) ↦ x ∈ s) ∘ (↑(OpenPartialHomeomorph.extend (chartAt H y) I).symm : E → ↥s))
  (comp (β := E × PUnit.{u_15 + 1})
    (⇑(ContinuousLinearEquiv.prodUnique 𝕜 E PUnit.{u_15 + 1}) : (a : E × PUnit.{u_15 + 1}) → E) fun (x : E) ↦ (x, 0))
  (OpenPartialHomeomorph.extend (chartAt H y) I).target
Tactic: apply IsImmersionAtOfComplement.mk_of_continuousAt (by fun_prop) (.prodUnique 𝕜 E _)
    (chartAt H y) (chartAt H y.val) (mem_chart_source H y) (mem_chart_source H y.val)
    (chart_mem_maximalAtlas y) (chart_mem_maximalAtlas y.val)