case empty
α : Type u_1
β : Type ?u.21052
inst✝ : DecidableEq α
⊢ antidiagonal 0 = map (fun t => (0 - t, t)) (powerset 0)

case cons
α : Type u_1
β : Type ?u.21052
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))
α : Type u_1
β : Type ?u.21052
inst✝ : DecidableEq α
s : Multiset α
⊢ antidiagonal s = map (fun t => (s - t, t)) (powerset s)
induction' s using Multiset.induction_on with a s hs
no goals
case empty
α : Type u_1
β : Type ?u.21052
inst✝ : DecidableEq α
⊢ antidiagonal 0 = map (fun t => (0 - t, t)) (powerset 0)
simp only [antidiagonal_zero, powerset_zero, zero_tsub, map_singleton]
case cons
α : Type u_1
β : Type ?u.21052
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)
case cons
α : Type u_1
β : Type ?u.21052
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))
simp_rw [antidiagonal_cons, powerset_cons, map_add, hs, map_map, Function.comp, Prod.map_mk,
  id.def, sub_cons, erase_cons_head]
case cons
α : Type u_1
β : Type ?u.21052
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)
case cons
α : Type u_1
β : Type ?u.21052
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)
rw [add_comm]
case cons.e_a
α : Type u_1
β : Type ?u.21052
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)
case cons
α : Type u_1
β : Type ?u.21052
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)
congr 1
case cons.e_a
α : Type u_1
β : Type ?u.21052
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)
case cons.e_a
α : Type u_1
β : Type ?u.21052
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)
refine' Multiset.map_congr rfl fun x hx ↦ _
no goals
case cons.e_a
α : Type u_1
β : Type ?u.21052
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)
rw [cons_sub_of_le _ (mem_powerset.mp hx)]