-- Module: Mathlib.Analysis.Normed.Operator.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace 𝕜 G
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
M₄ : Type u_8
inst_7 : SeminormedAddCommGroup M₁
inst_8 : NormedSpace 𝕜 M₁
inst_9 : SeminormedAddCommGroup M₂
inst_10 : NormedSpace 𝕜 M₂
inst_11 : SeminormedAddCommGroup M₃
inst_12 : NormedSpace 𝕜 M₃
inst_13 : SeminormedAddCommGroup M₄
inst_14 : NormedSpace 𝕜 M₄
φ : M₁ →L[𝕜] M₂
ψ : M₃ →L[𝕜] M₄
h :
  ∀ (x : M₁ × M₃) (x₁ : M₁) (x₂ : M₃),
    Eq (α := M₂ × M₄) (((φ, ψ).1.prodMap (φ, ψ).2 : (a : M₁ × M₃) → M₂ × M₄) (x₁, x₂) : M₂ × M₄)
      ((((have Φ₁ : (M₁ →L[𝕜] M₂) →L[𝕜] M₁ →L[𝕜] M₂ × M₄ :=
                    (compL 𝕜 M₁ M₂ (M₂ × M₄) : (a : M₂ →L[𝕜] M₂ × M₄) → (M₁ →L[𝕜] M₂) →L[𝕜] M₁ →L[𝕜] M₂ × M₄)
                      (inl 𝕜 M₂ M₄);
                  have Φ₂ : (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₂ × M₄ :=
                    (compL 𝕜 M₃ M₄ (M₂ × M₄) : (a : M₄ →L[𝕜] M₂ × M₄) → (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₂ × M₄)
                      (inr 𝕜 M₂ M₄);
                  have Φ₁' : (M₁ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄ :=
                    (flip (compL 𝕜 (M₁ × M₃) M₁ (M₂ × M₄)) :
                        (a : M₁ × M₃ →L[𝕜] M₁) → (M₁ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄)
                      (fst 𝕜 M₁ M₃);
                  have Φ₂' : (M₃ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄ :=
                    (flip (compL 𝕜 (M₁ × M₃) M₃ (M₂ × M₄)) :
                        (a : M₁ × M₃ →L[𝕜] M₃) → (M₃ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄)
                      (snd 𝕜 M₁ M₃);
                  have Ψ₁ : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄) →L[𝕜] M₁ →L[𝕜] M₂ := fst 𝕜 (M₁ →L[𝕜] M₂) (M₃ →L[𝕜] M₄);
                  have Ψ₂ : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₄ := snd 𝕜 (M₁ →L[𝕜] M₂) (M₃ →L[𝕜] M₄);
                  Φ₁' ∘SL Φ₁ ∘SL Ψ₁ + Φ₂' ∘SL Φ₂ ∘SL Ψ₂ :
                  (a : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄)) → M₁ × M₃ →L[𝕜] M₂ × M₄)
                (φ, ψ) :
              M₁ × M₃ →L[𝕜] M₂ × M₄) :
            (a : M₁ × M₃) → M₂ × M₄)
          (x₁, x₂) :
        M₂ × M₄)
⊢ (φ, ψ).1.prodMap (φ, ψ).2 =
    (have Φ₁ : (M₁ →L[𝕜] M₂) →L[𝕜] M₁ →L[𝕜] M₂ × M₄ :=
          (compL 𝕜 M₁ M₂ (M₂ × M₄) : (a : M₂ →L[𝕜] M₂ × M₄) → (M₁ →L[𝕜] M₂) →L[𝕜] M₁ →L[𝕜] M₂ × M₄) (inl 𝕜 M₂ M₄);
        have Φ₂ : (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₂ × M₄ :=
          (compL 𝕜 M₃ M₄ (M₂ × M₄) : (a : M₄ →L[𝕜] M₂ × M₄) → (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₂ × M₄) (inr 𝕜 M₂ M₄);
        have Φ₁' : (M₁ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄ :=
          (flip (compL 𝕜 (M₁ × M₃) M₁ (M₂ × M₄)) :
              (a : M₁ × M₃ →L[𝕜] M₁) → (M₁ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄)
            (fst 𝕜 M₁ M₃);
        have Φ₂' : (M₃ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄ :=
          (flip (compL 𝕜 (M₁ × M₃) M₃ (M₂ × M₄)) :
              (a : M₁ × M₃ →L[𝕜] M₃) → (M₃ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄)
            (snd 𝕜 M₁ M₃);
        have Ψ₁ : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄) →L[𝕜] M₁ →L[𝕜] M₂ := fst 𝕜 (M₁ →L[𝕜] M₂) (M₃ →L[𝕜] M₄);
        have Ψ₂ : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₄ := snd 𝕜 (M₁ →L[𝕜] M₂) (M₃ →L[𝕜] M₄);
        Φ₁' ∘SL Φ₁ ∘SL Ψ₁ + Φ₂' ∘SL Φ₂ ∘SL Ψ₂ :
        (a : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄)) → M₁ × M₃ →L[𝕜] M₂ × M₄)
      (φ, ψ)

Tactic:
refine ContinuousLinearMap.ext fun ⟨x₁, x₂⟩ => ?_

Premises used: ContinuousLinearMap.ext