-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_list_map_count [DecidableEq α] (l : List α) {M : Type*} [CommMonoid M] (f : α → M) :
    (l.map f).prod = ∏ m ∈ l.toFinset, f m ^ l.count m

Proof state:
case nil
α : Type u_3
inst✝¹ : DecidableEq α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
⊢ (List.map f []).prod = ∏ m ∈ [].toFinset, f m ^ count m []

Tactic:
simp only [map_nil, prod_nil, count_nil, pow_zero, prod_const_one]

Result:
no goals

Proof state:
case cons
α : Type u_3
inst✝¹ : DecidableEq α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
⊢ f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)

Tactic:
by_cases has : a ∈ s.toFinset

Result:
case pos
α : Type u_3
inst✝¹ : DecidableEq α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
⊢ f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)

case neg
α : Type u_3
inst✝¹ : DecidableEq α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∉ s.toFinset
⊢ f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)

Proof state:
case neg
α : Type u_3
inst✝¹ : DecidableEq α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∉ s.toFinset
⊢ f a * ∏ m ∈ s.toFinset, f m ^ count m s = f a * ∏ x ∈ s.toFinset, f x ^ count x (a :: s)

Tactic:
congr 1

Result:
case neg.e_a
α : Type u_3
inst✝¹ : DecidableEq α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∉ s.toFinset
⊢ ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ s.toFinset, f x ^ count x (a :: s)

Proof state:
case cons
α : Type u_3
inst✝¹ : DecidableEq α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
⊢ (List.map f (a :: s)).prod = ∏ m ∈ (a :: s).toFinset, f m ^ count m (a :: s)

Tactic:
simp only [List.map, List.prod_cons, toFinset_cons, IH]

Result:
case cons
α : Type u_3
inst✝¹ : DecidableEq α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
⊢ f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)

Proof state:
case neg.e_a
α : Type u_3
inst✝¹ : DecidableEq α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∉ s.toFinset
x : α
hx : x ∈ s.toFinset
⊢ f x ^ count x s = f x ^ count x (a :: s)

Tactic:
rw [count_cons_of_ne]

Result:
case neg.e_a.h
α : Type u_3
inst✝¹ : DecidableEq α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∉ s.toFinset
x : α
hx : x ∈ s.toFinset
⊢ x ≠ a

Proof state:
case neg
α : Type u_3
inst✝¹ : DecidableEq α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∉ s.toFinset
⊢ f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)

Tactic:
rw [prod_insert has, count_cons_self, count_eq_zero_of_not_mem (mt mem_toFinset.2 has), pow_one]

Result:
case neg
α : Type u_3
inst✝¹ : DecidableEq α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∉ s.toFinset
⊢ f a * ∏ m ∈ s.toFinset, f m ^ count m s = f a * ∏ x ∈ s.toFinset, f x ^ count x (a :: s)

Proof state:
case pos.e_a
α : Type u_3
inst✝¹ : DecidableEq α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
x : α
hx : x ∈ s.toFinset.erase a
⊢ f x ^ count x s = f x ^ count x (a :: s)

Tactic:
rw [count_cons_of_ne (ne_of_mem_erase hx)]

Result:
no goals

Proof state:
case pos
α : Type u_3
inst✝¹ : DecidableEq α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
⊢ f a * f a ^ count a s * ∏ x ∈ s.toFinset.erase a, f x ^ count x s =
    f a * f a ^ count a s * ∏ x ∈ s.toFinset.erase a, f x ^ count x (a :: s)

Tactic:
congr 1

Result:
case pos.e_a
α : Type u_3
inst✝¹ : DecidableEq α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
⊢ ∏ x ∈ s.toFinset.erase a, f x ^ count x s = ∏ x ∈ s.toFinset.erase a, f x ^ count x (a :: s)

Proof state:
case neg.e_a
α : Type u_3
inst✝¹ : DecidableEq α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∉ s.toFinset
⊢ ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ s.toFinset, f x ^ count x (a :: s)

Tactic:
refine prod_congr rfl fun x hx => ?_

Result:
case neg.e_a
α : Type u_3
inst✝¹ : DecidableEq α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∉ s.toFinset
x : α
hx : x ∈ s.toFinset
⊢ f x ^ count x s = f x ^ count x (a :: s)

Proof state:
case neg.e_a.h
α : Type u_3
inst✝¹ : DecidableEq α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∉ s.toFinset
x : α
hx : x ∈ s.toFinset
⊢ x ≠ a

Tactic:
rintro rfl

Result:
case neg.e_a.h
α : Type u_3
inst✝¹ : DecidableEq α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
s : List α
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
x : α
hx : x ∈ s.toFinset
has : x ∉ s.toFinset
⊢ False

Proof state:
case pos
α : Type u_3
inst✝¹ : DecidableEq α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
⊢ f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)

Tactic:
rw [insert_eq_of_mem has, ← insert_erase has, prod_insert (not_mem_erase _ _),
  prod_insert (not_mem_erase _ _), ← mul_assoc, count_cons_self, pow_succ']

Result:
case pos
α : Type u_3
inst✝¹ : DecidableEq α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
⊢ f a * f a ^ count a s * ∏ x ∈ s.toFinset.erase a, f x ^ count x s =
    f a * f a ^ count a s * ∏ x ∈ s.toFinset.erase a, f x ^ count x (a :: s)

Proof state:
case neg.e_a.h
α : Type u_3
inst✝¹ : DecidableEq α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
s : List α
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
x : α
hx : x ∈ s.toFinset
has : x ∉ s.toFinset
⊢ False

Tactic:
exact has hx

Result:
no goals

Proof state:
case pos.e_a
α : Type u_3
inst✝¹ : DecidableEq α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
⊢ ∏ x ∈ s.toFinset.erase a, f x ^ count x s = ∏ x ∈ s.toFinset.erase a, f x ^ count x (a :: s)

Tactic:
refine prod_congr rfl fun x hx => ?_

Result:
case pos.e_a
α : Type u_3
inst✝¹ : DecidableEq α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
x : α
hx : x ∈ s.toFinset.erase a
⊢ f x ^ count x s = f x ^ count x (a :: s)