-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mul_distrib (hf : (mulSupport f).Finite) (hg : (mulSupport g).Finite) :
    ∏ᶠ i, f i * g i = (∏ᶠ i, f i) * ∏ᶠ i, g i

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : (mulSupport f).Finite
hg : (mulSupport g).Finite
⊢ (mulSupport fun i => f i * g i) ⊆ ↑(hf.toFinset ∪ hg.toFinset)

Tactic:
simp only [Finset.coe_union, Finite.coe_toFinset, mulSupport_subset_iff,
  mem_union, mem_mulSupport]

Result:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : (mulSupport f).Finite
hg : (mulSupport g).Finite
⊢ ∀ (x : α), f x * g x ≠ 1 → f x ≠ 1 ∨ g x ≠ 1

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : (mulSupport f).Finite
hg : (mulSupport g).Finite
x : α
⊢ f x * g x ≠ 1 → f x ≠ 1 ∨ g x ≠ 1

Tactic:
contrapose!

Result:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : (mulSupport f).Finite
hg : (mulSupport g).Finite
x : α
⊢ f x = 1 ∧ g x = 1 → f x * g x = 1

Proof state:
case intro
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf✝ : (mulSupport f).Finite
hg✝ : (mulSupport g).Finite
x : α
hf : f x = 1
hg : g x = 1
⊢ f x * g x = 1

Tactic:
simp [hf, hg]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : (mulSupport f).Finite
hg : (mulSupport g).Finite
⊢ ∏ᶠ (i : α), f i * g i = ∏ x ∈ hf.toFinset ∪ hg.toFinset, f x * g x

Tactic:
refine finprod_eq_prod_of_mulSupport_subset _ ?_

Result:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : (mulSupport f).Finite
hg : (mulSupport g).Finite
⊢ (mulSupport fun i => f i * g i) ⊆ ↑(hf.toFinset ∪ hg.toFinset)

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : (mulSupport f).Finite
hg : (mulSupport g).Finite
⊢ ∀ (x : α), f x * g x ≠ 1 → f x ≠ 1 ∨ g x ≠ 1

Tactic:
intro x

Result:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : (mulSupport f).Finite
hg : (mulSupport g).Finite
x : α
⊢ f x * g x ≠ 1 → f x ≠ 1 ∨ g x ≠ 1

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : (mulSupport f).Finite
hg : (mulSupport g).Finite
x : α
⊢ f x = 1 ∧ g x = 1 → f x * g x = 1

Tactic:
rintro ⟨hf, hg⟩

Result:
case intro
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf✝ : (mulSupport f).Finite
hg✝ : (mulSupport g).Finite
x : α
hf : f x = 1
hg : g x = 1
⊢ f x * g x = 1

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : (mulSupport f).Finite
hg : (mulSupport g).Finite
⊢ ∏ᶠ (i : α), f i * g i = (∏ᶠ (i : α), f i) * ∏ᶠ (i : α), g i

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]

Result:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : (mulSupport f).Finite
hg : (mulSupport g).Finite
⊢ ∏ᶠ (i : α), f i * g i = ∏ x ∈ hf.toFinset ∪ hg.toFinset, f x * g x

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : (mulSupport f).Finite
hg : (mulSupport g).Finite
⊢ ∏ᶠ (i : α), f i * g i = (∏ᶠ (i : α), 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]

Result:
no goals