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

State before:
n : ℕ
hn : n ≠ 1
⊢ finMulAntidiagonal 0 n = ∅
Tactic:
ext
State after:
case a
n : ℕ
hn : n ≠ 1
a✝ : Fin 0 → ℕ
⊢ a✝ ∈ finMulAntidiagonal 0 n ↔ a✝ ∈ ∅

State before:
case a
n : ℕ
hn : n ≠ 1
a✝ : Fin 0 → ℕ
⊢ a✝ ∈ finMulAntidiagonal 0 n ↔ a✝ ∈ ∅
Tactic:
simp [hn.symm]
State after:
no goals