awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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
⊢ Eq.{u_6 + 1} (α := N) ((∏ᶠ (i : ι), f i) a) (∏ᶠ (i : ι), f i a)
have simp : Eq.{u_6 + 1} (α := N) (∏ c ∈ Finite.toFinset (s := mulSupport f) sorry, f c a)
  (∏ c ∈ Finite.toFinset (s := mulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a) sorry, f c a)
Tactic: simp only [finprod_def, dif_pos, hf, hf', Finset.prod_apply]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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
⊢ 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 symm : Eq.{u_6 + 1} (α := N) (∏ c ∈ Finite.toFinset (s := mulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a) sorry, f c a)
  (∏ c ∈ Finite.toFinset (s := mulSupport f) sorry, f c a)
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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
⊢ 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)
have h : Finite.toFinset (s := mulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a) sorry ⊆ Finite.toFinset (s := mulSupport f) sorry
Tactic: apply Finset.prod_subset
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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) ⋯
⊢ 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)
have hf₁ : ∀ x ∈ Finite.toFinset (s := mulSupport f) sorry,
  x ∉ Finite.toFinset (s := mulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a) sorry → f x a = 1
Tactic: apply Finset.prod_subset
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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) ((∏ᶠ (i : ι), f i) a) (∏ᶠ (i : ι), f i a)
have have : HasFiniteMulSupport.{u_8, u_6} (M := N) fun (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
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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
⊢ Eq.{u_6 + 1} (α := N) ((∏ᶠ (i : ι), f i) a) (∏ᶠ (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)
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
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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)
⊢ Eq.{u_6 + 1} (α := N) ((∏ᶠ (i : ι), f i) a) (∏ᶠ (i : ι), f i a)
have 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) sorry, f c a)
    (∏ c ∈ Finite.toFinset (s := mulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a) sorry, f c 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
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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)
⊢ Eq.{u_6 + 1} (α := N) ((∏ᶠ (i : ι), f i) a) (∏ᶠ (i : ι), f i a)
have 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) sorry, f c a)
    (∏ c ∈ Finite.toFinset (s := mulSupport f) sorry, f c 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
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq β
s : Finset α
f : α → M
g : α → β
⊢ (mulSupport.{u_2, u_5} (M := M) fun (b : β) ↦ ∏ a ∈ s with g a = b, f a) ⊆ (↑(image g s) : Set β)
have simp : (mulSupport.{u_2, u_5} (M := M) fun (b : β) ↦ ∏ a ∈ s with g a = b, f a) ⊆ g '' (↑s : Set α)
Tactic: simp only [Finset.coe_image]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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
⊢ b ∈ g '' (↑s : Set α)
have suffices : {a ∈ s | g a = b}.Nonempty
Tactic: suffices {a ∈ s | g a = b}.Nonempty by
    simpa only [fiber_nonempty_iff_mem_image, Finset.mem_image, exists_prop]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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
have refine_1 : ∀ a_1 ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), (fun (b : β) ↦ (a, b)) a_1 ∈ {x ∈ s | x.1 = a}
Tactic: refine Finset.prod_nbij' (fun b ↦ (a, b)) Prod.snd ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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}
⊢ ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f
have refine_2 : ∀ a_1 ∈ {x ∈ s | x.1 = a}, a_1.2 ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})
Tactic: refine Finset.prod_nbij' (fun b ↦ (a, b)) Prod.snd ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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})
⊢ ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f
have refine_3 : ∀ a_1 ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), ((fun (b : β) ↦ (a, b)) a_1).2 = a_1
Tactic: refine Finset.prod_nbij' (fun b ↦ (a, b)) Prod.snd ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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
⊢ ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f
have refine_4 : ∀ a_1 ∈ {x ∈ s | x.1 = a}, (fun (b : β) ↦ (a, b)) a_1.2 = a_1
Tactic: refine Finset.prod_nbij' (fun b ↦ (a, b)) Prod.snd ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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
⊢ ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f
have refine_5 : ∀ a_1 ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, a_1) = f ((fun (b : β) ↦ (a, b)) a_1)
Tactic: refine Finset.prod_nbij' (fun b ↦ (a, b)) Prod.snd ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
inst_2 : DecidableEq β
s : Finset (α × β)
f : α × β → M
⊢ 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))
have this : ∀ (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
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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
⊢ 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))
have 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))
Tactic: rw [finprod_mem_finset_eq_prod]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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
⊢ Eq.{u_5 + 1} (α := M) (∏ i ∈ s, f i)
    (∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b))
have simp_rw : Eq.{u_5 + 1} (α := M) (∏ i ∈ s, f i) (∏ᶠ (a : α), {ab ∈ s | ab.1 = a}.prod f)
Tactic: simp_rw [finprod_mem_finset_eq_prod, this]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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
⊢ Eq.{u_5 + 1} (α := M) (∏ i ∈ s, f i) (∏ᶠ (a : α), {ab ∈ s | ab.1 = a}.prod f)
have rw : ∀ i ∈ s, i.1 ∈ Finset.image Prod.fst s
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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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, i.1 ∈ Finset.image Prod.fst s
have simp : ∀ i ∈ s, ∃ a ∈ s, a.1 = i.1
Tactic: simp only [Finset.mem_image]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Finset (α × β)
f : α × β → M
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab) (∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b))
have 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))
Tactic: rw [finprod_mem_finset_product']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Finset (α × β)
f : α × β → M
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab) (∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b))
have 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))
Tactic: classical
    rw [finprod_mem_finset_product']
    simp
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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) (∏ᶠ (abc : α × β × γ) (_ : abc ∈ s), f abc)
    (∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c))
have 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))
Tactic: rw [finprod_mem_finset_product']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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 : α) (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))
have 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))
Tactic: simp_rw [finprod_mem_finset_product']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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) (∏ᶠ (abc : α × β × γ) (_ : abc ∈ s), f abc)
    (∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c))
have 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))
Tactic: classical
    rw [finprod_mem_finset_product']
    simp_rw [finprod_mem_finset_product']
    simp
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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))
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (abc : α × β × γ) (_ : abc ∈ s), f abc)
    (∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c))
have 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))
Tactic: classical
    rw [finprod_mem_finset_product']
    simp_rw [finprod_mem_finset_product']
    simp
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α × β → M
hf : HasFiniteMulSupport f
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (ab : α × β), f ab) (∏ᶠ (a : α) (b : β), f (a, b))
have h₁ : ∀ (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
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (hypothesis)
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) (∏ᶠ (ab : α × β), f ab) (∏ᶠ (a : α) (b : β), f (a, b))
have h₂ : 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
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (ab : α × β), f ab) (∏ᶠ (a : α) (b : β), f (a, b))
have simp_rw : Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α × β) (_ : a ∈ Finite.toFinset (s := mulSupport f) hf), f a)
  (∏ᶠ (a : α) (b : β), f (a, b))
Tactic: simp_rw [h₂, finprod_mem_finset_product, h₁]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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))
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (ab : α × β), f ab) (∏ᶠ (a : α) (b : β), f (a, b))
have 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))
Tactic: simp_rw [h₂, finprod_mem_finset_product, h₁]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
γ : Type u_7
f : α × β × γ → M
h : HasFiniteMulSupport f
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (abc : α × β × γ), f abc) (∏ᶠ (a : α) (b : β) (c : γ), f (a, b, c))
have rw : Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (b : β × γ), f (a, b)) (∏ᶠ (a : α) (b : β) (c : γ), f (a, b, c))
Tactic: rw [finprod_curry f h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
γ : Type u_7
f : α × β × γ → M
h : HasFiniteMulSupport f
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (b : β × γ), f (a, b)) (∏ᶠ (a : α) (b : β) (c : γ), f (a, b, c))
have e_f : Eq (α := α → M) (fun (a : α) ↦ ∏ᶠ (b : β × γ), f (a, b)) fun (a : α) ↦ ∏ᶠ (b : β) (c : γ), f (a, b, c)
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
γ : Type u_7
f : α × β × γ → M
h : HasFiniteMulSupport f
⊢ Eq (α := α → M) (fun (a : α) ↦ ∏ᶠ (b : β × γ), f (a, b)) fun (a : α) ↦ ∏ᶠ (b : β) (c : γ), f (a, b, c)
have e_f : ∀ (a : α), Eq.{u_5 + 1} (α := M) (∏ᶠ (b : β × γ), f (a, b)) (∏ᶠ (b : β) (c : γ), f (a, b, c))
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
γ : Type u_7
f : α × β × γ → M
h : HasFiniteMulSupport f
a : α
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (b : β × γ), f (a, b)) (∏ᶠ (b : β) (c : γ), f (a, b, c))
have e_f : HasFiniteMulSupport (M := M) fun (b : β × γ) ↦ f (a, b)
Tactic: rw [finprod_curry]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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
⊢ 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)
have 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)
Tactic: simp_rw [← finprod_eq_dif]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (b : β) (h : b ∈ range f), g (Classical.choose (p := fun (x : α) ↦ f x = b) h))
    (∏ᶠ (a : α), g a)
have rw : ∀ (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 [finprod_dmem, finprod_mem_range hf, finprod_congr fun a => _]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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 : α
⊢ (if h' : f a ∈ range f then g (Classical.choose (p := fun (x : α) ↦ f x = f a) h') else 1) = g a
have rw : g (Classical.choose (p := fun (x : α) ↦ f x = f a) sorry) = g a
Tactic: rw [dif_pos (Set.mem_range_self a), hf (Classical.choose_spec (Set.mem_range_self a))]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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
⊢ (if h' : f a ∈ range f then g (Classical.choose (p := fun (x : α) ↦ f x = f a) h') else 1) = g a
have rw₁ : g a = g a
Tactic: rw [dif_pos (Set.mem_range_self a), hf (Classical.choose_spec (Set.mem_range_self a))]
-- 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 : ι → ℕ
⊢ Eq.{u_7 + 1} (α := R) (↑(∏ᶠ (x : ι), f x) : R) (∏ᶠ (x : ι), (↑(f x) : R))
have pos : ∀ (hf : HasFiniteMulSupport f), Eq.{u_7 + 1} (α := R) (↑(∏ᶠ (x : ι), f x) : R) (∏ᶠ (x : ι), (↑(f x) : R))
Tactic: by_cases hf : f.HasFiniteMulSupport
-- 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 : ι → ℕ
pos : ∀ (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))
have neg : ∀ (hf : ¬HasFiniteMulSupport f), Eq.{u_7 + 1} (α := R) (↑(∏ᶠ (x : ι), f x) : R) (∏ᶠ (x : ι), (↑(f x) : R))
Tactic: by_cases hf : f.HasFiniteMulSupport