awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α → β → M
s : Finset α
t : Finset β
⊢ Eq.{u_5 + 1} (α := M) (∏ i ∈ s, ∏ i_1 ∈ t, f i i_1) (∏ i ∈ t, ∏ i_1 ∈ s, f i_1 i)

Tactic:
exact Finset.prod_comm

Premises used: Finset.prod_comm
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ x ∈ s, p (f x)
⊢ p (∏ᶠ (i : α) (_ : i ∈ s), f i)

Tactic:
finprod_induction _ hp₀ hp₁ fun x => finprod_induction _ hp₀ hp₁ <| hp₂ x

Premises used: finprod_induction
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
R : Type u_7
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
p : α → Prop
f : α → R
hf : ∀ (x : α), p x → 0 ≤ f x
⊢ LE.le.{u_7} (α := R) 0 (∏ᶠ (x : α) (_ : p x), f x)

Tactic:
finprod_nonneg fun x => finprod_nonneg <| hf x

Premises used: finprod_nonneg
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_7
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
i : α
f : α → M
hf : HasFiniteMulSupport f
h : ∀ (j : α), 1 ≤ f j
⊢ f i ≤ ∏ j ∈ insert i (Finite.toFinset (s := mulSupport f) hf), f j

Tactic:
Finset.single_le_prod' (fun j _ => h j) (Finset.mem_insert_self _ _)

Premises used: Finset.mem_insert_self, Finset.single_le_prod'
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_7
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
i : α
f : α → M
hf : HasFiniteMulSupport f
h : ∀ (j : α), 1 ≤ f j
⊢ Eq.{u_7 + 1} (α := M) (∏ j ∈ insert i (Finite.toFinset (s := mulSupport f) hf), f j) (∏ᶠ (j : α), f j)

Tactic:
(finprod_eq_prod_of_mulSupport_toFinset_subset _ hf (Finset.subset_insert _ _)).symm

Premises used: finprod_eq_prod_of_mulSupport_toFinset_subset, Finset.subset_insert, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_7
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
i : α
f : α → M
hf : HasFiniteMulSupport f
h : ∀ (j : α), 1 ≤ f j
⊢ f i ≤ ∏ᶠ (j : α), f j

Tactic:
calc
      f i ≤ ∏ j ∈ insert i hf.toFinset, f j :=
        Finset.single_le_prod' (fun j _ => h j) (Finset.mem_insert_self _ _)
      _ = ∏ᶠ j, f j :=
        (finprod_eq_prod_of_mulSupport_toFinset_subset _ hf (Finset.subset_insert _ _)).symm

Premises used: Finset.mem_insert_self, Finset.single_le_prod', finprod_eq_prod_of_mulSupport_toFinset_subset, Insert.insert, Set.Finite.toFinset, Finset.subset_insert, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_7
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
i : α
f : α → M
hf : HasFiniteMulSupport f
h : ∀ (j : α), 1 ≤ f j
⊢ f i ≤ ∏ᶠ (j : α), f j

Tactic:
classical calc
      f i ≤ ∏ j ∈ insert i hf.toFinset, f j :=
        Finset.single_le_prod' (fun j _ => h j) (Finset.mem_insert_self _ _)
      _ = ∏ᶠ j, f j :=
        (finprod_eq_prod_of_mulSupport_toFinset_subset _ hf (Finset.subset_insert _ _)).symm
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M₀ : Type u_7
inst : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : HasFiniteMulSupport f
⊢ Nontrivial M₀

Tactic:
nontriviality
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M₀ : Type u_7
inst : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : HasFiniteMulSupport f
h : Nontrivial M₀
rw : Eq.{u_7 + 1} (α := M₀) (∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i) 0
⊢ Eq.{u_7 + 1} (α := M₀) (∏ᶠ (x : α), f x) 0

Tactic:
rw [finprod_eq_prod f hf]

Premises used: finprod_eq_prod
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M₀ : Type u_7
inst : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : HasFiniteMulSupport f
h : Nontrivial M₀
⊢ Eq.{u_7 + 1} (α := M₀) (∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i) 0

Tactic:
Finset.prod_eq_zero (hf.mem_toFinset.2 ?_) hx

Premises used: Iff.mpr, Set.Finite.mem_toFinset, Finset.prod_eq_zero
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M₀ : Type u_7
inst : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : HasFiniteMulSupport f
h : Nontrivial M₀
refine : x ∈ mulSupport f
⊢ Eq.{u_7 + 1} (α := M₀) (∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i) 0

Tactic:
refine Finset.prod_eq_zero (hf.mem_toFinset.2 ?_) hx

Premises used: Iff.mpr, Set.Finite.mem_toFinset, Finset.prod_eq_zero
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M₀ : Type u_7
inst : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : HasFiniteMulSupport f
h : Nontrivial M₀
⊢ x ∈ mulSupport f

Tactic:
simp [hx]
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a b
rw :
  Subset.{u_1} (α := Set α) (mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ ∏ b ∈ s, f a b)
    (⋃ i ∈ (↑s : Set β), mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i)
⊢ (mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ ∏ b ∈ s, f a b) ⊆
    (↑(Finite.toFinset (s := ⋃ i ∈ (↑s : Set β), mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) ⋯) : Set α)

Tactic:
rw [Finite.coe_toFinset]

Premises used: Set.Finite.coe_toFinset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a b
x : α
hx : Membership.mem (γ := Set α) (mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ ∏ b ∈ s, f a b) x
simp : ∃ i ∈ s, ¬f x i = 1
⊢ Membership.mem (γ := Set α) (⋃ i ∈ (↑s : Set β), mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) x

Tactic:
simp only [exists_prop, mem_iUnion, Ne, mem_mulSupport, Finset.mem_coe]

Premises used: Set.mem_iUnion, Function.mem_mulSupport, Ne, exists_prop, Finset.mem_coe
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a b
x : α
hx : Membership.mem (γ := Set α) (mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ ∏ b ∈ s, f a b) x
contrapose! : ∀ (hx : ∀ (i : β) (_ : i ∈ s), f x i = 1), x ∉ mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ ∏ b ∈ s, f a b
⊢ ∃ i ∈ s, ¬f x i = 1

Tactic:
contrapose! hx
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a b
x : α
hx : ∀ (i : β) (_ : i ∈ s), f x i = 1
rw : ¬Ne.{u_5 + 1} (α := M) (∏ b ∈ s, f x b) 1
rw₁ : Eq.{u_5 + 1} (α := M) (∏ b ∈ s, f x b) 1
rw₂ : Eq.{u_5 + 1} (α := M) (∏ x ∈ s, 1) 1
rw₃ rw₄ : Eq.{u_5 + 1} (α := M) 1 1
⊢ x ∉ mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ ∏ b ∈ s, f a b

Tactic:
rw [mem_mulSupport, not_not, Finset.prod_congr rfl hx, Finset.prod_const_one]

Premises used: Classical.not_not, Function.mem_mulSupport, Finset.prod_congr, Finset.prod_const_one, rfl
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a b
⊢ (mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ ∏ b ∈ s, f a b) ⊆
    (↑(Finite.toFinset (s := ⋃ i ∈ (↑s : Set β), mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) ⋯) : Set α)

Tactic:
have hU :
    (mulSupport fun a => ∏ b ∈ s, f a b) ⊆
      (s.finite_toSet.biUnion fun b hb => h b (Finset.mem_coe.1 hb)).toFinset := by
    rw [Finite.coe_toFinset]
    intro x hx
    simp only [exists_prop, mem_iUnion, Ne, mem_mulSupport, Finset.mem_coe]
    contrapose! hx
    rw [mem_mulSupport, not_not, Finset.prod_congr rfl hx, Finset.prod_const_one]
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a b
hU :
  (mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ ∏ b ∈ s, f a b) ⊆
    (↑(Finite.toFinset (s := ⋃ i ∈ (↑s : Set β), mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) ⋯) : Set α)
rw :
  Eq.{u_5 + 1} (α := M)
    (∏ y ∈ s,
      ∏ x ∈ Finite.toFinset (s := ⋃ i ∈ (↑s : Set β), mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) ⋯, f x y)
    (∏ b ∈ s, ∏ᶠ (a : α), f a b)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α), ∏ b ∈ s, f a b) (∏ b ∈ s, ∏ᶠ (a : α), f a b)

Tactic:
rw [finprod_eq_prod_of_mulSupport_subset _ hU, Finset.prod_comm]

Premises used: Finset.prod_comm, 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
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a b
hU :
  (mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ ∏ b ∈ s, f a b) ⊆
    (↑(Finite.toFinset (s := ⋃ i ∈ (↑s : Set β), mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) ⋯) : Set α)
⊢ Eq.{u_5 + 1} (α := M)
    (∏ y ∈ s,
      ∏ x ∈ Finite.toFinset (s := ⋃ i ∈ (↑s : Set β), mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) ⋯, f x y)
    (∏ b ∈ s, ∏ᶠ (a : α), f a b)

Tactic:
Finset.prod_congr rfl fun b hb => (finprod_eq_prod_of_mulSupport_subset _ ?_).symm

Premises used: Finset.prod_congr, Eq.symm, finprod_eq_prod_of_mulSupport_subset, rfl
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a b
hU :
  (mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ ∏ b ∈ s, f a b) ⊆
    (↑(Finite.toFinset (s := ⋃ i ∈ (↑s : Set β), mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) ⋯) : Set α)
refine :
  ∀ (b : β) (hb : b ∈ s),
    (mulSupport.{u_1, u_5} (M := M) fun (x : α) ↦ f x b) ⊆
      (↑(Finite.toFinset (s := ⋃ i ∈ (↑s : Set β), mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) ⋯) : Set α)
⊢ Eq.{u_5 + 1} (α := M)
    (∏ y ∈ s,
      ∏ x ∈ Finite.toFinset (s := ⋃ i ∈ (↑s : Set β), mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) ⋯, f x y)
    (∏ b ∈ s, ∏ᶠ (a : α), f a b)

Tactic:
refine Finset.prod_congr rfl fun b hb => (finprod_eq_prod_of_mulSupport_subset _ ?_).symm

Premises used: Finset.prod_congr, Eq.symm, finprod_eq_prod_of_mulSupport_subset, rfl
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a b
hU :
  (mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ ∏ b ∈ s, f a b) ⊆
    (↑(Finite.toFinset (s := ⋃ i ∈ (↑s : Set β), mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) ⋯) : Set α)
b : β
hb : b ∈ s
a : α
ha : Membership.mem (γ := Set α) (mulSupport.{u_1, u_5} (M := M) fun (x : α) ↦ f x b) a
simp :
  ∃ (i : β) (_ : i ∈ (↑s : Set β)), Membership.mem (γ := Set α) (mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) a
⊢ a ∈ (↑(Finite.toFinset (s := ⋃ i ∈ (↑s : Set β), mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) ⋯) : Set α)

Tactic:
simp only [Finite.coe_toFinset, mem_iUnion]

Premises used: Set.mem_iUnion, Set.Finite.coe_toFinset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a b
hU :
  (mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ ∏ b ∈ s, f a b) ⊆
    (↑(Finite.toFinset (s := ⋃ i ∈ (↑s : Set β), mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) ⋯) : Set α)
b : β
hb : b ∈ s
a : α
ha : Membership.mem (γ := Set α) (mulSupport.{u_1, u_5} (M := M) fun (x : α) ↦ f x b) a
⊢ ∃ (i : β) (_ : i ∈ (↑s : Set β)), Membership.mem (γ := Set α) (mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) a

Tactic:
⟨b, hb, ha⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a b
hU :
  (mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ ∏ b ∈ s, f a b) ⊆
    (↑(Finite.toFinset (s := ⋃ i ∈ (↑s : Set β), mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) ⋯) : Set α)
b : β
hb : b ∈ s
a : α
ha : Membership.mem (γ := Set α) (mulSupport.{u_1, u_5} (M := M) fun (x : α) ↦ f x b) a
⊢ ∃ (i : β) (_ : i ∈ (↑s : Set β)), Membership.mem (γ := Set α) (mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) a

Tactic:
exact ⟨b, hb, ha⟩
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Finset α
f : α → β → M
h : ∀ a ∈ s, HasFiniteMulSupport (f a)
⊢ Eq.{u_5 + 1} (α := M) (∏ a ∈ s, ∏ᶠ (b : β), f a b) (∏ᶠ (b : β), ∏ a ∈ s, f a b)

Tactic:
(finprod_prod_comm s (fun b a => f a b) h).symm

Premises used: finprod_prod_comm, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
f : β → α
s : Finset β
g : β → M
rw : Eq.{u_5 + 1} (α := M) (∏ i ∈ Finset.image f s, ∏ y ∈ s with f y = i, g y) (∏ k ∈ s, g k)
s₁ : Finset α
h : (mulSupport.{u_1, u_5} (M := M) fun (x : α) ↦ ∏ y ∈ s with f y = x, g y) ⊆ (↑(Finset.image f s) : Set α)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (x : α), ∏ y ∈ s with f y = x, g y) (∏ k ∈ s, g k)

Tactic:
rw [finprod_eq_finsetProd_of_mulSupport_subset]

Premises used: finprod_eq_finsetProd_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 α
f : β → α
s : Finset β
g : β → M
eq : ∀ i ∈ s, Eq.{u_5 + 1} (α := M) (∏ y ∈ s with f y = f i, g y) (∏ j ∈ s with f j = f i, g j)
rw : β → α
⊢ Eq.{u_5 + 1} (α := M) (∏ i ∈ Finset.image f s, ∏ y ∈ s with f y = i, g y) (∏ k ∈ s, g k)

Tactic:
rw [Finset.prod_image']

Premises used: Finset.prod_image'
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ ∀ i ∈ s, Eq.{u_5 + 1} (α := M) (∏ y ∈ s with f y = f i, g y) (∏ j ∈ s with f j = f i, g j)

Tactic:
fun _ _ ↦ rfl

Premises used: rfl
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
f : β → α
s : Finset β
g : β → M
x : α
hx : Membership.mem (γ := Set α) (mulSupport.{u_1, u_5} (M := M) fun (x : α) ↦ ∏ y ∈ s with f y = x, g y) x
⊢ Ne.{u_5 + 1} (α := M) (∏ y ∈ s with f y = x, g y) 1

Tactic:
rw [mem_mulSupport] at hx

Premises used: Function.mem_mulSupport
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
f : β → α
s : Finset β
g : β → M
x : α
hx : Ne.{u_5 + 1} (α := M) (∏ y ∈ s with f y = x, g y) 1
h : ∀ (a : β) (h : a ∈ {y ∈ s | f y = x}), x ∈ (↑(Finset.image f s) : Set α)
⊢ x ∈ (↑(Finset.image f s) : Set α)

Tactic:
obtain ⟨a, h, -⟩ := Finset.exists_ne_one_of_prod_ne_one hx

Premises used: Finset.exists_ne_one_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 α
f : β → α
s : Finset β
g : β → M
x : α
hx : Ne.{u_5 + 1} (α := M) (∏ y ∈ s with f y = x, g y) 1
a : β
h : a ∈ {y ∈ s | f y = x}
h₁ : ∀ (h : a ∈ s ∧ f a = x), ∃ x_1 ∈ s, f x_1 = x
⊢ x ∈ (↑(Finset.image f s) : Set α)

Tactic:
simp only [Finset.mem_filter, Finset.coe_image, mem_image, SetLike.mem_coe] at h ⊢

Premises used: Set.mem_image, Finset.coe_image, SetLike.mem_coe, Finset.mem_filter
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
f : β → α
s : Finset β
g : β → M
x : α
hx : Ne.{u_5 + 1} (α := M) (∏ y ∈ s with f y = x, g y) 1
a : β
h : a ∈ s ∧ f a = x
⊢ ∃ x_1 ∈ s, f x_1 = x

Tactic:
⟨a, h⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
f : β → α
s : Finset β
g : β → M
x : α
hx : Ne.{u_5 + 1} (α := M) (∏ y ∈ s with f y = x, g y) 1
a : β
h : a ∈ s ∧ f a = x
⊢ ∃ x_1 ∈ s, f x_1 = x

Tactic:
exact ⟨a, h⟩
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
f : α → R
r : R
h : HasFiniteSupport f
⊢ r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a

Tactic:
(AddMonoidHom.mulLeft r).map_finsum h

Premises used: AddMonoidHom.map_finsum, AddMonoidHom.mulLeft
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
s : Set α
f : α → R
r : R
hs : s.Finite
⊢ r * ∑ᶠ (a : α) (_ : a ∈ s), f a = ∑ᶠ (a : α) (_ : a ∈ s), r * f a

Tactic:
(AddMonoidHom.mulLeft r).map_finsum_mem f hs

Premises used: AddMonoidHom.mulLeft, AddMonoidHom.map_finsum_mem
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
f : α → R
r : R
h : HasFiniteSupport f
⊢ (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r

Tactic:
(AddMonoidHom.mulRight r).map_finsum h

Premises used: AddMonoidHom.map_finsum, AddMonoidHom.mulRight
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
s : Set α
f : α → R
r : R
hs : s.Finite
⊢ (∑ᶠ (a : α) (_ : a ∈ s), f a) * r = ∑ᶠ (a : α) (_ : a ∈ s), f a * r

Tactic:
(AddMonoidHom.mulRight r).map_finsum_mem f hs

Premises used: AddMonoidHom.mulRight, AddMonoidHom.map_finsum_mem
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
f : α → R
r : R
pos : ∀ (hr : r = 0), r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a
neg : ∀ (hr : ¬r = 0), r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a
⊢ r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a

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

Tactic:
simp_all
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
pos : ∀ (h : (support f).Finite), r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a
neg : ∀ (h : ¬(support f).Finite), r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a
⊢ r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a

Tactic:
by_cases h : f.support.Finite

Premises used: Set.Finite, Function.support
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
h : (support f).Finite
⊢ r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a

Tactic:
mul_finsum' f r h

Premises used: mul_finsum'
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
h : (support f).Finite
⊢ r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a

Tactic:
exact mul_finsum' f r h

Premises used: mul_finsum'
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
h : ¬(support f).Finite
⊢ (support.{u_1, u_7} (M := R) fun (x : α) ↦ r * f x) = support f

Tactic:
aesop
-- 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
rw : Eq.{u_7 + 1} (α := R) (∑ᶠ (a : α), r * ∑ᶠ (_ : a ∈ s), f a) (∑ᶠ (a : α) (_ : a ∈ s), r * f a)
⊢ r * ∑ᶠ (a : α) (_ : a ∈ s), f a = ∑ᶠ (a : α) (_ : a ∈ s), r * f a

Tactic:
rw [mul_finsum]

Premises used: mul_finsum
-- 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 : Eq (α := α → R) (fun (a : α) ↦ r * ∑ᶠ (_ : a ∈ s), f a) fun (a : α) ↦ ∑ᶠ (_ : a ∈ s), r * f a
⊢ Eq.{u_7 + 1} (α := R) (∑ᶠ (a : α), r * ∑ᶠ (_ : a ∈ s), f a) (∑ᶠ (a : α) (_ : a ∈ s), r * f a)

Tactic:
congr
-- 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 : α), r * ∑ᶠ (_ : a ∈ s), f a = ∑ᶠ (_ : a ∈ s), r * f a
⊢ Eq (α := α → R) (fun (a : α) ↦ r * ∑ᶠ (_ : a ∈ s), f a) fun (a : α) ↦ ∑ᶠ (_ : a ∈ s), r * f a

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), r * ∑ᶠ (_ : a ∈ s), f a = ∑ᶠ (_ : a ∈ s), r * f a
neg : ∀ (h : a ∉ s), r * ∑ᶠ (_ : a ∈ s), f a = ∑ᶠ (_ : a ∈ s), r * f a
⊢ r * ∑ᶠ (_ : a ∈ s), f a = ∑ᶠ (_ : a ∈ s), r * f a

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
⊢ r * ∑ᶠ (_ : a ∈ s), f a = ∑ᶠ (_ : a ∈ s), r * f a

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
⊢ r * ∑ᶠ (_ : a ∈ s), f a = ∑ᶠ (_ : a ∈ s), r * f a

Tactic:
simp_all
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
f : α → R
r : R
pos : ∀ (hr : r = 0), (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r
neg : ∀ (hr : ¬r = 0), (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r
⊢ (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r

Tactic:
by_cases hr : r = 0
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
f : α → R
r : R
hr : r = 0
⊢ (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), 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
f : α → R
r : R
hr : ¬r = 0
pos : ∀ (h : (support f).Finite), (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r
neg : ∀ (h : ¬(support f).Finite), (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r
⊢ (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r

Tactic:
by_cases h : f.support.Finite

Premises used: Set.Finite, Function.support
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
h : (support f).Finite
⊢ (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r

Tactic:
finsum_mul' f r h

Premises used: finsum_mul'
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
h : (support f).Finite
⊢ (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r

Tactic:
exact finsum_mul' f r h

Premises used: finsum_mul'
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
h : ¬(support f).Finite
⊢ (support.{u_1, u_7} (M := R) fun (x : α) ↦ f x * r) = support f

Tactic:
aesop
-- 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
rw : Eq.{u_7 + 1} (α := R) (∑ᶠ (a : α), (∑ᶠ (_ : a ∈ s), f a) * r) (∑ᶠ (a : α) (_ : a ∈ s), f a * r)
⊢ (∑ᶠ (a : α) (_ : a ∈ s), f a) * r = ∑ᶠ (a : α) (_ : a ∈ s), f a * r

Tactic:
rw [finsum_mul]

Premises used: finsum_mul
-- 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 : Eq (α := α → R) (fun (a : α) ↦ (∑ᶠ (_ : a ∈ s), f a) * r) fun (a : α) ↦ ∑ᶠ (_ : a ∈ s), f a * r
⊢ Eq.{u_7 + 1} (α := R) (∑ᶠ (a : α), (∑ᶠ (_ : a ∈ s), f a) * r) (∑ᶠ (a : α) (_ : a ∈ s), f a * r)

Tactic:
congr