Theorem: Nat.finMulAntidiagonal_three (PrimeNumberTheoremAnd/Mathlib/Data/Nat/FinMulAntidiagonal.lean)

State before:
n : ℕ
⊢ ∀ a ∈ finMulAntidiagonal 3 n, a 0 * a 1 * a 2 = n
Tactic:
intro a ha
State after:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ a 0 * a 1 * a 2 = n

State before:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ a 0 * a 1 * a 2 = n
Tactic:
rw [← (mem_finMulAntidiagonal.mp ha).1, Fin.prod_univ_three a]
State after:
no goals