case nil
ι : Type ?u.450788
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
⊢ prod (List.map f []) = ∏ m in toFinset [], f m ^ count m []

case cons
ι : Type ?u.450788
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : prod (List.map f s) = ∏ m in toFinset s, f m ^ count m s
⊢ prod (List.map f (a :: s)) = ∏ m in toFinset (a :: s), f m ^ count m (a :: s)
ι : Type ?u.450788
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
l : List α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
⊢ prod (List.map f l) = ∏ m in toFinset l, f m ^ count m l
induction' l with a s IH
case cons
ι : Type ?u.450788
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : prod (List.map f s) = ∏ m in toFinset s, f m ^ count m s
⊢ f a * ∏ m in toFinset s, f m ^ count m s = ∏ x in insert a (toFinset s), f x ^ count x (a :: s)
case cons
ι : Type ?u.450788
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : prod (List.map f s) = ∏ m in toFinset s, f m ^ count m s
⊢ prod (List.map f (a :: s)) = ∏ m in toFinset (a :: s), f m ^ count m (a :: s)
simp only [List.map, List.prod_cons, toFinset_cons, IH]
case pos
ι : Type ?u.450788
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : prod (List.map f s) = ∏ m in toFinset s, f m ^ count m s
has : a ∈ toFinset s
⊢ f a * ∏ m in toFinset s, f m ^ count m s = ∏ x in insert a (toFinset s), f x ^ count x (a :: s)

case neg
ι : Type ?u.450788
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : prod (List.map f s) = ∏ m in toFinset s, f m ^ count m s
has : ¬a ∈ toFinset s
⊢ f a * ∏ m in toFinset s, f m ^ count m s = ∏ x in insert a (toFinset s), f x ^ count x (a :: s)
case cons
ι : Type ?u.450788
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : prod (List.map f s) = ∏ m in toFinset s, f m ^ count m s
⊢ f a * ∏ m in toFinset s, f m ^ count m s = ∏ x in insert a (toFinset s), f x ^ count x (a :: s)
by_cases has : a ∈ s.toFinset
case neg
ι : Type ?u.450788
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : prod (List.map f s) = ∏ m in toFinset s, f m ^ count m s
has : ¬a ∈ toFinset s
⊢ f a * ∏ m in toFinset s, f m ^ count m s = f a * ∏ x in toFinset s, f x ^ count x (a :: s)
case neg
ι : Type ?u.450788
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : prod (List.map f s) = ∏ m in toFinset s, f m ^ count m s
has : ¬a ∈ toFinset s
⊢ f a * ∏ m in toFinset s, f m ^ count m s = ∏ x in insert a (toFinset s), f x ^ count x (a :: s)
rw [prod_insert has, count_cons_self, count_eq_zero_of_not_mem (mt mem_toFinset.2 has), pow_one]
case neg.e_a
ι : Type ?u.450788
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : prod (List.map f s) = ∏ m in toFinset s, f m ^ count m s
has : ¬a ∈ toFinset s
⊢ ∏ m in toFinset s, f m ^ count m s = ∏ x in toFinset s, f x ^ count x (a :: s)
case neg
ι : Type ?u.450788
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : prod (List.map f s) = ∏ m in toFinset s, f m ^ count m s
has : ¬a ∈ toFinset s
⊢ f a * ∏ m in toFinset s, f m ^ count m s = f a * ∏ x in toFinset s, f x ^ count x (a :: s)
congr 1
case neg.e_a
ι : Type ?u.450788
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : prod (List.map f s) = ∏ m in toFinset s, f m ^ count m s
has : ¬a ∈ toFinset s
x : α
hx : x ∈ toFinset s
⊢ f x ^ count x s = f x ^ count x (a :: s)
case neg.e_a
ι : Type ?u.450788
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : prod (List.map f s) = ∏ m in toFinset s, f m ^ count m s
has : ¬a ∈ toFinset s
⊢ ∏ m in toFinset s, f m ^ count m s = ∏ x in toFinset s, f x ^ count x (a :: s)
refine' prod_congr rfl fun x hx => _
case neg.e_a.h
ι : Type ?u.450788
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : prod (List.map f s) = ∏ m in toFinset s, f m ^ count m s
has : ¬a ∈ toFinset s
x : α
hx : x ∈ toFinset s
⊢ x ≠ a
case neg.e_a
ι : Type ?u.450788
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : prod (List.map f s) = ∏ m in toFinset s, f m ^ count m s
has : ¬a ∈ toFinset s
x : α
hx : x ∈ toFinset s
⊢ f x ^ count x s = f x ^ count x (a :: s)
rw [count_cons_of_ne]
case neg.e_a.h
ι : Type ?u.450788
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
s : List α
IH : prod (List.map f s) = ∏ m in toFinset s, f m ^ count m s
x : α
hx : x ∈ toFinset s
has : ¬x ∈ toFinset s
⊢ False
case neg.e_a.h
ι : Type ?u.450788
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : prod (List.map f s) = ∏ m in toFinset s, f m ^ count m s
has : ¬a ∈ toFinset s
x : α
hx : x ∈ toFinset s
⊢ x ≠ a
rintro rfl
no goals
case neg.e_a.h
ι : Type ?u.450788
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
s : List α
IH : prod (List.map f s) = ∏ m in toFinset s, f m ^ count m s
x : α
hx : x ∈ toFinset s
has : ¬x ∈ toFinset s
⊢ False
exact has hx
no goals
case nil
ι : Type ?u.450788
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
⊢ prod (List.map f []) = ∏ m in toFinset [], f m ^ count m []
simp only [map_nil, prod_nil, count_nil, pow_zero, prod_const_one]
case pos
ι : Type ?u.450788
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : prod (List.map f s) = ∏ m in toFinset s, f m ^ count m s
has : a ∈ toFinset s
⊢ f a * f a ^ count a s * ∏ x in erase (toFinset s) a, f x ^ count x s =
    f a * f a ^ count a s * ∏ x in erase (toFinset s) a, f x ^ count x (a :: s)
case pos
ι : Type ?u.450788
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : prod (List.map f s) = ∏ m in toFinset s, f m ^ count m s
has : a ∈ toFinset s
⊢ f a * ∏ m in toFinset s, f m ^ count m s = ∏ x in insert a (toFinset s), f x ^ count x (a :: s)
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]
case pos.e_a
ι : Type ?u.450788
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : prod (List.map f s) = ∏ m in toFinset s, f m ^ count m s
has : a ∈ toFinset s
⊢ ∏ x in erase (toFinset s) a, f x ^ count x s = ∏ x in erase (toFinset s) a, f x ^ count x (a :: s)
case pos
ι : Type ?u.450788
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : prod (List.map f s) = ∏ m in toFinset s, f m ^ count m s
has : a ∈ toFinset s
⊢ f a * f a ^ count a s * ∏ x in erase (toFinset s) a, f x ^ count x s =
    f a * f a ^ count a s * ∏ x in erase (toFinset s) a, f x ^ count x (a :: s)
congr 1
case pos.e_a
ι : Type ?u.450788
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : prod (List.map f s) = ∏ m in toFinset s, f m ^ count m s
has : a ∈ toFinset s
x : α
hx : x ∈ erase (toFinset s) a
⊢ f x ^ count x s = f x ^ count x (a :: s)
case pos.e_a
ι : Type ?u.450788
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : prod (List.map f s) = ∏ m in toFinset s, f m ^ count m s
has : a ∈ toFinset s
⊢ ∏ x in erase (toFinset s) a, f x ^ count x s = ∏ x in erase (toFinset s) a, f x ^ count x (a :: s)
refine' prod_congr rfl fun x hx => _
no goals
case pos.e_a
ι : Type ?u.450788
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
a : α
s : List α
IH : prod (List.map f s) = ∏ m in toFinset s, f m ^ count m s
has : a ∈ toFinset s
x : α
hx : x ∈ erase (toFinset s) a
⊢ f x ^ count x s = f x ^ count x (a :: s)
rw [count_cons_of_ne (ne_of_mem_erase hx)]