case pos
α : Type u_1
β : Type u_2
γ : Type ?u.19798
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : IsIdempotent β op
h : a ∈ s
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.19798
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : IsIdempotent β op
h : ¬a ∈ s
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)
α : Type u_1
β : Type u_2
γ : Type ?u.19798
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : IsIdempotent β op
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)
by_cases h : a ∈ s
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.19798
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : IsIdempotent β op
h : a ∈ s
⊢ fold op b f (insert a (insert a (erase s a))) = op (f a) (fold op b f (insert a (erase s a)))
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.19798
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : IsIdempotent β op
h : a ∈ s
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)
rw [← insert_erase h]
no goals
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.19798
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : IsIdempotent β op
h : a ∈ s
⊢ fold op b f (insert a (insert a (erase s a))) = op (f a) (fold op b f (insert a (erase s a)))
simp [← ha.assoc, hi.idempotent]
no goals
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.19798
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : IsIdempotent β op
h : ¬a ∈ s
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)
apply fold_insert h