awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
P : Type u_11
inst : AddZeroClass M
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
g : N →+ P
f : α → M →+ N
a : α
rw : AddMonoidHom.comp (g.comp ((liftAddHom : (a : α → M →+ N) → (α →₀ M) →+ N) f)) (singleAddHom a) = g.comp (f a)
rw₁ : g.comp (AddMonoidHom.comp ((liftAddHom : (a : α → M →+ N) → (α →₀ M) →+ N) f) (singleAddHom a)) = g.comp (f a)
rw₂ rw₃ : g.comp (f a) = g.comp (f a)
⊢ (AddEquiv.symm liftAddHom : (a : (α →₀ M) →+ P) → α → M →+ P)
      (g.comp ((liftAddHom : (a : α → M →+ N) → (α →₀ M) →+ N) f)) a =
    g.comp (f a)

Tactic:
rw [liftAddHom_symm_apply, AddMonoidHom.comp_assoc, liftAddHom_comp_single]

Premises used: Finsupp.liftAddHom_comp_single, AddMonoidHom.comp_assoc, Finsupp.liftAddHom_symm_apply
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
γ : Type u_3
β : Type u_7
inst : AddGroup β
inst_1 : AddCommGroup γ
f g : α →₀ β
h : α → β → γ
h_sub : ∀ (a : α) (b₁ b₂ : β), h a (b₁ - b₂) = h a b₁ - h a b₂
⊢ (f - g).sum h = f.sum h - g.sum h

Tactic:
((liftAddHom (α := α) (M := β) (N := γ)) fun a =>
    AddMonoidHom.ofMapSub (h a) (h_sub a)).map_sub f g

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, AddMonoidHom.ofMapSub, AddMonoidHom.map_sub, DFunLike.coe, Finset.sum, Finsupp.liftAddHom
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_7
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
v : α →₀ M
f : α ↪ β
g : β → M → N
rw :
  Eq.{u_10 + 1} (α := N)
    (∏ x ∈ v.support, g ((f : (a : α) → β) x) ((embDomain f v : (a : β) → M) ((f : (a : α) → β) x : β)))
    (∏ a ∈ v.support, g ((f : (a : α) → β) a) ((v : (a : α) → M) a))
⊢ (embDomain f v).prod g = v.prod fun (a : α) (b : M) ↦ g ((f : (a : α) → β) a) b

Tactic:
rw [prod, prod, support_embDomain, Finset.prod_map]

Premises used: Finset.prod_map, Finsupp.support_embDomain, Finsupp.prod
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_7
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
v : α →₀ M
f : α ↪ β
g : β → M → N
⊢ Eq.{u_10 + 1} (α := N)
    (∏ x ∈ v.support, g ((f : (a : α) → β) x) ((embDomain f v : (a : β) → M) ((f : (a : α) → β) x : β)))
    (∏ a ∈ v.support, g ((f : (a : α) → β) a) ((v : (a : α) → M) a))

Tactic:
simp_rw [embDomain_apply_self]

Premises used: Finsupp.embDomain_apply_self
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
ι : Type u_2
M : Type u_8
N : Type u_10
inst : AddCommMonoid M
inst_1 : CommMonoid N
s_1 : Finset ι
g : ι → α →₀ M
h : α → M → N
h_zero : ∀ (a : α), h a 0 = 1
h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
a : ι
s : Finset ι
has : a ∉ s
ih : ∏ i ∈ s, (g i).prod h = prod (∑ i ∈ s, g i) h
rw : (g a).prod h * ∏ x ∈ s, (g x).prod h = prod (∑ i ∈ cons a s has, g i) h
rw₁ : (g a).prod h * prod (∑ i ∈ s, g i) h = prod (∑ i ∈ cons a s has, g i) h
rw₂ : (g a).prod h * prod (∑ i ∈ s, g i) h = (g a + ∑ x ∈ s, g x).prod h
rw₃ rw₄ : (g a).prod h * prod (∑ i ∈ s, g i) h = (g a).prod h * prod (∑ x ∈ s, g x) h
⊢ ∏ i ∈ cons a s has, (g i).prod h = prod (∑ i ∈ cons a s has, g i) h

Tactic:
rw [prod_cons, ih, sum_cons, prod_add_index' h_zero h_add]

Premises used: Finset.sum_cons, Finsupp.prod_add_index', Finset.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_7
M : Type u_8
N : Type u_10
P : Type u_11
inst : Zero M
inst_1 : AddCommMonoid N
inst_2 : CommMonoid P
f : α →₀ M
g : α → M → β →₀ N
h : β → N → P
h_zero : ∀ (a : β), h a 0 = 1
h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ (f.sum g).prod h = f.prod fun (a : α) (b : M) ↦ (g a b).prod h

Tactic:
(prod_finsetSum_index h_zero h_add).symm

Premises used: Finsupp.sum, Eq.symm, Finsupp.prod_finsetSum_index, Finsupp.prod
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
f : Multiset (α →₀ M)
h : α → M → N
h₀ : ∀ (a : α), h a 0 = 0
h₁ : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂
a : α →₀ M
s : Multiset (α →₀ M)
ih : s.sum.sum h = Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) s)
rw : (a + s.sum).sum h = Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) (a ::ₘ s))
rw₁ : (a + s.sum).sum h = (a.sum h ::ₘ Multiset.map (fun (g : α →₀ M) ↦ g.sum h) s).sum
rw₂ : (a + s.sum).sum h = a.sum h + Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) s)
rw₃ : a.sum h + s.sum.sum h = a.sum h + Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) s)
rw₄ rw₅ :
  a.sum h + Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) s) =
    a.sum h + Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) s)
⊢ (a ::ₘ s).sum.sum h = Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) (a ::ₘ s))

Tactic:
rw [Multiset.sum_cons, Multiset.map_cons, Multiset.sum_cons, sum_add_index' h₀ h₁, ih]

Premises used: Multiset.map_cons, Finsupp.sum_add_index', Multiset.sum_cons
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_16
ι : Type u_17
M : Type u_18
inst : DecidableEq α
inst_1 : AddCommMonoid M
g : ι → α →₀ M
s : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
⊢ Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ s, g i)) (s.biUnion fun (i : ι) ↦ (g i).support)

Tactic:
Finset.induction_on s ?_ ?_

Premises used: Finset.induction_on
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_16
ι : Type u_17
M : Type u_18
inst : DecidableEq α
inst_1 : AddCommMonoid M
g : ι → α →₀ M
s : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
refine_1 :
  Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ ∅, g i))
    (Finset.biUnion ∅ fun (i : ι) ↦ (g i).support)
refine_2 :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ s, g i))
          (s.biUnion fun (i : ι) ↦ (g i).support) →
        Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ insert a s, g i))
          ((insert a s).biUnion fun (i : ι) ↦ (g i).support)
⊢ Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ s, g i)) (s.biUnion fun (i : ι) ↦ (g i).support)

Tactic:
refine Finset.induction_on s ?_ ?_
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_16
ι : Type u_17
M : Type u_18
inst : DecidableEq α
inst_1 : AddCommMonoid M
g : ι → α →₀ M
s : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
⊢ Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ ∅, g i))
    (Finset.biUnion ∅ fun (i : ι) ↦ (g i).support)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_16
ι : Type u_17
M : Type u_18
inst : DecidableEq α
inst_1 : AddCommMonoid M
g : ι → α →₀ M
s_1 : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
refine_2 :
  Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ s, g i)) (s.biUnion fun (i : ι) ↦ (g i).support) →
    (g i + ∑ i ∈ s, g i).support = (g i).support ∪ s.biUnion fun (i : ι) ↦ (g i).support
⊢ Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ s, g i)) (s.biUnion fun (i : ι) ↦ (g i).support) →
    Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ insert i s, g i))
      ((insert i s).biUnion fun (i : ι) ↦ (g i).support)

Tactic:
simp only [hi, sum_insert, not_false_iff, biUnion_insert]

Premises used: Finset.biUnion_insert, Finset.sum_insert, not_false_iff
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_16
ι : Type u_17
M : Type u_18
inst : DecidableEq α
inst_1 : AddCommMonoid M
g : ι → α →₀ M
s_1 : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
hs :
  Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ s, g i)) (s.biUnion fun (i : ι) ↦ (g i).support)
refine_2 : Disjoint (g i).support (support.{u_16, u_18} (M := M) (∑ i ∈ s, g i))
⊢ (g i + ∑ i ∈ s, g i).support = (g i).support ∪ s.biUnion fun (i : ι) ↦ (g i).support

Tactic:
rw [Finsupp.support_add_eq, hs]

Premises used: Finsupp.support_add_eq
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_16
ι : Type u_17
M : Type u_18
inst : DecidableEq α
inst_1 : AddCommMonoid M
g : ι → α →₀ M
s_1 : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
hs :
  Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ s, g i)) (s.biUnion fun (i : ι) ↦ (g i).support)
refine_2 : ∀ i_1 ∈ s, Disjoint (g i).support (g i_1).support
⊢ Disjoint (g i).support (support.{u_16, u_18} (M := M) (∑ i ∈ s, g i))

Tactic:
rw [hs, Finset.disjoint_biUnion_right]

Premises used: Finset.disjoint_biUnion_right
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_16
ι : Type u_17
M : Type u_18
inst : DecidableEq α
inst_1 : AddCommMonoid M
g : ι → α →₀ M
s_1 : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
hs :
  Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ s, g i)) (s.biUnion fun (i : ι) ↦ (g i).support)
j : ι
hj : j ∈ s
⊢ Disjoint (g i).support (g j).support

Tactic:
h _ _ (ne_of_mem_of_not_mem hj hi).symm

Premises used: Ne.symm, ne_of_mem_of_not_mem
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_16
ι : Type u_17
M : Type u_18
inst : DecidableEq α
inst_1 : AddCommMonoid M
g : ι → α →₀ M
s_1 : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
hs :
  Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ s, g i)) (s.biUnion fun (i : ι) ↦ (g i).support)
j : ι
hj : j ∈ s
⊢ Disjoint (g i).support (g j).support

Tactic:
exact h _ _ (ne_of_mem_of_not_mem hj hi).symm

Premises used: Ne.symm, ne_of_mem_of_not_mem
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_16
ι : Type u_17
M : Type u_18
inst : DecidableEq α
inst_1 : AddCommMonoid M
g : ι → α →₀ M
s : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
refine_1 :
  Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ ∅, g i))
    (Finset.biUnion ∅ fun (i : ι) ↦ (g i).support)
refine_2 refine_2₁ :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ s, g i))
          (s.biUnion fun (i : ι) ↦ (g i).support) →
        Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ insert a s, g i))
          ((insert a s).biUnion fun (i : ι) ↦ (g i).support)
⊢ Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ s, g i)) (s.biUnion fun (i : ι) ↦ (g i).support)

Tactic:
classical
  refine Finset.induction_on s ?_ ?_
  · simp
  · intro i s hi
    simp only [hi, sum_insert, not_false_iff, biUnion_insert]
    intro hs
    rw [Finsupp.support_add_eq, hs]
    rw [hs, Finset.disjoint_biUnion_right]
    intro j hj
    exact h _ _ (ne_of_mem_of_not_mem hj hi).symm

Premises used: Finsupp.support_add_eq, Finset.biUnion_insert, Finset.disjoint_biUnion_right, Finset.sum_insert, not_false_iff
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
γ : Type u_3
β : Type u_7
M : Type u_8
inst : Zero M
f : α →₀ M
m : β → γ
h : α → M → Multiset β
⊢ Multiset.map m (f.sum h) = f.sum fun (a : α) (b : M) ↦ Multiset.map m (h a b)

Tactic:
map_sum (Multiset.mapAddMonoidHom m) _ f.support

Premises used: Multiset.map, Finsupp.sum, Finsupp.support, map_sum, Multiset.mapAddMonoidHom
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : AddCommMonoid N
f : α →₀ M
h : α → M → Multiset N
⊢ (f.sum h).sum = f.sum fun (a : α) (b : M) ↦ (h a b).sum

Tactic:
map_sum Multiset.sumAddMonoidHom _ f.support

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, Finsupp.support, map_sum, Multiset.sumAddMonoidHom
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
f1 f2 : α →₀ M
hd_1 : Disjoint f1.support f2.support
β : Type u_16
inst_1 : CommMonoid β
g : α → M → β
f1_1 f2_1 : α →₀ M
hd : Disjoint f1_1.support f2_1.support
x : α
hx : x ∈ f1_1.support
⊢ g x (HAdd.hAdd (α := M) (β := M) ((f1_1 : (a : α) → M) x : M) ((f2_1 : (a : α) → M) x : M)) =
    g x ((f1_1 : (a : α) → M) x)

Tactic:
simp only [notMem_support_iff.mp (disjoint_left.mp hd hx), add_zero]

Premises used: Finsupp.notMem_support_iff, Iff.mp, Finset.disjoint_left, add_zero
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
f1 f2 : α →₀ M
hd : Disjoint f1.support f2.support
β : Type u_16
inst_1 : CommMonoid β
g : α → M → β
⊢ ∀ {f1 f2 : α →₀ M},
    Disjoint f1.support f2.support →
      ∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)) =
        f1.prod g

Tactic:
have :
    ∀ {f1 f2 : α →₀ M},
      Disjoint f1.support f2.support → (∏ x ∈ f1.support, g x (f1 x + f2 x)) = f1.prod g :=
    fun hd =>
    Finset.prod_congr rfl fun x hx => by
      simp only [notMem_support_iff.mp (disjoint_left.mp hd hx), add_zero]
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
f1 f2 : α →₀ M
hd : Disjoint f1.support f2.support
β : Type u_16
inst_1 : CommMonoid β
g : α → M → β
this :
  ∀ {f1 f2 : α →₀ M},
    Disjoint f1.support f2.support →
      ∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)) =
        f1.prod g
simp_rw :
  (f1 + f2).prod g =
    (∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M))) *
      f2.prod g
simp_rw₁ :
  (f1 + f2).prod g =
    HMul.hMul (α := β)
      (∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)))
      (∏ x ∈ f2.support, g x (HAdd.hAdd (α := M) (β := M) ((f2 : (a : α) → M) x : M) ((f1 : (a : α) → M) x : M)))
simp_rw₂ :
  (f1 + f2).prod g =
    HMul.hMul (α := β)
      (∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)))
      (∏ x ∈ f2.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)))
simp_rw₃ :
  ∏ a ∈ (f1 + f2).support, g a ((f1 + f2 : (a : α) → M) a) =
    HMul.hMul (α := β)
      (∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)))
      (∏ x ∈ f2.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)))
simp_rw₄ :
  ∏ x ∈ f1.support ∪ f2.support, g x ((f1 + f2 : (a : α) → M) x) =
    HMul.hMul (α := β)
      (∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)))
      (∏ x ∈ f2.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)))
simp_rw₅ :
  HMul.hMul (α := β) (∏ x ∈ f1.support, g x ((f1 + f2 : (a : α) → M) x))
      (∏ x ∈ f2.support, g x ((f1 + f2 : (a : α) → M) x)) =
    HMul.hMul (α := β)
      (∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)))
      (∏ x ∈ f2.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)))
⊢ (f1 + f2).prod g = f1.prod g * f2.prod g

Tactic:
simp_rw [← this hd, ← this hd.symm, add_comm (f2 _), Finsupp.prod, support_add_eq hd,
      prod_union hd, add_apply]

Premises used: Finsupp.add_apply, Finsupp.support_add_eq, Finset.prod_union, add_comm, Disjoint.symm, DFunLike.coe, Finsupp.prod
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
f1 f2 : α →₀ M
hd : Disjoint f1.support f2.support
β : Type u_16
inst_1 : CommMonoid β
g : α → M → β
this :
  ∀ {f1 f2 : α →₀ M},
    Disjoint f1.support f2.support →
      ∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)) =
        f1.prod g
classical :
  (f1 + f2).prod g =
    (∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M))) *
      f2.prod g
classical₁ :
  (f1 + f2).prod g =
    HMul.hMul (α := β)
      (∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)))
      (∏ x ∈ f2.support, g x (HAdd.hAdd (α := M) (β := M) ((f2 : (a : α) → M) x : M) ((f1 : (a : α) → M) x : M)))
classical₂ :
  (f1 + f2).prod g =
    HMul.hMul (α := β)
      (∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)))
      (∏ x ∈ f2.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)))
classical₃ :
  ∏ a ∈ (f1 + f2).support, g a ((f1 + f2 : (a : α) → M) a) =
    HMul.hMul (α := β)
      (∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)))
      (∏ x ∈ f2.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)))
classical₄ :
  ∏ x ∈ f1.support ∪ f2.support, g x ((f1 + f2 : (a : α) → M) x) =
    HMul.hMul (α := β)
      (∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)))
      (∏ x ∈ f2.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)))
classical₅ :
  HMul.hMul (α := β) (∏ x ∈ f1.support, g x ((f1 + f2 : (a : α) → M) x))
      (∏ x ∈ f2.support, g x ((f1 + f2 : (a : α) → M) x)) =
    HMul.hMul (α := β)
      (∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)))
      (∏ x ∈ f2.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)))
⊢ (f1 + f2).prod g = f1.prod g * f2.prod g

Tactic:
classical simp_rw [← this hd, ← this hd.symm, add_comm (f2 _), Finsupp.prod, support_add_eq hd,
      prod_union hd, add_apply]

Premises used: Finsupp.add_apply, add_comm, Disjoint.symm, DFunLike.coe, Finsupp.prod
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a) ∣ g2 a ((f2 : (a : α) → M) a)
simp :
  Dvd.dvd.{u_10} (α := N) (∏ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a))
    (∏ a ∈ f2.support, g2 a ((f2 : (a : α) → M) a))
⊢ f1.prod g1 ∣ f2.prod g2

Tactic:
simp only [Finsupp.prod]

Premises used: Finsupp.prod
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a) ∣ g2 a ((f2 : (a : α) → M) a)
rw :
  ∏ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a) ∣
    HMul.hMul (α := N) (∏ x ∈ f2.support \ f1.support, g2 x ((f2 : (a : α) → M) x))
      (∏ x ∈ f1.support, g2 x ((f2 : (a : α) → M) x))
⊢ Dvd.dvd.{u_10} (α := N) (∏ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a))
    (∏ a ∈ f2.support, g2 a ((f2 : (a : α) → M) a))

Tactic:
rw [← sdiff_union_of_subset h1, prod_union sdiff_disjoint]

Premises used: Finset.prod_union, Finset.sdiff_union_of_subset, Finset.sdiff_disjoint
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a) ∣ g2 a ((f2 : (a : α) → M) a)
h :
  Dvd.dvd.{u_10} (α := N) (∏ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a))
    (∏ x ∈ f1.support, g2 x ((f2 : (a : α) → M) x))
⊢ ∏ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a) ∣
    HMul.hMul (α := N) (∏ x ∈ f2.support \ f1.support, g2 x ((f2 : (a : α) → M) x))
      (∏ x ∈ f1.support, g2 x ((f2 : (a : α) → M) x))

Tactic:
apply dvd_mul_of_dvd_right

Premises used: dvd_mul_of_dvd_right
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 h : ∀ i ∈ f1.support, g1 i ((f1 : (a : α) → M) i) ∣ g2 i ((f2 : (a : α) → M) i)
⊢ Dvd.dvd.{u_10} (α := N) (∏ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a))
    (∏ x ∈ f1.support, g2 x ((f2 : (a : α) → M) x))

Tactic:
apply prod_dvd_prod_of_dvd

Premises used: Finset.prod_dvd_prod_of_dvd
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a) ∣ g2 a ((f2 : (a : α) → M) a)
⊢ ∀ i ∈ f1.support, g1 i ((f1 : (a : α) → M) i) ∣ g2 i ((f2 : (a : α) → M) i)

Tactic:
h2
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a) ∣ g2 a ((f2 : (a : α) → M) a)
⊢ ∀ i ∈ f1.support, g1 i ((f1 : (a : α) → M) i) ∣ g2 i ((f2 : (a : α) → M) i)

Tactic:
exact h2
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a) ∣ g2 a ((f2 : (a : α) → M) a)
simp :
  Dvd.dvd.{u_10} (α := N) (∏ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a))
    (∏ a ∈ f2.support, g2 a ((f2 : (a : α) → M) a))
simp₁ :
  ∏ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a) ∣
    HMul.hMul (α := N) (∏ x ∈ f2.support \ f1.support, g2 x ((f2 : (a : α) → M) x))
      (∏ x ∈ f1.support, g2 x ((f2 : (a : α) → M) x))
h :
  Dvd.dvd.{u_10} (α := N) (∏ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a))
    (∏ x ∈ f1.support, g2 x ((f2 : (a : α) → M) x))
h₁ : ∀ i ∈ f1.support, g1 i ((f1 : (a : α) → M) i) ∣ g2 i ((f2 : (a : α) → M) i)
⊢ f1.prod g1 ∣ f2.prod g2

Tactic:
classical
    simp only [Finsupp.prod]
    rw [← sdiff_union_of_subset h1, prod_union sdiff_disjoint]
    apply dvd_mul_of_dvd_right
    apply prod_dvd_prod_of_dvd
    exact h2

Premises used: dvd_mul_of_dvd_right, Finset.prod_dvd_prod_of_dvd, Finset.prod_union, Finset.sdiff_disjoint, Finsupp.prod
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
rw :
  Eq (α := α →₀ M) (∑ x ∈ s.attach, single (↑x : α) ((indicator s f : (a : α) → M) (↑x : α)))
    (∑ x ∈ s.attach, single (↑x : α) (f (↑x : α) ⋯))
rw₁ :
  ∀ x ∈ s,
    x ∉ support (indicator s f) → Eq (α := α →₀ M) (single x ((indicator s f : (a : α) → M) x) : α →₀ M) (0 : α →₀ M)
⊢ Eq (α := α →₀ M) (indicator s f) (∑ x ∈ s.attach, single (↑x : α) (f (↑x : α) ⋯))

Tactic:
rw [← sum_single (indicator s f), sum, sum_subset (support_indicator_subset _ _), ← sum_attach]

Premises used: Finsupp.indicator, Finsupp.sum, Finset.sum_attach, Finset.sum_subset, Finsupp.support_indicator_subset, Finsupp.sum_single
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
⊢ Eq (α := α →₀ M) (∑ x ∈ s.attach, single (↑x : α) ((indicator s f : (a : α) → M) (↑x : α)))
    (∑ x ∈ s.attach, single (↑x : α) (f (↑x : α) ⋯))

Tactic:
Finset.sum_congr rfl (fun _ _ => ?_)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
refine :
  ∀ x ∈ s.attach,
    Eq (α := α →₀ M) (single (↑x : α) ((indicator s f : (a : α) → M) (↑x : α)) : α →₀ M)
      (single (↑x : α) (f (↑x : α) ⋯) : α →₀ M)
⊢ Eq (α := α →₀ M) (∑ x ∈ s.attach, single (↑x : α) ((indicator s f : (a : α) → M) (↑x : α)))
    (∑ x ∈ s.attach, single (↑x : α) (f (↑x : α) ⋯))

Tactic:
refine Finset.sum_congr rfl (fun _ _ => ?_)

Premises used: Finset.sum_congr, rfl