[GOAL]
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
a : α
b : δ a
s : Finset α
hs : ¬a ∈ s
e₁ e₂ : (a : α) → a ∈ s → δ a
eq : cons s a b e₁ = cons s a b e₂
e : α
h : e ∈ a ::ₘ s.val
⊢ e ∈ insert a s
[PROOFSTEP]
simpa only [Multiset.mem_cons, mem_insert] using h
[GOAL]
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
a : α
b : δ a
s : Finset α
hs : ¬a ∈ s
e₁ e₂ : (a : α) → a ∈ s → δ a
eq : cons s a b e₁ = cons s a b e₂
e : α
h : e ∈ a ::ₘ s.val
⊢ e ∈ insert a s
[PROOFSTEP]
simpa only [Multiset.mem_cons, mem_insert] using h
[GOAL]
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
a : α
b : δ a
s : Finset α
hs : ¬a ∈ s
e₁ e₂ : (a : α) → a ∈ s → δ a
eq : cons s a b e₁ = cons s a b e₂
e : α
h : e ∈ a ::ₘ s.val
⊢ cons s a b e₁ e (_ : e ∈ insert a s) = cons s a b e₂ e (_ : e ∈ insert a s)
[PROOFSTEP]
rw [eq]
[GOAL]
α : 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)
[PROOFSTEP]
apply eq_of_veq
[GOAL]
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
[PROOFSTEP]
rw [← (pi (insert a s) t).2.dedup]
[GOAL]
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
[PROOFSTEP]
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)
[GOAL]
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)))
[PROOFSTEP]
subst s'
[GOAL]
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)))
[PROOFSTEP]
rw [pi_cons]
[GOAL]
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)))
[PROOFSTEP]
congr
[GOAL]
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))
[PROOFSTEP]
funext b
[GOAL]
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))
[PROOFSTEP]
exact ((pi s t).nodup.map <| Multiset.Pi.cons_injective ha).dedup.symm
[GOAL]
α : Type u_1
β✝ : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
⊢ (pi s fun a => {f a}) = {fun a x => f a}
[PROOFSTEP]
rw [eq_singleton_iff_unique_mem]
[GOAL]
α : Type u_1
β✝ : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
⊢ ((fun a x => f a) ∈ pi s fun a => {f a}) ∧ ∀ (x : (a : α) → a ∈ s → β), (x ∈ pi s fun a => {f a}) → x = fun a x => f a
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u_1
β✝ : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
⊢ (fun a x => f a) ∈ pi s fun a => {f a}
[PROOFSTEP]
simp
[GOAL]
case right
α : Type u_1
β✝ : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
⊢ ∀ (x : (a : α) → a ∈ s → β), (x ∈ pi s fun a => {f a}) → x = fun a x => f a
[PROOFSTEP]
intro a ha
[GOAL]
case right
α : Type u_1
β✝ : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
a : (a : α) → a ∈ s → β
ha : a ∈ pi s fun a => {f a}
⊢ a = fun a x => f a
[PROOFSTEP]
ext i hi
[GOAL]
case right.h.h
α : Type u_1
β✝ : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
a : (a : α) → a ∈ s → β
ha : a ∈ pi s fun a => {f a}
i : α
hi : i ∈ s
⊢ a i hi = f i
[PROOFSTEP]
rw [mem_pi] at ha 
[GOAL]
case right.h.h
α : Type u_1
β✝ : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
a : (a : α) → a ∈ s → β
ha : ∀ (a_1 : α) (h : a_1 ∈ s), a a_1 h ∈ {f a_1}
i : α
hi : i ∈ s
⊢ a i hi = f i
[PROOFSTEP]
simpa using ha i hi
