awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
s : Set α
f : α → R
r : R
e_f : ∀ (a : α), (∑ᶠ (_ : a ∈ s), f a) * r = ∑ᶠ (_ : a ∈ s), f a * r
⊢ Eq (α := α → R) (fun (a : α) ↦ (∑ᶠ (_ : a ∈ s), f a) * r) fun (a : α) ↦ ∑ᶠ (_ : a ∈ s), f a * r

Tactic:
ext a
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
s : Set α
f : α → R
r : R
a : α
pos : ∀ (h : a ∈ s), (∑ᶠ (_ : a ∈ s), f a) * r = ∑ᶠ (_ : a ∈ s), f a * r
neg : ∀ (h : a ∉ s), (∑ᶠ (_ : a ∈ s), f a) * r = ∑ᶠ (_ : a ∈ s), f a * r
⊢ (∑ᶠ (_ : a ∈ s), f a) * r = ∑ᶠ (_ : a ∈ s), f a * r

Tactic:
by_cases h : a ∈ s
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
s : Set α
f : α → R
r : R
a : α
h : a ∈ s
⊢ (∑ᶠ (_ : a ∈ s), f a) * r = ∑ᶠ (_ : a ∈ s), f a * r

Tactic:
simp_all
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
s : Set α
f : α → R
r : R
a : α
h : a ∉ s
⊢ (∑ᶠ (_ : a ∈ s), f a) * r = ∑ᶠ (_ : a ∈ s), f a * r

Tactic:
simp_all
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
N : Type u_6
inst : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : HasFiniteMulSupport f
a : α
⊢ Eq.{u_6 + 1} (α := N) (1 a) 1

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
N : Type u_6
inst : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : HasFiniteMulSupport f
a : α
funProp : Eq.{u_6 + 1} (α := N) (1 a) 1
⊢ HasFiniteMulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a

Tactic:
fun_prop (disch := simp)
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
N : Type u_6
inst : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : HasFiniteMulSupport f
a : α
⊢ HasFiniteMulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a

Tactic:
have hf' : HasFiniteMulSupport fun i ↦ f i a := by fun_prop (disch := simp)
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
N : Type u_6
inst : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : HasFiniteMulSupport f
a : α
hf' : HasFiniteMulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a
simp :
  Eq.{u_6 + 1} (α := N) (∏ c ∈ Finite.toFinset (s := mulSupport f) ⋯, f c a)
    (∏ c ∈ Finite.toFinset (s := mulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a) ⋯, f c a)
⊢ Eq.{u_6 + 1} (α := N) ((∏ᶠ (i : ι), f i) a) (∏ᶠ (i : ι), f i a)

Tactic:
simp only [finprod_def, dif_pos, hf, hf', Finset.prod_apply]

Premises used: Finset.prod_apply, dif_pos, finprod_def
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
N : Type u_6
inst : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : HasFiniteMulSupport f
a : α
hf' : HasFiniteMulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a
symm :
  Eq.{u_6 + 1} (α := N) (∏ c ∈ Finite.toFinset (s := mulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a) ⋯, f c a)
    (∏ c ∈ Finite.toFinset (s := mulSupport f) ⋯, f c a)
⊢ Eq.{u_6 + 1} (α := N) (∏ c ∈ Finite.toFinset (s := mulSupport f) ⋯, f c a)
    (∏ c ∈ Finite.toFinset (s := mulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a) ⋯, f c a)

Tactic:
symm
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
N : Type u_6
inst : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : HasFiniteMulSupport f
a : α
hf' : HasFiniteMulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a
h : Finite.toFinset (s := mulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a) ⋯ ⊆ Finite.toFinset (s := mulSupport f) ⋯
hf₁ :
  ∀ x ∈ Finite.toFinset (s := mulSupport f) ⋯,
    x ∉ Finite.toFinset (s := mulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a) ⋯ → f x a = 1
⊢ Eq.{u_6 + 1} (α := N) (∏ c ∈ Finite.toFinset (s := mulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a) ⋯, f c a)
    (∏ c ∈ Finite.toFinset (s := mulSupport f) ⋯, f c a)

Tactic:
apply Finset.prod_subset

Premises used: Finset.prod_subset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
N : Type u_6
inst : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : HasFiniteMulSupport f
a : α
hf' : HasFiniteMulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a
⊢ Finite.toFinset (s := mulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a) ⋯ ⊆ Finite.toFinset (s := mulSupport f) ⋯

Tactic:
aesop
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
N : Type u_6
inst : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : HasFiniteMulSupport f
a : α
hf' : HasFiniteMulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a
⊢ ∀ x ∈ Finite.toFinset (s := mulSupport f) ⋯,
    x ∉ Finite.toFinset (s := mulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a) ⋯ → f x a = 1

Tactic:
aesop
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
N : Type u_6
inst : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : HasFiniteMulSupport f
a : α
have : HasFiniteMulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a
have₁ :
  ∀ (hf' : HasFiniteMulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a),
    Eq.{u_6 + 1} (α := N) ((∏ᶠ (i : ι), f i) a) (∏ᶠ (i : ι), f i a)
have₂ : HasFiniteMulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a
have₃ have₄ :
  ∀ (hf' : HasFiniteMulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a),
    Eq.{u_6 + 1} (α := N) ((∏ᶠ (i : ι), f i) a) (∏ᶠ (i : ι), f i a)
have₅ :
  ∀ (hf' : HasFiniteMulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a),
    Eq.{u_6 + 1} (α := N) (∏ c ∈ Finite.toFinset (s := mulSupport f) ⋯, f c a)
      (∏ c ∈ Finite.toFinset (s := mulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a) ⋯, f c a)
have₆ :
  ∀ (hf' : HasFiniteMulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a),
    Eq.{u_6 + 1} (α := N) (∏ c ∈ Finite.toFinset (s := mulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a) ⋯, f c a)
      (∏ c ∈ Finite.toFinset (s := mulSupport f) ⋯, f c a)
⊢ Eq.{u_6 + 1} (α := N) ((∏ᶠ (i : ι), f i) a) (∏ᶠ (i : ι), f i a)

Tactic:
classical
  have hf' : HasFiniteMulSupport fun i ↦ f i a := by fun_prop (disch := simp)
  simp only [finprod_def, dif_pos, hf, hf', Finset.prod_apply]
  symm
  apply Finset.prod_subset <;> aesop

Premises used: Finset.prod_apply, dif_pos, Finset.prod_subset, finprod_def
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq β
s : Finset α
f : α → M
g : α → β
simp : (mulSupport.{u_2, u_5} (M := M) fun (b : β) ↦ ∏ a ∈ s with g a = b, f a) ⊆ g '' (↑s : Set α)
⊢ (mulSupport.{u_2, u_5} (M := M) fun (b : β) ↦ ∏ a ∈ s with g a = b, f a) ⊆ (↑(image g s) : Set β)

Tactic:
simp only [Finset.coe_image]

Premises used: Finset.coe_image
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq β
s : Finset α
f : α → M
g : α → β
b : β
h : Membership.mem (γ := Set β) (mulSupport.{u_2, u_5} (M := M) fun (b : β) ↦ ∏ a ∈ s with g a = b, f a) b
this : {a ∈ s | g a = b}.Nonempty
⊢ b ∈ g '' (↑s : Set α)

Tactic:
simpa only [fiber_nonempty_iff_mem_image, Finset.mem_image, exists_prop]

Premises used: Finset.mem_image, Finset.fiber_nonempty_iff_mem_image, exists_prop
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq β
s : Finset α
f : α → M
g : α → β
b : β
h : Membership.mem (γ := Set β) (mulSupport.{u_2, u_5} (M := M) fun (b : β) ↦ ∏ a ∈ s with g a = b, f a) b
suffices : {a ∈ s | g a = b}.Nonempty
⊢ b ∈ g '' (↑s : Set α)

Tactic:
suffices {a ∈ s | g a = b}.Nonempty by
    simpa only [fiber_nonempty_iff_mem_image, Finset.mem_image, exists_prop]
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq β
s : Finset α
f : α → M
g : α → β
b : β
h : Membership.mem (γ := Set β) (mulSupport.{u_2, u_5} (M := M) fun (b : β) ↦ ∏ a ∈ s with g a = b, f a) b
⊢ {a ∈ s | g a = b}.Nonempty

Tactic:
Finset.nonempty_of_prod_ne_one h

Premises used: Finset.nonempty_of_prod_ne_one
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq β
s : Finset α
f : α → M
g : α → β
b : β
h : Membership.mem (γ := Set β) (mulSupport.{u_2, u_5} (M := M) fun (b : β) ↦ ∏ a ∈ s with g a = b, f a) b
⊢ {a ∈ s | g a = b}.Nonempty

Tactic:
exact Finset.nonempty_of_prod_ne_one h

Premises used: Finset.nonempty_of_prod_ne_one
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
inst_2 : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
⊢ ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f

Tactic:
Finset.prod_nbij' (fun b ↦ (a, b)) Prod.snd ?_ ?_ ?_ ?_ ?_

Premises used: Prod.mk, Finset.prod_nbij', Prod.snd
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
inst_2 : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
refine_1 : ∀ a_1 ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), (fun (b : β) ↦ (a, b)) a_1 ∈ {x ∈ s | x.1 = a}
refine_2 : ∀ a_1 ∈ {x ∈ s | x.1 = a}, a_1.2 ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})
refine_3 : ∀ a_1 ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), ((fun (b : β) ↦ (a, b)) a_1).2 = a_1
refine_4 : ∀ a_1 ∈ {x ∈ s | x.1 = a}, (fun (b : β) ↦ (a, b)) a_1.2 = a_1
refine_5 : ∀ a_1 ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, a_1) = f ((fun (b : β) ↦ (a, b)) a_1)
⊢ ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f

Tactic:
refine Finset.prod_nbij' (fun b ↦ (a, b)) Prod.snd ?_ ?_ ?_ ?_ ?_

Premises used: Prod.mk, Finset.prod_nbij', Prod.snd
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
inst_2 : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
⊢ ∀ a_1 ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), (fun (b : β) ↦ (a, b)) a_1 ∈ {x ∈ s | x.1 = a}

Tactic:
aesop
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
inst_2 : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
⊢ ∀ a_1 ∈ {x ∈ s | x.1 = a}, a_1.2 ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})

Tactic:
aesop
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
inst_2 : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
⊢ ∀ a_1 ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), ((fun (b : β) ↦ (a, b)) a_1).2 = a_1

Tactic:
aesop
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
inst_2 : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
⊢ ∀ a_1 ∈ {x ∈ s | x.1 = a}, (fun (b : β) ↦ (a, b)) a_1.2 = a_1

Tactic:
aesop
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
inst_2 : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
⊢ ∀ a_1 ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, a_1) = f ((fun (b : β) ↦ (a, b)) a_1)

Tactic:
aesop
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
inst_2 : DecidableEq β
s : Finset (α × β)
f : α × β → M
⊢ ∀ (a : α), ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f

Tactic:
have (a : _) :
      ∏ i ∈ (s.filter fun ab => Prod.fst ab = a).image Prod.snd, f (a, i) =
        (s.filter (Prod.fst · = a)).prod f := by
    refine Finset.prod_nbij' (fun b ↦ (a, b)) Prod.snd ?_ ?_ ?_ ?_ ?_ <;> aesop
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
inst_2 : DecidableEq β
s : Finset (α × β)
f : α × β → M
this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f
rw :
  Eq.{u_5 + 1} (α := M) (∏ i ∈ s, f i)
    (∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b))
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab)
    (∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b))

Tactic:
rw [finprod_mem_finset_eq_prod]

Premises used: finprod_mem_finset_eq_prod
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
inst_2 : DecidableEq β
s : Finset (α × β)
f : α × β → M
this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f
simp_rw : Eq.{u_5 + 1} (α := M) (∏ i ∈ s, f i) (∏ᶠ (a : α), {ab ∈ s | ab.1 = a}.prod f)
⊢ Eq.{u_5 + 1} (α := M) (∏ i ∈ s, f i)
    (∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b))

Tactic:
simp_rw [finprod_mem_finset_eq_prod, this]

Premises used: finprod_mem_finset_eq_prod
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
inst_2 : DecidableEq β
s : Finset (α × β)
f : α × β → M
this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f
rw : ∀ i ∈ s, i.1 ∈ Finset.image Prod.fst s
⊢ Eq.{u_5 + 1} (α := M) (∏ i ∈ s, f i) (∏ᶠ (a : α), {ab ∈ s | ab.1 = a}.prod f)

Tactic:
rw [finprod_eq_prod_of_mulSupport_subset _
      (s.mulSupport_of_fiberwise_prod_subset_image f Prod.fst),
    ← Finset.prod_fiberwise_of_maps_to (t := Finset.image Prod.fst s) _ f]

Premises used: Finset.prod_fiberwise_of_maps_to, Prod.fst, Finset.mulSupport_of_fiberwise_prod_subset_image, finprod_eq_prod_of_mulSupport_subset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
inst_2 : DecidableEq β
s : Finset (α × β)
f : α × β → M
this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f
simp : ∀ i ∈ s, ∃ a ∈ s, a.1 = i.1
⊢ ∀ i ∈ s, i.1 ∈ Finset.image Prod.fst s

Tactic:
simp only [Finset.mem_image]

Premises used: Finset.mem_image
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
inst_2 : DecidableEq β
s : Finset (α × β)
f : α × β → M
this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f
⊢ ∀ i ∈ s, ∃ a ∈ s, a.1 = i.1

Tactic:
fun x hx => ⟨x, hx, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
inst_2 : DecidableEq β
s : Finset (α × β)
f : α × β → M
this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f
⊢ ∀ i ∈ s, ∃ a ∈ s, a.1 = i.1

Tactic:
exact fun x hx => ⟨x, hx, rfl⟩
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Finset (α × β)
f : α × β → M
rw :
  Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b))
    (∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b))
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab) (∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b))

Tactic:
rw [finprod_mem_finset_product']

Premises used: finprod_mem_finset_product'
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Finset (α × β)
f : α × β → M
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b))
    (∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b))

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Finset (α × β)
f : α × β → M
rw rw₁ rw₂ :
  Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b))
    (∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b))
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab) (∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b))

Tactic:
classical
    rw [finprod_mem_finset_product']
    simp

Premises used: finprod_mem_finset_product'
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
γ : Type u_7
s : Finset (α × β × γ)
f : α × β × γ → M
rw :
  Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (b : β × γ) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b))
    (∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c))
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (abc : α × β × γ) (_ : abc ∈ s), f abc)
    (∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c))

Tactic:
rw [finprod_mem_finset_product']

Premises used: finprod_mem_finset_product'
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
γ : Type u_7
s : Finset (α × β × γ)
f : α × β × γ → M
simp_rw :
  Eq.{u_5 + 1} (α := M)
    (∏ᶠ (a : α) (a_1 : β) (b : γ) (_ :
      b ∈ Finset.image Prod.snd ({ab ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}) | ab.1 = a_1})), f (a, a_1, b))
    (∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c))
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (b : β × γ) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b))
    (∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c))

Tactic:
simp_rw [finprod_mem_finset_product']

Premises used: finprod_mem_finset_product'
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
γ : Type u_7
s : Finset (α × β × γ)
f : α × β × γ → M
⊢ Eq.{u_5 + 1} (α := M)
    (∏ᶠ (a : α) (a_1 : β) (b : γ) (_ :
      b ∈ Finset.image Prod.snd ({ab ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}) | ab.1 = a_1})), f (a, a_1, b))
    (∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c))

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
γ : Type u_7
s : Finset (α × β × γ)
f : α × β × γ → M
rw rw₁ rw₂ :
  Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (b : β × γ) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b))
    (∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c))
rw₃ :
  Eq.{u_5 + 1} (α := M)
    (∏ᶠ (a : α) (a_1 : β) (b : γ) (_ :
      b ∈ Finset.image Prod.snd ({ab ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}) | ab.1 = a_1})), f (a, a_1, b))
    (∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c))
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (abc : α × β × γ) (_ : abc ∈ s), f abc)
    (∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c))

Tactic:
classical
    rw [finprod_mem_finset_product']
    simp_rw [finprod_mem_finset_product']
    simp

Premises used: finprod_mem_finset_product'
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α × β → M
hf : HasFiniteMulSupport f
⊢ ∀ (a : α × β), ∏ᶠ (_ : a ∈ Finite.toFinset (s := mulSupport f) hf), f a = f a

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α × β → M
hf : HasFiniteMulSupport f
⊢ ∀ (a : α × β), ∏ᶠ (_ : a ∈ Finite.toFinset (s := mulSupport f) hf), f a = f a

Tactic:
have h₁ : ∀ a, ∏ᶠ _ : a ∈ hf.toFinset, f a = f a := by simp
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α × β → M
hf : HasFiniteMulSupport f
h₁ : ∀ (a : α × β), ∏ᶠ (_ : a ∈ Finite.toFinset (s := mulSupport f) hf), f a = f a
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α × β), f a) (∏ᶠ (a : α × β) (_ : a ∈ Finite.toFinset (s := mulSupport f) hf), f a)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α × β → M
hf : HasFiniteMulSupport f
h₁ : ∀ (a : α × β), ∏ᶠ (_ : a ∈ Finite.toFinset (s := mulSupport f) hf), f a = f a
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α × β), f a) (∏ᶠ (a : α × β) (_ : a ∈ Finite.toFinset (s := mulSupport f) hf), f a)

Tactic:
have h₂ : ∏ᶠ a, f a = ∏ᶠ (a) (_ : a ∈ hf.toFinset), f a := by simp
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α × β → M
hf : HasFiniteMulSupport f
h₁ : ∀ (a : α × β), ∏ᶠ (_ : a ∈ Finite.toFinset (s := mulSupport f) hf), f a = f a
h₂ : Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α × β), f a) (∏ᶠ (a : α × β) (_ : a ∈ Finite.toFinset (s := mulSupport f) hf), f a)
simp_rw :
  Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α × β) (_ : a ∈ Finite.toFinset (s := mulSupport f) hf), f a)
    (∏ᶠ (a : α) (b : β), f (a, b))
simp_rw₁ :
  Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ Finite.toFinset (s := mulSupport f) hf), f (a, b))
    (∏ᶠ (a : α) (b : β), f (a, b))
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (ab : α × β), f ab) (∏ᶠ (a : α) (b : β), f (a, b))

Tactic:
simp_rw [h₂, finprod_mem_finset_product, h₁]

Premises used: finprod_mem_finset_product
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
γ : Type u_7
f : α × β × γ → M
h : HasFiniteMulSupport f
rw : Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (b : β × γ), f (a, b)) (∏ᶠ (a : α) (b : β) (c : γ), f (a, b, c))
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (abc : α × β × γ), f abc) (∏ᶠ (a : α) (b : β) (c : γ), f (a, b, c))

Tactic:
rw [finprod_curry f h]

Premises used: finprod_curry
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
γ : Type u_7
f : α × β × γ → M
h : HasFiniteMulSupport f
e_f : Eq (α := α → M) (fun (a : α) ↦ ∏ᶠ (b : β × γ), f (a, b)) fun (a : α) ↦ ∏ᶠ (b : β) (c : γ), f (a, b, c)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (b : β × γ), f (a, b)) (∏ᶠ (a : α) (b : β) (c : γ), f (a, b, c))

Tactic:
congr
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
γ : Type u_7
f : α × β × γ → M
h : HasFiniteMulSupport f
e_f : ∀ (a : α), Eq.{u_5 + 1} (α := M) (∏ᶠ (b : β × γ), f (a, b)) (∏ᶠ (b : β) (c : γ), f (a, b, c))
⊢ Eq (α := α → M) (fun (a : α) ↦ ∏ᶠ (b : β × γ), f (a, b)) fun (a : α) ↦ ∏ᶠ (b : β) (c : γ), f (a, b, c)

Tactic:
ext a
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
γ : Type u_7
f : α × β × γ → M
h : HasFiniteMulSupport f
a : α
e_f : HasFiniteMulSupport (M := M) fun (b : β × γ) ↦ f (a, b)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (b : β × γ), f (a, b)) (∏ᶠ (b : β) (c : γ), f (a, b, c))

Tactic:
rw [finprod_curry]

Premises used: finprod_curry
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
γ : Type u_7
f : α × β × γ → M
h : HasFiniteMulSupport f
a : α
⊢ HasFiniteMulSupport (M := M) fun (b : β × γ) ↦ f (a, b)

Tactic:
simp [h]
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
f : (a : α) → a ∈ s → M
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (h : a ∈ s), f a h) (∏ᶠ (a : α) (_ : a ∈ s), if h' : a ∈ s then f a h' else 1)

Tactic:
finprod_congr fun _ => finprod_congr fun ha => (dif_pos ha).symm

Premises used: dif_pos, finprod_congr, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α → β
hf : Injective f
inst_1 : DecidablePred fun (x : β) ↦ x ∈ range f
g : α → M
simp_rw :
  Eq.{u_5 + 1} (α := M) (∏ᶠ (b : β) (h : b ∈ range f), g (Classical.choose (p := fun (x : α) ↦ f x = b) h))
    (∏ᶠ (a : α), g a)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (b : β), if h : b ∈ range f then g (Classical.choose (p := fun (x : α) ↦ f x = b) h) else 1)
    (∏ᶠ (a : α), g a)

Tactic:
simp_rw [← finprod_eq_dif]

Premises used: finprod_eq_dif