awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
inst : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
rw :
  Multiset.fold op (op b₁ b₂) (Multiset.map f (s₁ ∪ s₂).val + Multiset.map f (s₁ ∩ s₂).val) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
rw₁ :
  Multiset.fold op (op b₁ b₂) (Multiset.map f ((s₁ ∪ s₂).val + (s₁ ∩ s₂).val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
rw₂ :
  Multiset.fold op (op b₁ b₂) (Multiset.map f (s₁.val ∪ s₂.val + (s₁ ∩ s₂).val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
⊢ op (Multiset.fold op b₁ (Multiset.map f (s₁ ∪ s₂).val)) (Multiset.fold op b₂ (Multiset.map f (s₁ ∩ s₂).val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
have rw₃ : Multiset.fold op (op b₁ b₂) (Multiset.map f (s₁.val ∪ s₂.val + s₁.val ∩ s₂.val)) =
  op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
Tactic: rw [← fold_add op, ← Multiset.map_add, union_val, inter_val, union_add_inter, Multiset.map_add,
    hc.comm, fold_add]
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
inst : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
rw :
  Multiset.fold op (op b₁ b₂) (Multiset.map f (s₁ ∪ s₂).val + Multiset.map f (s₁ ∩ s₂).val) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
rw₁ :
  Multiset.fold op (op b₁ b₂) (Multiset.map f ((s₁ ∪ s₂).val + (s₁ ∩ s₂).val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
rw₂ :
  Multiset.fold op (op b₁ b₂) (Multiset.map f (s₁.val ∪ s₂.val + (s₁ ∩ s₂).val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
rw₃ :
  Multiset.fold op (op b₁ b₂) (Multiset.map f (s₁.val ∪ s₂.val + s₁.val ∩ s₂.val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
⊢ op (Multiset.fold op b₁ (Multiset.map f (s₁ ∪ s₂).val)) (Multiset.fold op b₂ (Multiset.map f (s₁ ∩ s₂).val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
have rw₄ : Multiset.fold op (op b₁ b₂) (Multiset.map f (s₁.val + s₂.val)) =
  op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
Tactic: rw [← fold_add op, ← Multiset.map_add, union_val, inter_val, union_add_inter, Multiset.map_add,
    hc.comm, fold_add]
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
inst : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
rw :
  Multiset.fold op (op b₁ b₂) (Multiset.map f (s₁ ∪ s₂).val + Multiset.map f (s₁ ∩ s₂).val) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
rw₁ :
  Multiset.fold op (op b₁ b₂) (Multiset.map f ((s₁ ∪ s₂).val + (s₁ ∩ s₂).val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
rw₂ :
  Multiset.fold op (op b₁ b₂) (Multiset.map f (s₁.val ∪ s₂.val + (s₁ ∩ s₂).val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
rw₃ :
  Multiset.fold op (op b₁ b₂) (Multiset.map f (s₁.val ∪ s₂.val + s₁.val ∩ s₂.val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
rw₄ :
  Multiset.fold op (op b₁ b₂) (Multiset.map f (s₁.val + s₂.val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
⊢ op (Multiset.fold op b₁ (Multiset.map f (s₁ ∪ s₂).val)) (Multiset.fold op b₂ (Multiset.map f (s₁ ∩ s₂).val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
have rw₅ : Multiset.fold op (op b₁ b₂) (Multiset.map f s₁.val + Multiset.map f s₂.val) =
  op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
Tactic: rw [← fold_add op, ← Multiset.map_add, union_val, inter_val, union_add_inter, Multiset.map_add,
    hc.comm, fold_add]
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
inst : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
rw :
  Multiset.fold op (op b₁ b₂) (Multiset.map f (s₁ ∪ s₂).val + Multiset.map f (s₁ ∩ s₂).val) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
rw₁ :
  Multiset.fold op (op b₁ b₂) (Multiset.map f ((s₁ ∪ s₂).val + (s₁ ∩ s₂).val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
rw₂ :
  Multiset.fold op (op b₁ b₂) (Multiset.map f (s₁.val ∪ s₂.val + (s₁ ∩ s₂).val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
rw₃ :
  Multiset.fold op (op b₁ b₂) (Multiset.map f (s₁.val ∪ s₂.val + s₁.val ∩ s₂.val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
rw₄ :
  Multiset.fold op (op b₁ b₂) (Multiset.map f (s₁.val + s₂.val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
rw₅ :
  Multiset.fold op (op b₁ b₂) (Multiset.map f s₁.val + Multiset.map f s₂.val) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
⊢ op (Multiset.fold op b₁ (Multiset.map f (s₁ ∪ s₂).val)) (Multiset.fold op b₂ (Multiset.map f (s₁ ∩ s₂).val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
have rw₆ : Multiset.fold op (op b₂ b₁) (Multiset.map f s₁.val + Multiset.map f s₂.val) =
  op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
Tactic: rw [← fold_add op, ← Multiset.map_add, union_val, inter_val, union_add_inter, Multiset.map_add,
    hc.comm, fold_add]
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
inst : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
rw :
  Multiset.fold op (op b₁ b₂) (Multiset.map f (s₁ ∪ s₂).val + Multiset.map f (s₁ ∩ s₂).val) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
rw₁ :
  Multiset.fold op (op b₁ b₂) (Multiset.map f ((s₁ ∪ s₂).val + (s₁ ∩ s₂).val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
rw₂ :
  Multiset.fold op (op b₁ b₂) (Multiset.map f (s₁.val ∪ s₂.val + (s₁ ∩ s₂).val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
rw₃ :
  Multiset.fold op (op b₁ b₂) (Multiset.map f (s₁.val ∪ s₂.val + s₁.val ∩ s₂.val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
rw₄ :
  Multiset.fold op (op b₁ b₂) (Multiset.map f (s₁.val + s₂.val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
rw₅ :
  Multiset.fold op (op b₁ b₂) (Multiset.map f s₁.val + Multiset.map f s₂.val) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
rw₆ :
  Multiset.fold op (op b₂ b₁) (Multiset.map f s₁.val + Multiset.map f s₂.val) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
⊢ op (Multiset.fold op b₁ (Multiset.map f (s₁ ∪ s₂).val)) (Multiset.fold op b₂ (Multiset.map f (s₁ ∩ s₂).val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
have rw₇ : op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val)) =
  op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
Tactic: rw [← fold_add op, ← Multiset.map_add, union_val, inter_val, union_add_inter, Multiset.map_add,
    hc.comm, fold_add]
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst : DecidableEq α
hi : Std.IdempotentOp op
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)
have pos : ∀ (h : a ∈ s), fold op b f (insert a s) = op (f a) (fold op b f s)
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst : DecidableEq α
hi : Std.IdempotentOp op
pos : ∀ (h : a ∈ s), fold op b f (insert a s) = op (f a) (fold op b f s)
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)
have neg : ∀ (h : a ∉ s), fold op b f (insert a s) = op (f a) (fold op b f s)
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst : DecidableEq α
hi : Std.IdempotentOp op
h : a ∈ s
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)
have pos : fold op b f (insert a (insert a (s.erase a))) = op (f a) (fold op b f (insert a (s.erase a)))
Tactic: rw [← insert_erase h]
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst : DecidableEq α
g : γ → α
hi : Std.IdempotentOp op
⊢ fold op b f (image g ∅) = fold op b (f ∘ g) ∅
have empty : fold op b f (image g ∅) = b
Tactic: rw [fold_empty, image_empty, fold_empty]
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst : DecidableEq α
g : γ → α
hi : Std.IdempotentOp op
empty : fold op b f (image g ∅) = b
⊢ fold op b f (image g ∅) = fold op b (f ∘ g) ∅
have empty₁ : fold op b f ∅ = b
Tactic: rw [fold_empty, image_empty, fold_empty]
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst : DecidableEq α
g : γ → α
hi : Std.IdempotentOp op
empty : fold op b f (image g ∅) = b
empty₁ : fold op b f ∅ = b
⊢ fold op b f (image g ∅) = fold op b (f ∘ g) ∅
have empty₂ : b = b
Tactic: rw [fold_empty, image_empty, fold_empty]
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst : DecidableEq α
g : γ → α
hi : Std.IdempotentOp 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)
have cons : ∀ (this : DecidableEq γ), fold op b f (image g (cons x xs hx)) = fold op b (f ∘ g) (cons x xs hx)
Tactic: haveI := Classical.decEq γ
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst : DecidableEq α
g : γ → α
hi : Std.IdempotentOp 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)
have cons : op (f (g x)) (fold op b (f ∘ g) xs) = op ((f ∘ g) x) (fold op b (f ∘ g) xs)
Tactic: rw [fold_cons, cons_eq_insert, image_insert, fold_insert_idem, ih]
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst : DecidableEq α
g : γ → α
s : Finset γ
hi : Std.IdempotentOp op
⊢ fold op b f (image g s) = fold op b (f ∘ g) s
have empty : fold op b f (image g ∅) = fold op b (f ∘ g) ∅
Tactic: induction s using Finset.cons_induction with
  | empty => rw [fold_empty, image_empty, fold_empty]
  | cons x xs hx ih =>
    haveI := Classical.decEq γ
    rw [fold_cons, cons_eq_insert, image_insert, fold_insert_idem, ih]
    simp only [Function.comp_apply]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst : DecidableEq α
g : γ → α
s : Finset γ
hi : Std.IdempotentOp op
empty : fold op b f (image g ∅) = fold op b (f ∘ g) ∅
⊢ fold op b f (image g s) = fold op b (f ∘ g) s
have cons : ∀ (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)
Tactic: induction s using Finset.cons_induction with
  | empty => rw [fold_empty, image_empty, fold_empty]
  | cons x xs hx ih =>
    haveI := Classical.decEq γ
    rw [fold_cons, cons_eq_insert, image_insert, fold_insert_idem, ih]
    simp only [Function.comp_apply]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s_1 : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst : DecidablePred p
x : α
s : Finset α
hx : x ∉ s
IH : fold op b (fun (i : α) ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
⊢ fold op b (fun (i : α) ↦ if p i then f i else g i) (insert x s) =
    op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))
have insert : op (if p x then f x else g x) (fold op b (fun (i : α) ↦ if p i then f i else g i) s) =
  op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))
Tactic: simp only [Finset.fold_insert hx]
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s_1 : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst : DecidablePred p
x : α
s : Finset α
hx : x ∉ s
IH : fold op b (fun (i : α) ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
⊢ op (if p x then f x else g x) (fold op b (fun (i : α) ↦ if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))
have pos : ∀ (h : p x),
  op (f x) (fold op b (fun (i : α) ↦ if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s_1 : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst : DecidablePred p
x : α
s : Finset α
hx : x ∉ s
IH : fold op b (fun (i : α) ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
pos :
  ∀ (h : p x),
    op (f x) (fold op b (fun (i : α) ↦ if p i then f i else g i) s) =
      op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))
⊢ op (if p x then f x else g x) (fold op b (fun (i : α) ↦ if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))
have neg : ∀ (h : ¬p x),
  op (g x) (fold op b (fun (i : α) ↦ if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (hypothesis)
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s_1 : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst : DecidablePred p
x : α
s : Finset α
hx : x ∉ s
IH : fold op b (fun (i : α) ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
h : p x
⊢ op (f x) (fold op b (fun (i : α) ↦ if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))
have this : x ∉ filter p s
Tactic: have : x ∉ Finset.filter p s := by simp [hx]
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (hypothesis)
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s_1 : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst : DecidablePred p
x : α
s : Finset α
hx : x ∉ s
IH : fold op b (fun (i : α) ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
h : ¬p x
⊢ op (g x) (fold op b (fun (i : α) ↦ if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))
have this : x ∉ {i ∈ s | ¬p i}
Tactic: have : x ∉ Finset.filter (fun i => ¬ p i) s := by simp [hx]
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst : DecidablePred p
⊢ fold op b (fun (i : α) ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
have empty : fold op b (fun (i : α) ↦ if p i then f i else g i) ∅ = op (fold op b f (filter p ∅)) (fold op b g ({i ∈ ∅ | ¬p i}))
Tactic: induction s using Finset.induction_on with
    | empty => simp [hb]
    | insert x s hx IH =>
      simp only [Finset.fold_insert hx]
      split_ifs with h
      · have : x ∉ Finset.filter p s := by simp [hx]
        simp [Finset.filter_insert, h, Finset.fold_insert this, ha.assoc, IH]
      · have : x ∉ Finset.filter (fun i => ¬ p i) s := by simp [hx]
        simp [Finset.filter_insert, h, Finset.fold_insert this, IH, ← ha.assoc, hc.comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst : DecidablePred p
empty :
  fold op b (fun (i : α) ↦ if p i then f i else g i) ∅ = op (fold op b f (filter p ∅)) (fold op b g ({i ∈ ∅ | ¬p i}))
⊢ fold op b (fun (i : α) ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
have insert : ∀ (x : α) (s : Finset α) (hx : x ∉ s)
  (IH :
    fold op b (fun (i : α) ↦ if p i then f i else g i) s =
      op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))),
  fold op b (fun (i : α) ↦ if p i then f i else g i) (insert x s) =
    op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))
Tactic: induction s using Finset.induction_on with
    | empty => simp [hb]
    | insert x s hx IH =>
      simp only [Finset.fold_insert hx]
      split_ifs with h
      · have : x ∉ Finset.filter p s := by simp [hx]
        simp [Finset.filter_insert, h, Finset.fold_insert this, ha.assoc, IH]
      · have : x ∉ Finset.filter (fun i => ¬ p i) s := by simp [hx]
        simp [Finset.filter_insert, h, Finset.fold_insert this, IH, ← ha.assoc, hc.comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst : DecidablePred p
⊢ fold op b (fun (i : α) ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
have empty : fold op b (fun (i : α) ↦ if p i then f i else g i) ∅ = op (fold op b f (filter p ∅)) (fold op b g ({i ∈ ∅ | ¬p i}))
Tactic: classical
    induction s using Finset.induction_on with
    | empty => simp [hb]
    | insert x s hx IH =>
      simp only [Finset.fold_insert hx]
      split_ifs with h
      · have : x ∉ Finset.filter p s := by simp [hx]
        simp [Finset.filter_insert, h, Finset.fold_insert this, ha.assoc, IH]
      · have : x ∉ Finset.filter (fun i => ¬ p i) s := by simp [hx]
        simp [Finset.filter_insert, h, Finset.fold_insert this, IH, ← ha.assoc, hc.comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst : DecidablePred p
empty :
  fold op b (fun (i : α) ↦ if p i then f i else g i) ∅ = op (fold op b f (filter p ∅)) (fold op b g ({i ∈ ∅ | ¬p i}))
⊢ fold op b (fun (i : α) ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
have insert : ∀ (x : α) (s : Finset α) (hx : x ∉ s)
  (IH :
    fold op b (fun (i : α) ↦ if p i then f i else g i) s =
      op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))),
  fold op b (fun (i : α) ↦ if p i then f i else g i) (insert x s) =
    op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))
Tactic: classical
    induction s using Finset.induction_on with
    | empty => simp [hb]
    | insert x s hx IH =>
      simp only [Finset.fold_insert hx]
      split_ifs with h
      · have : x ∉ Finset.filter p s := by simp [hx]
        simp [Finset.filter_insert, h, Finset.fold_insert this, ha.assoc, IH]
      · have : x ∉ Finset.filter (fun i => ¬ p i) s := by simp [hx]
        simp [Finset.filter_insert, h, Finset.fold_insert this, IH, ← ha.assoc, hc.comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha_1 : Std.Associative op
f : α → β
b : β
s_1 : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)
⊢ r c (fold op b f (insert a s)) ↔ r c b ∧ ∀ x ∈ insert a s, r c (f x)
have insert : (r c b ∧ r c (f a) ∧ ∀ x ∈ s, r c (f x)) ↔ r c b ∧ ∀ x ∈ insert a s, r c (f x)
Tactic: rw [Finset.fold_insert ha, hr, IH, ← and_assoc, @and_comm (r c (f a)), and_assoc]
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
⊢ r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)
have empty : r c (fold op b f ∅) ↔ r c b ∧ ∀ (x : α), Membership.mem (γ := Finset α) ∅ x → r c (f x)
Tactic: induction s using Finset.induction_on with
    | empty => simp
    | insert a s ha IH =>
      rw [Finset.fold_insert ha, hr, IH, ← and_assoc, @and_comm (r c (f a)), and_assoc]
      simp
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
empty : r c (fold op b f ∅) ↔ r c b ∧ ∀ (x : α), Membership.mem (γ := Finset α) ∅ x → r c (f x)
⊢ r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)
have insert : ∀ (a : α) (s : Finset α) (ha_1 : a ∉ s) (IH : r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)),
  r c (fold op b f (insert a s)) ↔ r c b ∧ ∀ x ∈ insert a s, r c (f x)
Tactic: induction s using Finset.induction_on with
    | empty => simp
    | insert a s ha IH =>
      rw [Finset.fold_insert ha, hr, IH, ← and_assoc, @and_comm (r c (f a)), and_assoc]
      simp
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
⊢ r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)
have empty : r c (fold op b f ∅) ↔ r c b ∧ ∀ (x : α), Membership.mem (γ := Finset α) ∅ x → r c (f x)
Tactic: classical
    induction s using Finset.induction_on with
    | empty => simp
    | insert a s ha IH =>
      rw [Finset.fold_insert ha, hr, IH, ← and_assoc, @and_comm (r c (f a)), and_assoc]
      simp