awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
op' : γ → γ → γ
inst : Std.Commutative op'
inst_1 : Std.Associative op'
m : β → γ
hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)
rw :
  Multiset.fold op' (m b) (Multiset.map (fun (x : α) ↦ m (f x)) s.val) =
    Multiset.fold op' (m b) (Multiset.map (m ∘ f) s.val)
⊢ fold op' (m b) (fun (x : α) ↦ m (f x)) s = m (fold op b f s)

Tactic:
rw [fold, fold, ← Multiset.fold_hom op hm, Multiset.map_map]

Premises used: Finset.fold, Multiset.fold_hom, Multiset.map_map
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
op' : γ → γ → γ
inst : Std.Commutative op'
inst_1 : Std.Associative op'
m : β → γ
hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)
⊢ Multiset.fold op' (m b) (Multiset.map (fun (x : α) ↦ m (f x)) s.val) =
    Multiset.fold op' (m b) (Multiset.map (m ∘ f) s.val)

Tactic:
simp only [Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
s₁ s₂ : Finset α
b₁ b₂ : β
h : Disjoint s₁ s₂
⊢ fold op (op b₁ b₂) f (s₁.disjUnion s₂ h) = op (fold op b₁ f s₁) (fold op b₂ f s₂)

Tactic:
(congr_arg _ <| Multiset.map_add _ _ _).trans (Multiset.fold_add _ _ _ _ _)

Premises used: Multiset.fold_add, Finset.fold, congr_arg, Multiset.map_add, Eq.trans
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
inst : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
unfold :
  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))
⊢ op (fold op b₁ f (s₁ ∪ s₂)) (fold op b₂ f (s₁ ∩ s₂)) = op (fold op b₂ f s₁) (fold op b₁ f s₂)

Tactic:
unfold fold

Premises used: Finset.fold
-- Module: Mathlib.Data.Finset.Fold
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))
rw₇ 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))
⊢ 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))

Tactic:
rw [← fold_add op, ← Multiset.map_add, union_val, inter_val, union_add_inter, Multiset.map_add,
    hc.comm, fold_add]

Premises used: Multiset.fold_add, Multiset.union_add_inter, Finset.union_val, Std.Commutative.comm, Finset.inter_val, Multiset.map_add
-- Module: Mathlib.Data.Finset.Fold
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)
neg : ∀ (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)

Tactic:
by_cases h : a ∈ s
-- Module: Mathlib.Data.Finset.Fold
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
pos : fold op b f (insert a (insert a (s.erase a))) = op (f a) (fold op b f (insert a (s.erase a)))
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)

Tactic:
rw [← insert_erase h]

Premises used: Finset.insert_erase
-- Module: Mathlib.Data.Finset.Fold
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 (insert a (s.erase a))) = op (f a) (fold op b f (insert a (s.erase a)))

Tactic:
simp [← ha.assoc, hi.idempotent]

Premises used: Std.Associative.assoc, Std.IdempotentOp.idempotent
-- Module: Mathlib.Data.Finset.Fold
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)

Tactic:
apply fold_insert h

Premises used: Finset.fold_insert
-- Module: Mathlib.Data.Finset.Fold
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
empty₂ empty₃ : b = b
⊢ fold op b f (image g ∅) = fold op b (f ∘ g) ∅

Tactic:
rw [fold_empty, image_empty, fold_empty]

Premises used: Finset.image_empty, Finset.fold_empty
-- Module: Mathlib.Data.Finset.Fold
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
cons : ∀ (this : DecidableEq γ), fold op b f (image g (Finset.cons x xs hx)) = fold op b (f ∘ g) (Finset.cons x xs hx)
⊢ fold op b f (image g (Finset.cons x xs hx)) = fold op b (f ∘ g) (Finset.cons x xs hx)

Tactic:
haveI := Classical.decEq γ
-- Module: Mathlib.Data.Finset.Fold
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 γ
cons : op (f (g x)) (fold op b (f ∘ g) xs) = op ((f ∘ g) x) (fold op b (f ∘ g) xs)
⊢ fold op b f (image g (Finset.cons x xs hx)) = fold op b (f ∘ g) (Finset.cons x xs hx)

Tactic:
rw [fold_cons, cons_eq_insert, image_insert, fold_insert_idem, ih]

Premises used: Finset.fold_cons, Finset.fold_insert_idem, Finset.cons_eq_insert, Finset.image_insert
-- Module: Mathlib.Data.Finset.Fold
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 γ
⊢ op (f (g x)) (fold op b (f ∘ g) xs) = op ((f ∘ g) x) (fold op b (f ∘ g) xs)

Tactic:
simp only [Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.Data.Finset.Fold
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) ∅
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 (Finset.cons x xs hx)) = fold op b (f ∘ g) (Finset.cons x xs hx)
⊢ fold op b f (image g s) = fold op b (f ∘ g) s

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]

Premises used: Finset.image_empty, Finset.cons, Finset.fold_cons, Finset.fold_empty, Finset.fold_insert_idem, Finset.cons_eq_insert, Function.comp_apply, Finset.image_insert
-- Module: Mathlib.Data.Finset.Fold
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) ∅ = op (fold op b f (filter p ∅)) (fold op b g ({i ∈ ∅ | ¬p i}))

Tactic:
simp [hb]
-- Module: Mathlib.Data.Finset.Fold
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}))
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.insert x s))) (fold op b g ({i ∈ Insert.insert x s | ¬p i}))
⊢ fold op b (fun (i : α) ↦ if p i then f i else g i) (Insert.insert x s) =
    op (fold op b f (filter p (Insert.insert x s))) (fold op b g ({i ∈ Insert.insert x s | ¬p i}))

Tactic:
simp only [Finset.fold_insert hx]

Premises used: Finset.fold_insert
-- Module: Mathlib.Data.Finset.Fold
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}))
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}))
⊢ 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:
split_ifs with h
-- Module: Mathlib.Data.Finset.Fold
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
⊢ x ∉ filter p s

Tactic:
simp [hx]
-- Module: Mathlib.Data.Finset.Fold
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
⊢ x ∉ filter p s

Tactic:
have : x ∉ Finset.filter p s := by simp [hx]
-- Module: Mathlib.Data.Finset.Fold
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
this : x ∉ filter p s
⊢ 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:
simp [Finset.filter_insert, h, Finset.fold_insert this, ha.assoc, IH]

Premises used: Std.Associative.assoc, Finset.filter_insert, Finset.fold_insert
-- Module: Mathlib.Data.Finset.Fold
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
⊢ x ∉ {i ∈ s | ¬p i}

Tactic:
simp [hx]
-- Module: Mathlib.Data.Finset.Fold
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
⊢ x ∉ {i ∈ s | ¬p i}

Tactic:
have : x ∉ Finset.filter (fun i => ¬ p i) s := by simp [hx]
-- Module: Mathlib.Data.Finset.Fold
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
this : x ∉ {i ∈ s | ¬p i}
⊢ 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:
simp [Finset.filter_insert, h, Finset.fold_insert this, IH, ← ha.assoc, hc.comm]

Premises used: Std.Associative.assoc, Finset.filter_insert, Std.Commutative.comm, Finset.fold_insert
-- Module: Mathlib.Data.Finset.Fold
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}))
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.insert x s) =
      op (fold op b f (filter p (Insert.insert x s))) (fold op b g ({i ∈ Insert.insert x s | ¬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}))

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]

Premises used: Std.Associative.assoc, Insert.insert, Finset.filter_insert, Std.Commutative.comm
-- Module: Mathlib.Data.Finset.Fold
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}))
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.insert x s) =
      op (fold op b f (filter p (Insert.insert x s))) (fold op b g ({i ∈ Insert.insert x s | ¬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}))

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]

Premises used: Std.Associative.assoc, Insert.insert, Finset.filter_insert, Std.Commutative.comm
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
inst : Std.IdempotentOp op
g : α → β
p : α → Prop
inst_1 : 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}))

Tactic:
fold_ite' (Std.IdempotentOp.idempotent _) _

Premises used: Std.IdempotentOp.idempotent, Finset.fold_ite'
-- Module: Mathlib.Data.Finset.Fold
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 ∅) ↔ r c b ∧ ∀ (x : α), Membership.mem (γ := Finset α) ∅ x → r c (f x)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Fold
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)
insert : (r c b ∧ r c (f a) ∧ ∀ x ∈ s, r c (f x)) ↔ r c b ∧ ∀ x ∈ Insert.insert a s, r c (f x)
⊢ r c (fold op b f (Insert.insert a s)) ↔ r c b ∧ ∀ x ∈ Insert.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]

Premises used: and_comm, and_assoc, Finset.fold_insert
-- Module: Mathlib.Data.Finset.Fold
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 b ∧ r c (f a) ∧ ∀ x ∈ s, r c (f x)) ↔ r c b ∧ ∀ x ∈ insert a s, r c (f x)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Fold
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)
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.insert a s)) ↔ r c b ∧ ∀ x ∈ Insert.insert a s, r c (f x)
⊢ r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ 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

Premises used: Insert.insert, and_assoc
-- Module: Mathlib.Data.Finset.Fold
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)
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.insert a s)) ↔ r c b ∧ ∀ x ∈ Insert.insert a s, r c (f x)
⊢ r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, 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

Premises used: Insert.insert, and_assoc
-- Module: Mathlib.Data.Finset.Fold
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 ∅) ↔ r c b ∨ ∃ (x : α), Membership.mem (γ := Finset α) ∅ x ∧ r c (f x)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Fold
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)
insert : (r c b ∨ r c (f a) ∨ ∃ x ∈ s, r c (f x)) ↔ r c b ∨ ∃ x ∈ Insert.insert a s, r c (f x)
⊢ r c (fold op b f (Insert.insert a s)) ↔ r c b ∨ ∃ x ∈ Insert.insert a s, r c (f x)

Tactic:
rw [Finset.fold_insert ha, hr, IH, ← or_assoc, @or_comm (r c (f a)), or_assoc]

Premises used: or_comm, Finset.fold_insert, or_assoc
-- Module: Mathlib.Data.Finset.Fold
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 b ∨ r c (f a) ∨ ∃ x ∈ s, r c (f x)) ↔ r c b ∨ ∃ x ∈ insert a s, r c (f x)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Fold
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)
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.insert a s)) ↔ r c b ∨ ∃ x ∈ Insert.insert a s, r c (f x)
⊢ r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ 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, ← or_assoc, @or_comm (r c (f a)), or_assoc]
      simp

Premises used: Insert.insert, or_assoc
-- Module: Mathlib.Data.Finset.Fold
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)
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.insert a s)) ↔ r c b ∨ ∃ x ∈ Insert.insert a s, r c (f x)
⊢ r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, 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, ← or_assoc, @or_comm (r c (f a)), or_assoc]
      simp

Premises used: Insert.insert, or_assoc
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Eq (α := Finset α) (fold (fun (x1 x2 : Finset α) ↦ x1 ∪ x2) ∅ singleton ∅) ∅

Tactic:
simp only [fold_empty]

Premises used: Finset.fold_empty