awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
f : ι → M
a : ι
s : Finset ι
ha : a ∈ s
⊢ f a ∣ ∏ i ∈ s, f i
have rw : f a ∣ f a * ∏ x ∈ s \ {a}, f x
Tactic: rw [Finset.prod_eq_mul_prod_diff_singleton_of_mem ha]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
f : ι → M
a : ι
s : Finset ι
ha : a ∈ s
⊢ f a ∣ ∏ i ∈ s, f i
have rw : f a ∣ f a * ∏ x ∈ s \ {a}, f x
Tactic: classical
    rw [Finset.prod_eq_mul_prod_diff_singleton_of_mem ha]
    exact dvd_mul_right _ _
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
i : ι
h : i ∉ s
f : ι → M
b : M
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, Function.update (β := fun (a : ι) ↦ M) f i b x) (∏ x ∈ s, f x)
have apply : ∀ x ∈ s, Function.update (β := fun (a : ι) ↦ M) f i b x = f x
Tactic: apply prod_congr rfl
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (hypothesis)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
i : ι
h : i ∉ s
f : ι → M
b : M
j : ι
hj : j ∈ s
⊢ Function.update (β := fun (a : ι) ↦ M) f i b j = f j
have this : j ≠ i
Tactic: have : j ≠ i := by
    rintro rfl
    exact h hj
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
i : ι
h : i ∈ s
f : ι → M
b : M
⊢ ∏ x ∈ s, Function.update (β := fun (a : ι) ↦ M) f i b x = b * ∏ x ∈ s \ {i}, f x
have rw : HMul.hMul (α := M) (∏ x ∈ s ∩ {i}, b) (∏ x ∈ s \ {i}, f x) = b * ∏ x ∈ s \ {i}, f x
Tactic: rw [update_eq_piecewise, prod_piecewise]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
⊢ (∏ i ∈ s, if p i then a else 1) = if ∃ i ∈ s, p i then a else 1
have pos : ∀ (h : ∃ i ∈ s, p i), (∏ i ∈ s, if p i then a else 1) = a
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
pos : ∀ (h : ∃ i ∈ s, p i), (∏ i ∈ s, if p i then a else 1) = a
⊢ (∏ i ∈ s, if p i then a else 1) = if ∃ i ∈ s, p i then a else 1
have neg : ∀ (h : ¬∃ i ∈ s, p i), Eq.{u_3 + 1} (α := M) (∏ i ∈ s, if p i then a else 1) 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
p : ι → Prop
inst_1 : DecidablePred p
h_1 : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
h : ∃ i ∈ s, p i
⊢ (∏ i ∈ s, if p i then a else 1) = a
have pos : ∀ (i : ι) (hi : i ∈ s) (hpi : p i), (∏ i ∈ s, if p i then a else 1) = a
Tactic: obtain ⟨i, hi, hpi⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
i : ι
hi : i ∈ s
hpi : p i
⊢ (∏ i ∈ s, if p i then a else 1) = a
have pos : ∀ b ∈ s, b ≠ i → (if p b then a else 1) = 1
Tactic: rw [prod_eq_single_of_mem _ hi, if_pos hpi]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (hypothesis)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
p : ι → Prop
inst_1 : DecidablePred p
h_1 : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
h : ¬∃ i ∈ s, p i
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, if p i then a else 1) 1
have h₁ : ∀ (i : ι) (_ : i ∈ s), ¬p i
Tactic: push Not at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
p : ι → Prop
inst_1 : DecidablePred p
h_1 : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
h : ∀ (i : ι) (_ : i ∈ s), ¬p i
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, if p i then a else 1) 1
have neg : ∀ x ∈ s, (if p x then a else 1) = 1
Tactic: rw [prod_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
inst_1 : IsRightCancelMul M
f g : ι → M
i : ι
hi : i ∈ s
hfg : ∀ j ∈ s, j ≠ i → f j = g j
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ s, f j) (∏ j ∈ s, g j) ↔ f i = g i
have rw : f i * ∏ x ∈ s \ {i}, f x = ∏ j ∈ s, g j ↔ f i = g i
Tactic: rw [prod_eq_mul_prod_diff_singleton_of_mem hi, prod_eq_mul_prod_diff_singleton_of_mem hi,
    prod_congr rfl (by simpa), mul_left_inj]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
inst_1 : IsRightCancelMul M
f g : ι → M
i : ι
hi : i ∈ s
hfg : ∀ j ∈ s, j ≠ i → f j = g j
rw : f i * ∏ x ∈ s \ {i}, f x = ∏ j ∈ s, g j ↔ f i = g i
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ s, f j) (∏ j ∈ s, g j) ↔ f i = g i
have rw₁ : f i * ∏ x ∈ s \ {i}, f x = g i * ∏ x ∈ s \ {i}, g x ↔ f i = g i
Tactic: rw [prod_eq_mul_prod_diff_singleton_of_mem hi, prod_eq_mul_prod_diff_singleton_of_mem hi,
    prod_congr rfl (by simpa), mul_left_inj]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
inst_1 : IsRightCancelMul M
f g : ι → M
i : ι
hi : i ∈ s
hfg : ∀ j ∈ s, j ≠ i → f j = g j
rw : f i * ∏ x ∈ s \ {i}, f x = ∏ j ∈ s, g j ↔ f i = g i
rw₁ : f i * ∏ x ∈ s \ {i}, f x = g i * ∏ x ∈ s \ {i}, g x ↔ f i = g i
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ s, f j) (∏ j ∈ s, g j) ↔ f i = g i
have rw₂ : f i * (s \ {i}).prod g = g i * ∏ x ∈ s \ {i}, g x ↔ f i = g i
Tactic: rw [prod_eq_mul_prod_diff_singleton_of_mem hi, prod_eq_mul_prod_diff_singleton_of_mem hi,
    prod_congr rfl (by simpa), mul_left_inj]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
inst_1 : IsRightCancelMul M
f g : ι → M
i : ι
hi : i ∈ s
hfg : ∀ j ∈ s, j ≠ i → f j = g j
rw : f i * ∏ x ∈ s \ {i}, f x = ∏ j ∈ s, g j ↔ f i = g i
rw₁ : f i * ∏ x ∈ s \ {i}, f x = g i * ∏ x ∈ s \ {i}, g x ↔ f i = g i
rw₂ : f i * (s \ {i}).prod g = g i * ∏ x ∈ s \ {i}, g x ↔ f i = g i
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ s, f j) (∏ j ∈ s, g j) ↔ f i = g i
have rw₃ : f i = g i ↔ f i = g i
Tactic: rw [prod_eq_mul_prod_diff_singleton_of_mem hi, prod_eq_mul_prod_diff_singleton_of_mem hi,
    prod_congr rfl (by simpa), mul_left_inj]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
inst_1 : IsRightCancelMul M
f g : ι → M
i : ι
hi : i ∈ s
hfg : ∀ j ∈ s, j ≠ i → f j = g j
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ s, f j) (∏ j ∈ s, g j) ↔ f i = g i
have rw : f i * ∏ x ∈ s \ {i}, f x = ∏ j ∈ s, g j ↔ f i = g i
Tactic: classical
  rw [prod_eq_mul_prod_diff_singleton_of_mem hi, prod_eq_mul_prod_diff_singleton_of_mem hi,
    prod_congr rfl (by simpa), mul_left_inj]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
inst_1 : IsRightCancelMul M
f g : ι → M
i : ι
hi : i ∈ s
hfg : ∀ j ∈ s, j ≠ i → f j = g j
rw : f i * ∏ x ∈ s \ {i}, f x = ∏ j ∈ s, g j ↔ f i = g i
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ s, f j) (∏ j ∈ s, g j) ↔ f i = g i
have rw₁ : f i * ∏ x ∈ s \ {i}, f x = g i * ∏ x ∈ s \ {i}, g x ↔ f i = g i
Tactic: classical
  rw [prod_eq_mul_prod_diff_singleton_of_mem hi, prod_eq_mul_prod_diff_singleton_of_mem hi,
    prod_congr rfl (by simpa), mul_left_inj]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
inst_1 : IsRightCancelMul M
f g : ι → M
i : ι
hi : i ∈ s
hfg : ∀ j ∈ s, j ≠ i → f j = g j
rw : f i * ∏ x ∈ s \ {i}, f x = ∏ j ∈ s, g j ↔ f i = g i
rw₁ : f i * ∏ x ∈ s \ {i}, f x = g i * ∏ x ∈ s \ {i}, g x ↔ f i = g i
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ s, f j) (∏ j ∈ s, g j) ↔ f i = g i
have rw₂ : f i * (s \ {i}).prod g = g i * ∏ x ∈ s \ {i}, g x ↔ f i = g i
Tactic: classical
  rw [prod_eq_mul_prod_diff_singleton_of_mem hi, prod_eq_mul_prod_diff_singleton_of_mem hi,
    prod_congr rfl (by simpa), mul_left_inj]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
inst_1 : IsRightCancelMul M
f g : ι → M
i : ι
hi : i ∈ s
hfg : ∀ j ∈ s, j ≠ i → f j = g j
rw : f i * ∏ x ∈ s \ {i}, f x = ∏ j ∈ s, g j ↔ f i = g i
rw₁ : f i * ∏ x ∈ s \ {i}, f x = g i * ∏ x ∈ s \ {i}, g x ↔ f i = g i
rw₂ : f i * (s \ {i}).prod g = g i * ∏ x ∈ s \ {i}, g x ↔ f i = g i
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ s, f j) (∏ j ∈ s, g j) ↔ f i = g i
have rw₃ : f i = g i ↔ f i = g i
Tactic: classical
  rw [prod_eq_mul_prod_diff_singleton_of_mem hi, prod_eq_mul_prod_diff_singleton_of_mem hi,
    prod_congr rfl (by simpa), mul_left_inj]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i : ι
f : (j : ι) → i = j → M
⊢ (∏ j : ι, if h : i = j then f j h else 1) = f i ⋯
have rw : (if Membership.mem (γ := Finset ι) univ i then f i sorry else 1) = f i sorry
Tactic: rw [Finset.prod_dite_eq, if_pos (mem_univ _)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i : ι
f : (j : ι) → i = j → M
rw : (if Membership.mem (γ := Finset ι) univ i then f i ⋯ else 1) = f i ⋯
⊢ (∏ j : ι, if h : i = j then f j h else 1) = f i ⋯
have rw₁ : f i sorry = f i sorry
Tactic: rw [Finset.prod_dite_eq, if_pos (mem_univ _)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i : ι
f : (j : ι) → j = i → M
⊢ (∏ j : ι, if h : j = i then f j h else 1) = f i ⋯
have rw : (if Membership.mem (γ := Finset ι) univ i then f i sorry else 1) = f i sorry
Tactic: rw [Finset.prod_dite_eq', if_pos (mem_univ _)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i : ι
f : (j : ι) → j = i → M
rw : (if Membership.mem (γ := Finset ι) univ i then f i ⋯ else 1) = f i ⋯
⊢ (∏ j : ι, if h : j = i then f j h else 1) = f i ⋯
have rw₁ : f i sorry = f i sorry
Tactic: rw [Finset.prod_dite_eq', if_pos (mem_univ _)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i : ι
f : ι → M
⊢ (∏ j : ι, if i = j then f j else 1) = f i
have rw : (if Membership.mem (γ := Finset ι) univ i then f i else 1) = f i
Tactic: rw [Finset.prod_ite_eq, if_pos (mem_univ _)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i : ι
f : ι → M
rw : (if Membership.mem (γ := Finset ι) univ i then f i else 1) = f i
⊢ (∏ j : ι, if i = j then f j else 1) = f i
have rw₁ : f i = f i
Tactic: rw [Finset.prod_ite_eq, if_pos (mem_univ _)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i : ι
f : ι → M
⊢ (∏ j : ι, if j = i then f j else 1) = f i
have rw : (if Membership.mem (γ := Finset ι) univ i then f i else 1) = f i
Tactic: rw [Finset.prod_ite_eq', if_pos (mem_univ _)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i : ι
f : ι → M
rw : (if Membership.mem (γ := Finset ι) univ i then f i else 1) = f i
⊢ (∏ j : ι, if j = i then f j else 1) = f i
have rw₁ : f i = f i
Tactic: rw [Finset.prod_ite_eq', if_pos (mem_univ _)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Powerset (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
a : α
inst : CommMonoid β
inst_1 : DecidableEq α
ha : a ∉ s
f : Finset α → β
⊢ ∏ t ∈ (insert a s).powerset, f t = HMul.hMul (α := β) (∏ t ∈ s.powerset, f t) (∏ t ∈ s.powerset, f (insert a t))
have rw : Set.InjOn (insert a) (↑s.powerset : Set (Finset α))
Tactic: rw [powerset_insert, prod_union, prod_image]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Powerset (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
a : α
inst : CommMonoid β
inst_1 : DecidableEq α
ha : a ∉ s
f : Finset α → β
rw : Set.InjOn (insert a) (↑s.powerset : Set (Finset α))
⊢ ∏ t ∈ (insert a s).powerset, f t = HMul.hMul (α := β) (∏ t ∈ s.powerset, f t) (∏ t ∈ s.powerset, f (insert a t))
have rw₁ : Disjoint s.powerset (image (insert a) s.powerset)
Tactic: rw [powerset_insert, prod_union, prod_image]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Powerset (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
a : α
inst : CommMonoid β
ha : a ∉ s
f : Finset α → β
⊢ ∏ t ∈ (cons a s ha).powerset, f t =
    HMul.hMul (α := β) (∏ t ∈ s.powerset, f t) (∏ t ∈ s.powerset.attach, f (cons a (↑t : Finset α) ⋯))
have simp_rw : ∏ x ∈ (insert a s).powerset, f x =
  HMul.hMul (α := β) (∏ x ∈ s.powerset, f x) (∏ x ∈ s.powerset.attach, f (insert a (↑x : Finset α)))
Tactic: simp_rw [cons_eq_insert]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Powerset (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
a : α
inst : CommMonoid β
ha : a ∉ s
f : Finset α → β
⊢ ∏ x ∈ (insert a s).powerset, f x =
    HMul.hMul (α := β) (∏ x ∈ s.powerset, f x) (∏ x ∈ s.powerset.attach, f (insert a (↑x : Finset α)))
have rw : HMul.hMul (α := β) (∏ t ∈ s.powerset, f t) (∏ t ∈ s.powerset, f (insert a t)) =
  HMul.hMul (α := β) (∏ x ∈ s.powerset, f x) (∏ x ∈ s.powerset.attach, f (insert a (↑x : Finset α)))
Tactic: rw [prod_powerset_insert ha, prod_attach _ fun t ↦ f (insert a t)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Powerset (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
a : α
inst : CommMonoid β
ha : a ∉ s
f : Finset α → β
rw :
  HMul.hMul (α := β) (∏ t ∈ s.powerset, f t) (∏ t ∈ s.powerset, f (insert a t)) =
    HMul.hMul (α := β) (∏ x ∈ s.powerset, f x) (∏ x ∈ s.powerset.attach, f (insert a (↑x : Finset α)))
⊢ ∏ x ∈ (insert a s).powerset, f x =
    HMul.hMul (α := β) (∏ x ∈ s.powerset, f x) (∏ x ∈ s.powerset.attach, f (insert a (↑x : Finset α)))
have rw₁ : HMul.hMul (α := β) (∏ t ∈ s.powerset, f t) (∏ t ∈ s.powerset, f (insert a t)) =
  HMul.hMul (α := β) (∏ x ∈ s.powerset, f x) (∏ x ∈ s.powerset, f (insert a x))
Tactic: rw [prod_powerset_insert ha, prod_attach _ fun t ↦ f (insert a t)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Powerset (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
a : α
inst : CommMonoid β
ha : a ∉ s
f : Finset α → β
⊢ ∏ t ∈ (cons a s ha).powerset, f t =
    HMul.hMul (α := β) (∏ t ∈ s.powerset, f t) (∏ t ∈ s.powerset.attach, f (cons a (↑t : Finset α) ⋯))
have simp_rw : ∏ x ∈ (insert a s).powerset, f x =
  HMul.hMul (α := β) (∏ x ∈ s.powerset, f x) (∏ x ∈ s.powerset.attach, f (insert a (↑x : Finset α)))
Tactic: classical
  simp_rw [cons_eq_insert]
  rw [prod_powerset_insert ha, prod_attach _ fun t ↦ f (insert a t)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Powerset (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid β
s : Finset α
f : Finset α → β
⊢ Eq.{u_2 + 1} (α := β) (∏ t ∈ s.powerset, f t) (∏ j ∈ range (#s + 1), ∏ t ∈ powersetCard j s, f t)
have rw : Eq.{u_2 + 1} (α := β) (∏ t ∈ (range (#s + 1)).disjiUnion (fun (i : ℕ) ↦ powersetCard i s) sorry, f t)
  (∏ j ∈ range (#s + 1), ∏ t ∈ powersetCard j s, f t)
Tactic: rw [powerset_card_disjiUnion, prod_disjiUnion]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Powerset (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid β
s : Finset α
f : Finset α → β
rw :
  Eq.{u_2 + 1} (α := β) (∏ t ∈ (range (#s + 1)).disjiUnion (fun (i : ℕ) ↦ powersetCard i s) ⋯, f t)
    (∏ j ∈ range (#s + 1), ∏ t ∈ powersetCard j s, f t)
⊢ Eq.{u_2 + 1} (α := β) (∏ t ∈ s.powerset, f t) (∏ j ∈ range (#s + 1), ∏ t ∈ powersetCard j s, f t)
have rw₁ : Eq.{u_2 + 1} (α := β) (∏ i ∈ range (#s + 1), ∏ x ∈ powersetCard i s, f x)
  (∏ j ∈ range (#s + 1), ∏ t ∈ powersetCard j s, f t)
Tactic: rw [powerset_card_disjiUnion, prod_disjiUnion]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Powerset (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid β
n : ℕ
s : Finset α
f : ℕ → β
⊢ ∏ t ∈ powersetCard n s, f #t = f n ^ (#s).choose n
have rw : ∀ a ∈ powersetCard n s, f #a = f n
Tactic: rw [prod_eq_pow_card, card_powersetCard]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Powerset (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid β
n : ℕ
s : Finset α
f : ℕ → β
a : Finset α
ha : a ∈ powersetCard n s
⊢ f #a = f n
have rw : f n = f n
Tactic: rw [(mem_powersetCard.1 ha).2]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Preimage (goal)
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst : CommMonoid β
f : ι → κ
inst_1 : DecidablePred fun (x : κ) ↦ x ∈ Set.range f
s : Finset κ
hf : Set.InjOn f (f ⁻¹' (↑s : Set κ))
g : κ → β
⊢ Eq.{u_3 + 1} (α := β) (∏ x ∈ image f (s.preimage f hf), g x) (∏ x ∈ s with x ∈ Set.range f, g x)
have rw : Eq.{u_3 + 1} (α := β) (∏ x ∈ s with x ∈ Set.range f, g x) (∏ x ∈ s with x ∈ Set.range f, g x)
Tactic: rw [image_preimage]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Preimage (goal)
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst : CommMonoid β
f : ι → κ
inst_1 : DecidablePred fun (x : κ) ↦ x ∈ Set.range f
s : Finset κ
hf : Set.InjOn f (f ⁻¹' (↑s : Set κ))
g : κ → β
⊢ Eq.{u_3 + 1} (α := β) (∏ x ∈ s.preimage f hf, g (f x)) (∏ x ∈ s with x ∈ Set.range f, g x)
have x : Eq.{u_3 + 1} (α := β) (∏ x ∈ image f (s.preimage f hf), g x) (∏ x ∈ s with x ∈ Set.range f, g x)
Tactic: calc
    ∏ x ∈ preimage s f hf, g (f x) = ∏ x ∈ image f (preimage s f hf), g x :=
      Eq.symm <| prod_image <| by simpa [mem_preimage, Set.InjOn] using hf
    _ = ∏ x ∈ s with x ∈ Set.range f, g x := by rw [image_preimage]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Preimage (goal)
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst : CommMonoid β
f : ι → κ
inst_1 : DecidablePred fun (x : κ) ↦ x ∈ Set.range f
s : Finset κ
hf : Set.InjOn f (f ⁻¹' (↑s : Set κ))
g : κ → β
⊢ Eq.{u_3 + 1} (α := β) (∏ x ∈ s.preimage f hf, g (f x)) (∏ x ∈ s with x ∈ Set.range f, g x)
have x : Eq.{u_3 + 1} (α := β) (∏ x ∈ image f (s.preimage f hf), g x) (∏ x ∈ s with x ∈ Set.range f, g x)
Tactic: classical
  calc
    ∏ x ∈ preimage s f hf, g (f x) = ∏ x ∈ image f (preimage s f hf), g x :=
      Eq.symm <| prod_image <| by simpa [mem_preimage, Set.InjOn] using hf
    _ = ∏ x ∈ s with x ∈ Set.range f, g x := by rw [image_preimage]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Preimage (goal)
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst : CommMonoid β
f : ι → κ
s : Finset κ
hf : Set.InjOn f (f ⁻¹' (↑s : Set κ))
g : κ → β
hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1
⊢ Eq.{u_3 + 1} (α := β) (∏ x ∈ s.preimage f hf, g (f x)) (∏ x ∈ s, g x)
have rw : ∀ x ∈ s, g x ≠ 1 → x ∈ Set.range f
Tactic: rw [prod_preimage', prod_filter_of_ne]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Preimage (goal)
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst : CommMonoid β
f : ι → κ
s : Finset κ
hf : Set.InjOn f (f ⁻¹' (↑s : Set κ))
g : κ → β
hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1
⊢ Eq.{u_3 + 1} (α := β) (∏ x ∈ s.preimage f hf, g (f x)) (∏ x ∈ s, g x)
have classical : Eq.{u_3 + 1} (α := β) (∏ x ∈ s with x ∈ Set.range f, g x) (∏ x ∈ s, g x)
Tactic: classical rw [prod_preimage', prod_filter_of_ne]; exact fun x hx ↦ Not.imp_symm (hg x hx)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Preimage (goal)
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst : CommMonoid β
f : ι → κ
s : Finset κ
hf : Set.InjOn f (f ⁻¹' (↑s : Set κ))
g : κ → β
hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1
classical : Eq.{u_3 + 1} (α := β) (∏ x ∈ s with x ∈ Set.range f, g x) (∏ x ∈ s, g x)
⊢ Eq.{u_3 + 1} (α := β) (∏ x ∈ s.preimage f hf, g (f x)) (∏ x ∈ s, g x)
have classical₁ : Eq.{u_3 + 1} (α := β) (∏ x ∈ s, g x) (∏ x ∈ s, g x)
Tactic: classical rw [prod_preimage', prod_filter_of_ne]; exact fun x hx ↦ Not.imp_symm (hg x hx)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Preimage (goal)
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst : CommMonoid β
f : ι → κ
s : Finset κ
hf : Set.InjOn f (f ⁻¹' (↑s : Set κ))
g : κ → β
hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1
classical : Eq.{u_3 + 1} (α := β) (∏ x ∈ s with x ∈ Set.range f, g x) (∏ x ∈ s, g x)
classical₁ : Eq.{u_3 + 1} (α := β) (∏ x ∈ s, g x) (∏ x ∈ s, g x)
⊢ Eq.{u_3 + 1} (α := β) (∏ x ∈ s.preimage f hf, g (f x)) (∏ x ∈ s, g x)
have classical₂ : ∀ x ∈ s, g x ≠ 1 → x ∈ Set.range f
Tactic: classical rw [prod_preimage', prod_filter_of_ne]; exact fun x hx ↦ Not.imp_symm (hg x hx)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Sigma (goal)
Goal:
α : Type u_3
β : Type u_4
inst : CommMonoid β
σ : α → Type u_6
s : Finset α
t : (a : α) → Finset (σ a)
f : Sigma σ → β
⊢ Eq.{u_4 + 1} (α := β) (∏ x ∈ s.sigma (α := σ) t, f x) (∏ a ∈ s, ∏ s ∈ t a, f (Sigma.mk (β := σ) a s))
have simp_rw : Eq.{u_4 + 1} (α := β) (∏ x ∈ s.disjiUnion (fun (i : α) ↦ map (Embedding.sigmaMk (β := σ) i) (t i)) sorry, f x)
  (∏ a ∈ s, ∏ s ∈ t a, f (Sigma.mk (β := σ) a s))
Tactic: simp_rw [← disjiUnion_map_sigma_mk, prod_disjiUnion, prod_map, Function.Embedding.sigmaMk_apply]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Sigma (goal)
Goal:
α : Type u_3
β : Type u_4
inst : CommMonoid β
σ : α → Type u_6
s : Finset α
t : (a : α) → Finset (σ a)
f : Sigma σ → β
simp_rw :
  Eq.{u_4 + 1} (α := β) (∏ x ∈ s.disjiUnion (fun (i : α) ↦ map (Embedding.sigmaMk (β := σ) i) (t i)) ⋯, f x)
    (∏ a ∈ s, ∏ s ∈ t a, f (Sigma.mk (β := σ) a s))
⊢ Eq.{u_4 + 1} (α := β) (∏ x ∈ s.sigma (α := σ) t, f x) (∏ a ∈ s, ∏ s ∈ t a, f (Sigma.mk (β := σ) a s))
have simp_rw₁ : Eq.{u_4 + 1} (α := β) (∏ i ∈ s, ∏ x ∈ map (Embedding.sigmaMk (β := σ) i) (t i), f x)
  (∏ a ∈ s, ∏ s ∈ t a, f (Sigma.mk (β := σ) a s))
Tactic: simp_rw [← disjiUnion_map_sigma_mk, prod_disjiUnion, prod_map, Function.Embedding.sigmaMk_apply]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Sigma (goal)
Goal:
α : Type u_3
β : Type u_4
inst : CommMonoid β
σ : α → Type u_6
s : Finset α
t : (a : α) → Finset (σ a)
f : Sigma σ → β
simp_rw :
  Eq.{u_4 + 1} (α := β) (∏ x ∈ s.disjiUnion (fun (i : α) ↦ map (Embedding.sigmaMk (β := σ) i) (t i)) ⋯, f x)
    (∏ a ∈ s, ∏ s ∈ t a, f (Sigma.mk (β := σ) a s))
simp_rw₁ :
  Eq.{u_4 + 1} (α := β) (∏ i ∈ s, ∏ x ∈ map (Embedding.sigmaMk (β := σ) i) (t i), f x)
    (∏ a ∈ s, ∏ s ∈ t a, f (Sigma.mk (β := σ) a s))
⊢ Eq.{u_4 + 1} (α := β) (∏ x ∈ s.sigma (α := σ) t, f x) (∏ a ∈ s, ∏ s ∈ t a, f (Sigma.mk (β := σ) a s))
have simp_rw₂ : Eq.{u_4 + 1} (α := β) (∏ x ∈ s, ∏ x_1 ∈ t x, f ((Embedding.sigmaMk (β := σ) x : (a : σ x) → (i : α) × σ i) x_1))
  (∏ a ∈ s, ∏ s ∈ t a, f (Sigma.mk (β := σ) a s))
Tactic: simp_rw [← disjiUnion_map_sigma_mk, prod_disjiUnion, prod_map, Function.Embedding.sigmaMk_apply]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Sigma (goal)
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
r : Finset (γ × α)
s : Finset γ
t : γ → Finset α
h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
f : γ × α → β
⊢ Eq.{u_4 + 1} (α := β) (∏ p ∈ r, f p) (∏ c ∈ s, ∏ a ∈ t c, f (c, a))
have refine : Eq.{u_4 + 1} (α := β) (∏ p ∈ r, f p)
  (∏ x ∈ s.sigma (α := fun (a : γ) ↦ α) t, f (x.fst (β := fun (a : γ) ↦ α), x.snd (β := fun (a : γ) ↦ α)))
Tactic: refine Eq.trans ?_ (prod_sigma s t fun p => f (p.1, p.2))