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

State before:
d : ℕ
⊢ d.finMulAntidiagonal 0 = ∅
Tactic:
ext
State after:
case a
d : ℕ
a✝ : Fin d → ℕ
⊢ a✝ ∈ d.finMulAntidiagonal 0 ↔ a✝ ∈ ∅

State before:
case a
d : ℕ
a✝ : Fin d → ℕ
⊢ a✝ ∈ d.finMulAntidiagonal 0 ↔ a✝ ∈ ∅
Tactic:
simp
State after:
no goals