[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
x : Multiset α × Multiset α
l : List α
⊢ x ∈ antidiagonal (Quotient.mk (isSetoid α) l) ↔ x.fst + x.snd = Quotient.mk (isSetoid α) l
[PROOFSTEP]
dsimp only [quot_mk_to_coe, antidiagonal_coe]
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
x : Multiset α × Multiset α
l : List α
⊢ x ∈ ↑(revzip (powersetAux l)) ↔ x.fst + x.snd = ↑l
[PROOFSTEP]
refine' ⟨fun h => revzip_powersetAux h, fun h ↦ _⟩
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
x : Multiset α × Multiset α
l : List α
h : x.fst + x.snd = ↑l
⊢ x ∈ ↑(revzip (powersetAux l))
[PROOFSTEP]
haveI := Classical.decEq α
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
x : Multiset α × Multiset α
l : List α
h : x.fst + x.snd = ↑l
this : DecidableEq α
⊢ x ∈ ↑(revzip (powersetAux l))
[PROOFSTEP]
simp only [revzip_powersetAux_lemma l revzip_powersetAux, h.symm, ge_iff_le, mem_coe, List.mem_map, mem_powersetAux]
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
cases' x with x₁ x₂
[GOAL]
case mk
α : Type u_1
β : Type u_2
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₂)
[PROOFSTEP]
exact ⟨x₁, le_add_right _ _, by rw [add_tsub_cancel_left x₁ x₂]⟩
[GOAL]
α : Type u_1
β : Type u_2
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₂)
[PROOFSTEP]
rw [add_tsub_cancel_left x₁ x₂]
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
l : List α
⊢ map Prod.fst (antidiagonal (Quotient.mk (isSetoid α) l)) = powerset (Quotient.mk (isSetoid α) l)
[PROOFSTEP]
simp [powersetAux']
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
l : List α
⊢ map Prod.snd (antidiagonal (Quotient.mk (isSetoid α) l)) = powerset (Quotient.mk (isSetoid α) l)
[PROOFSTEP]
simp [powersetAux']
[GOAL]
α : Type u_1
β : Type u_2
a : α
s : Multiset α
l : List α
⊢ antidiagonal (a ::ₘ Quotient.mk (isSetoid α) l) =
    map (Prod.map id (cons a)) (antidiagonal (Quotient.mk (isSetoid α) l)) +
      map (Prod.map (cons a) id) (antidiagonal (Quotient.mk (isSetoid α) l))
[PROOFSTEP]
simp only [revzip, reverse_append, quot_mk_to_coe, coe_eq_coe, powersetAux'_cons, cons_coe, coe_map, antidiagonal_coe',
  coe_add]
[GOAL]
α : Type u_1
β : Type u_2
a : α
s : Multiset α
l : List α
⊢ zip (powersetAux' l ++ List.map (cons a) (powersetAux' l))
      (reverse (List.map (cons a) (powersetAux' l)) ++ reverse (powersetAux' l)) ~
    List.map (fun x => Prod.map id (cons a) x) (zip (powersetAux' l) (reverse (powersetAux' l))) ++
      List.map (fun x => Prod.map (cons a) id x) (zip (powersetAux' l) (reverse (powersetAux' l)))
[PROOFSTEP]
rw [← zip_map, ← zip_map, zip_append, (_ : _ ++ _ = _)]
[GOAL]
α : Type u_1
β : Type u_2
a : α
s : Multiset α
l : List α
⊢ zip (powersetAux' l) (reverse (List.map (cons a) (powersetAux' l))) ++
      zip (List.map (cons a) (powersetAux' l)) (reverse (powersetAux' l)) =
    zip (List.map id (powersetAux' l)) (List.map (cons a) (reverse (powersetAux' l))) ++
      zip (List.map (cons a) (powersetAux' l)) (List.map id (reverse (powersetAux' l)))
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a
α : Type u_1
β : Type u_2
a : α
s : Multiset α
l : List α
⊢ powersetAux' l = List.map id (powersetAux' l)
case e_a.e_a
α : Type u_1
β : Type u_2
a : α
s : Multiset α
l : List α
⊢ reverse (List.map (cons a) (powersetAux' l)) = List.map (cons a) (reverse (powersetAux' l))
case e_a.e_a
α : Type u_1
β : Type u_2
a : α
s : Multiset α
l : List α
⊢ reverse (powersetAux' l) = List.map id (reverse (powersetAux' l))
[PROOFSTEP]
simp
[GOAL]
case e_a.e_a
α : Type u_1
β : Type u_2
a : α
s : Multiset α
l : List α
⊢ reverse (List.map (cons a) (powersetAux' l)) = List.map (cons a) (reverse (powersetAux' l))
case e_a.e_a
α : Type u_1
β : Type u_2
a : α
s : Multiset α
l : List α
⊢ reverse (powersetAux' l) = List.map id (reverse (powersetAux' l))
[PROOFSTEP]
rw [map_reverse]
[GOAL]
case e_a.e_a
α : Type u_1
β : Type u_2
a : α
s : Multiset α
l : List α
⊢ reverse (powersetAux' l) = List.map id (reverse (powersetAux' l))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
a : α
s : Multiset α
l : List α
⊢ length (powersetAux' l) = length (reverse (List.map (cons a) (powersetAux' l)))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Multiset α
⊢ antidiagonal s = map (fun t => (s - t, t)) (powerset s)
[PROOFSTEP]
induction' s using Multiset.induction_on with a s hs
[GOAL]
case empty
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
⊢ antidiagonal 0 = map (fun t => (0 - t, t)) (powerset 0)
[PROOFSTEP]
simp only [antidiagonal_zero, powerset_zero, zero_tsub, map_singleton]
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : antidiagonal s = map (fun t => (s - t, t)) (powerset s)
⊢ antidiagonal (a ::ₘ s) = map (fun t => (a ::ₘ s - t, t)) (powerset (a ::ₘ s))
[PROOFSTEP]
simp_rw [antidiagonal_cons, powerset_cons, map_add, hs, map_map, Function.comp, Prod.map_mk, id.def, sub_cons,
  erase_cons_head]
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : antidiagonal s = map (fun t => (s - t, t)) (powerset s)
⊢ map (fun x => (s - x, a ::ₘ x)) (powerset s) + map (fun x => (a ::ₘ (s - x), x)) (powerset s) =
    map (fun x => (a ::ₘ s - x, x)) (powerset s) + map (fun x => (s - x, a ::ₘ x)) (powerset s)
[PROOFSTEP]
rw [add_comm]
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : antidiagonal s = map (fun t => (s - t, t)) (powerset s)
⊢ map (fun x => (a ::ₘ (s - x), x)) (powerset s) + map (fun x => (s - x, a ::ₘ x)) (powerset s) =
    map (fun x => (a ::ₘ s - x, x)) (powerset s) + map (fun x => (s - x, a ::ₘ x)) (powerset s)
[PROOFSTEP]
congr 1
[GOAL]
case cons.e_a
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : antidiagonal s = map (fun t => (s - t, t)) (powerset s)
⊢ map (fun x => (a ::ₘ (s - x), x)) (powerset s) = map (fun x => (a ::ₘ s - x, x)) (powerset s)
[PROOFSTEP]
refine' Multiset.map_congr rfl fun x hx ↦ _
[GOAL]
case cons.e_a
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : antidiagonal s = map (fun t => (s - t, t)) (powerset s)
x : Multiset α
hx : x ∈ powerset s
⊢ (a ::ₘ (s - x), x) = (a ::ₘ s - x, x)
[PROOFSTEP]
rw [cons_sub_of_le _ (mem_powerset.mp hx)]
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
⊢ ↑card (antidiagonal s) = 2 ^ ↑card s
[PROOFSTEP]
have := card_powerset s
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
this : ↑card (powerset s) = 2 ^ ↑card s
⊢ ↑card (antidiagonal s) = 2 ^ ↑card s
[PROOFSTEP]
rwa [← antidiagonal_map_fst, card_map] at this 
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CommSemiring β
s : Multiset α
f g : α → β
⊢ prod (map (fun a => f a + g a) s) = sum (map (fun p => prod (map f p.fst) * prod (map g p.snd)) (antidiagonal s))
[PROOFSTEP]
refine' s.induction_on _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝ : CommSemiring β
s : Multiset α
f g : α → β
⊢ prod (map (fun a => f a + g a) 0) = sum (map (fun p => prod (map f p.fst) * prod (map g p.snd)) (antidiagonal 0))
[PROOFSTEP]
simp only [map_zero, prod_zero, antidiagonal_zero, map_singleton, mul_one, sum_singleton]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝ : CommSemiring β
s : Multiset α
f g : α → β
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    prod (map (fun a => f a + g a) s) = sum (map (fun p => prod (map f p.fst) * prod (map g p.snd)) (antidiagonal s)) →
      prod (map (fun a => f a + g a) (a ::ₘ s)) =
        sum (map (fun p => prod (map f p.fst) * prod (map g p.snd)) (antidiagonal (a ::ₘ s)))
[PROOFSTEP]
intro a s ih
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝ : CommSemiring β
s✝ : Multiset α
f g : α → β
a : α
s : Multiset α
ih : prod (map (fun a => f a + g a) s) = sum (map (fun p => prod (map f p.fst) * prod (map g p.snd)) (antidiagonal s))
⊢ prod (map (fun a => f a + g a) (a ::ₘ s)) =
    sum (map (fun p => prod (map f p.fst) * prod (map g p.snd)) (antidiagonal (a ::ₘ s)))
[PROOFSTEP]
simp only [map_cons, prod_cons, ih, sum_map_mul_left.symm, add_mul, mul_left_comm (f a), mul_left_comm (g a),
  sum_map_add, antidiagonal_cons, Prod_map, id_eq, map_add, map_map, Function.comp_apply, mul_assoc, sum_add]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝ : CommSemiring β
s✝ : Multiset α
f g : α → β
a : α
s : Multiset α
ih : prod (map (fun a => f a + g a) s) = sum (map (fun p => prod (map f p.fst) * prod (map g p.snd)) (antidiagonal s))
⊢ sum (map (fun i => prod (map f i.fst) * (f a * prod (map g i.snd))) (antidiagonal s)) +
      sum (map (fun i => prod (map f i.fst) * (g a * prod (map g i.snd))) (antidiagonal s)) =
    sum (map (fun x => prod (map f x.fst) * (g a * prod (map g x.snd))) (antidiagonal s)) +
      sum (map (fun i => prod (map f i.fst) * (f a * prod (map g i.snd))) (antidiagonal s))
[PROOFSTEP]
exact add_comm _ _
