case a
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : ¬a ∈ s
⊢ (pi (insert a s) t).val = (Finset.biUnion (t a) fun b => image (Pi.cons s a b) (pi s t)).val
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : ¬a ∈ s
⊢ pi (insert a s) t = Finset.biUnion (t a) fun b => image (Pi.cons s a b) (pi s t)
apply eq_of_veq
case a
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : ¬a ∈ s
⊢ dedup (pi (insert a s) t).val = (Finset.biUnion (t a) fun b => image (Pi.cons s a b) (pi s t)).val
case a
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : ¬a ∈ s
⊢ (pi (insert a s) t).val = (Finset.biUnion (t a) fun b => image (Pi.cons s a b) (pi s t)).val
rw [← (pi (insert a s) t).2.dedup]
case a
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : ¬a ∈ s
s' : Multiset α
h : s' = a ::ₘ s.val
⊢ dedup (Multiset.pi s' fun a => (t a).val) =
    dedup
      (Multiset.bind (t a).val fun b =>
        dedup
          (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' (_ : a' ∈ a ::ₘ s.val))
            (Multiset.pi s.val fun a => (t a).val)))
case a
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : ¬a ∈ s
⊢ dedup (pi (insert a s) t).val = (Finset.biUnion (t a) fun b => image (Pi.cons s a b) (pi s t)).val
refine'
  (fun s' (h : s' = a ::ₘ s.1) =>
      (_ :
        dedup (Multiset.pi s' fun a => (t a).1) =
          dedup
            ((t a).1.bind fun b =>
              dedup <|
                (Multiset.pi s.1 fun a : α => (t a).val).map fun f a' h' =>
                  Multiset.Pi.cons s.1 a b f a' (h ▸ h'))))
    _ (insert_val_of_not_mem ha)
case a
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : ¬a ∈ s
⊢ dedup (Multiset.pi (a ::ₘ s.val) fun a => (t a).val) =
    dedup
      (Multiset.bind (t a).val fun b =>
        dedup
          (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' (_ : a' ∈ a ::ₘ s.val))
            (Multiset.pi s.val fun a => (t a).val)))
case a
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : ¬a ∈ s
s' : Multiset α
h : s' = a ::ₘ s.val
⊢ dedup (Multiset.pi s' fun a => (t a).val) =
    dedup
      (Multiset.bind (t a).val fun b =>
        dedup
          (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' (_ : a' ∈ a ::ₘ s.val))
            (Multiset.pi s.val fun a => (t a).val)))
subst s'
case a
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : ¬a ∈ s
⊢ dedup
      (Multiset.bind (t a).val fun b =>
        Multiset.map (Multiset.Pi.cons s.val a b) (Multiset.pi s.val fun a => (t a).val)) =
    dedup
      (Multiset.bind (t a).val fun b =>
        dedup
          (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' (_ : a' ∈ a ::ₘ s.val))
            (Multiset.pi s.val fun a => (t a).val)))
case a
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : ¬a ∈ s
⊢ dedup (Multiset.pi (a ::ₘ s.val) fun a => (t a).val) =
    dedup
      (Multiset.bind (t a).val fun b =>
        dedup
          (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' (_ : a' ∈ a ::ₘ s.val))
            (Multiset.pi s.val fun a => (t a).val)))
rw [pi_cons]
case a.e_s.e_f
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : ¬a ∈ s
⊢ (fun b => Multiset.map (Multiset.Pi.cons s.val a b) (Multiset.pi s.val fun a => (t a).val)) = fun b =>
    dedup
      (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' (_ : a' ∈ a ::ₘ s.val))
        (Multiset.pi s.val fun a => (t a).val))
case a
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : ¬a ∈ s
⊢ dedup
      (Multiset.bind (t a).val fun b =>
        Multiset.map (Multiset.Pi.cons s.val a b) (Multiset.pi s.val fun a => (t a).val)) =
    dedup
      (Multiset.bind (t a).val fun b =>
        dedup
          (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' (_ : a' ∈ a ::ₘ s.val))
            (Multiset.pi s.val fun a => (t a).val)))
congr
case a.e_s.e_f.h
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : ¬a ∈ s
b : β a
⊢ Multiset.map (Multiset.Pi.cons s.val a b) (Multiset.pi s.val fun a => (t a).val) =
    dedup
      (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' (_ : a' ∈ a ::ₘ s.val))
        (Multiset.pi s.val fun a => (t a).val))
case a.e_s.e_f
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : ¬a ∈ s
⊢ (fun b => Multiset.map (Multiset.Pi.cons s.val a b) (Multiset.pi s.val fun a => (t a).val)) = fun b =>
    dedup
      (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' (_ : a' ∈ a ::ₘ s.val))
        (Multiset.pi s.val fun a => (t a).val))
funext b
no goals
case a.e_s.e_f.h
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : ¬a ∈ s
b : β a
⊢ Multiset.map (Multiset.Pi.cons s.val a b) (Multiset.pi s.val fun a => (t a).val) =
    dedup
      (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' (_ : a' ∈ a ::ₘ s.val))
        (Multiset.pi s.val fun a => (t a).val))
exact ((pi s t).nodup.map <| Multiset.Pi.cons_injective ha).dedup.symm