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