have := Fin.lexFold_inj (Fin.eq_of_val_eq hcontra)
case h
α : Type u
r c : Nat
a : Matrix α r c
i : Fin r
j₁ j₂ : Fin c
h : j₁ ≠ j₂
v : α
hcontra : ↑(Fin.lexFold i j₁) = ↑(Fin.lexFold i j₂)
⊢ False
case h
α : Type u
r c : Nat
a : Matrix α r c
i : Fin r
j₁ j₂ : Fin c
h : j₁ ≠ j₂
v : α
hcontra : ↑(Fin.lexFold i j₁) = ↑(Fin.lexFold i j₂)
this : i = i ∧ j₁ = j₂
⊢ False