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 : α → β
hf : Injective f
inst_1 : DecidablePred fun (x : β) ↦ x ∈ range f
g : α → M
rw : ∀ (a : α), (if h' : f a ∈ range f then g (Classical.choose (p := fun (x : α) ↦ f x = f a) h') else 1) = g a
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (b : β) (h : b ∈ range f), g (Classical.choose (p := fun (x : α) ↦ f x = b) h))
    (∏ᶠ (a : α), g a)

Tactic:
rw [finprod_dmem, finprod_mem_range hf, finprod_congr fun a => _]

Premises used: finprod_mem_range, finprod_congr, finprod_dmem
-- 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
a : α
rw : g (Classical.choose (p := fun (x : α) ↦ f x = f a) ⋯) = g a
rw₁ rw₂ : g a = g a
⊢ (if h' : f a ∈ range f then g (Classical.choose (p := fun (x : α) ↦ f x = f a) h') else 1) = g a

Tactic:
rw [dif_pos (Set.mem_range_self a), hf (Classical.choose_spec (Set.mem_range_self a))]

Premises used: Set.mem_range_self, dif_pos, Classical.choose_spec
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α ↪ β
inst_1 : DecidablePred fun (x : β) ↦ Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x
g : α → M
⊢ Eq.{u_5 + 1} (α := M)
    (∏ᶠ (b : β),
      if h : Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b then
        g (Classical.choose (p := fun (x : α) ↦ (f : (a : α) → β) x = b) h)
      else 1)
    (∏ᶠ (a : α), g a)

Tactic:
finprod_emb_domain' f.injective g

Premises used: Set.Mem, Function.Embedding.injective, finprod_emb_domain'
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
ι : Type u_3
inst : Finite ι
R : Type u_7
inst_1 : CommSemiring R
f : ι → ℕ
⊢ Eq.{u_7 + 1} (α := R) (↑(∏ᶠ (x : ι), f x) : R) (∏ᶠ (x : ι), (↑(f x) : R))

Tactic:
(Nat.castRingHom R).map_finprod f.mulSupport.toFinite

Premises used: Set.toFinite, Nat.castRingHom, Function.mulSupport, MonoidHom.map_finprod, RingHom.toMonoidHom
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
ι : Type u_3
R : Type u_7
inst : CommSemiring R
inst_1 : CharZero R
f : ι → ℕ
pos : ∀ (hf : HasFiniteMulSupport f), Eq.{u_7 + 1} (α := R) (↑(∏ᶠ (x : ι), f x) : R) (∏ᶠ (x : ι), (↑(f x) : R))
neg : ∀ (hf : ¬HasFiniteMulSupport f), Eq.{u_7 + 1} (α := R) (↑(∏ᶠ (x : ι), f x) : R) (∏ᶠ (x : ι), (↑(f x) : R))
⊢ Eq.{u_7 + 1} (α := R) (↑(∏ᶠ (x : ι), f x) : R) (∏ᶠ (x : ι), (↑(f x) : R))

Tactic:
by_cases hf : f.HasFiniteMulSupport

Premises used: Function.HasFiniteMulSupport
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
ι : Type u_3
R : Type u_7
inst : CommSemiring R
inst_1 : CharZero R
f : ι → ℕ
hf : HasFiniteMulSupport f
⊢ Eq.{u_7 + 1} (α := R) (↑(∏ᶠ (x : ι), f x) : R) (∏ᶠ (x : ι), (↑(f x) : R))

Tactic:
map_finprod (Nat.castRingHom R) hf

Premises used: map_finprod, Nat.castRingHom
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
ι : Type u_3
R : Type u_7
inst : CommSemiring R
inst_1 : CharZero R
f : ι → ℕ
hf : HasFiniteMulSupport f
⊢ Eq.{u_7 + 1} (α := R) (↑(∏ᶠ (x : ι), f x) : R) (∏ᶠ (x : ι), (↑(f x) : R))

Tactic:
exact map_finprod (Nat.castRingHom R) hf

Premises used: map_finprod, Nat.castRingHom
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
ι : Type u_3
R : Type u_7
inst : CommSemiring R
inst_1 : CharZero R
f : ι → ℕ
hf : ¬HasFiniteMulSupport f
⊢ ¬HasFiniteMulSupport.{u_3, u_7} (M := R) fun (i : ι) ↦ (↑(f i) : R)

Tactic:
have H : ¬ (fun i ↦ (f i : R)).HasFiniteMulSupport :=
      fun h ↦ hf <| h.of_comp cast_one cast_injective
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
ι : Type u_3
R : Type u_7
inst : CommSemiring R
inst_1 : CharZero R
f : ι → ℕ
hf : ¬HasFiniteMulSupport f
H : ¬HasFiniteMulSupport.{u_3, u_7} (M := R) fun (i : ι) ↦ (↑(f i) : R)
neg : Eq.{u_7 + 1} (α := R) (↑1 : R) (∏ᶠ (x : ι), (↑(f x) : R))
neg₁ : Eq.{u_7 + 1} (α := R) (↑1 : R) 1
neg₂ neg₃ : Eq.{u_7 + 1} (α := R) 1 1
⊢ Eq.{u_7 + 1} (α := R) (↑(∏ᶠ (x : ι), f x) : R) (∏ᶠ (x : ι), (↑(f x) : R))

Tactic:
rw [finprod_of_not_hasFiniteMulSupport hf, finprod_of_not_hasFiniteMulSupport H, cast_one]

Premises used: finprod_of_not_hasFiniteMulSupport, Nat.cast_one
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
ι : Type u_3
s : Set ι
hs : s.Finite
R : Type u_7
inst : CommSemiring R
f : ι → ℕ
⊢ Eq.{u_7 + 1} (α := R) (↑(∏ᶠ (x : ι) (_ : x ∈ s), f x) : R) (∏ᶠ (x : ι) (_ : x ∈ s), (↑(f x) : R))

Tactic:
(Nat.castRingHom R).map_finprod_mem _ hs

Premises used: MonoidHom.map_finprod_mem, Nat.castRingHom, RingHom.toMonoidHom
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
ι : Type u_3
inst : Finite ι
M : Type u_7
inst_1 : AddCommMonoidWithOne M
f : ι → ℕ
⊢ Eq.{u_7 + 1} (α := M) (↑(∑ᶠ (x : ι), f x) : M) (∑ᶠ (x : ι), (↑(f x) : M))

Tactic:
(Nat.castAddMonoidHom M).map_finsum f.support.toFinite

Premises used: Nat.castAddMonoidHom, AddMonoidHom.map_finsum, Set.toFinite, Function.support
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
ι : Type u_3
s : Set ι
hs : s.Finite
M : Type u_7
inst : AddCommMonoidWithOne M
f : ι → ℕ
⊢ Eq.{u_7 + 1} (α := M) (↑(∑ᶠ (x : ι) (_ : x ∈ s), f x) : M) (∑ᶠ (x : ι) (_ : x ∈ s), (↑(f x) : M))

Tactic:
(Nat.castAddMonoidHom M).map_finsum_mem _ hs

Premises used: Nat.castAddMonoidHom, AddMonoidHom.map_finsum_mem
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_2
inst : DecidableEq α
inst_1 : CommMonoid M
s : Multiset α
f : α → M
⊢ (mulSupport.{u_1, u_2} (M := M) fun (a : α) ↦ f a ^ count a s) ⊆ (↑s.toFinset : Set α)

Tactic:
simp +contextual [not_imp_comm]

Premises used: not_imp_comm
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_2
inst : DecidableEq α
inst_1 : CommMonoid M
s : Multiset α
f : α → M
⊢ HasFiniteMulSupport.{u_1, u_2} (M := M) fun (a : α) ↦ f a ^ count a s

Tactic:
s.toFinset.finite_toSet.subset <| mulSupport_fun_pow_count_subset ..

Premises used: Multiset.toFinset, Set.Finite.subset, Multiset.mulSupport_fun_pow_count_subset, Finset.finite_toSet, Function.HasFiniteMulSupport
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_2
inst : DecidableEq α
inst_1 : CommMonoid M
s : Multiset α
f : α → M
rw : Eq.{u_2 + 1} (α := M) (∏ᶠ (a : α), f a ^ count a s) (∏ m ∈ s.toFinset, f m ^ count m s)
⊢ (map f s).prod = ∏ᶠ (a : α), f a ^ count a s

Tactic:
rw [Finset.prod_multiset_map_count, eq_comm]

Premises used: Finset.prod_multiset_map_count, eq_comm
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_2
inst : DecidableEq α
inst_1 : CommMonoid M
s : Multiset α
f : α → M
⊢ Eq.{u_2 + 1} (α := M) (∏ᶠ (a : α), f a ^ count a s) (∏ m ∈ s.toFinset, f m ^ count m s)

Tactic:
finprod_eq_prod_of_mulSupport_subset _ <| mulSupport_fun_pow_count_subset ..

Premises used: Multiset.mulSupport_fun_pow_count_subset, finprod_eq_prod_of_mulSupport_subset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_2
inst : DecidableEq α
inst_1 : CommMonoid M
s : Multiset α
f : α → M
⊢ Eq.{u_2 + 1} (α := M) (∏ᶠ (a : α), f a ^ count a s) (∏ m ∈ s.toFinset, f m ^ count m s)

Tactic:
exact finprod_eq_prod_of_mulSupport_subset _ <| mulSupport_fun_pow_count_subset ..

Premises used: Multiset.mulSupport_fun_pow_count_subset, finprod_eq_prod_of_mulSupport_subset
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f : α →₀ M
⊢ Eq.{u_10 + 1} (α := N) (f.prod fun (x : α) (x_1 : M) ↦ 1) 1

Tactic:
simp [prod]

Premises used: Finsupp.prod
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f : α →₀ M
s : Finset α
hs : f.support ⊆ s
g : α → M → N
h : ∀ i ∈ s, g i 0 = 1
⊢ f.prod g = ∏ x ∈ s, g x ((f : (a : α) → M) x)

Tactic:
Finset.prod_subset hs fun x hxs hx => h x hxs ▸ (congr_arg (g x) ?_)

Premises used: Eq.rec, Finset.prod_subset, congr_arg, Finsupp.prod
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f : α →₀ M
s : Finset α
hs : f.support ⊆ s
g : α → M → N
h : ∀ i ∈ s, g i 0 = 1
refine : ∀ (x : α) (hxs : x ∈ s) (hx : x ∉ f.support), Eq.{u_8 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
⊢ f.prod g = ∏ x ∈ s, g x ((f : (a : α) → M) x)

Tactic:
refine Finset.prod_subset hs fun x hxs hx => h x hxs ▸ (congr_arg (g x) ?_)

Premises used: Finset.prod_subset
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f : α →₀ M
s : Finset α
hs : f.support ⊆ s
g : α → M → N
h : ∀ i ∈ s, g i 0 = 1
x : α
hxs : x ∈ s
hx : x ∉ f.support
⊢ Eq.{u_8 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)

Tactic:
notMem_support_iff.1 hx

Premises used: Finsupp.notMem_support_iff, Iff.mp
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f : α →₀ M
s : Finset α
hs : f.support ⊆ s
g : α → M → N
h : ∀ i ∈ s, g i 0 = 1
x : α
hxs : x ∈ s
hx : x ∉ f.support
⊢ Eq.{u_8 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)

Tactic:
exact notMem_support_iff.1 hx

Premises used: Finsupp.notMem_support_iff, Iff.mp
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
inst_2 : Fintype α
f : α →₀ M
g : α → M → N
h : ∀ (i : α), g i 0 = 1
⊢ f.prod g = ∏ i : α, g i ((f : (a : α) → M) i)

Tactic:
f.prod_of_support_subset (subset_univ _) g fun x _ => h x

Premises used: Finsupp.prod_of_support_subset, Finset.subset_univ
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
a : α
b : M
h : α → M → N
h_zero : h a 0 = 1
⊢ ∏ x ∈ {a}, h x ((single a b : (a : α) → M) x) = h a b

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
M' : Type u_9
N : Type u_10
inst : Zero M
inst_1 : Zero M'
inst_2 : CommMonoid N
f : M → M'
hf : f 0 = 0
g : α →₀ M
h : α → M' → N
h0 : ∀ (a : α), h a 0 = 1
x : α
h_1 : x ∈ g.support
H : x ∉ (mapRange f hf g).support
rw : h x 0 = 1
rw₁ rw₂ : Eq.{u_10 + 1} (α := N) 1 1
⊢ h x ((mapRange f hf g : (a : α) → M') x) = 1

Tactic:
rw [notMem_support_iff.1 H, h0]

Premises used: Finsupp.notMem_support_iff, Iff.mp
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
g : α → M → N
hg : ∀ i ∈ s, g i 0 = 1
⊢ (onFinset s f hf).prod g = ∏ a ∈ s, g a (f a)

Tactic:
prod_of_support_subset _ support_onFinset_subset _ hg

Premises used: Finsupp.prod_of_support_subset, Finsupp.support_onFinset_subset
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
h : α → M → N
⊢ prod 0 h = 1

Tactic:
rfl

Premises used: Multiset.foldr, Multiset.prod, Finset.prod, List.foldr, Finsupp.prod, rfl
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_7
M : Type u_8
M' : Type u_9
N : Type u_10
inst : Zero M
inst_1 : Zero M'
inst_2 : CommMonoid N
f : α →₀ M
g : β →₀ M'
h : α → M → β → M' → N
⊢ Eq.{u_10 + 1} (α := N) (f.prod fun (x : α) (v : M) ↦ g.prod fun (x' : β) (v' : M') ↦ h x v x' v')
    (g.prod fun (x' : β) (v' : M') ↦ f.prod fun (x : α) (v : M) ↦ h x v x' v')

Tactic:
Finset.prod_comm

Premises used: Finset.prod_comm, Finsupp.prod
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_7
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
s : Finset β
f : α →₀ M
h : α → M → β → N
⊢ Eq.{u_10 + 1} (α := N) (f.prod fun (a : α) (m : M) ↦ ∏ b ∈ s, h a m b) (∏ b ∈ s, f.prod fun (a : α) (m : M) ↦ h a m b)

Tactic:
Finset.prod_comm

Premises used: Finset.prod_comm, Finsupp.prod
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
inst_2 : DecidableEq α
f : α →₀ M
a : α
b : α → M → N
rw rw₁ :
  (if a ∈ f.support then b a ((f : (a : α) → M) a) else 1) = if a ∈ f.support then b a ((f : (a : α) → M) a) else 1
⊢ (∏ a_1 ∈ f.support, if a = a_1 then b a_1 ((f : (a : α) → M) a_1) else 1) =
    if a ∈ f.support then b a ((f : (a : α) → M) a) else 1

Tactic:
rw [f.support.prod_ite_eq]

Premises used: Finsupp.support, Finset.prod_ite_eq
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
inst : DecidableEq α
N : Type u_16
inst_1 : AddCommMonoid N
f : α →₀ N
a : α
⊢ Eq (α := N) (f.sum fun (x : α) (v : N) ↦ if a = x then v else 0 : N) ((f : (a : α) → N) a : N)

Tactic:
simp_all
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
inst : DecidableEq α
N : Type u_16
inst_1 : Zero N
f : α →₀ N
a : α
simp :
  Eq.{u_16 + 1} (α := N) ((f : (a : α) → N) a : N) (0 : N) → Eq.{u_16 + 1} (α := N) (0 : N) ((f : (a : α) → N) a : N)
⊢ Eq.{u_16 + 1} (α := N) (if a ∈ f.support then (f : (a : α) → N) a else 0 : N) ((f : (a : α) → N) a : N)

Tactic:
simp only [mem_support_iff, ne_eq, ite_eq_left_iff, not_not]

Premises used: Finsupp.mem_support_iff, ite_eq_left_iff, Classical.not_not, ne_eq
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
inst : DecidableEq α
N : Type u_16
inst_1 : Zero N
f : α →₀ N
a : α
⊢ Eq.{u_16 + 1} (α := N) ((f : (a : α) → N) a : N) (0 : N) → Eq.{u_16 + 1} (α := N) (0 : N) ((f : (a : α) → N) a : N)

Tactic:
fun h ↦ h.symm

Premises used: Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
inst : DecidableEq α
N : Type u_16
inst_1 : Zero N
f : α →₀ N
a : α
⊢ Eq.{u_16 + 1} (α := N) ((f : (a : α) → N) a : N) (0 : N) → Eq.{u_16 + 1} (α := N) (0 : N) ((f : (a : α) → N) a : N)

Tactic:
exact fun h ↦ h.symm
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
inst_2 : DecidableEq α
f : α →₀ M
a : α
b : α → M → N
rw rw₁ :
  (if a ∈ f.support then b a ((f : (a : α) → M) a) else 1) = if a ∈ f.support then b a ((f : (a : α) → M) a) else 1
⊢ (∏ a_1 ∈ f.support, if a_1 = a then b a_1 ((f : (a : α) → M) a_1) else 1) =
    if a ∈ f.support then b a ((f : (a : α) → M) a) else 1

Tactic:
rw [f.support.prod_ite_eq']

Premises used: Finset.prod_ite_eq', Finsupp.support
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
inst : DecidableEq α
N : Type u_16
inst_1 : AddCommMonoid N
f : α →₀ N
a : α
⊢ Eq (α := N) (f.sum fun (x : α) (v : N) ↦ if x = a then v else 0 : N) ((f : (a : α) → N) a : N)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
N : Type u_10
inst : CommMonoid N
inst_1 : Fintype α
f : α →₀ ℕ
g : α → N
⊢ Eq.{u_10 + 1} (α := N) (f.prod fun (a : α) (b : ℕ) ↦ g a ^ b)
    (∏ a : α, HPow.hPow (β := ℕ) (g a) ((f : (a : α) → ℕ) a : ℕ))

Tactic:
f.prod_fintype _ fun _ ↦ pow_zero _

Premises used: pow_zero, Finsupp.prod_fintype
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
N : Type u_16
inst : DivisionCommMonoid N
inst_1 : Fintype α
f : α →₀ ℤ
g : α → N
⊢ Eq.{u_16 + 1} (α := N) (f.prod fun (a : α) (b : ℤ) ↦ g a ^ b)
    (∏ a : α, HPow.hPow (β := ℤ) (g a) ((f : (a : α) → ℤ) a : ℤ))

Tactic:
f.prod_fintype _ fun _ ↦ zpow_zero _

Premises used: zpow_zero, Finsupp.prod_fintype
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
s : Finset α
f : α → M
g : α → M → N
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
hg : ∀ (a : α), g a 0 = 1
⊢ ∀ x ∈ s, x ∉ (onFinset s f hf).support → g x ((onFinset s f hf : (a : α) → M) x) = 1

Tactic:
simp +contextual [*]
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hyf : y ∈ f.support
rw : ∀ x ∈ f.support.erase y, g x ((erase y f : (a : α) → M) x) = g x ((f : (a : α) → M) x)
⊢ g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g

Tactic:
rw [Finsupp.prod, Finsupp.prod, ← Finset.mul_prod_erase _ _ hyf, Finsupp.support_erase,
      Finset.prod_congr rfl]

Premises used: Finsupp.support_erase, Finset.mul_prod_erase, Finset.prod_congr, Finsupp.prod, rfl
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hyf : y ∈ f.support
h : α
hx : h ∈ f.support.erase y
rw rw₁ : g h ((f : (a : α) → M) h) = g h ((f : (a : α) → M) h)
⊢ g h ((erase y f : (a : α) → M) h) = g h ((f : (a : α) → M) h)

Tactic:
rw [Finsupp.erase_ne (ne_of_mem_erase hx)]

Premises used: Finsupp.erase_ne, Finset.ne_of_mem_erase
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hyf : y ∈ f.support
rw : g y ((f : (a : α) → M) y) * ∏ a ∈ (erase y f).support, g a ((erase y f : (a : α) → M) a) = f.prod g
rw₁ :
  g y ((f : (a : α) → M) y) * ∏ a ∈ (erase y f).support, g a ((erase y f : (a : α) → M) a) =
    ∏ a ∈ f.support, g a ((f : (a : α) → M) a)
rw₂ :
  g y ((f : (a : α) → M) y) * ∏ a ∈ (erase y f).support, g a ((erase y f : (a : α) → M) a) =
    g y ((f : (a : α) → M) y) * ∏ x ∈ f.support.erase y, g x ((f : (a : α) → M) x)
rw₃ :
  g y ((f : (a : α) → M) y) * ∏ a ∈ f.support.erase y, g a ((erase y f : (a : α) → M) a) =
    g y ((f : (a : α) → M) y) * ∏ x ∈ f.support.erase y, g x ((f : (a : α) → M) x)
rw₄ :
  g y ((f : (a : α) → M) y) * ∏ x ∈ f.support.erase y, g x ((f : (a : α) → M) x) =
    g y ((f : (a : α) → M) y) * ∏ x ∈ f.support.erase y, g x ((f : (a : α) → M) x)
rw₅ : ∀ x ∈ f.support.erase y, g x ((erase y f : (a : α) → M) x) = g x ((f : (a : α) → M) x)
rw₆ : α → N
rw₇ :
  g y ((f : (a : α) → M) y) * ∏ x ∈ f.support.erase y, g x ((f : (a : α) → M) x) =
    g y ((f : (a : α) → M) y) * ∏ x ∈ f.support.erase y, g x ((f : (a : α) → M) x)
rw₈ : ∀ x ∈ f.support.erase y, g x ((erase y f : (a : α) → M) x) = g x ((f : (a : α) → M) x)
rw₉ : α → N
rw₁₀ rw₁₁ : ∀ (h : α) (hx : h ∈ f.support.erase y), g h ((erase y f : (a : α) → M) h) = g h ((f : (a : α) → M) h)
⊢ g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g

Tactic:
classical
    rw [Finsupp.prod, Finsupp.prod, ← Finset.mul_prod_erase _ _ hyf, Finsupp.support_erase,
      Finset.prod_congr rfl]
    intro h hx
    rw [Finsupp.erase_ne (ne_of_mem_erase hx)]

Premises used: Finsupp.support_erase, Finset.prod_congr, Finsupp.prod, rfl
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
pos : ∀ (hyf : y ∈ f.support), g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g
neg : ∀ (hyf : y ∉ f.support), g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g
⊢ g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g

Tactic:
by_cases hyf : y ∈ f.support

Premises used: Finsupp.support
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
hyf : y ∈ f.support
⊢ g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g

Tactic:
Finsupp.mul_prod_erase f y g hyf

Premises used: Finsupp.mul_prod_erase
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
hyf : y ∈ f.support
⊢ g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g

Tactic:
exact Finsupp.mul_prod_erase f y g hyf

Premises used: Finsupp.mul_prod_erase
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
hyf : y ∉ f.support
neg : g y 0 * (erase y f).prod g = f.prod g
neg₁ : 1 * (erase y f).prod g = f.prod g
neg₂ : 1 * f.prod g = f.prod g
neg₃ neg₄ : f.prod g = f.prod g
⊢ g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g

Tactic:
rw [notMem_support_iff.mp hyf, hg y, erase_of_notMem_support hyf, one_mul]

Premises used: Finsupp.notMem_support_iff, Finsupp.erase_of_notMem_support, Iff.mp, one_mul
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
pos : ∀ (hyf : y ∈ f.support), g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g
neg neg₁ : ∀ (hyf : y ∉ f.support), g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g
⊢ g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g

Tactic:
classical
    by_cases hyf : y ∈ f.support
    · exact Finsupp.mul_prod_erase f y g hyf
    · rw [notMem_support_iff.mp hyf, hg y, erase_of_notMem_support hyf, one_mul]

Premises used: Finsupp.support, one_mul
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
S : Type u_16
inst_2 : SetLike S N
inst_3 : SubmonoidClass S N
s : S
f : α →₀ M
g : α → M → N
h : ∀ (c : α), Ne.{u_8 + 1} (α := M) ((f : (a : α) → M) c : M) (0 : M) → g c ((f : (a : α) → M) c) ∈ s
⊢ f.prod g ∈ s

Tactic:
prod_mem fun _i hi => h _ (Finsupp.mem_support_iff.mp hi)

Premises used: Finsupp.mem_support_iff, Set.Mem, Iff.mp, Finsupp.prod, prod_mem
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f : α →₀ M
g1 g2 : α → M → N
h : ∀ x ∈ f.support, g1 x ((f : (a : α) → M) x) = g2 x ((f : (a : α) → M) x)
⊢ f.prod g1 = f.prod g2

Tactic:
Finset.prod_congr rfl h

Premises used: Finset.prod_congr, Finsupp.prod, rfl
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
inst_2 : DecidableEq α
f1 f2 : α →₀ M
g1 g2 : α → M → N
h : ∀ x ∈ f1.support ∪ f2.support, g1 x ((f1 : (a : α) → M) x) = g2 x ((f2 : (a : α) → M) x)
h1 : ∀ x ∈ f1.support ∪ f2.support, g1 x 0 = 1
h2 : ∀ x ∈ f1.support ∪ f2.support, g2 x 0 = 1
rw :
  Eq.{u_10 + 1} (α := N) (∏ x ∈ f1.support ∪ f2.support, g1 x ((f1 : (a : α) → M) x))
    (∏ x ∈ f1.support ∪ f2.support, g2 x ((f2 : (a : α) → M) x))
⊢ f1.prod g1 = f2.prod g2

Tactic:
rw [Finsupp.prod_of_support_subset f1 Finset.subset_union_left _ h1,
    Finsupp.prod_of_support_subset f2 Finset.subset_union_right _ h2]

Premises used: Finsupp.prod_of_support_subset, Finset.subset_union_left, Finset.subset_union_right
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
inst_2 : DecidableEq α
f1 f2 : α →₀ M
g1 g2 : α → M → N
h : ∀ x ∈ f1.support ∪ f2.support, g1 x ((f1 : (a : α) → M) x) = g2 x ((f2 : (a : α) → M) x)
h1 : ∀ x ∈ f1.support ∪ f2.support, g1 x 0 = 1
h2 : ∀ x ∈ f1.support ∪ f2.support, g2 x 0 = 1
⊢ Eq.{u_10 + 1} (α := N) (∏ x ∈ f1.support ∪ f2.support, g1 x ((f1 : (a : α) → M) x))
    (∏ x ∈ f1.support ∪ f2.support, g2 x ((f2 : (a : α) → M) x))

Tactic:
Finset.prod_congr rfl h

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
inst_2 : DecidableEq α
f1 f2 : α →₀ M
g1 g2 : α → M → N
h : ∀ x ∈ f1.support ∪ f2.support, g1 x ((f1 : (a : α) → M) x) = g2 x ((f2 : (a : α) → M) x)
h1 : ∀ x ∈ f1.support ∪ f2.support, g1 x 0 = 1
h2 : ∀ x ∈ f1.support ∪ f2.support, g2 x 0 = 1
⊢ Eq.{u_10 + 1} (α := N) (∏ x ∈ f1.support ∪ f2.support, g1 x ((f1 : (a : α) → M) x))
    (∏ x ∈ f1.support ∪ f2.support, g2 x ((f2 : (a : α) → M) x))

Tactic:
exact Finset.prod_congr rfl h

Premises used: Finset.prod_congr, rfl