case empty
α : Type u_1
β : Type u_3
γ : Type u_2
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
g : γ → α
hi : IsIdempotent β op
⊢ fold op b f (image g ∅) = fold op b (f ∘ g) ∅

case cons
α : Type u_1
β : Type u_3
γ : Type u_2
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
g : γ → α
hi : IsIdempotent β op
x : γ
xs : Finset γ
hx : ¬x ∈ xs
ih : fold op b f (image g xs) = fold op b (f ∘ g) xs
⊢ fold op b f (image g (cons x xs hx)) = fold op b (f ∘ g) (cons x xs hx)
α : Type u_1
β : Type u_3
γ : Type u_2
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
inst✝ : DecidableEq α
g : γ → α
s : Finset γ
hi : IsIdempotent β op
⊢ fold op b f (image g s) = fold op b (f ∘ g) s
induction' s using Finset.cons_induction with x xs hx ih
no goals
case empty
α : Type u_1
β : Type u_3
γ : Type u_2
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
g : γ → α
hi : IsIdempotent β op
⊢ fold op b f (image g ∅) = fold op b (f ∘ g) ∅
rw [fold_empty, image_empty, fold_empty]
case cons
α : Type u_1
β : Type u_3
γ : Type u_2
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
g : γ → α
hi : IsIdempotent β op
x : γ
xs : Finset γ
hx : ¬x ∈ xs
ih : fold op b f (image g xs) = fold op b (f ∘ g) xs
this : DecidableEq γ
⊢ fold op b f (image g (cons x xs hx)) = fold op b (f ∘ g) (cons x xs hx)
case cons
α : Type u_1
β : Type u_3
γ : Type u_2
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
g : γ → α
hi : IsIdempotent β op
x : γ
xs : Finset γ
hx : ¬x ∈ xs
ih : fold op b f (image g xs) = fold op b (f ∘ g) xs
⊢ fold op b f (image g (cons x xs hx)) = fold op b (f ∘ g) (cons x xs hx)
haveI := Classical.decEq γ
case cons
α : Type u_1
β : Type u_3
γ : Type u_2
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
g : γ → α
hi : IsIdempotent β op
x : γ
xs : Finset γ
hx : ¬x ∈ xs
ih : fold op b f (image g xs) = fold op b (f ∘ g) xs
this : DecidableEq γ
⊢ op (f (g x)) (fold op b (f ∘ g) xs) = op ((f ∘ g) x) (fold op b (f ∘ g) xs)
case cons
α : Type u_1
β : Type u_3
γ : Type u_2
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
g : γ → α
hi : IsIdempotent β op
x : γ
xs : Finset γ
hx : ¬x ∈ xs
ih : fold op b f (image g xs) = fold op b (f ∘ g) xs
this : DecidableEq γ
⊢ fold op b f (image g (cons x xs hx)) = fold op b (f ∘ g) (cons x xs hx)
rw [fold_cons, cons_eq_insert, image_insert, fold_insert_idem, ih]
no goals
case cons
α : Type u_1
β : Type u_3
γ : Type u_2
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
g : γ → α
hi : IsIdempotent β op
x : γ
xs : Finset γ
hx : ¬x ∈ xs
ih : fold op b f (image g xs) = fold op b (f ∘ g) xs
this : DecidableEq γ
⊢ op (f (g x)) (fold op b (f ∘ g) xs) = op ((f ∘ g) x) (fold op b (f ∘ g) xs)
simp only [Function.comp_apply]