awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s t : Finset ι
f g : ι → M
rw :
  HMul.hMul (α := M) (∏ x ∈ s with x ∈ t, f x) (∏ x ∈ s with x ∉ t, g x) =
    HMul.hMul (α := M) (∏ x ∈ s ∩ t, f x) (∏ x ∈ s \ t, g x)
rw₁ :
  HMul.hMul (α := M) (∏ x ∈ s ∩ t, f x) (∏ x ∈ s with x ∉ t, g x) =
    HMul.hMul (α := M) (∏ x ∈ s ∩ t, f x) (∏ x ∈ s \ t, g x)
rw₂ rw₃ :
  HMul.hMul (α := M) (∏ x ∈ s ∩ t, f x) (∏ x ∈ s \ t, g x) = HMul.hMul (α := M) (∏ x ∈ s ∩ t, f x) (∏ x ∈ s \ t, g x)
⊢ (∏ x ∈ s, if x ∈ t then f x else g x) = HMul.hMul (α := M) (∏ x ∈ s ∩ t, f x) (∏ x ∈ s \ t, g x)

Tactic:
rw [prod_ite, filter_mem_eq_inter, ← sdiff_eq_filter]

Premises used: Finset.sdiff_eq_filter, Finset.prod_ite, Finset.filter_mem_eq_inter
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ HMul.hMul (α := M) (∏ x ∈ s ∩ t, f x) (∏ x ∈ s \ t, f x) = ∏ x ∈ s, t.piecewise (π := fun (i : ι) ↦ M) f f x

Tactic:
(s.prod_piecewise t f f).symm

Premises used: Eq.symm, Finset.prod_piecewise
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s t : Finset ι
f : ι → M
h : ∀ x ∈ s, f = t.piecewise (π := fun (i : ι) ↦ M) f f
⊢ HMul.hMul (α := M) (∏ x ∈ s ∩ t, f x) (∏ x ∈ s \ t, f x) = ∏ x ∈ s, f x

Tactic:
convert! (s.prod_piecewise t f f).symm

Premises used: Eq.symm, Finset.prod_piecewise
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s t : Finset ι
f : ι → M
x : ι
h : x ∈ s
⊢ f = t.piecewise (π := fun (i : ι) ↦ M) f f

Tactic:
simp +unfoldPartialApp [Finset.piecewise]

Premises used: Finset.piecewise
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : i ∉ s → f i = 1
pos : ∀ (hs : i ∈ s), ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x
neg : ∀ (hs : i ∉ s), ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x
⊢ ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x

Tactic:
by_cases hs : i ∈ s
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : i ∉ s → f i = 1
hs : i ∈ s
⊢ ∏ x ∈ s, f x = HMul.hMul (α := M) (∏ x ∈ s ∩ {i}, f x) (∏ x ∈ s \ {i}, f x)

Tactic:
(s.prod_inter_mul_prod_diff { i } f).symm

Premises used: Finset.prod_inter_mul_prod_diff, Singleton.singleton, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : i ∉ s → f i = 1
hs : i ∈ s
h₁ : f i = ∏ x ∈ s ∩ {i}, f x
⊢ ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x

Tactic:
convert! (s.prod_inter_mul_prod_diff { i } f).symm

Premises used: Finset.prod_inter_mul_prod_diff, Singleton.singleton, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : i ∉ s → f i = 1
hs : i ∈ s
⊢ f i = ∏ x ∈ s ∩ {i}, f x

Tactic:
simp [hs]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : i ∉ s → f i = 1
hs : i ∉ s
neg : ∀ (h : f i = 1) (hs : i ∉ s), Eq.{u_3 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ s \ {i}, f x)
⊢ ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x

Tactic:
simp_all only [not_false_eq_true, forall_const, one_mul]

Premises used: forall_const, not_false_eq_true, one_mul
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : f i = 1
hs : i ∉ s
neg : s = s \ {i}
neg₁ : ∀ x ∈ s \ {i}, f x = f x
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ s \ {i}, f x)

Tactic:
apply Finset.prod_congr

Premises used: Finset.prod_congr
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : f i = 1
hs : i ∉ s
⊢ s = s \ {i}

Tactic:
aesop
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : f i = 1
hs : i ∉ s
⊢ ∀ x ∈ s \ {i}, f x = f x

Tactic:
aesop
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
i : ι
h : i ∈ s
f : ι → M
⊢ i ∉ s → f i = 1

Tactic:
simp_all
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
i : ι
h : i ∈ s
f : ι → M
rw : f i * ∏ x ∈ s \ {i}, f x = (∏ x ∈ s \ {i}, f x) * f i
rw₁ rw₂ : (∏ x ∈ s \ {i}, f x) * f i = (∏ x ∈ s \ {i}, f x) * f i
⊢ ∏ x ∈ s, f x = (∏ x ∈ s \ {i}, f x) * f i

Tactic:
rw [prod_eq_mul_prod_diff_singleton_of_mem h, mul_comm]

Premises used: Finset.prod_eq_mul_prod_diff_singleton_of_mem, mul_comm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
inst_2 : Fintype ι
a : ι
f : ι → M
⊢ ∏ i : ι, f i = f a * ∏ i ∈ {a}ᶜ, f i

Tactic:
prod_eq_mul_prod_diff_singleton_of_mem (mem_univ a) f

Premises used: Finset.mem_univ, Finset.prod_eq_mul_prod_diff_singleton_of_mem
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
inst_2 : Fintype ι
a : ι
f : ι → M
⊢ ∏ i : ι, f i = (∏ i ∈ {a}ᶜ, f i) * f a

Tactic:
prod_eq_prod_diff_singleton_mul (mem_univ a) f

Premises used: Finset.mem_univ, Finset.prod_eq_prod_diff_singleton_mul
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
f : ι → M
a : ι
s : Finset ι
ha : a ∈ s
rw : f a ∣ f a * ∏ x ∈ s \ {a}, f x
⊢ f a ∣ ∏ i ∈ s, f i

Tactic:
rw [Finset.prod_eq_mul_prod_diff_singleton_of_mem ha]

Premises used: Finset.prod_eq_mul_prod_diff_singleton_of_mem
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
f : ι → M
a : ι
s : Finset ι
ha : a ∈ s
⊢ f a ∣ f a * ∏ x ∈ s \ {a}, f x

Tactic:
dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
f : ι → M
a : ι
s : Finset ι
ha : a ∈ s
⊢ f a ∣ f a * ∏ x ∈ s \ {a}, f x

Tactic:
exact dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
f : ι → M
a : ι
s : Finset ι
ha : a ∈ s
rw rw₁ rw₂ : f a ∣ f a * ∏ x ∈ s \ {a}, f x
⊢ f a ∣ ∏ i ∈ s, f i

Tactic:
classical
    rw [Finset.prod_eq_mul_prod_diff_singleton_of_mem ha]
    exact dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
i : ι
h : i ∉ s
f : ι → M
b : M
apply : ∀ x ∈ s, Function.update (β := fun (a : ι) ↦ M) f i b x = f x
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, Function.update (β := fun (a : ι) ↦ M) f i b x) (∏ x ∈ s, f x)

Tactic:
apply prod_congr rfl

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
f : ι → M
b : M
j : ι
hj : j ∈ s
h : j ∉ s
⊢ False

Tactic:
h hj
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
f : ι → M
b : M
j : ι
hj : j ∈ s
h : j ∉ s
⊢ False

Tactic:
exact h hj
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
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
⊢ j ≠ i

Tactic:
have : j ≠ i := by
    rintro rfl
    exact h hj
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
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
this : j ≠ i
⊢ Function.update (β := fun (a : ι) ↦ M) f i b j = f j

Tactic:
simp [this]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
i : ι
h : i ∈ s
f : ι → M
b : M
rw : HMul.hMul (α := M) (∏ x ∈ s ∩ {i}, b) (∏ x ∈ s \ {i}, f x) = b * ∏ x ∈ s \ {i}, f x
⊢ ∏ x ∈ s, Function.update (β := fun (a : ι) ↦ M) f i b x = b * ∏ x ∈ s \ {i}, f x

Tactic:
rw [update_eq_piecewise, prod_piecewise]

Premises used: Finset.update_eq_piecewise, Finset.prod_piecewise
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
i : ι
h : i ∈ s
f : ι → M
b : M
⊢ HMul.hMul (α := M) (∏ x ∈ s ∩ {i}, b) (∏ x ∈ s \ {i}, f x) = b * ∏ x ∈ s \ {i}, f x

Tactic:
simp [h]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
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
neg : ∀ (h : ¬∃ i ∈ s, p i), Eq.{u_3 + 1} (α := M) (∏ i ∈ s, if p i then a else 1) 1
⊢ (∏ i ∈ s, if p i then a else 1) = if ∃ i ∈ s, p i then a else 1

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
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
pos : ∀ (i : ι) (hi : i ∈ s) (hpi : p i), (∏ i ∈ s, if p i then a else 1) = a
⊢ (∏ i ∈ s, if p i then a else 1) = a

Tactic:
obtain ⟨i, hi, hpi⟩ := h
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
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
pos : ∀ b ∈ s, b ≠ i → (if p b then a else 1) = 1
⊢ (∏ i ∈ s, if p i then a else 1) = a

Tactic:
rw [prod_eq_single_of_mem _ hi, if_pos hpi]

Premises used: Finset.prod_eq_single_of_mem, if_pos
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
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
⊢ ∀ b ∈ s, b ≠ i → (if p b then a else 1) = 1

Tactic:
fun j hj hji ↦ if_neg fun hpj ↦ hji <| h _ hj _ hi hpj hpi

Premises used: if_neg
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
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
⊢ ∀ b ∈ s, b ≠ i → (if p b then a else 1) = 1

Tactic:
exact fun j hj hji ↦ if_neg fun hpj ↦ hji <| h _ hj _ hi hpj hpi

Premises used: if_neg
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
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 : ι) (_ : i ∈ s), ¬p i

Tactic:
push Not at h

Premises used: Not
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
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
neg : ∀ x ∈ s, (if p x then a else 1) = 1
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, if p i then a else 1) 1

Tactic:
rw [prod_eq_one]

Premises used: Finset.prod_eq_one
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
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
⊢ ∀ x ∈ s, (if p x then a else 1) = 1

Tactic:
fun i hi => if_neg (h i hi)

Premises used: if_neg
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
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
⊢ ∀ x ∈ s, (if p x then a else 1) = 1

Tactic:
exact fun i hi => if_neg (h i hi)

Premises used: if_neg
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
⊢ ∏ x ∈ s, HPow.hPow (β := ℕ) (f x) (if a = x then 1 else 0) = if a ∈ s then f a else 1

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
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
⊢ ∀ x ∈ s \ {i}, f x = g x

Tactic:
simpa
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
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
rw₃ rw₄ : f i = g i ↔ f i = g i
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ s, f j) (∏ 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]

Premises used: mul_left_inj, Finset.prod_congr, Finset.prod_eq_mul_prod_diff_singleton_of_mem, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
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
rw₃ rw₄ : f i = g i ↔ f i = g i
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ s, f j) (∏ 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]

Premises used: mul_left_inj, Finset.prod_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
p : ι → Prop
inst : DecidablePred p
s : Finset ι
⊢ #({i ∈ s | p i}) = ∑ i ∈ s, if p i then 1 else 0

Tactic:
simp [sum_ite]

Premises used: Finset.sum_ite
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
p : ι → Prop
inst_2 : DecidablePred p
h : ∀ (i j : ι), p i → p j → i = j
a : M
⊢ ∀ (i : ι),
    Membership.mem (γ := Finset ι) univ i → ∀ (j : ι), Membership.mem (γ := Finset ι) univ j → p i → p j → i = j

Tactic:
simpa using h
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
p : ι → Prop
inst_2 : DecidablePred p
h : ∀ (i j : ι), p i → p j → i = j
a : M
⊢ (∏ i : ι, if p i then a else 1) = if ∃ (i : ι), p i then a else 1

Tactic:
simp [prod_ite_one univ p (by simpa using h)]

Premises used: Finset.prod_ite_one, Finset.univ
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
inst_2 : DecidableEq ι
s : Finset ι
f : ι → M
⊢ Eq.{u_3 + 1} (α := M) (∏ i : ι, if i ∈ s then f i else 1) (∏ i ∈ s, f i)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
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 ⋯
rw₁ rw₂ : f i ⋯ = f i ⋯
⊢ (∏ j : ι, if h : i = j then f j h else 1) = f i ⋯

Tactic:
rw [Finset.prod_dite_eq, if_pos (mem_univ _)]

Premises used: Finset.mem_univ, if_pos, Finset.prod_dite_eq
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
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 ⋯
rw₁ rw₂ : f i ⋯ = f i ⋯
⊢ (∏ j : ι, if h : j = i then f j h else 1) = f i ⋯

Tactic:
rw [Finset.prod_dite_eq', if_pos (mem_univ _)]

Premises used: Finset.mem_univ, if_pos, Finset.prod_dite_eq'
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
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
rw₁ rw₂ : f i = f i
⊢ (∏ j : ι, if i = j then f j else 1) = f i

Tactic:
rw [Finset.prod_ite_eq, if_pos (mem_univ _)]

Premises used: Finset.mem_univ, if_pos, Finset.prod_ite_eq
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
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
rw₁ rw₂ : f i = f i
⊢ (∏ j : ι, if j = i then f j else 1) = f i

Tactic:
rw [Finset.prod_ite_eq', if_pos (mem_univ _)]

Premises used: Finset.mem_univ, Finset.prod_ite_eq', if_pos
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_6
inst_2 : (i : ι) → CommMonoid (M i)
i : ι
f : (i : ι) → M i
⊢ ∏ j : ι, Pi.mulSingle (M := M) j (f j) i = f i

Tactic:
prod_dite_eq _ _

Premises used: Function.update, Fintype.prod_dite_eq, Pi.mulSingle
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i : ι
a : M
⊢ ∏ j : ι, Pi.mulSingle (M := fun (a : ι) ↦ M) i a j = a

Tactic:
prod_dite_eq' _ _

Premises used: Function.update, Fintype.prod_dite_eq', Pi.mulSingle
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Powerset
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 α))
rw₁ : Disjoint s.powerset (image (insert a) s.powerset)
⊢ ∏ t ∈ (insert a s).powerset, f t = HMul.hMul (α := β) (∏ t ∈ s.powerset, f t) (∏ t ∈ s.powerset, f (insert a t))

Tactic:
rw [powerset_insert, prod_union, prod_image]

Premises used: Finset.powerset_insert, Finset.prod_union, Finset.prod_image
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Powerset
Goal:
α : Type u_1
β : Type u_2
s : Finset α
a : α
inst : CommMonoid β
inst_1 : DecidableEq α
ha : a ∉ s
f : Finset α → β
⊢ Set.InjOn (insert a) (↑s.powerset : Set (Finset α))

Tactic:
insert_erase_invOn.2.injOn.mono fun t ht ↦ notMem_mono (mem_powerset.1 ht) ha

Premises used: Finset.insert_erase_invOn, Finset.mem_powerset, And.right, Iff.mp, Set.InjOn.mono, Finset.notMem_mono, Set.LeftInvOn.injOn
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Powerset
Goal:
α : Type u_1
β : Type u_2
s : Finset α
a : α
inst : CommMonoid β
inst_1 : DecidableEq α
ha : a ∉ s
f : Finset α → β
⊢ Set.InjOn (insert a) (↑s.powerset : Set (Finset α))

Tactic:
exact insert_erase_invOn.2.injOn.mono fun t ht ↦ notMem_mono (mem_powerset.1 ht) ha

Premises used: Finset.insert_erase_invOn, Finset.mem_powerset, And.right, Iff.mp, Set.InjOn.mono, Finset.notMem_mono, Set.LeftInvOn.injOn
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Powerset
Goal:
α : Type u_1
β : Type u_2
s : Finset α
a : α
inst : CommMonoid β
inst_1 : DecidableEq α
ha : a ∉ s
f : Finset α → β
⊢ Disjoint s.powerset (image (insert a) s.powerset)

Tactic:
aesop (add simp [disjoint_left, insert_subset_iff])

Premises used: Finset.insert_subset_iff, Finset.disjoint_left
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Powerset
Goal:
α : Type u_1
β : Type u_2
s : Finset α
a : α
inst : CommMonoid β
ha : a ∉ s
f : Finset α → β
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 α)))
⊢ ∏ t ∈ (cons a s ha).powerset, f t =
    HMul.hMul (α := β) (∏ t ∈ s.powerset, f t) (∏ t ∈ s.powerset.attach, f (cons a (↑t : Finset α) ⋯))

Tactic:
simp_rw [cons_eq_insert]

Premises used: Finset.cons_eq_insert
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Powerset
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 α)))
rw₁ 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))
⊢ ∏ x ∈ (insert a s).powerset, f x =
    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)]

Premises used: Insert.insert, Finset.prod_attach, Finset.prod_powerset_insert
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Powerset
Goal:
α : Type u_1
β : Type u_2
s : Finset α
a : α
inst : CommMonoid β
ha : a ∉ s
f : Finset α → β
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 α)))
⊢ ∏ t ∈ (cons a s ha).powerset, f t =
    HMul.hMul (α := β) (∏ t ∈ s.powerset, f t) (∏ t ∈ s.powerset.attach, f (cons a (↑t : Finset α) ⋯))

Tactic:
classical
  simp_rw [cons_eq_insert]
  rw [prod_powerset_insert ha, prod_attach _ fun t ↦ f (insert a t)]

Premises used: Finset.cons_eq_insert
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Powerset
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)
rw₁ 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)
⊢ Eq.{u_2 + 1} (α := β) (∏ t ∈ s.powerset, f t) (∏ j ∈ range (#s + 1), ∏ t ∈ powersetCard j s, f t)

Tactic:
rw [powerset_card_disjiUnion, prod_disjiUnion]

Premises used: Finset.prod_disjiUnion, Finset.powerset_card_disjiUnion
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Powerset
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid β
n : ℕ
s : Finset α
f : ℕ → β
rw : ∀ a ∈ powersetCard n s, f #a = f n
⊢ ∏ t ∈ powersetCard n s, f #t = f n ^ (#s).choose n

Tactic:
rw [prod_eq_pow_card, card_powersetCard]

Premises used: Finset.prod_eq_pow_card, Finset.card_powersetCard
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Powerset
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid β
n : ℕ
s : Finset α
f : ℕ → β
a : Finset α
ha : a ∈ powersetCard n s
rw rw₁ : f n = f n
⊢ f #a = f n

Tactic:
rw [(mem_powersetCard.1 ha).2]

Premises used: Finset.mem_powersetCard, And.right, Iff.mp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Preimage
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 : κ → β
⊢ Set.InjOn f (↑(s.preimage f hf) : Set ι)

Tactic:
simpa [mem_preimage, Set.InjOn] using hf

Premises used: Finset.mem_preimage, Set.InjOn