awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (hypothesis)
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))
have H : ¬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
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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)
⊢ Eq.{u_7 + 1} (α := R) (↑(∏ᶠ (x : ι), f x) : R) (∏ᶠ (x : ι), (↑(f x) : R))
have neg : Eq.{u_7 + 1} (α := R) (↑1 : R) (∏ᶠ (x : ι), (↑(f x) : R))
Tactic: rw [finprod_of_not_hasFiniteMulSupport hf, finprod_of_not_hasFiniteMulSupport H, cast_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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))
⊢ Eq.{u_7 + 1} (α := R) (↑(∏ᶠ (x : ι), f x) : R) (∏ᶠ (x : ι), (↑(f x) : R))
have neg₁ : Eq.{u_7 + 1} (α := R) (↑1 : R) 1
Tactic: rw [finprod_of_not_hasFiniteMulSupport hf, finprod_of_not_hasFiniteMulSupport H, cast_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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
⊢ Eq.{u_7 + 1} (α := R) (↑(∏ᶠ (x : ι), f x) : R) (∏ᶠ (x : ι), (↑(f x) : R))
have neg₂ : Eq.{u_7 + 1} (α := R) 1 1
Tactic: rw [finprod_of_not_hasFiniteMulSupport hf, finprod_of_not_hasFiniteMulSupport H, cast_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_2
inst : DecidableEq α
inst_1 : CommMonoid M
s : Multiset α
f : α → M
⊢ (map f s).prod = ∏ᶠ (a : α), f a ^ count a s
have rw : Eq.{u_2 + 1} (α := M) (∏ᶠ (a : α), f a ^ count a s) (∏ m ∈ s.toFinset, f m ^ count m s)
Tactic: rw [Finset.prod_multiset_map_count, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
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)
have refine : ∀ (x : α) (hxs : x ∈ s) (hx : x ∉ f.support), Eq.{u_8 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
Tactic: refine Finset.prod_subset hs fun x hxs hx => h x hxs ▸ (congr_arg (g x) ?_)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
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
⊢ h x ((mapRange f hf g : (a : α) → M') x) = 1
have rw : h x 0 = 1
Tactic: rw [notMem_support_iff.1 H, h0]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
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
⊢ h x ((mapRange f hf g : (a : α) → M') x) = 1
have rw₁ : Eq.{u_10 + 1} (α := N) 1 1
Tactic: rw [notMem_support_iff.1 H, h0]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
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
⊢ (∏ 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
have 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
Tactic: rw [f.support.prod_ite_eq]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
N : Type u_16
inst_1 : Zero N
f : α →₀ N
a : α
⊢ Eq.{u_16 + 1} (α := N) (if a ∈ f.support then (f : (a : α) → N) a else 0 : N) ((f : (a : α) → N) a : N)
have 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)
Tactic: simp only [mem_support_iff, ne_eq, ite_eq_left_iff, not_not]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
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
⊢ (∏ 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
have 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
Tactic: rw [f.support.prod_ite_eq']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
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
⊢ g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g
have rw : ∀ x ∈ f.support.erase y, g x ((erase y f : (a : α) → M) x) = g x ((f : (a : α) → M) x)
Tactic: rw [Finsupp.prod, Finsupp.prod, ← Finset.mul_prod_erase _ _ hyf, Finsupp.support_erase,
      Finset.prod_congr rfl]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
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
⊢ g h ((erase y f : (a : α) → M) h) = g h ((f : (a : α) → M) h)
have rw : g h ((f : (a : α) → M) h) = g h ((f : (a : α) → M) h)
Tactic: rw [Finsupp.erase_ne (ne_of_mem_erase hx)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
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
⊢ g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g
have rw : g y ((f : (a : α) → M) y) * ∏ a ∈ (erase y f).support, g a ((erase y f : (a : α) → M) a) = 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)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
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
⊢ g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g
have 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)
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)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
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)
⊢ g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g
have 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)
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)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
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)
⊢ g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g
have 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)
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)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
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)
⊢ g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g
have 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)
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)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
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)
⊢ g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g
have rw₅ : ∀ x ∈ f.support.erase y, g x ((erase y f : (a : α) → M) x) = g x ((f : (a : α) → M) x)
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)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
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)
⊢ g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g
have rw₆ : α → N
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)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
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
⊢ g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g
have pos : ∀ (hyf : y ∈ f.support), g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g
Tactic: by_cases hyf : y ∈ f.support
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
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
⊢ g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g
have neg : ∀ (hyf : y ∉ f.support), g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g
Tactic: by_cases hyf : y ∈ f.support
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
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
have neg : g y 0 * (erase y f).prod g = f.prod g
Tactic: rw [notMem_support_iff.mp hyf, hg y, erase_of_notMem_support hyf, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
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
⊢ g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g
have neg₁ : 1 * (erase y f).prod g = f.prod g
Tactic: rw [notMem_support_iff.mp hyf, hg y, erase_of_notMem_support hyf, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
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
⊢ g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g
have neg₂ : 1 * f.prod g = f.prod g
Tactic: rw [notMem_support_iff.mp hyf, hg y, erase_of_notMem_support hyf, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
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
⊢ g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g
have neg₃ : f.prod g = f.prod g
Tactic: rw [notMem_support_iff.mp hyf, hg y, erase_of_notMem_support hyf, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
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
⊢ g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g
have pos : ∀ (hyf : y ∈ f.support), 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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
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
⊢ g y ((f : (a : α) → M) y) * (erase y f).prod g = f.prod g
have neg : ∀ (hyf : y ∉ f.support), 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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
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
⊢ f1.prod g1 = f2.prod g2
have 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))
Tactic: rw [Finsupp.prod_of_support_subset f1 Finset.subset_union_left _ h1,
    Finsupp.prod_of_support_subset f2 Finset.subset_union_right _ h2]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), Ne.{u_8 + 1} (α := M) ((f : (a : α) → M) b : M) (0 : M) → b ≠ a → g b ((f : (a : α) → M) b) = 1
h₁ : Eq.{u_8 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) → g a 0 = 1
⊢ f.prod g = g a ((f : (a : α) → M) a)
have refine_1 : ∀ (b : α) (hb₁ : b ∈ f.support) (hb₂ : b ≠ a), g b ((f : (a : α) → M) b) = 1
Tactic: refine Finset.prod_eq_single a (fun b hb₁ hb₂ => ?_) (fun h => ?_)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), Ne.{u_8 + 1} (α := M) ((f : (a : α) → M) b : M) (0 : M) → b ≠ a → g b ((f : (a : α) → M) b) = 1
h₁ : Eq.{u_8 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) → g a 0 = 1
refine_1 : ∀ (b : α) (hb₁ : b ∈ f.support) (hb₂ : b ≠ a), g b ((f : (a : α) → M) b) = 1
⊢ f.prod g = g a ((f : (a : α) → M) a)
have refine_2 : ∀ (h : a ∉ f.support), g a ((f : (a : α) → M) a) = 1
Tactic: refine Finset.prod_eq_single a (fun b hb₁ hb₂ => ?_) (fun h => ?_)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (hypothesis)
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), Ne.{u_8 + 1} (α := M) ((f : (a : α) → M) b : M) (0 : M) → b ≠ a → g b ((f : (a : α) → M) b) = 1
h₁ : Eq.{u_8 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) → g a 0 = 1
h : a ∉ f.support
⊢ g a ((f : (a : α) → M) a) = 1
have h₂ : Eq.{u_8 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
Tactic: simp only [notMem_support_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), Ne.{u_8 + 1} (α := M) ((f : (a : α) → M) b : M) (0 : M) → b ≠ a → g b ((f : (a : α) → M) b) = 1
h₁ : Eq.{u_8 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) → g a 0 = 1
h : Eq.{u_8 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
⊢ g a ((f : (a : α) → M) a) = 1
have refine_2 : g a 0 = 1
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
s_1 : Multiset M
a_1 : α
a : M
s : Multiset M
ih : Eq (α := α →₀ M) (single a_1 s.sum) (Multiset.sum (Multiset.map (single a_1) s))
⊢ Eq (α := α →₀ M) (single a_1 (a ::ₘ s).sum) (Multiset.sum (Multiset.map (single a_1) (a ::ₘ s)))
have rw : Eq (α := α →₀ M) (single a_1 (a + s.sum)) (Multiset.sum (Multiset.map (single a_1) (a ::ₘ s)))
Tactic: rw [Multiset.sum_cons, single_add, ih, Multiset.map_cons, Multiset.sum_cons]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
s_1 : Multiset M
a_1 : α
a : M
s : Multiset M
ih : Eq (α := α →₀ M) (single a_1 s.sum) (Multiset.sum (Multiset.map (single a_1) s))
rw : Eq (α := α →₀ M) (single a_1 (a + s.sum)) (Multiset.sum (Multiset.map (single a_1) (a ::ₘ s)))
⊢ Eq (α := α →₀ M) (single a_1 (a ::ₘ s).sum) (Multiset.sum (Multiset.map (single a_1) (a ::ₘ s)))
have rw₁ : HAdd.hAdd (α := α →₀ M) (single a_1 a) (single a_1 s.sum) = Multiset.sum (Multiset.map (single a_1) (a ::ₘ s))
Tactic: rw [Multiset.sum_cons, single_add, ih, Multiset.map_cons, Multiset.sum_cons]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
s_1 : Multiset M
a_1 : α
a : M
s : Multiset M
ih : Eq (α := α →₀ M) (single a_1 s.sum) (Multiset.sum (Multiset.map (single a_1) s))
rw : Eq (α := α →₀ M) (single a_1 (a + s.sum)) (Multiset.sum (Multiset.map (single a_1) (a ::ₘ s)))
rw₁ : HAdd.hAdd (α := α →₀ M) (single a_1 a) (single a_1 s.sum) = Multiset.sum (Multiset.map (single a_1) (a ::ₘ s))
⊢ Eq (α := α →₀ M) (single a_1 (a ::ₘ s).sum) (Multiset.sum (Multiset.map (single a_1) (a ::ₘ s)))
have rw₂ : HAdd.hAdd (α := α →₀ M) (single a_1 a) (Multiset.sum (Multiset.map (single a_1) s)) =
  Multiset.sum (Multiset.map (single a_1) (a ::ₘ s))
Tactic: rw [Multiset.sum_cons, single_add, ih, Multiset.map_cons, Multiset.sum_cons]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
s_1 : Multiset M
a_1 : α
a : M
s : Multiset M
ih : Eq (α := α →₀ M) (single a_1 s.sum) (Multiset.sum (Multiset.map (single a_1) s))
rw : Eq (α := α →₀ M) (single a_1 (a + s.sum)) (Multiset.sum (Multiset.map (single a_1) (a ::ₘ s)))
rw₁ : HAdd.hAdd (α := α →₀ M) (single a_1 a) (single a_1 s.sum) = Multiset.sum (Multiset.map (single a_1) (a ::ₘ s))
rw₂ :
  HAdd.hAdd (α := α →₀ M) (single a_1 a) (Multiset.sum (Multiset.map (single a_1) s)) =
    Multiset.sum (Multiset.map (single a_1) (a ::ₘ s))
⊢ Eq (α := α →₀ M) (single a_1 (a ::ₘ s).sum) (Multiset.sum (Multiset.map (single a_1) (a ::ₘ s)))
have rw₃ : HAdd.hAdd (α := α →₀ M) (single a_1 a) (Multiset.sum (Multiset.map (single a_1) s)) =
  Multiset.sum (single a_1 a ::ₘ Multiset.map (single a_1) s)
Tactic: rw [Multiset.sum_cons, single_add, ih, Multiset.map_cons, Multiset.sum_cons]