awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Action (goal)
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)
⊢ ∏ 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)
have 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)
Tactic: rw [prod_cons, ih, smul_mul_smul_comm, ← prod_cons hj, ← prod_cons hj]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Action (goal)
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)
⊢ ∏ 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)
have 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)
Tactic: rw [prod_cons, ih, smul_mul_smul_comm, ← prod_cons hj, ← prod_cons hj]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Action (goal)
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)
⊢ ∏ 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)
have 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)
Tactic: rw [prod_cons, ih, smul_mul_smul_comm, ← prod_cons hj, ← prod_cons hj]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Action (goal)
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)
⊢ ∏ 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)
have 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)
Tactic: rw [prod_cons, ih, smul_mul_smul_comm, ← prod_cons hj, ← prod_cons hj]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Action (goal)
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
⊢ ∏ i ∈ s, b i • f i = HSMul.hSMul.{u_1, u_2, u_2} (α := M) (β := N) (∏ i ∈ s, b i) (∏ i ∈ s, f i)
have empty : ∏ i ∈ ∅, b i • f i = HSMul.hSMul.{u_1, u_2, u_2} (α := M) (β := N) (∏ i ∈ ∅, b i) (∏ i ∈ ∅, 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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Action (goal)
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)
⊢ ∏ i ∈ s, b i • f i = HSMul.hSMul.{u_1, u_2, u_2} (α := M) (β := N) (∏ i ∈ s, b i) (∏ i ∈ s, f i)
have 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 ∈ cons a s hj, b i • f i =
    HSMul.hSMul.{u_1, u_2, u_2} (α := M) (β := N) (∏ i ∈ cons a s hj, b i) (∏ i ∈ cons a s hj, 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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Finset (goal)
Goal:
ι : Type u_1
M₀ : Type u_4
inst : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
i : ι
hi : i ∈ s
h : f i = 0
⊢ Eq.{u_4 + 1} (α := M₀) (∏ j ∈ s, f j) 0
have rw : (∏ x ∈ s.erase i, f x) * f i = 0
Tactic: rw [← prod_erase_mul _ _ hi, h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Finset (goal)
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
⊢ Eq.{u_4 + 1} (α := M₀) (∏ j ∈ s, f j) 0
have rw₁ : HMul.hMul (α := M₀) (∏ x ∈ s.erase i, f x) 0 = 0
Tactic: rw [← prod_erase_mul _ _ hi, h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Finset (goal)
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
⊢ Eq.{u_4 + 1} (α := M₀) (∏ j ∈ s, f j) 0
have rw₂ : Eq.{u_4 + 1} (α := M₀) 0 0
Tactic: rw [← prod_erase_mul _ _ hi, h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Finset (goal)
Goal:
ι : Type u_1
M₀ : Type u_4
inst : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
i : ι
hi : i ∈ s
h : f i = 0
⊢ Eq.{u_4 + 1} (α := M₀) (∏ j ∈ s, f j) 0
have classical : (∏ x ∈ s.erase i, f x) * f i = 0
Tactic: classical rw [← prod_erase_mul _ _ hi, h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Finset (goal)
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
⊢ Eq.{u_4 + 1} (α := M₀) (∏ j ∈ s, f j) 0
have classical₁ : HMul.hMul (α := M₀) (∏ x ∈ s.erase i, f x) 0 = 0
Tactic: classical rw [← prod_erase_mul _ _ hi, h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Finset (goal)
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
⊢ Eq.{u_4 + 1} (α := M₀) (∏ j ∈ s, f j) 0
have classical₂ : Eq.{u_4 + 1} (α := M₀) 0 0
Tactic: classical rw [← prod_erase_mul _ _ hi, h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Finset (goal)
Goal:
ι : Type u_1
M₀ : Type u_4
inst : CommMonoidWithZero M₀
p : ι → Prop
inst_1 : DecidablePred p
f : ι → M₀
s : Finset ι
⊢ 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)
have 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)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Finset (goal)
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)
⊢ 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)
have neg : ∀ (h : ¬∀ i ∈ s, p i), Eq.{u_4 + 1} (α := M₀) (∏ i ∈ s, if p i then f i else 0) 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Finset (hypothesis)
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) 0
have h₁ : ∃ i ∈ s, ¬p i
Tactic: push Not at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Finset (goal)
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) 0
have neg : ∀ (i : ι) (hi : i ∈ s) (hq : ¬p i), Eq.{u_4 + 1} (α := M₀) (∏ i ∈ s, if p i then f i else 0) 0
Tactic: rcases h with ⟨i, hi, hq⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Finset (goal)
Goal:
ι : Type u_1
M₀ : Type u_4
inst : CommMonoidWithZero M₀
p : ι → Prop
inst_1 : DecidablePred p
s : Finset ι
⊢ Eq.{u_4 + 1} (α := M₀) (∏ i ∈ s, if p i then 1 else 0) (if ∀ i ∈ s, p i then 1 else 0)
have 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)
Tactic: rw [prod_ite_zero, prod_const_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Finset (goal)
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)
⊢ Eq.{u_4 + 1} (α := M₀) (∏ i ∈ s, if p i then 1 else 0) (if ∀ i ∈ s, p i then 1 else 0)
have rw₁ : Eq.{u_4 + 1} (α := M₀) (if ∀ i ∈ s, p i then 1 else 0) (if ∀ i ∈ s, p i then 1 else 0)
Tactic: rw [prod_ite_zero, prod_const_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Finset (goal)
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
⊢ Eq.{u_4 + 1} (α := M₀) (∏ x ∈ insert a s_1, f x) 0 ↔ ∃ a_1 ∈ insert a s_1, f a_1 = 0
have insert : f a * ∏ x ∈ s_1, f x = 0 ↔ ∃ a_1 ∈ insert a s_1, f a_1 = 0
Tactic: rw [prod_insert ha, mul_eq_zero, exists_mem_insert, ih]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Finset (goal)
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
⊢ 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
have 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
Tactic: rw [prod_insert ha, mul_eq_zero, exists_mem_insert, ih]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Finset (goal)
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
⊢ 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
have insert₂ : f a = 0 ∨ Eq.{u_4 + 1} (α := M₀) (∏ x ∈ s_1, f x) 0 ↔ f a = 0 ∨ ∃ x ∈ s_1, f x = 0
Tactic: rw [prod_insert ha, mul_eq_zero, exists_mem_insert, ih]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Finset (goal)
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
⊢ 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
have insert₃ : (f a = 0 ∨ ∃ a ∈ s_1, f a = 0) ↔ f a = 0 ∨ ∃ x ∈ s_1, f x = 0
Tactic: rw [prod_insert ha, mul_eq_zero, exists_mem_insert, ih]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Finset (goal)
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 ∈ s, f x) 0 ↔ ∃ a ∈ s, f a = 0
have empty : Eq.{u_4 + 1} (α := M₀) (∏ x ∈ ∅, f x) 0 ↔ ∃ (a : ι), Membership.mem (γ := Finset ι) ∅ a ∧ 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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Finset (goal)
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
⊢ Eq.{u_4 + 1} (α := M₀) (∏ x ∈ s, f x) 0 ↔ ∃ a ∈ s, f a = 0
have 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 a s, f x) 0 ↔ ∃ a_1 ∈ insert a s, f a_1 = 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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Finset (goal)
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 ∈ s, f x) 0 ↔ ∃ a ∈ s, f a = 0
have empty : Eq.{u_4 + 1} (α := M₀) (∏ x ∈ ∅, f x) 0 ↔ ∃ (a : ι), Membership.mem (γ := Finset ι) ∅ a ∧ 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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Finset (goal)
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
⊢ Eq.{u_4 + 1} (α := M₀) (∏ x ∈ s, f x) 0 ↔ ∃ a ∈ s, f a = 0
have 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 a s, f x) 0 ↔ ∃ a_1 ∈ insert a s, f a_1 = 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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Finset (goal)
Goal:
ι : Type u_1
M₀ : Type u_4
inst : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
⊢ Ne.{u_4 + 1} (α := M₀) (∏ x ∈ s, f x) 0 ↔ ∀ a ∈ s, f a ≠ 0
have rw : (¬∃ a ∈ s, f a = 0) ↔ ∀ a ∈ s, f a ≠ 0
Tactic: rw [Ne, prod_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Finset (goal)
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, f a = 0) ↔ ∀ a ∈ s, f a ≠ 0
have push : (∀ (a : ι) (_ : a ∈ s), f a ≠ 0) ↔ ∀ a ∈ s, f a ≠ 0
Tactic: push Not
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Finset (goal)
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
⊢ mk0 (∏ i ∈ s, f i) h = ∏ i ∈ s.attach, mk0 (f (↑i : ι)) ⋯
have empty : ∀ (h : Ne.{u_3 + 1} (α := G₀) (∏ i ∈ ∅, f i) 0), mk0 (∏ i ∈ ∅, f i) h = ∏ i ∈ Finset.attach ∅, mk0 (f (↑i : ι)) sorry
Tactic: induction s using Finset.cons_induction_on
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Finset (goal)
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 : ι)) ⋯
⊢ mk0 (∏ i ∈ s, f i) h = ∏ i ∈ s.attach, mk0 (f (↑i : ι)) ⋯
have 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 : ι)) sorry) →
    ∀ (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 : ι)) sorry
Tactic: induction s using Finset.cons_induction_on
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
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)
have rw : Eq.{u_3 + 1} (α := M) (∏ x ∈ Ico a b, f (x + c)) (∏ x ∈ Ico a b, f ((addRightEmbedding c : (a : α) → α) x))
Tactic: rw [← map_add_right_Ico, prod_map]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
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 (c + x)) (∏ x ∈ Ico (a + c) (b + c), f x)
have h : ∀ x ∈ Ico a b, f (c + x) = f (x + c)
Tactic: convert! prod_Ico_add' f a b c using 2
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
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 : x ∈ Ico a b
⊢ f (c + x) = f (x + c)
have h : f (x + c) = f (x + c)
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
a b : ℕ
hab : a ≤ b
f : ℕ → M
⊢ ∏ k ∈ Ico a (b + 1), f k = (∏ k ∈ Ico a b, f k) * f b
have rw : ∏ k ∈ insert b (Ico a b), 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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
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
⊢ ∏ k ∈ Ico a (b + 1), f k = (∏ k ∈ Ico a b, f k) * f b
have rw₁ : f b * ∏ x ∈ Ico a b, f x = (∏ 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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
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
⊢ ∏ k ∈ Ico a (b + 1), f k = (∏ k ∈ Ico a b, f k) * f b
have rw₂ : (∏ x ∈ Ico a b, f x) * f b = (∏ 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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
⊢ HMul.hMul (α := M) (∏ i ∈ Ioc m n, f i) (∏ i ∈ Ioc n k, f i) = ∏ i ∈ Ioc m k, f i
have rw : Disjoint (Ioc m n) (Ioc n k)
Tactic: rw [← Ioc_union_Ioc_eq_Ioc hmn hnk, prod_union]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
⊢ Disjoint (Ioc m n) (Ioc n k)
have apply : ∀ (x : ℕ) (hx : x ∈ Ioc m n) (h'x : x ∈ Ioc n k), False
Tactic: apply disjoint_left.2 fun x hx h'x => _
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
a b : ℕ
hab : a ≤ b
f : ℕ → M
⊢ ∏ k ∈ Ioc a (b + 1), f k = (∏ k ∈ Ioc a b, f k) * f (b + 1)
have rw : HMul.hMul (α := M) (∏ i ∈ Ioc a b, f i) (∏ i ∈ Ioc b b.succ, f i) = (∏ k ∈ Ioc a b, f k) * f (b + 1)
Tactic: rw [← prod_Ioc_consecutive _ hab (Nat.le_succ b), Nat.Ioc_succ_singleton, prod_singleton]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
a b : ℕ
hab : a ≤ b
f : ℕ → M
rw : HMul.hMul (α := M) (∏ i ∈ Ioc a b, f i) (∏ i ∈ Ioc b b.succ, f i) = (∏ k ∈ Ioc a b, f k) * f (b + 1)
⊢ ∏ k ∈ Ioc a (b + 1), f k = (∏ k ∈ Ioc a b, f k) * f (b + 1)
have rw₁ : HMul.hMul (α := M) (∏ i ∈ Ioc a b, f i) (∏ i ∈ {b + 1}, f i) = (∏ k ∈ Ioc a b, f k) * f (b + 1)
Tactic: rw [← prod_Ioc_consecutive _ hab (Nat.le_succ b), Nat.Ioc_succ_singleton, prod_singleton]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
a b : ℕ
hab : a ≤ b
f : ℕ → M
rw : HMul.hMul (α := M) (∏ i ∈ Ioc a b, f i) (∏ i ∈ Ioc b b.succ, f i) = (∏ k ∈ Ioc a b, f k) * f (b + 1)
rw₁ : HMul.hMul (α := M) (∏ i ∈ Ioc a b, f i) (∏ i ∈ {b + 1}, f i) = (∏ k ∈ Ioc a b, f k) * f (b + 1)
⊢ ∏ k ∈ Ioc a (b + 1), f k = (∏ k ∈ Ioc a b, f k) * f (b + 1)
have rw₂ : (∏ i ∈ Ioc a b, f i) * f (b + 1) = (∏ k ∈ Ioc a b, f k) * f (b + 1)
Tactic: rw [← prod_Ioc_consecutive _ hab (Nat.le_succ b), Nat.Ioc_succ_singleton, prod_singleton]