case empty
α : Type u_1
β : Type ?u.62282
γ : Type ?u.62285
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
⊢ fold (fun x x_1 => x ∪ x_1) ∅ singleton ∅ = ∅

case insert
α : Type u_1
β : Type ?u.62282
γ : Type ?u.62285
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
inst✝ : DecidableEq α
a : α
s : Finset α
has : ¬a ∈ s
ih : fold (fun x x_1 => x ∪ x_1) ∅ singleton s = s
⊢ fold (fun x x_1 => x ∪ x_1) ∅ singleton (insert a s) = insert a s
α : Type u_1
β : Type ?u.62282
γ : Type ?u.62285
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
inst✝ : DecidableEq α
s : Finset α
⊢ fold (fun x x_1 => x ∪ x_1) ∅ singleton s = s
induction' s using Finset.induction_on with a s has ih
no goals
case empty
α : Type u_1
β : Type ?u.62282
γ : Type ?u.62285
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
⊢ fold (fun x x_1 => x ∪ x_1) ∅ singleton ∅ = ∅
simp only [fold_empty]
no goals
case insert
α : Type u_1
β : Type ?u.62282
γ : Type ?u.62285
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
inst✝ : DecidableEq α
a : α
s : Finset α
has : ¬a ∈ s
ih : fold (fun x x_1 => x ∪ x_1) ∅ singleton s = s
⊢ fold (fun x x_1 => x ∪ x_1) ∅ singleton (insert a s) = insert a s
rw [fold_insert has, ih, insert_eq]