awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
x : ↥s
h : x ∈ s.attach
rw : Eq (α := α →₀ M) (single (↑x : α) (f (↑x : α) ⋯)) (single (↑x : α) (f (↑x : α) ⋯))
hi : (↑x : α) ∈ s
rw₁ : Eq (α := α →₀ M) (single (↑x : α) (f (↑x : α) ⋯)) (single (↑x : α) (f (↑x : α) ⋯))
hi₁ : (↑x : α) ∈ s
⊢ Eq (α := α →₀ M) (single (↑x : α) ((indicator s f : (a : α) → M) (↑x : α)) : α →₀ M)
    (single (↑x : α) (f (↑x : α) ⋯) : α →₀ M)

Tactic:
rw [indicator_of_mem]

Premises used: Finsupp.indicator_of_mem
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
i : α
_ :
  i ∈ s →
    i ∉ support (indicator s f) → Eq (α := α →₀ M) (single i ((indicator s f : (a : α) → M) i) : α →₀ M) (0 : α →₀ M)
⊢ i ∈ s →
    i ∉ support (indicator s f) → Eq (α := α →₀ M) (single i ((indicator s f : (a : α) → M) i) : α →₀ M) (0 : α →₀ M)

Tactic:
_
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
i : α
h : i ∈ s
hi : i ∉ support (indicator s f)
rw : Eq (α := α →₀ M) (single i 0) 0
rw₁ rw₂ : Eq (α := α →₀ M) 0 0
⊢ Eq (α := α →₀ M) (single i ((indicator s f : (a : α) → M) i) : α →₀ M) (0 : α →₀ M)

Tactic:
rw [notMem_support_iff.mp hi, single_zero]

Premises used: Finsupp.notMem_support_iff, Iff.mp, Finsupp.single_zero
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
s : Finset α
f : α → M
⊢ Eq (α := α →₀ M) (indicator s fun (x : α) (x_1 : x ∈ s) ↦ f x) (∑ x ∈ s, single x (f x))

Tactic:
(indicator_eq_sum_attach_single _).trans <| sum_attach _ fun x ↦ single x (f x)

Premises used: Finset.sum_attach, Finsupp.indicator_eq_sum_attach_single, Eq.trans, Finsupp.single
-- 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
s : Finset α
f : (a : α) → a ∈ s → M
h : α → M → N
h_zero : ∀ a ∈ s, h a 0 = 1
rw :
  Eq.{u_10 + 1} (α := N) (∏ x ∈ s.attach, h (↑x : α) ((indicator s f : (a : α) → M) (↑x : α)))
    (∏ x ∈ s.attach, h (↑x : α) (f (↑x : α) ⋯))
⊢ prod (indicator s f) h = ∏ x ∈ s.attach, h (↑x : α) (f (↑x : α) ⋯)

Tactic:
rw [prod_of_support_subset _ (support_indicator_subset _ _) h h_zero, ← prod_attach]

Premises used: Finsupp.prod_of_support_subset, Finset.prod_attach, Finsupp.support_indicator_subset
-- 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
s : Finset α
f : (a : α) → a ∈ s → M
h : α → M → N
h_zero : ∀ a ∈ s, h a 0 = 1
⊢ Eq.{u_10 + 1} (α := N) (∏ x ∈ s.attach, h (↑x : α) ((indicator s f : (a : α) → M) (↑x : α)))
    (∏ x ∈ s.attach, h (↑x : α) (f (↑x : α) ⋯))

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

Premises used: Finset.prod_congr, rfl
-- 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
s : Finset α
f : (a : α) → a ∈ s → M
h : α → M → N
h_zero : ∀ a ∈ s, h a 0 = 1
refine : ∀ x ∈ s.attach, h (↑x : α) ((indicator s f : (a : α) → M) (↑x : α)) = h (↑x : α) (f (↑x : α) ⋯)
⊢ Eq.{u_10 + 1} (α := N) (∏ x ∈ s.attach, h (↑x : α) ((indicator s f : (a : α) → M) (↑x : α)))
    (∏ x ∈ s.attach, h (↑x : α) (f (↑x : α) ⋯))

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

Premises used: Finset.prod_congr, rfl
-- 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
s : Finset α
f : (a : α) → a ∈ s → M
h : α → M → N
h_zero : ∀ a ∈ s, h a 0 = 1
x : ↥s
h_1 : x ∈ s.attach
rw : h (↑x : α) (f (↑x : α) ⋯) = h (↑x : α) (f (↑x : α) ⋯)
hi : (↑x : α) ∈ s
rw₁ : h (↑x : α) (f (↑x : α) ⋯) = h (↑x : α) (f (↑x : α) ⋯)
hi₁ : (↑x : α) ∈ s
⊢ h (↑x : α) ((indicator s f : (a : α) → M) (↑x : α)) = h (↑x : α) (f (↑x : α) ⋯)

Tactic:
rw [indicator_of_mem]

Premises used: Finsupp.indicator_of_mem
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : CommMonoid N
s : Finset α
f : α → M
h : α → M → N
⊢ Eq.{u_10 + 1} (α := N) (∏ x ∈ s.attach, h (↑x : α) (f (↑x : α))) (∏ x ∈ s, h x (f x))

Tactic:
prod_attach _ fun x ↦ h x (f x)

Premises used: Finset.prod_attach
-- 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
s : Finset α
f : α → M
h : α → M → N
h_zero : ∀ a ∈ s, h a 0 = 1
⊢ prod (indicator s fun (x : α) (x_1 : x ∈ s) ↦ f x) h = ∏ x ∈ s, h x (f x)

Tactic:
simp +contextual [h_zero]
-- 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
f : α →₀ M
g : α → M → N
n₁ n₂ : N
a : α
ha : a ∈ f.support
h : g a ((f : (a : α) → M) a) * n₁ = g a ((f : (a : α) → M) a) * n₂
⊢ f.prod g * n₁ = f.prod g * n₂

Tactic:
Finset.prod_mul_eq_prod_mul_of_exists a ha h

Premises used: Finsupp.prod, Finset.prod_mul_eq_prod_mul_of_exists
-- 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
f : α →₀ M
g : α → M → N
n₁ n₂ : N
a : α
ha : a ∈ f.support
h : g a ((f : (a : α) → M) a) * n₁ = g a ((f : (a : α) → M) a) * n₂
⊢ f.prod g * n₁ = f.prod g * n₂

Tactic:
exact Finset.prod_mul_eq_prod_mul_of_exists a ha h

Premises used: Finset.prod_mul_eq_prod_mul_of_exists
-- 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
f : α →₀ M
g : α → M → N
n₁ n₂ : N
a : α
ha : a ∈ f.support
h : g a ((f : (a : α) → M) a) * n₁ = g a ((f : (a : α) → M) a) * n₂
⊢ f.prod g * n₁ = f.prod g * n₂

Tactic:
classical
  exact Finset.prod_mul_eq_prod_mul_of_exists a ha h

Premises used: Finset.prod_mul_eq_prod_mul_of_exists
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
ι : Type u_2
A : Type u_4
inst : AddCommMonoid A
s : Finset α
f : α → ι →₀ A
i : ι
⊢ Eq.{u_4 + 1} (α := A) ((∑ k ∈ s, f k : (a : ι) → A) i : A) (∑ k ∈ s, (f k : (a : ι) → A) i : A)

Tactic:
map_sum (Finsupp.applyAddHom i) f s

Premises used: Finsupp.applyAddHom, map_sum
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
inst : AddCommMonoid A
inst_1 : AddCommMonoid B
g : ι →₀ A
k : ι → A → γ → B
x : γ
⊢ g.sum k x = g.sum fun (i : ι) (b : A) ↦ k i b x

Tactic:
Finset.sum_apply _ _ _

Premises used: Finset.sum_apply, Finsupp.sum
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
ι : Type u_2
γ : Type u_3
B : Type u_5
inst : AddCommMonoid B
A : Type u_16
F : Type u_17
inst_1 : AddZeroClass A
inst_2 : AddCommMonoid F
inst_3 : FunLike F γ B
g : ι →₀ A
k : ι → A → F
x : γ
h0 : Eq.{u_5 + 1} (α := B) ((0 : (a : γ) → B) x : B) (0 : B)
hadd :
  ∀ (f g : F), (f + g : (a : γ) → B) x = HAdd.hAdd (α := B) (β := B) ((f : (a : γ) → B) x : B) ((g : (a : γ) → B) x : B)
unfold :
  Eq.{u_5 + 1} (α := B) ((∑ a ∈ g.support, k a ((g : (a : ι) → A) a) : (a : γ) → B) x : B)
    (∑ a ∈ g.support, (fun (i : ι) (a : A) ↦ ((k i a : (a : γ) → B) x : B)) a ((g : (a : ι) → A) a) : B)
⊢ Eq.{u_5 + 1} (α := B) ((g.sum k : (a : γ) → B) x : B) (g.sum fun (i : ι) (a : A) ↦ (k i a : (a : γ) → B) x : B)

Tactic:
unfold Finsupp.sum

Premises used: Finsupp.sum
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
ι : Type u_2
γ : Type u_3
B : Type u_5
inst : AddCommMonoid B
A : Type u_16
F : Type u_17
inst_1 : AddZeroClass A
inst_2 : AddCommMonoid F
inst_3 : FunLike F γ B
g : ι →₀ A
k : ι → A → F
x : γ
h0 : Eq.{u_5 + 1} (α := B) ((0 : (a : γ) → B) x : B) (0 : B)
hadd :
  ∀ (f g : F), (f + g : (a : γ) → B) x = HAdd.hAdd (α := B) (β := B) ((f : (a : γ) → B) x : B) ((g : (a : γ) → B) x : B)
⊢ Eq.{u_5 + 1} (α := B) ((∑ a ∈ ∅, k a ((g : (a : ι) → A) a) : (a : γ) → B) x : B)
    (∑ a ∈ ∅, (fun (i : ι) (a : A) ↦ ((k i a : (a : γ) → B) x : B)) a ((g : (a : ι) → A) a) : B)

Tactic:
simp [h0]
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
ι : Type u_2
γ : Type u_3
B : Type u_5
inst : AddCommMonoid B
A : Type u_16
F : Type u_17
inst_1 : AddZeroClass A
inst_2 : AddCommMonoid F
inst_3 : FunLike F γ B
g : ι →₀ A
k : ι → A → F
x : γ
h0 : Eq.{u_5 + 1} (α := B) ((0 : (a : γ) → B) x : B) (0 : B)
hadd :
  ∀ (f g : F), (f + g : (a : γ) → B) x = HAdd.hAdd (α := B) (β := B) ((f : (a : γ) → B) x : B) ((g : (a : γ) → B) x : B)
i : ι
s : Finset ι
hi : i ∉ s
ih :
  Eq.{u_5 + 1} (α := B) ((∑ a ∈ s, k a ((g : (a : ι) → A) a) : (a : γ) → B) x : B)
    (∑ a ∈ s, (fun (i : ι) (a : A) ↦ ((k i a : (a : γ) → B) x : B)) a ((g : (a : ι) → A) a) : B)
⊢ Eq.{u_5 + 1} (α := B) ((∑ a ∈ insert i s, k a ((g : (a : ι) → A) a) : (a : γ) → B) x : B)
    (∑ a ∈ insert i s, (fun (i : ι) (a : A) ↦ ((k i a : (a : γ) → B) x : B)) a ((g : (a : ι) → A) a) : B)

Tactic:
simp [sum_insert hi, hadd, ih]

Premises used: Finset.sum_insert
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
ι : Type u_2
γ : Type u_3
B : Type u_5
inst : AddCommMonoid B
A : Type u_16
F : Type u_17
inst_1 : AddZeroClass A
inst_2 : AddCommMonoid F
inst_3 : FunLike F γ B
g : ι →₀ A
k : ι → A → F
x : γ
h0 : Eq.{u_5 + 1} (α := B) ((0 : (a : γ) → B) x : B) (0 : B)
hadd :
  ∀ (f g : F), (f + g : (a : γ) → B) x = HAdd.hAdd (α := B) (β := B) ((f : (a : γ) → B) x : B) ((g : (a : γ) → B) x : B)
induction :
  ∀ (x_1 : Finset ι),
    Eq.{u_5 + 1} (α := B) ((∑ a ∈ x_1, k a ((g : (a : ι) → A) a) : (a : γ) → B) x : B)
      (∑ a ∈ x_1, (fun (i : ι) (a : A) ↦ ((k i a : (a : γ) → B) x : B)) a ((g : (a : ι) → A) a) : B)
⊢ Eq.{u_5 + 1} (α := B) ((∑ a ∈ g.support, k a ((g : (a : ι) → A) a) : (a : γ) → B) x : B)
    (∑ a ∈ g.support, (fun (i : ι) (a : A) ↦ ((k i a : (a : γ) → B) x : B)) a ((g : (a : ι) → A) a) : B)

Tactic:
induction g.support using Finset.induction with
  | empty => simp [h0]
  | insert i s hi ih => simp [sum_insert hi, hadd, ih]

Premises used: Finsupp.support, Insert.insert
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
ι : Type u_2
γ : Type u_3
B : Type u_5
inst : AddCommMonoid B
A : Type u_16
F : Type u_17
inst_1 : AddZeroClass A
inst_2 : AddCommMonoid F
inst_3 : FunLike F γ B
g : ι →₀ A
k : ι → A → F
x : γ
h0 : Eq.{u_5 + 1} (α := B) ((0 : (a : γ) → B) x : B) (0 : B)
hadd :
  ∀ (f g : F), (f + g : (a : γ) → B) x = HAdd.hAdd (α := B) (β := B) ((f : (a : γ) → B) x : B) ((g : (a : γ) → B) x : B)
unfold :
  Eq.{u_5 + 1} (α := B) ((∑ a ∈ g.support, k a ((g : (a : ι) → A) a) : (a : γ) → B) x : B)
    (∑ a ∈ g.support, (fun (i : ι) (a : A) ↦ ((k i a : (a : γ) → B) x : B)) a ((g : (a : ι) → A) a) : B)
⊢ Eq.{u_5 + 1} (α := B) ((g.sum k : (a : γ) → B) x : B) (g.sum fun (i : ι) (a : A) ↦ (k i a : (a : γ) → B) x : B)

Tactic:
classical
  unfold Finsupp.sum
  induction g.support using Finset.induction with
  | empty => simp [h0]
  | insert i s hi ih => simp [sum_insert hi, hadd, ih]

Premises used: Finsupp.sum, Finsupp.support, Insert.insert
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
R : Type u_14
S : Type u_15
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
b : S
s : α →₀ R
f : α → R → S
⊢ s.sum f * b = s.sum fun (a : α) (c : R) ↦ f a c * b

Tactic:
simp only [Finsupp.sum, Finset.sum_mul]

Premises used: Finsupp.sum, Finset.sum_mul
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
R : Type u_14
S : Type u_15
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
b : S
s : α →₀ R
f : α → R → S
⊢ b * s.sum f = s.sum fun (a : α) (c : R) ↦ b * f a c

Tactic:
simp only [Finsupp.sum, Finset.mul_sum]

Premises used: Finset.mul_sum, Finsupp.sum
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
ι : Type u_2
M : Type u_8
inst : Zero M
f : ι →₀ M
g : ι → M → Multiset α
⊢ (f.sum g).card = f.sum fun (i : ι) (m : M) ↦ (g i m).card

Tactic:
map_finsuppSum cardHom ..

Premises used: Multiset.cardHom, map_finsuppSum, Multiset.card
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
f : ℕ →₀ ℕ
nhf : 0 ∉ f.support
x : ℕ
hf : x ∈ f.support
H : x = 0
⊢ 0 ∈ f.support

Tactic:
subst H
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
f : ℕ →₀ ℕ
nhf : 0 ∉ f.support
hf : 0 ∈ f.support
⊢ False

Tactic:
nhf hf
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
f : ℕ →₀ ℕ
nhf : 0 ∉ f.support
hf : 0 ∈ f.support
⊢ False

Tactic:
exact nhf hf
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
ι : Type u_16
M : Type u_17
N : Type u_18
inst : AddCommMonoid M
inst_1 : Zero N
f : ι →₀ N
g : ι → N → M
⊢ op (f.sum g) = f.sum fun (i : ι) (n : N) ↦ op (g i n)

Tactic:
op_sum ..

Premises used: Finsupp.sum, Finset.op_sum
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
ι : Type u_16
M : Type u_17
N : Type u_18
inst : AddCommMonoid M
inst_1 : Zero N
f : ι →₀ N
g : ι → N → Mᵐᵒᵖ
⊢ unop (f.sum g) = f.sum fun (i : ι) (n : N) ↦ unop (g i n)

Tactic:
unop_sum ..

Premises used: Finsupp.sum, Finset.unop_sum
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
ι : Type u_16
M : Type u_17
N : Type u_18
inst : CommMonoid M
inst_1 : Zero N
f : ι →₀ N
g : ι → N → M
⊢ op (f.prod g) = f.prod fun (i : ι) (n : N) ↦ op (g i n)

Tactic:
op_prod ..

Premises used: Finset.op_prod, Finsupp.prod
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
ι : Type u_16
M : Type u_17
N : Type u_18
inst : CommMonoid M
inst_1 : Zero N
f : ι →₀ N
g : ι → N → Mᵐᵒᵖ
⊢ unop (f.prod g) = f.prod fun (i : ι) (n : N) ↦ unop (g i n)

Tactic:
unop_prod ..

Premises used: Finset.unop_prod, Finsupp.prod
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Fin
Goal:
M : Type u_1
inst : AddCommMonoid M
n : ℕ
σ : Fin n →₀ M
i : M
rw : ∑ i_1 : Fin (n + 1), (cons i σ : (a : Fin (n + 1)) → M) i_1 = i + ∑ i : Fin n, (σ : (a : Fin n) → M) i
⊢ ((cons i σ).sum fun (x : Fin (n + 1)) (e : M) ↦ e) = i + σ.sum fun (x : Fin n) (e : M) ↦ e

Tactic:
rw [sum_fintype _ _ (fun _ => rfl), sum_fintype _ _ (fun _ => rfl)]

Premises used: Finsupp.sum_fintype
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Fin
Goal:
M : Type u_1
inst : AddCommMonoid M
n : ℕ
σ : Fin n →₀ M
i : M
⊢ ∑ i_1 : Fin (n + 1), (cons i σ : (a : Fin (n + 1)) → M) i_1 = i + ∑ i : Fin n, (σ : (a : Fin n) → M) i

Tactic:
Fin.sum_cons i σ

Premises used: Fin.cons, Fin.sum_cons, Fin.induction, Fin.cases, DFunLike.coe
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Fin
Goal:
M : Type u_1
inst : AddCommMonoid M
n : ℕ
σ : Fin n →₀ M
i : M
⊢ ∑ i_1 : Fin (n + 1), (cons i σ : (a : Fin (n + 1)) → M) i_1 = i + ∑ i : Fin n, (σ : (a : Fin n) → M) i

Tactic:
exact Fin.sum_cons i σ

Premises used: Fin.sum_cons, DFunLike.coe
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Fin
Goal:
M : Type u_1
N : Type u_2
inst : Zero M
inst_1 : AddCommMonoid N
n : ℕ
σ : Fin n →₀ M
i : M
f : Fin (n + 1) → M → N
h : ∀ (x : Fin (n + 1)), f x 0 = 0
x : Fin (n + 1)
⊢ f x 0 = 0

Tactic:
apply h
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Fin
Goal:
M : Type u_1
N : Type u_2
inst : Zero M
inst_1 : AddCommMonoid N
n : ℕ
σ : Fin n →₀ M
i : M
f : Fin (n + 1) → M → N
h : ∀ (x : Fin (n + 1)), f x 0 = 0
x : Fin n
⊢ Fin.tail (α := fun (i : Fin (n + 1)) ↦ M → N) f x 0 = 0

Tactic:
apply h
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Fin
Goal:
M : Type u_1
N : Type u_2
inst : Zero M
inst_1 : AddCommMonoid N
n : ℕ
σ : Fin n →₀ M
i : M
f : Fin (n + 1) → M → N
h : ∀ (x : Fin (n + 1)), f x 0 = 0
rw :
  ∑ i_1 : Fin (n + 1), f i_1 ((cons i σ : (a : Fin (n + 1)) → M) i_1) =
    f 0 i + ∑ i : Fin n, Fin.tail (α := fun (i : Fin (n + 1)) ↦ M → N) f i ((σ : (a : Fin n) → M) i)
⊢ (cons i σ).sum f = f 0 i + σ.sum (Fin.tail (α := fun (i : Fin (n + 1)) ↦ M → N) f)

Tactic:
rw [sum_fintype _ _ (fun _ => by apply h), sum_fintype _ _ (fun _ => by apply h)]

Premises used: Finsupp.sum_fintype
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Fin
Goal:
M : Type u_1
N : Type u_2
inst : Zero M
inst_1 : AddCommMonoid N
n : ℕ
σ : Fin n →₀ M
i : M
f : Fin (n + 1) → M → N
h : ∀ (x : Fin (n + 1)), f x 0 = 0
simp_rw :
  f 0 i + ∑ x : Fin n, f x.succ ((σ : (a : Fin n) → M) x) =
    f 0 i + ∑ i : Fin n, Fin.tail (α := fun (i : Fin (n + 1)) ↦ M → N) f i ((σ : (a : Fin n) → M) i)
⊢ ∑ i_1 : Fin (n + 1), f i_1 ((cons i σ : (a : Fin (n + 1)) → M) i_1) =
    f 0 i + ∑ i : Fin n, Fin.tail (α := fun (i : Fin (n + 1)) ↦ M → N) f i ((σ : (a : Fin n) → M) i)

Tactic:
simp_rw [Fin.sum_univ_succ, cons_zero, cons_succ]

Premises used: Finsupp.cons_succ, Finsupp.cons_zero, Fin.sum_univ_succ
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Fin
Goal:
M : Type u_1
N : Type u_2
inst : Zero M
inst_1 : AddCommMonoid N
n : ℕ
σ : Fin n →₀ M
i : M
f : Fin (n + 1) → M → N
h : ∀ (x : Fin (n + 1)), f x 0 = 0
⊢ f 0 i + ∑ x : Fin n, f x.succ ((σ : (a : Fin n) → M) x) =
    f 0 i + ∑ i : Fin n, Fin.tail (α := fun (i : Fin (n + 1)) ↦ M → N) f i ((σ : (a : Fin n) → M) i)

Tactic:
congr
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Fin
Goal:
n : Fin 2 →₀ ℕ
rw :
  Eq (α := ℕ)
      (((ofSupportFinite ![(n : (a : Fin 2) → ℕ) 0, (n : (a : Fin 2) → ℕ) 1] ⋯ : Fin (Nat.succ 0).succ →₀ ℕ) :
            (a : Fin (Nat.succ 0).succ) → ℕ)
          0 :
        ℕ)
      ((n : (a : Fin (Nat.succ 0).succ) → ℕ) 0 : ℕ) ∧
    Eq (α := ℕ)
      (((ofSupportFinite ![(n : (a : Fin 2) → ℕ) 0, (n : (a : Fin 2) → ℕ) 1] ⋯ : Fin (Nat.succ 0).succ →₀ ℕ) :
            (a : Fin (Nat.succ 0).succ) → ℕ)
          1 :
        ℕ)
      ((n : (a : Fin (Nat.succ 0).succ) → ℕ) 1 : ℕ)
⊢ ofSupportFinite ![(n : (a : Fin 2) → ℕ) 0, (n : (a : Fin 2) → ℕ) 1] ⋯ = n

Tactic:
rw [Finsupp.ext_iff, Fin.forall_fin_two]

Premises used: Fin.forall_fin_two, Finsupp.ext_iff
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Fin
Goal:
n : Fin 2 →₀ ℕ
⊢ Eq (α := ℕ)
      (((ofSupportFinite ![(n : (a : Fin 2) → ℕ) 0, (n : (a : Fin 2) → ℕ) 1] ⋯ : Fin (Nat.succ 0).succ →₀ ℕ) :
            (a : Fin (Nat.succ 0).succ) → ℕ)
          0 :
        ℕ)
      ((n : (a : Fin (Nat.succ 0).succ) → ℕ) 0 : ℕ) ∧
    Eq (α := ℕ)
      (((ofSupportFinite ![(n : (a : Fin 2) → ℕ) 0, (n : (a : Fin 2) → ℕ) 1] ⋯ : Fin (Nat.succ 0).succ →₀ ℕ) :
            (a : Fin (Nat.succ 0).succ) → ℕ)
          1 :
        ℕ)
      ((n : (a : Fin (Nat.succ 0).succ) → ℕ) 1 : ℕ)

Tactic:
⟨rfl, rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Fin
Goal:
n : Fin 2 →₀ ℕ
⊢ Eq (α := ℕ)
      (((ofSupportFinite ![(n : (a : Fin 2) → ℕ) 0, (n : (a : Fin 2) → ℕ) 1] ⋯ : Fin (Nat.succ 0).succ →₀ ℕ) :
            (a : Fin (Nat.succ 0).succ) → ℕ)
          0 :
        ℕ)
      ((n : (a : Fin (Nat.succ 0).succ) → ℕ) 0 : ℕ) ∧
    Eq (α := ℕ)
      (((ofSupportFinite ![(n : (a : Fin 2) → ℕ) 0, (n : (a : Fin 2) → ℕ) 1] ⋯ : Fin (Nat.succ 0).succ →₀ ℕ) :
            (a : Fin (Nat.succ 0).succ) → ℕ)
          1 :
        ℕ)
      ((n : (a : Fin (Nat.succ 0).succ) → ℕ) 1 : ℕ)

Tactic:
exact ⟨rfl, rfl⟩
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Fin
Goal:
M : Type u_1
d : M × M
inst : AddCommMonoid M
apply : ∑ a : Fin 2, ((finTwoArrowEquiv M).symm : (a : M × M) → Fin 2 → M) d a = d.1 + d.2
⊢ (Finsupp.sum ((Equiv.symm (finTwoArrowEquiv' M) : (a : M × M) → Fin 2 →₀ M) d) fun (x : Fin 2) (n : M) ↦ n) =
    d.1 + d.2

Tactic:
apply (Finsupp.equivFunOnFinite_symm_sum _).trans

Premises used: Finsupp.equivFunOnFinite_symm_sum, Eq.trans
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Fin
Goal:
M : Type u_1
d : M × M
inst : AddCommMonoid M
⊢ ∑ a : Fin 2, ((finTwoArrowEquiv M).symm : (a : M × M) → Fin 2 → M) d a = d.1 + d.2

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
⊢ ∏ i ∈ s, f i = fold (fun (x1 x2 : M) ↦ x1 * x2) 1 f s

Tactic:
rfl

Premises used: Finset.fold, rfl, Multiset.fold
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst : CommMonoid M
f : ι → M
h : a ∉ s
⊢ ∏ x ∈ cons a s h, f x = f a * ∏ x ∈ s, f x

Tactic:
fold_cons h

Premises used: Multiset.prod, Finset.fold_cons, Finset.prod
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst : CommMonoid M
h : a ∉ s
h₁ : ∀ (f : ι → M), (cons a s h).prod f = f a * ∏ x ∈ s, f x
⊢ Eq (α := (f : ι → M) → M) (cons a s h).prod fun (f : ι → M) ↦ f a * ∏ x ∈ s, f x

Tactic:
funext f
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst : CommMonoid M
h : a ∉ s
f : ι → M
h₁ h₂ : f a * ∏ x ∈ s, f x = f a * ∏ x ∈ s, f x
⊢ (cons a s h).prod f = f a * ∏ x ∈ s, f x

Tactic:
rw [Finset.prod_cons h]

Premises used: Finset.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
⊢ a ∉ s → ∏ x ∈ insert a s, f x = f a * ∏ x ∈ s, f x

Tactic:
fold_insert

Premises used: Multiset.prod, Finset.prod, Finset.fold_insert
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst : CommMonoid M
inst_1 : DecidableEq ι
h : a ∉ s
h₁ : ∀ (f : ι → M), (insert a s).prod f = f a * ∏ x ∈ s, f x
⊢ Eq (α := (f : ι → M) → M) (insert a s).prod fun (f : ι → M) ↦ f a * ∏ x ∈ s, f x

Tactic:
funext f
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst : CommMonoid M
inst_1 : DecidableEq ι
h : a ∉ s
f : ι → M
h₁ h₂ : f a * ∏ x ∈ s, f x = f a * ∏ x ∈ s, f x
⊢ (insert a s).prod f = f a * ∏ x ∈ s, f x

Tactic:
rw [Finset.prod_insert h]

Premises used: Finset.prod_insert
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
h : a ∉ s → f a = 1
pos : a ∈ s → Eq.{u_4 + 1} (α := M) (∏ x ∈ insert a s, f x) (∏ x ∈ s, f x)
neg : a ∉ s → Eq.{u_4 + 1} (α := M) (∏ x ∈ insert a s, f x) (∏ x ∈ s, f x)
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ insert a s, f x) (∏ x ∈ s, f x)

Tactic:
by_cases a ∈ s
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
h : a ∉ s → f a = 1
h_1 : a ∈ s
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ insert a s, f x) (∏ x ∈ s, f x)

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
h : a ∉ s → f a = 1
h_1 : a ∉ s
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ insert a s, f x) (∏ x ∈ s, f x)

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
h : f a = 1
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ insert a s, f x) (∏ x ∈ s, f x)

Tactic:
simp [h]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
f : ι → M
a : ι
⊢ ∏ x ∈ {a}, f x = f a

Tactic:
Eq.trans fold_singleton <| mul_one _

Premises used: Finset.fold_singleton, mul_one, Eq.trans
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
a : ι
h : ∀ (f : ι → M), Finset.prod {a} f = f a
⊢ Eq (α := (f : ι → M) → M) (Finset.prod {a}) fun (f : ι → M) ↦ f a

Tactic:
funext f
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
a : ι
f : ι → M
⊢ Finset.prod {a} f = f a

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
a b : ι
h : a ≠ b
rw : f a * ∏ x ∈ {b}, f x = f a * f b
rw₁ rw₂ : f a * f b = f a * f b
⊢ ∏ x ∈ {a, b}, f x = f a * f b

Tactic:
rw [prod_insert (notMem_singleton.2 h), prod_singleton]

Premises used: Finset.notMem_singleton, Iff.mpr, Finset.prod_insert, Finset.prod_singleton
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
s : Finset κ
g : κ → ι
⊢ Set.InjOn g (↑s : Set κ) → Eq.{u_4 + 1} (α := M) (∏ x ∈ image g s, f x) (∏ x ∈ s, f (g x))

Tactic:
fold_image

Premises used: Multiset.prod, Finset.prod, Finset.fold_image