awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
x : α
contrapose! : f x = 1 ∧ g x = 1 → f x * g x = 1
⊢ f x * g x ≠ 1 → f x ≠ 1 ∨ g x ≠ 1

Tactic:
contrapose!
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f g : α → M
hf_1 : HasFiniteMulSupport f
hg_1 : HasFiniteMulSupport g
x : α
hf : f x = 1
hg : g x = 1
⊢ f x * g x = 1

Tactic:
simp [hf, hg]
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
rw :
  ∏ᶠ (i : α), f i * g i =
    HMul.hMul (α := M) (∏ i ∈ Finite.toFinset (s := mulSupport f) hf ∪ Finite.toFinset (s := mulSupport g) hg, f i)
      (∏ᶠ (i : α), g i)
rw₁ : Finset α
rw₂ :
  ∏ᶠ (i : α), f i * g i =
    HMul.hMul (α := M) (∏ i ∈ Finite.toFinset (s := mulSupport f) hf ∪ Finite.toFinset (s := mulSupport g) hg, f i)
      (∏ i ∈ Finite.toFinset (s := mulSupport f) hf ∪ Finite.toFinset (s := mulSupport g) hg, g i)
rw₃ rw₄ : Finset α
rw₅ rw₆ rw₇ :
  Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i * g i)
    (∏ x ∈ Finite.toFinset (s := mulSupport f) hf ∪ Finite.toFinset (s := mulSupport g) hg, f x * g x)
rw₈ :
  (mulSupport.{u_1, u_5} (M := M) fun (i : α) ↦ f i * g i) ⊆
    (↑(Finite.toFinset (s := mulSupport f) hf ∪ Finite.toFinset (s := mulSupport g) hg) : Set α)
rw₉ rw₁₀ : ∀ (x : α), f x * g x ≠ 1 → f x ≠ 1 ∨ g x ≠ 1
rw₁₁ : ∀ (x : α), f x = 1 ∧ g x = 1 → f x * g x = 1
rw₁₂ : ∀ (x : α) (hf : f x = 1) (hg : g x = 1), f x * g x = 1
⊢ ∏ᶠ (i : α), f i * g i = HMul.hMul (α := M) (∏ᶠ (i : α), f i) (∏ᶠ (i : α), g i)

Tactic:
classical
    rw [finprod_eq_prod_of_mulSupport_toFinset_subset f hf Finset.subset_union_left,
      finprod_eq_prod_of_mulSupport_toFinset_subset g hg Finset.subset_union_right, ←
      Finset.prod_mul_distrib]
    refine finprod_eq_prod_of_mulSupport_subset _ ?_
    simp only [Finset.coe_union, Finite.coe_toFinset, mulSupport_subset_iff,
      mem_union, mem_mulSupport]
    intro x
    contrapose!
    rintro ⟨hf, hg⟩
    simp [hf, hg]

Premises used: Set.mem_union, Finset.prod_mul_distrib, Function.mem_mulSupport, Function.mulSupport_subset_iff, Set.Finite.coe_toFinset, finprod_eq_prod_of_mulSupport_subset, Finset.coe_union
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
G : Type u_4
inst : DivisionCommMonoid G
f g : α → G
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
⊢ ∏ᶠ (i : α), f i / g i = HDiv.hDiv (α := G) (∏ᶠ (i : α), f i) (∏ᶠ (i : α), g i)

Tactic:
simp only [div_eq_mul_inv, finprod_mul_distrib hf <| hg.fun_inv, finprod_inv_distrib]

Premises used: finprod_mul_distrib, div_eq_mul_inv, Function.HasFiniteMulSupport.fun_inv, finprod_inv_distrib
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f g : α → M
s : Set α
hf : (s ∩ mulSupport f).Finite
hg : (s ∩ mulSupport g).Finite
⊢ (mulSupport (s.mulIndicator f)).Finite

Tactic:
rw [← mulSupport_mulIndicator] at hf hg

Premises used: Set.mulSupport_mulIndicator
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f g : α → M
s : Set α
hf : (s ∩ mulSupport f).Finite
hg : (s ∩ mulSupport g).Finite
hf₁ : (mulSupport (s.mulIndicator f)).Finite
⊢ (mulSupport (s.mulIndicator g)).Finite

Tactic:
rw [← mulSupport_mulIndicator] at hf hg

Premises used: Set.mulSupport_mulIndicator
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f g : α → M
s : Set α
hf : (mulSupport (s.mulIndicator f)).Finite
hg : (mulSupport (s.mulIndicator g)).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i * g i = HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ s), g i)

Tactic:
simp only [finprod_mem_def, mulIndicator_mul, finprod_mul_distrib hf hg]

Premises used: Set.mulIndicator_mul, finprod_mul_distrib, finprod_mem_def
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
s : Set α
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), 1) 1

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
hf : EqOn f 1 s
rw : Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ s), 1)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) 1

Tactic:
rw [← finprod_mem_one s]

Premises used: finprod_mem_one
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
hf : EqOn f 1 s
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ s), 1)

Tactic:
finprod_mem_congr rfl hf

Premises used: finprod_mem_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
hf : EqOn f 1 s
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ s), 1)

Tactic:
exact finprod_mem_congr rfl hf

Premises used: finprod_mem_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
h : Ne.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) 1
by_contra! : ∀ (h' : ∀ (x : α) (_ : x ∈ s), f x = 1), False
⊢ ∃ x ∈ s, f x ≠ 1

Tactic:
by_contra! h'
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
h : Ne.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) 1
h' : ∀ (x : α) (_ : x ∈ s), f x = 1
⊢ False

Tactic:
h (finprod_mem_of_eqOn_one h')

Premises used: finprod_mem_of_eqOn_one
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
h : Ne.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) 1
h' : ∀ (x : α) (_ : x ∈ s), f x = 1
⊢ False

Tactic:
exact h (finprod_mem_of_eqOn_one h')

Premises used: finprod_mem_of_eqOn_one
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f g : α → M
s : Set α
hs : s.Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i * g i = HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ s), g i)

Tactic:
finprod_mem_mul_distrib' (hs.inter_of_left _) (hs.inter_of_left _)

Premises used: Set.Finite.inter_of_left, finprod_mem_mul_distrib'
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
N : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
f : α → M
g : M →* N
hf : HasFiniteMulSupport f
⊢ Eq.{u_6 + 1} (α := N) ((g : (a : M) → N) (∏ᶠ (i : α), f i) : N) (∏ᶠ (i : α), (g : (a : M) → N) (f i) : N)

Tactic:
g.map_finprod_plift f <| hf.preimage Equiv.plift.injective.injOn

Premises used: Function.Injective.injOn, Equiv.plift, Equiv.injective, MonoidHom.map_finprod_plift, Set.Finite.preimage
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
N : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
f : α → M
G : Type u_7
inst_2 : FunLike G M N
inst_3 : MonoidHomClass G M N
g : G
hf : HasFiniteMulSupport f
⊢ Eq.{u_6 + 1} (α := N) ((g : (a : M) → N) (∏ᶠ (i : α), f i) : N) (∏ᶠ (i : α), (g : (a : M) → N) (f i) : N)

Tactic:
(g : M →* N).map_finprod hf

Premises used: MonoidHomClass.toMonoidHom, MonoidHom.map_finprod
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
hf : HasFiniteMulSupport f
n : ℕ
⊢ HPow.hPow (α := M) (∏ᶠ (i : α), f i) n = ∏ᶠ (i : α), f i ^ n

Tactic:
(powMonoidHom n).map_finprod hf

Premises used: powMonoidHom, MonoidHom.map_finprod
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
ι : Type u_3
R : Type u_7
M : Type u_8
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : ι → R
hf : HasFiniteSupport f
x : M
⊢ HSMul.hSMul.{u_7, u_8, u_8} (α := R) (∑ᶠ (i : ι), f i) x = ∑ᶠ (i : ι), f i • x

Tactic:
((smulAddHom R M).flip x).map_finsum hf

Premises used: AddMonoidHom.map_finsum, AddMonoidHom.flip, smulAddHom, DFunLike.coe
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
ι : Type u_3
R : Type u_7
M : Type u_8
inst : AddCommMonoid M
inst_1 : DistribSMul R M
c : R
f : ι → M
hf : HasFiniteSupport f
⊢ HSMul.hSMul (β := M) c (∑ᶠ (i : ι), f i) = ∑ᶠ (i : ι), c • f i

Tactic:
(DistribSMul.toAddMonoidHom M c).map_finsum hf

Premises used: AddMonoidHom.map_finsum, DistribSMul.toAddMonoidHom
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
N : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
s : Set α
f : α → M
g : M →* N
h₀ : (s ∩ mulSupport f).Finite
rw :
  Eq.{u_6 + 1} (α := N) (∏ᶠ (i : α), (g : (a : M) → N) (∏ᶠ (_ : i ∈ s), f i))
    (∏ᶠ (i : α) (_ : i ∈ s), (g : (a : M) → N) (f i))
rw₁ : HasFiniteMulSupport.{u_1, u_5} (M := M) fun (j : α) ↦ ∏ᶠ (_ : j ∈ s), f j
⊢ Eq.{u_6 + 1} (α := N) ((g : (a : M) → N) (∏ᶠ (j : α) (_ : j ∈ s), f j) : N)
    (∏ᶠ (i : α) (_ : i ∈ s), (g : (a : M) → N) (f i) : N)

Tactic:
rw [g.map_finprod]

Premises used: MonoidHom.map_finprod
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
N : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
s : Set α
f : α → M
g : M →* N
h₀ : (s ∩ mulSupport f).Finite
⊢ Eq.{u_6 + 1} (α := N) (∏ᶠ (i : α), (g : (a : M) → N) (∏ᶠ (_ : i ∈ s), f i))
    (∏ᶠ (i : α) (_ : i ∈ s), (g : (a : M) → N) (f i))

Tactic:
simp only [g.map_finprod_Prop]

Premises used: MonoidHom.map_finprod_Prop
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
N : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
s : Set α
f : α → M
g : M →* N
h₀ : (s ∩ mulSupport f).Finite
⊢ HasFiniteMulSupport.{u_1, u_5} (M := M) fun (j : α) ↦ ∏ᶠ (_ : j ∈ s), f j

Tactic:
simpa only [finprod_eq_mulIndicator_apply, HasFiniteMulSupport, mulSupport_mulIndicator]

Premises used: Set.mulSupport_mulIndicator, finprod_eq_mulIndicator_apply, Function.HasFiniteMulSupport
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
N : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
s : Set α
f : α → M
g : M →* N
hs : s.Finite
⊢ Eq.{u_6 + 1} (α := N) ((g : (a : M) → N) (∏ᶠ (j : α) (_ : j ∈ s), f j) : N)
    (∏ᶠ (i : α) (_ : i ∈ s), (g : (a : M) → N) (f i) : N)

Tactic:
g.map_finprod_mem' (hs.inter_of_left _)

Premises used: MonoidHom.map_finprod_mem', Set.Finite.inter_of_left
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
N : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
g : M ≃* N
f : α → M
s : Set α
hs : s.Finite
⊢ Eq.{u_6 + 1} (α := N) ((g : (a : M) → N) (∏ᶠ (i : α) (_ : i ∈ s), f i) : N)
    (∏ᶠ (i : α) (_ : i ∈ s), (g : (a : M) → N) (f i) : N)

Tactic:
g.toMonoidHom.map_finprod_mem f hs

Premises used: MonoidHom.map_finprod_mem, MulEquiv.toMonoidHom
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
G : Type u_4
s : Set α
inst : DivisionCommMonoid G
f : α → G
hs : s.Finite
⊢ Eq.{u_4 + 1} (α := G) (∏ᶠ (x : α) (_ : x ∈ s), (f x)⁻¹) (∏ᶠ (x : α) (_ : x ∈ s), f x)⁻¹

Tactic:
((MulEquiv.inv G).map_finprod_mem f hs).symm

Premises used: MulEquiv.inv, Eq.symm, MulEquiv.map_finprod_mem
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
G : Type u_4
s : Set α
inst : DivisionCommMonoid G
f g : α → G
hs : s.Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i / g i = HDiv.hDiv (α := G) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ s), g i)

Tactic:
simp only [div_eq_mul_inv, finprod_mem_mul_distrib hs, finprod_mem_inv_distrib g hs]

Premises used: div_eq_mul_inv, finprod_mem_mul_distrib, finprod_mem_inv_distrib
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : Membership.mem (γ := Set α) ∅ i), f i) 1

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
h : Ne.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) 1
⊢ s.Nonempty

Tactic:
nonempty_iff_ne_empty.2 fun h' => h <| h'.symm ▸ finprod_mem_empty

Premises used: Iff.mpr, Eq.rec, finprod_mem_empty, Set.nonempty_iff_ne_empty, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ s.Finite

Tactic:
hs
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
hs : s.Finite
ht : t.Finite
lift :
  ∀ (s : Finset α),
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α) ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α) ∩ t), f i) =
      HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
⊢ HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)

Tactic:
lift s to Finset α using hs

Premises used: Finset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
t : Set α
ht : t.Finite
s : Finset α
⊢ t.Finite

Tactic:
ht
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
t : Set α
ht : t.Finite
s : Finset α
lift :
  ∀ (t : Finset α),
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α) ∪ (↑t : Set α)), f i)
        (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α) ∩ (↑t : Set α)), f i) =
      HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)), f i) (∏ᶠ (i : α) (_ : i ∈ (↑t : Set α)), f i)
⊢ HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α) ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α) ∩ t), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)

Tactic:
lift t to Finset α using ht

Premises used: Finset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Finset α
rw :
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑(s ∪ t) : Set α)), f i) (∏ᶠ (i : α) (_ : i ∈ (↑(s ∩ t) : Set α)), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)), f i) (∏ᶠ (i : α) (_ : i ∈ (↑t : Set α)), f i)
⊢ HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α) ∪ (↑t : Set α)), f i)
      (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α) ∩ (↑t : Set α)), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)), f i) (∏ᶠ (i : α) (_ : i ∈ (↑t : Set α)), f i)

Tactic:
rw [← Finset.coe_union, ← Finset.coe_inter]

Premises used: Finset.coe_inter, Finset.coe_union
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Finset α
⊢ HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑(s ∪ t) : Set α)), f i) (∏ᶠ (i : α) (_ : i ∈ (↑(s ∩ t) : Set α)), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)), f i) (∏ᶠ (i : α) (_ : i ∈ (↑t : Set α)), f i)

Tactic:
simp only [finprod_mem_coe_finset, Finset.prod_union_inter]

Premises used: finprod_mem_coe_finset, Finset.prod_union_inter
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Finset α
rw :
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑(s ∪ t) : Set α)), f i)
      (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α) ∩ (↑t : Set α)), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)), f i) (∏ᶠ (i : α) (_ : i ∈ (↑t : Set α)), f i)
rw₁ rw₂ rw₃ :
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑(s ∪ t) : Set α)), f i) (∏ᶠ (i : α) (_ : i ∈ (↑(s ∩ t) : Set α)), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)), f i) (∏ᶠ (i : α) (_ : i ∈ (↑t : Set α)), f i)
⊢ HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α) ∪ (↑t : Set α)), f i)
      (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α) ∩ (↑t : Set α)), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)), f i) (∏ᶠ (i : α) (_ : i ∈ (↑t : Set α)), f i)

Tactic:
classical
    rw [← Finset.coe_union, ← Finset.coe_inter]
    simp only [finprod_mem_coe_finset, Finset.prod_union_inter]

Premises used: finprod_mem_coe_finset, Finset.coe_inter, Finset.prod_union_inter, Finset.coe_union
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
rw :
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ t ∩ mulSupport f), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i)
      (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f ∩ (t ∩ mulSupport f)), f i)
⊢ HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)

Tactic:
rw [← finprod_mem_inter_mulSupport f s, ← finprod_mem_inter_mulSupport f t, ←
    finprod_mem_union_inter hs ht, ← union_inter_distrib_right, finprod_mem_inter_mulSupport, ←
    finprod_mem_inter_mulSupport f (s ∩ t)]

Premises used: Inter.inter, finprod_mem_union_inter, Set.union_inter_distrib_right, finprod_mem_inter_mulSupport
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
rw :
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ t ∩ mulSupport f), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i)
      (∏ᶠ (i : α) (_ : i ∈ t ∩ (s ∩ mulSupport f ∩ mulSupport f)), f i)
rw₁ :
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ (t ∩ mulSupport f)), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i)
      (∏ᶠ (i : α) (_ : i ∈ t ∩ (s ∩ mulSupport f ∩ mulSupport f)), f i)
rw₂ :
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ (t ∩ mulSupport f)), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i)
      (∏ᶠ (i : α) (_ : i ∈ t ∩ (s ∩ (mulSupport f ∩ mulSupport f))), f i)
rw₃ :
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ (t ∩ mulSupport f)), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ t ∩ (s ∩ mulSupport f)), f i)
rw₄ rw₅ :
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ t ∩ (s ∩ mulSupport f)), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ t ∩ (s ∩ mulSupport f)), f i)
⊢ HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ t ∩ mulSupport f), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i)
      (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f ∩ (t ∩ mulSupport f)), f i)

Tactic:
rw [inter_left_comm, inter_assoc, inter_assoc, inter_self, inter_left_comm]

Premises used: Set.inter_self, Set.inter_left_comm, Set.inter_assoc
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
hst : Disjoint s t
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
rw :
  ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i)
rw₁ :
  ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : Membership.mem (γ := Set α) ∅ i), f i)
rw₂ : ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) 1
rw₃ rw₄ : Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i)
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)

Tactic:
rw [← finprod_mem_union_inter' hs ht, disjoint_iff_inter_eq_empty.1 hst, finprod_mem_empty,
    mul_one]

Premises used: finprod_mem_empty, finprod_mem_union_inter', Set.disjoint_iff_inter_eq_empty, Iff.mp, mul_one
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
hst : Disjoint s t
hs : s.Finite
ht : t.Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)

Tactic:
finprod_mem_union' hst (hs.inter_of_left _) (ht.inter_of_left _)

Premises used: finprod_mem_union', Set.Finite.inter_of_left
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
hst : Disjoint (s ∩ mulSupport f) (t ∩ mulSupport f)
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
rw :
  ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
rw₁ :
  ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i) (∏ᶠ (i : α) (_ : i ∈ t ∩ mulSupport f), f i)
rw₂ :
  Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i)
    (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f ∪ t ∩ mulSupport f), f i)
rw₃ : Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ (s ∪ t) ∩ mulSupport f), f i)
rw₄ rw₅ : Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i)
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)

Tactic:
rw [← finprod_mem_inter_mulSupport f s, ← finprod_mem_inter_mulSupport f t, ←
    finprod_mem_union hst hs ht, ← union_inter_distrib_right, finprod_mem_inter_mulSupport]

Premises used: finprod_mem_union, Set.union_inter_distrib_right, finprod_mem_inter_mulSupport
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
rw : ∏ᶠ (i : α) (_ : i ∈ (↑{a} : Set α)), f i = f a
rw₁ : ∏ i ∈ {a}, f i = f a
rw₂ rw₃ : f a = f a
⊢ ∏ᶠ (i : α) (_ : Membership.mem (γ := Set α) {a} i), f i = f a

Tactic:
rw [← Finset.coe_singleton, finprod_mem_coe_finset, Finset.prod_singleton]

Premises used: Finset.coe_singleton, Finset.prod_singleton, finprod_mem_coe_finset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
⊢ ∏ᶠ (i : α) (_ : i = a), f i = f a

Tactic:
finprod_mem_singleton

Premises used: Set.Mem, setOf, Set.singleton, finprod_mem_singleton
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
⊢ ∏ᶠ (i : α) (_ : a = i), f i = f a

Tactic:
simp [@eq_comm _ a]

Premises used: eq_comm
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
a : α
s : Set α
f : α → M
h : a ∉ s
hs : (s ∩ mulSupport f).Finite
rw : Disjoint {a} s
rw₁ : ({a} ∩ mulSupport f).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ insert a s), f i = f a * ∏ᶠ (i : α) (_ : i ∈ s), f i

Tactic:
rw [insert_eq, finprod_mem_union' _ _ hs, finprod_mem_singleton]

Premises used: finprod_mem_union', Set.insert_eq, finprod_mem_singleton
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
a : α
s : Set α
f : α → M
h : a ∉ s
hs : (s ∩ mulSupport f).Finite
rwa rwa₁ rwa₂ rwa₃ : a ∉ s
⊢ Disjoint {a} s

Tactic:
rwa [disjoint_singleton_left]

Premises used: Set.disjoint_singleton_left
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
a : α
s : Set α
f : α → M
h : a ∉ s
hs : (s ∩ mulSupport f).Finite
⊢ ({a} ∩ mulSupport f).Finite

Tactic:
(finite_singleton a).inter_of_left _

Premises used: Set.Finite.inter_of_left, Set.finite_singleton
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
a : α
s : Set α
f : α → M
h : a ∉ s
hs : (s ∩ mulSupport f).Finite
⊢ ({a} ∩ mulSupport f).Finite

Tactic:
exact (finite_singleton a).inter_of_left _

Premises used: Set.Finite.inter_of_left, Set.finite_singleton
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
a : α
s : Set α
f : α → M
h : a ∉ s
hs : s.Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ insert a s), f i = f a * ∏ᶠ (i : α) (_ : i ∈ s), f i

Tactic:
finprod_mem_insert' f h <| hs.inter_of_left _

Premises used: Set.Finite.inter_of_left, finprod_mem_insert'
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
s : Set α
h : a ∉ s → f a = 1
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ insert a s), f i) (∏ᶠ (i : α) (_ : i ∈ s), f i)

Tactic:
finprod_mem_inter_mulSupport_eq' _ _ _ fun x hx => ⟨?_, Or.inr⟩

Premises used: finprod_mem_inter_mulSupport_eq', Iff.intro, Or.inr