-- Mathlib/Data/Finset/Pi.lean
theorem pi_insert [∀ a, DecidableEq (β a)] {s : Finset α} {t : ∀ a : α, Finset (β a)} {a : α}
    (ha : a ∉ s) : pi (insert a s) t = (t a).biUnion fun b => (pi s t).image (Pi.cons s a b)

Proof state:
α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ (insert a s).pi t = (t a).biUnion fun b => image (Pi.cons s a b) (s.pi t)

Tactic:
apply eq_of_veq

Result:
case a
α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ ((insert a s).pi t).val = ((t a).biUnion fun b => image (Pi.cons s a b) (s.pi t)).val

Proof state:
case a
α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
s' : Multiset α
h : s' = a ::ₘ s.val
⊢ (s'.pi fun a => (t a).val).dedup =
    ((t a).val.bind fun b =>
        (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a => (t a).val)).dedup).dedup

Tactic:
subst s'

Result:
case a
α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ ((a ::ₘ s.val).pi fun a => (t a).val).dedup =
    ((t a).val.bind fun b =>
        (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a => (t a).val)).dedup).dedup

Proof state:
case a
α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ ((insert a s).pi t).val.dedup = ((t a).biUnion fun b => image (Pi.cons s a b) (s.pi t)).val

Tactic:
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)

Result:
case a
α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
s' : Multiset α
h : s' = a ::ₘ s.val
⊢ (s'.pi fun a => (t a).val).dedup =
    ((t a).val.bind fun b =>
        (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a => (t a).val)).dedup).dedup

Proof state:
case a
α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ ((a ::ₘ s.val).pi fun a => (t a).val).dedup =
    ((t a).val.bind fun b =>
        (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a => (t a).val)).dedup).dedup

Tactic:
rw [pi_cons]

Result:
case a
α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ ((t a).val.bind fun b => Multiset.map (Multiset.Pi.cons s.val a b) (s.val.pi fun a => (t a).val)).dedup =
    ((t a).val.bind fun b =>
        (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a => (t a).val)).dedup).dedup

Proof state:
case a.e_s.e_f
α : Type u_1
β : α → Type u
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) (s.val.pi fun a => (t a).val)) = fun b =>
    (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a => (t a).val)).dedup

Tactic:
funext b

Result:
case a.e_s.e_f.h
α : Type u_1
β : α → Type u
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) (s.val.pi fun a => (t a).val) =
    (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a => (t a).val)).dedup

Proof state:
case a
α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ ((t a).val.bind fun b => Multiset.map (Multiset.Pi.cons s.val a b) (s.val.pi fun a => (t a).val)).dedup =
    ((t a).val.bind fun b =>
        (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a => (t a).val)).dedup).dedup

Tactic:
congr

Result:
case a.e_s.e_f
α : Type u_1
β : α → Type u
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) (s.val.pi fun a => (t a).val)) = fun b =>
    (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a => (t a).val)).dedup

Proof state:
case a.e_s.e_f.h
α : Type u_1
β : α → Type u
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) (s.val.pi fun a => (t a).val) =
    (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a => (t a).val)).dedup

Tactic:
exact ((pi s t).nodup.map <| Multiset.Pi.cons_injective ha).dedup.symm

Result:
no goals

Proof state:
case a
α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ ((insert a s).pi t).val = ((t a).biUnion fun b => image (Pi.cons s a b) (s.pi t)).val

Tactic:
rw [← (pi (insert a s) t).2.dedup]

Result:
case a
α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ ((insert a s).pi t).val.dedup = ((t a).biUnion fun b => image (Pi.cons s a b) (s.pi t)).val