case empty
α : Type u_1
β : Type u_2
γ : Type ?u.12073
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
hd✝ : Decidable (s = ∅)
c : β
h : op c (op b c) = op b c
hd : Decidable (∅ = ∅)
⊢ fold op b (fun x => c) ∅ = if ∅ = ∅ then b else op b c

case insert
α : Type u_1
β : Type u_2
γ : Type ?u.12073
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
hd✝ : Decidable (s✝ = ∅)
c : β
h : op c (op b c) = op b c
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ [hd : Decidable (s = ∅)], fold op b (fun x => c) s = if s = ∅ then b else op b c
hd : Decidable (insert x s = ∅)
⊢ fold op b (fun x => c) (insert x s) = if insert x s = ∅ then b else op b c
α : Type u_1
β : Type u_2
γ : Type ?u.12073
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
hd : Decidable (s = ∅)
c : β
h : op c (op b c) = op b c
⊢ fold op b (fun x => c) s = if s = ∅ then b else op b c
induction' s using Finset.induction_on with x s hx IH generalizing hd
no goals
case empty
α : Type u_1
β : Type u_2
γ : Type ?u.12073
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
hd✝ : Decidable (s = ∅)
c : β
h : op c (op b c) = op b c
hd : Decidable (∅ = ∅)
⊢ fold op b (fun x => c) ∅ = if ∅ = ∅ then b else op b c
simp
case insert
α : Type u_1
β : Type u_2
γ : Type ?u.12073
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
hd✝ : Decidable (s✝ = ∅)
c : β
h : op c (op b c) = op b c
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ [hd : Decidable (s = ∅)], fold op b (fun x => c) s = if s = ∅ then b else op b c
hd : Decidable (insert x s = ∅)
⊢ op c (if s = ∅ then b else op b c) = op b c
case insert
α : Type u_1
β : Type u_2
γ : Type ?u.12073
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
hd✝ : Decidable (s✝ = ∅)
c : β
h : op c (op b c) = op b c
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ [hd : Decidable (s = ∅)], fold op b (fun x => c) s = if s = ∅ then b else op b c
hd : Decidable (insert x s = ∅)
⊢ fold op b (fun x => c) (insert x s) = if insert x s = ∅ then b else op b c
simp only [Finset.fold_insert hx, IH, if_false, Finset.insert_ne_empty]
case insert.inl
α : Type u_1
β : Type u_2
γ : Type ?u.12073
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
hd✝ : Decidable (s✝ = ∅)
c : β
h : op c (op b c) = op b c
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ [hd : Decidable (s = ∅)], fold op b (fun x => c) s = if s = ∅ then b else op b c
hd : Decidable (insert x s = ∅)
h✝ : s = ∅
⊢ op c b = op b c

case insert.inr
α : Type u_1
β : Type u_2
γ : Type ?u.12073
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
hd✝ : Decidable (s✝ = ∅)
c : β
h : op c (op b c) = op b c
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ [hd : Decidable (s = ∅)], fold op b (fun x => c) s = if s = ∅ then b else op b c
hd : Decidable (insert x s = ∅)
h✝ : ¬s = ∅
⊢ op c (op b c) = op b c
case insert
α : Type u_1
β : Type u_2
γ : Type ?u.12073
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
hd✝ : Decidable (s✝ = ∅)
c : β
h : op c (op b c) = op b c
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ [hd : Decidable (s = ∅)], fold op b (fun x => c) s = if s = ∅ then b else op b c
hd : Decidable (insert x s = ∅)
⊢ op c (if s = ∅ then b else op b c) = op b c
split_ifs
no goals
case insert.inl
α : Type u_1
β : Type u_2
γ : Type ?u.12073
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
hd✝ : Decidable (s✝ = ∅)
c : β
h : op c (op b c) = op b c
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ [hd : Decidable (s = ∅)], fold op b (fun x => c) s = if s = ∅ then b else op b c
hd : Decidable (insert x s = ∅)
h✝ : s = ∅
⊢ op c b = op b c
rw [hc.comm]
no goals
case insert.inr
α : Type u_1
β : Type u_2
γ : Type ?u.12073
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
hd✝ : Decidable (s✝ = ∅)
c : β
h : op c (op b c) = op b c
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ [hd : Decidable (s = ∅)], fold op b (fun x => c) s = if s = ∅ then b else op b c
hd : Decidable (insert x s = ∅)
h✝ : ¬s = ∅
⊢ op c (op b c) = op b c
exact h