-- Mathlib/Data/Multiset/Antidiagonal.lean
theorem antidiagonal_eq_map_powerset [DecidableEq α] (s : Multiset α) :
    s.antidiagonal = s.powerset.map fun t ↦ (s - t, t)

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun t => (s - t, t)) s.powerset
⊢ (a ::ₘ s).antidiagonal = map (fun t => (a ::ₘ s - t, t)) (a ::ₘ s).powerset

Tactic:
simp_rw [antidiagonal_cons, powerset_cons, map_add, hs, map_map, Function.comp, Prod.map_apply,
  id, sub_cons, erase_cons_head]

Result:
case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun t => (s - t, t)) s.powerset
⊢ map (fun x => (s - x, a ::ₘ x)) s.powerset + map (fun x => (a ::ₘ (s - x), x)) s.powerset =
    map (fun x => (a ::ₘ s - x, x)) s.powerset + map (fun x => (s - x, a ::ₘ x)) s.powerset

Proof state:
case cons.e_a
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun t => (s - t, t)) s.powerset
x : Multiset α
hx : x ∈ s.powerset
⊢ (a ::ₘ (s - x), x) = (a ::ₘ s - x, x)

Tactic:
rw [cons_sub_of_le _ (mem_powerset.mp hx)]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ s.antidiagonal = map (fun t => (s - t, t)) s.powerset

Tactic:
induction' s using Multiset.induction_on with a s hs

Result:
case empty
α : Type u_1
inst✝ : DecidableEq α
⊢ antidiagonal 0 = map (fun t => (0 - t, t)) (powerset 0)

case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun t => (s - t, t)) s.powerset
⊢ (a ::ₘ s).antidiagonal = map (fun t => (a ::ₘ s - t, t)) (a ::ₘ s).powerset

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun t => (s - t, t)) s.powerset
⊢ map (fun x => (a ::ₘ (s - x), x)) s.powerset + map (fun x => (s - x, a ::ₘ x)) s.powerset =
    map (fun x => (a ::ₘ s - x, x)) s.powerset + map (fun x => (s - x, a ::ₘ x)) s.powerset

Tactic:
congr 1

Result:
case cons.e_a
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun t => (s - t, t)) s.powerset
⊢ map (fun x => (a ::ₘ (s - x), x)) s.powerset = map (fun x => (a ::ₘ s - x, x)) s.powerset

Proof state:
case cons.e_a
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun t => (s - t, t)) s.powerset
⊢ map (fun x => (a ::ₘ (s - x), x)) s.powerset = map (fun x => (a ::ₘ s - x, x)) s.powerset

Tactic:
refine Multiset.map_congr rfl fun x hx ↦ ?_

Result:
case cons.e_a
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun t => (s - t, t)) s.powerset
x : Multiset α
hx : x ∈ s.powerset
⊢ (a ::ₘ (s - x), x) = (a ::ₘ s - x, x)

Proof state:
case empty
α : Type u_1
inst✝ : DecidableEq α
⊢ antidiagonal 0 = map (fun t => (0 - t, t)) (powerset 0)

Tactic:
simp only [antidiagonal_zero, powerset_zero, Multiset.zero_sub, map_singleton]

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun t => (s - t, t)) s.powerset
⊢ map (fun x => (s - x, a ::ₘ x)) s.powerset + map (fun x => (a ::ₘ (s - x), x)) s.powerset =
    map (fun x => (a ::ₘ s - x, x)) s.powerset + map (fun x => (s - x, a ::ₘ x)) s.powerset

Tactic:
rw [add_comm]

Result:
case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun t => (s - t, t)) s.powerset
⊢ map (fun x => (a ::ₘ (s - x), x)) s.powerset + map (fun x => (s - x, a ::ₘ x)) s.powerset =
    map (fun x => (a ::ₘ s - x, x)) s.powerset + map (fun x => (s - x, a ::ₘ x)) s.powerset