Automatically generated lemmas for working with concrete matrices

In Mathlib3, this file contained "magic" lemmas which autogenerate to the correct size of matrix. For instance, Matrix.of_mul_of_fin could be used as:

example {α} [AddCommMonoid α] [Mul α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α) :
  !![a₁₁, a₁₂;
     a₂₁, a₂₂] * !![b₁₁, b₁₂;
                    b₂₁, b₂₂] = !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂;
                                   a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂] := by
  rw [of_mul_of_fin]

Porting note: these magic lemmas have been skipped for now, though the plumbing lemmas in Mathlib.Data.Matrix.Reflection are still available