α : Type u_1
β : Type ?u.9087
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)))
α : Type u_1
β : Type ?u.9087
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))
simp only [revzip, reverse_append, quot_mk_to_coe, coe_eq_coe, powersetAux'_cons, cons_coe,
  coe_map, antidiagonal_coe', coe_add]
α : Type u_1
β : Type ?u.9087
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)))

α : Type u_1
β : Type ?u.9087
a : α
s : Multiset α
l : List α
⊢ length (powersetAux' l) = length (reverse (List.map (cons a) (powersetAux' l)))
α : Type u_1
β : Type ?u.9087
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)))
rw [← zip_map, ← zip_map, zip_append, (_ : _ ++ _ = _)]
case e_a.e_a
α : Type u_1
β : Type ?u.9087
a : α
s : Multiset α
l : List α
⊢ powersetAux' l = List.map id (powersetAux' l)

case e_a.e_a
α : Type u_1
β : Type ?u.9087
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.9087
a : α
s : Multiset α
l : List α
⊢ reverse (powersetAux' l) = List.map id (reverse (powersetAux' l))
α : Type u_1
β : Type ?u.9087
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)))
congr
case e_a.e_a
α : Type u_1
β : Type ?u.9087
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.9087
a : α
s : Multiset α
l : List α
⊢ reverse (powersetAux' l) = List.map id (reverse (powersetAux' l))
case e_a.e_a
α : Type u_1
β : Type ?u.9087
a : α
s : Multiset α
l : List α
⊢ powersetAux' l = List.map id (powersetAux' l)

case e_a.e_a
α : Type u_1
β : Type ?u.9087
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.9087
a : α
s : Multiset α
l : List α
⊢ reverse (powersetAux' l) = List.map id (reverse (powersetAux' l))
simp
case e_a.e_a
α : Type u_1
β : Type ?u.9087
a : α
s : Multiset α
l : List α
⊢ reverse (powersetAux' l) = List.map id (reverse (powersetAux' l))
case e_a.e_a
α : Type u_1
β : Type ?u.9087
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.9087
a : α
s : Multiset α
l : List α
⊢ reverse (powersetAux' l) = List.map id (reverse (powersetAux' l))
rw [map_reverse]
no goals
case e_a.e_a
α : Type u_1
β : Type ?u.9087
a : α
s : Multiset α
l : List α
⊢ reverse (powersetAux' l) = List.map id (reverse (powersetAux' l))
simp
no goals
α : Type u_1
β : Type ?u.9087
a : α
s : Multiset α
l : List α
⊢ length (powersetAux' l) = length (reverse (List.map (cons a) (powersetAux' l)))
simp