English
x ∈ antidiagonal s iff x.1 + x.2 = s.
Русский
x ∈ антидиагональ s тогда, когда x.1 + x.2 = s.
LaTeX
$$$$ x \in \operatorname{antidiagonal}(s) \iff x_1 + x_2 = s $$$$
Lean4
/-- A pair `(t₁, t₂)` of multisets is contained in `antidiagonal s`
if and only if `t₁ + t₂ = s`. -/
@[simp]
theorem mem_antidiagonal {s : Multiset α} {x : Multiset α × Multiset α} : x ∈ antidiagonal s ↔ x.1 + x.2 = s :=
Quotient.inductionOn s fun l ↦ by
dsimp only [quot_mk_to_coe, antidiagonal_coe]
refine ⟨fun h => revzip_powersetAux h, fun h ↦ ?_⟩
have _ := Classical.decEq α
simp only [revzip_powersetAux_lemma l revzip_powersetAux, h.symm, mem_coe, List.mem_map, mem_powersetAux]
obtain ⟨x₁, x₂⟩ := x
exact ⟨x₁, le_add_right _ _, by rw [add_tsub_cancel_left x₁ x₂]⟩
