Theorem: List.prod_map_ite_eq (FormalSnarksProject/ToMathlib/ForTransformations.lean)

State before:
case nil
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
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
State after:
no goals

State before:
case cons
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
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] at ih ⊢
State after:
case cons
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
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 (x :: xs) * (g x * (map g xs).prod)

State before:
case cons
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
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 (x :: xs) * (g x * (map g xs).prod)
Tactic:
rw [ih]
State after:
case cons
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
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 (x :: xs) * (g x * (map g xs).prod)

State before:
case cons
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
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 (x :: xs) * (g x * (map g xs).prod)
Tactic:
clear ih
State after:
case cons
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
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 (x :: xs) * (g x * (map g xs).prod)

State before:
case cons
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
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 (x :: xs) * (g x * (map g xs).prod)
Tactic:
rw [List.count_cons]
State after:
case cons
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
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 a = x then 1 else 0) * (g x * (map g xs).prod)

State before:
case cons
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
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 a = x then 1 else 0) * (g x * (map g xs).prod)
Tactic:
by_cases hx : x = a
State after:
case pos
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
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 a = x then 1 else 0) * (g x * (map g xs).prod)

case neg
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
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 a = x then 1 else 0) * (g x * (map g xs).prod)

State before:
case pos
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
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 a = x then 1 else 0) * (g x * (map g xs).prod)
Tactic:
simp [hx, ite_true, pow_add]
State after:
case pos
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : x = a
⊢ f a * (f a ^ count a xs / g a ^ count a xs * (map g xs).prod) =
    f a ^ count a xs / g a ^ count a xs * (f a / g a) * (g a * (map g xs).prod)

State before:
case pos
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : x = a
⊢ f a * (f a ^ count a xs / g a ^ count a xs * (map g xs).prod) =
    f a ^ count a xs / g a ^ count a xs * (f a / g a) * (g a * (map g xs).prod)
Tactic:
simp only [mul_assoc, mul_comm (f a / g a) _, mul_comm (f a) _]
State after:
case pos
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : x = a
⊢ f a ^ count a xs / g a ^ count a xs * ((map g xs).prod * f a) =
    f a ^ count a xs / g a ^ count a xs * (g a * ((map g xs).prod * (f a / g a)))

State before:
case pos
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : x = a
⊢ f a ^ count a xs / g a ^ count a xs * ((map g xs).prod * f a) =
    f a ^ count a xs / g a ^ count a xs * (g a * ((map g xs).prod * (f a / g a)))
Tactic:
simp only [mul_right_inj]
State after:
case pos
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : x = a
⊢ (map g xs).prod * f a = g a * ((map g xs).prod * (f a / g a))

State before:
case pos
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : x = a
⊢ (map g xs).prod * f a = g a * ((map g xs).prod * (f a / g a))
Tactic:
simp only [mul_assoc, mul_comm (g a) _]
State after:
case pos
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : x = a
⊢ (map g xs).prod * f a = (map g xs).prod * (f a / g a * g a)

State before:
case pos
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : x = a
⊢ (map g xs).prod * f a = (map g xs).prod * (f a / g a * g a)
Tactic:
simp only [mul_right_inj]
State after:
case pos
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : x = a
⊢ f a = f a / g a * g a

State before:
case pos
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : x = a
⊢ f a = f a / g a * g a
Tactic:
simp only [div_mul_cancel]
State after:
no goals

State before:
case neg
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
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 a = x then 1 else 0) * (g x * (map g xs).prod)
Tactic:
simp only [hx, ite_false, ne_comm.mp hx, add_zero]
State after:
case neg
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : ¬x = a
⊢ g x * ((f a / g a) ^ count a xs * (map g xs).prod) = (f a / g a) ^ count a xs * (g x * (map g xs).prod)

State before:
case neg
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : ¬x = a
⊢ g x * ((f a / g a) ^ count a xs * (map g xs).prod) = (f a / g a) ^ count a xs * (g x * (map g xs).prod)
Tactic:
simp only [mul_assoc, mul_comm (g x) _]
State after:
no goals