Easy simplification of linear equation

Stream: maths

[Anirudh Suresh]

import Mathlib
open scoped Matrix


theorem ha (a b c d:ℂ) (m00 m01 m10 m11:Matrix (Fin (4)) (Fin (1)) ℂ) : (4:ℤ) • a • (2:ℂ)⁻¹ • (2:ℂ)⁻¹ • m00 +
    ((4:ℤ) • b • (2:ℂ)⁻¹ • (2:ℂ)⁻¹ • m01 + ((4:ℤ) • c • (2:ℂ)⁻¹ • (2:ℂ)⁻¹ • m11 + (4:ℤ) • d • (2:ℂ)⁻¹ • (2:ℂ)⁻¹ • m10)) =
  a • m00 + (b • m01 + (c • m11 + d • m10)):= by {

  }

Is there some way in Lean where we can directly prove linear equations like this easily without using a bunch of rewrites?

[Bhavik Mehta]

Yes, use module