have hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2 := by
  rw [finMulAntidiagonal_three a ha, hfab1, finMulAntidiagonal_three b hb]
case intro
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
⊢ a = b
case intro
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
⊢ a = b