awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
ι : Type u_3
M : Type u_5
inst : CommMonoid M
f : α → M
inst_1 : Finite ι
val : Fintype ι
t : (i : ι) → Finset α
h : Pairwise.{u_3} (α := ι) (onFun.{u_3 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : ι) ↦ (↑(t i) : Set α))
intro :
  Eq.{u_5 + 1} (α := M)
    (∏ᶠ (a : α) (_ :
      Membership.mem (γ := Set α) (⋃ (x : ι), ⋃ (_ : Membership.mem (γ := Set ι) univ x), (↑(t x) : Set α)) a), f a)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
⊢ Eq.{u_5 + 1} (α := M)
    (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ (i : ι), (fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
have intro₁ : Eq.{u_5 + 1} (α := M)
  (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ x ∈ (↑Finset.univ : Set ι), (↑(t x) : Set α)) a), f a)
  (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
Tactic: classical
    rw [← biUnion_univ, ← Finset.coe_univ, ← Finset.coe_biUnion, finprod_mem_coe_finset,
      Finset.prod_biUnion]
    · simp only [finprod_mem_coe_finset, finprod_eq_prod_of_fintype]
    · exact fun x _ y _ hxy => Finset.disjoint_coe.1 (h hxy)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
ι : Type u_3
M : Type u_5
inst : CommMonoid M
f : α → M
inst_1 : Finite ι
val : Fintype ι
t : (i : ι) → Finset α
h : Pairwise.{u_3} (α := ι) (onFun.{u_3 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : ι) ↦ (↑(t i) : Set α))
intro :
  Eq.{u_5 + 1} (α := M)
    (∏ᶠ (a : α) (_ :
      Membership.mem (γ := Set α) (⋃ (x : ι), ⋃ (_ : Membership.mem (γ := Set ι) univ x), (↑(t x) : Set α)) a), f a)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
intro₁ :
  Eq.{u_5 + 1} (α := M)
    (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ x ∈ (↑Finset.univ : Set ι), (↑(t x) : Set α)) a), f a)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
⊢ Eq.{u_5 + 1} (α := M)
    (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ (i : ι), (fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
have intro₂ : Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (_ : a ∈ (↑(Finset.biUnion Finset.univ t) : Set α)), f a)
  (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
Tactic: classical
    rw [← biUnion_univ, ← Finset.coe_univ, ← Finset.coe_biUnion, finprod_mem_coe_finset,
      Finset.prod_biUnion]
    · simp only [finprod_mem_coe_finset, finprod_eq_prod_of_fintype]
    · exact fun x _ y _ hxy => Finset.disjoint_coe.1 (h hxy)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
ι : Type u_3
M : Type u_5
inst : CommMonoid M
f : α → M
inst_1 : Finite ι
val : Fintype ι
t : (i : ι) → Finset α
h : Pairwise.{u_3} (α := ι) (onFun.{u_3 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : ι) ↦ (↑(t i) : Set α))
intro :
  Eq.{u_5 + 1} (α := M)
    (∏ᶠ (a : α) (_ :
      Membership.mem (γ := Set α) (⋃ (x : ι), ⋃ (_ : Membership.mem (γ := Set ι) univ x), (↑(t x) : Set α)) a), f a)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
intro₁ :
  Eq.{u_5 + 1} (α := M)
    (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ x ∈ (↑Finset.univ : Set ι), (↑(t x) : Set α)) a), f a)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
intro₂ :
  Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (_ : a ∈ (↑(Finset.biUnion Finset.univ t) : Set α)), f a)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
⊢ Eq.{u_5 + 1} (α := M)
    (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ (i : ι), (fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
have intro₃ : Eq.{u_5 + 1} (α := M) (∏ i ∈ Finset.biUnion Finset.univ t, f i)
  (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
Tactic: classical
    rw [← biUnion_univ, ← Finset.coe_univ, ← Finset.coe_biUnion, finprod_mem_coe_finset,
      Finset.prod_biUnion]
    · simp only [finprod_mem_coe_finset, finprod_eq_prod_of_fintype]
    · exact fun x _ y _ hxy => Finset.disjoint_coe.1 (h hxy)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
ι : Type u_3
M : Type u_5
inst : CommMonoid M
f : α → M
inst_1 : Finite ι
val : Fintype ι
t : (i : ι) → Finset α
h : Pairwise.{u_3} (α := ι) (onFun.{u_3 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : ι) ↦ (↑(t i) : Set α))
intro :
  Eq.{u_5 + 1} (α := M)
    (∏ᶠ (a : α) (_ :
      Membership.mem (γ := Set α) (⋃ (x : ι), ⋃ (_ : Membership.mem (γ := Set ι) univ x), (↑(t x) : Set α)) a), f a)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
intro₁ :
  Eq.{u_5 + 1} (α := M)
    (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ x ∈ (↑Finset.univ : Set ι), (↑(t x) : Set α)) a), f a)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
intro₂ :
  Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (_ : a ∈ (↑(Finset.biUnion Finset.univ t) : Set α)), f a)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
intro₃ :
  Eq.{u_5 + 1} (α := M) (∏ i ∈ Finset.biUnion Finset.univ t, f i)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
⊢ Eq.{u_5 + 1} (α := M)
    (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ (i : ι), (fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
have intro₄ : Eq.{u_5 + 1} (α := M) (∏ x : ι, ∏ i ∈ t x, f i)
  (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
Tactic: classical
    rw [← biUnion_univ, ← Finset.coe_univ, ← Finset.coe_biUnion, finprod_mem_coe_finset,
      Finset.prod_biUnion]
    · simp only [finprod_mem_coe_finset, finprod_eq_prod_of_fintype]
    · exact fun x _ y _ hxy => Finset.disjoint_coe.1 (h hxy)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
ι : Type u_3
M : Type u_5
inst : CommMonoid M
f : α → M
inst_1 : Finite ι
val : Fintype ι
t : (i : ι) → Finset α
h : Pairwise.{u_3} (α := ι) (onFun.{u_3 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : ι) ↦ (↑(t i) : Set α))
intro :
  Eq.{u_5 + 1} (α := M)
    (∏ᶠ (a : α) (_ :
      Membership.mem (γ := Set α) (⋃ (x : ι), ⋃ (_ : Membership.mem (γ := Set ι) univ x), (↑(t x) : Set α)) a), f a)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
intro₁ :
  Eq.{u_5 + 1} (α := M)
    (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ x ∈ (↑Finset.univ : Set ι), (↑(t x) : Set α)) a), f a)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
intro₂ :
  Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (_ : a ∈ (↑(Finset.biUnion Finset.univ t) : Set α)), f a)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
intro₃ :
  Eq.{u_5 + 1} (α := M) (∏ i ∈ Finset.biUnion Finset.univ t, f i)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
intro₄ :
  Eq.{u_5 + 1} (α := M) (∏ x : ι, ∏ i ∈ t x, f i)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
⊢ Eq.{u_5 + 1} (α := M)
    (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ (i : ι), (fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
have intro₅ : (↑Finset.univ : Set ι).PairwiseDisjoint t
Tactic: classical
    rw [← biUnion_univ, ← Finset.coe_univ, ← Finset.coe_biUnion, finprod_mem_coe_finset,
      Finset.prod_biUnion]
    · simp only [finprod_mem_coe_finset, finprod_eq_prod_of_fintype]
    · exact fun x _ y _ hxy => Finset.disjoint_coe.1 (h hxy)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
ι : Type u_3
M : Type u_5
inst : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ x ∈ I, t x) a), f a)
    (∏ᶠ (i : ι) (_ : i ∈ I) (j : α) (_ : j ∈ t i), f j)
have haveI : ∀ (this : Fintype (↑I : Type u_3)),
  Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ x ∈ I, t x) a), f a)
    (∏ᶠ (i : ι) (_ : i ∈ I) (j : α) (_ : j ∈ t i), f j)
Tactic: haveI := hI.fintype
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
ι : Type u_3
M : Type u_5
inst : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
this : Fintype (↑I : Type u_3)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ x ∈ I, t x) a), f a)
    (∏ᶠ (i : ι) (_ : i ∈ I) (j : α) (_ : j ∈ t i), f j)
have h₁ : Pairwise.{u_3} (α := (↑I : Type u_3))
  (onFun.{u_3 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (x : (↑I : Type u_3)) ↦ t (↑x : ι))
Tactic: rw [biUnion_eq_iUnion, finprod_mem_iUnion, ← finprod_set_coe_eq_finprod_mem]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
ι : Type u_3
M : Type u_5
inst : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
this : Fintype (↑I : Type u_3)
h₁ :
  Pairwise.{u_3} (α := (↑I : Type u_3))
    (onFun.{u_3 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (x : (↑I : Type u_3)) ↦ t (↑x : ι))
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ x ∈ I, t x) a), f a)
    (∏ᶠ (i : ι) (_ : i ∈ I) (j : α) (_ : j ∈ t i), f j)
have ht₁ : ∀ (i : (↑I : Type u_3)), (t (↑i : ι)).Finite
Tactic: rw [biUnion_eq_iUnion, finprod_mem_iUnion, ← finprod_set_coe_eq_finprod_mem]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
t : Set (Set α)
h : t.PairwiseDisjoint id
ht₀ : t.Finite
ht₁ : ∀ x ∈ t, x.Finite
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (_ : a ∈ ⋃₀ t), f a) (∏ᶠ (s : Set α) (_ : s ∈ t) (a : α) (_ : a ∈ s), f a)
have rw : Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ i ∈ t, i) a), f a)
  (∏ᶠ (s : Set α) (_ : s ∈ t) (a : α) (_ : a ∈ s), f a)
Tactic: rw [Set.sUnion_eq_biUnion]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (hypothesis)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : Option α → M
hf : HasFiniteMulSupport (f ∘ some)
⊢ ∏ᶠ (o : Option α), f o = f none * ∏ᶠ (a : α), f (some a)
have hf₁ : (mulSupport f).Finite
Tactic: replace hf : (mulSupport f).Finite := by simpa [finite_option]
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
⊢ ∏ᶠ (o : Option α), f o = f none * ∏ᶠ (a : α), f (some a)
have h : ∀ (x : Option α), f x = ∏ᶠ (_ : Membership.mem (γ := Set (Option α)) (insert none (range some)) x), f x
Tactic: convert!
    finprod_mem_insert' f (show none ∉ Set.range Option.some by simp) (hf.subset inter_subset_right)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
h : ∀ (x : Option α), f x = ∏ᶠ (_ : Membership.mem (γ := Set (Option α)) (insert none (range some)) x), f x
⊢ ∏ᶠ (o : Option α), f o = f none * ∏ᶠ (a : α), f (some a)
have h₁ : Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α), f (some a))
  (∏ᶠ (i : Option α) (_ : Membership.mem (γ := Set (Option α)) (range some) i), f i)
Tactic: convert!
    finprod_mem_insert' f (show none ∉ Set.range Option.some by simp) (hf.subset inter_subset_right)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α), f (some a))
    (∏ᶠ (i : Option α) (_ : Membership.mem (γ := Set (Option α)) (range some) i), f i)
have h : Injective.{u_1 + 1, u_1 + 1} (α := α) some
Tactic: rw [finprod_mem_range]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : Set α → M
s : Set α
a : α
hs : s.Finite
has : a ∉ s
⊢ ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 insert a s), f t =
    HMul.hMul (α := M) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f (insert a t))
have rw : ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s ∪ insert a '' 𝒫 s), f t =
  HMul.hMul (α := M) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f (insert a t))
Tactic: rw [Set.powerset_insert,
    finprod_mem_union (disjoint_powerset_insert has) hs.powerset (hs.powerset.image (insert a)),
    finprod_mem_image (powerset_insert_injOn has)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : Set α → M
s : Set α
a : α
hs : s.Finite
has : a ∉ s
rw :
  ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s ∪ insert a '' 𝒫 s), f t =
    HMul.hMul (α := M) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f (insert a t))
⊢ ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 insert a s), f t =
    HMul.hMul (α := M) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f (insert a t))
have rw₁ : HMul.hMul (α := M) (∏ᶠ (i : Set α) (_ : i ∈ 𝒫 s), f i) (∏ᶠ (i : Set α) (_ : i ∈ insert a '' 𝒫 s), f i) =
  HMul.hMul (α := M) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f (insert a t))
Tactic: rw [Set.powerset_insert,
    finprod_mem_union (disjoint_powerset_insert has) hs.powerset (hs.powerset.image (insert a)),
    finprod_mem_image (powerset_insert_injOn has)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : Set α → M
s : Set α
a : α
hs : s.Finite
has : a ∉ s
rw :
  ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s ∪ insert a '' 𝒫 s), f t =
    HMul.hMul (α := M) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f (insert a t))
rw₁ :
  HMul.hMul (α := M) (∏ᶠ (i : Set α) (_ : i ∈ 𝒫 s), f i) (∏ᶠ (i : Set α) (_ : i ∈ insert a '' 𝒫 s), f i) =
    HMul.hMul (α := M) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f (insert a t))
⊢ ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 insert a s), f t =
    HMul.hMul (α := M) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f (insert a t))
have rw₂ : HMul.hMul (α := M) (∏ᶠ (i : Set α) (_ : i ∈ 𝒫 s), f i) (∏ᶠ (j : Set α) (_ : j ∈ 𝒫 s), f (insert a j)) =
  HMul.hMul (α := M) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f (insert a t))
Tactic: rw [Set.powerset_insert,
    finprod_mem_union (disjoint_powerset_insert has) hs.powerset (hs.powerset.image (insert a)),
    finprod_mem_image (powerset_insert_injOn has)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : Set α → M
s : Set α
a : α
hs : s.Finite
has : a ∈ s
⊢ ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t =
    HMul.hMul (α := M) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f t)
      (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f (insert a t))
have nth_rw : ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 insert a (s \ {a})), f t =
  HMul.hMul (α := M) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f t) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f (insert a t))
Tactic: nth_rw 1 2 [← Set.insert_diff_self_of_mem has]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ᶠ (i : α), f i
have rw : f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
Tactic: rw [finprod_eq_prod _ hf]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a}
have rw : x ≠ a ↔ f x ≠ 1 ∧ ¬x = a
Tactic: rw [Finset.mem_sdiff, Finset.mem_singleton, Finite.mem_toFinset, mem_mulSupport]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (hypothesis)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
have h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a})
Tactic: have h : ∀ x : α, f x ≠ 1 → (x ≠ a ↔ x ∈ hf.toFinset \ {a}) := by
      intro x hx
      rw [Finset.mem_sdiff, Finset.mem_singleton, Finite.mem_toFinset, mem_mulSupport]
      grind
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a})
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
have rw : f a * ∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
Tactic: rw [finprod_cond_eq_prod_of_cond_iff f (fun hx => h _ hx), Finset.sdiff_singleton_eq_erase]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a})
⊢ f a * ∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
have pos : ∀ (ha : a ∈ mulSupport f),
  f a * ∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
Tactic: by_cases ha : a ∈ mulSupport f
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a})
pos :
  ∀ (ha : a ∈ mulSupport f),
    f a * ∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i =
      ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
⊢ f a * ∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
have neg : ∀ (ha : a ∉ mulSupport f),
  f a * ∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
Tactic: by_cases ha : a ∈ mulSupport f
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (hypothesis)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a})
ha : a ∉ mulSupport f
⊢ f a * ∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
have ha₁ : f a = 1
Tactic: rw [mem_mulSupport, not_not] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a})
ha : f a = 1
⊢ f a * ∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
have neg : Eq.{u_5 + 1} (α := M) (∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i)
  (∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i)
Tactic: rw [ha, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ᶠ (i : α), f i
have rw : f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
Tactic: classical
    rw [finprod_eq_prod _ hf]
    have h : ∀ x : α, f x ≠ 1 → (x ≠ a ↔ x ∈ hf.toFinset \ {a}) := by
      intro x hx
      rw [Finset.mem_sdiff, Finset.mem_singleton, Finite.mem_toFinset, mem_mulSupport]
      grind
    rw [finprod_cond_eq_prod_of_cond_iff f (fun hx => h _ hx), Finset.sdiff_singleton_eq_erase]
    by_cases ha : a ∈ mulSupport f
    · apply Finset.mul_prod_erase _ _ ((Finite.mem_toFinset _).mpr ha)
    · rw [mem_mulSupport, not_not] at ha
      rw [ha, one_mul]
      apply Finset.prod_erase _ ha
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
rw rw₁ rw₂ : f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ᶠ (i : α), f i
have rw₃ : ∀ (h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a})),
  f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
Tactic: classical
    rw [finprod_eq_prod _ hf]
    have h : ∀ x : α, f x ≠ 1 → (x ≠ a ↔ x ∈ hf.toFinset \ {a}) := by
      intro x hx
      rw [Finset.mem_sdiff, Finset.mem_singleton, Finite.mem_toFinset, mem_mulSupport]
      grind
    rw [finprod_cond_eq_prod_of_cond_iff f (fun hx => h _ hx), Finset.sdiff_singleton_eq_erase]
    by_cases ha : a ∈ mulSupport f
    · apply Finset.mul_prod_erase _ _ ((Finite.mem_toFinset _).mpr ha)
    · rw [mem_mulSupport, not_not] at ha
      rw [ha, one_mul]
      apply Finset.prod_erase _ ha
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
rw rw₁ rw₂ : f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
rw₃ :
  ∀ (h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a})),
    f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ᶠ (i : α), f i
have rw₄ : ∀ (h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a})),
  f a * ∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
Tactic: classical
    rw [finprod_eq_prod _ hf]
    have h : ∀ x : α, f x ≠ 1 → (x ≠ a ↔ x ∈ hf.toFinset \ {a}) := by
      intro x hx
      rw [Finset.mem_sdiff, Finset.mem_singleton, Finite.mem_toFinset, mem_mulSupport]
      grind
    rw [finprod_cond_eq_prod_of_cond_iff f (fun hx => h _ hx), Finset.sdiff_singleton_eq_erase]
    by_cases ha : a ∈ mulSupport f
    · apply Finset.mul_prod_erase _ _ ((Finite.mem_toFinset _).mpr ha)
    · rw [mem_mulSupport, not_not] at ha
      rw [ha, one_mul]
      apply Finset.prod_erase _ ha