Module: Mathlib.Geometry.Manifold.Immersion

Goal state before:
pp: case h
𝕜 : 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✝²⁷ : NormedAddCommGroup E
inst✝²⁶ : NormedSpace 𝕜 E
inst✝²⁵ : NormedAddCommGroup E'
inst✝²⁴ : NormedSpace 𝕜 E'
inst✝²³ : NormedAddCommGroup E''
inst✝²² : NormedSpace 𝕜 E''
inst✝²¹ : NormedAddCommGroup E'''
inst✝²⁰ : NormedSpace 𝕜 E'''
inst✝¹⁹ : NormedAddCommGroup F
inst✝¹⁸ : NormedSpace 𝕜 F
inst✝¹⁷ : NormedAddCommGroup F'
inst✝¹⁶ : NormedSpace 𝕜 F'
H : Type u_7
inst✝¹⁵ : TopologicalSpace H
H' : Type u_8
inst✝¹⁴ : TopologicalSpace H'
G : Type u_9
inst✝¹³ : TopologicalSpace G
G' : Type u_10
inst✝¹² : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
M' : Type u_12
inst✝⁹ : TopologicalSpace M'
inst✝⁸ : ChartedSpace H' M'
N : Type u_13
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
N' : Type u_14
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace G' N'
n : ℕ∞ω
x : M
f✝ : M → N
g✝ : M' → N'
x' : M'
inst✝³ : IsManifold I n M
inst✝² : IsManifold I' n M'
inst✝¹ : IsManifold J n N
inst✝ : IsManifold J' n N'
hf : IsImmersionAtOfComplement F I J n f✝ x
hg : IsImmersionAtOfComplement F' I' J' n g✝ 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) ∘ f ∘ ↑(φ₁.extend I).symm) (⇑equiv₁ ∘ fun x ↦ (x, 0)) (φ₁.extend I).target
equiv₂ : (E' × F') ≃L[𝕜] E'''
hgprop : EqOn (↑(ψ₂.extend J') ∘ g ∘ ↑(φ₂.extend I').symm) (⇑equiv₂ ∘ fun x ↦ (x, 0)) (φ₂.extend I').target
⊢ EqOn (↑((ψ₁.prod ψ₂).extend (J.prod J')) ∘ Prod.map f g ∘ ↑((φ₁.prod φ₂).extend (I.prod I')).symm)
    (⇑((ContinuousLinearEquiv.prodProdProdComm 𝕜 E E' F F').trans (equiv₁.prodCongr equiv₂)) ∘ fun x ↦ (x, 0))
    ((φ₁.prod φ₂).extend (I.prod I')).target

Tactic:
rw [φ₁.extend_prod φ₂, ψ₁.extend_prod, PartialEquiv.prod_target, eqOn_prod_iff]

Goal state after:
case h
𝕜 : 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✝²⁷ : NormedAddCommGroup E
inst✝²⁶ : NormedSpace 𝕜 E
inst✝²⁵ : NormedAddCommGroup E'
inst✝²⁴ : NormedSpace 𝕜 E'
inst✝²³ : NormedAddCommGroup E''
inst✝²² : NormedSpace 𝕜 E''
inst✝²¹ : NormedAddCommGroup E'''
inst✝²⁰ : NormedSpace 𝕜 E'''
inst✝¹⁹ : NormedAddCommGroup F
inst✝¹⁸ : NormedSpace 𝕜 F
inst✝¹⁷ : NormedAddCommGroup F'
inst✝¹⁶ : NormedSpace 𝕜 F'
H : Type u_7
inst✝¹⁵ : TopologicalSpace H
H' : Type u_8
inst✝¹⁴ : TopologicalSpace H'
G : Type u_9
inst✝¹³ : TopologicalSpace G
G' : Type u_10
inst✝¹² : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
M' : Type u_12
inst✝⁹ : TopologicalSpace M'
inst✝⁸ : ChartedSpace H' M'
N : Type u_13
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
N' : Type u_14
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace G' N'
n : ℕ∞ω
x : M
f✝ : M → N
g✝ : M' → N'
x' : M'
inst✝³ : IsManifold I n M
inst✝² : IsManifold I' n M'
inst✝¹ : IsManifold J n N
inst✝ : IsManifold J' n N'
hf : IsImmersionAtOfComplement F I J n f✝ x
hg : IsImmersionAtOfComplement F' I' J' n g✝ 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) ∘ f ∘ ↑(φ₁.extend I).symm) (⇑equiv₁ ∘ fun x ↦ (x, 0)) (φ₁.extend I).target
equiv₂ : (E' × F') ≃L[𝕜] E'''
hgprop : EqOn (↑(ψ₂.extend J') ∘ g ∘ ↑(φ₂.extend I').symm) (⇑equiv₂ ∘ fun x ↦ (x, 0)) (φ₂.extend I').target
⊢ EqOn (Prod.fst ∘ ↑((ψ₁.extend J).prod (ψ₂.extend J')) ∘ Prod.map f g ∘ ↑((φ₁.extend I).prod (φ₂.extend I')).symm)
      (Prod.fst ∘
        ⇑((ContinuousLinearEquiv.prodProdProdComm 𝕜 E E' F F').trans (equiv₁.prodCongr equiv₂)) ∘ fun x ↦ (x, 0))
      ((φ₁.extend I).target ×ˢ (φ₂.extend I').target) ∧
    EqOn (Prod.snd ∘ ↑((ψ₁.extend J).prod (ψ₂.extend J')) ∘ Prod.map f g ∘ ↑((φ₁.extend I).prod (φ₂.extend I')).symm)
      (Prod.snd ∘
        ⇑((ContinuousLinearEquiv.prodProdProdComm 𝕜 E E' F F').trans (equiv₁.prodCongr equiv₂)) ∘ fun x ↦ (x, 0))
      ((φ₁.extend I).target ×ˢ (φ₂.extend I').target)