α : Type u_1
β : Type ?u.819
s : Multiset α
x : Multiset α × Multiset α
l : List α
⊢ x ∈ ↑(revzip (powersetAux l)) ↔ x.fst + x.snd = ↑l
α : Type u_1
β : Type ?u.819
s : Multiset α
x : Multiset α × Multiset α
l : List α
⊢ x ∈ antidiagonal (Quotient.mk (isSetoid α) l) ↔ x.fst + x.snd = Quotient.mk (isSetoid α) l
dsimp only [quot_mk_to_coe, antidiagonal_coe]
α : Type u_1
β : Type ?u.819
s : Multiset α
x : Multiset α × Multiset α
l : List α
h : x.fst + x.snd = ↑l
⊢ x ∈ ↑(revzip (powersetAux l))
α : Type u_1
β : Type ?u.819
s : Multiset α
x : Multiset α × Multiset α
l : List α
⊢ x ∈ ↑(revzip (powersetAux l)) ↔ x.fst + x.snd = ↑l
refine' ⟨fun h => revzip_powersetAux h, fun h ↦ _⟩
α : Type u_1
β : Type ?u.819
s : Multiset α
x : Multiset α × Multiset α
l : List α
h : x.fst + x.snd = ↑l
this : DecidableEq α
⊢ x ∈ ↑(revzip (powersetAux l))
α : Type u_1
β : Type ?u.819
s : Multiset α
x : Multiset α × Multiset α
l : List α
h : x.fst + x.snd = ↑l
⊢ x ∈ ↑(revzip (powersetAux l))
haveI := Classical.decEq α
α : Type u_1
β : Type ?u.819
s : Multiset α
x : Multiset α × Multiset α
l : List α
h : x.fst + x.snd = ↑l
this : DecidableEq α
⊢ ∃ a, a ≤ x.fst + x.snd ∧ (a, x.fst + x.snd - a) = x
α : Type u_1
β : Type ?u.819
s : Multiset α
x : Multiset α × Multiset α
l : List α
h : x.fst + x.snd = ↑l
this : DecidableEq α
⊢ x ∈ ↑(revzip (powersetAux l))
simp only [revzip_powersetAux_lemma l revzip_powersetAux, h.symm, ge_iff_le, mem_coe,
  List.mem_map, mem_powersetAux]
case mk
α : Type u_1
β : Type ?u.819
s : Multiset α
l : List α
this : DecidableEq α
x₁ x₂ : Multiset α
h : (x₁, x₂).fst + (x₁, x₂).snd = ↑l
⊢ ∃ a, a ≤ (x₁, x₂).fst + (x₁, x₂).snd ∧ (a, (x₁, x₂).fst + (x₁, x₂).snd - a) = (x₁, x₂)
α : Type u_1
β : Type ?u.819
s : Multiset α
x : Multiset α × Multiset α
l : List α
h : x.fst + x.snd = ↑l
this : DecidableEq α
⊢ ∃ a, a ≤ x.fst + x.snd ∧ (a, x.fst + x.snd - a) = x
cases' x with x₁ x₂
no goals
case mk
α : Type u_1
β : Type ?u.819
s : Multiset α
l : List α
this : DecidableEq α
x₁ x₂ : Multiset α
h : (x₁, x₂).fst + (x₁, x₂).snd = ↑l
⊢ ∃ a, a ≤ (x₁, x₂).fst + (x₁, x₂).snd ∧ (a, (x₁, x₂).fst + (x₁, x₂).snd - a) = (x₁, x₂)
exact ⟨x₁, le_add_right _ _, by rw [add_tsub_cancel_left x₁ x₂]⟩
no goals
α : Type u_1
β : Type ?u.819
s : Multiset α
l : List α
this : DecidableEq α
x₁ x₂ : Multiset α
h : (x₁, x₂).fst + (x₁, x₂).snd = ↑l
⊢ (x₁, (x₁, x₂).fst + (x₁, x₂).snd - x₁) = (x₁, x₂)
rw [add_tsub_cancel_left x₁ x₂]