Equality of vectors/matrices

Stream: new members

[Snir Broshi]

I'm working with vectors and matrices of dimension 2, and I want to prove some vectors/matrices are equal when they are given explicitly, e.g.:

import Mathlib
open Matrix

theorem foo (a b c d e f : ℤ) :
    !![a, b; c, d] *ᵥ ![e, f] = ![a * e + b * f, c * e + d * f] := by
  ext i
  have : i = 0 ∨ i = 1 := by sorry
  cases this
    <;> simp [*]
    <;> ring

What's the proper way of doing this? funext + cases on Fin 2 seems pretty weird.
(the specific example above is the mat-mul formula so maybe there's a theorem for it specifically for Fin 2 (which I couldn't find), but I'm asking about vector/matrix extensionality in general)

[Ruben Van de Velde]

fin_cases?

[Aaron Liu]

yeah usually I see something like

import Mathlib
open Matrix

theorem foo (a b c d e f : ℤ) :
    !![a, b; c, d] *ᵥ ![e, f] = ![a * e + b * f, c * e + d * f] := by
  ext i; fin_cases i <;> simp <;> ring

[Snir Broshi]

Thanks! Is that the idiomatic way to do it? I thought there would be some tactic/theorem that hides the fact that vectors/matrices are functions, similar to how Set likes to hide that fact. Maybe something combining ext and fin_cases together?

[Aaron Liu]

applying matrices (like !![a, b; c, d]) to Fin numbers as if they are functions is something that's theoretically bad I guess but no one seems to care

[Aaron Liu]

applying finvecs (like ![a, b, c]) to Fin numbers as if they are functions is perfectly fine since it is just a function

[Kenny Lau]

it is possible to approach this with a simproc (which is yet to be written) but I think this is a bit of a low priority because mathlib itself doesn't do concrete matrices often

[Kenny Lau]

e.g. #28148 for transpose

[Ruben Van de Velde]

Aaron Liu said:

applying matrices (like !![a, b; c, d]) to Fin numbers as if they are functions is something that's theoretically bad I guess but no one seems to care

That's not happening in this example though, is it?