awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action
Goal:
N : Type u_2
inst : CommMonoid N
G : Type u_4
inst_1 : Group G
inst_2 : MulDistribMulAction G N
inst_3 : Finite G
b : N
g : G
val : Fintype G
⊢ HSMul.hSMul (β := N) g (∏ᶠ (h : G), h • b) = ∏ᶠ (h : G), h • b

Tactic:
simp only [finprod_eq_prod_of_fintype, Finset.smul_prod_perm]

Premises used: finprod_eq_prod_of_fintype, Finset.smul_prod_perm
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : MulOneClass N
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
inst_4 : SMulCommClass M N N
m : M
⊢ HSMul.hSMul (β := N) (m ^ length.{u_2} (α := N) []) (prod []) = prod (map (fun (x : N) ↦ m • x) [])

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : MulOneClass N
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
inst_4 : SMulCommClass M N N
m : M
head : N
tail : List N
ih : m ^ tail.length • tail.prod = prod (map (fun (x : N) ↦ m • x) tail)
⊢ m ^ (head :: tail).length • (head :: tail).prod = prod (map (fun (x : N) ↦ m • x) (head :: tail))

Tactic:
simp [← ih, smul_mul_smul_comm, pow_succ']

Premises used: smul_mul_smul_comm, pow_succ'
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : MulOneClass N
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
inst_4 : SMulCommClass M N N
l : List N
m : M
nil : HSMul.hSMul (β := N) (m ^ length.{u_2} (α := N) []) (prod []) = prod (map (fun (x : N) ↦ m • x) [])
cons :
  ∀ (head : N) (tail : List N) (ih : m ^ tail.length • tail.prod = prod (map (fun (x : N) ↦ m • x) tail)),
    m ^ (head :: tail).length • (head :: tail).prod = prod (map (fun (x : N) ↦ m • x) (head :: tail))
⊢ m ^ l.length • l.prod = prod (map (fun (x : N) ↦ m • x) l)

Tactic:
induction l with
  | nil => simp
  | cons head tail ih => simp [← ih, smul_mul_smul_comm, pow_succ']

Premises used: List.head, smul_mul_smul_comm, List.tail, List.cons, pow_succ', List.nil
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : CommMonoid N
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
inst_4 : SMulCommClass M N N
s : Multiset N
b : M
⊢ ∀ (a : List N),
    b ^ card (Quot.mk (⇑(List.isSetoid N) : List N → List N → Prop) a) •
        prod (Quot.mk (⇑(List.isSetoid N) : List N → List N → Prop) a) =
      prod (map (fun (x : N) ↦ b • x) (Quot.mk (⇑(List.isSetoid N) : List N → List N → Prop) a))

Tactic:
simp [List.smul_prod]

Premises used: List.smul_prod
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action
Goal:
M : Type u_1
N : Type u_2
ι : Type u_4
inst : CommMonoid N
inst_1 : Monoid M
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
inst_4 : SMulCommClass M N N
s : Finset ι
b : M
f : ι → N
⊢ Eq (α := Multiset N) (Multiset.map (fun (x : ι) ↦ b • f x) s.val)
    (Multiset.map (fun (x : N) ↦ b • x) (Multiset.map f s.val))

Tactic:
simp only [Multiset.map_map, Function.comp_apply]

Premises used: Multiset.map_map, Function.comp_apply
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action
Goal:
M : Type u_1
N : Type u_2
ι : Type u_4
inst : CommMonoid N
inst_1 : Monoid M
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
inst_4 : SMulCommClass M N N
s : Finset ι
b : M
f : ι → N
⊢ Eq (α := Multiset N) (Multiset.map (fun (x : ι) ↦ b • f x) s.val)
    (Multiset.map (fun (x : N) ↦ b • x) (Multiset.map f s.val))

Tactic:
have : Multiset.map (fun (x : ι) ↦ b • f x) s.val =
      Multiset.map (fun x ↦ b • x) (Multiset.map f s.val) := by
    simp only [Multiset.map_map, Function.comp_apply]
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action
Goal:
M : Type u_1
N : Type u_2
ι : Type u_4
inst : CommMonoid N
inst_1 : Monoid M
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
inst_4 : SMulCommClass M N N
s : Finset ι
b : M
f : ι → N
this :
  Eq (α := Multiset N) (Multiset.map (fun (x : ι) ↦ b • f x) s.val)
    (Multiset.map (fun (x : N) ↦ b • x) (Multiset.map f s.val))
simp_rw : b ^ #s • (Multiset.map f s.val).prod = Multiset.prod (Multiset.map (fun (x : ι) ↦ b • f x) s.val)
simp_rw₁ : b ^ s.val.card • (Multiset.map f s.val).prod = Multiset.prod (Multiset.map (fun (x : ι) ↦ b • f x) s.val)
simp_rw₂ :
  b ^ s.val.card • (Multiset.map f s.val).prod =
    Multiset.prod (Multiset.map (fun (x : N) ↦ b • x) (Multiset.map f s.val))
simp_rw₃ : b ^ s.val.card • (Multiset.map f s.val).prod = b ^ (Multiset.map f s.val).card • (Multiset.map f s.val).prod
⊢ HSMul.hSMul (β := N) (b ^ #s) (∏ x ∈ s, f x) = ∏ x ∈ s, b • f x

Tactic:
simp_rw [prod_eq_multiset_prod, card_def, this, ← Multiset.smul_prod _ b, Multiset.card_map]

Premises used: Finset.prod_eq_multiset_prod, Finset.card_def, Multiset.smul_prod, Multiset.card_map
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action
Goal:
M : Type u_1
N : Type u_2
ι : Type u_4
inst : CommMonoid N
inst_1 : CommMonoid M
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
inst_4 : SMulCommClass M N N
b : ι → M
f : ι → N
⊢ ∏ i ∈ ∅, b i • f i = HSMul.hSMul.{u_1, u_2, u_2} (α := M) (β := N) (∏ i ∈ ∅, b i) (∏ i ∈ ∅, f i)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action
Goal:
M : Type u_1
N : Type u_2
ι : Type u_4
inst : CommMonoid N
inst_1 : CommMonoid M
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
inst_4 : SMulCommClass M N N
b : ι → M
f : ι → N
a : ι
s : Finset ι
hj : a ∉ s
ih : ∏ i ∈ s, b i • f i = HSMul.hSMul.{u_1, u_2, u_2} (α := M) (β := N) (∏ i ∈ s, b i) (∏ i ∈ s, f i)
cons :
  b a • f a * ∏ x ∈ s, b x • f x =
    HSMul.hSMul.{u_1, u_2, u_2} (α := M) (β := N) (∏ i ∈ Finset.cons a s hj, b i) (∏ i ∈ Finset.cons a s hj, f i)
cons₁ :
  b a • f a * HSMul.hSMul.{u_1, u_2, u_2} (α := M) (β := N) (∏ i ∈ s, b i) (∏ i ∈ s, f i) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := M) (β := N) (∏ i ∈ Finset.cons a s hj, b i) (∏ i ∈ Finset.cons a s hj, f i)
cons₂ :
  (b a * ∏ i ∈ s, b i) • (f a * ∏ i ∈ s, f i) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := M) (β := N) (∏ i ∈ Finset.cons a s hj, b i) (∏ i ∈ Finset.cons a s hj, f i)
cons₃ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := M) (∏ x ∈ Finset.cons a s hj, b x) (f a * ∏ i ∈ s, f i) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := M) (β := N) (∏ i ∈ Finset.cons a s hj, b i) (∏ i ∈ Finset.cons a s hj, f i)
cons₄ cons₅ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := M) (β := N) (∏ x ∈ Finset.cons a s hj, b x) (∏ x ∈ Finset.cons a s hj, f x) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := M) (β := N) (∏ i ∈ Finset.cons a s hj, b i) (∏ i ∈ Finset.cons a s hj, f i)
⊢ ∏ i ∈ Finset.cons a s hj, b i • f i =
    HSMul.hSMul.{u_1, u_2, u_2} (α := M) (β := N) (∏ i ∈ Finset.cons a s hj, b i) (∏ i ∈ Finset.cons a s hj, f i)

Tactic:
rw [prod_cons, ih, smul_mul_smul_comm, ← prod_cons hj, ← prod_cons hj]

Premises used: smul_mul_smul_comm, Finset.prod_cons
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action
Goal:
M : Type u_1
N : Type u_2
ι : Type u_4
inst : CommMonoid N
inst_1 : CommMonoid M
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
inst_4 : SMulCommClass M N N
s : Finset ι
b : ι → M
f : ι → N
empty : ∏ i ∈ ∅, b i • f i = HSMul.hSMul.{u_1, u_2, u_2} (α := M) (β := N) (∏ i ∈ ∅, b i) (∏ i ∈ ∅, f i)
cons :
  ∀ (a : ι) (s : Finset ι) (hj : a ∉ s)
    (ih : ∏ i ∈ s, b i • f i = HSMul.hSMul.{u_1, u_2, u_2} (α := M) (β := N) (∏ i ∈ s, b i) (∏ i ∈ s, f i)),
    ∏ i ∈ Finset.cons a s hj, b i • f i =
      HSMul.hSMul.{u_1, u_2, u_2} (α := M) (β := N) (∏ i ∈ Finset.cons a s hj, b i) (∏ i ∈ Finset.cons a s hj, f i)
⊢ ∏ i ∈ s, b i • f i = HSMul.hSMul.{u_1, u_2, u_2} (α := M) (β := N) (∏ i ∈ s, b i) (∏ i ∈ s, f i)

Tactic:
induction s using Finset.cons_induction_on with
  | empty => simp
  | cons _ _ hj ih => rw [prod_cons, ih, smul_mul_smul_comm, ← prod_cons hj, ← prod_cons hj]

Premises used: Finset.cons, smul_mul_smul_comm, Finset.prod_cons
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
M₀ : Type u_4
inst : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
i : ι
hi : i ∈ s
h : f i = 0
rw : (∏ x ∈ s.erase i, f x) * f i = 0
rw₁ : HMul.hMul (α := M₀) (∏ x ∈ s.erase i, f x) 0 = 0
rw₂ rw₃ : Eq.{u_4 + 1} (α := M₀) 0 0
⊢ Eq.{u_4 + 1} (α := M₀) (∏ j ∈ s, f j) 0

Tactic:
rw [← prod_erase_mul _ _ hi, h, mul_zero]

Premises used: Finset.prod_erase_mul, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
M₀ : Type u_4
inst : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
i : ι
hi : i ∈ s
h : f i = 0
classical : (∏ x ∈ s.erase i, f x) * f i = 0
classical₁ : HMul.hMul (α := M₀) (∏ x ∈ s.erase i, f x) 0 = 0
classical₂ classical₃ : Eq.{u_4 + 1} (α := M₀) 0 0
⊢ Eq.{u_4 + 1} (α := M₀) (∏ j ∈ s, f j) 0

Tactic:
classical rw [← prod_erase_mul _ _ hi, h, mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
M₀ : Type u_4
inst : CommMonoidWithZero M₀
p : ι → Prop
inst_1 : DecidablePred p
f : ι → M₀
s : Finset ι
pos : ∀ (h : ∀ i ∈ s, p i), Eq.{u_4 + 1} (α := M₀) (∏ i ∈ s, if p i then f i else 0) (∏ i ∈ s, f i)
neg : ∀ (h : ¬∀ i ∈ s, p i), Eq.{u_4 + 1} (α := M₀) (∏ i ∈ s, if p i then f i else 0) 0
⊢ Eq.{u_4 + 1} (α := M₀) (∏ i ∈ s, if p i then f i else 0) (if ∀ i ∈ s, p i then ∏ i ∈ s, f i else 0)

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
M₀ : Type u_4
inst : CommMonoidWithZero M₀
p : ι → Prop
inst_1 : DecidablePred p
f : ι → M₀
s : Finset ι
h : ∀ i ∈ s, p i
i : ι
hi : i ∈ s
⊢ (if p i then f i else 0) = f i

Tactic:
simp [h i hi]
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
M₀ : Type u_4
inst : CommMonoidWithZero M₀
p : ι → Prop
inst_1 : DecidablePred p
f : ι → M₀
s : Finset ι
h : ∀ i ∈ s, p i
⊢ Eq.{u_4 + 1} (α := M₀) (∏ i ∈ s, if p i then f i else 0) (∏ i ∈ s, f i)

Tactic:
exact prod_congr rfl fun i hi => by simp [h i hi]

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
M₀ : Type u_4
inst : CommMonoidWithZero M₀
p : ι → Prop
inst_1 : DecidablePred p
f : ι → M₀
s : Finset ι
h : ¬∀ i ∈ s, p i
⊢ ∃ i ∈ s, ¬p i

Tactic:
push Not at h

Premises used: Not
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
M₀ : Type u_4
inst : CommMonoidWithZero M₀
p : ι → Prop
inst_1 : DecidablePred p
f : ι → M₀
s : Finset ι
h : ∃ i ∈ s, ¬p i
neg : ∀ (i : ι) (hi : i ∈ s) (hq : ¬p i), Eq.{u_4 + 1} (α := M₀) (∏ i ∈ s, if p i then f i else 0) 0
⊢ Eq.{u_4 + 1} (α := M₀) (∏ i ∈ s, if p i then f i else 0) 0

Tactic:
rcases h with ⟨i, hi, hq⟩
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
M₀ : Type u_4
inst : CommMonoidWithZero M₀
p : ι → Prop
inst_1 : DecidablePred p
f : ι → M₀
s : Finset ι
i : ι
hi : i ∈ s
hq : ¬p i
⊢ (if p i then f i else 0) = 0

Tactic:
simp [hq]
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
M₀ : Type u_4
inst : CommMonoidWithZero M₀
p : ι → Prop
inst_1 : DecidablePred p
f : ι → M₀
s : Finset ι
i : ι
hi : i ∈ s
hq : ¬p i
⊢ Eq.{u_4 + 1} (α := M₀) (∏ i ∈ s, if p i then f i else 0) 0

Tactic:
exact prod_eq_zero hi (by simp [hq])

Premises used: Finset.prod_eq_zero
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
M₀ : Type u_4
inst : CommMonoidWithZero M₀
p : ι → Prop
inst_1 : DecidablePred p
s : Finset ι
rw : Eq.{u_4 + 1} (α := M₀) (if ∀ i ∈ s, p i then ∏ i ∈ s, 1 else 0) (if ∀ i ∈ s, p i then 1 else 0)
rw₁ rw₂ : Eq.{u_4 + 1} (α := M₀) (if ∀ i ∈ s, p i then 1 else 0) (if ∀ i ∈ s, p i then 1 else 0)
⊢ Eq.{u_4 + 1} (α := M₀) (∏ i ∈ s, if p i then 1 else 0) (if ∀ i ∈ s, p i then 1 else 0)

Tactic:
rw [prod_ite_zero, prod_const_one]

Premises used: Finset.prod_ite_zero, Finset.prod_const_one
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst : CommMonoidWithZero M₀
s : Finset ι
f : ι → κ → M₀
⊢ Subset.{u_2} (α := Set κ) (support.{u_2, u_4} (M := M₀) fun (x : κ) ↦ ∏ i ∈ s, f i x) (⋂ i ∈ s, support (f i))

Tactic:
fun _ hx ↦ Set.mem_iInter₂.2 fun _ hi H ↦ hx <| prod_eq_zero hi H

Premises used: Iff.mpr, Set.mem_iInter₂, Set.Subset, Finset.prod_eq_zero
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
M₀ : Type u_4
α : ι → Type u_5
inst : CommMonoidWithZero M₀
s : Finset ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ Eq.{u_4 + 1} (α := M₀) (((↑s : Set ι).pi (α := α) t).indicator 1 f) (∏ i ∈ s, (t i).indicator 1 (f i))

Tactic:
simp [Set.indicator, prod_boole]

Premises used: Set.indicator, Finset.prod_boole
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
M₀ : Type u_4
α : ι → Type u_5
inst : CommMonoidWithZero M₀
s : Finset ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ Eq.{u_4 + 1} (α := M₀) (((↑s : Set ι).pi (α := α) t).indicator 1 f) (∏ i ∈ s, (t i).indicator 1 (f i))

Tactic:
classical simp [Set.indicator, prod_boole]

Premises used: Set.indicator, Finset.prod_boole
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
M₀ : Type u_4
inst : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
h : ∃ (a : ι), Membership.mem (γ := Finset ι) ∅ a ∧ f a = 0
w : ι
H : Membership.mem (γ := Finset ι) ∅ w
right : f w = 0
⊢ Eq.{u_4 + 1} (α := M₀) (∏ x ∈ ∅, f x) 0

Tactic:
simp at H
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
M₀ : Type u_4
inst : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
⊢ Eq.{u_4 + 1} (α := M₀) (∏ x ∈ ∅, f x) 0 ↔ ∃ (a : ι), Membership.mem (γ := Finset ι) ∅ a ∧ f a = 0

Tactic:
exact ⟨Not.elim one_ne_zero, fun ⟨_, H, _⟩ => by simp at H⟩
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
M₀ : Type u_4
inst : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
a : ι
s_1 : Finset ι
ha : a ∉ s_1
ih : Eq.{u_4 + 1} (α := M₀) (∏ x ∈ s_1, f x) 0 ↔ ∃ a ∈ s_1, f a = 0
insert : f a * ∏ x ∈ s_1, f x = 0 ↔ ∃ a_1 ∈ Insert.insert a s_1, f a_1 = 0
insert₁ : f a = 0 ∨ Eq.{u_4 + 1} (α := M₀) (∏ x ∈ s_1, f x) 0 ↔ ∃ a_1 ∈ Insert.insert a s_1, f a_1 = 0
insert₂ : f a = 0 ∨ Eq.{u_4 + 1} (α := M₀) (∏ x ∈ s_1, f x) 0 ↔ f a = 0 ∨ ∃ x ∈ s_1, f x = 0
insert₃ insert₄ : (f a = 0 ∨ ∃ a ∈ s_1, f a = 0) ↔ f a = 0 ∨ ∃ x ∈ s_1, f x = 0
⊢ Eq.{u_4 + 1} (α := M₀) (∏ x ∈ Insert.insert a s_1, f x) 0 ↔ ∃ a_1 ∈ Insert.insert a s_1, f a_1 = 0

Tactic:
rw [prod_insert ha, mul_eq_zero, exists_mem_insert, ih]

Premises used: Finset.prod_insert, Finset.exists_mem_insert, mul_eq_zero
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
M₀ : Type u_4
inst : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
empty : Eq.{u_4 + 1} (α := M₀) (∏ x ∈ ∅, f x) 0 ↔ ∃ (a : ι), Membership.mem (γ := Finset ι) ∅ a ∧ f a = 0
insert :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s) (ih : Eq.{u_4 + 1} (α := M₀) (∏ x ∈ s, f x) 0 ↔ ∃ a ∈ s, f a = 0),
    Eq.{u_4 + 1} (α := M₀) (∏ x ∈ Insert.insert a s, f x) 0 ↔ ∃ a_1 ∈ Insert.insert a s, f a_1 = 0
⊢ Eq.{u_4 + 1} (α := M₀) (∏ x ∈ s, f x) 0 ↔ ∃ a ∈ s, f a = 0

Tactic:
induction s using Finset.induction_on with
    | empty => exact ⟨Not.elim one_ne_zero, fun ⟨_, H, _⟩ => by simp at H⟩
    | insert _ _ ha ih => rw [prod_insert ha, mul_eq_zero, exists_mem_insert, ih]

Premises used: Finset.exists_mem_insert, Insert.insert, mul_eq_zero
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
M₀ : Type u_4
inst : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
empty : Eq.{u_4 + 1} (α := M₀) (∏ x ∈ ∅, f x) 0 ↔ ∃ (a : ι), Membership.mem (γ := Finset ι) ∅ a ∧ f a = 0
insert :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s) (ih : Eq.{u_4 + 1} (α := M₀) (∏ x ∈ s, f x) 0 ↔ ∃ a ∈ s, f a = 0),
    Eq.{u_4 + 1} (α := M₀) (∏ x ∈ Insert.insert a s, f x) 0 ↔ ∃ a_1 ∈ Insert.insert a s, f a_1 = 0
⊢ Eq.{u_4 + 1} (α := M₀) (∏ x ∈ s, f x) 0 ↔ ∃ a ∈ s, f a = 0

Tactic:
classical
    induction s using Finset.induction_on with
    | empty => exact ⟨Not.elim one_ne_zero, fun ⟨_, H, _⟩ => by simp at H⟩
    | insert _ _ ha ih => rw [prod_insert ha, mul_eq_zero, exists_mem_insert, ih]

Premises used: Finset.exists_mem_insert, Insert.insert, mul_eq_zero
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
M₀ : Type u_4
inst : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
rw : (¬∃ a ∈ s, f a = 0) ↔ ∀ a ∈ s, f a ≠ 0
⊢ Ne.{u_4 + 1} (α := M₀) (∏ x ∈ s, f x) 0 ↔ ∀ a ∈ s, f a ≠ 0

Tactic:
rw [Ne, prod_eq_zero_iff]

Premises used: Ne, Finset.prod_eq_zero_iff
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
M₀ : Type u_4
inst : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
push : (∀ (a : ι) (_ : a ∈ s), f a ≠ 0) ↔ ∀ a ∈ s, f a ≠ 0
⊢ (¬∃ a ∈ s, f a = 0) ↔ ∀ a ∈ s, f a ≠ 0

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
M₀ : Type u_4
inst : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
⊢ (∀ (a : ι) (_ : a ∈ s), f a ≠ 0) ↔ ∀ a ∈ s, f a ≠ 0

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst : CommMonoidWithZero M₀
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
s : Finset ι
f : ι → κ → M₀
x : κ
⊢ Membership.mem (γ := Set κ) (support.{u_2, u_4} (M := M₀) fun (j : κ) ↦ ∏ i ∈ s, f i j) x ↔
    Membership.mem (γ := Set κ) (⋂ i ∈ s, support (f i)) x

Tactic:
simp [support, prod_eq_zero_iff]

Premises used: Finset.prod_eq_zero_iff, Function.support
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
M₀ : Type u_4
inst : Fintype ι
inst_1 : CommMonoidWithZero M₀
p : ι → Prop
inst_2 : DecidablePred p
f : ι → M₀
⊢ Eq.{u_4 + 1} (α := M₀) (∏ i : ι, if p i then f i else 0) (if ∀ (i : ι), p i then ∏ i : ι, f i else 0)

Tactic:
simp [Finset.prod_ite_zero]

Premises used: Finset.prod_ite_zero
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
M₀ : Type u_4
inst : Fintype ι
inst_1 : CommMonoidWithZero M₀
p : ι → Prop
inst_2 : DecidablePred p
⊢ Eq.{u_4 + 1} (α := M₀) (∏ i : ι, if p i then 1 else 0) (if ∀ (i : ι), p i then 1 else 0)

Tactic:
simp [Finset.prod_boole]

Premises used: Finset.prod_boole
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
G₀ : Type u_3
inst : CommGroupWithZero G₀
s : Finset ι
f : ι → G₀
h : Ne.{u_3 + 1} (α := G₀) (∏ i ∈ s, f i) 0
empty :
  ∀ (h : Ne.{u_3 + 1} (α := G₀) (∏ i ∈ ∅, f i) 0), mk0 (∏ i ∈ ∅, f i) h = ∏ i ∈ Finset.attach ∅, mk0 (f (↑i : ι)) ⋯
cons :
  ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
    (∀ (h : Ne.{u_3 + 1} (α := G₀) (∏ i ∈ s, f i) 0), mk0 (∏ i ∈ s, f i) h = ∏ i ∈ s.attach, mk0 (f (↑i : ι)) ⋯) →
      ∀ (h_1 : Ne.{u_3 + 1} (α := G₀) (∏ i ∈ Finset.cons a s h, f i) 0),
        mk0 (∏ i ∈ Finset.cons a s h, f i) h_1 = ∏ i ∈ (Finset.cons a s h).attach, mk0 (f (↑i : ι)) ⋯
⊢ mk0 (∏ i ∈ s, f i) h = ∏ i ∈ s.attach, mk0 (f (↑i : ι)) ⋯

Tactic:
induction s using Finset.cons_induction_on
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
G₀ : Type u_3
inst : CommGroupWithZero G₀
f : ι → G₀
h : Ne.{u_3 + 1} (α := G₀) (∏ i ∈ ∅, f i) 0
⊢ mk0 (∏ i ∈ ∅, f i) h = ∏ i ∈ Finset.attach ∅, mk0 (f (↑i : ι)) ⋯

Tactic:
simp [*]
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
G₀ : Type u_3
inst : CommGroupWithZero G₀
f : ι → G₀
a : ι
s : Finset ι
h_1 : a ∉ s
h_2 : ∀ (h : Ne.{u_3 + 1} (α := G₀) (∏ i ∈ s, f i) 0), mk0 (∏ i ∈ s, f i) h = ∏ i ∈ s.attach, mk0 (f (↑i : ι)) ⋯
h : Ne.{u_3 + 1} (α := G₀) (∏ i ∈ Finset.cons a s h_1, f i) 0
⊢ mk0 (∏ i ∈ Finset.cons a s h_1, f i) h = ∏ i ∈ (Finset.cons a s h_1).attach, mk0 (f (↑i : ι)) ⋯

Tactic:
simp [*]
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
α : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : AddCommMonoid α
inst_2 : PartialOrder α
inst_3 : IsOrderedCancelAddMonoid α
inst_4 : ExistsAddOfLE α
inst_5 : LocallyFiniteOrder α
f : α → M
a b c : α
rw : Eq.{u_3 + 1} (α := M) (∏ x ∈ Ico a b, f (x + c)) (∏ x ∈ Ico a b, f ((addRightEmbedding c : (a : α) → α) x))
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ Ico a b, f (x + c)) (∏ x ∈ Ico (a + c) (b + c), f x)

Tactic:
rw [← map_add_right_Ico, prod_map]

Premises used: Finset.map_add_right_Ico, Finset.prod_map
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
α : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : AddCommMonoid α
inst_2 : PartialOrder α
inst_3 : IsOrderedCancelAddMonoid α
inst_4 : ExistsAddOfLE α
inst_5 : LocallyFiniteOrder α
f : α → M
a b c : α
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ Ico a b, f (x + c)) (∏ x ∈ Ico a b, f ((addRightEmbedding c : (a : α) → α) x))

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
α : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : AddCommMonoid α
inst_2 : PartialOrder α
inst_3 : IsOrderedCancelAddMonoid α
inst_4 : ExistsAddOfLE α
inst_5 : LocallyFiniteOrder α
f : α → M
a b c : α
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ Ico a b, f (x + c)) (∏ x ∈ Ico (a + c) (b + c), f x)

Tactic:
prod_Ico_add' f a b c

Premises used: Finset.prod_Ico_add'
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
α : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : AddCommMonoid α
inst_2 : PartialOrder α
inst_3 : IsOrderedCancelAddMonoid α
inst_4 : ExistsAddOfLE α
inst_5 : LocallyFiniteOrder α
f : α → M
a b c : α
h : ∀ x ∈ Ico a b, f (c + x) = f (x + c)
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ Ico a b, f (c + x)) (∏ x ∈ Ico (a + c) (b + c), f x)

Tactic:
convert! prod_Ico_add' f a b c using 2

Premises used: Finset.prod_Ico_add'
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
α : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : AddCommMonoid α
inst_2 : PartialOrder α
inst_3 : IsOrderedCancelAddMonoid α
inst_4 : ExistsAddOfLE α
inst_5 : LocallyFiniteOrder α
f : α → M
a b c x : α
h_1 : x ∈ Ico a b
h h₁ : f (x + c) = f (x + c)
⊢ f (c + x) = f (x + c)

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
α : Type u_1
M : Type u_3
inst : CommMonoid M
f : α → M
inst_1 : AddCommMonoid α
inst_2 : PartialOrder α
inst_3 : IsOrderedCancelAddMonoid α
inst_4 : ExistsAddOfLE α
inst_5 : LocallyFiniteOrder α
inst_6 : Sub α
inst_7 : OrderedSub α
a b c : α
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ Ico (a + c) (b + c), f (x - c)) (∏ x ∈ Ico a b, f x)

Tactic:
simp only [← map_add_right_Ico, prod_map, addRightEmbedding_apply, add_tsub_cancel_right]

Premises used: addRightEmbedding_apply, Finset.map_add_right_Ico, add_tsub_cancel_right, Finset.prod_map
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommMonoid M
a b : ℕ
hab : a ≤ b
f : ℕ → M
rw : ∏ k ∈ insert b (Ico a b), f k = (∏ k ∈ Ico a b, f k) * f b
rw₁ : f b * ∏ x ∈ Ico a b, f x = (∏ k ∈ Ico a b, f k) * f b
rw₂ rw₃ : (∏ x ∈ Ico a b, f x) * f b = (∏ k ∈ Ico a b, f k) * f b
⊢ ∏ k ∈ Ico a (b + 1), f k = (∏ k ∈ Ico a b, f k) * f b

Tactic:
rw [← Finset.insert_Ico_right_eq_Ico_add_one hab, prod_insert right_notMem_Ico, mul_comm]

Premises used: Finset.prod_insert, Finset.right_notMem_Ico, Finset.insert_Ico_right_eq_Ico_add_one, mul_comm
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
⊢ HMul.hMul (α := M) (∏ i ∈ Ico m n, f i) (∏ i ∈ Ico n k, f i) = ∏ i ∈ Ico m k, f i

Tactic:
Ico_union_Ico_eq_Ico hmn hnk ▸ Eq.symm (prod_union (Ico_disjoint_Ico_consecutive m n k))

Premises used: Finset.Ico_disjoint_Ico_consecutive, Eq.rec, Finset.prod_union, Finset.Ico_union_Ico_eq_Ico, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
rw : Disjoint (Ioc m n) (Ioc n k)
⊢ HMul.hMul (α := M) (∏ i ∈ Ioc m n, f i) (∏ i ∈ Ioc n k, f i) = ∏ i ∈ Ioc m k, f i

Tactic:
rw [← Ioc_union_Ioc_eq_Ioc hmn hnk, prod_union]

Premises used: Finset.Ioc_union_Ioc_eq_Ioc, Finset.prod_union