-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
F₁ : Type u_11
inst_20 : NormedAddCommGroup F₁
inst_21 : NormedSpace 𝕜 F₁
E₁ : B → Type u_12
inst_22 : TopologicalSpace (TotalSpace F₁ E₁)
inst_23 : (x : B) → AddCommMonoid (E₁ x)
inst_24 : (x : B) → Module.{u_1, u_12} 𝕜 (E₁ x)
F₂ : Type u_13
inst_25 : NormedAddCommGroup F₂
inst_26 : NormedSpace 𝕜 F₂
E₂ : B → Type u_14
inst_27 : TopologicalSpace (TotalSpace F₂ E₂)
inst_28 : (x : B) → AddCommMonoid (E₂ x)
inst_29 : (x : B) → Module.{u_1, u_14} 𝕜 (E₂ x)
inst_30 : (x : B) → TopologicalSpace (E₁ x)
inst_31 : (x : B) → TopologicalSpace (E₂ x)
inst_32 : FiberBundle F₁ E₁
inst_33 : FiberBundle F₂ E₂
inst_34 : VectorBundle 𝕜 F₁ E₁
inst_35 : VectorBundle 𝕜 F₂ E₂
inst_36 : ContMDiffVectorBundle n F₁ E₁ IB
inst_37 : ContMDiffVectorBundle n F₂ E₂ IB
inst_38 : IsManifold IB n B
e₁ : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
i₁ : MemTrivializationAtlas (E := E₁) e₁
i₂ : MemTrivializationAtlas (E := E₂) e₂
e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
i₁' : MemTrivializationAtlas (E := E₁) e₁'
i₂' : MemTrivializationAtlas (E := E₂) e₂'
refine_1 :
  ContMDiffOn.{u_1, u_7, u_8, u_2, u_11, u_11, u_11} IB (E' := F₁ →L[𝕜] F₁) 𝓘(𝕜, F₁ →L[𝕜] F₁) (M' := F₁ →L[𝕜] F₁) n
    (fun (y : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁ e₁' y) : F₁ →L[𝕜] F₁))
    ((e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet ∩ (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂').baseSet)
⊢ ContMDiffOn IB (E' := F₁ × F₂ →L[𝕜] F₁ × F₂) 𝓘(𝕜, F₁ × F₂ →L[𝕜] F₁ × F₂) (M' := F₁ × F₂ →L[𝕜] F₁ × F₂) n
    (fun (y : B) ↦
      ContinuousLinearMap.prodMap (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁ e₁' y) : F₁ →L[𝕜] F₁)
        (↑(Trivialization.coordChangeL 𝕜 (E := E₂) e₂ e₂' y) : F₂ →L[𝕜] F₂))
    ((e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet ∩ (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂').baseSet)
have refine_2 : ContMDiffOn.{u_1, u_7, u_8, u_2, u_13, u_13, u_13} IB (E' := F₂ →L[𝕜] F₂) 𝓘(𝕜, F₂ →L[𝕜] F₂) (M' := F₂ →L[𝕜] F₂) n
  (fun (y : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₂) e₂ e₂' y) : F₂ →L[𝕜] F₂))
  ((e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet ∩ (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂').baseSet)
Tactic: refine ContMDiffOn.clm_prodMap ?_ ?_