case nil
α : Type u_2
l : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : Monoid β
a✝ : α
f : α → β
hf✝ : ∀ (a' : α), a' ≠ a✝ → a' ∈ l → f a' = 1
a : α
hf : ∀ (a' : α), a' ≠ a → a' ∈ [] → f a' = 1
⊢ prod (map f []) = f a ^ count a []

case cons
α : Type u_2
l : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : Monoid β
a✝ : α
f : α → β
hf✝ : ∀ (a' : α), a' ≠ a✝ → a' ∈ l → f a' = 1
a' : α
as : List α
h : ∀ (a : α), (∀ (a' : α), a' ≠ a → a' ∈ as → f a' = 1) → prod (map f as) = f a ^ count a as
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
⊢ prod (map f (a' :: as)) = f a ^ count a (a' :: as)
α : Type u_2
l : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : Monoid β
a : α
f : α → β
hf : ∀ (a' : α), a' ≠ a → a' ∈ l → f a' = 1
⊢ prod (map f l) = f a ^ count a l
induction' l with a' as h generalizing a
no goals
case nil
α : Type u_2
l : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : Monoid β
a✝ : α
f : α → β
hf✝ : ∀ (a' : α), a' ≠ a✝ → a' ∈ l → f a' = 1
a : α
hf : ∀ (a' : α), a' ≠ a → a' ∈ [] → f a' = 1
⊢ prod (map f []) = f a ^ count a []
rw [map_nil, prod_nil, count_nil, _root_.pow_zero]
case cons
α : Type u_2
l : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : Monoid β
a✝ : α
f : α → β
hf✝ : ∀ (a' : α), a' ≠ a✝ → a' ∈ l → f a' = 1
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : prod (map f as) = f a ^ count a as
⊢ prod (map f (a' :: as)) = f a ^ count a (a' :: as)
case cons
α : Type u_2
l : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : Monoid β
a✝ : α
f : α → β
hf✝ : ∀ (a' : α), a' ≠ a✝ → a' ∈ l → f a' = 1
a' : α
as : List α
h : ∀ (a : α), (∀ (a' : α), a' ≠ a → a' ∈ as → f a' = 1) → prod (map f as) = f a ^ count a as
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
⊢ prod (map f (a' :: as)) = f a ^ count a (a' :: as)
specialize h a fun a' ha' hfa' => hf a' ha' (mem_cons_of_mem _ hfa')
case cons
α : Type u_2
l : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : Monoid β
a✝ : α
f : α → β
hf✝ : ∀ (a' : α), a' ≠ a✝ → a' ∈ l → f a' = 1
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : prod (map f as) = f a ^ count a as
⊢ f a' * f a ^ count a as = f a ^ if a = a' then succ (count a as) else count a as
case cons
α : Type u_2
l : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : Monoid β
a✝ : α
f : α → β
hf✝ : ∀ (a' : α), a' ≠ a✝ → a' ∈ l → f a' = 1
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : prod (map f as) = f a ^ count a as
⊢ prod (map f (a' :: as)) = f a ^ count a (a' :: as)
rw [List.map_cons, List.prod_cons, count_cons, h]
case cons.inl
α : Type u_2
l : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : Monoid β
a✝ : α
f : α → β
hf✝ : ∀ (a' : α), a' ≠ a✝ → a' ∈ l → f a' = 1
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : prod (map f as) = f a ^ count a as
ha' : a = a'
⊢ f a' * f a ^ count a as = f a ^ succ (count a as)

case cons.inr
α : Type u_2
l : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : Monoid β
a✝ : α
f : α → β
hf✝ : ∀ (a' : α), a' ≠ a✝ → a' ∈ l → f a' = 1
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : prod (map f as) = f a ^ count a as
ha' : ¬a = a'
⊢ f a' * f a ^ count a as = f a ^ count a as
case cons
α : Type u_2
l : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : Monoid β
a✝ : α
f : α → β
hf✝ : ∀ (a' : α), a' ≠ a✝ → a' ∈ l → f a' = 1
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : prod (map f as) = f a ^ count a as
⊢ f a' * f a ^ count a as = f a ^ if a = a' then succ (count a as) else count a as
split_ifs with ha'
no goals
case cons.inl
α : Type u_2
l : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : Monoid β
a✝ : α
f : α → β
hf✝ : ∀ (a' : α), a' ≠ a✝ → a' ∈ l → f a' = 1
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : prod (map f as) = f a ^ count a as
ha' : a = a'
⊢ f a' * f a ^ count a as = f a ^ succ (count a as)
rw [ha', _root_.pow_succ]
no goals
case cons.inr
α : Type u_2
l : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : Monoid β
a✝ : α
f : α → β
hf✝ : ∀ (a' : α), a' ≠ a✝ → a' ∈ l → f a' = 1
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : prod (map f as) = f a ^ count a as
ha' : ¬a = a'
⊢ f a' * f a ^ count a as = f a ^ count a as
rw [hf a' (Ne.symm ha') (List.mem_cons_self a' as), one_mul]