awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
α : Type u_5
inst : CommMonoid M
m : Multiset ι
s : Finset α
f : ι → α → M
empty :
  Eq.{u_4 + 1} (α := M) (prod (map (fun (i : ι) ↦ ∏ a ∈ ∅, f i a) m)) (∏ a ∈ ∅, prod (map (fun (i : ι) ↦ f i a) m))
⊢ Eq.{u_4 + 1} (α := M) (prod (map (fun (i : ι) ↦ ∏ a ∈ s, f i a) m)) (∏ a ∈ s, prod (map (fun (i : ι) ↦ f i a) m))
have insert : ∀ (a : α) (s : Finset α) (ha : a ∉ s)
  (ih :
    Eq.{u_4 + 1} (α := M) (prod (map (fun (i : ι) ↦ ∏ a ∈ s, f i a) m)) (∏ a ∈ s, prod (map (fun (i : ι) ↦ f i a) m))),
  Eq.{u_4 + 1} (α := M) (prod (map (fun (i : ι) ↦ ∏ a ∈ insert a s, f i a) m))
    (∏ a ∈ insert a s, prod (map (fun (i : ι) ↦ f i a) m))
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih => simp [Finset.prod_insert ha, prod_map_mul, ih]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
α : Type u_5
inst : CommMonoid M
m : Multiset ι
s : Finset α
f : ι → α → M
⊢ Eq.{u_4 + 1} (α := M) (prod (map (fun (i : ι) ↦ ∏ a ∈ s, f i a) m)) (∏ a ∈ s, prod (map (fun (i : ι) ↦ f i a) m))
have empty : Eq.{u_4 + 1} (α := M) (prod (map (fun (i : ι) ↦ ∏ a ∈ ∅, f i a) m)) (∏ a ∈ ∅, prod (map (fun (i : ι) ↦ f i a) m))
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih => simp [Finset.prod_insert ha, prod_map_mul, ih]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
α : Type u_5
inst : CommMonoid M
m : Multiset ι
s : Finset α
f : ι → α → M
empty :
  Eq.{u_4 + 1} (α := M) (prod (map (fun (i : ι) ↦ ∏ a ∈ ∅, f i a) m)) (∏ a ∈ ∅, prod (map (fun (i : ι) ↦ f i a) m))
⊢ Eq.{u_4 + 1} (α := M) (prod (map (fun (i : ι) ↦ ∏ a ∈ s, f i a) m)) (∏ a ∈ s, prod (map (fun (i : ι) ↦ f i a) m))
have insert : ∀ (a : α) (s : Finset α) (ha : a ∉ s)
  (ih :
    Eq.{u_4 + 1} (α := M) (prod (map (fun (i : ι) ↦ ∏ a ∈ s, f i a) m)) (∏ a ∈ s, prod (map (fun (i : ι) ↦ f i a) m))),
  Eq.{u_4 + 1} (α := M) (prod (map (fun (i : ι) ↦ ∏ a ∈ insert a s, f i a) m))
    (∏ a ∈ insert a s, prod (map (fun (i : ι) ↦ f i a) m))
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih => simp [Finset.prod_insert ha, prod_map_mul, ih]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
m : Multiset ι
hms : ∀ a ∈ m, a ∈ s
⊢ ∑ a ∈ s, count a m = m.card
have rw : Eq (α := ℕ) (∑ x ∈ s with count x m ≠ 0, count x m) (∑ a ∈ m.toFinset, count a m)
Tactic: rw [← toFinset_sum_count_eq, ← Finset.sum_filter_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
m : Multiset ι
hms : ∀ a ∈ m, a ∈ s
⊢ Eq (α := ℕ) (∑ x ∈ s with count x m ≠ 0, count x m) (∑ a ∈ m.toFinset, count a m)
have e_s : ∀ (a : ι), a ∈ {x ∈ s | count x m ≠ 0} ↔ a ∈ m.toFinset
Tactic: congr with a
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Multiset ι
⊢ ∑ a ∈ s.toFinset, HSMul.hSMul (β := Multiset ι) (count a s) {a} = s
have rw : sum (map singleton s) = s
Tactic: rw [← Finset.sum_multiset_map_count, Multiset.sum_map_singleton]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Multiset ι
rw : sum (map singleton s) = s
⊢ ∑ a ∈ s.toFinset, HSMul.hSMul (β := Multiset ι) (count a s) {a} = s
have rw₁ : s = s
Tactic: rw [← Finset.sum_multiset_map_count, Multiset.sum_map_singleton]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
⊢ ∃ (u : Multiset ι), s = k • u
have h₁ : s = HSMul.hSMul (β := Multiset ι) k (∑ a ∈ s.toFinset, HSMul.hSMul (β := Multiset ι) (count a s / k) {a})
Tactic: use ∑ a ∈ s.toFinset, (s.count a / k) • {a}
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
⊢ Eq (α := Multiset ι) (∑ x ∈ s.toFinset, k • HSMul.hSMul (β := Multiset ι) (count x s / k) {x})
    (∑ x ∈ s.toFinset, HSMul.hSMul (β := Multiset ι) (count x s) {x})
have apply : ∀ x ∈ s.toFinset, k • HSMul.hSMul (β := Multiset ι) (count x s / k) {x} = HSMul.hSMul (β := Multiset ι) (count x s) {x}
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
x : ι
hx : x ∈ s.toFinset
⊢ k • HSMul.hSMul (β := Multiset ι) (count x s / k) {x} = HSMul.hSMul (β := Multiset ι) (count x s) {x}
have rw : HSMul.hSMul (β := Multiset ι) (k * (count x s / k)) {x} = HSMul.hSMul (β := Multiset ι) (count x s) {x}
Tactic: rw [← mul_nsmul', Nat.mul_div_cancel' (h x (mem_toFinset.mp hx))]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
x : ι
hx : x ∈ s.toFinset
rw : HSMul.hSMul (β := Multiset ι) (k * (count x s / k)) {x} = HSMul.hSMul (β := Multiset ι) (count x s) {x}
⊢ k • HSMul.hSMul (β := Multiset ι) (count x s / k) {x} = HSMul.hSMul (β := Multiset ι) (count x s) {x}
have rw₁ : HSMul.hSMul (β := Multiset ι) (count x s) {x} = HSMul.hSMul (β := Multiset ι) (count x s) {x}
Tactic: rw [← mul_nsmul', Nat.mul_div_cancel' (h x (mem_toFinset.mp hx))]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (hypothesis)
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
⊢ s = HSMul.hSMul (β := Multiset ι) k (∑ a ∈ s.toFinset, HSMul.hSMul (β := Multiset ι) (count a s / k) {a})
have h₂ : Eq (α := Multiset ι) (∑ x ∈ s.toFinset, k • HSMul.hSMul (β := Multiset ι) (count x s / k) {x})
  (∑ x ∈ s.toFinset, HSMul.hSMul (β := Multiset ι) (count x s) {x})
Tactic: have h₂ :
    (∑ x ∈ s.toFinset, k • (count x s / k) • ({x} : Multiset ι)) =
      ∑ x ∈ s.toFinset, count x s • {x} := by
    apply Finset.sum_congr rfl
    intro x hx
    rw [← mul_nsmul', Nat.mul_div_cancel' (h x (mem_toFinset.mp hx))]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
h₂ :
  Eq (α := Multiset ι) (∑ x ∈ s.toFinset, k • HSMul.hSMul (β := Multiset ι) (count x s / k) {x})
    (∑ x ∈ s.toFinset, HSMul.hSMul (β := Multiset ι) (count x s) {x})
⊢ s = HSMul.hSMul (β := Multiset ι) k (∑ a ∈ s.toFinset, HSMul.hSMul (β := Multiset ι) (count a s / k) {a})
have h₁ : s = ∑ x ∈ s.toFinset, k • HSMul.hSMul (β := Multiset ι) (count x s / k) {x}
Tactic: rw [← Finset.sum_nsmul, h₂, toFinset_sum_count_nsmul_eq]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
h₂ :
  Eq (α := Multiset ι) (∑ x ∈ s.toFinset, k • HSMul.hSMul (β := Multiset ι) (count x s / k) {x})
    (∑ x ∈ s.toFinset, HSMul.hSMul (β := Multiset ι) (count x s) {x})
h₁ : s = ∑ x ∈ s.toFinset, k • HSMul.hSMul (β := Multiset ι) (count x s / k) {x}
⊢ s = HSMul.hSMul (β := Multiset ι) k (∑ a ∈ s.toFinset, HSMul.hSMul (β := Multiset ι) (count a s / k) {a})
have h₃ : s = ∑ x ∈ s.toFinset, HSMul.hSMul (β := Multiset ι) (count x s) {x}
Tactic: rw [← Finset.sum_nsmul, h₂, toFinset_sum_count_nsmul_eq]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
h₂ :
  Eq (α := Multiset ι) (∑ x ∈ s.toFinset, k • HSMul.hSMul (β := Multiset ι) (count x s / k) {x})
    (∑ x ∈ s.toFinset, HSMul.hSMul (β := Multiset ι) (count x s) {x})
h₁ : s = ∑ x ∈ s.toFinset, k • HSMul.hSMul (β := Multiset ι) (count x s / k) {x}
h₃ : s = ∑ x ∈ s.toFinset, HSMul.hSMul (β := Multiset ι) (count x s) {x}
⊢ s = HSMul.hSMul (β := Multiset ι) k (∑ a ∈ s.toFinset, HSMul.hSMul (β := Multiset ι) (count a s / k) {a})
have h₄ : s = s
Tactic: rw [← Finset.sum_nsmul, h₂, toFinset_sum_count_nsmul_eq]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
ι : Type u_5
inst : CommMonoid M
f : ι → Multiset M
s : Finset ι
⊢ Eq.{u_4 + 1} (α := M) (prod (∑ x ∈ s, f x)) (∏ x ∈ s, (f x).prod)
have empty : Eq.{u_4 + 1} (α := M) (prod (∑ x ∈ ∅, f x)) (∏ x ∈ ∅, (f x).prod)
Tactic: induction s using Finset.cons_induction with grind
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
ι : Type u_5
inst : CommMonoid M
f : ι → Multiset M
s : Finset ι
empty : Eq.{u_4 + 1} (α := M) (prod (∑ x ∈ ∅, f x)) (∏ x ∈ ∅, (f x).prod)
⊢ Eq.{u_4 + 1} (α := M) (prod (∑ x ∈ s, f x)) (∏ x ∈ s, (f x).prod)
have cons : ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
  Eq.{u_4 + 1} (α := M) (prod (∑ x ∈ s, f x)) (∏ x ∈ s, (f x).prod) →
    Eq.{u_4 + 1} (α := M) (prod (∑ x ∈ Finset.cons a s h, f x)) (∏ x ∈ Finset.cons a s h, (f x).prod)
Tactic: induction s using Finset.cons_induction with grind
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
⊢ IsUnit.{u_4} (M := M) (∏ a ∈ s, f a) ↔ ∀ a ∈ s, IsUnit (f a)
have empty : IsUnit.{u_4} (M := M) (∏ a ∈ ∅, f a) ↔ ∀ (a : ι), Membership.mem (γ := Finset ι) ∅ a → IsUnit (f a)
Tactic: induction s using Finset.cons_induction with grind
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
empty : IsUnit.{u_4} (M := M) (∏ a ∈ ∅, f a) ↔ ∀ (a : ι), Membership.mem (γ := Finset ι) ∅ a → IsUnit (f a)
⊢ IsUnit.{u_4} (M := M) (∏ a ∈ s, f a) ↔ ∀ a ∈ s, IsUnit (f a)
have cons : ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
  (IsUnit.{u_4} (M := M) (∏ a ∈ s, f a) ↔ ∀ a ∈ s, IsUnit (f a)) →
    (IsUnit.{u_4} (M := M) (∏ a ∈ Finset.cons a s h, f a) ↔ ∀ a_2 ∈ Finset.cons a s h, IsUnit (f a_2))
Tactic: induction s using Finset.cons_induction with grind
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℤ
⊢ natAbs (∑ i ∈ s, f i) ≤ ∑ i ∈ s, (f i).natAbs
have empty : natAbs (∑ i ∈ ∅, f i) ≤ ∑ i ∈ ∅, (f i).natAbs
Tactic: induction s using Finset.cons_induction with grind
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℤ
empty : natAbs (∑ i ∈ ∅, f i) ≤ ∑ i ∈ ∅, (f i).natAbs
⊢ natAbs (∑ i ∈ s, f i) ≤ ∑ i ∈ s, (f i).natAbs
have cons : ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
  natAbs (∑ i ∈ s, f i) ≤ ∑ i ∈ s, (f i).natAbs →
    natAbs (∑ i ∈ Finset.cons a s h, f i) ≤ ∑ i ∈ Finset.cons a s h, (f i).natAbs
Tactic: induction s using Finset.cons_induction with grind
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
M : Type u_3
inst : CommMonoid M
s : Finset M
⊢ s.val.prod = s.prod id
have rw : s.val.prod = (Multiset.map id s.val).prod
Tactic: rw [Finset.prod, Multiset.map_id]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
M : Type u_3
inst : CommMonoid M
s : Finset M
rw : s.val.prod = (Multiset.map id s.val).prod
⊢ s.val.prod = s.prod id
have rw₁ : s.val.prod = s.val.prod
Tactic: rw [Finset.prod, Multiset.map_id]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : CommMonoid M
inst_1 : CommMonoid N
G : Type u_7
inst_2 : FunLike G M N
inst_3 : MonoidHomClass G M N
g : G
f : ι → M
s : Finset ι
⊢ Eq.{u_4 + 1} (α := N) ((g : (a : M) → N) (∏ x ∈ s, f x) : N) (∏ x ∈ s, (g : (a : M) → N) (f x) : N)
have simp : Eq.{u_4 + 1} (α := N) (Multiset.prod (Multiset.map ((⇑g : (a : M) → N) ∘ f) s.val))
  (Multiset.prod (Multiset.map (fun (x : ι) ↦ (g : (a : M) → N) (f x)) s.val))
Tactic: simp only [Finset.prod_eq_multiset_prod, map_multiset_prod, Multiset.map_map]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
M : Type u_3
f : ι → M
inst : CommMonoid M
inst_1 : IsEmpty ι
s : Finset ι
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, f i) 1
have rw : Eq.{u_3 + 1} (α := M) (∏ i ∈ ∅, f i) 1
Tactic: rw [eq_empty_of_isEmpty s, prod_empty]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
M : Type u_3
f : ι → M
inst : CommMonoid M
inst_1 : IsEmpty ι
s : Finset ι
rw : Eq.{u_3 + 1} (α := M) (∏ i ∈ ∅, f i) 1
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, f i) 1
have rw₁ : Eq.{u_3 + 1} (α := M) 1 1
Tactic: rw [eq_empty_of_isEmpty s, prod_empty]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
e : ι ↪ κ
f : κ → M
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ map e s, f x) (∏ x ∈ s, f ((e : (a : ι) → κ) x))
have rw : Eq.{u_3 + 1} (α := M) (Multiset.prod (Multiset.map ((fun (x : κ) ↦ f x) ∘ (⇑e : (a : ι) → κ)) s.val))
  (∏ x ∈ s, f ((e : (a : ι) → κ) x))
Tactic: rw [Finset.prod, Finset.map_val, Multiset.map_map]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
e : ι ↪ κ
⊢ Eq (α := (f : κ → M) → M) (map e s).prod fun (f : κ → M) ↦ ∏ x ∈ s, f ((e : (a : ι) → κ) x)
have h : ∀ (f : κ → M), (map e s).prod f = ∏ x ∈ s, f ((e : (a : ι) → κ) x)
Tactic: funext f
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → M
⊢ (List.map f s.toList).prod = s.prod f
have rw : (List.map f s.toList).prod = (Multiset.map f s.val).prod
Tactic: rw [Finset.prod, ← Multiset.prod_coe, ← Multiset.map_coe, Finset.coe_toList]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → M
rw : (List.map f s.toList).prod = (Multiset.map f s.val).prod
⊢ (List.map f s.toList).prod = s.prod f
have rw₁ : (↑(List.map f s.toList) : Multiset M).prod = (Multiset.map f s.val).prod
Tactic: rw [Finset.prod, ← Multiset.prod_coe, ← Multiset.map_coe, Finset.coe_toList]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → M
rw : (List.map f s.toList).prod = (Multiset.map f s.val).prod
rw₁ : (↑(List.map f s.toList) : Multiset M).prod = (Multiset.map f s.val).prod
⊢ (List.map f s.toList).prod = s.prod f
have rw₂ : (Multiset.map f (↑s.toList : Multiset ι)).prod = (Multiset.map f s.val).prod
Tactic: rw [Finset.prod, ← Multiset.prod_coe, ← Multiset.map_coe, Finset.coe_toList]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → M
rw : (List.map f s.toList).prod = (Multiset.map f s.val).prod
rw₁ : (↑(List.map f s.toList) : Multiset M).prod = (Multiset.map f s.val).prod
rw₂ : (Multiset.map f (↑s.toList : Multiset ι)).prod = (Multiset.map f s.val).prod
⊢ (List.map f s.toList).prod = s.prod f
have rw₃ : (Multiset.map f s.val).prod = (Multiset.map f s.val).prod
Tactic: rw [Finset.prod, ← Multiset.prod_coe, ← Multiset.map_coe, Finset.coe_toList]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
σ : Equiv.Perm ι
s : Finset ι
f : ι → M
hs : {a : ι | (σ : (a : ι) → ι) a ≠ a} ⊆ (↑s : Set ι)
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, f ((σ : (a : ι) → ι) x)) (∏ x ∈ s, f x)
have h : s = map (Equiv.toEmbedding σ) s
Tactic: convert! (prod_map s σ.toEmbedding f).symm
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
σ : Equiv.Perm ι
s : Finset ι
f : ι → ι → M
hs : {a : ι | (σ : (a : ι) → ι) a ≠ a} ⊆ (↑s : Set ι)
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, f ((σ : (a : ι) → ι) x) x) (∏ x ∈ s, f x ((Equiv.symm σ : (a : ι) → ι) x))
have h : ∀ (x : ι), x = (Equiv.symm σ : (a : ι) → ι) ((σ : (a : ι) → ι) x : ι)
Tactic: convert! σ.prod_comp s (fun x => f x (σ.symm x)) hs
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
σ : Equiv.Perm ι
s : Finset ι
f : ι → ι → M
hs : {a : ι | (σ : (a : ι) → ι) a ≠ a} ⊆ (↑s : Set ι)
x : ι
⊢ x = (Equiv.symm σ : (a : ι) → ι) ((σ : (a : ι) → ι) x : ι)
have h : x = x
Tactic: rw [Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → κ
j : (a : κ) → a ∈ t → ι
hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a
h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ t, g x)
have refine : ∀ (a1 : ι) (h1 : a1 ∈ s) (a2 : ι) (h2 : a2 ∈ s) (eq : i a1 h1 = i a2 h2), a1 = a2
Tactic: refine prod_bij i hi (fun a1 h1 a2 h2 eq ↦ ?_) (fun b hb ↦ ⟨_, hj b hb, right_inv b hb⟩) h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → κ
j : (a : κ) → a ∈ t → ι
hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a
h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)
a1 : ι
h1 : a1 ∈ s
a2 : ι
h2 : a2 ∈ s
eq : i a1 h1 = i a2 h2
⊢ a1 = a2
have rw : j (i a1 h1) sorry = j (i a2 h2) sorry
Tactic: rw [← left_inv a1 h1, ← left_inv a2 h2]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι ≃ κ
hst : ∀ (i : ι), i ∈ s ↔ Membership.mem (α := κ) t ((e : (a : ι) → κ) i : κ)
hfg : ∀ i ∈ s, f i = g ((e : (a : ι) → κ) i)
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, f i) (∏ i ∈ t, g i)
have refine_1 : ∀ a ∈ s, Membership.mem (α := κ) t ((e : (a : ι) → κ) a : κ)
Tactic: refine prod_nbij' e e.symm ?_ ?_ ?_ ?_ hfg
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι ≃ κ
hst : ∀ (i : ι), i ∈ s ↔ Membership.mem (α := κ) t ((e : (a : ι) → κ) i : κ)
hfg : ∀ i ∈ s, f i = g ((e : (a : ι) → κ) i)
refine_1 : ∀ a ∈ s, Membership.mem (α := κ) t ((e : (a : ι) → κ) a : κ)
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, f i) (∏ i ∈ t, g i)
have refine_2 : ∀ a ∈ t, Membership.mem (α := ι) s ((e.symm : (a : κ) → ι) a : ι)
Tactic: refine prod_nbij' e e.symm ?_ ?_ ?_ ?_ hfg
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι ≃ κ
hst : ∀ (i : ι), i ∈ s ↔ Membership.mem (α := κ) t ((e : (a : ι) → κ) i : κ)
hfg : ∀ i ∈ s, f i = g ((e : (a : ι) → κ) i)
refine_1 : ∀ a ∈ s, Membership.mem (α := κ) t ((e : (a : ι) → κ) a : κ)
refine_2 : ∀ a ∈ t, Membership.mem (α := ι) s ((e.symm : (a : κ) → ι) a : ι)
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, f i) (∏ i ∈ t, g i)
have refine_3 : ∀ a ∈ s, (e.symm : (a : κ) → ι) ((e : (a : ι) → κ) a : κ) = a
Tactic: refine prod_nbij' e e.symm ?_ ?_ ?_ ?_ hfg
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι ≃ κ
hst : ∀ (i : ι), i ∈ s ↔ Membership.mem (α := κ) t ((e : (a : ι) → κ) i : κ)
hfg : ∀ i ∈ s, f i = g ((e : (a : ι) → κ) i)
refine_1 : ∀ a ∈ s, Membership.mem (α := κ) t ((e : (a : ι) → κ) a : κ)
refine_2 : ∀ a ∈ t, Membership.mem (α := ι) s ((e.symm : (a : κ) → ι) a : ι)
refine_3 : ∀ a ∈ s, (e.symm : (a : κ) → ι) ((e : (a : ι) → κ) a : κ) = a
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, f i) (∏ i ∈ t, g i)
have refine_4 : ∀ a ∈ t, (e : (a : ι) → κ) ((e.symm : (a : κ) → ι) a : ι) = a
Tactic: refine prod_nbij' e e.symm ?_ ?_ ?_ ?_ hfg
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : CommMonoid M
inst_1 : CommMonoid N
r : M → N → Prop
f : ι → M
g : ι → N
s : Finset ι
h₁ : r 1 1
h₂ : ∀ (a : ι) (b : M) (c : N), r b c → r (f a * b) (g a * c)
⊢ r (∏ x ∈ s, f x) (∏ x ∈ s, g x)
have delta : r (Multiset.prod (Multiset.map (fun (x : ι) ↦ f x) s.val)) (Multiset.prod (Multiset.map (fun (x : ι) ↦ g x) s.val))
Tactic: delta Finset.prod
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
p : Prop
inst_1 : Decidable p
s : Finset ι
f g : ι → M
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, if p then f x else g x) (if p then ∏ x ∈ s, f x else ∏ x ∈ s, g x)
have pos : ∀ (h : p), Eq.{u_3 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ s, f x)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
p : Prop
inst_1 : Decidable p
s : Finset ι
f g : ι → M
pos : ∀ (h : p), Eq.{u_3 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ s, f x)
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, if p then f x else g x) (if p then ∏ x ∈ s, f x else ∏ x ∈ s, g x)
have neg : ∀ (h : ¬p), Eq.{u_3 + 1} (α := M) (∏ x ∈ s, g x) (∏ x ∈ s, g x)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
p : Prop
inst_1 : Decidable p
s : Finset ι
f : p → ι → M
g : ¬p → ι → M
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, if h : p then f h x else g h x) (if h : p then ∏ x ∈ s, f h x else ∏ x ∈ s, g h x)
have pos : ∀ (h : p), Eq.{u_3 + 1} (α := M) (∏ x ∈ s, f h x) (∏ x ∈ s, f h x)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
p : Prop
inst_1 : Decidable p
s : Finset ι
f : p → ι → M
g : ¬p → ι → M
pos : ∀ (h : p), Eq.{u_3 + 1} (α := M) (∏ x ∈ s, f h x) (∏ x ∈ s, f h x)
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, if h : p then f h x else g h x) (if h : p then ∏ x ∈ s, f h x else ∏ x ∈ s, g h x)
have neg : ∀ (h : ¬p), Eq.{u_3 + 1} (α := M) (∏ x ∈ s, g h x) (∏ x ∈ s, g h x)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
⊢ Eq.{u_3 + 1} (α := M) (∏ k ∈ range 0, f k) 1
have rw : Eq.{u_3 + 1} (α := M) (∏ k ∈ ∅, f k) 1
Tactic: rw [range_zero, prod_empty]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
rw : Eq.{u_3 + 1} (α := M) (∏ k ∈ ∅, f k) 1
⊢ Eq.{u_3 + 1} (α := M) (∏ k ∈ range 0, f k) 1
have rw₁ : Eq.{u_3 + 1} (α := M) 1 1
Tactic: rw [range_zero, prod_empty]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
m : Multiset ι
f : { x : ι // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x : ι // x ∈ m }), f x = g (↑x : ι)
⊢ Eq.{u_3 + 1} (α := M) (∏ x : { x : ι // x ∈ m }, f x) (∏ x ∈ m.toFinset, g x)
have refine_1 : ∀ (a : { x : ι // x ∈ m }) (ha : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ a),
  (fun (x : { x : ι // x ∈ m }) (x_1 : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ x) ↦ (↑x : ι)) a ha ∈
    m.toFinset
Tactic: refine prod_bij' (fun x _ ↦ x) (fun x hx ↦ ⟨x, Multiset.mem_toFinset.1 hx⟩) ?_ ?_ ?_ ?_ ?_