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 : α → M
s : Set α
rw : Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α), (s ∩ mulSupport f).mulIndicator f a) (∏ᶠ (i : α) (_ : i ∈ s), f i)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i) (∏ᶠ (i : α) (_ : i ∈ s), f i)
have rw₁ : Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α), (s ∩ mulSupport f).mulIndicator f a) (∏ᶠ (a : α), s.mulIndicator f a)
Tactic: rw [finprod_mem_def, finprod_mem_def, mulIndicator_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 : Set α
rw : Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α), (s ∩ mulSupport f).mulIndicator f a) (∏ᶠ (i : α) (_ : i ∈ s), f i)
rw₁ : Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α), (s ∩ mulSupport f).mulIndicator f a) (∏ᶠ (a : α), s.mulIndicator f a)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i) (∏ᶠ (i : α) (_ : i ∈ s), f i)
have rw₂ : Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α), s.mulIndicator f a) (∏ᶠ (a : α), s.mulIndicator f a)
Tactic: rw [finprod_mem_def, finprod_mem_def, mulIndicator_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 α
h : s ∩ mulSupport f = t ∩ mulSupport f
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
have rw : Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
Tactic: rw [← finprod_mem_inter_mulSupport, h, 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 α
h : s ∩ mulSupport f = t ∩ mulSupport f
rw : Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
have rw₁ : Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ t ∩ mulSupport f), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
Tactic: rw [← finprod_mem_inter_mulSupport, h, 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 α
h : s ∩ mulSupport f = t ∩ mulSupport f
rw : Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
rw₁ : Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ t ∩ mulSupport f), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
have rw₂ : Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ t), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
Tactic: rw [← finprod_mem_inter_mulSupport, h, 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 α
h : ∀ x ∈ mulSupport f, x ∈ s ↔ x ∈ t
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
have h₁ : s ∩ mulSupport f = t ∩ mulSupport f
Tactic: apply finprod_mem_inter_mulSupport_eq
-- 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 α
h : ∀ x ∈ mulSupport f, x ∈ s ↔ x ∈ t
⊢ s ∩ mulSupport f = t ∩ mulSupport f
have h₁ : ∀ (x : α), x ∈ s ∩ mulSupport f ↔ x ∈ t ∩ mulSupport f
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
ι : Type u_3
M : Type u_7
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
p : ι → Prop
h : ∀ (i : ι), p i → 1 ≤ f i
h' : ∃ (i : ι), p i ∧ 1 < f i
hf : (mulSupport f ∩ {i : ι | p i}).Finite
⊢ LT.lt.{u_7} (α := M) 1 (∏ᶠ (i : ι) (_ : p i), f i)
have rw : LT.lt.{u_7} (α := M) 1 (∏ i ∈ hf.toFinset (s := mulSupport f ∩ {i : ι | p i}), f i)
Tactic: rw [finprod_cond_eq_prod_of_cond_iff (t := hf.toFinset)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
ι : Type u_3
M : Type u_7
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
p : ι → Prop
h : ∀ (i : ι), p i → 1 ≤ f i
h' : ∃ (i : ι), p i ∧ 1 < f i
hf : (mulSupport f ∩ {i : ι | p i}).Finite
rw : LT.lt.{u_7} (α := M) 1 (∏ i ∈ hf.toFinset (s := mulSupport f ∩ {i : ι | p i}), f i)
⊢ LT.lt.{u_7} (α := M) 1 (∏ᶠ (i : ι) (_ : p i), f i)
have h₁ : ∀ {x : ι}, f x ≠ 1 → (p x ↔ x ∈ hf.toFinset (s := mulSupport f ∩ {i : ι | p i}))
Tactic: rw [finprod_cond_eq_prod_of_cond_iff (t := hf.toFinset)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
ι : Type u_3
M : Type u_7
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
p : ι → Prop
h : ∀ (i : ι), p i → 1 ≤ f i
h' : ∃ (i : ι), p i ∧ 1 < f i
hf : (mulSupport f ∩ {i : ι | p i}).Finite
⊢ LT.lt.{u_7} (α := M) 1 (∏ i ∈ hf.toFinset (s := mulSupport f ∩ {i : ι | p i}), f i)
have h₁ : ∀ i ∈ hf.toFinset (s := mulSupport f ∩ {i : ι | p i}), 1 ≤ f i
Tactic: apply Finset.one_lt_prod'
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
ι : Type u_3
M : Type u_7
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
p : ι → Prop
h : ∀ (i : ι), p i → 1 ≤ f i
h' : ∃ (i : ι), p i ∧ 1 < f i
hf : (mulSupport f ∩ {i : ι | p i}).Finite
h₁ : ∀ i ∈ hf.toFinset (s := mulSupport f ∩ {i : ι | p i}), 1 ≤ f i
⊢ LT.lt.{u_7} (α := M) 1 (∏ i ∈ hf.toFinset (s := mulSupport f ∩ {i : ι | p i}), f i)
have hs : ∃ i ∈ hf.toFinset (s := mulSupport f ∩ {i : ι | p i}), 1 < f i
Tactic: apply Finset.one_lt_prod'
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
ι : Type u_3
M : Type u_7
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ (i : ι), 1 < f i
hf : HasFiniteMulSupport f
⊢ LT.lt.{u_7} (α := M) 1 (∏ᶠ (i : ι), f i)
have rw : LT.lt.{u_7} (α := M) 1 (∏ᶠ (i : ι) (_ : Membership.mem (γ := Set ι) univ i), f i)
Tactic: rw [← finprod_mem_univ]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
ι : Type u_3
M : Type u_7
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ (i : ι), 1 < f i
hf : HasFiniteMulSupport f
⊢ LT.lt.{u_7} (α := M) 1 (∏ᶠ (i : ι) (_ : Membership.mem (γ := Set ι) univ i), f i)
have h₁ : ∀ (i : ι), Membership.mem (γ := Set ι) univ i → 1 ≤ f i
Tactic: apply one_lt_finprod_cond
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
ι : Type u_3
M : Type u_7
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ (i : ι), 1 < f i
hf : HasFiniteMulSupport f
h₁ : ∀ (i : ι), Membership.mem (γ := Set ι) univ i → 1 ≤ f i
⊢ LT.lt.{u_7} (α := M) 1 (∏ᶠ (i : ι) (_ : Membership.mem (γ := Set ι) univ i), f i)
have h'₁ : ∃ (i : ι), Membership.mem (γ := Set ι) univ i ∧ 1 < f i
Tactic: apply one_lt_finprod_cond
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
ι : Type u_3
M : Type u_7
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ (i : ι), 1 < f i
hf : HasFiniteMulSupport f
h₁ : ∀ (i : ι), Membership.mem (γ := Set ι) univ i → 1 ≤ f i
h'₁ : ∃ (i : ι), Membership.mem (γ := Set ι) univ i ∧ 1 < f i
⊢ LT.lt.{u_7} (α := M) 1 (∏ᶠ (i : ι) (_ : Membership.mem (γ := Set ι) univ i), f i)
have hf₁ : (mulSupport f ∩ {i : ι | Membership.mem (γ := Set ι) univ i}).Finite
Tactic: apply one_lt_finprod_cond
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f g : α → M
inst_1 : PartialOrder M
inst_2 : MulLeftMono M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
h : f ≤ g
⊢ LE.le.{u_5} (α := M) (∏ᶠ (a : α), f a) (∏ᶠ (a : α), g a)
have have : ∀ (this : Fintype (↑(mulSupport f ∪ mulSupport g) : Type u_1)), LE.le.{u_5} (α := M) (∏ᶠ (a : α), f a) (∏ᶠ (a : α), g a)
Tactic: have : Fintype ↑(f.mulSupport ∪ g.mulSupport) := (hf.union hg).fintype
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f g : α → M
inst_1 : PartialOrder M
inst_2 : MulLeftMono M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype (↑(mulSupport f ∪ mulSupport g) : Type u_1)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ LE.le.{u_5} (α := M) (∏ᶠ (a : α), f a) (∏ᶠ (a : α), g a)
have rw : LE.le.{u_5} (α := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
Tactic: rw [finprod_eq_finsetProd_of_mulSupport_subset f (show f.mulSupport ⊆ s by grind),
    finprod_eq_finsetProd_of_mulSupport_subset g (show g.mulSupport ⊆ s by grind)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_7
inst : CommMonoidWithZero M
inst_1 : PartialOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
f g : α → M
hf : HasFiniteMulSupport f
hf₀ : ∀ (a : α), 0 ≤ f a
hg : HasFiniteMulSupport g
h : f ≤ g
⊢ LE.le.{u_7} (α := M) (∏ᶠ (a : α), f a) (∏ᶠ (a : α), g a)
have have : ∀ (this : Fintype (↑(mulSupport f ∪ mulSupport g) : Type u_1)), LE.le.{u_7} (α := M) (∏ᶠ (a : α), f a) (∏ᶠ (a : α), g a)
Tactic: have : Fintype ↑(f.mulSupport ∪ g.mulSupport) := (hf.union hg).fintype
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_7
inst : CommMonoidWithZero M
inst_1 : PartialOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
f g : α → M
hf : HasFiniteMulSupport f
hf₀ : ∀ (a : α), 0 ≤ f a
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype (↑(mulSupport f ∪ mulSupport g) : Type u_1)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ LE.le.{u_7} (α := M) (∏ᶠ (a : α), f a) (∏ᶠ (a : α), g a)
have rw : LE.le.{u_7} (α := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
Tactic: rw [finprod_eq_finsetProd_of_mulSupport_subset f (show f.mulSupport ⊆ s by grind),
    finprod_eq_finsetProd_of_mulSupport_subset g (show g.mulSupport ⊆ s by grind)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
M : Type u_7
α : Type u_8
inst : CommMonoidWithZero M
inst_1 : PartialOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
⊢ LE.le.{u_7} (α := M) (∏ᶠ (x : α), 0) 1
have rw : LE.le.{u_7} (α := M) (∏ᶠ (x : α), 0) (∏ᶠ (x : α), 1)
Tactic: rw [← finprod_one (α := α)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
M : Type u_7
α : Type u_8
inst : CommMonoidWithZero M
inst_1 : PartialOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
⊢ LE.le.{u_7} (α := M) (∏ᶠ (x : α), 0) (∏ᶠ (x : α), 1)
have pos : ∀ (H : HasFiniteMulSupport.{u_8, u_7} (M := M) fun (x : α) ↦ 0), LE.le.{u_7} (α := M) (∏ᶠ (x : α), 0) (∏ᶠ (x : α), 1)
Tactic: by_cases H : (fun _ : α ↦ (0 : M)).HasFiniteMulSupport
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
M : Type u_7
α : Type u_8
inst : CommMonoidWithZero M
inst_1 : PartialOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
pos :
  ∀ (H : HasFiniteMulSupport.{u_8, u_7} (M := M) fun (x : α) ↦ 0), LE.le.{u_7} (α := M) (∏ᶠ (x : α), 0) (∏ᶠ (x : α), 1)
⊢ LE.le.{u_7} (α := M) (∏ᶠ (x : α), 0) (∏ᶠ (x : α), 1)
have neg : ∀ (H : ¬HasFiniteMulSupport.{u_8, u_7} (M := M) fun (x : α) ↦ 0), LE.le.{u_7} (α := M) (∏ᶠ (x : α), 0) (∏ᶠ (x : α), 1)
Tactic: by_cases H : (fun _ : α ↦ (0 : M)).HasFiniteMulSupport
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
M : Type u_7
α : Type u_8
inst : CommMonoidWithZero M
inst_1 : PartialOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
H : ¬HasFiniteMulSupport.{u_8, u_7} (M := M) fun (x : α) ↦ 0
⊢ LE.le.{u_7} (α := M) (∏ᶠ (x : α), 0) (∏ᶠ (x : α), 1)
have neg : LE.le.{u_7} (α := M) 1 (∏ᶠ (x : α), 1)
Tactic: rw [finprod_of_not_hasFiniteMulSupport H]
-- 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
⊢ ∏ᶠ (i : α), f i * g i = HMul.hMul (α := M) (∏ᶠ (i : α), f i) (∏ᶠ (i : α), g i)
have 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)
Tactic: 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]
-- 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
⊢ 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)
have refine : (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 α)
Tactic: refine finprod_eq_prod_of_mulSupport_subset _ ?_
-- 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
⊢ (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 α)
have simp : ∀ (x : α), f x * g x ≠ 1 → f x ≠ 1 ∨ g x ≠ 1
Tactic: simp only [Finset.coe_union, Finite.coe_toFinset, mulSupport_subset_iff,
      mem_union, mem_mulSupport]
-- 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
x : α
⊢ f x * g x ≠ 1 → f x ≠ 1 ∨ g x ≠ 1
have contrapose! : f x = 1 ∧ g x = 1 → f x * g x = 1
Tactic: contrapose!
-- 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
⊢ ∏ᶠ (i : α), f i * g i = HMul.hMul (α := M) (∏ᶠ (i : α), f i) (∏ᶠ (i : α), g i)
have 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)
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 (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)
⊢ ∏ᶠ (i : α), f i * g i = HMul.hMul (α := M) (∏ᶠ (i : α), f i) (∏ᶠ (i : α), g i)
have rw₁ : Finset α
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 (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 α
⊢ ∏ᶠ (i : α), f i * g i = HMul.hMul (α := M) (∏ᶠ (i : α), f i) (∏ᶠ (i : α), g i)
have 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)
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 (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 α
⊢ ∏ᶠ (i : α), f i * g i = HMul.hMul (α := M) (∏ᶠ (i : α), f i) (∏ᶠ (i : α), g i)
have 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)
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 (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)
⊢ ∏ᶠ (i : α), f i * g i = HMul.hMul (α := M) (∏ᶠ (i : α), f i) (∏ᶠ (i : α), g i)
have 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 α)
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 (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 α)
⊢ ∏ᶠ (i : α), f i * g i = HMul.hMul (α := M) (∏ᶠ (i : α), f i) (∏ᶠ (i : α), g i)
have rw₉ : ∀ (x : α), f x * g x ≠ 1 → f x ≠ 1 ∨ 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 (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
⊢ ∏ᶠ (i : α), f i * g i = HMul.hMul (α := M) (∏ᶠ (i : α), f i) (∏ᶠ (i : α), g i)
have rw₁₁ : ∀ (x : α), f x = 1 ∧ 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]