-- Mathlib/Data/Multiset/Antidiagonal.lean
theorem antidiagonal_cons (a : α) (s) :
    antidiagonal (a ::ₘ s) =
      map (Prod.map id (cons a)) (antidiagonal s) + map (Prod.map (cons a) id) (antidiagonal s) :=
  Quotient.inductionOn s fun l ↦ by
    simp only [revzip, reverse_append, quot_mk_to_coe, coe_eq_coe, powersetAux'_cons, cons_coe,
      map_coe, antidiagonal_coe', coe_add]
    rw [← zip_map, ← zip_map, zip_append, (_ : _ ++ _ = _)]
    · congr
      · simp only [List.map_id]
      · rw [map_reverse]
      · simp
    · simp

Proof state:
case e_a.e_a
α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (List.map (cons a) (powersetAux' l)).reverse = List.map (cons a) (powersetAux' l).reverse

Tactic:
rw [map_reverse]

Result:
no goals

Proof state:
α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (a ::ₘ ⟦l⟧).antidiagonal =
    map (Prod.map id (cons a)) (antidiagonal ⟦l⟧) + map (Prod.map (cons a) id) (antidiagonal ⟦l⟧)

Tactic:
simp only [revzip, reverse_append, quot_mk_to_coe, coe_eq_coe, powersetAux'_cons, cons_coe,
  map_coe, antidiagonal_coe', coe_add]

Result:
α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (powersetAux' l ++ List.map (cons a) (powersetAux' l)).zip
      ((List.map (cons a) (powersetAux' l)).reverse ++ (powersetAux' l).reverse) ~
    List.map (fun x => Prod.map id (cons a) x) ((powersetAux' l).zip (powersetAux' l).reverse) ++
      List.map (fun x => Prod.map (cons a) id x) ((powersetAux' l).zip (powersetAux' l).reverse)

Proof state:
α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (powersetAux' l).length = (List.map (cons a) (powersetAux' l)).reverse.length

Tactic:
simp

Result:
no goals

Proof state:
case e_a.e_a
α : Type u_1
a : α
s : Multiset α
l : List α
⊢ powersetAux' l = List.map id (powersetAux' l)

Tactic:
simp only [List.map_id]

Result:
no goals

Proof state:
case e_a.e_a
α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (powersetAux' l).reverse = List.map id (powersetAux' l).reverse

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (powersetAux' l ++ List.map (cons a) (powersetAux' l)).zip
      ((List.map (cons a) (powersetAux' l)).reverse ++ (powersetAux' l).reverse) ~
    List.map (fun x => Prod.map id (cons a) x) ((powersetAux' l).zip (powersetAux' l).reverse) ++
      List.map (fun x => Prod.map (cons a) id x) ((powersetAux' l).zip (powersetAux' l).reverse)

Tactic:
rw [← zip_map, ← zip_map, zip_append, (_ : _ ++ _ = _)]

Result:
α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (powersetAux' l).zip (List.map (cons a) (powersetAux' l)).reverse ++
      (List.map (cons a) (powersetAux' l)).zip (powersetAux' l).reverse =
    (List.map id (powersetAux' l)).zip (List.map (cons a) (powersetAux' l).reverse) ++
      (List.map (cons a) (powersetAux' l)).zip (List.map id (powersetAux' l).reverse)

α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (powersetAux' l).length = (List.map (cons a) (powersetAux' l)).reverse.length

Proof state:
α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (powersetAux' l).zip (List.map (cons a) (powersetAux' l)).reverse ++
      (List.map (cons a) (powersetAux' l)).zip (powersetAux' l).reverse =
    (List.map id (powersetAux' l)).zip (List.map (cons a) (powersetAux' l).reverse) ++
      (List.map (cons a) (powersetAux' l)).zip (List.map id (powersetAux' l).reverse)

Tactic:
congr

Result:
case e_a.e_a
α : Type u_1
a : α
s : Multiset α
l : List α
⊢ powersetAux' l = List.map id (powersetAux' l)

case e_a.e_a
α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (List.map (cons a) (powersetAux' l)).reverse = List.map (cons a) (powersetAux' l).reverse

case e_a.e_a
α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (powersetAux' l).reverse = List.map id (powersetAux' l).reverse