-- 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
⊢ 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
have h : 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: rw [φ₁.extend_prod φ₂, ψ₁.extend_prod, PartialEquiv.prod_target, eqOn_prod_iff]