-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
@[to_additive]
lemma prod_map_ite (p : α → Prop) [DecidablePred p] (f g : α → M) (l : List α) :
    (l.map fun a => if p a then f a else g a).prod =
      ((l.filter p).map f).prod * ((l.filter fun a ↦ ¬p a).map g).prod

Proof state:
case neg
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
hx : ¬p x
⊢ (if p x then f x else g x) *
      ((map f (filter (fun b => decide (p b)) xs)).prod * (map g (filter (fun a => decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun b => decide (p b)) xs
          else filter (fun b => decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a => decide ¬p a) xs
          else filter (fun a => decide ¬p a) xs)).prod

Tactic:
simp only [hx, ↓reduceIte, decide_not, decide_false, Bool.false_eq_true, not_false_eq_true,
decide_true, map_cons, prod_cons, mul_left_comm]

Result:
no goals

Proof state:
case cons
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
ih :
  (map (fun a => if p a then f a else g a) xs).prod =
    (map f (filter (fun b => decide (p b)) xs)).prod * (map g (filter (fun a => decide ¬p a) xs)).prod
⊢ (if p x then f x else g x) *
      ((map f (filter (fun b => decide (p b)) xs)).prod * (map g (filter (fun a => decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun b => decide (p b)) xs
          else filter (fun b => decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a => decide ¬p a) xs
          else filter (fun a => decide ¬p a) xs)).prod

Tactic:
clear ih

Result:
case cons
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
⊢ (if p x then f x else g x) *
      ((map f (filter (fun b => decide (p b)) xs)).prod * (map g (filter (fun a => decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun b => decide (p b)) xs
          else filter (fun b => decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a => decide ¬p a) xs
          else filter (fun a => decide ¬p a) xs)).prod

Proof state:
case cons
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
ih :
  (map (fun a => if p a then f a else g a) xs).prod =
    (map f (filter (fun b => decide (p b)) xs)).prod * (map g (filter (fun a => decide ¬p a) xs)).prod
⊢ (if p x then f x else g x) * (map (fun a => if p a then f a else g a) xs).prod =
    (map f
          (if decide (p x) = true then x :: filter (fun b => decide (p b)) xs
          else filter (fun b => decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a => decide ¬p a) xs
          else filter (fun a => decide ¬p a) xs)).prod

Tactic:
rw [ih]

Result:
case cons
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
ih :
  (map (fun a => if p a then f a else g a) xs).prod =
    (map f (filter (fun b => decide (p b)) xs)).prod * (map g (filter (fun a => decide ¬p a) xs)).prod
⊢ (if p x then f x else g x) *
      ((map f (filter (fun b => decide (p b)) xs)).prod * (map g (filter (fun a => decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun b => decide (p b)) xs
          else filter (fun b => decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a => decide ¬p a) xs
          else filter (fun a => decide ¬p a) xs)).prod

Proof state:
case cons
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
ih :
  (map (fun a => if p a then f a else g a) xs).prod =
    (map f (filter (fun b => decide (p b)) xs)).prod * (map g (filter (fun a => decide ¬p a) xs)).prod
⊢ (map (fun a => if p a then f a else g a) (x :: xs)).prod =
    (map f (filter (fun b => decide (p b)) (x :: xs))).prod * (map g (filter (fun a => decide ¬p a) (x :: xs))).prod

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

Result:
case cons
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
ih :
  (map (fun a => if p a then f a else g a) xs).prod =
    (map f (filter (fun b => decide (p b)) xs)).prod * (map g (filter (fun a => decide ¬p a) xs)).prod
⊢ (if p x then f x else g x) * (map (fun a => if p a then f a else g a) xs).prod =
    (map f
          (if decide (p x) = true then x :: filter (fun b => decide (p b)) xs
          else filter (fun b => decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a => decide ¬p a) xs
          else filter (fun a => decide ¬p a) xs)).prod

Proof state:
case pos
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
hx : p x
⊢ (if p x then f x else g x) *
      ((map f (filter (fun b => decide (p b)) xs)).prod * (map g (filter (fun a => decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun b => decide (p b)) xs
          else filter (fun b => decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a => decide ¬p a) xs
          else filter (fun a => decide ¬p a) xs)).prod

Tactic:
simp only [hx, ↓reduceIte, decide_not, decide_true, map_cons, prod_cons, not_true_eq_false,
  decide_false, Bool.false_eq_true, mul_assoc]

Result:
no goals

Proof state:
case cons
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
⊢ (if p x then f x else g x) *
      ((map f (filter (fun b => decide (p b)) xs)).prod * (map g (filter (fun a => decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun b => decide (p b)) xs
          else filter (fun b => decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a => decide ¬p a) xs
          else filter (fun a => decide ¬p a) xs)).prod

Tactic:
by_cases hx : p x

Result:
case pos
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
hx : p x
⊢ (if p x then f x else g x) *
      ((map f (filter (fun b => decide (p b)) xs)).prod * (map g (filter (fun a => decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun b => decide (p b)) xs
          else filter (fun b => decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a => decide ¬p a) xs
          else filter (fun a => decide ¬p a) xs)).prod

case neg
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
hx : ¬p x
⊢ (if p x then f x else g x) *
      ((map f (filter (fun b => decide (p b)) xs)).prod * (map g (filter (fun a => decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun b => decide (p b)) xs
          else filter (fun b => decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a => decide ¬p a) xs
          else filter (fun a => decide ¬p a) xs)).prod

Proof state:
case nil
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
⊢ (map (fun a => if p a then f a else g a) []).prod =
    (map f (filter (fun b => decide (p b)) [])).prod * (map g (filter (fun a => decide ¬p a) [])).prod

Tactic:
simp

Result:
no goals