case mk
α : Type u
f p₁ p₂ : α →₀ ℕ
⊢ (p₁, p₂) ∈ antidiagonal f ↔ (p₁, p₂).fst + (p₁, p₂).snd = f
α : Type u
f : α →₀ ℕ
p : (α →₀ ℕ) × (α →₀ ℕ)
⊢ p ∈ antidiagonal f ↔ p.fst + p.snd = f
rcases p with ⟨p₁, p₂⟩
no goals
case mk
α : Type u
f p₁ p₂ : α →₀ ℕ
⊢ (p₁, p₂) ∈ antidiagonal f ↔ (p₁, p₂).fst + (p₁, p₂).snd = f
simp [antidiagonal, antidiagonal', ← and_assoc, ← Finsupp.toMultiset.apply_eq_iff_eq]