awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Finsupp
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
t : ι → Finset α
f : (i : ι) → i ∈ s → α
hf : f ∈ s.pi (β := fun (a : ι) ↦ α) t
i : ι
hi : i ∈ s
h : ((({ toFun := indicator s, inj' := ⋯ } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) f : ι →₀ α) : (a : ι) → α) i = f i hi
⊢ Membership.mem (α := α) (t i)
    (((({ toFun := indicator s, inj' := ⋯ } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) f : ι →₀ α) : (a : ι) → α) i : α)

Tactic:
convert! mem_pi.1 hf i hi

Premises used: Finset.mem_pi, Iff.mp
-- Module: Mathlib.Data.Finset.Finsupp
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
t : ι → Finset α
f : (i : ι) → i ∈ s → α
hf : f ∈ s.pi (β := fun (a : ι) ↦ α) t
i : ι
hi : i ∈ s
⊢ ((({ toFun := indicator s, inj' := ⋯ } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) f : ι →₀ α) : (a : ι) → α) i = f i hi

Tactic:
indicator_of_mem hi _

Premises used: Finsupp.indicator_of_mem
-- Module: Mathlib.Data.Finset.Finsupp
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
t : ι → Finset α
f : (i : ι) → i ∈ s → α
hf : f ∈ s.pi (β := fun (a : ι) ↦ α) t
i : ι
hi : i ∈ s
⊢ ((({ toFun := indicator s, inj' := ⋯ } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) f : ι →₀ α) : (a : ι) → α) i = f i hi

Tactic:
exact indicator_of_mem hi _

Premises used: Finsupp.indicator_of_mem
-- Module: Mathlib.Data.Finset.Finsupp
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
⊢ (f.support ⊆ s ∧ ∀ i ∈ s, Membership.mem (α := α) (t i) ((f : (a : ι) → α) i : α)) →
    ∃ a ∈ s.pi (β := fun (a : ι) ↦ α) t,
      ({ toFun := indicator s, inj' := ⋯ } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) a = f

Tactic:
fun h => ⟨fun i _ => f i, mem_pi.2 h.2, ?_⟩

Premises used: Iff.mpr, And.right, And.intro, Finset.mem_pi, Exists.intro, DFunLike.coe
-- Module: Mathlib.Data.Finset.Finsupp
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
refine_2 :
  ∀ (h : f.support ⊆ s ∧ ∀ i ∈ s, Membership.mem (α := α) (t i) ((f : (a : ι) → α) i : α)),
    (({ toFun := indicator s, inj' := ⋯ } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) fun (i : ι) (x : i ∈ s) ↦
        (f : (a : ι) → α) i) =
      f
⊢ (f.support ⊆ s ∧ ∀ i ∈ s, Membership.mem (α := α) (t i) ((f : (a : ι) → α) i : α)) →
    ∃ a ∈ s.pi (β := fun (a : ι) ↦ α) t,
      ({ toFun := indicator s, inj' := ⋯ } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) a = f

Tactic:
refine fun h => ⟨fun i _ => f i, mem_pi.2 h.2, ?_⟩
-- Module: Mathlib.Data.Finset.Finsupp
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
h : f.support ⊆ s ∧ ∀ i ∈ s, Membership.mem (α := α) (t i) ((f : (a : ι) → α) i : α)
refine_2 :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := α)
      ((({ toFun := indicator s, inj' := ⋯ } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) fun (i : ι) (x : i ∈ s) ↦
              (f : (a : ι) → α) i :
            (a : ι) → α)
          i :
        α)
      ((f : (a : ι) → α) i : α)
⊢ (({ toFun := indicator s, inj' := ⋯ } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) fun (i : ι) (x : i ∈ s) ↦
      (f : (a : ι) → α) i) =
    f

Tactic:
ext i
-- Module: Mathlib.Data.Finset.Finsupp
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
h : f.support ⊆ s ∧ ∀ i ∈ s, Membership.mem (α := α) (t i) ((f : (a : ι) → α) i : α)
i : ι
⊢ Eq.{u_2 + 1} (α := α)
    ((({ toFun := indicator s, inj' := ⋯ } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) fun (i : ι) (x : i ∈ s) ↦
            (f : (a : ι) → α) i :
          (a : ι) → α)
        i :
      α)
    ((f : (a : ι) → α) i : α)

Tactic:
ite_eq_left_iff.2 fun hi => (notMem_support_iff.1 fun H => hi <| h.1 H).symm

Premises used: Iff.mpr, ite_eq_left_iff, Finsupp.notMem_support_iff, dite, And.left, Iff.mp, Eq.symm, ite
-- Module: Mathlib.Data.Finset.Finsupp
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
h : f.support ⊆ s ∧ ∀ i ∈ s, Membership.mem (α := α) (t i) ((f : (a : ι) → α) i : α)
i : ι
⊢ Eq.{u_2 + 1} (α := α)
    ((({ toFun := indicator s, inj' := ⋯ } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) fun (i : ι) (x : i ∈ s) ↦
            (f : (a : ι) → α) i :
          (a : ι) → α)
        i :
      α)
    ((f : (a : ι) → α) i : α)

Tactic:
exact ite_eq_left_iff.2 fun hi => (notMem_support_iff.1 fun H => hi <| h.1 H).symm

Premises used: Iff.mpr, ite_eq_left_iff, Finsupp.notMem_support_iff, And.left, Iff.mp, Eq.symm
-- Module: Mathlib.Data.Finset.Finsupp
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 : α)
refine_2 refine_2₁ :
  (f.support ⊆ s ∧ ∀ i ∈ s, Membership.mem (α := α) (t i) ((f : (a : ι) → α) i : α)) →
    ∃ a ∈ s.pi (β := fun (a : ι) ↦ α) t,
      ({ toFun := indicator s, inj' := ⋯ } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) a = f
⊢ Membership.mem (γ := Finset (ι →₀ α)) (s.finsupp t) f ↔
    f.support ⊆ s ∧ ∀ i ∈ s, Membership.mem (α := α) (t i) ((f : (a : ι) → α) i : α)

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

Premises used: Iff.intro, Iff.trans, Finset.mem_map, rfl
-- Module: Mathlib.Data.Finset.Finsupp
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 : α)

Tactic:
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⟩⟩)

Premises used: Iff.mpr, Finsupp.mem_support_iff, Finset.mem_finsupp_iff, And.intro, Iff.intro, Iff.mp, forall_congr', Iff.trans, Iff.symm, forall_and
-- Module: Mathlib.Data.Finset.Finsupp
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 : α)
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 : α)
⊢ 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 : α)

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⟩⟩)

Premises used: Iff.mpr, Finsupp.mem_support_iff, Finset.mem_finsupp_iff, And.intro, Iff.intro, Iff.mp, forall_congr', Iff.trans, Iff.symm, forall_and
-- Module: Mathlib.Data.Finset.Finsupp
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 : α)
neg :
  ∀ (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 : α)

Tactic:
by_cases hi : i ∈ s
-- Module: Mathlib.Data.Finset.Finsupp
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 : α)

Tactic:
h.2 hi

Premises used: And.right
-- Module: Mathlib.Data.Finset.Finsupp
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 : α)

Tactic:
exact h.2 hi

Premises used: And.right
-- Module: Mathlib.Data.Finset.Finsupp
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
neg : Membership.mem (γ := Finset α) 0 0
⊢ Membership.mem.{u_2, u_2} (α := α) (γ := Finset α) ((t : (a : ι) → Finset α) i : Finset α) ((f : (a : ι) → α) i : α)

Tactic:
rw [notMem_support_iff.1 (mt h.1 hi), notMem_support_iff.1 fun H => hi <| ht H]

Premises used: Finsupp.notMem_support_iff, mt, And.left, Iff.mp
-- Module: Mathlib.Data.Finset.Finsupp
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 (γ := Finset α) 0 0

Tactic:
zero_mem_zero

Premises used: Finset.zero_mem_zero
-- Module: Mathlib.Data.Finset.Finsupp
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 (γ := Finset α) 0 0

Tactic:
exact zero_mem_zero

Premises used: Finset.zero_mem_zero
-- Module: Mathlib.Data.Finset.Finsupp
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 : α)
refine_2₁ refine_2₂ refine_2₃ 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 : α)
⊢ Eq.{u_2 + 1} (α := α) ((f : (a : ι) → α) i : α) (0 : α)

Tactic:
rwa [H, mem_zero] at h

Premises used: Finset.mem_zero
-- Module: Mathlib.Data.Finset.Finsupp
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
t : ι → Finset α
⊢ card (α := ι →₀ α) (s.finsupp t) = ∏ i ∈ s, #(t i)

Tactic:
(card_map _).trans <| card_pi _ _

Premises used: Finset.card_pi, Finset.card_map, Finset.finsupp, Eq.trans
-- Module: Mathlib.Data.Finset.Finsupp
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
t : ι → Finset α
⊢ card (α := ι →₀ α) (s.finsupp t) = ∏ i ∈ s, #(t i)

Tactic:
exact (card_map _).trans <| card_pi _ _

Premises used: Finset.card_pi, Finset.card_map, Eq.trans
-- Module: Mathlib.Data.Finset.Finsupp
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
t : ι → Finset α
⊢ card (α := ι →₀ α) (s.finsupp t) = ∏ i ∈ s, #(t i)

Tactic:
classical exact (card_map _).trans <| card_pi _ _

Premises used: Finset.card_pi, Finset.card_map, Eq.trans
-- Module: Mathlib.Data.Finset.Finsupp
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
f : Finsupp.{u_1, u_2} ι (Finset α)
g : ι →₀ α
⊢ g ∈ f.pi ↔
    ∀ (i : ι),
      Membership.mem.{u_2, u_2} (α := α) (γ := Finset α) ((f : (a : ι) → Finset α) i : Finset α)
        ((g : (a : ι) → α) i : α)

Tactic:
mem_finsupp_iff_of_support_subset <| Subset.refl _

Premises used: Set.Mem, Finset.Subset.refl, setOf, Finset.mem_finsupp_iff_of_support_subset
-- Module: Mathlib.Data.Finset.Finsupp
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
f : Finsupp.{u_1, u_2} ι (Finset α)
rw :
  Eq (α := ℕ) (∏ i ∈ f.support, card.{u_2} (α := α) ((f : (a : ι) → Finset α) i))
    (f.prod fun (i : ι) ↦ (↑(card.{u_2} (α := α) ((f : (a : ι) → Finset α) i)) : Finset α → ℕ))
⊢ #f.pi = f.prod fun (i : ι) ↦ (↑(card.{u_2} (α := α) ((f : (a : ι) → Finset α) i)) : Finset α → ℕ)

Tactic:
rw [pi, card_finsupp]

Premises used: Finsupp.pi, Finset.card_finsupp
-- Module: Mathlib.Data.Finset.Finsupp
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
f : Finsupp.{u_1, u_2} ι (Finset α)
i : ι
h : i ∈ f.support
⊢ card.{u_2} (α := α) ((f : (a : ι) → Finset α) i) =
    (fun (i : ι) ↦ ((↑(card.{u_2} (α := α) ((f : (a : ι) → Finset α) i)) : Finset α → ℕ) : Finset α → ℕ)) i
      ((f : (a : ι) → Finset α) i)

Tactic:
simp only [Pi.natCast_apply, Nat.cast_id]

Premises used: Nat.cast_id, Pi.natCast_apply
-- Module: Mathlib.Data.Finset.Finsupp
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
f : Finsupp.{u_1, u_2} ι (Finset α)
⊢ Eq (α := ℕ) (∏ i ∈ f.support, card.{u_2} (α := α) ((f : (a : ι) → Finset α) i))
    (f.prod fun (i : ι) ↦ (↑(card.{u_2} (α := α) ((f : (a : ι) → Finset α) i)) : Finset α → ℕ))

Tactic:
exact Finset.prod_congr rfl fun i _ => by simp only [Pi.natCast_apply, Nat.cast_id]

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
⊢ fold op b f ∅ = b

Tactic:
rfl

Premises used: Multiset.foldr, Finset.fold, List.foldr, rfl, Multiset.fold
-- 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 : α
h : a ∉ s
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))
⊢ fold op b f (cons a s h) = op (f a) (fold op b f s)

Tactic:
dsimp only [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 : α → β
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))
rw₂ 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))
⊢ 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:
rw [cons_val, Multiset.map_cons, fold_cons_left]

Premises used: Multiset.fold_cons_left, Multiset.map_cons, Finset.cons_val
-- 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 α
h : a ∉ s
unfold : Multiset.fold op b (Multiset.map f (insert a s).val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
⊢ fold op b f (insert a s) = op (f a) (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 : α → β
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))
rw₃ 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))
⊢ Multiset.fold op b (Multiset.map f (insert 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]

Premises used: Multiset.fold_cons_left, Finset.insert_val, Multiset.ndinsert_of_notMem, Multiset.map_cons
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
a : α
⊢ fold op b f {a} = op (f a) b

Tactic:
rfl

Premises used: Multiset.foldr, Finset.fold, List.foldr, rfl, Multiset.fold
-- 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 : β
g : γ ↪ α
s : Finset γ
⊢ fold op b f (map g s) = fold op b (f ∘ (⇑g : (a : γ) → α)) s

Tactic:
simp only [fold, map, Multiset.map_map]

Premises used: Finset.fold, Finset.map, 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 : β
inst : DecidableEq α
g : γ → α
s : Finset γ
H : Set.InjOn g (↑s : Set γ)
⊢ fold op b f (image g s) = fold op b (f ∘ g) s

Tactic:
simp only [fold, image_val_of_injOn H, Multiset.map_map]

Premises used: Finset.fold, Finset.image_val_of_injOn, Multiset.map_map
-- 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 : α → β
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)
rw₂ rw₃ : Multiset.fold op b (Multiset.map g s.val) = Multiset.fold op b (Multiset.map g s.val)
⊢ fold op b f s = fold op b g s

Tactic:
rw [fold, fold, map_congr rfl H]

Premises used: Finset.fold, Multiset.map_congr, rfl
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
s : Finset α
f g : α → β
b₁ b₂ : β
⊢ fold op (op b₁ b₂) (fun (x : α) ↦ op (f x) (g x)) s = op (fold op b₁ f s) (fold op b₂ g s)

Tactic:
simp only [fold, fold_distrib]

Premises used: Finset.fold, Multiset.fold_distrib
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : 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 (Eq.{u_1 + 1} (α := Finset α) ∅ ∅)
⊢ fold op b (fun (x : α) ↦ c) ∅ = if Eq.{u_1 + 1} (α := Finset α) ∅ ∅ then b else op b c

Tactic:
simp
-- Module: Mathlib.Data.Finset.Fold
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.insert x s = ∅)
insert : op c (if s = ∅ then b else op b c) = op b c
⊢ fold op b (fun (x : α) ↦ c) (Insert.insert x s) = if Insert.insert x s = ∅ then b else op b c

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

Premises used: if_false, Finset.insert_ne_empty, Finset.fold_insert
-- Module: Mathlib.Data.Finset.Fold
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
neg : ¬s = ∅ → op c (op b c) = op b c
⊢ op c (if s = ∅ then b else op b c) = op b c

Tactic:
split_ifs
-- Module: Mathlib.Data.Finset.Fold
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 = ∅
pos pos₁ : op b c = op b c
⊢ op c b = op b c

Tactic:
rw [hc.comm]

Premises used: Std.Commutative.comm
-- Module: Mathlib.Data.Finset.Fold
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 (op b c) = op b c

Tactic:
h
-- Module: Mathlib.Data.Finset.Fold
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 (op b c) = op b c

Tactic:
exact h
-- Module: Mathlib.Data.Finset.Fold
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
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.insert x s = ∅)],
    fold op b (fun (x : α) ↦ c) (Insert.insert x s) = if Insert.insert x s = ∅ then b else 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 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

Premises used: if_false, Insert.insert, Std.Commutative.comm, Finset.insert_ne_empty
-- Module: Mathlib.Data.Finset.Fold
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
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.insert x s = ∅)],
    fold op b (fun (x : α) ↦ c) (Insert.insert x s) = if Insert.insert x s = ∅ then b else op b c
⊢ fold op b (fun (x : α) ↦ c) s = if 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

Premises used: if_false, Insert.insert, Std.Commutative.comm, Finset.insert_ne_empty