awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
rw : Eq.{u_4 + 1} (α := M) (∏ x ∈ image (fun (a : ↥s) ↦ (↑a : ι)) s.attach, f x) (∏ x ∈ s, f x)
rw₁ rw₂ : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ s, f x)
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.attach, f (↑x : ι)) (∏ x ∈ s, f x)

Tactic:
rw [← prod_image Subtype.coe_injective.injOn, attach_image_val]

Premises used: Function.Injective.injOn, Subtype.coe_injective, Finset.attach_image_val, Finset.prod_image
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
classical : Eq.{u_4 + 1} (α := M) (∏ x ∈ image (fun (a : ↥s) ↦ (↑a : ι)) s.attach, f x) (∏ x ∈ s, f x)
classical₁ classical₂ : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ s, f x)
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.attach, f (↑x : ι)) (∏ x ∈ s, f x)

Tactic:
classical rw [← prod_image Subtype.coe_injective.injOn, attach_image_val]

Premises used: Function.Injective.injOn, Subtype.coe_injective, Finset.attach_image_val, Finset.prod_image
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst : CommMonoid M
f g : ι → M
h : s₁ = s₂
rw : (∀ x ∈ s₂, f x = g x) → s₂.prod f = s₂.prod g
⊢ (∀ x ∈ s₂, f x = g x) → s₁.prod f = s₂.prod g

Tactic:
rw [h]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst : CommMonoid M
f g : ι → M
h : s₁ = s₂
⊢ (∀ x ∈ s₂, f x = g x) → s₂.prod f = s₂.prod g

Tactic:
fold_congr

Premises used: Multiset.prod, Finset.fold_congr, Finset.prod
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst : CommMonoid M
f g : ι → M
h : s₁ = s₂
⊢ (∀ x ∈ s₂, f x = g x) → s₂.prod f = s₂.prod g

Tactic:
exact fold_congr

Premises used: Finset.fold_congr
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
h : ∀ x ∈ s, f x = 1
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1

Tactic:
calc
  ∏ x ∈ s, f x = ∏ _x ∈ s, 1 := prod_congr rfl h
  _ = 1 := prod_const_one

Premises used: Trans.trans, Finset.prod_congr, Finset.prod_const_one, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
inst_1 : Subsingleton.{u_4 + 1} Mˣ
empty : Eq.{u_4 + 1} (α := M) (∏ i ∈ ∅, f i) 1 ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i = 1
cons :
  ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
    (Eq.{u_4 + 1} (α := M) (∏ i ∈ s, f i) 1 ↔ ∀ i ∈ s, f i = 1) →
      (Eq.{u_4 + 1} (α := M) (∏ i ∈ Finset.cons a s h, f i) 1 ↔ ∀ i ∈ Finset.cons a s h, f i = 1)
⊢ Eq.{u_4 + 1} (α := M) (∏ i ∈ s, f i) 1 ↔ ∀ i ∈ s, f i = 1

Tactic:
induction s using Finset.cons_induction
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
inst_1 : Subsingleton.{u_4 + 1} Mˣ
⊢ Eq.{u_4 + 1} (α := M) (∏ i ∈ ∅, f i) 1 ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i = 1

Tactic:
simp [*]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
inst_1 : Subsingleton.{u_4 + 1} Mˣ
a : ι
s_1 : Finset ι
h : a ∉ s_1
h_1 : Eq.{u_4 + 1} (α := M) (∏ i ∈ s_1, f i) 1 ↔ ∀ i ∈ s_1, f i = 1
⊢ Eq.{u_4 + 1} (α := M) (∏ i ∈ cons a s_1 h, f i) 1 ↔ ∀ i ∈ cons a s_1 h, f i = 1

Tactic:
simp [*]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst : CommMonoid M
f : ι → M
h : Disjoint s₁ s₂
⊢ ∏ x ∈ s₁.disjUnion s₂ h, f x = HMul.hMul (α := M) (∏ x ∈ s₁, f x) (∏ x ∈ s₂, f x)

Tactic:
Eq.trans ?_ (fold_disjUnion h)

Premises used: Finset.fold_disjUnion, Eq.trans
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst : CommMonoid M
f : ι → M
h : Disjoint s₁ s₂
refine :
  ∏ x ∈ s₁.disjUnion s₂ h, f x =
    fold (fun (x1 x2 : M) ↦ x1 * x2) (HMul.hMul (α := M) 1 1) (fun (x : ι) ↦ f x) (s₁.disjUnion s₂ h)
⊢ ∏ x ∈ s₁.disjUnion s₂ h, f x = HMul.hMul (α := M) (∏ x ∈ s₁, f x) (∏ x ∈ s₂, f x)

Tactic:
refine Eq.trans ?_ (fold_disjUnion h)

Premises used: Finset.fold_disjUnion, Eq.trans
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst : CommMonoid M
f : ι → M
h : Disjoint s₁ s₂
rw :
  Eq.{u_4 + 1} (α := M) (∏ x ∈ s₁.disjUnion s₂ h, f x)
    (fold (fun (x1 x2 : M) ↦ x1 * x2) 1 (fun (x : ι) ↦ f x) (s₁.disjUnion s₂ h))
⊢ ∏ x ∈ s₁.disjUnion s₂ h, f x =
    fold (fun (x1 x2 : M) ↦ x1 * x2) (HMul.hMul (α := M) 1 1) (fun (x : ι) ↦ f x) (s₁.disjUnion s₂ h)

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst : CommMonoid M
f : ι → M
h : Disjoint s₁ s₂
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s₁.disjUnion s₂ h, f x)
    (fold (fun (x1 x2 : M) ↦ x1 * x2) 1 (fun (x : ι) ↦ f x) (s₁.disjUnion s₂ h))

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
f : ι → M
s : Finset κ
t : κ → Finset ι
h : (↑s : Set κ).PairwiseDisjoint t
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.disjiUnion t h, f x) (∏ i ∈ s, ∏ x ∈ t i, f x)

Tactic:
Eq.trans ?_ (fold_disjiUnion h)

Premises used: Finset.fold_disjiUnion, Eq.trans
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
f : ι → M
s : Finset κ
t : κ → Finset ι
h : (↑s : Set κ).PairwiseDisjoint t
refine :
  Eq.{u_4 + 1} (α := M) (∏ x ∈ s.disjiUnion t h, f x)
    (fold (fun (x1 x2 : M) ↦ x1 * x2) (fold (fun (x1 x2 : M) ↦ x1 * x2) 1 (fun (i : κ) ↦ 1) s) (fun (x : ι) ↦ f x)
      (s.disjiUnion t h))
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.disjiUnion t h, f x) (∏ i ∈ s, ∏ x ∈ t i, f x)

Tactic:
refine Eq.trans ?_ (fold_disjiUnion h)

Premises used: Finset.fold_disjiUnion, Eq.trans
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
f : ι → M
s : Finset κ
t : κ → Finset ι
h : (↑s : Set κ).PairwiseDisjoint t
dsimp :
  Eq.{u_4 + 1} (α := M)
    (Multiset.foldr (fun (x1 x2 : M) ↦ x1 * x2) 1
      (Multiset.map (fun (x : ι) ↦ f x) (s.val.bind fun (a : κ) ↦ (t a).val)))
    (Multiset.foldr (fun (x1 x2 : M) ↦ x1 * x2)
      (Multiset.foldr (fun (x1 x2 : M) ↦ x1 * x2) 1 (Multiset.map (fun (i : κ) ↦ 1) s.val))
      (Multiset.map (fun (x : ι) ↦ f x) (s.val.bind fun (a : κ) ↦ (t a).val)))
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.disjiUnion t h, f x)
    (fold (fun (x1 x2 : M) ↦ x1 * x2) (fold (fun (x1 x2 : M) ↦ x1 * x2) 1 (fun (i : κ) ↦ 1) s) (fun (x : ι) ↦ f x)
      (s.disjiUnion t h))

Tactic:
dsimp [Finset.prod, Multiset.prod, Multiset.fold, Finset.disjUnion, Finset.fold]

Premises used: Multiset.prod, Finset.fold, Finset.disjUnion, Finset.prod, Multiset.fold
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
f : ι → M
s : Finset κ
t : κ → Finset ι
h : (↑s : Set κ).PairwiseDisjoint t
e_b : Eq.{u_4 + 1} (α := M) 1 (Multiset.foldr (fun (x1 x2 : M) ↦ x1 * x2) 1 (Multiset.map (fun (i : κ) ↦ 1) s.val))
⊢ Eq.{u_4 + 1} (α := M)
    (Multiset.foldr (fun (x1 x2 : M) ↦ x1 * x2) 1
      (Multiset.map (fun (x : ι) ↦ f x) (s.val.bind fun (a : κ) ↦ (t a).val)))
    (Multiset.foldr (fun (x1 x2 : M) ↦ x1 * x2)
      (Multiset.foldr (fun (x1 x2 : M) ↦ x1 * x2) 1 (Multiset.map (fun (i : κ) ↦ 1) s.val))
      (Multiset.map (fun (x : ι) ↦ f x) (s.val.bind fun (a : κ) ↦ (t a).val)))

Tactic:
congr
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
f : ι → M
s : Finset κ
t : κ → Finset ι
h : (↑s : Set κ).PairwiseDisjoint t
⊢ Eq.{u_4 + 1} (α := M) 1 (Multiset.foldr (fun (x1 x2 : M) ↦ x1 * x2) 1 (Multiset.map (fun (i : κ) ↦ 1) s.val))

Tactic:
prod_const_one.symm

Premises used: Multiset.prod, Finset.prod, Finset.prod_const_one, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
f : ι → M
s : Finset κ
t : κ → Finset ι
h : (↑s : Set κ).PairwiseDisjoint t
⊢ Eq.{u_4 + 1} (α := M) 1 (Multiset.foldr (fun (x1 x2 : M) ↦ x1 * x2) 1 (Multiset.map (fun (i : κ) ↦ 1) s.val))

Tactic:
exact prod_const_one.symm

Premises used: Finset.prod_const_one, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
⊢ HMul.hMul (α := M) (∏ x ∈ s₁ ∪ s₂, f x) (∏ x ∈ s₁ ∩ s₂, f x) = HMul.hMul (α := M) (∏ x ∈ s₁, f x) (∏ x ∈ s₂, f x)

Tactic:
fold_union_inter

Premises used: Multiset.prod, Finset.prod, Finset.fold_union_inter
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
h : Disjoint s₁ s₂
rw : ∏ x ∈ s₁ ∪ s₂, f x = HMul.hMul (α := M) (∏ x ∈ s₁ ∪ s₂, f x) (∏ x ∈ ∅, f x)
⊢ ∏ x ∈ s₁ ∪ s₂, f x = HMul.hMul (α := M) (∏ x ∈ s₁, f x) (∏ x ∈ s₂, f x)

Tactic:
rw [← prod_union_inter, disjoint_iff_inter_eq_empty.mp h]

Premises used: Finset.disjoint_iff_inter_eq_empty, Iff.mp, Finset.prod_union_inter
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
h : Disjoint s₁ s₂
⊢ ∏ x ∈ s₁ ∪ s₂, f x = HMul.hMul (α := M) (∏ x ∈ s₁ ∪ s₂, f x) (∏ x ∈ ∅, f x)

Tactic:
(mul_one _).symm

Premises used: Multiset.foldr, Multiset.prod, Finset.prod, mul_one, Eq.symm, List.foldr
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
h : Disjoint s₁ s₂
⊢ ∏ x ∈ s₁ ∪ s₂, f x = HMul.hMul (α := M) (∏ x ∈ s₁ ∪ s₂, f x) (∏ x ∈ ∅, f x)

Tactic:
exact (mul_one _).symm

Premises used: mul_one, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : (x : ι) → Decidable ¬p x
f : ι → M
have : ∀ (this : DecidableEq ι), HMul.hMul (α := M) (∏ x ∈ s with p x, f x) (∏ x ∈ s with ¬p x, f x) = ∏ x ∈ s, f x
⊢ HMul.hMul (α := M) (∏ x ∈ s with p x, f x) (∏ x ∈ s with ¬p x, f x) = ∏ x ∈ s, f x

Tactic:
have := Classical.decEq ι
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : (x : ι) → Decidable ¬p x
f : ι → M
this : DecidableEq ι
rw : Eq.{u_4 + 1} (α := M) (∏ x ∈ filter p s ∪ {a ∈ s | ¬p a}, f x) (∏ x ∈ s, f x)
rw₁ rw₂ : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ s, f x)
⊢ HMul.hMul (α := M) (∏ x ∈ s with p x, f x) (∏ x ∈ s with ¬p x, f x) = ∏ x ∈ s, f x

Tactic:
rw [← prod_union (disjoint_filter_filter_not s s p), filter_union_filter_not_eq]

Premises used: Finset.prod_union, Finset.disjoint_filter_filter_not, Finset.filter_union_filter_not_eq
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : (x : ι) → Decidable ¬p x
f : ι → M
rw : HMul.hMul (α := M) (∏ x ∈ s with p x, f x) (∏ x ∈ s with ¬p x, f x) = ∏ x ∈ s, f x
rw₁ rw₂ : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ s, f x)
⊢ HMul.hMul (α := M) (∏ x ∈ s with ¬p x, f x) (∏ x ∈ s with p x, f x) = ∏ x ∈ s, f x

Tactic:
rw [mul_comm, prod_filter_mul_prod_filter_not]

Premises used: mul_comm, Finset.prod_filter_mul_prod_filter_not
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
p q : ι → Prop
inst_1 : DecidablePred p
inst_2 : DecidablePred q
rw : Eq.{u_4 + 1} (α := M) (∏ x ∈ s with Xor (p x) (q x), f x) (∏ x ∈ s with p x ∧ ¬q x ∨ q x ∧ ¬p x, f x)
⊢ ∏ x ∈ s with Xor (p x) (q x), f x = HMul.hMul (α := M) (∏ x ∈ s with p x ∧ ¬q x, f x) (∏ x ∈ s with q x ∧ ¬p x, f x)

Tactic:
rw [← prod_union (disjoint_filter_and_not_filter _ _), ← filter_or]

Premises used: Finset.prod_union, Finset.filter_or, Finset.disjoint_filter_and_not_filter
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
p q : ι → Prop
inst_1 : DecidablePred p
inst_2 : DecidablePred q
classical : Eq.{u_4 + 1} (α := M) (∏ x ∈ s with Xor (p x) (q x), f x) (∏ x ∈ s with p x ∧ ¬q x ∨ q x ∧ ¬p x, f x)
⊢ ∏ x ∈ s with Xor (p x) (q x), f x = HMul.hMul (α := M) (∏ x ∈ s with p x ∧ ¬q x, f x) (∏ x ∈ s with q x ∧ ¬p x, f x)

Tactic:
classical rw [← prod_union (disjoint_filter_and_not_filter _ _), ← filter_or]

Premises used: Finset.prod_union, Finset.filter_or, Finset.disjoint_filter_and_not_filter
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
p q : ι → Prop
inst_1 : DecidablePred p
inst_2 : DecidablePred q
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s with Xor (p x) (q x), f x) (∏ x ∈ s with p x ∧ ¬q x ∨ q x ∧ ¬p x, f x)

Tactic:
simp only [Xor]

Premises used: Xor
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Fintype ι
s t : Finset ι
h : IsCompl s t
f : ι → M
rw : Eq.{u_4 + 1} (α := M) (∏ x ∈ ⊤, f x) (∏ i : ι, f i)
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.disjUnion t ⋯, f x) (∏ i : ι, f i)

Tactic:
rw [Finset.disjUnion_eq_union, ← Finset.sup_eq_union, h.sup_eq_top]

Premises used: IsCompl.sup_eq_top, Finset.disjUnion_eq_union, Finset.sup_eq_union
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Fintype ι
s t : Finset ι
h : IsCompl s t
f : ι → M
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ ⊤, f x) (∏ i : ι, f i)

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Fintype ι
s t : Finset ι
h : IsCompl s t
f : ι → M
classical : Eq.{u_4 + 1} (α := M) (∏ x ∈ s ∪ t, f x) (∏ i : ι, f i)
classical₁ : Eq.{u_4 + 1} (α := M) (∏ x ∈ s ⊔ t, f x) (∏ i : ι, f i)
classical₂ classical₃ classical₄ classical₅ : Eq.{u_4 + 1} (α := M) (∏ x ∈ ⊤, f x) (∏ i : ι, f i)
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.disjUnion t ⋯, f x) (∏ i : ι, f i)

Tactic:
classical rw [Finset.disjUnion_eq_union, ← Finset.sup_eq_union, h.sup_eq_top]; rfl

Premises used: IsCompl.sup_eq_top, Finset.disjUnion_eq_union, Finset.sup_eq_union
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Fintype ι
inst_2 : DecidableEq ι
s : Finset ι
f : ι → M
⊢ HMul.hMul (α := M) (∏ i ∈ s, f i) (∏ i ∈ sᶜ, f i) = ∏ i : ι, f i

Tactic:
IsCompl.prod_mul_prod isCompl_compl f

Premises used: IsCompl.prod_mul_prod
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Fintype ι
inst_2 : DecidableEq ι
s : Finset ι
f : ι → M
⊢ HMul.hMul (α := M) (∏ i ∈ sᶜ, f i) (∏ i ∈ s, f i) = ∏ i : ι, f i

Tactic:
(@isCompl_compl _ s _).symm.prod_mul_prod f

Premises used: IsCompl.prod_mul_prod, isCompl_compl, IsCompl.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
h : s₁ ⊆ s₂
rw : Eq.{u_4 + 1} (α := M) (∏ x ∈ s₂ \ s₁ ∪ s₁, f x) (∏ x ∈ s₂, f x)
rw₁ rw₂ : Eq.{u_4 + 1} (α := M) (∏ x ∈ s₂, f x) (∏ x ∈ s₂, f x)
⊢ HMul.hMul (α := M) (∏ x ∈ s₂ \ s₁, f x) (∏ x ∈ s₁, f x) = ∏ x ∈ s₂, f x

Tactic:
rw [← prod_union sdiff_disjoint, sdiff_union_of_subset h]

Premises used: Finset.prod_union, Finset.sdiff_union_of_subset, Finset.sdiff_disjoint
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst : CommMonoid M
f g : ι → M
inst_1 : DecidableEq ι
h : s₁ ⊆ s₂
hg : ∀ x ∈ s₂ \ s₁, g x = 1
hfg : ∀ x ∈ s₁, f x = g x
rw : Eq.{u_4 + 1} (α := M) (∏ i ∈ s₁, f i) (∏ x ∈ s₁, g x)
⊢ Eq.{u_4 + 1} (α := M) (∏ i ∈ s₁, f i) (∏ i ∈ s₂, g i)

Tactic:
rw [← prod_sdiff h, prod_eq_one hg, one_mul]

Premises used: Finset.prod_eq_one, Finset.prod_sdiff, one_mul
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst : CommMonoid M
f g : ι → M
inst_1 : DecidableEq ι
h : s₁ ⊆ s₂
hg : ∀ x ∈ s₂ \ s₁, g x = 1
hfg : ∀ x ∈ s₁, f x = g x
⊢ Eq.{u_4 + 1} (α := M) (∏ i ∈ s₁, f i) (∏ x ∈ s₁, g x)

Tactic:
prod_congr rfl hfg

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst : CommMonoid M
f g : ι → M
inst_1 : DecidableEq ι
h : s₁ ⊆ s₂
hg : ∀ x ∈ s₂ \ s₁, g x = 1
hfg : ∀ x ∈ s₁, f x = g x
⊢ Eq.{u_4 + 1} (α := M) (∏ i ∈ s₁, f i) (∏ x ∈ s₁, g x)

Tactic:
exact prod_congr rfl hfg

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst : CommMonoid M
f : ι → M
h : s₁ ⊆ s₂
hf : ∀ x ∈ s₂, x ∉ s₁ → f x = 1
this : DecidableEq ι
⊢ ∀ x ∈ s₂ \ s₁, f x = 1

Tactic:
simpa
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι ⊕ κ → M
rw :
  HMul.hMul (α := M) (∏ x ∈ s, f ((Embedding.inl : (a : ι) → ι ⊕ κ) x))
      (∏ x ∈ t, f ((Embedding.inr : (a : κ) → ι ⊕ κ) x)) =
    HMul.hMul (α := M) (∏ x ∈ s, f (Sum.inl x)) (∏ x ∈ t, f (Sum.inr x))
⊢ ∏ x ∈ s.disjSum t, f x = HMul.hMul (α := M) (∏ x ∈ s, f (Sum.inl x)) (∏ x ∈ t, f (Sum.inr x))

Tactic:
rw [← map_inl_disjUnion_map_inr, prod_disjUnion, prod_map, prod_map]

Premises used: Finset.map_inl_disjUnion_map_inr, Finset.prod_disjUnion, Finset.prod_map
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι ⊕ κ → M
⊢ HMul.hMul (α := M) (∏ x ∈ s, f ((Embedding.inl : (a : ι) → ι ⊕ κ) x))
      (∏ x ∈ t, f ((Embedding.inr : (a : κ) → ι ⊕ κ) x)) =
    HMul.hMul (α := M) (∏ x ∈ s, f (Sum.inl x)) (∏ x ∈ t, f (Sum.inr x))

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
s : Finset (ι ⊕ κ)
f : ι ⊕ κ → M
rw :
  ∏ x ∈ s.toLeft.disjSum s.toRight, f x =
    HMul.hMul (α := M) (∏ x ∈ (s.toLeft.disjSum s.toRight).toLeft, f (Sum.inl x))
      (∏ x ∈ (s.toLeft.disjSum s.toRight).toRight, f (Sum.inr x))
rw₁ :
  HMul.hMul (α := M) (∏ x ∈ s.toLeft, f (Sum.inl x)) (∏ x ∈ s.toRight, f (Sum.inr x)) =
    HMul.hMul (α := M) (∏ x ∈ (s.toLeft.disjSum s.toRight).toLeft, f (Sum.inl x))
      (∏ x ∈ (s.toLeft.disjSum s.toRight).toRight, f (Sum.inr x))
rw₂ :
  HMul.hMul (α := M) (∏ x ∈ s.toLeft, f (Sum.inl x)) (∏ x ∈ s.toRight, f (Sum.inr x)) =
    HMul.hMul (α := M) (∏ x ∈ s.toLeft, f (Sum.inl x)) (∏ x ∈ (s.toLeft.disjSum s.toRight).toRight, f (Sum.inr x))
rw₃ rw₄ :
  HMul.hMul (α := M) (∏ x ∈ s.toLeft, f (Sum.inl x)) (∏ x ∈ s.toRight, f (Sum.inr x)) =
    HMul.hMul (α := M) (∏ x ∈ s.toLeft, f (Sum.inl x)) (∏ x ∈ s.toRight, f (Sum.inr x))
⊢ ∏ x ∈ s, f x = HMul.hMul (α := M) (∏ x ∈ s.toLeft, f (Sum.inl x)) (∏ x ∈ s.toRight, f (Sum.inr x))

Tactic:
rw [← Finset.toLeft_disjSum_toRight (u := s), Finset.prod_disjSum, Finset.toLeft_disjSum,
    Finset.toRight_disjSum]

Premises used: Finset.toRight_disjSum, Finset.toLeft_disjSum, Finset.prod_disjSum, Finset.toLeft_disjSum_toRight
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
⊢ ∏ x ∈ s.disjSum t, Sum.elim f g x = HMul.hMul (α := M) (∏ x ∈ s, f x) (∏ x ∈ t, g x)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s : Set κ).PairwiseDisjoint t
rw : Eq.{u_4 + 1} (α := M) (∏ x ∈ s.disjiUnion t hs, f x) (∏ x ∈ s, ∏ i ∈ t x, f i)
rw₁ rw₂ : Eq.{u_4 + 1} (α := M) (∏ i ∈ s, ∏ x ∈ t i, f x) (∏ x ∈ s, ∏ i ∈ t x, f i)
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.biUnion t, f x) (∏ x ∈ s, ∏ i ∈ t x, f i)

Tactic:
rw [← disjiUnion_eq_biUnion _ _ hs, prod_disjiUnion]

Premises used: Finset.disjiUnion_eq_biUnion, Finset.prod_disjiUnion
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι → κ
he : Set.InjOn e (↑s : Set ι)
hest : Set.MapsTo e (↑s : Set ι) (↑t : Set κ)
h' : ∀ i ∈ t, i ∉ e '' (↑s : Set ι) → g i = 1
h : ∀ i ∈ s, f i = g (e i)
⊢ Set.SurjOn e (↑s : Set ι) (↑(image e s) : Set κ)

Tactic:
simp [Set.surjOn_image]

Premises used: Set.surjOn_image
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι → κ
he : Set.InjOn e (↑s : Set ι)
hest : Set.MapsTo e (↑s : Set ι) (↑t : Set κ)
h' : ∀ i ∈ t, i ∉ e '' (↑s : Set ι) → g i = 1
h : ∀ i ∈ s, f i = g (e i)
⊢ ∀ x ∈ t, x ∉ image e s → g x = 1

Tactic:
simpa using h'
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι → κ
he : Set.InjOn e (↑s : Set ι)
hest : Set.MapsTo e (↑s : Set ι) (↑t : Set κ)
h' : ∀ i ∈ t, i ∉ e '' (↑s : Set ι) → g i = 1
h : ∀ i ∈ s, f i = g (e i)
⊢ Eq.{u_4 + 1} (α := M) (∏ i ∈ s, f i) (∏ j ∈ t, g j)

Tactic:
exact (prod_nbij e (fun a ↦ mem_image_of_mem e) he (by simp [Set.surjOn_image]) h).trans <|
    prod_subset (image_subset_iff.2 hest) <| by simpa using h'

Premises used: Iff.mpr, Finset.prod_subset, Finset.image_subset_iff, Finset.mem_image_of_mem, Finset.prod_nbij, Eq.trans
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι → κ
he : Set.InjOn e (↑s : Set ι)
hest : Set.MapsTo e (↑s : Set ι) (↑t : Set κ)
h' : ∀ i ∈ t, i ∉ e '' (↑s : Set ι) → g i = 1
h : ∀ i ∈ s, f i = g (e i)
⊢ Eq.{u_4 + 1} (α := M) (∏ i ∈ s, f i) (∏ j ∈ t, g j)

Tactic:
classical
  exact (prod_nbij e (fun a ↦ mem_image_of_mem e) he (by simp [Set.surjOn_image]) h).trans <|
    prod_subset (image_subset_iff.2 hest) <| by simpa using h'

Premises used: Iff.mpr, Finset.prod_subset, Finset.image_subset_iff
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : ι → M
h : Set.PairwiseDisjoint.{u_1, u_2} (α := Finset ι) (↑t : Set κ) fun (j : κ) ↦ {i ∈ s | g i = j}
⊢ Eq.{u_4 + 1} (α := M) (∏ j ∈ t, ∏ i ∈ s with g i = j, f i) (∏ i ∈ s with g i ∈ t, f i)

Tactic:
rw [← prod_disjiUnion, disjiUnion_filter_eq]

Premises used: Finset.disjiUnion_filter_eq, Finset.prod_disjiUnion
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : ι → M
x' : κ
hx : x' ∈ (↑t : Set κ)
y' : κ
hy : y' ∈ (↑t : Set κ)
hne : x' ≠ y'
h : ∀ ⦃a : ι⦄, a ∈ s ∧ g a = x' → ¬(a ∈ s ∧ g a = y')
⊢ onFun.{u_2 + 1, u_1 + 1, 1} (β := Finset ι) Disjoint (fun (j : κ) ↦ {i ∈ s | g i = j}) x' y'

Tactic:
simp_rw [disjoint_left, mem_filter]

Premises used: Finset.mem_filter, Finset.disjoint_left
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : ι → M
i : ι
left : i ∈ s
hx : g i ∈ (↑t : Set κ)
left_1 : i ∈ s
hy : g i ∈ (↑t : Set κ)
hne : g i ≠ g i
⊢ False

Tactic:
hne rfl

Premises used: rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : ι → M
i : ι
left : i ∈ s
hx : g i ∈ (↑t : Set κ)
left_1 : i ∈ s
hy : g i ∈ (↑t : Set κ)
hne : g i ≠ g i
⊢ False

Tactic:
exact hne rfl

Premises used: rfl