-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
M₁ M₂ : CStarMatrix m n A
h :
  ∀ (x : C⋆ᵐᵒᵈ(A, m → A)) (i : n),
    Eq.{u_5 + 1} (α := A)
      (({
              toFun :=
                Function.comp (β := n → A)
                  (⇑(ContinuousLinearEquiv.symm (WithCStarModule.equivL ℂ (A := A) (E := n → A)) :
                        (n → A) ≃L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
                    (a : n → A) → C⋆ᵐᵒᵈ(A, n → A))
                  ((fun (v : m → A) ↦ v ᵥ* (M₁ + M₂)) ∘
                    (⇑(WithCStarModule.equivL ℂ (A := A) (E := m → A) : C⋆ᵐᵒᵈ(A, m → A) ≃L[ℂ] m → A) :
                      (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A)),
              map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } :
            (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
          x i :
        A)
      ((HAdd.hAdd (α := C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
              {
                toFun :=
                  Function.comp (β := n → A)
                    (⇑(ContinuousLinearEquiv.symm (WithCStarModule.equivL ℂ (A := A) (E := n → A)) :
                          (n → A) ≃L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
                      (a : n → A) → C⋆ᵐᵒᵈ(A, n → A))
                    ((fun (v : m → A) ↦ v ᵥ* M₁) ∘
                      (⇑(WithCStarModule.equivL ℂ (A := A) (E := m → A) : C⋆ᵐᵒᵈ(A, m → A) ≃L[ℂ] m → A) :
                        (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A)),
                map_add' := ⋯, map_smul' := ⋯, cont := ⋯ : C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A) }
              {
                toFun :=
                  Function.comp (β := n → A)
                    (⇑(ContinuousLinearEquiv.symm (WithCStarModule.equivL ℂ (A := A) (E := n → A)) :
                          (n → A) ≃L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
                      (a : n → A) → C⋆ᵐᵒᵈ(A, n → A))
                    ((fun (v : m → A) ↦ v ᵥ* M₂) ∘
                      (⇑(WithCStarModule.equivL ℂ (A := A) (E := m → A) : C⋆ᵐᵒᵈ(A, m → A) ≃L[ℂ] m → A) :
                        (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A)),
                map_add' := ⋯, map_smul' := ⋯, cont := ⋯ : C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A) } :
            (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
          x i :
        A)
⊢ {
      toFun :=
        Function.comp (β := n → A)
          (⇑(ContinuousLinearEquiv.symm (WithCStarModule.equivL ℂ (A := A) (E := n → A)) :
                (n → A) ≃L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
            (a : n → A) → C⋆ᵐᵒᵈ(A, n → A))
          ((fun (v : m → A) ↦ v ᵥ* (M₁ + M₂)) ∘
            (⇑(WithCStarModule.equivL ℂ (A := A) (E := m → A) : C⋆ᵐᵒᵈ(A, m → A) ≃L[ℂ] m → A) :
              (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A)),
      map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } =
    HAdd.hAdd (α := C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
      {
        toFun :=
          Function.comp (β := n → A)
            (⇑(ContinuousLinearEquiv.symm (WithCStarModule.equivL ℂ (A := A) (E := n → A)) :
                  (n → A) ≃L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
              (a : n → A) → C⋆ᵐᵒᵈ(A, n → A))
            ((fun (v : m → A) ↦ v ᵥ* M₁) ∘
              (⇑(WithCStarModule.equivL ℂ (A := A) (E := m → A) : C⋆ᵐᵒᵈ(A, m → A) ≃L[ℂ] m → A) :
                (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A)),
        map_add' := ⋯, map_smul' := ⋯, cont := ⋯ : C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A) }
      {
        toFun :=
          Function.comp (β := n → A)
            (⇑(ContinuousLinearEquiv.symm (WithCStarModule.equivL ℂ (A := A) (E := n → A)) :
                  (n → A) ≃L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
              (a : n → A) → C⋆ᵐᵒᵈ(A, n → A))
            ((fun (v : m → A) ↦ v ᵥ* M₂) ∘
              (⇑(WithCStarModule.equivL ℂ (A := A) (E := m → A) : C⋆ᵐᵒᵈ(A, m → A) ≃L[ℂ] m → A) :
                (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A)),
        map_add' := ⋯, map_smul' := ⋯, cont := ⋯ : C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A) }

Tactic:
ext