awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.Finsupp (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
refine_1 :
  (∃ a ∈ s.pi (β := fun (a : ι) ↦ α) t,
      ({ toFun := indicator s, inj' := ⋯ } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) a = f) →
    f.support ⊆ s ∧ ∀ i ∈ s, Membership.mem (α := α) (t i) ((f : (a : ι) → α) i : α)
⊢ Membership.mem (γ := Finset (ι →₀ α)) (s.finsupp t) f ↔
    f.support ⊆ s ∧ ∀ i ∈ s, Membership.mem (α := α) (t i) ((f : (a : ι) → α) i : α)
have refine_2 : (f.support ⊆ s ∧ ∀ i ∈ s, Membership.mem (α := α) (t i) ((f : (a : ι) → α) i : α)) →
  ∃ a ∈ s.pi (β := fun (a : ι) ↦ α) t, ({ toFun := indicator s, inj' := sorry } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) a = f
Tactic: classical
  refine mem_map.trans ⟨?_, ?_⟩
  · rintro ⟨f, hf, rfl⟩
    refine ⟨support_indicator_subset _ _, fun i hi => ?_⟩
    convert! mem_pi.1 hf i hi
    exact indicator_of_mem hi _
  · refine fun h => ⟨fun i _ => f i, mem_pi.2 h.2, ?_⟩
    ext i
    exact ite_eq_left_iff.2 fun hi => (notMem_support_iff.1 fun H => hi <| h.1 H).symm
-- Lean 4 proof step from Mathlib.Data.Finset.Finsupp (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : ι →₀ α
t : Finsupp.{u_1, u_2} ι (Finset α)
ht : t.support ⊆ s
⊢ Membership.mem (γ := Finset (ι →₀ α)) (s.finsupp (⇑t : (a : ι) → Finset α)) f ↔
    ∀ (i : ι),
      Membership.mem.{u_2, u_2} (α := α) (γ := Finset α) ((t : (a : ι) → Finset α) i : Finset α)
        ((f : (a : ι) → α) i : α)
have refine_1 : ∀ (i : ι)
  (h :
    (i ∈ f.support → i ∈ s) ∧
      (i ∈ s →
        Membership.mem.{u_2, u_2} (α := α) (γ := Finset α) ((t : (a : ι) → Finset α) i : Finset α)
          ((f : (a : ι) → α) i : α))),
  Membership.mem.{u_2, u_2} (α := α) (γ := Finset α) ((t : (a : ι) → Finset α) i : Finset α) ((f : (a : ι) → α) i : α)
Tactic: refine
    mem_finsupp_iff.trans
      (forall_and.symm.trans <|
        forall_congr' fun i =>
          ⟨fun h => ?_, fun h =>
            ⟨fun hi => ht <| mem_support_iff.2 fun H => mem_support_iff.1 hi ?_, fun _ => h⟩⟩)
-- Lean 4 proof step from Mathlib.Data.Finset.Finsupp (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : ι →₀ α
t : Finsupp.{u_1, u_2} ι (Finset α)
ht : t.support ⊆ s
refine_1 :
  ∀ (i : ι)
    (h :
      (i ∈ f.support → i ∈ s) ∧
        (i ∈ s →
          Membership.mem.{u_2, u_2} (α := α) (γ := Finset α) ((t : (a : ι) → Finset α) i : Finset α)
            ((f : (a : ι) → α) i : α))),
    Membership.mem.{u_2, u_2} (α := α) (γ := Finset α) ((t : (a : ι) → Finset α) i : Finset α) ((f : (a : ι) → α) i : α)
⊢ Membership.mem (γ := Finset (ι →₀ α)) (s.finsupp (⇑t : (a : ι) → Finset α)) f ↔
    ∀ (i : ι),
      Membership.mem.{u_2, u_2} (α := α) (γ := Finset α) ((t : (a : ι) → Finset α) i : Finset α)
        ((f : (a : ι) → α) i : α)
have refine_2 : ∀ (i : ι)
  (h :
    Membership.mem.{u_2, u_2} (α := α) (γ := Finset α) ((t : (a : ι) → Finset α) i : Finset α)
      ((f : (a : ι) → α) i : α))
  (hi : i ∈ f.support) (H : Eq.{u_2 + 1} (α := Finset α) ((t : (a : ι) → Finset α) i : Finset α) (0 : Finset α)),
  Eq.{u_2 + 1} (α := α) ((f : (a : ι) → α) i : α) (0 : α)
Tactic: refine
    mem_finsupp_iff.trans
      (forall_and.symm.trans <|
        forall_congr' fun i =>
          ⟨fun h => ?_, fun h =>
            ⟨fun hi => ht <| mem_support_iff.2 fun H => mem_support_iff.1 hi ?_, fun _ => h⟩⟩)
-- Lean 4 proof step from Mathlib.Data.Finset.Finsupp (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : ι →₀ α
t : Finsupp.{u_1, u_2} ι (Finset α)
ht : t.support ⊆ s
i : ι
h :
  (i ∈ f.support → i ∈ s) ∧
    (i ∈ s →
      Membership.mem.{u_2, u_2} (α := α) (γ := Finset α) ((t : (a : ι) → Finset α) i : Finset α)
        ((f : (a : ι) → α) i : α))
⊢ Membership.mem.{u_2, u_2} (α := α) (γ := Finset α) ((t : (a : ι) → Finset α) i : Finset α) ((f : (a : ι) → α) i : α)
have pos : ∀ (hi : i ∈ s),
  Membership.mem.{u_2, u_2} (α := α) (γ := Finset α) ((t : (a : ι) → Finset α) i : Finset α) ((f : (a : ι) → α) i : α)
Tactic: by_cases hi : i ∈ s
-- Lean 4 proof step from Mathlib.Data.Finset.Finsupp (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : ι →₀ α
t : Finsupp.{u_1, u_2} ι (Finset α)
ht : t.support ⊆ s
i : ι
h :
  (i ∈ f.support → i ∈ s) ∧
    (i ∈ s →
      Membership.mem.{u_2, u_2} (α := α) (γ := Finset α) ((t : (a : ι) → Finset α) i : Finset α)
        ((f : (a : ι) → α) i : α))
pos :
  ∀ (hi : i ∈ s),
    Membership.mem.{u_2, u_2} (α := α) (γ := Finset α) ((t : (a : ι) → Finset α) i : Finset α) ((f : (a : ι) → α) i : α)
⊢ Membership.mem.{u_2, u_2} (α := α) (γ := Finset α) ((t : (a : ι) → Finset α) i : Finset α) ((f : (a : ι) → α) i : α)
have neg : ∀ (hi : i ∉ s),
  Membership.mem.{u_2, u_2} (α := α) (γ := Finset α) ((t : (a : ι) → Finset α) i : Finset α) ((f : (a : ι) → α) i : α)
Tactic: by_cases hi : i ∈ s
-- Lean 4 proof step from Mathlib.Data.Finset.Finsupp (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : ι →₀ α
t : Finsupp.{u_1, u_2} ι (Finset α)
ht : t.support ⊆ s
i : ι
h :
  (i ∈ f.support → i ∈ s) ∧
    (i ∈ s →
      Membership.mem.{u_2, u_2} (α := α) (γ := Finset α) ((t : (a : ι) → Finset α) i : Finset α)
        ((f : (a : ι) → α) i : α))
hi : i ∉ s
⊢ Membership.mem.{u_2, u_2} (α := α) (γ := Finset α) ((t : (a : ι) → Finset α) i : Finset α) ((f : (a : ι) → α) i : α)
have neg : Membership.mem (γ := Finset α) 0 0
Tactic: rw [notMem_support_iff.1 (mt h.1 hi), notMem_support_iff.1 fun H => hi <| ht H]
-- Lean 4 proof step from Mathlib.Data.Finset.Finsupp (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : ι →₀ α
t : Finsupp.{u_1, u_2} ι (Finset α)
ht : t.support ⊆ s
i : ι
h : Membership.mem.{u_2, u_2} (α := α) (γ := Finset α) ((t : (a : ι) → Finset α) i : Finset α) ((f : (a : ι) → α) i : α)
hi : i ∈ f.support
H : Eq.{u_2 + 1} (α := Finset α) ((t : (a : ι) → Finset α) i : Finset α) (0 : Finset α)
⊢ Eq.{u_2 + 1} (α := α) ((f : (a : ι) → α) i : α) (0 : α)
have refine_2 : ∀ (h : Membership.mem.{u_2, u_2} (α := α) (γ := Finset α) 0 ((f : (a : ι) → α) i : α)) (hi : i ∈ f.support)
  (H : Eq.{u_2 + 1} (α := Finset α) ((t : (a : ι) → Finset α) i : Finset α) (0 : Finset α)),
  Eq.{u_2 + 1} (α := α) ((f : (a : ι) → α) i : α) (0 : α)
Tactic: rwa [H, mem_zero] at h
Cleared hypotheses: h, hi, H
-- Lean 4 proof step from Mathlib.Data.Finset.Finsupp (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : ι →₀ α
t : Finsupp.{u_1, u_2} ι (Finset α)
ht : t.support ⊆ s
i : ι
h : Membership.mem.{u_2, u_2} (α := α) (γ := Finset α) ((t : (a : ι) → Finset α) i : Finset α) ((f : (a : ι) → α) i : α)
hi : i ∈ f.support
H : Eq.{u_2 + 1} (α := Finset α) ((t : (a : ι) → Finset α) i : Finset α) (0 : Finset α)
refine_2 :
  ∀ (h : Membership.mem.{u_2, u_2} (α := α) (γ := Finset α) 0 ((f : (a : ι) → α) i : α)) (hi : i ∈ f.support)
    (H : Eq.{u_2 + 1} (α := Finset α) ((t : (a : ι) → Finset α) i : Finset α) (0 : Finset α)),
    Eq.{u_2 + 1} (α := α) ((f : (a : ι) → α) i : α) (0 : α)
⊢ Eq.{u_2 + 1} (α := α) ((f : (a : ι) → α) i : α) (0 : α)
have refine_2₁ : ∀ (h : Eq.{u_2 + 1} (α := α) ((f : (a : ι) → α) i : α) (0 : α)) (hi : i ∈ f.support)
  (H : Eq.{u_2 + 1} (α := Finset α) ((t : (a : ι) → Finset α) i : Finset α) (0 : Finset α)),
  Eq.{u_2 + 1} (α := α) ((f : (a : ι) → α) i : α) (0 : α)
Tactic: rwa [H, mem_zero] at h
Cleared hypotheses: h, hi, H
-- Lean 4 proof step from Mathlib.Data.Finset.Finsupp (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
f : Finsupp.{u_1, u_2} ι (Finset α)
⊢ #f.pi = f.prod fun (i : ι) ↦ (↑(card.{u_2} (α := α) ((f : (a : ι) → Finset α) i)) : Finset α → ℕ)
have rw : Eq (α := ℕ) (∏ i ∈ f.support, card.{u_2} (α := α) ((f : (a : ι) → Finset α) i))
  (f.prod fun (i : ι) ↦ (↑(card.{u_2} (α := α) ((f : (a : ι) → Finset α) i)) : Finset α → ℕ))
Tactic: rw [pi, card_finsupp]
-- 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 : α
h : a ∉ s
⊢ fold op b f (cons a s h) = op (f a) (fold op b f s)
have dsimp : Multiset.fold op b (Multiset.map f (cons a s h).val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
Tactic: dsimp only [fold]
-- 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 : α
h : a ∉ s
⊢ Multiset.fold op b (Multiset.map f (cons a s h).val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
have rw : Multiset.fold op b (Multiset.map f (a ::ₘ s.val)) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
Tactic: rw [cons_val, Multiset.map_cons, fold_cons_left]
-- 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 : α
h : a ∉ s
rw : Multiset.fold op b (Multiset.map f (a ::ₘ s.val)) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
⊢ Multiset.fold op b (Multiset.map f (cons a s h).val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
have rw₁ : Multiset.fold op b (f a ::ₘ Multiset.map f s.val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
Tactic: rw [cons_val, Multiset.map_cons, fold_cons_left]
-- 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 : α
h : a ∉ s
rw : Multiset.fold op b (Multiset.map f (a ::ₘ s.val)) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
rw₁ : Multiset.fold op b (f a ::ₘ Multiset.map f s.val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
⊢ Multiset.fold op b (Multiset.map f (cons a s h).val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
have rw₂ : op (f a) (Multiset.fold op b (Multiset.map f s.val)) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
Tactic: rw [cons_val, Multiset.map_cons, fold_cons_left]
-- 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 α
h : a ∉ s
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)
have unfold : Multiset.fold op b (Multiset.map f (insert a s).val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
Tactic: unfold fold
-- 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 α
h : a ∉ s
⊢ Multiset.fold op b (Multiset.map f (insert a s).val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
have rw : Multiset.fold op b (Multiset.map f (ndinsert a s.val)) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
Tactic: rw [insert_val, ndinsert_of_notMem h, Multiset.map_cons, fold_cons_left]
-- 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 α
h : a ∉ s
rw : Multiset.fold op b (Multiset.map f (ndinsert a s.val)) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
⊢ Multiset.fold op b (Multiset.map f (insert a s).val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
have rw₁ : Multiset.fold op b (Multiset.map f (a ::ₘ s.val)) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
Tactic: rw [insert_val, ndinsert_of_notMem h, Multiset.map_cons, fold_cons_left]
-- 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 α
h : a ∉ s
rw : Multiset.fold op b (Multiset.map f (ndinsert a s.val)) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
rw₁ : Multiset.fold op b (Multiset.map f (a ::ₘ s.val)) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
⊢ Multiset.fold op b (Multiset.map f (insert a s).val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
have rw₂ : Multiset.fold op b (f a ::ₘ Multiset.map f s.val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
Tactic: rw [insert_val, ndinsert_of_notMem h, Multiset.map_cons, fold_cons_left]
-- 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 α
h : a ∉ s
rw : Multiset.fold op b (Multiset.map f (ndinsert a s.val)) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
rw₁ : Multiset.fold op b (Multiset.map f (a ::ₘ s.val)) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
rw₂ : Multiset.fold op b (f a ::ₘ Multiset.map f s.val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
⊢ Multiset.fold op b (Multiset.map f (insert a s).val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
have rw₃ : op (f a) (Multiset.fold op b (Multiset.map f s.val)) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
Tactic: rw [insert_val, ndinsert_of_notMem h, Multiset.map_cons, fold_cons_left]
-- 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 : α → β
H : ∀ x ∈ s, f x = g x
⊢ fold op b f s = fold op b g s
have rw : Multiset.fold op b (Multiset.map f s.val) = fold op b g s
Tactic: rw [fold, fold, map_congr rfl 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 : Finset α
g : α → β
H : ∀ x ∈ s, f x = g x
rw : Multiset.fold op b (Multiset.map f s.val) = fold op b g s
⊢ fold op b f s = fold op b g s
have rw₁ : Multiset.fold op b (Multiset.map f s.val) = Multiset.fold op b (Multiset.map g s.val)
Tactic: rw [fold, fold, map_congr rfl 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 : Finset α
g : α → β
H : ∀ x ∈ s, f x = g x
rw : Multiset.fold op b (Multiset.map f s.val) = fold op b g s
rw₁ : Multiset.fold op b (Multiset.map f s.val) = Multiset.fold op b (Multiset.map g s.val)
⊢ fold op b f s = fold op b g s
have rw₂ : Multiset.fold op b (Multiset.map g s.val) = Multiset.fold op b (Multiset.map g s.val)
Tactic: rw [fold, fold, map_congr rfl 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
b : β
s_1 : 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
have insert : op c (if s = ∅ then b else op b c) = op b c
Tactic: simp only [Finset.fold_insert hx, IH, if_false, Finset.insert_ne_empty]
-- 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
b : β
s_1 : 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
have pos : s = ∅ → op c b = op b c
Tactic: split_ifs
-- 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
b : β
s_1 : 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 = ∅)
pos : s = ∅ → op c b = op b c
⊢ op c (if s = ∅ then b else op b c) = op b c
have neg : ¬s = ∅ → op c (op b c) = op b c
Tactic: split_ifs
-- 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
b : β
s_1 : 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_1 : s = ∅
⊢ op c b = op b c
have pos : op b c = op b c
Tactic: rw [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
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
have empty : ∀ [hd : Decidable (Eq.{u_1 + 1} (α := Finset α) ∅ ∅)],
  fold op b (fun (x : α) ↦ c) ∅ = if Eq.{u_1 + 1} (α := Finset α) ∅ ∅ then b else op b c
Tactic: induction s using Finset.induction_on generalizing hd with
    | empty => simp
    | insert x s hx IH =>
      simp only [Finset.fold_insert hx, IH, if_false, Finset.insert_ne_empty]
      split_ifs
      · rw [hc.comm]
      · exact h
Cleared hypotheses: hd
-- 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
b : β
s : Finset α
hd : Decidable (s = ∅)
c : β
h : op c (op b c) = op b c
empty :
  ∀ [hd : Decidable (Eq.{u_1 + 1} (α := Finset α) ∅ ∅)],
    fold op b (fun (x : α) ↦ c) ∅ = if Eq.{u_1 + 1} (α := Finset α) ∅ ∅ then b else op b c
⊢ fold op b (fun (x : α) ↦ c) s = if s = ∅ then b else op b c
have insert : ∀ (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: induction s using Finset.induction_on generalizing hd with
    | empty => simp
    | insert x s hx IH =>
      simp only [Finset.fold_insert hx, IH, if_false, Finset.insert_ne_empty]
      split_ifs
      · rw [hc.comm]
      · exact h
Cleared hypotheses: hd
-- 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
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
have empty : ∀ [hd : Decidable (Eq.{u_1 + 1} (α := Finset α) ∅ ∅)],
  fold op b (fun (x : α) ↦ c) ∅ = if Eq.{u_1 + 1} (α := Finset α) ∅ ∅ then b else op b c
Tactic: classical
    induction s using Finset.induction_on generalizing hd with
    | empty => simp
    | insert x s hx IH =>
      simp only [Finset.fold_insert hx, IH, if_false, Finset.insert_ne_empty]
      split_ifs
      · rw [hc.comm]
      · exact h
Cleared hypotheses: hd
-- 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
b : β
s : Finset α
hd : Decidable (s = ∅)
c : β
h : op c (op b c) = op b c
empty :
  ∀ [hd : Decidable (Eq.{u_1 + 1} (α := Finset α) ∅ ∅)],
    fold op b (fun (x : α) ↦ c) ∅ = if Eq.{u_1 + 1} (α := Finset α) ∅ ∅ then b else op b c
⊢ fold op b (fun (x : α) ↦ c) s = if s = ∅ then b else op b c
have insert : ∀ (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: classical
    induction s using Finset.induction_on generalizing hd with
    | empty => simp
    | insert x s hx IH =>
      simp only [Finset.fold_insert hx, IH, if_false, Finset.insert_ne_empty]
      split_ifs
      · rw [hc.comm]
      · exact h
Cleared hypotheses: hd
-- 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 : β
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)
⊢ fold op' (m b) (fun (x : α) ↦ m (f x)) s = m (fold op b f s)
have 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)
Tactic: rw [fold, fold, ← Multiset.fold_hom op hm, Multiset.map_map]
-- 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₂ : β
⊢ op (fold op b₁ f (s₁ ∪ s₂)) (fold op b₂ f (s₁ ∩ s₂)) = op (fold op b₂ f s₁) (fold op b₁ f s₂)
have 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))
Tactic: unfold fold
-- 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₂ : β
⊢ 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₁ ∪ 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))
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))
⊢ 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₁ ∪ s₂).val + (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]
-- 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))
⊢ 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₁ ∩ 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]