awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
Goal:
ι : Type u_2
M : Type u_5
N : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
s : Multiset ι
F : Type u_8
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
g : ι → M
⊢ Eq.{u_6 + 1} (α := N) (prod (map (fun (i : ι) ↦ (f : (a : M) → N) (g i)) s) : N)
    ((f : (a : M) → N) (map g s).prod : N)
have h : Eq.{u_6 + 1} (α := Multiset N) (map (fun (i : ι) ↦ (f : (a : M) → N) (g i)) s) (map (⇑f : (a : M) → N) (map g s))
Tactic: convert! (s.map g).prod_hom f
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
Goal:
ι : Type u_2
M : Type u_5
N : Type u_6
O : Type u_7
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : CommMonoid O
s : Multiset ι
hs : s ≠ 0
f : M → N → O
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
⊢ prod (map (fun (i : ι) ↦ f (f₁ i) (f₂ i)) s) = f (map f₁ s).prod (map f₂ s).prod
have h : ∀ (a : List ι) (hs : ⟦a⟧ ≠ 0), prod (map (fun (i : ι) ↦ f (f₁ i) (f₂ i)) ⟦a⟧) = f (map f₁ ⟦a⟧).prod (map f₂ ⟦a⟧).prod
Tactic: induction s using Quotient.inductionOn
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
Goal:
M : Type u_5
inst : CommMonoid M
s t : Multiset M
h : s ≤ t
⊢ s.prod ∣ t.prod
have obtain : ∀ (z : Multiset M) (h : s ≤ s + z), s.prod ∣ (s + z).prod
Tactic: obtain ⟨z, rfl⟩ := exists_add_of_le h
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
Goal:
M : Type u_5
N : Type u_6
inst : CommMonoid N
S : Multiset M
g1 g2 : M → N
h : ∀ (a : M), a ∈ S → g1 a ∣ g2 a
⊢ (map g1 S).prod ∣ (map g2 S).prod
have h₁ : (map g1 0).prod ∣ (map g2 0).prod
Tactic: apply Multiset.induction_on' S
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
Goal:
M : Type u_5
N : Type u_6
inst : CommMonoid N
S : Multiset M
g1 g2 : M → N
h : ∀ (a : M), a ∈ S → g1 a ∣ g2 a
h₁ : (map g1 0).prod ∣ (map g2 0).prod
⊢ (map g1 S).prod ∣ (map g2 S).prod
have h₂ : ∀ {a : M} {s : Multiset M},
  a ∈ S → s ⊆ S → (map g1 s).prod ∣ (map g2 s).prod → (map g1 (insert a s)).prod ∣ (map g2 (insert a s)).prod
Tactic: apply Multiset.induction_on' S
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
Goal:
ι : Type u_2
G : Type u_4
inst : DivisionCommMonoid G
m : Multiset ι
f : ι → G
⊢ prod (map (fun (i : ι) ↦ (f i)⁻¹) m) = (map f m).prod⁻¹
have rw : prod (map (fun (i : ι) ↦ (f i)⁻¹) m) = (map Inv.inv (map f m)).prod
Tactic: rw [← (m.map f).prod_map_inv', map_map, Function.comp_def]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
Goal:
ι : Type u_2
G : Type u_4
inst : DivisionCommMonoid G
m : Multiset ι
f : ι → G
rw : prod (map (fun (i : ι) ↦ (f i)⁻¹) m) = (map Inv.inv (map f m)).prod
⊢ prod (map (fun (i : ι) ↦ (f i)⁻¹) m) = (map f m).prod⁻¹
have rw₁ : prod (map (fun (i : ι) ↦ (f i)⁻¹) m) = (map (Inv.inv ∘ f) m).prod
Tactic: rw [← (m.map f).prod_map_inv', map_map, Function.comp_def]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
Goal:
ι : Type u_2
G : Type u_4
inst : DivisionCommMonoid G
m : Multiset ι
f : ι → G
rw : prod (map (fun (i : ι) ↦ (f i)⁻¹) m) = (map Inv.inv (map f m)).prod
rw₁ : prod (map (fun (i : ι) ↦ (f i)⁻¹) m) = (map (Inv.inv ∘ f) m).prod
⊢ prod (map (fun (i : ι) ↦ (f i)⁻¹) m) = (map f m).prod⁻¹
have rw₂ : Eq.{u_4 + 1} (α := G) (prod (map (fun (i : ι) ↦ (f i)⁻¹) m)) (prod (map (fun (x : ι) ↦ (f x)⁻¹) m))
Tactic: rw [← (m.map f).prod_map_inv', map_map, Function.comp_def]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
Goal:
ι : Type u_2
G : Type u_4
inst : DivisionCommMonoid G
m : Multiset ι
f : ι → G
n : ℤ
⊢ prod (map (fun (i : ι) ↦ f i ^ n) m) = (map f m).prod ^ n
have h : Eq (α := Multiset G) (map (fun (i : ι) ↦ f i ^ n) m) (map (⇑(zpowGroupHom n) : (a : G) → G) (map f m))
Tactic: convert! (m.map f).prod_hom (zpowGroupHom n : G →* G)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
Goal:
s : Multiset ℕ
n : ℕ
⊢ s.sum % n = sum (map (fun (x : ℕ) ↦ x % n) s) % n
have empty : sum 0 % n = sum (map (fun (x : ℕ) ↦ x % n) 0) % n
Tactic: induction s using Multiset.induction
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
Goal:
s : Multiset ℕ
n : ℕ
empty : sum 0 % n = sum (map (fun (x : ℕ) ↦ x % n) 0) % n
⊢ s.sum % n = sum (map (fun (x : ℕ) ↦ x % n) s) % n
have cons : ∀ (a : ℕ) (s : Multiset ℕ),
  s.sum % n = sum (map (fun (x : ℕ) ↦ x % n) s) % n → (a ::ₘ s).sum % n = sum (map (fun (x : ℕ) ↦ x % n) (a ::ₘ s)) % n
Tactic: induction s using Multiset.induction
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
Goal:
s : Multiset ℕ
n : ℕ
⊢ s.prod % n = prod (map (fun (x : ℕ) ↦ x % n) s) % n
have empty : prod 0 % n = prod (map (fun (x : ℕ) ↦ x % n) 0) % n
Tactic: induction s using Multiset.induction
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
Goal:
s : Multiset ℕ
n : ℕ
empty : prod 0 % n = prod (map (fun (x : ℕ) ↦ x % n) 0) % n
⊢ s.prod % n = prod (map (fun (x : ℕ) ↦ x % n) s) % n
have cons : ∀ (a : ℕ) (s : Multiset ℕ),
  s.prod % n = prod (map (fun (x : ℕ) ↦ x % n) s) % n →
    (a ::ₘ s).prod % n = prod (map (fun (x : ℕ) ↦ x % n) (a ::ₘ s)) % n
Tactic: induction s using Multiset.induction
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
Goal:
s : Multiset ℤ
n : ℤ
⊢ s.sum % n = sum (map (fun (x : ℤ) ↦ x % n) s) % n
have empty : sum 0 % n = sum (map (fun (x : ℤ) ↦ x % n) 0) % n
Tactic: induction s using Multiset.induction
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
Goal:
s : Multiset ℤ
n : ℤ
empty : sum 0 % n = sum (map (fun (x : ℤ) ↦ x % n) 0) % n
⊢ s.sum % n = sum (map (fun (x : ℤ) ↦ x % n) s) % n
have cons : ∀ (a : ℤ) (s : Multiset ℤ),
  s.sum % n = sum (map (fun (x : ℤ) ↦ x % n) s) % n → (a ::ₘ s).sum % n = sum (map (fun (x : ℤ) ↦ x % n) (a ::ₘ s)) % n
Tactic: induction s using Multiset.induction
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
Goal:
s : Multiset ℤ
n : ℤ
⊢ s.prod % n = prod (map (fun (x : ℤ) ↦ x % n) s) % n
have empty : prod 0 % n = prod (map (fun (x : ℤ) ↦ x % n) 0) % n
Tactic: induction s using Multiset.induction
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
Goal:
s : Multiset ℤ
n : ℤ
empty : prod 0 % n = prod (map (fun (x : ℤ) ↦ x % n) 0) % n
⊢ s.prod % n = prod (map (fun (x : ℤ) ↦ x % n) s) % n
have cons : ∀ (a : ℤ) (s : Multiset ℤ),
  s.prod % n = prod (map (fun (x : ℤ) ↦ x % n) s) % n →
    (a ::ₘ s).prod % n = prod (map (fun (x : ℤ) ↦ x % n) (a ::ₘ s)) % n
Tactic: induction s using Multiset.induction
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
Goal:
ι : Type u_2
M : Type u_5
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : ExistsAddOfLE M
inst_3 : AddLeftMono M
inst_4 : AddLeftReflectLE M
inst_5 : Sub M
inst_6 : OrderedSub M
l : Multiset ι
f g : ι → M
hfg : ∀ (x : ι), x ∈ l → g x ≤ f x
⊢ sum (map (fun (x : ι) ↦ f x - g x) l) + (map g l).sum = (map f l).sum
have rw : sum (map (fun (i : ι) ↦ f i - g i + g i) l) = (map f l).sum
Tactic: rw [← sum_map_add]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
Goal:
ι : Type u_2
M : Type u_5
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : ExistsAddOfLE M
inst_3 : AddLeftMono M
inst_4 : AddLeftReflectLE M
inst_5 : Sub M
inst_6 : OrderedSub M
l : Multiset ι
f g : ι → M
hfg : ∀ (x : ι), x ∈ l → g x ≤ f x
⊢ sum (map (fun (i : ι) ↦ f i - g i + g i) l) = (map f l).sum
have e_a : map (fun (i : ι) ↦ f i - g i + g i) l = map f l
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Defs (goal)
Goal:
M : Type u_3
inst : CommMonoid M
s : Multiset M
| s.prod
have rw : (↑s.toList : Multiset M).prod
Tactic: rw [← coe_toList s]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Defs (goal)
Goal:
M : Type u_3
inst : CommMonoid M
s : Multiset M
⊢ s.toList.prod = s.prod
have conv_rhs : s.toList.prod = (↑s.toList : Multiset M).prod
Tactic: conv_rhs => rw [← coe_toList s]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Defs (goal)
Goal:
M : Type u_3
inst : CommMonoid M
s : Multiset M
⊢ s.toList.prod = (↑s.toList : Multiset M).prod
have rw : s.toList.prod = s.toList.prod
Tactic: rw [prod_coe]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Defs (goal)
Goal:
ι : Type u_2
M : Type u_3
inst : CommMonoid M
s : Multiset ι
f : ι → M
⊢ (List.map f s.toList).prod = (map f s).prod
have rw : (↑(List.map f s.toList) : Multiset M).prod = (map f s).prod
Tactic: rw [← Multiset.prod_coe, ← Multiset.map_coe, coe_toList]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Defs (goal)
Goal:
ι : Type u_2
M : Type u_3
inst : CommMonoid M
s : Multiset ι
f : ι → M
rw : (↑(List.map f s.toList) : Multiset M).prod = (map f s).prod
⊢ (List.map f s.toList).prod = (map f s).prod
have rw₁ : (map f (↑s.toList : Multiset ι)).prod = (map f s).prod
Tactic: rw [← Multiset.prod_coe, ← Multiset.map_coe, coe_toList]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Defs (goal)
Goal:
ι : Type u_2
M : Type u_3
inst : CommMonoid M
s : Multiset ι
f : ι → M
rw : (↑(List.map f s.toList) : Multiset M).prod = (map f s).prod
rw₁ : (map f (↑s.toList : Multiset ι)).prod = (map f s).prod
⊢ (List.map f s.toList).prod = (map f s).prod
have rw₂ : (map f s).prod = (map f s).prod
Tactic: rw [← Multiset.prod_coe, ← Multiset.map_coe, coe_toList]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Defs (goal)
Goal:
M : Type u_3
inst : CommMonoid M
a b : M
⊢ prod {a, b} = a * b
have rw : (a ::ₘ {b}).prod = a * b
Tactic: rw [insert_eq_cons, prod_cons, prod_singleton]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Defs (goal)
Goal:
M : Type u_3
inst : CommMonoid M
a b : M
rw : (a ::ₘ {b}).prod = a * b
⊢ prod {a, b} = a * b
have rw₁ : a * prod {b} = a * b
Tactic: rw [insert_eq_cons, prod_cons, prod_singleton]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Defs (goal)
Goal:
M : Type u_3
inst : CommMonoid M
a b : M
rw : (a ::ₘ {b}).prod = a * b
rw₁ : a * prod {b} = a * b
⊢ prod {a, b} = a * b
have rw₂ : a * b = a * b
Tactic: rw [insert_eq_cons, prod_cons, prod_singleton]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Defs (goal)
Goal:
M : Type u_3
inst : CommMonoid M
s : Multiset M
inst_1 : DecidableEq M
a : M
⊢ a ^ count a s = (filter (Eq a) s).prod
have rw : a ^ count a s = (replicate (count a s) a).prod
Tactic: rw [filter_eq, prod_replicate]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Defs (goal)
Goal:
M : Type u_3
inst : CommMonoid M
s : Multiset M
inst_1 : DecidableEq M
a : M
rw : a ^ count a s = (replicate (count a s) a).prod
⊢ a ^ count a s = (filter (Eq a) s).prod
have rw₁ : a ^ count a s = a ^ count a s
Tactic: rw [filter_eq, prod_replicate]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Defs (goal)
Goal:
ι : Type u_2
M : Type u_3
inst : CommMonoid M
m : Multiset ι
⊢ Eq.{u_3 + 1} (α := M) (prod (map (fun (x : ι) ↦ 1) m)) 1
have rw : Eq.{u_3 + 1} (α := M) (prod (replicate m.card 1)) 1
Tactic: rw [map_const', prod_replicate, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Defs (goal)
Goal:
ι : Type u_2
M : Type u_3
inst : CommMonoid M
m : Multiset ι
rw : Eq.{u_3 + 1} (α := M) (prod (replicate m.card 1)) 1
⊢ Eq.{u_3 + 1} (α := M) (prod (map (fun (x : ι) ↦ 1) m)) 1
have rw₁ : HPow.hPow (α := M) 1 m.card = 1
Tactic: rw [map_const', prod_replicate, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Defs (goal)
Goal:
ι : Type u_2
M : Type u_3
inst : CommMonoid M
m : Multiset ι
rw : Eq.{u_3 + 1} (α := M) (prod (replicate m.card 1)) 1
rw₁ : HPow.hPow (α := M) 1 m.card = 1
⊢ Eq.{u_3 + 1} (α := M) (prod (map (fun (x : ι) ↦ 1) m)) 1
have rw₂ : Eq.{u_3 + 1} (α := M) 1 1
Tactic: rw [map_const', prod_replicate, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Defs (goal)
Goal:
M : Type u_3
inst : CommMonoid M
p : M → Prop
s : Multiset M
p_mul : ∀ (a b : M), p a → p b → p (a * b)
p_one : p 1
p_s : ∀ (a : M), a ∈ s → p a
⊢ p s.prod
have rw : p (foldr (fun (x1 x2 : M) ↦ x1 * x2) 1 s)
Tactic: rw [prod_eq_foldr]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Defs (goal)
Goal:
M : Type u_3
inst : CommMonoid M
s_1 : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
a : M
s : Multiset M
hsa : ∀ (hs : s ≠ ∅) (p_s : ∀ (a : M), a ∈ s → p a), p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1
⊢ p (a ::ₘ s).prod
have cons : p (a * s.prod)
Tactic: rw [prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Defs (goal)
Goal:
M : Type u_3
inst : CommMonoid M
s_1 : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
a : M
s : Multiset M
hsa : ∀ (hs : s ≠ ∅) (p_s : ∀ (a : M), a ∈ s → p a), p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1
⊢ p (a * s.prod)
have pos : ∀ (hs_empty : s = ∅), p (a * s.prod)
Tactic: by_cases hs_empty : s = ∅
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Defs (goal)
Goal:
M : Type u_3
inst : CommMonoid M
s_1 : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
a : M
s : Multiset M
hsa : ∀ (hs : s ≠ ∅) (p_s : ∀ (a : M), a ∈ s → p a), p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1
pos : ∀ (hs_empty : s = ∅), p (a * s.prod)
⊢ p (a * s.prod)
have neg : ∀ (hs_empty : ¬s = ∅), p (a * s.prod)
Tactic: by_cases hs_empty : s = ∅
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Defs (goal)
Goal:
M : Type u_3
inst : CommMonoid M
s_1 : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
a : M
s : Multiset M
hsa : ∀ (hs : s ≠ ∅) (p_s : ∀ (a : M), a ∈ s → p a), p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1
hs_empty : ¬s = ∅
⊢ p (a * s.prod)
have neg : ∀ (hps : ∀ (x : M), x ∈ s → p x), p (a * s.prod)
Tactic: have hps : ∀ x, x ∈ s → p x := fun x hxs => p_s x (mem_cons_of_mem hxs)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Defs (goal)
Goal:
M : Type u_3
inst : CommMonoid M
s : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
hs : s ≠ ∅
p_s : ∀ (a : M), a ∈ s → p a
⊢ p s.prod
have empty : ∀ (hs : Ne.{u_3 + 1} (α := Multiset M) 0 ∅) (p_s : ∀ (a : M), Membership.mem (γ := Multiset M) 0 a → p a), p (prod 0)
Tactic: induction s using Multiset.induction_on with
  | empty => simp at hs
  | cons a s hsa =>
    rw [prod_cons]
    by_cases hs_empty : s = ∅
    · simp [hs_empty, p_s a]
    have hps : ∀ x, x ∈ s → p x := fun x hxs => p_s x (mem_cons_of_mem hxs)
    exact p_mul a s.prod (p_s a (mem_cons_self a s)) (hsa hs_empty hps)
Cleared hypotheses: hs, p_s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Defs (goal)
Goal:
M : Type u_3
inst : CommMonoid M
s : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
hs : s ≠ ∅
p_s : ∀ (a : M), a ∈ s → p a
empty :
  ∀ (hs : Ne.{u_3 + 1} (α := Multiset M) 0 ∅) (p_s : ∀ (a : M), Membership.mem (γ := Multiset M) 0 a → p a), p (prod 0)
⊢ p s.prod
have cons : ∀ (a : M) (s : Multiset M) (hsa : ∀ (hs : s ≠ ∅) (p_s : ∀ (a : M), a ∈ s → p a), p s.prod) (hs : a ::ₘ s ≠ ∅)
  (p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1), p (a ::ₘ s).prod
Tactic: induction s using Multiset.induction_on with
  | empty => simp at hs
  | cons a s hsa =>
    rw [prod_cons]
    by_cases hs_empty : s = ∅
    · simp [hs_empty, p_s a]
    have hps : ∀ x, x ∈ s → p x := fun x hxs => p_s x (mem_cons_of_mem hxs)
    exact p_mul a s.prod (p_s a (mem_cons_self a s)) (hsa hs_empty hps)
Cleared hypotheses: hs, p_s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Action (goal)
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : CommMonoid N
inst_2 : MulDistribMulAction M N
ι : Sort u_4
inst_3 : Finite ι
f : ι → N
r : M
⊢ HSMul.hSMul (β := N) r (∏ᶠ (x : ι), f x) = ∏ᶠ (x : ι), r • f x
have intro : ∀ (val : Fintype (PLift ι)), HSMul.hSMul (β := N) r (∏ᶠ (x : ι), f x) = ∏ᶠ (x : ι), r • f x
Tactic: cases nonempty_fintype (PLift ι)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Action (goal)
Goal:
N : Type u_2
inst : CommMonoid N
G : Type u_4
inst_1 : Group G
inst_2 : MulDistribMulAction G N
inst_3 : Fintype G
b : N
g : G
⊢ HSMul.hSMul (β := N) g (∏ h : G, h • b) = ∏ h : G, h • b
have simp : Eq.{u_2 + 1} (α := N) (∏ x : G, (g * x) • b) (∏ h : G, h • b)
Tactic: simp only [smul_prod', smul_smul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Action (goal)
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
⊢ HSMul.hSMul (β := N) g (∏ᶠ (h : G), h • b) = ∏ᶠ (h : G), h • b
have intro : ∀ (val : Fintype G), HSMul.hSMul (β := N) g (∏ᶠ (h : G), h • b) = ∏ᶠ (h : G), h • b
Tactic: cases nonempty_fintype G
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Action (goal)
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
⊢ m ^ l.length • l.prod = prod (map (fun (x : N) ↦ m • x) l)
have nil : HSMul.hSMul (β := N) (m ^ length.{u_2} (α := N) []) (prod []) = prod (map (fun (x : N) ↦ m • x) [])
Tactic: induction l with
  | nil => simp
  | cons head tail ih => simp [← ih, smul_mul_smul_comm, pow_succ']
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Action (goal)
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) [])
⊢ m ^ l.length • l.prod = prod (map (fun (x : N) ↦ m • x) l)
have 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))
Tactic: induction l with
  | nil => simp
  | cons head tail ih => simp [← ih, smul_mul_smul_comm, pow_succ']
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.GroupWithZero.Action (hypothesis)
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
⊢ HSMul.hSMul (β := N) (b ^ #s) (∏ x ∈ s, f x) = ∏ x ∈ s, b • f x
have 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))
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]
-- 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 : 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))
⊢ HSMul.hSMul (β := N) (b ^ #s) (∏ x ∈ s, f x) = ∏ x ∈ s, b • f x
have simp_rw : b ^ #s • (Multiset.map f s.val).prod = Multiset.prod (Multiset.map (fun (x : ι) ↦ b • f x) s.val)
Tactic: simp_rw [prod_eq_multiset_prod, card_def, this, ← Multiset.smul_prod _ b, Multiset.card_map]
-- 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 : 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)
⊢ HSMul.hSMul (β := N) (b ^ #s) (∏ x ∈ s, f x) = ∏ x ∈ s, b • f x
have simp_rw₁ : b ^ s.val.card • (Multiset.map f s.val).prod = Multiset.prod (Multiset.map (fun (x : ι) ↦ b • f x) s.val)
Tactic: simp_rw [prod_eq_multiset_prod, card_def, this, ← Multiset.smul_prod _ b, Multiset.card_map]
-- 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 : 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)
⊢ HSMul.hSMul (β := N) (b ^ #s) (∏ x ∈ s, f x) = ∏ x ∈ s, b • f x
have 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))
Tactic: simp_rw [prod_eq_multiset_prod, card_def, this, ← Multiset.smul_prod _ b, Multiset.card_map]
-- 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 : 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))
⊢ HSMul.hSMul (β := N) (b ^ #s) (∏ x ∈ s, f x) = ∏ x ∈ s, b • f x
have 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
Tactic: simp_rw [prod_eq_multiset_prod, card_def, this, ← Multiset.smul_prod _ b, Multiset.card_map]
-- 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)
⊢ ∏ 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)
have cons : b a • f a * ∏ x ∈ s, b x • f x =
  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: rw [prod_cons, ih, smul_mul_smul_comm, ← prod_cons hj, ← prod_cons hj]