awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
rw :
  ∏ᶠ (i : α), f i * g i =
    HMul.hMul (α := M) (∏ i ∈ Finite.toFinset (s := mulSupport f) hf ∪ Finite.toFinset (s := mulSupport g) hg, f i)
      (∏ᶠ (i : α), g i)
rw₁ : Finset α
rw₂ :
  ∏ᶠ (i : α), f i * g i =
    HMul.hMul (α := M) (∏ i ∈ Finite.toFinset (s := mulSupport f) hf ∪ Finite.toFinset (s := mulSupport g) hg, f i)
      (∏ i ∈ Finite.toFinset (s := mulSupport f) hf ∪ Finite.toFinset (s := mulSupport g) hg, g i)
rw₃ rw₄ : Finset α
rw₅ rw₆ rw₇ :
  Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i * g i)
    (∏ x ∈ Finite.toFinset (s := mulSupport f) hf ∪ Finite.toFinset (s := mulSupport g) hg, f x * g x)
rw₈ :
  (mulSupport.{u_1, u_5} (M := M) fun (i : α) ↦ f i * g i) ⊆
    (↑(Finite.toFinset (s := mulSupport f) hf ∪ Finite.toFinset (s := mulSupport g) hg) : Set α)
rw₉ rw₁₀ : ∀ (x : α), f x * g x ≠ 1 → f x ≠ 1 ∨ g x ≠ 1
rw₁₁ : ∀ (x : α), f x = 1 ∧ g x = 1 → f x * g x = 1
⊢ ∏ᶠ (i : α), f i * g i = HMul.hMul (α := M) (∏ᶠ (i : α), f i) (∏ᶠ (i : α), g i)
have rw₁₂ : ∀ (x : α) (hf : f x = 1) (hg : g x = 1), f x * g x = 1
Tactic: classical
    rw [finprod_eq_prod_of_mulSupport_toFinset_subset f hf Finset.subset_union_left,
      finprod_eq_prod_of_mulSupport_toFinset_subset g hg Finset.subset_union_right, ←
      Finset.prod_mul_distrib]
    refine finprod_eq_prod_of_mulSupport_subset _ ?_
    simp only [Finset.coe_union, Finite.coe_toFinset, mulSupport_subset_iff,
      mem_union, mem_mulSupport]
    intro x
    contrapose!
    rintro ⟨hf, hg⟩
    simp [hf, hg]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (hypothesis)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f g : α → M
s : Set α
hf : (s ∩ mulSupport f).Finite
hg : (s ∩ mulSupport g).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i * g i = HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ s), g i)
have hf₁ : (mulSupport (s.mulIndicator f)).Finite
Tactic: rw [← mulSupport_mulIndicator] at hf hg
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (hypothesis)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f g : α → M
s : Set α
hf : (s ∩ mulSupport f).Finite
hg : (s ∩ mulSupport g).Finite
hf₁ : (mulSupport (s.mulIndicator f)).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i * g i = HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ s), g i)
have hg₁ : (mulSupport (s.mulIndicator g)).Finite
Tactic: rw [← mulSupport_mulIndicator] at hf hg
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
hf : EqOn f 1 s
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) 1
have rw : Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ s), 1)
Tactic: rw [← finprod_mem_one s]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
h : Ne.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) 1
⊢ ∃ x ∈ s, f x ≠ 1
have by_contra! : ∀ (h' : ∀ (x : α) (_ : x ∈ s), f x = 1), False
Tactic: by_contra! h'
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
N : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
s : Set α
f : α → M
g : M →* N
h₀ : (s ∩ mulSupport f).Finite
⊢ Eq.{u_6 + 1} (α := N) ((g : (a : M) → N) (∏ᶠ (j : α) (_ : j ∈ s), f j) : N)
    (∏ᶠ (i : α) (_ : i ∈ s), (g : (a : M) → N) (f i) : N)
have rw : Eq.{u_6 + 1} (α := N) (∏ᶠ (i : α), (g : (a : M) → N) (∏ᶠ (_ : i ∈ s), f i))
  (∏ᶠ (i : α) (_ : i ∈ s), (g : (a : M) → N) (f i))
Tactic: rw [g.map_finprod]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
N : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
s : Set α
f : α → M
g : M →* N
h₀ : (s ∩ mulSupport f).Finite
rw :
  Eq.{u_6 + 1} (α := N) (∏ᶠ (i : α), (g : (a : M) → N) (∏ᶠ (_ : i ∈ s), f i))
    (∏ᶠ (i : α) (_ : i ∈ s), (g : (a : M) → N) (f i))
⊢ Eq.{u_6 + 1} (α := N) ((g : (a : M) → N) (∏ᶠ (j : α) (_ : j ∈ s), f j) : N)
    (∏ᶠ (i : α) (_ : i ∈ s), (g : (a : M) → N) (f i) : N)
have rw₁ : HasFiniteMulSupport.{u_1, u_5} (M := M) fun (j : α) ↦ ∏ᶠ (_ : j ∈ s), f j
Tactic: rw [g.map_finprod]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
have lift : ∀ (s : Finset α),
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α) ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α) ∩ t), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
Tactic: lift s to Finset α using hs
Cleared hypotheses: s, hs
-- 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 α
ht : t.Finite
s : Finset α
⊢ HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α) ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α) ∩ t), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
have lift : ∀ (t : Finset α),
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α) ∪ (↑t : Set α)), f i)
      (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α) ∩ (↑t : Set α)), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)), f i) (∏ᶠ (i : α) (_ : i ∈ (↑t : Set α)), f i)
Tactic: lift t to Finset α using ht
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Finset α
⊢ HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α) ∪ (↑t : Set α)), f i)
      (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α) ∩ (↑t : Set α)), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)), f i) (∏ᶠ (i : α) (_ : i ∈ (↑t : Set α)), f i)
have rw : HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑(s ∪ t) : Set α)), f i) (∏ᶠ (i : α) (_ : i ∈ (↑(s ∩ t) : Set α)), f i) =
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)), f i) (∏ᶠ (i : α) (_ : i ∈ (↑t : Set α)), f i)
Tactic: rw [← Finset.coe_union, ← Finset.coe_inter]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Finset α
⊢ HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α) ∪ (↑t : Set α)), f i)
      (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α) ∩ (↑t : Set α)), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)), f i) (∏ᶠ (i : α) (_ : i ∈ (↑t : Set α)), f i)
have rw : HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑(s ∪ t) : Set α)), f i)
    (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α) ∩ (↑t : Set α)), f i) =
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)), f i) (∏ᶠ (i : α) (_ : i ∈ (↑t : Set α)), f i)
Tactic: classical
    rw [← Finset.coe_union, ← Finset.coe_inter]
    simp only [finprod_mem_coe_finset, Finset.prod_union_inter]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Finset α
rw :
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑(s ∪ t) : Set α)), f i)
      (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α) ∩ (↑t : Set α)), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)), f i) (∏ᶠ (i : α) (_ : i ∈ (↑t : Set α)), f i)
⊢ HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α) ∪ (↑t : Set α)), f i)
      (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α) ∩ (↑t : Set α)), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)), f i) (∏ᶠ (i : α) (_ : i ∈ (↑t : Set α)), f i)
have rw₁ : HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑(s ∪ t) : Set α)), f i) (∏ᶠ (i : α) (_ : i ∈ (↑(s ∩ t) : Set α)), f i) =
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)), f i) (∏ᶠ (i : α) (_ : i ∈ (↑t : Set α)), f i)
Tactic: classical
    rw [← Finset.coe_union, ← Finset.coe_inter]
    simp only [finprod_mem_coe_finset, Finset.prod_union_inter]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
have rw : HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ t ∩ mulSupport f), f i) =
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f ∩ (t ∩ mulSupport f)), f i)
Tactic: rw [← finprod_mem_inter_mulSupport f s, ← finprod_mem_inter_mulSupport f t, ←
    finprod_mem_union_inter hs ht, ← union_inter_distrib_right, finprod_mem_inter_mulSupport, ←
    finprod_mem_inter_mulSupport f (s ∩ t)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ t ∩ mulSupport f), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i)
      (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f ∩ (t ∩ mulSupport f)), f i)
have rw : HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ t ∩ mulSupport f), f i) =
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ t ∩ (s ∩ mulSupport f ∩ mulSupport f)), f i)
Tactic: rw [inter_left_comm, inter_assoc, inter_assoc, inter_self, inter_left_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
rw :
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ t ∩ mulSupport f), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i)
      (∏ᶠ (i : α) (_ : i ∈ t ∩ (s ∩ mulSupport f ∩ mulSupport f)), f i)
⊢ HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ t ∩ mulSupport f), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i)
      (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f ∩ (t ∩ mulSupport f)), f i)
have rw₁ : HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ (t ∩ mulSupport f)), f i) =
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ t ∩ (s ∩ mulSupport f ∩ mulSupport f)), f i)
Tactic: rw [inter_left_comm, inter_assoc, inter_assoc, inter_self, inter_left_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
rw :
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ t ∩ mulSupport f), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i)
      (∏ᶠ (i : α) (_ : i ∈ t ∩ (s ∩ mulSupport f ∩ mulSupport f)), f i)
rw₁ :
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ (t ∩ mulSupport f)), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i)
      (∏ᶠ (i : α) (_ : i ∈ t ∩ (s ∩ mulSupport f ∩ mulSupport f)), f i)
⊢ HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ t ∩ mulSupport f), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i)
      (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f ∩ (t ∩ mulSupport f)), f i)
have rw₂ : HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ (t ∩ mulSupport f)), f i) =
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i)
    (∏ᶠ (i : α) (_ : i ∈ t ∩ (s ∩ (mulSupport f ∩ mulSupport f))), f i)
Tactic: rw [inter_left_comm, inter_assoc, inter_assoc, inter_self, inter_left_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
rw :
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ t ∩ mulSupport f), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i)
      (∏ᶠ (i : α) (_ : i ∈ t ∩ (s ∩ mulSupport f ∩ mulSupport f)), f i)
rw₁ :
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ (t ∩ mulSupport f)), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i)
      (∏ᶠ (i : α) (_ : i ∈ t ∩ (s ∩ mulSupport f ∩ mulSupport f)), f i)
rw₂ :
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ (t ∩ mulSupport f)), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i)
      (∏ᶠ (i : α) (_ : i ∈ t ∩ (s ∩ (mulSupport f ∩ mulSupport f))), f i)
⊢ HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ t ∩ mulSupport f), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i)
      (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f ∩ (t ∩ mulSupport f)), f i)
have rw₃ : HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ (t ∩ mulSupport f)), f i) =
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ t ∩ (s ∩ mulSupport f)), f i)
Tactic: rw [inter_left_comm, inter_assoc, inter_assoc, inter_self, inter_left_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
rw :
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ t ∩ mulSupport f), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i)
      (∏ᶠ (i : α) (_ : i ∈ t ∩ (s ∩ mulSupport f ∩ mulSupport f)), f i)
rw₁ :
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ (t ∩ mulSupport f)), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i)
      (∏ᶠ (i : α) (_ : i ∈ t ∩ (s ∩ mulSupport f ∩ mulSupport f)), f i)
rw₂ :
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ (t ∩ mulSupport f)), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i)
      (∏ᶠ (i : α) (_ : i ∈ t ∩ (s ∩ (mulSupport f ∩ mulSupport f))), f i)
rw₃ :
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ (t ∩ mulSupport f)), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ t ∩ (s ∩ mulSupport f)), f i)
⊢ HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ t ∩ mulSupport f), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i)
      (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f ∩ (t ∩ mulSupport f)), f i)
have rw₄ : HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ t ∩ (s ∩ mulSupport f)), f i) =
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ t ∩ (s ∩ mulSupport f)), f i)
Tactic: rw [inter_left_comm, inter_assoc, inter_assoc, inter_self, inter_left_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
hst : Disjoint s t
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
have rw : ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i)
Tactic: rw [← finprod_mem_union_inter' hs ht, disjoint_iff_inter_eq_empty.1 hst, finprod_mem_empty,
    mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
hst : Disjoint s t
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
rw :
  ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i)
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
have rw₁ : ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i =
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : Membership.mem (γ := Set α) ∅ i), f i)
Tactic: rw [← finprod_mem_union_inter' hs ht, disjoint_iff_inter_eq_empty.1 hst, finprod_mem_empty,
    mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
hst : Disjoint s t
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
rw :
  ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i)
rw₁ :
  ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : Membership.mem (γ := Set α) ∅ i), f i)
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
have rw₂ : ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) 1
Tactic: rw [← finprod_mem_union_inter' hs ht, disjoint_iff_inter_eq_empty.1 hst, finprod_mem_empty,
    mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
hst : Disjoint s t
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
rw :
  ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i)
rw₁ :
  ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : Membership.mem (γ := Set α) ∅ i), f i)
rw₂ : ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) 1
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
have rw₃ : Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i)
Tactic: rw [← finprod_mem_union_inter' hs ht, disjoint_iff_inter_eq_empty.1 hst, finprod_mem_empty,
    mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
hst : Disjoint (s ∩ mulSupport f) (t ∩ mulSupport f)
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
have rw : ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i =
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
Tactic: rw [← finprod_mem_inter_mulSupport f s, ← finprod_mem_inter_mulSupport f t, ←
    finprod_mem_union hst hs ht, ← union_inter_distrib_right, finprod_mem_inter_mulSupport]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
hst : Disjoint (s ∩ mulSupport f) (t ∩ mulSupport f)
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
rw :
  ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
have rw₁ : ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i =
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i) (∏ᶠ (i : α) (_ : i ∈ t ∩ mulSupport f), f i)
Tactic: rw [← finprod_mem_inter_mulSupport f s, ← finprod_mem_inter_mulSupport f t, ←
    finprod_mem_union hst hs ht, ← union_inter_distrib_right, finprod_mem_inter_mulSupport]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
hst : Disjoint (s ∩ mulSupport f) (t ∩ mulSupport f)
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
rw :
  ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
rw₁ :
  ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i) (∏ᶠ (i : α) (_ : i ∈ t ∩ mulSupport f), f i)
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
have rw₂ : Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f ∪ t ∩ mulSupport f), f i)
Tactic: rw [← finprod_mem_inter_mulSupport f s, ← finprod_mem_inter_mulSupport f t, ←
    finprod_mem_union hst hs ht, ← union_inter_distrib_right, finprod_mem_inter_mulSupport]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
hst : Disjoint (s ∩ mulSupport f) (t ∩ mulSupport f)
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
rw :
  ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
rw₁ :
  ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i) (∏ᶠ (i : α) (_ : i ∈ t ∩ mulSupport f), f i)
rw₂ :
  Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i)
    (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f ∪ t ∩ mulSupport f), f i)
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
have rw₃ : Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ (s ∪ t) ∩ mulSupport f), f i)
Tactic: rw [← finprod_mem_inter_mulSupport f s, ← finprod_mem_inter_mulSupport f t, ←
    finprod_mem_union hst hs ht, ← union_inter_distrib_right, finprod_mem_inter_mulSupport]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
hst : Disjoint (s ∩ mulSupport f) (t ∩ mulSupport f)
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
rw :
  ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
rw₁ :
  ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i) (∏ᶠ (i : α) (_ : i ∈ t ∩ mulSupport f), f i)
rw₂ :
  Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i)
    (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f ∪ t ∩ mulSupport f), f i)
rw₃ : Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ (s ∪ t) ∩ mulSupport f), f i)
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
have rw₄ : Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i)
Tactic: rw [← finprod_mem_inter_mulSupport f s, ← finprod_mem_inter_mulSupport f t, ←
    finprod_mem_union hst hs ht, ← union_inter_distrib_right, finprod_mem_inter_mulSupport]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
⊢ ∏ᶠ (i : α) (_ : Membership.mem (γ := Set α) {a} i), f i = f a
have rw : ∏ᶠ (i : α) (_ : i ∈ (↑{a} : Set α)), f i = f a
Tactic: rw [← Finset.coe_singleton, finprod_mem_coe_finset, Finset.prod_singleton]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
rw : ∏ᶠ (i : α) (_ : i ∈ (↑{a} : Set α)), f i = f a
⊢ ∏ᶠ (i : α) (_ : Membership.mem (γ := Set α) {a} i), f i = f a
have rw₁ : ∏ i ∈ {a}, f i = f a
Tactic: rw [← Finset.coe_singleton, finprod_mem_coe_finset, Finset.prod_singleton]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
rw : ∏ᶠ (i : α) (_ : i ∈ (↑{a} : Set α)), f i = f a
rw₁ : ∏ i ∈ {a}, f i = f a
⊢ ∏ᶠ (i : α) (_ : Membership.mem (γ := Set α) {a} i), f i = f a
have rw₂ : f a = f a
Tactic: rw [← Finset.coe_singleton, finprod_mem_coe_finset, Finset.prod_singleton]