-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
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
⊢ {
      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) }
have 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' := sorry, map_smul' := sorry, cont := sorry } :
          (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' := sorry, map_smul' := sorry, cont := sorry : 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' := sorry, map_smul' := sorry, cont := sorry : C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A) } :
          (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
        x i :
      A)
Tactic: ext