awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Module
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
⊢ ∑ i ∈ Ioc m n, f i • g i =
    HSMul.hSMul (β := M) (f n) (∑ i ∈ range (n + 1), g i) -
        HSMul.hSMul (β := M) (f (m + 1)) (∑ i ∈ range (m + 1), g i) -
      ∑ i ∈ Ioc m (n - 1), HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i)

Tactic:
simpa only [← Ico_add_one_add_one_eq_Ioc, Nat.sub_add_cancel (Nat.one_le_of_lt hmn),
    add_tsub_cancel_right] using sum_Ico_by_parts f g (Nat.succ_lt_succ hmn)

Premises used: Nat.succ_lt_succ, Nat.one_le_of_lt, Finset.sum_Ico_by_parts, Nat.sub_add_cancel, add_tsub_cancel_right, Finset.Ico_add_one_add_one_eq_Ioc
-- Module: Mathlib.Algebra.BigOperators.Module
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ℕ → R
g : ℕ → M
n : ℕ
pos :
  ∀ (hn : n = 0),
    ∑ i ∈ range n, f i • g i =
      HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
        ∑ i ∈ range (n - 1), HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i)
neg :
  ∀ (hn : ¬n = 0),
    ∑ i ∈ range n, f i • g i =
      HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
        ∑ i ∈ range (n - 1), HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i)
⊢ ∑ i ∈ range n, f i • g i =
    HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      ∑ i ∈ range (n - 1), HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i)

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.Algebra.BigOperators.Module
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ℕ → R
g : ℕ → M
n : ℕ
hn : n = 0
⊢ ∑ i ∈ range n, f i • g i =
    HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      ∑ i ∈ range (n - 1), HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i)

Tactic:
simp [hn]
-- Module: Mathlib.Algebra.BigOperators.Module
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ℕ → R
g : ℕ → M
n : ℕ
hn : ¬n = 0
neg :
  ∑ x ∈ Ico 0 n, f x • g x =
    HSMul.hSMul (β := M) (f (n - 1)) (∑ x ∈ Ico 0 n, g x) -
      ∑ x ∈ Ico 0 (n - 1), HSMul.hSMul (β := M) (f (x + 1) - f x) (∑ x ∈ Ico 0 (x + 1), g x)
⊢ ∑ i ∈ range n, f i • g i =
    HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      ∑ i ∈ range (n - 1), HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i)

Tactic:
simp only [range_eq_Ico]

Premises used: Finset.range_eq_Ico
-- Module: Mathlib.Algebra.BigOperators.Module
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ℕ → R
g : ℕ → M
n : ℕ
hn : ¬n = 0
neg :
  HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      ∑ i ∈ Ico 0 (n - 1), HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i) =
    HSMul.hSMul (β := M) (f (n - 1)) (∑ x ∈ Ico 0 n, g x) -
      ∑ x ∈ Ico 0 (n - 1), HSMul.hSMul (β := M) (f (x + 1) - f x) (∑ x ∈ Ico 0 (x + 1), g x)
⊢ ∑ x ∈ Ico 0 n, f x • g x =
    HSMul.hSMul (β := M) (f (n - 1)) (∑ x ∈ Ico 0 n, g x) -
      ∑ x ∈ Ico 0 (n - 1), HSMul.hSMul (β := M) (f (x + 1) - f x) (∑ x ∈ Ico 0 (x + 1), g x)

Tactic:
rw [sum_Ico_by_parts f g (Nat.pos_of_ne_zero hn), sum_range_zero, smul_zero, sub_zero]

Premises used: sub_zero, smul_zero, Finset.sum_range_zero, Finset.sum_Ico_by_parts, Nat.pos_of_ne_zero
-- Module: Mathlib.Algebra.BigOperators.Module
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ℕ → R
g : ℕ → M
n : ℕ
hn : ¬n = 0
⊢ HSMul.hSMul (β := M) (f (n - 1)) (∑ i ∈ range n, g i) -
      ∑ i ∈ Ico 0 (n - 1), HSMul.hSMul (β := M) (f (i + 1) - f i) (∑ i ∈ range (i + 1), g i) =
    HSMul.hSMul (β := M) (f (n - 1)) (∑ x ∈ Ico 0 n, g x) -
      ∑ x ∈ Ico 0 (n - 1), HSMul.hSMul (β := M) (f (x + 1) - f x) (∑ x ∈ Ico 0 (x + 1), g x)

Tactic:
simp only [← range_eq_Ico]

Premises used: Finset.range_eq_Ico
-- Module: Mathlib.Algebra.BigOperators.NatAntidiagonal
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
rw :
  f (0, n + 1) *
      ∏ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        f
          (({ toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }.prodMap (Function.Embedding.refl ℕ) :
              (a : ℕ × ℕ) → ℕ × ℕ)
            x) =
    f (0, n + 1) * ∏ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, f (p.1 + 1, p.2)
⊢ ∏ p ∈ @antidiagonal _ Nat.instAddMonoid _ (n + 1), f p =
    f (0, n + 1) * ∏ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, f (p.1 + 1, p.2)

Tactic:
rw [antidiagonal_succ, prod_cons, prod_map]

Premises used: Finset.Nat.antidiagonal_succ, Finset.prod_cons, Finset.prod_map
-- Module: Mathlib.Algebra.BigOperators.NatAntidiagonal
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ f (0, n + 1) *
      ∏ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        f
          (({ toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }.prodMap (Function.Embedding.refl ℕ) :
              (a : ℕ × ℕ) → ℕ × ℕ)
            x) =
    f (0, n + 1) * ∏ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, f (p.1 + 1, p.2)

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.NatAntidiagonal
Goal:
N : Type u_2
inst : AddCommMonoid N
n : ℕ
f : ℕ × ℕ → N
⊢ ∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ (n + 1), f p =
    f (0, n + 1) + ∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, f (p.1 + 1, p.2)

Tactic:
@prod_antidiagonal_succ (Multiplicative N) _ _ _

Premises used: Multiset.sum, Finset.Nat.prod_antidiagonal_succ, Multiset.foldr, Multiset.prod, Finset.prod, Multiplicative, Finset.sum
-- Module: Mathlib.Algebra.BigOperators.NatAntidiagonal
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
rw :
  ∏ x ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
    f (Prod.swap (({ toFun := Prod.swap, inj' := ⋯ } : (a : ℕ × ℕ) → ℕ × ℕ) x))
| ∏ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, f p.swap

Tactic:
rw [← map_swap_antidiagonal, Finset.prod_map]

Premises used: Finset.map_swap_antidiagonal, Finset.prod_map
-- Module: Mathlib.Algebra.BigOperators.NatAntidiagonal
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
conv_lhs :
  Eq.{u_1 + 1} (α := M)
    (∏ x ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      f (Prod.swap (({ toFun := Prod.swap, inj' := ⋯ } : (a : ℕ × ℕ) → ℕ × ℕ) x)))
    (∏ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, f p)
⊢ Eq.{u_1 + 1} (α := M) (∏ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, f p.swap)
    (∏ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, f p)

Tactic:
conv_lhs => rw [← map_swap_antidiagonal, Finset.prod_map]

Premises used: Finset.map_swap_antidiagonal, Finset.prod_map
-- Module: Mathlib.Algebra.BigOperators.NatAntidiagonal
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ Eq.{u_1 + 1} (α := M)
    (∏ x ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      f (Prod.swap (({ toFun := Prod.swap, inj' := ⋯ } : (a : ℕ × ℕ) → ℕ × ℕ) x)))
    (∏ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, f p)

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.NatAntidiagonal
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
rw :
  f (Prod.swap (0, n + 1)) * ∏ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, f (p.swap.1 + 1, p.swap.2).swap =
    f (n + 1, 0) * ∏ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, f (p.1, p.2 + 1)
⊢ ∏ p ∈ @antidiagonal _ Nat.instAddMonoid _ (n + 1), f p =
    f (n + 1, 0) * ∏ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, f (p.1, p.2 + 1)

Tactic:
rw [← prod_antidiagonal_swap, prod_antidiagonal_succ, ← prod_antidiagonal_swap]

Premises used: Finset.Nat.prod_antidiagonal_succ, Finset.Nat.prod_antidiagonal_swap
-- Module: Mathlib.Algebra.BigOperators.NatAntidiagonal
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ f (Prod.swap (0, n + 1)) * ∏ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, f (p.swap.1 + 1, p.swap.2).swap =
    f (n + 1, 0) * ∏ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, f (p.1, p.2 + 1)

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.NatAntidiagonal
Goal:
N : Type u_2
inst : AddCommMonoid N
n : ℕ
f : ℕ × ℕ → N
⊢ ∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ (n + 1), f p =
    f (n + 1, 0) + ∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, f (p.1, p.2 + 1)

Tactic:
@prod_antidiagonal_succ' (Multiplicative N) _ _ _

Premises used: Multiset.sum, Multiset.foldr, Multiset.prod, Finset.Nat.prod_antidiagonal_succ', Finset.prod, Multiplicative, Finset.sum
-- Module: Mathlib.Algebra.BigOperators.NatAntidiagonal
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
f : ℕ × ℕ → ℕ → M
p : ℕ × ℕ
hp : p ∈ @antidiagonal _ Nat.instAddMonoid _ n
rw rw₁ : f p n = f p n
⊢ f p n = f p (p.1 + p.2)

Tactic:
rw [mem_antidiagonal.mp hp]

Premises used: Finset.HasAntidiagonal.mem_antidiagonal, Iff.mp
-- Module: Mathlib.Algebra.BigOperators.NatAntidiagonal
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ × ℕ → M
n : ℕ
⊢ Eq.{u_3 + 1} (α := M) (∏ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, f ij) (∏ k ∈ range n.succ, f (k, n - k))

Tactic:
Finset.prod_map (range n.succ) ⟨fun i ↦ (i, n - i), fun _ _ h ↦ (Prod.mk.inj h).1⟩ f

Premises used: Prod.mk.inj, Multiset.map, HSub.hSub, Finset.map, Function.Embedding.mk, Multiset.Nat.antidiagonal, Prod.mk, Finset.range, And.left, Finset.prod_map, Nat.succ, List.Nat.antidiagonal
-- Module: Mathlib.Algebra.BigOperators.NatAntidiagonal
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ Eq.{u_3 + 1} (α := M) (∏ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, f ij.1 ij.2) (∏ k ∈ range n.succ, f k (n - k))

Tactic:
prod_antidiagonal_eq_prod_range_succ_mk _ _

Premises used: Finset.Nat.prod_antidiagonal_eq_prod_range_succ_mk
-- Module: Mathlib.Algebra.BigOperators.Option
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : Option α → M
s : Finset α
⊢ ∏ x ∈ (insertNone : (a : Finset α) → Finset (Option α)) s, f x = f none * ∏ x ∈ s, f (some x)

Tactic:
simp [insertNone]

Premises used: Finset.insertNone
-- Module: Mathlib.Algebra.BigOperators.Option
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
x : M
s : Finset α
⊢ x * ∏ i ∈ s, f i = ∏ i ∈ (insertNone : (a : Finset α) → Finset (Option α)) s, i.elim x f

Tactic:
(prod_insertNone (fun i => i.elim x f) _).symm

Premises used: Finset.prod_insertNone, Eq.symm, Option.elim
-- Module: Mathlib.Algebra.BigOperators.Option
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
s : Finset (Option α)
⊢ Eq.{u_2 + 1} (α := M) (∏ x ∈ (eraseNone : (a : Finset (Option α)) → Finset α) s, f x)
    (∏ x ∈ map Embedding.some ((eraseNone : (a : Finset (Option α)) → Finset α) s), Option.elim' 1 f x)

Tactic:
(prod_map (eraseNone s) Embedding.some <| Option.elim' 1 f).symm

Premises used: Function.Embedding.some, Option.elim', Finset.eraseNone, Finset.prod_map, OfNat.ofNat, Eq.symm, DFunLike.coe
-- Module: Mathlib.Algebra.BigOperators.Option
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
s : Finset (Option α)
rw rw₁ : Eq.{u_2 + 1} (α := M) (∏ x ∈ s.erase none, Option.elim' 1 f x) (∏ x ∈ s.erase none, Option.elim' 1 f x)
⊢ Eq.{u_2 + 1} (α := M)
    (∏ x ∈ map Embedding.some ((eraseNone : (a : Finset (Option α)) → Finset α) s), Option.elim' 1 f x)
    (∏ x ∈ s.erase none, Option.elim' 1 f x)

Tactic:
rw [map_some_eraseNone]

Premises used: Finset.map_some_eraseNone
-- Module: Mathlib.Algebra.BigOperators.Option
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
s : Finset (Option α)
⊢ Eq.{u_2 + 1} (α := M) (∏ x ∈ s.erase none, Option.elim' 1 f x) (∏ x ∈ s, Option.elim' 1 f x)

Tactic:
prod_erase _ rfl

Premises used: Finset.prod_erase, rfl
-- Module: Mathlib.Algebra.BigOperators.Option
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
s : Finset (Option α)
x :
  Eq.{u_2 + 1} (α := M)
    (∏ x ∈ map Embedding.some ((eraseNone : (a : Finset (Option α)) → Finset α) s), Option.elim' 1 f x)
    (∏ x ∈ s.erase none, Option.elim' 1 f x)
⊢ Eq.{u_2 + 1} (α := M) (∏ x ∈ (eraseNone : (a : Finset (Option α)) → Finset α) s, f x) (∏ x ∈ s, Option.elim' 1 f x)

Tactic:
calc
      ∏ x ∈ eraseNone s, f x = ∏ x ∈ (eraseNone s).map Embedding.some, Option.elim' 1 f x :=
        (prod_map (eraseNone s) Embedding.some <| Option.elim' 1 f).symm
      _ = ∏ x ∈ s.erase none, Option.elim' 1 f x := by rw [map_some_eraseNone]
      _ = ∏ x ∈ s, Option.elim' 1 f x := prod_erase _ rfl

Premises used: Finset.prod_erase, Function.Embedding.some, Option.elim', Finset.eraseNone, Finset.map, Option.none, Finset.prod_map, OfNat.ofNat, Eq.symm, Finset.erase, DFunLike.coe, rfl
-- Module: Mathlib.Algebra.BigOperators.Option
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
s : Finset (Option α)
classical :
  Eq.{u_2 + 1} (α := M)
    (∏ x ∈ map Embedding.some ((eraseNone : (a : Finset (Option α)) → Finset α) s), Option.elim' 1 f x)
    (∏ x ∈ s.erase none, Option.elim' 1 f x)
⊢ Eq.{u_2 + 1} (α := M) (∏ x ∈ (eraseNone : (a : Finset (Option α)) → Finset α) s, f x) (∏ x ∈ s, Option.elim' 1 f x)

Tactic:
classical calc
      ∏ x ∈ eraseNone s, f x = ∏ x ∈ (eraseNone s).map Embedding.some, Option.elim' 1 f x :=
        (prod_map (eraseNone s) Embedding.some <| Option.elim' 1 f).symm
      _ = ∏ x ∈ s.erase none, Option.elim' 1 f x := by rw [map_some_eraseNone]
      _ = ∏ x ∈ s, Option.elim' 1 f x := prod_erase _ rfl

Premises used: Function.Embedding.some, Option.elim', Finset.eraseNone, Finset.map, Finset.prod_map, OfNat.ofNat, Eq.symm, DFunLike.coe
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
α : Type u_7
M : α → Type u_8
inst : (a : α) → Monoid (M a)
a : α
l : List ((a : α) → M a)
⊢ l.prod a = List.prod (List.map (fun (f : (a : α) → M a) ↦ f a) l)

Tactic:
map_list_prod (evalMonoidHom M a) _

Premises used: map_list_prod, Pi.evalMonoidHom, List.prod
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
α : Type u_7
M : α → Type u_8
inst : (a : α) → CommMonoid (M a)
a : α
s : Multiset ((a : α) → M a)
⊢ s.prod a = Multiset.prod (Multiset.map (fun (f : (a : α) → M a) ↦ f a) s)

Tactic:
(evalMonoidHom M a).map_multiset_prod _

Premises used: Multiset.foldr, Multiset.prod, Pi.evalMonoidHom, MonoidHom.map_multiset_prod
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_1
α : Type u_7
M : α → Type u_8
inst : (a : α) → CommMonoid (M a)
a : α
s : Finset ι
g : ι → (a : α) → M a
⊢ Eq.{u_8 + 1} (α := M a) ((∏ c ∈ s, g c) a) (∏ c ∈ s, g c a)

Tactic:
map_prod (Pi.evalMonoidHom M a) _ _

Premises used: Multiset.foldr, Multiset.prod, map_prod, Finset.prod, Pi.evalMonoidHom
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
α : Type u_7
M : α → Type u_8
ι : Type u_9
inst : (a : α) → CommMonoid (M a)
s : Finset ι
g : ι → (a : α) → M a
⊢ Eq (α := (a : α) → M a) (∏ c ∈ s, g c) fun (a : α) ↦ ∏ c ∈ s, g c a

Tactic:
funext fun _ ↦ Finset.prod_apply _ _ _

Premises used: Finset.prod_apply, funext
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_1
α : Type u_7
M : α → Type u_8
inst : Fintype ι
inst_1 : (a : α) → CommMonoid (M a)
a : α
g : ι → (a : α) → M a
⊢ Eq.{u_8 + 1} (α := M a) ((∏ c : ι, g c) a) (∏ c : ι, g c a)

Tactic:
Finset.prod_apply a Finset.univ g

Premises used: Finset.univ, Finset.prod_apply
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : CommMonoid M
inst_1 : CommMonoid N
s : Finset ι
f : ι → M
g : ι → N
this : DecidableEq ι
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      Eq (α := M × N) (∏ x ∈ s, f x, ∏ x ∈ s, g x) (∏ x ∈ s, (f x, g x)) →
        Eq (α := M × N) (∏ x ∈ insert a s, f x, ∏ x ∈ insert a s, g x) (∏ x ∈ insert a s, (f x, g x))

Tactic:
simp +contextual [Prod.ext_iff]

Premises used: Prod.ext_iff
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
R : Type u_8
inst_2 : NonAssocSemiring R
x : ι → R
h : ∀ (x_1 : ι), x x_1 = (∑ i : ι, HSMul.hSMul (β := (j : ι) → R) (x i) fun (j : ι) ↦ if i = j then 1 else 0) x_1
⊢ x = ∑ i : ι, HSMul.hSMul (β := (j : ι) → R) (x i) fun (j : ι) ↦ if i = j then 1 else 0

Tactic:
ext
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
R : Type u_8
inst_2 : NonAssocSemiring R
x : ι → R
x_1 : ι
⊢ x x_1 = (∑ i : ι, HSMul.hSMul (β := (j : ι) → R) (x i) fun (j : ι) ↦ if i = j then 1 else 0) x_1

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
R : Type u_8
inst_2 : NonAssocSemiring R
x : ι → R
⊢ x = ∑ i : ι, HSMul.hSMul (β := (j : ι) → R) (x i) fun (j : ι) ↦ if i = j then 1 else 0

Tactic:
pi_eq_sum_univ x

Premises used: pi_eq_sum_univ
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
R : Type u_8
inst_2 : NonAssocSemiring R
x : ι → R
h :
  ∀ (x : ι),
    Membership.mem (γ := Finset ι) Finset.univ x →
      ∀ (x_1 : ι), Eq.{u_8 + 1} (α := R) (Pi.single (M := fun (x : ι) ↦ R) x 1 x_1 : R) (if x = x_1 then 1 else 0 : R)
⊢ x = ∑ i : ι, HSMul.hSMul (β := (j : ι) → R) (x i) (Pi.single (M := fun (x : ι) ↦ R) i 1)

Tactic:
convert! pi_eq_sum_univ x

Premises used: pi_eq_sum_univ
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
R : Type u_8
inst_2 : NonAssocSemiring R
x : ι → R
x_1 : ι
h : Membership.mem (γ := Finset ι) Finset.univ x_1
x_2 : ι
⊢ Eq.{u_8 + 1} (α := R) (Pi.single (M := fun (x : ι) ↦ R) x_1 1 x_2 : R) (if x_1 = x_2 then 1 else 0 : R)

Tactic:
aesop
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
pos :
  ∀ (hj : Membership.mem (γ := Set κ) (⋂ x ∈ s, f x) j),
    Eq.{u_5 + 1} (α := R) (∏ i ∈ s, (f i).indicator (g i) j) ((∏ i ∈ s, g i) j)
neg : ∀ (hj : j ∉ ⋂ x ∈ s, f x), Eq.{u_5 + 1} (α := R) (∏ i ∈ s, (f i).indicator (g i) j) 0
⊢ Eq.{u_5 + 1} (α := R) (∏ i ∈ s, (f i).indicator (g i) j)
    (if Membership.mem (γ := Set κ) (⋂ x ∈ s, f x) j then (∏ i ∈ s, g i) j else 0)

Tactic:
split_ifs with hj
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
hj : Membership.mem (γ := Set κ) (⋂ x ∈ s, f x) j
pos : Eq.{u_5 + 1} (α := R) (∏ i ∈ s, (f i).indicator (g i) j) (∏ c ∈ s, g c j)
⊢ Eq.{u_5 + 1} (α := R) (∏ i ∈ s, (f i).indicator (g i) j) ((∏ i ∈ s, g i) j)

Tactic:
rw [Finset.prod_apply]

Premises used: Finset.prod_apply
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
hj : Membership.mem (γ := Set κ) (⋂ x ∈ s, f x) j
pos : ∀ (i : ι) (hi : i ∈ s), (f i).indicator (g i) j = g i j
⊢ Eq.{u_5 + 1} (α := R) (∏ i ∈ s, (f i).indicator (g i) j) (∏ c ∈ s, g c j)

Tactic:
congr! 1 with i hi
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
hj : Membership.mem (γ := Set κ) (⋂ x ∈ s, f x) j
i : ι
hi : i ∈ s
⊢ ∀ (i : ι) (i_1 : i ∈ s), j ∈ f i

Tactic:
simp only [Set.mem_iInter] at hj

Premises used: Set.mem_iInter
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
i : ι
hi : i ∈ s
hj : ∀ (i : ι) (i_1 : i ∈ s), j ∈ f i
⊢ (f i).indicator (g i) j = g i j

Tactic:
Set.indicator_of_mem (hj _ hi) _

Premises used: Set.indicator_of_mem
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
i : ι
hi : i ∈ s
hj : ∀ (i : ι) (i_1 : i ∈ s), j ∈ f i
⊢ (f i).indicator (g i) j = g i j

Tactic:
exact Set.indicator_of_mem (hj _ hi) _

Premises used: Set.indicator_of_mem
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
hj : j ∉ ⋂ x ∈ s, f x
⊢ ∃ x ∈ s, j ∉ f x

Tactic:
simpa using hj
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
hj : j ∉ ⋂ x ∈ s, f x
neg : ∀ (i : ι) (hi : i ∈ s) (hj : j ∉ f i), Eq.{u_5 + 1} (α := R) (∏ i ∈ s, (f i).indicator (g i) j) 0
⊢ Eq.{u_5 + 1} (α := R) (∏ i ∈ s, (f i).indicator (g i) j) 0

Tactic:
obtain ⟨i, hi, hj⟩ := by simpa using hj
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
hj_1 : j ∉ ⋂ x ∈ s, f x
i : ι
hi : i ∈ s
hj : j ∉ f i
⊢ Eq.{u_5 + 1} (α := R) (∏ i ∈ s, (f i).indicator (g i) j) 0

Tactic:
Finset.prod_eq_zero hi <| Set.indicator_of_notMem hj _

Premises used: Finset.prod_eq_zero, Set.indicator_of_notMem
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
hj_1 : j ∉ ⋂ x ∈ s, f x
i : ι
hi : i ∈ s
hj : j ∉ f i
⊢ Eq.{u_5 + 1} (α := R) (∏ i ∈ s, (f i).indicator (g i) j) 0

Tactic:
exact Finset.prod_eq_zero hi <| Set.indicator_of_notMem hj _

Premises used: Finset.prod_eq_zero, Set.indicator_of_notMem
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
h :
  ∀ (a : κ), Eq.{u_5 + 1} (α := R) ((∏ i ∈ s, (f i).indicator (g i)) a) (Set.indicator (⋂ x ∈ s, f x) (∏ i ∈ s, g i) a)
⊢ Eq (α := (x : κ) → R) (∏ i ∈ s, (f i).indicator (g i)) (Set.indicator (⋂ x ∈ s, f x) (∏ i ∈ s, g i))

Tactic:
ext a
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
a : κ
⊢ Eq.{u_5 + 1} (α := R) ((∏ i ∈ s, (f i).indicator (g i)) a) (Set.indicator (⋂ x ∈ s, f x) (∏ i ∈ s, g i) a)

Tactic:
simpa using prod_indicator_apply ..

Premises used: prod_indicator_apply
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst : CommSemiring R
s : Finset ι
f : ι → Set κ
g : κ → R
j : κ
⊢ ∏ i ∈ s, (f i).indicator g j = Set.indicator (⋂ x ∈ s, f x) (g ^ #s) j

Tactic:
simp [prod_indicator_apply]

Premises used: prod_indicator_apply
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst : CommSemiring R
s : Finset ι
f : ι → Set κ
g : κ → R
⊢ ∏ i ∈ s, (f i).indicator g = Set.indicator (⋂ x ∈ s, f x) (g ^ #s)

Tactic:
simp [prod_indicator]

Premises used: prod_indicator
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
I : Type u_7
inst : DecidableEq I
M : I → Type u_8
inst_1 : (i : I) → CommMonoid (M i)
inst_2 : Fintype I
f : (i : I) → M i
h : ∀ (a : I), (∏ i : I, Pi.mulSingle (M := M) i (f i)) a = f a
⊢ ∏ i : I, Pi.mulSingle (M := M) i (f i) = f

Tactic:
ext a
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
I : Type u_7
inst : DecidableEq I
M : I → Type u_8
inst_1 : (i : I) → CommMonoid (M i)
inst_2 : Fintype I
f : (i : I) → M i
a : I
⊢ (∏ i : I, Pi.mulSingle (M := M) i (f i)) a = f a

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
I : Type u_7
inst : DecidableEq I
M : I → Type u_8
inst_1 : (i : I) → CommMonoid (M i)
inst_2 : Finite I
N : Type u_9
inst_3 : CommMonoid N
g h : ((i : I) → M i) →* N
H :
  ∀ (i : I) (x : M i),
    Eq.{u_9 + 1} (α := N) ((g : (a : (i : I) → M i) → N) (Pi.mulSingle (M := M) i x) : N)
      ((h : (a : (i : I) → M i) → N) (Pi.mulSingle (M := M) i x) : N)
intro : ∀ (val : Fintype I), g = h
⊢ g = h

Tactic:
cases nonempty_fintype I

Premises used: nonempty_fintype
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
I : Type u_7
inst : DecidableEq I
M : I → Type u_8
inst_1 : (i : I) → CommMonoid (M i)
inst_2 : Finite I
N : Type u_9
inst_3 : CommMonoid N
g h : ((i : I) → M i) →* N
H :
  ∀ (i : I) (x : M i),
    Eq.{u_9 + 1} (α := N) ((g : (a : (i : I) → M i) → N) (Pi.mulSingle (M := M) i x) : N)
      ((h : (a : (i : I) → M i) → N) (Pi.mulSingle (M := M) i x) : N)
val : Fintype I
intro :
  ∀ (k : (i : I) → M i),
    Eq.{u_9 + 1} (α := N) ((g : (a : (i : I) → M i) → N) k : N) ((h : (a : (i : I) → M i) → N) k : N)
⊢ g = h

Tactic:
ext k