awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
f : ℕ → M
n : ℕ
rw : ∏ k ∈ range (n + 1 + 1), f k = (∏ x ∈ range n, f (x + 1)) * f (n + 1) * f 0
rw₁ : ∏ k ∈ range (n + 1 + 1), f k = (∏ x ∈ range n, f (x + 1)) * f 0 * f (n + 1)
rw₂ : ∏ k ∈ range (n + 1 + 1), f k = (∏ k ∈ range (n + 1), f k) * f (n + 1)
⊢ ∏ k ∈ range (n + 1 + 1), f k = (∏ k ∈ range (n + 1), f (k + 1)) * f 0
have rw₃ : (∏ x ∈ range (n + 1), f x) * f (n + 1) = (∏ k ∈ range (n + 1), f k) * f (n + 1)
Tactic: rw [prod_range_succ _ n, mul_right_comm, ← prod_range_succ' _ n, prod_range_succ]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
u : ℕ → M
N : ℕ
hu : ∀ n ≥ N, u n = 1
n : ℕ
hn : N ≤ n
⊢ Eq.{u_4 + 1} (α := M) (∏ k ∈ range n, u k) (∏ k ∈ range N, u k)
have obtain : ∀ (m : ℕ) (hn : N ≤ N + m), Eq.{u_4 + 1} (α := M) (∏ k ∈ range (N + m), u k) (∏ k ∈ range N, u k)
Tactic: obtain ⟨m, rfl : n = N + m⟩ := Nat.exists_eq_add_of_le hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
u : ℕ → M
N : ℕ
hu : ∀ n ≥ N, u n = 1
m : ℕ
⊢ Eq.{u_4 + 1} (α := M) (∏ k ∈ range (N + m), u k) (∏ k ∈ range N, u k)
have zero : Eq.{u_4 + 1} (α := M) (∏ k ∈ range (N + 0), u k) (∏ k ∈ range N, u k)
Tactic: induction m with
  | zero => simp
  | succ m hm => simp [← add_assoc, prod_range_succ, hm, hu]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
u : ℕ → M
N : ℕ
hu : ∀ n ≥ N, u n = 1
m : ℕ
zero : Eq.{u_4 + 1} (α := M) (∏ k ∈ range (N + 0), u k) (∏ k ∈ range N, u k)
⊢ Eq.{u_4 + 1} (α := M) (∏ k ∈ range (N + m), u k) (∏ k ∈ range N, u k)
have succ : ∀ (m : ℕ) (hm : Eq.{u_4 + 1} (α := M) (∏ k ∈ range (N + m), u k) (∏ k ∈ range N, u k)),
  Eq.{u_4 + 1} (α := M) (∏ k ∈ range (N + (m + 1)), u k) (∏ k ∈ range N, u k)
Tactic: induction m with
  | zero => simp
  | succ m hm => simp [← add_assoc, prod_range_succ, hm, hu]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
f : ℕ → M
n m : ℕ
hm : ∏ x ∈ range (n + m), f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range m, f (n + x))
⊢ ∏ x ∈ range (n + (m + 1)), f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range (m + 1), f (n + x))
have succ : ∏ x ∈ range (n + m).succ, f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range (m + 1), f (n + x))
Tactic: rw [Nat.add_succ, prod_range_succ, prod_range_succ, hm, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
f : ℕ → M
n m : ℕ
hm : ∏ x ∈ range (n + m), f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range m, f (n + x))
succ : ∏ x ∈ range (n + m).succ, f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range (m + 1), f (n + x))
⊢ ∏ x ∈ range (n + (m + 1)), f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range (m + 1), f (n + x))
have succ₁ : (∏ x ∈ range (n + m), f x) * f (n + m) = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range (m + 1), f (n + x))
Tactic: rw [Nat.add_succ, prod_range_succ, prod_range_succ, hm, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
f : ℕ → M
n m : ℕ
hm : ∏ x ∈ range (n + m), f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range m, f (n + x))
succ : ∏ x ∈ range (n + m).succ, f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range (m + 1), f (n + x))
succ₁ :
  (∏ x ∈ range (n + m), f x) * f (n + m) = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range (m + 1), f (n + x))
⊢ ∏ x ∈ range (n + (m + 1)), f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range (m + 1), f (n + x))
have succ₂ : (∏ x ∈ range (n + m), f x) * f (n + m) = (∏ x ∈ range n, f x) * ((∏ x ∈ range m, f (n + x)) * f (n + m))
Tactic: rw [Nat.add_succ, prod_range_succ, prod_range_succ, hm, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
f : ℕ → M
n m : ℕ
hm : ∏ x ∈ range (n + m), f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range m, f (n + x))
succ : ∏ x ∈ range (n + m).succ, f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range (m + 1), f (n + x))
succ₁ :
  (∏ x ∈ range (n + m), f x) * f (n + m) = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range (m + 1), f (n + x))
succ₂ : (∏ x ∈ range (n + m), f x) * f (n + m) = (∏ x ∈ range n, f x) * ((∏ x ∈ range m, f (n + x)) * f (n + m))
⊢ ∏ x ∈ range (n + (m + 1)), f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range (m + 1), f (n + x))
have succ₃ : HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range m, f (n + x)) * f (n + m) =
  (∏ x ∈ range n, f x) * ((∏ x ∈ range m, f (n + x)) * f (n + m))
Tactic: rw [Nat.add_succ, prod_range_succ, prod_range_succ, hm, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
f : ℕ → M
n m : ℕ
hm : ∏ x ∈ range (n + m), f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range m, f (n + x))
succ : ∏ x ∈ range (n + m).succ, f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range (m + 1), f (n + x))
succ₁ :
  (∏ x ∈ range (n + m), f x) * f (n + m) = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range (m + 1), f (n + x))
succ₂ : (∏ x ∈ range (n + m), f x) * f (n + m) = (∏ x ∈ range n, f x) * ((∏ x ∈ range m, f (n + x)) * f (n + m))
succ₃ :
  HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range m, f (n + x)) * f (n + m) =
    (∏ x ∈ range n, f x) * ((∏ x ∈ range m, f (n + x)) * f (n + m))
⊢ ∏ x ∈ range (n + (m + 1)), f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range (m + 1), f (n + x))
have succ₄ : (∏ x ∈ range n, f x) * ((∏ x ∈ range m, f (n + x)) * f (n + m)) =
  (∏ x ∈ range n, f x) * ((∏ x ∈ range m, f (n + x)) * f (n + m))
Tactic: rw [Nat.add_succ, prod_range_succ, prod_range_succ, hm, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
f : ℕ → M
n m : ℕ
⊢ ∏ x ∈ range (n + m), f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range m, f (n + x))
have zero : ∏ x ∈ range (n + 0), f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range 0, f (n + x))
Tactic: induction m with
  | zero => simp
  | succ m hm => rw [Nat.add_succ, prod_range_succ, prod_range_succ, hm, mul_assoc]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
f : ℕ → M
n m : ℕ
zero : ∏ x ∈ range (n + 0), f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range 0, f (n + x))
⊢ ∏ x ∈ range (n + m), f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range m, f (n + x))
have succ : ∀ (m : ℕ) (hm : ∏ x ∈ range (n + m), f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range m, f (n + x))),
  ∏ x ∈ range (n + (m + 1)), f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range (m + 1), f (n + x))
Tactic: induction m with
  | zero => simp
  | succ m hm => rw [Nat.add_succ, prod_range_succ, prod_range_succ, hm, mul_assoc]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
f : ℕ → M
⊢ ∏ k ∈ range 1, f k = f 0
have rw : ∏ k ∈ {0}, f k = f 0
Tactic: rw [range_one, prod_singleton]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
f : ℕ → M
rw : ∏ k ∈ {0}, f k = f 0
⊢ ∏ k ∈ range 1, f k = f 0
have rw₁ : f 0 = f 0
Tactic: rw [range_one, prod_singleton]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
⊢ (List.map f (a :: s)).prod = ∏ m ∈ (a :: s).toFinset, f m ^ count m (a :: s)
have cons : f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)
Tactic: simp only [List.map, List.prod_cons, toFinset_cons, IH]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
⊢ f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)
have pos : ∀ (has : a ∈ s.toFinset), f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)
Tactic: by_cases has : a ∈ s.toFinset
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
pos :
  ∀ (has : a ∈ s.toFinset), f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)
⊢ f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)
have neg : ∀ (has : a ∉ s.toFinset), f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)
Tactic: by_cases has : a ∈ s.toFinset
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
⊢ f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)
have pos : f a * f a ^ count a s * ∏ x ∈ s.toFinset.erase a, f x ^ count x s =
  f a * f a ^ count a s * ∏ x ∈ s.toFinset.erase a, f x ^ count x (a :: s)
Tactic: rw [insert_eq_of_mem has, ← insert_erase has, prod_insert (notMem_erase _ _),
      prod_insert (notMem_erase _ _), ← mul_assoc, count_cons_self, pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
⊢ f a * f a ^ count a s * ∏ x ∈ s.toFinset.erase a, f x ^ count x s =
    f a * f a ^ count a s * ∏ x ∈ s.toFinset.erase a, f x ^ count x (a :: s)
have pos : Eq.{u_4 + 1} (α := M) (∏ x ∈ s.toFinset.erase a, f x ^ count x s) (∏ x ∈ s.toFinset.erase a, f x ^ count x (a :: s))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.toFinset.erase a, f x ^ count x s) (∏ x ∈ s.toFinset.erase a, f x ^ count x (a :: s))
have pos : ∀ (x : ι) (hx : x ∈ s.toFinset.erase a), f x ^ count x s = f x ^ count x (a :: s)
Tactic: refine prod_congr rfl fun x hx => ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
x : ι
hx : x ∈ s.toFinset.erase a
⊢ f x ^ count x s = f x ^ count x (a :: s)
have pos : f x ^ count x s = f x ^ count x s
Tactic: rw [count_cons_of_ne (ne_of_mem_erase hx).symm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∉ s.toFinset
⊢ f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)
have neg : f a * ∏ m ∈ s.toFinset, f m ^ count m s = f a * ∏ x ∈ s.toFinset, f x ^ count x (a :: s)
Tactic: rw [prod_insert has, count_cons_self, count_eq_zero_of_not_mem (mt mem_toFinset.2 has), pow_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
l : List ι
f : ι → M
⊢ (List.map f l).prod = ∏ m ∈ l.toFinset, f m ^ count m l
have nil : (List.map f []).prod = ∏ m ∈ toFinset [], f m ^ count m []
Tactic: induction l with
  | nil => simp only [map_nil, prod_nil, count_nil, pow_zero, prod_const_one]
  | cons a s IH =>
  simp only [List.map, List.prod_cons, toFinset_cons, IH]
  by_cases has : a ∈ s.toFinset
  · rw [insert_eq_of_mem has, ← insert_erase has, prod_insert (notMem_erase _ _),
      prod_insert (notMem_erase _ _), ← mul_assoc, count_cons_self, pow_succ']
    congr 1
    refine prod_congr rfl fun x hx => ?_
    rw [count_cons_of_ne (ne_of_mem_erase hx).symm]
  rw [prod_insert has, count_cons_self, count_eq_zero_of_not_mem (mt mem_toFinset.2 has), pow_one]
  grind [Finset.prod_congr]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
l : List ι
f : ι → M
nil : (List.map f []).prod = ∏ m ∈ toFinset [], f m ^ count m []
⊢ (List.map f l).prod = ∏ m ∈ l.toFinset, f m ^ count m l
have cons : ∀ (a : ι) (s : List ι) (IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s),
  (List.map f (a :: s)).prod = ∏ m ∈ (a :: s).toFinset, f m ^ count m (a :: s)
Tactic: induction l with
  | nil => simp only [map_nil, prod_nil, count_nil, pow_zero, prod_const_one]
  | cons a s IH =>
  simp only [List.map, List.prod_cons, toFinset_cons, IH]
  by_cases has : a ∈ s.toFinset
  · rw [insert_eq_of_mem has, ← insert_erase has, prod_insert (notMem_erase _ _),
      prod_insert (notMem_erase _ _), ← mul_assoc, count_cons_self, pow_succ']
    congr 1
    refine prod_congr rfl fun x hx => ?_
    rw [count_cons_of_ne (ne_of_mem_erase hx).symm]
  rw [prod_insert has, count_cons_self, count_eq_zero_of_not_mem (mt mem_toFinset.2 has), pow_one]
  grind [Finset.prod_congr]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq M
m : List M
s : Finset M
hs : m.toFinset ⊆ s
⊢ m.prod = ∏ i ∈ s, i ^ count i m
have rw : Eq (α := M) (∏ m_1 ∈ m.toFinset, m_1 ^ count m_1 m) (∏ i ∈ s, i ^ count i m)
Tactic: rw [prod_list_count]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq M
m : List M
s : Finset M
hs : m.toFinset ⊆ s
⊢ Eq (α := M) (∏ m_1 ∈ m.toFinset, m_1 ^ count m_1 m) (∏ i ∈ s, i ^ count i m)
have refine : ∀ x ∈ s, ∀ (hx : x ∉ m.toFinset), x ^ count x m = 1
Tactic: refine prod_subset hs fun x _ hx => ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (hypothesis)
Goal:
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq M
m : List M
s : Finset M
hs : m.toFinset ⊆ s
x : M
h : x ∈ s
hx : x ∉ m.toFinset
⊢ x ^ count x m = 1
have hx₁ : x ∉ m
Tactic: rw [mem_toFinset] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq M
m : List M
s : Finset M
hs : m.toFinset ⊆ s
x : M
h : x ∈ s
hx : x ∉ m
⊢ x ^ count x m = 1
have rw : HPow.hPow (β := ℕ) x 0 = 1
Tactic: rw [count_eq_zero_of_not_mem hx, pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq M
m : List M
s : Finset M
hs : m.toFinset ⊆ s
x : M
h : x ∈ s
hx : x ∉ m
rw : HPow.hPow (β := ℕ) x 0 = 1
⊢ x ^ count x m = 1
have rw₁ : Eq.{u_4 + 1} (α := M) 1 1
Tactic: rw [count_eq_zero_of_not_mem hx, pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Multiset ι
M : Type u_5
inst_1 : CommMonoid M
f : ι → M
⊢ (Multiset.map f s).prod = ∏ m ∈ s.toFinset, f m ^ Multiset.count m s
have refine : ∀ (l : List ι),
  (Multiset.map f (Quot.mk (⇑(isSetoid ι) : List ι → List ι → Prop) l)).prod =
    ∏ m ∈ Multiset.toFinset (Quot.mk (⇑(isSetoid ι) : List ι → List ι → Prop) l),
      f m ^ Multiset.count m (Quot.mk (⇑(isSetoid ι) : List ι → List ι → Prop) l)
Tactic: refine Quot.induction_on s fun l => ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq M
s : Multiset M
⊢ s.prod = ∏ m ∈ s.toFinset, m ^ Multiset.count m s
have h : s = Multiset.map id s
Tactic: convert! prod_multiset_map_count s id
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq M
s : Multiset M
⊢ s = Multiset.map id s
have h : s = s
Tactic: rw [Multiset.map_id]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq M
m : Multiset M
s : Finset M
hs : m.toFinset ⊆ s
⊢ m.prod = ∏ i ∈ s, i ^ Multiset.count i m
have revert : ∀ (hs : m.toFinset ⊆ s), m.prod = ∏ i ∈ s, i ^ Multiset.count i m
Tactic: revert hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq M
m : Multiset M
s : Finset M
⊢ ∀ (hs : m.toFinset ⊆ s), m.prod = ∏ i ∈ s, i ^ Multiset.count i m
have refine : ∀ (l : List M) (hs : Multiset.toFinset (Quot.mk (⇑(isSetoid M) : List M → List M → Prop) l) ⊆ s),
  Multiset.prod (Quot.mk (⇑(isSetoid M) : List M → List M → Prop) l) =
    ∏ i ∈ s, i ^ Multiset.count i (Quot.mk (⇑(isSetoid M) : List M → List M → Prop) l)
Tactic: refine Quot.induction_on m fun l => ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq M
m : Multiset M
s : Finset M
l : List M
⊢ ∀ (hs : Multiset.toFinset (Quot.mk (⇑(isSetoid M) : List M → List M → Prop) l) ⊆ s),
    Multiset.prod (Quot.mk (⇑(isSetoid M) : List M → List M → Prop) l) =
      ∏ i ∈ s, i ^ Multiset.count i (Quot.mk (⇑(isSetoid M) : List M → List M → Prop) l)
have simp : ∀ (hs : (↑l : Multiset M).toFinset ⊆ s), l.prod = ∏ x ∈ s, x ^ List.count x l
Tactic: simp only [quot_mk_to_coe'', prod_coe, coe_count]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
f s : ℕ → M
base : s 0 = 1
step : ∀ k < 0, s (k + 1) = s k * f k
⊢ ∏ k ∈ range 0, f k = s 0
have zero : 1 = s 0
Tactic: rw [Finset.prod_range_zero, base]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
f s : ℕ → M
base : s 0 = 1
step : ∀ k < 0, s (k + 1) = s k * f k
zero : 1 = s 0
⊢ ∏ k ∈ range 0, f k = s 0
have zero₁ : Eq.{u_4 + 1} (α := M) 1 1
Tactic: rw [Finset.prod_range_zero, base]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
f s : ℕ → M
base : s 0 = 1
k : ℕ
hk : ∀ (step : ∀ k_1 < k, s (k_1 + 1) = s k_1 * f k_1), ∏ k ∈ range k, f k = s k
step : ∀ k_1 < k + 1, s (k_1 + 1) = s k_1 * f k_1
⊢ ∏ k ∈ range (k + 1), f k = s (k + 1)
have succ : ∀ k_1 < k, s (k_1 + 1) = s k_1 * f k_1
Tactic: rw [Finset.prod_range_succ, step _ (Nat.lt_succ_self _), hk]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
f s : ℕ → M
base : s 0 = 1
n : ℕ
step : ∀ k < n, s (k + 1) = s k * f k
⊢ ∏ k ∈ range n, f k = s n
have zero : ∀ (step : ∀ k < 0, s (k + 1) = s k * f k), ∏ k ∈ range 0, f k = s 0
Tactic: induction n with
  | zero => rw [Finset.prod_range_zero, base]
  | succ k hk =>
    rw [Finset.prod_range_succ, step _ (Nat.lt_succ_self _), hk]
    exact fun _ hl ↦ step _ (Nat.lt_succ_of_lt hl)
Cleared hypotheses: n, step
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
f s : ℕ → M
base : s 0 = 1
n : ℕ
step : ∀ k < n, s (k + 1) = s k * f k
zero : ∀ (step : ∀ k < 0, s (k + 1) = s k * f k), ∏ k ∈ range 0, f k = s 0
⊢ ∏ k ∈ range n, f k = s n
have succ : ∀ (k : ℕ) (hk : ∀ (step : ∀ k_1 < k, s (k_1 + 1) = s k_1 * f k_1), ∏ k ∈ range k, f k = s k)
  (step : ∀ k_1 < k + 1, s (k_1 + 1) = s k_1 * f k_1), ∏ k ∈ range (k + 1), f k = s (k + 1)
Tactic: induction n with
  | zero => rw [Finset.prod_range_zero, base]
  | succ k hk =>
    rw [Finset.prod_range_succ, step _ (Nat.lt_succ_self _), hk]
    exact fun _ hl ↦ step _ (Nat.lt_succ_of_lt hl)
Cleared hypotheses: n, step
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
f : ℕ → M
⊢ Eq.{u_4 + 1} (α := M) (∏ r ∈ range (HAdd.hAdd (α := ℕ) 0 1), f (0 - r)) (∏ k ∈ range (HAdd.hAdd (α := ℕ) 0 1), f k)
have zero : f (HSub.hSub (α := ℕ) 0 0) = ∏ k ∈ range (HAdd.hAdd (α := ℕ) 0 1), f k
Tactic: rw [prod_range_one, prod_range_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
f : ℕ → M
zero : f (HSub.hSub (α := ℕ) 0 0) = ∏ k ∈ range (HAdd.hAdd (α := ℕ) 0 1), f k
⊢ Eq.{u_4 + 1} (α := M) (∏ r ∈ range (HAdd.hAdd (α := ℕ) 0 1), f (0 - r)) (∏ k ∈ range (HAdd.hAdd (α := ℕ) 0 1), f k)
have zero₁ : f (HSub.hSub (α := ℕ) 0 0) = f 0
Tactic: rw [prod_range_one, prod_range_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
f : ℕ → M
n : ℕ
ih : Eq.{u_4 + 1} (α := M) (∏ r ∈ range (n + 1), f (n - r)) (∏ k ∈ range (n + 1), f k)
⊢ Eq.{u_4 + 1} (α := M) (∏ r ∈ range (n + 1 + 1), f (n + 1 - r)) (∏ k ∈ range (n + 1 + 1), f k)
have succ : (∏ k ∈ range (n + 1), f (n + 1 - (k + 1))) * f (n + 1 - 0) = (∏ x ∈ range n.succ, f x) * f n.succ
Tactic: rw [prod_range_succ', prod_range_succ _ (Nat.succ n)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
n : ℕ
f : ℕ → M
⊢ Eq.{u_4 + 1} (α := M) (∏ r ∈ range (n + 1), f (n - r)) (∏ k ∈ range (n + 1), f k)
have zero : Eq.{u_4 + 1} (α := M) (∏ r ∈ range (HAdd.hAdd (α := ℕ) 0 1), f (0 - r)) (∏ k ∈ range (HAdd.hAdd (α := ℕ) 0 1), f k)
Tactic: induction n with
  | zero => rw [prod_range_one, prod_range_one]
  | succ n ih =>
    rw [prod_range_succ', prod_range_succ _ (Nat.succ n)]
    simp [← ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
n : ℕ
f : ℕ → M
zero :
  Eq.{u_4 + 1} (α := M) (∏ r ∈ range (HAdd.hAdd (α := ℕ) 0 1), f (0 - r)) (∏ k ∈ range (HAdd.hAdd (α := ℕ) 0 1), f k)
⊢ Eq.{u_4 + 1} (α := M) (∏ r ∈ range (n + 1), f (n - r)) (∏ k ∈ range (n + 1), f k)
have succ : ∀ (n : ℕ) (ih : Eq.{u_4 + 1} (α := M) (∏ r ∈ range (n + 1), f (n - r)) (∏ k ∈ range (n + 1), f k)),
  Eq.{u_4 + 1} (α := M) (∏ r ∈ range (n + 1 + 1), f (n + 1 - r)) (∏ k ∈ range (n + 1 + 1), f k)
Tactic: induction n with
  | zero => rw [prod_range_one, prod_range_one]
  | succ n ih =>
    rw [prod_range_succ', prod_range_succ _ (Nat.succ n)]
    simp [← ih]
Cleared hypotheses: n