-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
@[to_additive]
lemma prod_map_ite_eq {A : Type*} [DecidableEq A] (l : List A) (f g : A → G) (a : A) :
    (l.map fun x => if x = a then f x else g x).prod
      = (f a / g a) ^ (l.count a) * (l.map g).prod

Proof state:
case cons
G : Type u_7
inst✝¹ : CommGroup G
A : Type u_8
inst✝ : DecidableEq A
f g : A → G
a x : A
xs : List A
ih : (map (fun x => if x = a then f x else g x) xs).prod = (f a / g a) ^ count a xs * (map g xs).prod
⊢ (map (fun x => if x = a then f x else g x) (x :: xs)).prod = (f a / g a) ^ count a (x :: xs) * (map g (x :: xs)).prod

Tactic:
simp only [map_cons, prod_cons, nodup_cons, ne_eq, mem_cons, count_cons] at ih ⊢

Result:
case cons
G : Type u_7
inst✝¹ : CommGroup G
A : Type u_8
inst✝ : DecidableEq A
f g : A → G
a x : A
xs : List A
ih : (map (fun x => if x = a then f x else g x) xs).prod = (f a / g a) ^ count a xs * (map g xs).prod
⊢ (if x = a then f x else g x) * (map (fun x => if x = a then f x else g x) xs).prod =
    (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)

Proof state:
case pos
G : Type u_7
inst✝¹ : CommGroup G
A : Type u_8
inst✝ : DecidableEq A
f g : A → G
a x : A
xs : List A
hx : x = a
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)

Tactic:
simp only [hx, ite_true, div_pow, pow_add, pow_one, div_eq_mul_inv, mul_assoc, mul_comm,
  mul_left_comm, mul_inv_cancel_left, beq_self_eq_true]

Result:
no goals

Proof state:
case cons
G : Type u_7
inst✝¹ : CommGroup G
A : Type u_8
inst✝ : DecidableEq A
f g : A → G
a x : A
xs : List A
ih : (map (fun x => if x = a then f x else g x) xs).prod = (f a / g a) ^ count a xs * (map g xs).prod
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)

Tactic:
clear ih

Result:
case cons
G : Type u_7
inst✝¹ : CommGroup G
A : Type u_8
inst✝ : DecidableEq A
f g : A → G
a x : A
xs : List A
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)

Proof state:
case neg
G : Type u_7
inst✝¹ : CommGroup G
A : Type u_8
inst✝ : DecidableEq A
f g : A → G
a x : A
xs : List A
hx : ¬x = a
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)

Tactic:
simp only [hx, ite_false, ne_comm.mp hx, add_zero, mul_assoc, mul_comm (g x) _, beq_iff_eq]

Result:
no goals

Proof state:
case nil
G : Type u_7
inst✝¹ : CommGroup G
A : Type u_8
inst✝ : DecidableEq A
f g : A → G
a : A
⊢ (map (fun x => if x = a then f x else g x) []).prod = (f a / g a) ^ count a [] * (map g []).prod

Tactic:
simp

Result:
no goals

Proof state:
case cons
G : Type u_7
inst✝¹ : CommGroup G
A : Type u_8
inst✝ : DecidableEq A
f g : A → G
a x : A
xs : List A
ih : (map (fun x => if x = a then f x else g x) xs).prod = (f a / g a) ^ count a xs * (map g xs).prod
⊢ (if x = a then f x else g x) * (map (fun x => if x = a then f x else g x) xs).prod =
    (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)

Tactic:
rw [ih]

Result:
case cons
G : Type u_7
inst✝¹ : CommGroup G
A : Type u_8
inst✝ : DecidableEq A
f g : A → G
a x : A
xs : List A
ih : (map (fun x => if x = a then f x else g x) xs).prod = (f a / g a) ^ count a xs * (map g xs).prod
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)

Proof state:
case cons
G : Type u_7
inst✝¹ : CommGroup G
A : Type u_8
inst✝ : DecidableEq A
f g : A → G
a x : A
xs : List A
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)

Tactic:
by_cases hx : x = a

Result:
case pos
G : Type u_7
inst✝¹ : CommGroup G
A : Type u_8
inst✝ : DecidableEq A
f g : A → G
a x : A
xs : List A
hx : x = a
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)

case neg
G : Type u_7
inst✝¹ : CommGroup G
A : Type u_8
inst✝ : DecidableEq A
f g : A → G
a x : A
xs : List A
hx : ¬x = a
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)