no goals
α : Type u_1
β : Type ?u.211564
ι : Type ?u.211567
G : Type ?u.211570
M : Type u_2
N : Type ?u.211576
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hf : Set.Finite (mulSupport f)
hg : Set.Finite (mulSupport g)
⊢ (∏ᶠ (i : α), f i * g i) = (∏ᶠ (i : α), f i) * ∏ᶠ (i : α), g i
classical
  rw [finprod_eq_prod_of_mulSupport_toFinset_subset _ hf (Finset.subset_union_left _ _),
    finprod_eq_prod_of_mulSupport_toFinset_subset _ 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]
α : Type u_1
β : Type ?u.211564
ι : Type ?u.211567
G : Type ?u.211570
M : Type u_2
N : Type ?u.211576
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hf : Set.Finite (mulSupport f)
hg : Set.Finite (mulSupport g)
⊢ (∏ᶠ (i : α), f i * g i) = ∏ x in Finite.toFinset hf ∪ Finite.toFinset hg, f x * g x
α : Type u_1
β : Type ?u.211564
ι : Type ?u.211567
G : Type ?u.211570
M : Type u_2
N : Type ?u.211576
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hf : Set.Finite (mulSupport f)
hg : Set.Finite (mulSupport g)
⊢ (∏ᶠ (i : α), f i * g i) = (∏ᶠ (i : α), f i) * ∏ᶠ (i : α), g i
rw [finprod_eq_prod_of_mulSupport_toFinset_subset _ hf (Finset.subset_union_left _ _),
  finprod_eq_prod_of_mulSupport_toFinset_subset _ hg (Finset.subset_union_right _ _), ←
  Finset.prod_mul_distrib]
α : Type u_1
β : Type ?u.211564
ι : Type ?u.211567
G : Type ?u.211570
M : Type u_2
N : Type ?u.211576
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hf : Set.Finite (mulSupport f)
hg : Set.Finite (mulSupport g)
⊢ (mulSupport fun i => f i * g i) ⊆ ↑(Finite.toFinset hf ∪ Finite.toFinset hg)
α : Type u_1
β : Type ?u.211564
ι : Type ?u.211567
G : Type ?u.211570
M : Type u_2
N : Type ?u.211576
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hf : Set.Finite (mulSupport f)
hg : Set.Finite (mulSupport g)
⊢ (∏ᶠ (i : α), f i * g i) = ∏ x in Finite.toFinset hf ∪ Finite.toFinset hg, f x * g x
refine' finprod_eq_prod_of_mulSupport_subset _ _
α : Type u_1
β : Type ?u.211564
ι : Type ?u.211567
G : Type ?u.211570
M : Type u_2
N : Type ?u.211576
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hf : Set.Finite (mulSupport f)
hg : Set.Finite (mulSupport g)
⊢ ∀ (x : α), f x * g x ≠ 1 → f x ≠ 1 ∨ g x ≠ 1
α : Type u_1
β : Type ?u.211564
ι : Type ?u.211567
G : Type ?u.211570
M : Type u_2
N : Type ?u.211576
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hf : Set.Finite (mulSupport f)
hg : Set.Finite (mulSupport g)
⊢ (mulSupport fun i => f i * g i) ⊆ ↑(Finite.toFinset hf ∪ Finite.toFinset hg)
simp only [Finset.coe_union, Finite.coe_toFinset, mulSupport_subset_iff,
  mem_union, mem_mulSupport]
α : Type u_1
β : Type ?u.211564
ι : Type ?u.211567
G : Type ?u.211570
M : Type u_2
N : Type ?u.211576
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hf : Set.Finite (mulSupport f)
hg : Set.Finite (mulSupport g)
x : α
⊢ f x * g x ≠ 1 → f x ≠ 1 ∨ g x ≠ 1
α : Type u_1
β : Type ?u.211564
ι : Type ?u.211567
G : Type ?u.211570
M : Type u_2
N : Type ?u.211576
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hf : Set.Finite (mulSupport f)
hg : Set.Finite (mulSupport g)
⊢ ∀ (x : α), f x * g x ≠ 1 → f x ≠ 1 ∨ g x ≠ 1
intro x
α : Type u_1
β : Type ?u.211564
ι : Type ?u.211567
G : Type ?u.211570
M : Type u_2
N : Type ?u.211576
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hf : Set.Finite (mulSupport f)
hg : Set.Finite (mulSupport g)
x : α
⊢ f x = 1 ∧ g x = 1 → f x * g x = 1
α : Type u_1
β : Type ?u.211564
ι : Type ?u.211567
G : Type ?u.211570
M : Type u_2
N : Type ?u.211576
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hf : Set.Finite (mulSupport f)
hg : Set.Finite (mulSupport g)
x : α
⊢ f x * g x ≠ 1 → f x ≠ 1 ∨ g x ≠ 1
contrapose!
case intro
α : Type u_1
β : Type ?u.211564
ι : Type ?u.211567
G : Type ?u.211570
M : Type u_2
N : Type ?u.211576
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hf✝ : Set.Finite (mulSupport f)
hg✝ : Set.Finite (mulSupport g)
x : α
hf : f x = 1
hg : g x = 1
⊢ f x * g x = 1
α : Type u_1
β : Type ?u.211564
ι : Type ?u.211567
G : Type ?u.211570
M : Type u_2
N : Type ?u.211576
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hf : Set.Finite (mulSupport f)
hg : Set.Finite (mulSupport g)
x : α
⊢ f x = 1 ∧ g x = 1 → f x * g x = 1
rintro ⟨hf,hg⟩
no goals
case intro
α : Type u_1
β : Type ?u.211564
ι : Type ?u.211567
G : Type ?u.211570
M : Type u_2
N : Type ?u.211576
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hf✝ : Set.Finite (mulSupport f)
hg✝ : Set.Finite (mulSupport g)
x : α
hf : f x = 1
hg : g x = 1
⊢ f x * g x = 1
simp [hf, hg]