funext i
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
hab2 : a 2 = b 2
hab0 : a 0 = b 0
hab1 : a 1 = b 1
⊢ a = b
case intro.h
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
hab2 : a 2 = b 2
hab0 : a 0 = b 0
hab1 : a 1 = b 1
i : Fin 3
⊢ a i = b i