-- Mathlib/Data/Finset/Fold.lean
theorem fold_const [hd : Decidable (s = ∅)] (c : β) (h : op c (op b c) = op b c) :
    Finset.fold op b (fun _ => c) s = if s = ∅ then b else op b c

Proof state:
case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
b : β
s✝ : Finset α
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

Tactic:
split_ifs

Result:
case pos
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
b : β
s✝ : Finset α
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 neg
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
b : β
s✝ : Finset α
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

Proof state:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
b : β
s : Finset α
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

Tactic:
induction' s using Finset.induction_on with x s hx IH generalizing hd

Result:
case empty
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
b : β
s : Finset α
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
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
b : β
s✝ : Finset α
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

Proof state:
case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
b : β
s✝ : Finset α
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

Tactic:
simp only [Finset.fold_insert hx, IH, if_false, Finset.insert_ne_empty]

Result:
case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
b : β
s✝ : Finset α
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

Proof state:
case neg
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
b : β
s✝ : Finset α
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

Tactic:
exact h

Result:
no goals

Proof state:
case empty
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
b : β
s : Finset α
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

Tactic:
simp

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
b : β
s✝ : Finset α
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

Tactic:
rw [hc.comm]

Result:
no goals