awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
a b : R
s : Finset ι
refine :
  ∀ (t : Finset ι) (ht : t ∈ s.powerset), a ^ #t * b ^ (#s - #t) = HMul.hMul (α := R) (∏ i ∈ t, a) (∏ i ∈ s \ t, b)
⊢ Eq.{u_4 + 1} (α := R) (∑ t ∈ s.powerset, a ^ #t * b ^ (#s - #t))
    (∑ t ∈ s.powerset, HMul.hMul (α := R) (∏ i ∈ t, a) (∏ i ∈ s \ t, b))

Tactic:
refine Finset.sum_congr rfl fun t ht => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
a b : R
s t : Finset ι
ht : t ∈ s.powerset
rw : a ^ #t * b ^ (#s - #t) = a ^ #t * ∏ i ∈ s \ t, b
rw₁ : a ^ #t * b ^ (#s - #t) = a ^ #t * b ^ #(s \ t)
rw₂ rw₃ : a ^ #t * b ^ #(s \ t) = a ^ #t * b ^ #(s \ t)
⊢ a ^ #t * b ^ (#s - #t) = HMul.hMul (α := R) (∏ i ∈ t, a) (∏ i ∈ s \ t, b)

Tactic:
rw [prod_const, prod_const, ← card_sdiff_of_subset (mem_powerset.1 ht)]

Premises used: Finset.card_sdiff_of_subset, Finset.prod_const, Finset.mem_powerset, Iff.mp
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
a b : R
s : Finset ι
rw : Eq.{u_4 + 1} (α := R) (∑ t ∈ s.powerset, a ^ #t * b ^ (#s - #t)) (∏ _x ∈ s, (a + b))
rw₁ rw₂ rw₃ :
  Eq.{u_4 + 1} (α := R) (∑ t ∈ s.powerset, a ^ #t * b ^ (#s - #t))
    (∑ t ∈ s.powerset, HMul.hMul (α := R) (∏ i ∈ t, a) (∏ i ∈ s \ t, b))
rw₄ : ∀ (t : Finset ι) (ht : t ∈ s.powerset), a ^ #t * b ^ (#s - #t) = HMul.hMul (α := R) (∏ i ∈ t, a) (∏ i ∈ s \ t, b)
⊢ ∑ t ∈ s.powerset, a ^ #t * b ^ (#s - #t) = (a + b) ^ #s

Tactic:
classical
  rw [← prod_const, prod_add]
  refine Finset.sum_congr rfl fun t ht => ?_
  rw [prod_const, prod_const, ← card_sdiff_of_subset (mem_powerset.1 ht)]

Premises used: Finset.prod_add, Finset.prod_const, Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
R : Type u_4
inst : CommSemiring R
ι : Type u_5
inst_1 : Fintype ι
a b : R
⊢ ∑ s : Finset ι, a ^ #s * b ^ (Fintype.card ι - #s) = (a + b) ^ Fintype.card ι

Tactic:
Finset.sum_pow_mul_eq_add_pow _ _ _

Premises used: Finset.univ, Fintype.card, Finset.sum_pow_mul_eq_add_pow, Finset.powerset
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : Finset ι
f : ι → ℕ
⊢ Eq.{u_4 + 1} (α := R) (↑(∏ i ∈ s, f i) : R) (∏ i ∈ s, (↑(f i) : R))

Tactic:
map_prod (Nat.castRingHom R) f s

Premises used: map_prod, Nat.castRingHom
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommRing R
inst_1 : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ Eq.{u_4 + 1} (α := R) (∏ i ∈ s, (f i - g i))
    (∑ t ∈ s.powerset, (HPow.hPow (α := R) (-1) #t * ∏ i ∈ s \ t, f i) * ∏ i ∈ t, g i)

Tactic:
simp [sub_eq_neg_add, prod_add, prod_neg, mul_right_comm]

Premises used: Finset.prod_add, sub_eq_neg_add, Finset.prod_neg, mul_right_comm
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommRing R
inst_1 : LinearOrder ι
s : Finset ι
f g : ι → R
simp :
  ∏ x ∈ s, (f x + -g x) =
    HAdd.hAdd (α := R) (∏ i ∈ s, f i) (-∑ x ∈ s, (g x * ∏ x ∈ s with x < x, (f x + -g x)) * ∏ i ∈ s with x < i, f i)
⊢ ∏ i ∈ s, (f i - g i) =
    HSub.hSub (α := R) (∏ i ∈ s, f i) (∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j - g j)) * ∏ j ∈ s with i < j, f j)

Tactic:
simp only [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommRing R
inst_1 : LinearOrder ι
s : Finset ι
f g : ι → R
⊢ ∏ i ∈ s, (f i + -g i) =
    HAdd.hAdd (α := R) (∏ i ∈ s, f i) (∑ i ∈ s, (-g i * ∏ j ∈ s with j < i, (f j + -g j)) * ∏ j ∈ s with i < j, f j)

Tactic:
prod_add_ordered s f fun i => -g i

Premises used: Finset.prod_add_ordered, Neg.neg
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommRing R
inst_1 : LinearOrder ι
s : Finset ι
f g : ι → R
h :
  Eq.{u_4 + 1} (α := R) (-∑ x ∈ s, (g x * ∏ x ∈ s with x < x, (f x + -g x)) * ∏ i ∈ s with x < i, f i)
    (∑ i ∈ s, (-g i * ∏ j ∈ s with j < i, (f j + -g j)) * ∏ j ∈ s with i < j, f j)
⊢ ∏ x ∈ s, (f x + -g x) =
    HAdd.hAdd (α := R) (∏ i ∈ s, f i) (-∑ x ∈ s, (g x * ∏ x ∈ s with x < x, (f x + -g x)) * ∏ i ∈ s with x < i, f i)

Tactic:
convert! prod_add_ordered s f fun i => -g i

Premises used: Finset.prod_add_ordered, Neg.neg
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommRing R
inst_1 : LinearOrder ι
s : Finset ι
f g : ι → R
⊢ Eq.{u_4 + 1} (α := R) (-∑ x ∈ s, (g x * ∏ x ∈ s with x < x, (f x + -g x)) * ∏ i ∈ s with x < i, f i)
    (∑ i ∈ s, (-g i * ∏ j ∈ s with j < i, (f j + -g j)) * ∏ j ∈ s with i < j, f j)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommRing R
inst_1 : LinearOrder ι
s : Finset ι
f : ι → R
rw :
  HSub.hSub (α := R) (∏ i ∈ s, 1) (∑ i ∈ s, (f i * ∏ j ∈ s with j < i, (1 - f j)) * ∏ j ∈ s with i < j, 1) =
    HSub.hSub (α := R) 1 (∑ i ∈ s, f i * ∏ j ∈ s with j < i, (1 - f j))
⊢ ∏ i ∈ s, (1 - f i) = HSub.hSub (α := R) 1 (∑ i ∈ s, f i * ∏ j ∈ s with j < i, (1 - f j))

Tactic:
rw [prod_sub_ordered]

Premises used: Finset.prod_sub_ordered
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommRing R
inst_1 : LinearOrder ι
s : Finset ι
f : ι → R
⊢ HSub.hSub (α := R) (∏ i ∈ s, 1) (∑ i ∈ s, (f i * ∏ j ∈ s with j < i, (1 - f j)) * ∏ j ∈ s with i < j, 1) =
    HSub.hSub (α := R) 1 (∑ i ∈ s, f i * ∏ j ∈ s with j < i, (1 - f j))

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
R : Type u_4
inst : CommRing R
n k : ℕ
rw : Eq.{u_4 + 1} (α := R) (∏ i ∈ range k, HSub.hSub (α := R) (↑n : R) (↑i : R)) (∏ i ∈ range k, (↑(n - i) : R))
⊢ Eq.{u_4 + 1} (α := R) (∏ i ∈ range k, HSub.hSub (α := R) (↑n : R) (↑i : R)) (↑(∏ i ∈ range k, (n - i)) : R)

Tactic:
rw [prod_natCast]

Premises used: Finset.prod_natCast
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
R : Type u_4
inst : CommRing R
n k : ℕ
inl :
  ∀ (hkn : k ≤ n),
    Eq.{u_4 + 1} (α := R) (∏ i ∈ range k, HSub.hSub (α := R) (↑n : R) (↑i : R)) (∏ i ∈ range k, (↑(n - i) : R))
inr :
  ∀ (hnk : n < k),
    Eq.{u_4 + 1} (α := R) (∏ i ∈ range k, HSub.hSub (α := R) (↑n : R) (↑i : R)) (∏ i ∈ range k, (↑(n - i) : R))
⊢ Eq.{u_4 + 1} (α := R) (∏ i ∈ range k, HSub.hSub (α := R) (↑n : R) (↑i : R)) (∏ i ∈ range k, (↑(n - i) : R))

Tactic:
rcases le_or_gt k n with hkn | hnk

Premises used: le_or_gt
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
R : Type u_4
inst : CommRing R
n k : ℕ
hkn : k ≤ n
⊢ Eq.{u_4 + 1} (α := R) (∏ i ∈ range k, HSub.hSub (α := R) (↑n : R) (↑i : R)) (∏ i ∈ range k, (↑(n - i) : R))

Tactic:
prod_congr rfl fun i hi => (Nat.cast_sub <| (mem_range.1 hi).le.trans hkn).symm

Premises used: Nat.cast_sub, LT.lt.le, Finset.prod_congr, Finset.mem_range, Iff.mp, LE.le.trans, Eq.symm, rfl
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
R : Type u_4
inst : CommRing R
n k : ℕ
hkn : k ≤ n
⊢ Eq.{u_4 + 1} (α := R) (∏ i ∈ range k, HSub.hSub (α := R) (↑n : R) (↑i : R)) (∏ i ∈ range k, (↑(n - i) : R))

Tactic:
exact prod_congr rfl fun i hi => (Nat.cast_sub <| (mem_range.1 hi).le.trans hkn).symm

Premises used: Nat.cast_sub, LT.lt.le, Finset.prod_congr, Finset.mem_range, Iff.mp, LE.le.trans, Eq.symm, rfl
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
R : Type u_4
inst : CommRing R
n k : ℕ
hnk : n < k
⊢ n ∈ range k

Tactic:
rw [← mem_range] at hnk

Premises used: Finset.mem_range
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
R : Type u_4
inst : CommRing R
n k : ℕ
hnk : n ∈ range k
inr : Eq.{u_4 + 1} (α := R) (↑(n - n) : R) 0
inr₁ : HSub.hSub (α := R) (↑n : R) (↑n : R) = 0
⊢ Eq.{u_4 + 1} (α := R) (∏ i ∈ range k, HSub.hSub (α := R) (↑n : R) (↑i : R)) (∏ i ∈ range k, (↑(n - i) : R))

Tactic:
rw [prod_eq_zero hnk, prod_eq_zero hnk]

Premises used: Finset.prod_eq_zero
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
R : Type u_4
inst : CommRing R
n k : ℕ
hnk : n ∈ range k
⊢ Eq.{u_4 + 1} (α := R) (↑(n - n) : R) 0

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
R : Type u_4
inst : CommRing R
n k : ℕ
hnk : n ∈ range k
⊢ HSub.hSub (α := R) (↑n : R) (↑n : R) = 0

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_5
R : Type u_7
inst : Fintype ι
inst_1 : CommSemiring R
f : ι → R
n : ℕ
⊢ HPow.hPow (α := R) (∑ a : ι, f a) n = ∑ p : Fin n → ι, ∏ i : Fin n, f (p i)

Tactic:
simp [sum_pow']

Premises used: Finset.sum_pow'
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_5
R : Type u_7
inst : Fintype ι
inst_1 : CommSemiring R
inst_2 : DecidableEq ι
κ : ι → Type u_8
inst_3 : (i : ι) → Fintype (κ i)
f : (i : ι) → κ i → R
⊢ Eq.{u_7 + 1} (α := R) (∏ i : ι, ∑ j : κ i, f i j) (∑ x : (i : ι) → κ i, ∏ i : ι, f i (x i))

Tactic:
Finset.prod_univ_sum _ _

Premises used: Finset.univ, Finset.map, Fintype.piFinset, Finset.prod_univ_sum
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_5
R : Type u_7
inst : Fintype ι
inst_1 : CommSemiring R
inst_2 : DecidableEq ι
f g : ι → R
⊢ Eq.{u_7 + 1} (α := R) (∏ a : ι, (f a + g a)) (∑ t : Finset ι, HMul.hMul (α := R) (∏ a ∈ t, f a) (∏ a ∈ tᶜ, g a))

Tactic:
simpa [compl_eq_univ_sdiff] using Finset.prod_add f g univ

Premises used: Finset.compl_eq_univ_sdiff, Finset.prod_add, Finset.univ
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_5
s : Finset ι
f : ι → ℕ
n : ℕ
hf : ∀ i ∈ s, n ∣ f i
inl : ∀ (hf : ∀ i ∈ s, 0 ∣ f i), HDiv.hDiv (α := ℕ) (∑ i ∈ s, f i) 0 = ∑ i ∈ s, f i / 0
inr : ∀ (hn : n > 0), (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n
⊢ (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n

Tactic:
obtain rfl | hn := n.eq_zero_or_pos

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_5
s : Finset ι
f : ι → ℕ
hf : ∀ i ∈ s, 0 ∣ f i
⊢ HDiv.hDiv (α := ℕ) (∑ i ∈ s, f i) 0 = ∑ i ∈ s, f i / 0

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_5
s : Finset ι
f : ι → ℕ
n : ℕ
hf : ∀ i ∈ s, n ∣ f i
hn : n > 0
inr : Eq (α := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i / n * n)
⊢ (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n

Tactic:
rw [Nat.div_eq_iff_eq_mul_left hn (dvd_sum hf), sum_mul]

Premises used: Finset.dvd_sum, Nat.div_eq_iff_eq_mul_left, Finset.sum_mul
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_5
s : Finset ι
f : ι → ℕ
n : ℕ
hf : ∀ i ∈ s, n ∣ f i
hn : n > 0
⊢ Eq (α := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i / n * n)

Tactic:
sum_congr rfl fun s hs ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_5
s : Finset ι
f : ι → ℕ
n : ℕ
hf : ∀ i ∈ s, n ∣ f i
hn : n > 0
inr : ∀ (s_1 : ι) (hs : s_1 ∈ s), f s_1 = f s_1 / n * n
⊢ Eq (α := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i / n * n)

Tactic:
refine sum_congr rfl fun s hs ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_5
s_1 : Finset ι
f : ι → ℕ
n : ℕ
hf : ∀ i ∈ s_1, n ∣ f i
hn : n > 0
s : ι
hs : s ∈ s_1
inr inr₁ : f s = f s
⊢ f s = f s / n * n

Tactic:
rw [Nat.div_mul_cancel (hf _ hs)]

Premises used: Nat.div_mul_cancel
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
R : Type u_4
inst : AddMonoidWithOne R
s : List ℕ
⊢ Eq.{u_4 + 1} (α := R) (↑s.sum : R) (List.sum (List.map Nat.cast s))

Tactic:
map_list_sum (castAddMonoidHom R) _

Premises used: Nat.castAddMonoidHom, map_list_sum
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
R : Type u_4
inst : Semiring R
s : List ℕ
⊢ Eq.{u_4 + 1} (α := R) (↑s.prod : R) (List.prod (List.map Nat.cast s))

Tactic:
map_list_prod (castRingHom R) _

Premises used: map_list_prod, Nat.castRingHom
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
R : Type u_4
inst : AddCommMonoidWithOne R
s : Multiset ℕ
⊢ Eq.{u_4 + 1} (α := R) (↑s.sum : R) (Multiset.sum (Multiset.map Nat.cast s))

Tactic:
map_multiset_sum (castAddMonoidHom R) _

Premises used: map_multiset_sum, Nat.castAddMonoidHom
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
R : Type u_4
inst : CommSemiring R
s : Multiset ℕ
⊢ Eq.{u_4 + 1} (α := R) (↑s.prod : R) (Multiset.prod (Multiset.map Nat.cast s))

Tactic:
map_multiset_prod (castRingHom R) _

Premises used: map_multiset_prod, Nat.castRingHom
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
R : Type u_4
ι : Type u_5
inst : AddCommMonoidWithOne R
s : Finset ι
f : ι → ℕ
⊢ Eq.{u_4 + 1} (α := R) (↑(∑ x ∈ s, f x) : R) (∑ x ∈ s, (↑(f x) : R))

Tactic:
map_sum (castAddMonoidHom R) _ _

Premises used: Nat.castAddMonoidHom, map_sum
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
R : Type u_4
ι : Type u_5
inst : CommSemiring R
f : ι → ℕ
s : Finset ι
⊢ Eq.{u_4 + 1} (α := R) (↑(∏ i ∈ s, f i) : R) (∏ i ∈ s, (↑(f i) : R))

Tactic:
map_prod (castRingHom R) _ _

Premises used: map_prod, Nat.castRingHom
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_5
s : Finset ι
f : ι → ℤ
n : ℤ
hf : ∀ i ∈ s, n ∣ f i
inl : ∀ (hf : ∀ i ∈ s, 0 ∣ f i), HDiv.hDiv (α := ℤ) (∑ i ∈ s, f i) 0 = ∑ i ∈ s, f i / 0
inr : ∀ (hn : n ≠ 0), (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n
⊢ (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n

Tactic:
obtain rfl | hn := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_5
s : Finset ι
f : ι → ℤ
hf : ∀ i ∈ s, 0 ∣ f i
⊢ HDiv.hDiv (α := ℤ) (∑ i ∈ s, f i) 0 = ∑ i ∈ s, f i / 0

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_5
s : Finset ι
f : ι → ℤ
n : ℤ
hf : ∀ i ∈ s, n ∣ f i
hn : n ≠ 0
inr : Eq (α := ℤ) (∑ i ∈ s, f i) (∑ i ∈ s, f i / n * n)
⊢ (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n

Tactic:
rw [Int.ediv_eq_iff_eq_mul_left hn (dvd_sum hf), sum_mul]

Premises used: Finset.dvd_sum, Int.ediv_eq_iff_eq_mul_left, Finset.sum_mul
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_5
s : Finset ι
f : ι → ℤ
n : ℤ
hf : ∀ i ∈ s, n ∣ f i
hn : n ≠ 0
⊢ Eq (α := ℤ) (∑ i ∈ s, f i) (∑ i ∈ s, f i / n * n)

Tactic:
sum_congr rfl fun s hs ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_5
s : Finset ι
f : ι → ℤ
n : ℤ
hf : ∀ i ∈ s, n ∣ f i
hn : n ≠ 0
inr : ∀ (s_1 : ι) (hs : s_1 ∈ s), f s_1 = f s_1 / n * n
⊢ Eq (α := ℤ) (∑ i ∈ s, f i) (∑ i ∈ s, f i / n * n)

Tactic:
refine sum_congr rfl fun s hs ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_5
s_1 : Finset ι
f : ι → ℤ
n : ℤ
hf : ∀ i ∈ s_1, n ∣ f i
hn : n ≠ 0
s : ι
hs : s ∈ s_1
inr inr₁ : f s = f s
⊢ f s = f s / n * n

Tactic:
rw [Int.ediv_mul_cancel (hf _ hs)]

Premises used: Int.ediv_mul_cancel
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
R : Type u_4
inst : AddGroupWithOne R
s : List ℤ
⊢ Eq.{u_4 + 1} (α := R) (↑s.sum : R) (List.sum (List.map Int.cast s))

Tactic:
map_list_sum (castAddHom R) _

Premises used: map_list_sum, Int.castAddHom
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
R : Type u_4
inst : Ring R
s : List ℤ
⊢ Eq.{u_4 + 1} (α := R) (↑s.prod : R) (List.prod (List.map Int.cast s))

Tactic:
map_list_prod (castRingHom R) _

Premises used: map_list_prod, Int.castRingHom
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
R : Type u_4
inst : AddCommGroupWithOne R
s : Multiset ℤ
⊢ Eq.{u_4 + 1} (α := R) (↑s.sum : R) (Multiset.sum (Multiset.map Int.cast s))

Tactic:
map_multiset_sum (castAddHom R) _

Premises used: map_multiset_sum, Int.castAddHom
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
R : Type u_6
inst : CommRing R
s : Multiset ℤ
⊢ Eq.{u_6 + 1} (α := R) (↑s.prod : R) (Multiset.prod (Multiset.map Int.cast s))

Tactic:
map_multiset_prod (castRingHom R) _

Premises used: map_multiset_prod, Int.castRingHom
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
R : Type u_4
ι : Type u_5
inst : AddCommGroupWithOne R
s : Finset ι
f : ι → ℤ
⊢ Eq.{u_4 + 1} (α := R) (↑(∑ x ∈ s, f x) : R) (∑ x ∈ s, (↑(f x) : R))

Tactic:
map_sum (castAddHom R) _ _

Premises used: map_sum, Int.castAddHom
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_5
R : Type u_6
inst : CommRing R
f : ι → ℤ
s : Finset ι
⊢ Eq.{u_6 + 1} (α := R) (↑(∏ i ∈ s, f i) : R) (∏ i ∈ s, (↑(f i) : R))

Tactic:
map_prod (Int.castRingHom R) _ _

Premises used: map_prod, Int.castRingHom
-- Module: Mathlib.Algebra.BigOperators.Ring.List
Goal:
R : Type u_5
inst : NonUnitalNonAssocSemiring R
a : R
h : ∀ (b : R), Membership.mem (γ := List R) [] b → Commute a b
⊢ Commute a (sum [])

Tactic:
Commute.zero_right _

Premises used: List.sum, Commute.zero_right, List.foldr
-- Module: Mathlib.Algebra.BigOperators.Ring.List
Goal:
R : Type u_5
inst : NonUnitalNonAssocSemiring R
a : R
h : ∀ (b : R), Membership.mem (γ := List R) [] b → Commute a b
⊢ Commute a (sum [])

Tactic:
exact Commute.zero_right _

Premises used: Commute.zero_right
-- Module: Mathlib.Algebra.BigOperators.Ring.List
Goal:
R : Type u_5
inst : NonUnitalNonAssocSemiring R
a x : R
xs : List R
ih : ∀ (h : ∀ (b : R), b ∈ xs → Commute a b), Commute a xs.sum
h : ∀ (b : R), b ∈ x :: xs → Commute a b
cons : Commute a (x + xs.sum)
⊢ Commute a (x :: xs).sum

Tactic:
rw [List.sum_cons]

Premises used: List.sum_cons
-- Module: Mathlib.Algebra.BigOperators.Ring.List
Goal:
R : Type u_5
inst : NonUnitalNonAssocSemiring R
a x : R
xs : List R
ih : ∀ (h : ∀ (b : R), b ∈ xs → Commute a b), Commute a xs.sum
h : ∀ (b : R), b ∈ x :: xs → Commute a b
⊢ Commute a (x + xs.sum)

Tactic:
(h _ mem_cons_self).add_right (ih fun j hj ↦ h _ <| mem_cons_of_mem _ hj)

Premises used: List.mem_cons_of_mem, Commute.add_right, List.mem_cons_self
-- Module: Mathlib.Algebra.BigOperators.Ring.List
Goal:
R : Type u_5
inst : NonUnitalNonAssocSemiring R
a x : R
xs : List R
ih : ∀ (h : ∀ (b : R), b ∈ xs → Commute a b), Commute a xs.sum
h : ∀ (b : R), b ∈ x :: xs → Commute a b
⊢ Commute a (x + xs.sum)

Tactic:
exact (h _ mem_cons_self).add_right (ih fun j hj ↦ h _ <| mem_cons_of_mem _ hj)

Premises used: List.mem_cons_of_mem, Commute.add_right, List.mem_cons_self
-- Module: Mathlib.Algebra.BigOperators.Ring.List
Goal:
R : Type u_5
inst : NonUnitalNonAssocSemiring R
a : R
l : List R
h : ∀ (b : R), b ∈ l → Commute a b
nil : ∀ (h : ∀ (b : R), Membership.mem (γ := List R) [] b → Commute a b), Commute a (sum [])
cons :
  ∀ (x : R) (xs : List R) (ih : ∀ (h : ∀ (b : R), b ∈ xs → Commute a b), Commute a xs.sum)
    (h : ∀ (b : R), b ∈ x :: xs → Commute a b), Commute a (x :: xs).sum
⊢ Commute a l.sum

Tactic:
induction l with
  | nil => exact Commute.zero_right _
  | cons x xs ih =>
    rw [List.sum_cons]
    exact (h _ mem_cons_self).add_right (ih fun j hj ↦ h _ <| mem_cons_of_mem _ hj)

Premises used: Commute.zero_right, List.cons, List.sum_cons, List.nil
-- Module: Mathlib.Algebra.BigOperators.Ring.List
Goal:
R : Type u_5
inst : NonUnitalNonAssocSemiring R
b : R
l : List R
h : ∀ (a : R), a ∈ l → Commute a b
⊢ Commute l.sum b

Tactic:
((Commute.list_sum_right _ _) fun _x hx ↦ (h _ hx).symm).symm

Premises used: Commute.symm, Commute.list_sum_right
-- Module: Mathlib.Algebra.BigOperators.Ring.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : HasDistribNeg M
l : List M
nil : prod (map Neg.neg []) = HPow.hPow (α := M) (-1) (length.{u_3} (α := M) []) * prod []
cons :
  ∀ (head : M) (tail : List M),
    (map Neg.neg tail).prod = HPow.hPow (α := M) (-1) tail.length * tail.prod →
      (map Neg.neg (head :: tail)).prod = HPow.hPow (α := M) (-1) (head :: tail).length * (head :: tail).prod
⊢ (map Neg.neg l).prod = HPow.hPow (α := M) (-1) l.length * l.prod

Tactic:
induction l
-- Module: Mathlib.Algebra.BigOperators.Ring.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : HasDistribNeg M
⊢ prod (map Neg.neg []) = HPow.hPow (α := M) (-1) (length.{u_3} (α := M) []) * prod []

Tactic:
simp [*, pow_succ, ((Commute.neg_one_left _).pow_left _).left_comm]

Premises used: Commute.left_comm, pow_succ, Commute.pow_left, Commute.neg_one_left
-- Module: Mathlib.Algebra.BigOperators.Ring.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : HasDistribNeg M
head : M
tail : List M
tail_ih : (map Neg.neg tail).prod = HPow.hPow (α := M) (-1) tail.length * tail.prod
⊢ (map Neg.neg (head :: tail)).prod = HPow.hPow (α := M) (-1) (head :: tail).length * (head :: tail).prod

Tactic:
simp [*, pow_succ, ((Commute.neg_one_left _).pow_left _).left_comm]

Premises used: Commute.left_comm, pow_succ, Commute.pow_left, Commute.neg_one_left
-- Module: Mathlib.Algebra.BigOperators.Ring.List
Goal:
M₀ : Type u_4
inst : MonoidWithZero M₀
a : M₀
l : List M₀
h : 0 ∈ a :: l
rw : a * l.prod = 0
⊢ (a :: l).prod = 0

Tactic:
rw [prod_cons]

Premises used: List.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Ring.List
Goal:
M₀ : Type u_4
inst : MonoidWithZero M₀
a : M₀
l : List M₀
h : 0 ∈ a :: l
inl : ∀ (ha : 0 = a), a * l.prod = 0
inr : ∀ (hl : 0 ∈ l), a * l.prod = 0
⊢ a * l.prod = 0

Tactic:
rcases mem_cons.1 h with ha | hl

Premises used: Iff.mp, List.mem_cons
-- Module: Mathlib.Algebra.BigOperators.Ring.List
Goal:
M₀ : Type u_4
inst : MonoidWithZero M₀
a : M₀
l : List M₀
h : 0 ∈ a :: l
ha : 0 = a
⊢ a * l.prod = 0

Tactic:
mul_eq_zero_of_left ha.symm _

Premises used: mul_eq_zero_of_left, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Ring.List
Goal:
M₀ : Type u_4
inst : MonoidWithZero M₀
a : M₀
l : List M₀
h : 0 ∈ a :: l
hl : 0 ∈ l
⊢ a * l.prod = 0

Tactic:
mul_eq_zero_of_right _ (prod_eq_zero hl)

Premises used: mul_eq_zero_of_right
-- Module: Mathlib.Algebra.BigOperators.Ring.List
Goal:
M₀ : Type u_4
inst : MonoidWithZero M₀
a : M₀
l : List M₀
h : 0 ∈ a :: l
ha : 0 = a
⊢ a * l.prod = 0

Tactic:
exacts [mul_eq_zero_of_left ha.symm _, mul_eq_zero_of_right _ (prod_eq_zero hl)]

Premises used: mul_eq_zero_of_left, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Ring.List
Goal:
M₀ : Type u_4
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
⊢ Eq.{u_4 + 1} (α := M₀) (prod []) 0 ↔ Membership.mem (γ := List M₀) [] 0

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Ring.List
Goal:
M₀ : Type u_4
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
a : M₀
l : List M₀
rw : a * l.prod = 0 ↔ 0 ∈ a :: l
rw₁ : a = 0 ∨ l.prod = 0 ↔ 0 ∈ a :: l
rw₂ : a = 0 ∨ 0 ∈ l ↔ 0 ∈ a :: l
rw₃ : a = 0 ∨ 0 ∈ l ↔ 0 = a ∨ 0 ∈ l
rw₄ rw₅ : 0 = a ∨ 0 ∈ l ↔ 0 = a ∨ 0 ∈ l
⊢ (a :: l).prod = 0 ↔ 0 ∈ a :: l

Tactic:
rw [prod_cons, mul_eq_zero, prod_eq_zero_iff, mem_cons, eq_comm]

Premises used: eq_comm, mul_eq_zero, List.mem_cons, List.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Ring.List
Goal:
M₀ : Type u_4
inst : MonoidWithZero M₀
l : List M₀
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
hL : ¬0 ∈ l
⊢ l.prod ≠ 0

Tactic:
mt prod_eq_zero_iff.1 hL

Premises used: mt, List.prod_eq_zero_iff, Iff.mp
-- Module: Mathlib.Algebra.BigOperators.Ring.List
Goal:
ι : Type u_1
R : Type u_5
inst : NonUnitalNonAssocSemiring R
l : List ι
f : ι → R
r : R
⊢ sum (map (fun (b : ι) ↦ r * f b) l) = r * (map f l).sum

Tactic:
sum_map_hom l f <| AddMonoidHom.mulLeft r

Premises used: List.sum_map_hom, AddMonoidHom.mulLeft
-- Module: Mathlib.Algebra.BigOperators.Ring.List
Goal:
ι : Type u_1
R : Type u_5
inst : NonUnitalNonAssocSemiring R
l : List ι
f : ι → R
r : R
⊢ sum (map (fun (b : ι) ↦ f b * r) l) = (map f l).sum * r

Tactic:
sum_map_hom l f <| AddMonoidHom.mulRight r

Premises used: List.sum_map_hom, AddMonoidHom.mulRight
-- Module: Mathlib.Algebra.BigOperators.Ring.List
Goal:
R : Type u_5
inst : NonUnitalSemiring R
a : R
h : ∀ (x : R), Membership.mem (γ := List R) [] x → a ∣ x
⊢ a ∣ sum []

Tactic:
dvd_zero _

Premises used: dvd_zero, List.sum, List.foldr
-- Module: Mathlib.Algebra.BigOperators.Ring.List
Goal:
R : Type u_5
inst : NonUnitalSemiring R
a : R
h : ∀ (x : R), Membership.mem (γ := List R) [] x → a ∣ x
⊢ a ∣ sum []

Tactic:
exact dvd_zero _

Premises used: dvd_zero
-- Module: Mathlib.Algebra.BigOperators.Ring.List
Goal:
R : Type u_5
inst : NonUnitalSemiring R
a x : R
l : List R
ih : ∀ (h : ∀ (x : R), x ∈ l → a ∣ x), a ∣ l.sum
h : ∀ (x_1 : R), x_1 ∈ x :: l → a ∣ x_1
cons : a ∣ x + l.sum
⊢ a ∣ (x :: l).sum

Tactic:
rw [List.sum_cons]

Premises used: List.sum_cons