-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
@[to_additive]
lemma prod_map_eq_pow_single [DecidableEq α] {l : List α} (a : α) (f : α → M)
    (hf : ∀ a', a' ≠ a → a' ∈ l → f a' = 1) : (l.map f).prod = f a ^ l.count a

Proof state:
case cons
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : (map f as).prod = f a ^ count a as
⊢ f a' * f a ^ count a as = f a ^ (count a as + if a' = a then 1 else 0)

Tactic:
split_ifs with ha'

Result:
case pos
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : (map f as).prod = f a ^ count a as
ha' : a' = a
⊢ f a' * f a ^ count a as = f a ^ (count a as + 1)

case neg
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : (map f as).prod = f a ^ count a as
ha' : ¬a' = a
⊢ f a' * f a ^ count a as = f a ^ (count a as + 0)

Proof state:
case cons
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : (map f as).prod = f a ^ count a as
⊢ (map f (a' :: as)).prod = f a ^ count a (a' :: as)

Tactic:
rw [List.map_cons, List.prod_cons, count_cons, h]

Result:
case cons
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : (map f as).prod = f a ^ count a as
⊢ f a' * f a ^ count a as = f a ^ (count a as + if (a' == a) = true then 1 else 0)

Proof state:
case neg
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : (map f as).prod = f a ^ count a as
ha' : ¬a' = a
⊢ f a' * f a ^ count a as = f a ^ (count a as + 0)

Tactic:
rw [hf a' ha' (List.mem_cons_self a' as), one_mul, add_zero]

Result:
no goals

Proof state:
case cons
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : (map f as).prod = f a ^ count a as
⊢ f a' * f a ^ count a as = f a ^ (count a as + if (a' == a) = true then 1 else 0)

Tactic:
simp only [beq_iff_eq]

Result:
case cons
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : (map f as).prod = f a ^ count a as
⊢ f a' * f a ^ count a as = f a ^ (count a as + if a' = a then 1 else 0)

Proof state:
case nil
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a : α
hf : ∀ (a' : α), a' ≠ a → a' ∈ [] → f a' = 1
⊢ (map f []).prod = f a ^ count a []

Tactic:
rw [map_nil, prod_nil, count_nil, _root_.pow_zero]

Result:
no goals

Proof state:
case cons
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
h : ∀ (a : α), (∀ (a' : α), a' ≠ a → a' ∈ as → f a' = 1) → (map f as).prod = f a ^ count a as
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
⊢ (map f (a' :: as)).prod = f a ^ count a (a' :: as)

Tactic:
specialize h a fun a' ha' hfa' => hf a' ha' (mem_cons_of_mem _ hfa')

Result:
case cons
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : (map f as).prod = f a ^ count a as
⊢ (map f (a' :: as)).prod = f a ^ count a (a' :: as)

Proof state:
case pos
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : (map f as).prod = f a ^ count a as
ha' : a' = a
⊢ f a' * f a ^ count a as = f a ^ (count a as + 1)

Tactic:
rw [ha', _root_.pow_succ']

Result:
no goals