[GOAL]
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
hf : Set.Finite (mulSupport (f ∘ PLift.down))
s : Finset (PLift α)
hs : Finite.toFinset hf ⊆ s
⊢ ∏ᶠ (i : α), f i = ∏ i in s, f i.down
[PROOFSTEP]
rw [finprod, dif_pos]
[GOAL]
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
hf : Set.Finite (mulSupport (f ∘ PLift.down))
s : Finset (PLift α)
hs : Finite.toFinset hf ⊆ s
⊢ ∏ i in Finite.toFinset ?hc, f i.down = ∏ i in s, f i.down
case hc
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
hf : Set.Finite (mulSupport (f ∘ PLift.down))
s : Finset (PLift α)
hs : Finite.toFinset hf ⊆ s
⊢ Set.Finite (mulSupport ((fun i => f i) ∘ PLift.down))
[PROOFSTEP]
refine' Finset.prod_subset hs fun x _ hxf => _
[GOAL]
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
hf : Set.Finite (mulSupport (f ∘ PLift.down))
s : Finset (PLift α)
hs : Finite.toFinset hf ⊆ s
x : PLift α
x✝ : x ∈ s
hxf : ¬x ∈ Finite.toFinset hf
⊢ f x.down = 1
[PROOFSTEP]
rwa [hf.mem_toFinset, nmem_mulSupport] at hxf 
[GOAL]
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset (PLift α)
hs : mulSupport (f ∘ PLift.down) ⊆ ↑s
x : PLift α
hx : x ∈ Finite.toFinset (_ : Set.Finite (mulSupport (f ∘ PLift.down)))
⊢ x ∈ s
[PROOFSTEP]
rw [Finite.mem_toFinset] at hx 
[GOAL]
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset (PLift α)
hs : mulSupport (f ∘ PLift.down) ⊆ ↑s
x : PLift α
hx : x ∈ mulSupport (f ∘ PLift.down)
⊢ x ∈ s
[PROOFSTEP]
exact hs hx
[GOAL]
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
⊢ ∏ᶠ (x : α), 1 = 1
[PROOFSTEP]
have : (mulSupport fun x : PLift α => (fun _ => 1 : α → M) x.down) ⊆ (∅ : Finset (PLift α)) := fun x h => by simp at h 
[GOAL]
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
x : PLift α
h : x ∈ mulSupport fun x => (fun x => 1) x.down
⊢ x ∈ ↑∅
[PROOFSTEP]
simp at h 
[GOAL]
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
this : (mulSupport fun x => (fun x => 1) x.down) ⊆ ↑∅
⊢ ∏ᶠ (x : α), 1 = 1
[PROOFSTEP]
rw [finprod_eq_prod_pLift_of_mulSupport_subset this, Finset.prod_empty]
[GOAL]
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : IsEmpty α
f : α → M
⊢ ∏ᶠ (i : α), f i = 1
[PROOFSTEP]
rw [← finprod_one]
[GOAL]
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : IsEmpty α
f : α → M
⊢ ∏ᶠ (i : α), f i = ∏ᶠ (x : ?m.32760), 1
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : IsEmpty α
f : α → M
⊢ Sort ?u.32758
[PROOFSTEP]
congr
[GOAL]
case e_f
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : IsEmpty α
f : α → M
⊢ (fun i => f i) = fun x => 1
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
⊢ ∏ᶠ (x : α), f x = f a
[PROOFSTEP]
have : mulSupport (f ∘ PLift.down) ⊆ ({PLift.up a} : Finset (PLift α)) :=
  by
  intro x
  contrapose
  simpa [PLift.eq_up_iff_down_eq] using ha x.down
[GOAL]
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
⊢ mulSupport (f ∘ PLift.down) ⊆ ↑{{ down := a }}
[PROOFSTEP]
intro x
[GOAL]
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
x : PLift α
⊢ x ∈ mulSupport (f ∘ PLift.down) → x ∈ ↑{{ down := a }}
[PROOFSTEP]
contrapose
[GOAL]
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
x : PLift α
⊢ ¬x ∈ ↑{{ down := a }} → ¬x ∈ mulSupport (f ∘ PLift.down)
[PROOFSTEP]
simpa [PLift.eq_up_iff_down_eq] using ha x.down
[GOAL]
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
this : mulSupport (f ∘ PLift.down) ⊆ ↑{{ down := a }}
⊢ ∏ᶠ (x : α), f x = f a
[PROOFSTEP]
rw [finprod_eq_prod_pLift_of_mulSupport_subset this, Finset.prod_singleton]
[GOAL]
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
p : Prop
inst✝ : Decidable p
f : p → M
⊢ ∏ᶠ (i : p), f i = if h : p then f h else 1
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
p : Prop
inst✝ : Decidable p
f : p → M
h : p
⊢ ∏ᶠ (i : p), f i = f h
[PROOFSTEP]
haveI : Unique p := ⟨⟨h⟩, fun _ => rfl⟩
[GOAL]
case pos
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
p : Prop
inst✝ : Decidable p
f : p → M
h : p
this : Unique p
⊢ ∏ᶠ (i : p), f i = f h
[PROOFSTEP]
exact finprod_unique f
[GOAL]
case neg
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
p : Prop
inst✝ : Decidable p
f : p → M
h : ¬p
⊢ ∏ᶠ (i : p), f i = 1
[PROOFSTEP]
haveI : IsEmpty p := ⟨h⟩
[GOAL]
case neg
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
p : Prop
inst✝ : Decidable p
f : p → M
h : ¬p
this : IsEmpty p
⊢ ∏ᶠ (i : p), f i = 1
[PROOFSTEP]
exact finprod_of_isEmpty f
[GOAL]
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
p q : Prop
f : p → M
g : q → M
hpq : p = q
hfg : ∀ (h : q), f (_ : p) = g h
⊢ finprod f = finprod g
[PROOFSTEP]
subst q
[GOAL]
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
p : Prop
f g : p → M
hfg : ∀ (h : p), f (_ : p) = g h
⊢ finprod f = finprod g
[PROOFSTEP]
exact finprod_congr hfg
[GOAL]
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
⊢ p (∏ᶠ (i : α), f i)
[PROOFSTEP]
rw [finprod]
[GOAL]
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
⊢ p (if h : Set.Finite (mulSupport ((fun i => f i) ∘ PLift.down)) then ∏ i in Finite.toFinset h, f i.down else 1)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
h✝ : Set.Finite (mulSupport ((fun i => f i) ∘ PLift.down))
⊢ p (∏ i in Finite.toFinset h✝, f i.down)
case neg
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
h✝ : ¬Set.Finite (mulSupport ((fun i => f i) ∘ PLift.down))
⊢ p 1
[PROOFSTEP]
exacts [Finset.prod_induction _ _ hp₁ hp₀ fun i _ => hp₂ _, hp₀]
[GOAL]
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
g : α → M
h : Set.Finite (mulSupport (g ∘ PLift.down))
⊢ ↑f (∏ᶠ (x : α), g x) = ∏ᶠ (x : α), ↑f (g x)
[PROOFSTEP]
rw [finprod_eq_prod_pLift_of_mulSupport_subset h.coe_toFinset.ge, finprod_eq_prod_pLift_of_mulSupport_subset,
  f.map_prod]
[GOAL]
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
g : α → M
h : Set.Finite (mulSupport (g ∘ PLift.down))
⊢ mulSupport ((fun x => ↑f (g x)) ∘ PLift.down) ⊆ ↑(Finite.toFinset h)
[PROOFSTEP]
rw [h.coe_toFinset]
[GOAL]
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
g : α → M
h : Set.Finite (mulSupport (g ∘ PLift.down))
⊢ mulSupport ((fun x => ↑f (g x)) ∘ PLift.down) ⊆ mulSupport (g ∘ PLift.down)
[PROOFSTEP]
exact mulSupport_comp_subset f.map_one (g ∘ PLift.down)
[GOAL]
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), ↑f x = 1 → x = 1
g : α → M
⊢ ↑f (∏ᶠ (i : α), g i) = ∏ᶠ (i : α), ↑f (g i)
[PROOFSTEP]
by_cases hg : (mulSupport <| g ∘ PLift.down).Finite
[GOAL]
case pos
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), ↑f x = 1 → x = 1
g : α → M
hg : Set.Finite (mulSupport (g ∘ PLift.down))
⊢ ↑f (∏ᶠ (i : α), g i) = ∏ᶠ (i : α), ↑f (g i)
[PROOFSTEP]
exact f.map_finprod_pLift g hg
[GOAL]
case neg
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), ↑f x = 1 → x = 1
g : α → M
hg : ¬Set.Finite (mulSupport (g ∘ PLift.down))
⊢ ↑f (∏ᶠ (i : α), g i) = ∏ᶠ (i : α), ↑f (g i)
[PROOFSTEP]
rw [finprod, dif_neg, f.map_one, finprod, dif_neg]
[GOAL]
case neg.hnc
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), ↑f x = 1 → x = 1
g : α → M
hg : ¬Set.Finite (mulSupport (g ∘ PLift.down))
⊢ ¬Set.Finite (mulSupport ((fun i => ↑f (g i)) ∘ PLift.down))
case neg.hnc
G : Type u_1
M : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), ↑f x = 1 → x = 1
g : α → M
hg : ¬Set.Finite (mulSupport (g ∘ PLift.down))
⊢ ¬Set.Finite (mulSupport ((fun i => g i) ∘ PLift.down))
[PROOFSTEP]
exacts [Infinite.mono (fun x hx => mt (hf (g x.down)) hx) hg, hg]
[GOAL]
G : Type u_1
M✝ : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝⁵ : CommMonoid M✝
inst✝⁴ : CommMonoid N
R : Type u_7
M : Type u_8
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : ι → R
x : M
⊢ (∑ᶠ (i : ι), f i) • x = ∑ᶠ (i : ι), f i • x
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | hx)
[GOAL]
case inl
G : Type u_1
M✝ : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝⁵ : CommMonoid M✝
inst✝⁴ : CommMonoid N
R : Type u_7
M : Type u_8
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : ι → R
⊢ (∑ᶠ (i : ι), f i) • 0 = ∑ᶠ (i : ι), f i • 0
[PROOFSTEP]
simp
[GOAL]
case inr
G : Type u_1
M✝ : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝⁵ : CommMonoid M✝
inst✝⁴ : CommMonoid N
R : Type u_7
M : Type u_8
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : ι → R
x : M
hx : x ≠ 0
⊢ (∑ᶠ (i : ι), f i) • x = ∑ᶠ (i : ι), f i • x
[PROOFSTEP]
exact ((smulAddHom R M).flip x).map_finsum_of_injective (smul_left_injective R hx) _
[GOAL]
G : Type u_1
M✝ : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝⁵ : CommMonoid M✝
inst✝⁴ : CommMonoid N
R : Type u_7
M : Type u_8
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
c : R
f : ι → M
⊢ c • ∑ᶠ (i : ι), f i = ∑ᶠ (i : ι), c • f i
[PROOFSTEP]
rcases eq_or_ne c 0 with (rfl | hc)
[GOAL]
case inl
G : Type u_1
M✝ : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝⁵ : CommMonoid M✝
inst✝⁴ : CommMonoid N
R : Type u_7
M : Type u_8
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : ι → M
⊢ 0 • ∑ᶠ (i : ι), f i = ∑ᶠ (i : ι), 0 • f i
[PROOFSTEP]
simp
[GOAL]
case inr
G : Type u_1
M✝ : Type u_2
N : Type u_3
α : Sort u_4
β : Sort u_5
ι : Sort u_6
inst✝⁵ : CommMonoid M✝
inst✝⁴ : CommMonoid N
R : Type u_7
M : Type u_8
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
c : R
f : ι → M
hc : c ≠ 0
⊢ c • ∑ᶠ (i : ι), f i = ∑ᶠ (i : ι), c • f i
[PROOFSTEP]
exact (smulAddHom R M c).map_finsum_of_injective (smul_right_injective M hc) _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
s : Set α
f : α → M
a : α
⊢ ∏ᶠ (_ : a ∈ s), f a = mulIndicator s f a
[PROOFSTEP]
classical convert finprod_eq_if (M := M) (p := a ∈ s) (x := f a)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
s : Set α
f : α → M
a : α
⊢ ∏ᶠ (_ : a ∈ s), f a = mulIndicator s f a
[PROOFSTEP]
convert finprod_eq_if (M := M) (p := a ∈ s) (x := f a)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
a : α
⊢ ∏ᶠ (_ : f a ≠ 1), f a = f a
[PROOFSTEP]
rw [← mem_mulSupport, finprod_eq_mulIndicator_apply, mulIndicator_mulSupport]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
⊢ ∏ᶠ (i : α), f i = ∏ i in s, f i
[PROOFSTEP]
have A : mulSupport (f ∘ PLift.down) = Equiv.plift.symm '' mulSupport f :=
  by
  rw [mulSupport_comp_eq_preimage]
  exact (Equiv.plift.symm.image_eq_preimage _).symm
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
⊢ mulSupport (f ∘ PLift.down) = ↑Equiv.plift.symm '' mulSupport f
[PROOFSTEP]
rw [mulSupport_comp_eq_preimage]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
⊢ PLift.down ⁻¹' mulSupport f = ↑Equiv.plift.symm '' mulSupport f
[PROOFSTEP]
exact (Equiv.plift.symm.image_eq_preimage _).symm
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ↑Equiv.plift.symm '' mulSupport f
⊢ ∏ᶠ (i : α), f i = ∏ i in s, f i
[PROOFSTEP]
have : mulSupport (f ∘ PLift.down) ⊆ s.map Equiv.plift.symm.toEmbedding :=
  by
  rw [A, Finset.coe_map]
  exact image_subset _ h
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ↑Equiv.plift.symm '' mulSupport f
⊢ mulSupport (f ∘ PLift.down) ⊆ ↑(Finset.map (Equiv.toEmbedding Equiv.plift.symm) s)
[PROOFSTEP]
rw [A, Finset.coe_map]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ↑Equiv.plift.symm '' mulSupport f
⊢ ↑Equiv.plift.symm '' mulSupport f ⊆ ↑(Equiv.toEmbedding Equiv.plift.symm) '' ↑s
[PROOFSTEP]
exact image_subset _ h
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ↑Equiv.plift.symm '' mulSupport f
this : mulSupport (f ∘ PLift.down) ⊆ ↑(Finset.map (Equiv.toEmbedding Equiv.plift.symm) s)
⊢ ∏ᶠ (i : α), f i = ∏ i in s, f i
[PROOFSTEP]
rw [finprod_eq_prod_pLift_of_mulSupport_subset this]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ↑Equiv.plift.symm '' mulSupport f
this : mulSupport (f ∘ PLift.down) ⊆ ↑(Finset.map (Equiv.toEmbedding Equiv.plift.symm) s)
⊢ ∏ i in Finset.map (Equiv.toEmbedding Equiv.plift.symm) s, f i.down = ∏ i in s, f i
[PROOFSTEP]
simp only [Finset.prod_map, Equiv.coe_toEmbedding]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ↑Equiv.plift.symm '' mulSupport f
this : mulSupport (f ∘ PLift.down) ⊆ ↑(Finset.map (Equiv.toEmbedding Equiv.plift.symm) s)
⊢ ∏ x in s, f (↑Equiv.plift.symm x).down = ∏ i in s, f i
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
⊢ Finite.toFinset (_ : Set.Finite (mulSupport f)) ⊆ s
[PROOFSTEP]
simpa [← Finset.coe_subset, Set.coe_toFinset]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f : α → M
inst✝ : Decidable (Set.Finite (mulSupport f))
⊢ ∏ᶠ (i : α), f i = if h : Set.Finite (mulSupport f) then ∏ i in Finite.toFinset h, f i else 1
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f : α → M
inst✝ : Decidable (Set.Finite (mulSupport f))
h : Set.Finite (mulSupport f)
⊢ ∏ᶠ (i : α), f i = ∏ i in Finite.toFinset h, f i
[PROOFSTEP]
exact finprod_eq_prod_of_mulSupport_toFinset_subset _ h (Finset.Subset.refl _)
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f : α → M
inst✝ : Decidable (Set.Finite (mulSupport f))
h : ¬Set.Finite (mulSupport f)
⊢ ∏ᶠ (i : α), f i = 1
[PROOFSTEP]
rw [finprod, dif_neg]
[GOAL]
case neg.hnc
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f : α → M
inst✝ : Decidable (Set.Finite (mulSupport f))
h : ¬Set.Finite (mulSupport f)
⊢ ¬Set.Finite (mulSupport ((fun i => f i) ∘ PLift.down))
[PROOFSTEP]
rw [mulSupport_comp_eq_preimage]
[GOAL]
case neg.hnc
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f : α → M
inst✝ : Decidable (Set.Finite (mulSupport f))
h : ¬Set.Finite (mulSupport f)
⊢ ¬Set.Finite (PLift.down ⁻¹' mulSupport fun i => f i)
[PROOFSTEP]
exact mt (fun hf => hf.of_preimage Equiv.plift.surjective) h
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
hf : Set.Infinite (mulSupport f)
⊢ ∏ᶠ (i : α), f i = 1
[PROOFSTEP]
classical rw [finprod_def, dif_neg hf]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
hf : Set.Infinite (mulSupport f)
⊢ ∏ᶠ (i : α), f i = 1
[PROOFSTEP]
rw [finprod_def, dif_neg hf]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
hf : Set.Finite (mulSupport f)
⊢ ∏ᶠ (i : α), f i = ∏ i in Finite.toFinset hf, f i
[PROOFSTEP]
classical rw [finprod_def, dif_pos hf]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
hf : Set.Finite (mulSupport f)
⊢ ∏ᶠ (i : α), f i = ∏ i in Finite.toFinset hf, f i
[PROOFSTEP]
rw [finprod_def, dif_pos hf]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
⊢ ∏ᶠ (i : α) (_ : p i), f i = ∏ i in t, f i
[PROOFSTEP]
set s := {x | p x}
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
⊢ ∏ᶠ (i : α) (_ : p i), f i = ∏ i in t, f i
[PROOFSTEP]
have : mulSupport (s.mulIndicator f) ⊆ t :=
  by
  rw [Set.mulSupport_mulIndicator]
  intro x hx
  exact (h hx.2).1 hx.1
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
⊢ mulSupport (mulIndicator s f) ⊆ ↑t
[PROOFSTEP]
rw [Set.mulSupport_mulIndicator]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
⊢ s ∩ mulSupport f ⊆ ↑t
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
x : α
hx : x ∈ s ∩ mulSupport f
⊢ x ∈ ↑t
[PROOFSTEP]
exact (h hx.2).1 hx.1
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
this : mulSupport (mulIndicator s f) ⊆ ↑t
⊢ ∏ᶠ (i : α) (_ : p i), f i = ∏ i in t, f i
[PROOFSTEP]
erw [finprod_mem_def, finprod_eq_prod_of_mulSupport_subset _ this]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
this : mulSupport (mulIndicator s f) ⊆ ↑t
⊢ ∏ i in t, mulIndicator s f i = ∏ i in t, f i
[PROOFSTEP]
refine' Finset.prod_congr rfl fun x hx => mulIndicator_apply_eq_self.2 fun hxs => _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
this : mulSupport (mulIndicator s f) ⊆ ↑t
x : α
hx : x ∈ t
hxs : ¬x ∈ s
⊢ f x = 1
[PROOFSTEP]
contrapose! hxs
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
this : mulSupport (mulIndicator s f) ⊆ ↑t
x : α
hx : x ∈ t
hxs : f x ≠ 1
⊢ x ∈ {x | p x}
[PROOFSTEP]
exact (h hxs).2 hx
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f : α → M
a : α
inst✝ : DecidableEq α
hf : Set.Finite (mulSupport f)
⊢ ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i in Finset.erase (Finite.toFinset hf) a, f i
[PROOFSTEP]
apply finprod_cond_eq_prod_of_cond_iff
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f : α → M
a : α
inst✝ : DecidableEq α
hf : Set.Finite (mulSupport f)
⊢ ∀ {x : α}, f x ≠ 1 → (x ≠ a ↔ x ∈ Finset.erase (Finite.toFinset hf) a)
[PROOFSTEP]
intro x hx
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f : α → M
a : α
inst✝ : DecidableEq α
hf : Set.Finite (mulSupport f)
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ x ∈ Finset.erase (Finite.toFinset hf) a
[PROOFSTEP]
rw [Finset.mem_erase, Finite.mem_toFinset, mem_mulSupport]
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f : α → M
a : α
inst✝ : DecidableEq α
hf : Set.Finite (mulSupport f)
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ x ≠ a ∧ f x ≠ 1
[PROOFSTEP]
exact ⟨fun h => And.intro h hx, fun h => h.1⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
⊢ ∀ {x : α}, f x ≠ 1 → (x ∈ s ↔ x ∈ t)
[PROOFSTEP]
intro x hxf
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : f x ≠ 1
⊢ x ∈ s ↔ x ∈ t
[PROOFSTEP]
rw [← mem_mulSupport] at hxf 
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
⊢ x ∈ s ↔ x ∈ t
[PROOFSTEP]
refine ⟨fun hx => ?_, fun hx => ?_⟩
[GOAL]
case refine_1
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ s
⊢ x ∈ t
[PROOFSTEP]
refine ((mem_inter_iff x t (mulSupport f)).mp ?_).1
[GOAL]
case refine_1
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ s
⊢ x ∈ ↑t ∩ mulSupport f
[PROOFSTEP]
rw [← Set.ext_iff.mp h x, mem_inter_iff]
[GOAL]
case refine_1
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ s
⊢ x ∈ s ∧ x ∈ mulSupport f
[PROOFSTEP]
exact ⟨hx, hxf⟩
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ t
⊢ x ∈ s
[PROOFSTEP]
refine ((mem_inter_iff x s (mulSupport f)).mp ?_).1
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ t
⊢ x ∈ s ∩ mulSupport f
[PROOFSTEP]
rw [Set.ext_iff.mp h x, mem_inter_iff]
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ t
⊢ x ∈ ↑t ∧ x ∈ mulSupport f
[PROOFSTEP]
exact ⟨hx, hxf⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
hf : Set.Finite (s ∩ mulSupport f)
⊢ (s ∩ mulSupport fun i => f i) = ↑(Finite.toFinset hf) ∩ mulSupport fun i => f i
[PROOFSTEP]
simp [inter_assoc]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f : α → M
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hf : Set.Finite (mulSupport f)
⊢ (s ∩ mulSupport fun i => f i) = ↑(Finset.filter (fun x => x ∈ s) (Finite.toFinset hf)) ∩ mulSupport fun i => f i
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f : α → M
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hf : Set.Finite (mulSupport f)
x : α
⊢ (x ∈ s ∩ mulSupport fun i => f i) ↔
    x ∈ ↑(Finset.filter (fun x => x ∈ s) (Finite.toFinset hf)) ∩ mulSupport fun i => f i
[PROOFSTEP]
simp [and_comm]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f : α → M
s : Set α
inst✝ : Fintype ↑s
⊢ (s ∩ mulSupport fun i => f i) = ↑(toFinset s) ∩ mulSupport fun i => f i
[PROOFSTEP]
simp_rw [coe_toFinset s]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
hs : Set.Finite s
⊢ (s ∩ mulSupport fun i => f i) = ↑(Finite.toFinset hs) ∩ mulSupport fun i => f i
[PROOFSTEP]
rw [hs.coe_toFinset]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
hs : Set.Infinite (s ∩ mulSupport f)
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = 1
[PROOFSTEP]
rw [finprod_mem_def]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
hs : Set.Infinite (s ∩ mulSupport f)
⊢ ∏ᶠ (a : α), mulIndicator s (fun i => f i) a = 1
[PROOFSTEP]
apply finprod_of_infinite_mulSupport
[GOAL]
case hf
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
hs : Set.Infinite (s ∩ mulSupport f)
⊢ Set.Infinite (mulSupport fun i => mulIndicator s (fun i => f i) i)
[PROOFSTEP]
rwa [← mulSupport_mulIndicator] at hs 
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
h : ∀ (x : α), x ∈ s → f x = 1
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = 1
[PROOFSTEP]
simp (config := { contextual := true }) [h]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i
[PROOFSTEP]
rw [finprod_mem_def, finprod_mem_def, mulIndicator_inter_mulSupport]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s t : Set α
h : s ∩ mulSupport f = t ∩ mulSupport f
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i
[PROOFSTEP]
rw [← finprod_mem_inter_mulSupport, h, finprod_mem_inter_mulSupport]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s t : Set α
h : ∀ (x : α), x ∈ mulSupport f → (x ∈ s ↔ x ∈ t)
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i
[PROOFSTEP]
apply finprod_mem_inter_mulSupport_eq
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s t : Set α
h : ∀ (x : α), x ∈ mulSupport f → (x ∈ s ↔ x ∈ t)
⊢ (s ∩ mulSupport fun i => f i) = t ∩ mulSupport fun i => f i
[PROOFSTEP]
ext x
[GOAL]
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s t : Set α
h : ∀ (x : α), x ∈ mulSupport f → (x ∈ s ↔ x ∈ t)
x : α
⊢ (x ∈ s ∩ mulSupport fun i => f i) ↔ x ∈ t ∩ mulSupport fun i => f i
[PROOFSTEP]
exact and_congr_left (h x)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
f : α → M
h : ∀ (x : α), f x = 1
⊢ ∏ᶠ (i : α), f i = 1
[PROOFSTEP]
simp (config := { contextual := true }) [h]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M✝ : Type u_5
N : Type u_6
inst✝² : CommMonoid M✝
inst✝¹ : CommMonoid N
f✝ g : α → M✝
a b : α
s t : Set α
M : Type u_7
inst✝ : OrderedCancelCommMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ i, 1 < f i
hf : Set.Finite (mulSupport f)
⊢ 1 < ∏ᶠ (i : ι), f i
[PROOFSTEP]
rcases h' with ⟨i, hi⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M✝ : Type u_5
N : Type u_6
inst✝² : CommMonoid M✝
inst✝¹ : CommMonoid N
f✝ g : α → M✝
a b : α
s t : Set α
M : Type u_7
inst✝ : OrderedCancelCommMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
hf : Set.Finite (mulSupport f)
i : ι
hi : 1 < f i
⊢ 1 < ∏ᶠ (i : ι), f i
[PROOFSTEP]
rw [finprod_eq_prod _ hf]
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M✝ : Type u_5
N : Type u_6
inst✝² : CommMonoid M✝
inst✝¹ : CommMonoid N
f✝ g : α → M✝
a b : α
s t : Set α
M : Type u_7
inst✝ : OrderedCancelCommMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
hf : Set.Finite (mulSupport f)
i : ι
hi : 1 < f i
⊢ 1 < ∏ i in Finite.toFinset hf, f i
[PROOFSTEP]
refine Finset.one_lt_prod' (fun i _ ↦ h i) ⟨i, ?_, hi⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M✝ : Type u_5
N : Type u_6
inst✝² : CommMonoid M✝
inst✝¹ : CommMonoid N
f✝ g : α → M✝
a b : α
s t : Set α
M : Type u_7
inst✝ : OrderedCancelCommMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
hf : Set.Finite (mulSupport f)
i : ι
hi : 1 < f i
⊢ i ∈ Finite.toFinset hf
[PROOFSTEP]
simpa only [Finite.mem_toFinset, mem_mulSupport] using ne_of_gt hi
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
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
[PROOFSTEP]
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]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
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
[PROOFSTEP]
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]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
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
[PROOFSTEP]
refine' finprod_eq_prod_of_mulSupport_subset _ _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
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)
[PROOFSTEP]
simp only [Finset.coe_union, Finite.coe_toFinset, mulSupport_subset_iff, mem_union, mem_mulSupport]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
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
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
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
[PROOFSTEP]
contrapose!
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
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
[PROOFSTEP]
rintro ⟨hf, hg⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
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
[PROOFSTEP]
simp [hf, hg]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a b : α
s t : Set α
inst✝ : DivisionCommMonoid G
f g : α → G
hf : Set.Finite (mulSupport f)
hg : Set.Finite (mulSupport g)
⊢ ∏ᶠ (i : α), f i / g i = (∏ᶠ (i : α), f i) / ∏ᶠ (i : α), g i
[PROOFSTEP]
simp only [div_eq_mul_inv, finprod_mul_distrib hf ((mulSupport_inv g).symm.rec hg), finprod_inv_distrib]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hf : Set.Finite (s ∩ mulSupport f)
hg : Set.Finite (s ∩ mulSupport g)
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i * g i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ s), g i
[PROOFSTEP]
rw [← mulSupport_mulIndicator] at hf hg 
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hf : Set.Finite (mulSupport (mulIndicator s f))
hg : Set.Finite (mulSupport (mulIndicator s g))
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i * g i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ s), g i
[PROOFSTEP]
simp only [finprod_mem_def, mulIndicator_mul, finprod_mul_distrib hf hg]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s✝ t s : Set α
⊢ ∏ᶠ (i : α) (_ : i ∈ s), 1 = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hf : EqOn f 1 s
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = 1
[PROOFSTEP]
rw [← finprod_mem_one s]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hf : EqOn f 1 s
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (i : α) (_ : i ∈ s), 1
[PROOFSTEP]
exact finprod_mem_congr rfl hf
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
h : ∏ᶠ (i : α) (_ : i ∈ s), f i ≠ 1
⊢ ∃ x, x ∈ s ∧ f x ≠ 1
[PROOFSTEP]
by_contra' h'
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
h : ∏ᶠ (i : α) (_ : i ∈ s), f i ≠ 1
h' : ∀ (x : α), x ∈ s → f x = 1
⊢ False
[PROOFSTEP]
exact h (finprod_mem_of_eqOn_one h')
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g✝ : α → M
a b : α
s t : Set α
f : α → M
g : M →* N
h₀ : Set.Finite (s ∩ mulSupport f)
⊢ ↑g (∏ᶠ (j : α) (_ : j ∈ s), f j) = ∏ᶠ (i : α) (_ : i ∈ s), ↑g (f i)
[PROOFSTEP]
rw [g.map_finprod]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g✝ : α → M
a b : α
s t : Set α
f : α → M
g : M →* N
h₀ : Set.Finite (s ∩ mulSupport f)
⊢ ∏ᶠ (i : α), ↑g (∏ᶠ (_ : i ∈ s), f i) = ∏ᶠ (i : α) (_ : i ∈ s), ↑g (f i)
[PROOFSTEP]
simp only [g.map_finprod_Prop]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g✝ : α → M
a b : α
s t : Set α
f : α → M
g : M →* N
h₀ : Set.Finite (s ∩ mulSupport f)
⊢ Set.Finite (mulSupport fun j => ∏ᶠ (_ : j ∈ s), f j)
[PROOFSTEP]
simpa only [finprod_eq_mulIndicator_apply, mulSupport_mulIndicator]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a b : α
s t : Set α
inst✝ : DivisionCommMonoid G
f g : α → G
hs : Set.Finite s
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i / g i = (∏ᶠ (i : α) (_ : i ∈ s), f i) / ∏ᶠ (i : α) (_ : i ∈ s), g i
[PROOFSTEP]
simp only [div_eq_mul_inv, finprod_mem_mul_distrib hs, finprod_mem_inv_distrib g hs]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
⊢ ∏ᶠ (i : α) (_ : i ∈ ∅), f i = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hs : Set.Finite s
ht : Set.Finite t
⊢ (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i =
    (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
[PROOFSTEP]
lift s to Finset α using hs
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
t : Set α
ht : Set.Finite t
s : Finset α
⊢ (∏ᶠ (i : α) (_ : i ∈ ↑s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑s ∩ t), f i =
    (∏ᶠ (i : α) (_ : i ∈ ↑s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
[PROOFSTEP]
lift t to Finset α using ht
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Finset α
⊢ (∏ᶠ (i : α) (_ : i ∈ ↑s ∪ ↑t), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑s ∩ ↑t), f i =
    (∏ᶠ (i : α) (_ : i ∈ ↑s), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑t), f i
[PROOFSTEP]
classical
rw [← Finset.coe_union, ← Finset.coe_inter]
simp only [finprod_mem_coe_finset, Finset.prod_union_inter]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Finset α
⊢ (∏ᶠ (i : α) (_ : i ∈ ↑s ∪ ↑t), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑s ∩ ↑t), f i =
    (∏ᶠ (i : α) (_ : i ∈ ↑s), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑t), f i
[PROOFSTEP]
rw [← Finset.coe_union, ← Finset.coe_inter]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Finset α
⊢ (∏ᶠ (i : α) (_ : i ∈ ↑(s ∪ t)), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑(s ∩ t)), f i =
    (∏ᶠ (i : α) (_ : i ∈ ↑s), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑t), f i
[PROOFSTEP]
simp only [finprod_mem_coe_finset, Finset.prod_union_inter]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hs : Set.Finite (s ∩ mulSupport f)
ht : Set.Finite (t ∩ mulSupport f)
⊢ (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i =
    (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
[PROOFSTEP]
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)]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hs : Set.Finite (s ∩ mulSupport f)
ht : Set.Finite (t ∩ mulSupport f)
⊢ (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t ∩ mulSupport f), f i =
    (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f ∩ (t ∩ mulSupport f)), f i
[PROOFSTEP]
congr 2
[GOAL]
case e_a.e_f
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hs : Set.Finite (s ∩ mulSupport f)
ht : Set.Finite (t ∩ mulSupport f)
⊢ (fun i => ∏ᶠ (_ : i ∈ s ∩ t ∩ mulSupport f), f i) = fun i => ∏ᶠ (_ : i ∈ s ∩ mulSupport f ∩ (t ∩ mulSupport f)), f i
[PROOFSTEP]
rw [inter_left_comm, inter_assoc, inter_assoc, inter_self, inter_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hst : Disjoint s t
hs : Set.Finite (s ∩ mulSupport f)
ht : Set.Finite (t ∩ mulSupport f)
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
[PROOFSTEP]
rw [← finprod_mem_union_inter' hs ht, disjoint_iff_inter_eq_empty.1 hst, finprod_mem_empty, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hst : Disjoint (s ∩ mulSupport f) (t ∩ mulSupport f)
hs : Set.Finite (s ∩ mulSupport f)
ht : Set.Finite (t ∩ mulSupport f)
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
[PROOFSTEP]
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]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
⊢ ∏ᶠ (i : α) (_ : i ∈ {a}), f i = f a
[PROOFSTEP]
rw [← Finset.coe_singleton, finprod_mem_coe_finset, Finset.prod_singleton]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
⊢ ∏ᶠ (i : α) (_ : a = i), f i = f a
[PROOFSTEP]
simp [@eq_comm _ a]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
f : α → M
h : ¬a ∈ s
hs : Set.Finite (s ∩ mulSupport f)
⊢ ∏ᶠ (i : α) (_ : i ∈ insert a s), f i = f a * ∏ᶠ (i : α) (_ : i ∈ s), f i
[PROOFSTEP]
rw [insert_eq, finprod_mem_union' _ _ hs, finprod_mem_singleton]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
f : α → M
h : ¬a ∈ s
hs : Set.Finite (s ∩ mulSupport f)
⊢ Disjoint {a} s
[PROOFSTEP]
rwa [disjoint_singleton_left]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
f : α → M
h : ¬a ∈ s
hs : Set.Finite (s ∩ mulSupport f)
⊢ Set.Finite ({a} ∩ mulSupport f)
[PROOFSTEP]
exact (finite_singleton a).inter_of_left _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
h : ¬a ∈ s → f a = 1
⊢ ∏ᶠ (i : α) (_ : i ∈ insert a s), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i
[PROOFSTEP]
refine' finprod_mem_inter_mulSupport_eq' _ _ _ fun x hx => ⟨_, Or.inr⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
h : ¬a ∈ s → f a = 1
x : α
hx : x ∈ mulSupport fun i => f i
⊢ x ∈ insert a s → x ∈ s
[PROOFSTEP]
rintro (rfl | hxs)
[GOAL]
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
b : α
s t : Set α
x : α
hx : x ∈ mulSupport fun i => f i
h : ¬x ∈ s → f x = 1
⊢ x ∈ s
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
h : ¬a ∈ s → f a = 1
x : α
hx : x ∈ mulSupport fun i => f i
hxs : x ∈ s
⊢ x ∈ s
[PROOFSTEP]
exacts [not_imp_comm.1 h hx, hxs]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a✝ b : α
s t : Set α
f : α → N
a : α
hf : Set.Finite (mulSupport f)
⊢ f a ∣ finprod f
[PROOFSTEP]
by_cases ha : a ∈ mulSupport f
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a✝ b : α
s t : Set α
f : α → N
a : α
hf : Set.Finite (mulSupport f)
ha : a ∈ mulSupport f
⊢ f a ∣ finprod f
[PROOFSTEP]
rw [finprod_eq_prod_of_mulSupport_toFinset_subset f hf (Set.Subset.refl _)]
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a✝ b : α
s t : Set α
f : α → N
a : α
hf : Set.Finite (mulSupport f)
ha : a ∈ mulSupport f
⊢ f a ∣ ∏ i in Finite.toFinset hf, f i
[PROOFSTEP]
exact Finset.dvd_prod_of_mem f ((Finite.mem_toFinset hf).mpr ha)
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a✝ b : α
s t : Set α
f : α → N
a : α
hf : Set.Finite (mulSupport f)
ha : ¬a ∈ mulSupport f
⊢ f a ∣ finprod f
[PROOFSTEP]
rw [nmem_mulSupport.mp ha]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a✝ b : α
s t : Set α
f : α → N
a : α
hf : Set.Finite (mulSupport f)
ha : ¬a ∈ mulSupport f
⊢ 1 ∣ finprod f
[PROOFSTEP]
exact one_dvd (finprod f)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
h : a ≠ b
⊢ ∏ᶠ (i : α) (_ : i ∈ {a, b}), f i = f a * f b
[PROOFSTEP]
rw [finprod_mem_insert, finprod_mem_singleton]
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
h : a ≠ b
⊢ ¬a ∈ {b}
case hs
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
h : a ≠ b
⊢ Set.Finite {b}
[PROOFSTEP]
exacts [h, finite_singleton b]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
⊢ ∏ᶠ (i : α) (_ : i ∈ g '' s), f i = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)
[PROOFSTEP]
classical
by_cases hs : (s ∩ mulSupport (f ∘ g)).Finite
· have hg : ∀ x ∈ hs.toFinset, ∀ y ∈ hs.toFinset, g x = g y → x = y := by simpa only [hs.mem_toFinset]
  have := finprod_mem_eq_prod (comp f g) hs
  unfold Function.comp at this 
  rw [this, ← Finset.prod_image hg]
  refine' finprod_mem_eq_prod_of_inter_mulSupport_eq f _
  rw [Finset.coe_image, hs.coe_toFinset, ← image_inter_mulSupport_eq, inter_assoc, inter_self]
· unfold Function.comp at hs 
  rw [finprod_mem_eq_one_of_infinite hs, finprod_mem_eq_one_of_infinite]
  rwa [image_inter_mulSupport_eq, infinite_image_iff hg]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
⊢ ∏ᶠ (i : α) (_ : i ∈ g '' s), f i = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)
[PROOFSTEP]
by_cases hs : (s ∩ mulSupport (f ∘ g)).Finite
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
hs : Set.Finite (s ∩ mulSupport (f ∘ g))
⊢ ∏ᶠ (i : α) (_ : i ∈ g '' s), f i = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)
[PROOFSTEP]
have hg : ∀ x ∈ hs.toFinset, ∀ y ∈ hs.toFinset, g x = g y → x = y := by simpa only [hs.mem_toFinset]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
hs : Set.Finite (s ∩ mulSupport (f ∘ g))
⊢ ∀ (x : β), x ∈ Finite.toFinset hs → ∀ (y : β), y ∈ Finite.toFinset hs → g x = g y → x = y
[PROOFSTEP]
simpa only [hs.mem_toFinset]
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg✝ : InjOn g (s ∩ mulSupport (f ∘ g))
hs : Set.Finite (s ∩ mulSupport (f ∘ g))
hg : ∀ (x : β), x ∈ Finite.toFinset hs → ∀ (y : β), y ∈ Finite.toFinset hs → g x = g y → x = y
⊢ ∏ᶠ (i : α) (_ : i ∈ g '' s), f i = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)
[PROOFSTEP]
have := finprod_mem_eq_prod (comp f g) hs
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg✝ : InjOn g (s ∩ mulSupport (f ∘ g))
hs : Set.Finite (s ∩ mulSupport (f ∘ g))
hg : ∀ (x : β), x ∈ Finite.toFinset hs → ∀ (y : β), y ∈ Finite.toFinset hs → g x = g y → x = y
this : ∏ᶠ (i : β) (_ : i ∈ s), (f ∘ g) i = ∏ i in Finite.toFinset hs, (f ∘ g) i
⊢ ∏ᶠ (i : α) (_ : i ∈ g '' s), f i = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)
[PROOFSTEP]
unfold Function.comp at this 
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg✝ : InjOn g (s ∩ mulSupport (f ∘ g))
hs : Set.Finite (s ∩ mulSupport (f ∘ g))
hg : ∀ (x : β), x ∈ Finite.toFinset hs → ∀ (y : β), y ∈ Finite.toFinset hs → g x = g y → x = y
this : ∏ᶠ (i : β) (_ : i ∈ s), f (g i) = ∏ i in Finite.toFinset hs, f (g i)
⊢ ∏ᶠ (i : α) (_ : i ∈ g '' s), f i = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)
[PROOFSTEP]
rw [this, ← Finset.prod_image hg]
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg✝ : InjOn g (s ∩ mulSupport (f ∘ g))
hs : Set.Finite (s ∩ mulSupport (f ∘ g))
hg : ∀ (x : β), x ∈ Finite.toFinset hs → ∀ (y : β), y ∈ Finite.toFinset hs → g x = g y → x = y
this : ∏ᶠ (i : β) (_ : i ∈ s), f (g i) = ∏ i in Finite.toFinset hs, f (g i)
⊢ ∏ᶠ (i : α) (_ : i ∈ g '' s), f i = ∏ x in Finset.image (fun x => g x) (Finite.toFinset hs), f x
[PROOFSTEP]
refine' finprod_mem_eq_prod_of_inter_mulSupport_eq f _
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg✝ : InjOn g (s ∩ mulSupport (f ∘ g))
hs : Set.Finite (s ∩ mulSupport (f ∘ g))
hg : ∀ (x : β), x ∈ Finite.toFinset hs → ∀ (y : β), y ∈ Finite.toFinset hs → g x = g y → x = y
this : ∏ᶠ (i : β) (_ : i ∈ s), f (g i) = ∏ i in Finite.toFinset hs, f (g i)
⊢ g '' s ∩ mulSupport f = ↑(Finset.image (fun x => g x) (Finite.toFinset hs)) ∩ mulSupport f
[PROOFSTEP]
rw [Finset.coe_image, hs.coe_toFinset, ← image_inter_mulSupport_eq, inter_assoc, inter_self]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
hs : ¬Set.Finite (s ∩ mulSupport (f ∘ g))
⊢ ∏ᶠ (i : α) (_ : i ∈ g '' s), f i = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)
[PROOFSTEP]
unfold Function.comp at hs 
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
hs : ¬Set.Finite (s ∩ mulSupport fun x => f (g x))
⊢ ∏ᶠ (i : α) (_ : i ∈ g '' s), f i = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)
[PROOFSTEP]
rw [finprod_mem_eq_one_of_infinite hs, finprod_mem_eq_one_of_infinite]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
hs : ¬Set.Finite (s ∩ mulSupport fun x => f (g x))
⊢ Set.Infinite (g '' s ∩ mulSupport fun i => f i)
[PROOFSTEP]
rwa [image_inter_mulSupport_eq, infinite_image_iff hg]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s t : Set α
g : β → α
hg : InjOn g (mulSupport (f ∘ g))
⊢ ∏ᶠ (i : α) (_ : i ∈ range g), f i = ∏ᶠ (j : β), f (g j)
[PROOFSTEP]
rw [← image_univ, finprod_mem_image', finprod_mem_univ]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s t : Set α
g : β → α
hg : InjOn g (mulSupport (f ∘ g))
⊢ InjOn g (univ ∩ mulSupport ((fun i => f i) ∘ g))
[PROOFSTEP]
rwa [univ_inter]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g✝ : α → M
a b : α
s✝ t✝ s : Set α
t : Set β
f : α → M
g : β → M
e : α → β
he₀ : BijOn e s t
he₁ : ∀ (x : α), x ∈ s → f x = g (e x)
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (j : β) (_ : j ∈ t), g j
[PROOFSTEP]
rw [← Set.BijOn.image_eq he₀, finprod_mem_image he₀.2.1]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g✝ : α → M
a b : α
s✝ t✝ s : Set α
t : Set β
f : α → M
g : β → M
e : α → β
he₀ : BijOn e s t
he₁ : ∀ (x : α), x ∈ s → f x = g (e x)
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (j : α) (_ : j ∈ s), g (e j)
[PROOFSTEP]
exact finprod_mem_congr rfl he₁
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g✝ : α → M
a b : α
s t : Set α
f : α → M
g : β → M
e : α → β
he₀ : Bijective e
he₁ : ∀ (x : α), f x = g (e x)
⊢ ∏ᶠ (i : α), f i = ∏ᶠ (j : β), g j
[PROOFSTEP]
rw [← finprod_mem_univ f, ← finprod_mem_univ g]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g✝ : α → M
a b : α
s t : Set α
f : α → M
g : β → M
e : α → β
he₀ : Bijective e
he₁ : ∀ (x : α), f x = g (e x)
⊢ ∏ᶠ (i : α) (_ : i ∈ univ), f i = ∏ᶠ (i : β) (_ : i ∈ univ), g i
[PROOFSTEP]
exact finprod_mem_eq_of_bijOn _ (bijective_iff_bijOn_univ.mp he₀) fun x _ => he₁ x
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s✝ t s : Set α
⊢ ∏ᶠ (j : ↑s), f ↑j = ∏ᶠ (i : α) (_ : i ∈ s), f i
[PROOFSTEP]
rw [← finprod_mem_range, Subtype.range_coe]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s✝ t s : Set α
⊢ Injective fun j => ↑j
[PROOFSTEP]
exact Subtype.coe_injective
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ t : Set α
h : Set.Finite (s ∩ mulSupport f)
⊢ (∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s \ t), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i
[PROOFSTEP]
rw [← finprod_mem_union', inter_union_diff]
[GOAL]
case hst
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ t : Set α
h : Set.Finite (s ∩ mulSupport f)
⊢ Disjoint (s ∩ t) (s \ t)
case hs
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ t : Set α
h : Set.Finite (s ∩ mulSupport f)
⊢ Set.Finite (s ∩ t ∩ mulSupport fun i => f i)
case ht
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ t : Set α
h : Set.Finite (s ∩ mulSupport f)
⊢ Set.Finite (s \ t ∩ mulSupport fun i => f i)
[PROOFSTEP]
rw [disjoint_iff_inf_le]
[GOAL]
case hst
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ t : Set α
h : Set.Finite (s ∩ mulSupport f)
⊢ s ∩ t ⊓ s \ t ≤ ⊥
case hs
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ t : Set α
h : Set.Finite (s ∩ mulSupport f)
⊢ Set.Finite (s ∩ t ∩ mulSupport fun i => f i)
case ht
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ t : Set α
h : Set.Finite (s ∩ mulSupport f)
⊢ Set.Finite (s \ t ∩ mulSupport fun i => f i)
[PROOFSTEP]
exacts [fun x hx => hx.2.2 hx.1.2, h.subset fun x hx => ⟨hx.1.1, hx.2⟩, h.subset fun x hx => ⟨hx.1.1, hx.2⟩]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hst : s ⊆ t
ht : Set.Finite (t ∩ mulSupport f)
⊢ (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t \ s), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i
[PROOFSTEP]
rw [← finprod_mem_inter_mul_diff' _ ht, inter_eq_self_of_subset_right hst]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
inst✝ : Finite ι
t : ι → Set α
h : Pairwise (Disjoint on t)
ht : ∀ (i : ι), Set.Finite (t i)
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ (i : ι), t i), f a = ∏ᶠ (i : ι) (a : α) (_ : a ∈ t i), f a
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
inst✝ : Finite ι
t : ι → Set α
h : Pairwise (Disjoint on t)
ht : ∀ (i : ι), Set.Finite (t i)
val✝ : Fintype ι
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ (i : ι), t i), f a = ∏ᶠ (i : ι) (a : α) (_ : a ∈ t i), f a
[PROOFSTEP]
lift t to ι → Finset α using ht
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i => ↑(t i))
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ (i : ι), (fun i => ↑(t i)) i), f a = ∏ᶠ (i : ι) (a : α) (_ : a ∈ (fun i => ↑(t i)) i), f a
[PROOFSTEP]
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)
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i => ↑(t i))
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ (i : ι), (fun i => ↑(t i)) i), f a = ∏ᶠ (i : ι) (a : α) (_ : a ∈ (fun i => ↑(t i)) i), f a
[PROOFSTEP]
rw [← biUnion_univ, ← Finset.coe_univ, ← Finset.coe_biUnion, finprod_mem_coe_finset, Finset.prod_biUnion]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i => ↑(t i))
⊢ ∏ x : ι, ∏ i in t x, f i = ∏ᶠ (i : ι) (a : α) (_ : a ∈ (fun i => ↑(t i)) i), f a
[PROOFSTEP]
simp only [finprod_mem_coe_finset, finprod_eq_prod_of_fintype]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i => ↑(t i))
⊢ PairwiseDisjoint ↑Finset.univ fun x => t x
[PROOFSTEP]
exact fun x _ y _ hxy => Finset.disjoint_coe.1 (h hxy)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
I : Set ι
t : ι → Set α
h : PairwiseDisjoint I t
hI : Set.Finite I
ht : ∀ (i : ι), i ∈ I → Set.Finite (t i)
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ (x : ι) (_ : x ∈ I), t x), f a = ∏ᶠ (i : ι) (_ : i ∈ I) (j : α) (_ : j ∈ t i), f j
[PROOFSTEP]
haveI := hI.fintype
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
I : Set ι
t : ι → Set α
h : PairwiseDisjoint I t
hI : Set.Finite I
ht : ∀ (i : ι), i ∈ I → Set.Finite (t i)
this : Fintype ↑I
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ (x : ι) (_ : x ∈ I), t x), f a = ∏ᶠ (i : ι) (_ : i ∈ I) (j : α) (_ : j ∈ t i), f j
[PROOFSTEP]
rw [biUnion_eq_iUnion, finprod_mem_iUnion, ← finprod_set_coe_eq_finprod_mem]
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
I : Set ι
t : ι → Set α
h : PairwiseDisjoint I t
hI : Set.Finite I
ht : ∀ (i : ι), i ∈ I → Set.Finite (t i)
this : Fintype ↑I
⊢ Pairwise (Disjoint on fun x => t ↑x)
case ht
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
I : Set ι
t : ι → Set α
h : PairwiseDisjoint I t
hI : Set.Finite I
ht : ∀ (i : ι), i ∈ I → Set.Finite (t i)
this : Fintype ↑I
⊢ ∀ (i : ↑I), Set.Finite (t ↑i)
[PROOFSTEP]
exacts [fun x y hxy => h x.2 y.2 (Subtype.coe_injective.ne hxy), fun b => ht b b.2]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
t : Set (Set α)
h : PairwiseDisjoint t id
ht₀ : Set.Finite t
ht₁ : ∀ (x : Set α), x ∈ t → Set.Finite x
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃₀ t), f a = ∏ᶠ (s : Set α) (_ : s ∈ t) (a : α) (_ : a ∈ s), f a
[PROOFSTEP]
rw [Set.sUnion_eq_biUnion]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
t : Set (Set α)
h : PairwiseDisjoint t id
ht₀ : Set.Finite t
ht₁ : ∀ (x : Set α), x ∈ t → Set.Finite x
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ (i : Set α) (_ : i ∈ t), i), f a = ∏ᶠ (s : Set α) (_ : s ∈ t) (a : α) (_ : a ∈ s), f a
[PROOFSTEP]
exact finprod_mem_biUnion h ht₀ ht₁
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ᶠ (i : α), f i
[PROOFSTEP]
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]
  exact ⟨fun h => And.intro hx h, fun h => h.2⟩
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
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ᶠ (i : α), f i
[PROOFSTEP]
rw [finprod_eq_prod _ hf]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i in Finite.toFinset hf, f i
[PROOFSTEP]
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]
  exact ⟨fun h => And.intro hx h, fun h => h.2⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
⊢ ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ x ∈ Finite.toFinset hf \ {a}
[PROOFSTEP]
rw [Finset.mem_sdiff, Finset.mem_singleton, Finite.mem_toFinset, mem_mulSupport]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ f x ≠ 1 ∧ ¬x = a
[PROOFSTEP]
exact ⟨fun h => And.intro hx h, fun h => h.2⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i in Finite.toFinset hf, f i
[PROOFSTEP]
rw [finprod_cond_eq_prod_of_cond_iff f (fun hx => h _ hx), Finset.sdiff_singleton_eq_erase]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
⊢ f a * ∏ i in Finset.erase (Finite.toFinset hf) a, f i = ∏ i in Finite.toFinset hf, f i
[PROOFSTEP]
by_cases ha : a ∈ mulSupport f
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : a ∈ mulSupport f
⊢ f a * ∏ i in Finset.erase (Finite.toFinset hf) a, f i = ∏ i in Finite.toFinset hf, f i
[PROOFSTEP]
apply Finset.mul_prod_erase _ _ ((Finite.mem_toFinset _).mpr ha)
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : ¬a ∈ mulSupport f
⊢ f a * ∏ i in Finset.erase (Finite.toFinset hf) a, f i = ∏ i in Finite.toFinset hf, f i
[PROOFSTEP]
rw [mem_mulSupport, not_not] at ha 
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : f a = 1
⊢ f a * ∏ i in Finset.erase (Finite.toFinset hf) a, f i = ∏ i in Finite.toFinset hf, f i
[PROOFSTEP]
rw [ha, one_mul]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : f a = 1
⊢ ∏ i in Finset.erase (Finite.toFinset hf) a, f i = ∏ i in Finite.toFinset hf, f i
[PROOFSTEP]
apply Finset.prod_erase _ ha
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t✝ s : Set α
t : Set β
f : α → β → M
hs : Set.Finite s
ht : Set.Finite t
⊢ ∏ᶠ (i : α) (_ : i ∈ s) (j : β) (_ : j ∈ t), f i j = ∏ᶠ (j : β) (_ : j ∈ t) (i : α) (_ : i ∈ s), f i j
[PROOFSTEP]
lift s to Finset α using hs
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t✝ : Set α
t : Set β
f : α → β → M
ht : Set.Finite t
s : Finset α
⊢ ∏ᶠ (i : α) (_ : i ∈ ↑s) (j : β) (_ : j ∈ t), f i j = ∏ᶠ (j : β) (_ : j ∈ t) (i : α) (_ : i ∈ ↑s), f i j
[PROOFSTEP]
lift t to Finset β using ht
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t✝ : Set α
f : α → β → M
s : Finset α
t : Finset β
⊢ ∏ᶠ (i : α) (_ : i ∈ ↑s) (j : β) (_ : j ∈ ↑t), f i j = ∏ᶠ (j : β) (_ : j ∈ ↑t) (i : α) (_ : i ∈ ↑s), f i j
[PROOFSTEP]
simp only [finprod_mem_coe_finset]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t✝ : Set α
f : α → β → M
s : Finset α
t : Finset β
⊢ ∏ i in s, ∏ i_1 in t, f i i_1 = ∏ i in t, ∏ i_1 in s, f i_1 i
[PROOFSTEP]
exact Finset.prod_comm
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M✝ : Type u_5
N : Type u_6
inst✝² : CommMonoid M✝
inst✝¹ : CommMonoid N
f✝ g : α → M✝
a b : α
s t : Set α
M : Type u_7
inst✝ : OrderedCommMonoid M
i : α
f : α → M
hf : Set.Finite (mulSupport f)
h : ∀ (j : α), 1 ≤ f j
⊢ f i ≤ ∏ᶠ (j : α), f j
[PROOFSTEP]
classical calc
  f i ≤ ∏ j in insert i hf.toFinset, f j := Finset.single_le_prod' (fun j _ => h j) (Finset.mem_insert_self _ _)
  _ = ∏ᶠ j, f j := (finprod_eq_prod_of_mulSupport_toFinset_subset _ hf (Finset.subset_insert _ _)).symm
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M✝ : Type u_5
N : Type u_6
inst✝² : CommMonoid M✝
inst✝¹ : CommMonoid N
f✝ g : α → M✝
a b : α
s t : Set α
M : Type u_7
inst✝ : OrderedCommMonoid M
i : α
f : α → M
hf : Set.Finite (mulSupport f)
h : ∀ (j : α), 1 ≤ f j
⊢ f i ≤ ∏ᶠ (j : α), f j
[PROOFSTEP]
calc
  f i ≤ ∏ j in insert i hf.toFinset, f j := Finset.single_le_prod' (fun j _ => h j) (Finset.mem_insert_self _ _)
  _ = ∏ᶠ j, f j := (finprod_eq_prod_of_mulSupport_toFinset_subset _ hf (Finset.subset_insert _ _)).symm
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
M₀ : Type u_7
inst✝ : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : Set.Finite (mulSupport f)
⊢ ∏ᶠ (x : α), f x = 0
[PROOFSTEP]
nontriviality
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
M₀ : Type u_7
inst✝ : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : Set.Finite (mulSupport f)
✝ : Nontrivial M₀
⊢ ∏ᶠ (x : α), f x = 0
[PROOFSTEP]
rw [finprod_eq_prod f hf]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
M₀ : Type u_7
inst✝ : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : Set.Finite (mulSupport f)
✝ : Nontrivial M₀
⊢ ∏ i in Finite.toFinset hf, f i = 0
[PROOFSTEP]
refine' Finset.prod_eq_zero (hf.mem_toFinset.2 _) hx
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
M₀ : Type u_7
inst✝ : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : Set.Finite (mulSupport f)
✝ : Nontrivial M₀
⊢ x ∈ mulSupport f
[PROOFSTEP]
simp [hx]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
⊢ ∏ᶠ (a : α), ∏ b in s, f a b = ∏ b in s, ∏ᶠ (a : α), f a b
[PROOFSTEP]
have hU :
  (mulSupport fun a => ∏ b in s, f a b) ⊆ (s.finite_toSet.biUnion fun b hb => h b (Finset.mem_coe.1 hb)).toFinset :=
  by
  rw [Finite.coe_toFinset]
  intro x hx
  simp only [exists_prop, mem_iUnion, Ne.def, mem_mulSupport, Finset.mem_coe]
  contrapose! hx
  rw [mem_mulSupport, not_not, Finset.prod_congr rfl hx, Finset.prod_const_one]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
⊢ (mulSupport fun a => ∏ b in s, f a b) ⊆
    ↑(Finite.toFinset (_ : Set.Finite (⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i)))
[PROOFSTEP]
rw [Finite.coe_toFinset]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
⊢ (mulSupport fun a => ∏ b in s, f a b) ⊆ ⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
x : α
hx : x ∈ mulSupport fun a => ∏ b in s, f a b
⊢ x ∈ ⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i
[PROOFSTEP]
simp only [exists_prop, mem_iUnion, Ne.def, mem_mulSupport, Finset.mem_coe]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
x : α
hx : x ∈ mulSupport fun a => ∏ b in s, f a b
⊢ ∃ i, i ∈ s ∧ ¬f x i = 1
[PROOFSTEP]
contrapose! hx
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
x : α
hx : ∀ (i : β), i ∈ s → f x i = 1
⊢ ¬x ∈ mulSupport fun a => ∏ b in s, f a b
[PROOFSTEP]
rw [mem_mulSupport, not_not, Finset.prod_congr rfl hx, Finset.prod_const_one]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
hU :
  (mulSupport fun a => ∏ b in s, f a b) ⊆
    ↑(Finite.toFinset (_ : Set.Finite (⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i)))
⊢ ∏ᶠ (a : α), ∏ b in s, f a b = ∏ b in s, ∏ᶠ (a : α), f a b
[PROOFSTEP]
rw [finprod_eq_prod_of_mulSupport_subset _ hU, Finset.prod_comm]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
hU :
  (mulSupport fun a => ∏ b in s, f a b) ⊆
    ↑(Finite.toFinset (_ : Set.Finite (⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i)))
⊢ ∏ y in s, ∏ x in Finite.toFinset (_ : Set.Finite (⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i)), f x y =
    ∏ b in s, ∏ᶠ (a : α), f a b
[PROOFSTEP]
refine' Finset.prod_congr rfl fun b hb => (finprod_eq_prod_of_mulSupport_subset _ _).symm
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b✝ : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
hU :
  (mulSupport fun a => ∏ b in s, f a b) ⊆
    ↑(Finite.toFinset (_ : Set.Finite (⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i)))
b : β
hb : b ∈ s
⊢ (mulSupport fun x => f x b) ⊆ ↑(Finite.toFinset (_ : Set.Finite (⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i)))
[PROOFSTEP]
intro a ha
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a✝ b✝ : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
hU :
  (mulSupport fun a => ∏ b in s, f a b) ⊆
    ↑(Finite.toFinset (_ : Set.Finite (⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i)))
b : β
hb : b ∈ s
a : α
ha : a ∈ mulSupport fun x => f x b
⊢ a ∈ ↑(Finite.toFinset (_ : Set.Finite (⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i)))
[PROOFSTEP]
simp only [Finite.coe_toFinset, mem_iUnion]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a✝ b✝ : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
hU :
  (mulSupport fun a => ∏ b in s, f a b) ⊆
    ↑(Finite.toFinset (_ : Set.Finite (⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i)))
b : β
hb : b ∈ s
a : α
ha : a ∈ mulSupport fun x => f x b
⊢ ∃ i i_1, a ∈ mulSupport fun a => f a i
[PROOFSTEP]
exact ⟨b, hb, ha⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a b : α
s✝ t : Set α
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
⊢ (mulSupport fun b => Finset.prod (filter (fun a => g a = b) s) f) ⊆ ↑(image g s)
[PROOFSTEP]
simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, Function.support_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a b : α
s✝ t : Set α
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
⊢ (mulSupport fun b => Finset.prod (filter (fun a => g a = b) s) f) ⊆ g '' ↑s
[PROOFSTEP]
intro b h
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a b✝ : α
s✝ t : Set α
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
b : β
h : b ∈ mulSupport fun b => Finset.prod (filter (fun a => g a = b) s) f
⊢ b ∈ g '' ↑s
[PROOFSTEP]
suffices (s.filter fun a : α => g a = b).Nonempty by
  simpa only [s.fiber_nonempty_iff_mem_image g b, Finset.mem_image, exists_prop]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a b✝ : α
s✝ t : Set α
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
b : β
h : b ∈ mulSupport fun b => Finset.prod (filter (fun a => g a = b) s) f
this : Finset.Nonempty (filter (fun a => g a = b) s)
⊢ b ∈ g '' ↑s
[PROOFSTEP]
simpa only [s.fiber_nonempty_iff_mem_image g b, Finset.mem_image, exists_prop]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a b✝ : α
s✝ t : Set α
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
b : β
h : b ∈ mulSupport fun b => Finset.prod (filter (fun a => g a = b) s) f
⊢ Finset.Nonempty (filter (fun a => g a = b) s)
[PROOFSTEP]
exact Finset.nonempty_of_prod_ne_one h
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
⊢ ∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab =
    ∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.fst = a) s)), f (a, b)
[PROOFSTEP]
have :
  ∀ a,
    (∏ i : β in (s.filter fun ab => Prod.fst ab = a).image Prod.snd, f (a, i)) =
      (Finset.filter (fun ab => Prod.fst ab = a) s).prod f :=
  by
  refine' fun a => Finset.prod_bij (fun b _ => (a, b)) _ _ _ _ <;> simp
  suffices ∀ a' b, (a', b) ∈ s → a' = a → (a, b) ∈ s ∧ a' = a by simpa
  rintro a' b hp rfl
  exact ⟨hp, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
⊢ ∀ (a : α),
    ∏ i in Finset.image Prod.snd (Finset.filter (fun ab => ab.fst = a) s), f (a, i) =
      Finset.prod (Finset.filter (fun ab => ab.fst = a) s) f
[PROOFSTEP]
refine' fun a => Finset.prod_bij (fun b _ => (a, b)) _ _ _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
f✝ g : α → M
a✝ b : α
s✝ t : Set α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
⊢ ∀ (a_1 : β) (ha : a_1 ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.fst = a) s)),
    (fun b x => (a, b)) a_1 ha ∈ Finset.filter (fun ab => ab.fst = a) s
[PROOFSTEP]
simp
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
f✝ g : α → M
a✝ b : α
s✝ t : Set α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
⊢ ∀ (a_1 : β) (ha : a_1 ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.fst = a) s)),
    f (a, a_1) = f ((fun b x => (a, b)) a_1 ha)
[PROOFSTEP]
simp
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
f✝ g : α → M
a✝ b : α
s✝ t : Set α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
⊢ ∀ (a₁ a₂ : β) (ha₁ : a₁ ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.fst = a) s))
    (ha₂ : a₂ ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.fst = a) s)),
    (fun b x => (a, b)) a₁ ha₁ = (fun b x => (a, b)) a₂ ha₂ → a₁ = a₂
[PROOFSTEP]
simp
[GOAL]
case refine'_4
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
f✝ g : α → M
a✝ b : α
s✝ t : Set α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
⊢ ∀ (b : α × β), b ∈ Finset.filter (fun ab => ab.fst = a) s → ∃ a_2 ha, b = (fun b x => (a, b)) a_2 ha
[PROOFSTEP]
simp
[GOAL]
case refine'_4
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
f✝ g : α → M
a✝ b : α
s✝ t : Set α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
⊢ ∀ (a_1 : α) (b : β), (a_1, b) ∈ s → a_1 = a → (a, b) ∈ s ∧ a_1 = a
[PROOFSTEP]
suffices ∀ a' b, (a', b) ∈ s → a' = a → (a, b) ∈ s ∧ a' = a by simpa
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
f✝ g : α → M
a✝ b : α
s✝ t : Set α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
this : ∀ (a' : α) (b : β), (a', b) ∈ s → a' = a → (a, b) ∈ s ∧ a' = a
⊢ ∀ (a_1 : α) (b : β), (a_1, b) ∈ s → a_1 = a → (a, b) ∈ s ∧ a_1 = a
[PROOFSTEP]
simpa
[GOAL]
case refine'_4
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
f✝ g : α → M
a✝ b : α
s✝ t : Set α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
⊢ ∀ (a' : α) (b : β), (a', b) ∈ s → a' = a → (a, b) ∈ s ∧ a' = a
[PROOFSTEP]
rintro a' b hp rfl
[GOAL]
case refine'_4
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
f✝ g : α → M
a b✝ : α
s✝ t : Set α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
a' : α
b : β
hp : (a', b) ∈ s
⊢ (a', b) ∈ s ∧ a' = a'
[PROOFSTEP]
exact ⟨hp, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this :
  ∀ (a : α),
    ∏ i in Finset.image Prod.snd (Finset.filter (fun ab => ab.fst = a) s), f (a, i) =
      Finset.prod (Finset.filter (fun ab => ab.fst = a) s) f
⊢ ∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab =
    ∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.fst = a) s)), f (a, b)
[PROOFSTEP]
rw [finprod_mem_finset_eq_prod]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this :
  ∀ (a : α),
    ∏ i in Finset.image Prod.snd (Finset.filter (fun ab => ab.fst = a) s), f (a, i) =
      Finset.prod (Finset.filter (fun ab => ab.fst = a) s) f
⊢ ∏ i in s, f i = ∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.fst = a) s)), f (a, b)
[PROOFSTEP]
simp_rw [finprod_mem_finset_eq_prod, this]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this :
  ∀ (a : α),
    ∏ i in Finset.image Prod.snd (Finset.filter (fun ab => ab.fst = a) s), f (a, i) =
      Finset.prod (Finset.filter (fun ab => ab.fst = a) s) f
⊢ ∏ i in s, f i = ∏ᶠ (a : α), Finset.prod (Finset.filter (fun ab => ab.fst = a) s) f
[PROOFSTEP]
rw [finprod_eq_prod_of_mulSupport_subset _ (s.mulSupport_of_fiberwise_prod_subset_image f Prod.fst), ←
  Finset.prod_fiberwise_of_maps_to (t := Finset.image Prod.fst s) _ f]
  -- `finish` could close the goal here
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this :
  ∀ (a : α),
    ∏ i in Finset.image Prod.snd (Finset.filter (fun ab => ab.fst = a) s), f (a, i) =
      Finset.prod (Finset.filter (fun ab => ab.fst = a) s) f
⊢ ∀ (x : α × β), x ∈ s → x.fst ∈ Finset.image Prod.fst s
[PROOFSTEP]
simp only [Finset.mem_image, Prod.mk.eta]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this :
  ∀ (a : α),
    ∏ i in Finset.image Prod.snd (Finset.filter (fun ab => ab.fst = a) s), f (a, i) =
      Finset.prod (Finset.filter (fun ab => ab.fst = a) s) f
⊢ ∀ (x : α × β), x ∈ s → ∃ a, a ∈ s ∧ a.fst = x.fst
[PROOFSTEP]
exact fun x hx => ⟨x, hx, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset (α × β)
f : α × β → M
⊢ ∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab = ∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b)
[PROOFSTEP]
classical
rw [finprod_mem_finset_product']
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset (α × β)
f : α × β → M
⊢ ∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab = ∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b)
[PROOFSTEP]
rw [finprod_mem_finset_product']
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset (α × β)
f : α × β → M
⊢ ∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.fst = a) s)), f (a, b) =
    ∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
γ : Type u_7
s : Finset (α × β × γ)
f : α × β × γ → M
⊢ ∏ᶠ (abc : α × β × γ) (_ : abc ∈ s), f abc = ∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c)
[PROOFSTEP]
classical
rw [finprod_mem_finset_product']
simp_rw [finprod_mem_finset_product']
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
γ : Type u_7
s : Finset (α × β × γ)
f : α × β × γ → M
⊢ ∏ᶠ (abc : α × β × γ) (_ : abc ∈ s), f abc = ∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c)
[PROOFSTEP]
rw [finprod_mem_finset_product']
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
γ : Type u_7
s : Finset (α × β × γ)
f : α × β × γ → M
⊢ ∏ᶠ (a : α) (b : β × γ) (_ : b ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.fst = a) s)), f (a, b) =
    ∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c)
[PROOFSTEP]
simp_rw [finprod_mem_finset_product']
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
γ : Type u_7
s : Finset (α × β × γ)
f : α × β × γ → M
⊢ ∏ᶠ (a : α) (a_1 : β) (b : γ) (_ :
      b ∈
        Finset.image Prod.snd
          (Finset.filter (fun ab => ab.fst = a_1) (Finset.image Prod.snd (Finset.filter (fun ab => ab.fst = a) s)))),
      f (a, a_1, b) =
    ∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
f : α × β → M
hf : Set.Finite (mulSupport f)
⊢ ∏ᶠ (ab : α × β), f ab = ∏ᶠ (a : α) (b : β), f (a, b)
[PROOFSTEP]
have h₁ : ∀ a, ∏ᶠ _ : a ∈ hf.toFinset, f a = f a := by simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
f : α × β → M
hf : Set.Finite (mulSupport f)
⊢ ∀ (a : α × β), ∏ᶠ (_ : a ∈ Finite.toFinset hf), f a = f a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
f : α × β → M
hf : Set.Finite (mulSupport f)
h₁ : ∀ (a : α × β), ∏ᶠ (_ : a ∈ Finite.toFinset hf), f a = f a
⊢ ∏ᶠ (ab : α × β), f ab = ∏ᶠ (a : α) (b : β), f (a, b)
[PROOFSTEP]
have h₂ : ∏ᶠ a, f a = ∏ᶠ (a) (_ : a ∈ hf.toFinset), f a := by simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
f : α × β → M
hf : Set.Finite (mulSupport f)
h₁ : ∀ (a : α × β), ∏ᶠ (_ : a ∈ Finite.toFinset hf), f a = f a
⊢ ∏ᶠ (a : α × β), f a = ∏ᶠ (a : α × β) (_ : a ∈ Finite.toFinset hf), f a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
f : α × β → M
hf : Set.Finite (mulSupport f)
h₁ : ∀ (a : α × β), ∏ᶠ (_ : a ∈ Finite.toFinset hf), f a = f a
h₂ : ∏ᶠ (a : α × β), f a = ∏ᶠ (a : α × β) (_ : a ∈ Finite.toFinset hf), f a
⊢ ∏ᶠ (ab : α × β), f ab = ∏ᶠ (a : α) (b : β), f (a, b)
[PROOFSTEP]
simp_rw [h₂, finprod_mem_finset_product, h₁]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
γ : Type u_7
f : α × β × γ → M
h : Set.Finite (mulSupport f)
⊢ ∏ᶠ (abc : α × β × γ), f abc = ∏ᶠ (a : α) (b : β) (c : γ), f (a, b, c)
[PROOFSTEP]
rw [finprod_curry f h]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
γ : Type u_7
f : α × β × γ → M
h : Set.Finite (mulSupport f)
⊢ ∏ᶠ (a : α) (b : β × γ), f (a, b) = ∏ᶠ (a : α) (b : β) (c : γ), f (a, b, c)
[PROOFSTEP]
congr
[GOAL]
case e_f
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
γ : Type u_7
f : α × β × γ → M
h : Set.Finite (mulSupport f)
⊢ (fun a => ∏ᶠ (b : β × γ), f (a, b)) = fun a => ∏ᶠ (b : β) (c : γ), f (a, b, c)
[PROOFSTEP]
ext a
[GOAL]
case e_f.h
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a✝ b : α
s t : Set α
γ : Type u_7
f : α × β × γ → M
h : Set.Finite (mulSupport f)
a : α
⊢ ∏ᶠ (b : β × γ), f (a, b) = ∏ᶠ (b : β) (c : γ), f (a, b, c)
[PROOFSTEP]
rw [finprod_curry]
[GOAL]
case e_f.h.hf
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a✝ b : α
s t : Set α
γ : Type u_7
f : α × β × γ → M
h : Set.Finite (mulSupport f)
a : α
⊢ Set.Finite (mulSupport fun b => f (a, b))
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a b : α
s t : Set α
f : α → β
hf : Injective f
inst✝ : DecidablePred fun x => x ∈ range f
g : α → M
⊢ (∏ᶠ (b : β), if h : b ∈ range f then g (Classical.choose h) else 1) = ∏ᶠ (a : α), g a
[PROOFSTEP]
simp_rw [← finprod_eq_dif]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a b : α
s t : Set α
f : α → β
hf : Injective f
inst✝ : DecidablePred fun x => x ∈ range f
g : α → M
⊢ ∏ᶠ (b : β) (h : b ∈ range f), g (Classical.choose h) = ∏ᶠ (a : α), g a
[PROOFSTEP]
rw [finprod_dmem, finprod_mem_range hf, finprod_congr fun a => _]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a b : α
s t : Set α
f : α → β
hf : Injective f
inst✝ : DecidablePred fun x => x ∈ range f
g : α → M
⊢ ∀ (a : α), (if h' : f a ∈ range f then g (Classical.choose h') else 1) = g a
[PROOFSTEP]
intro a
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
G : Type u_4
M : Type u_5
N : Type u_6
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a✝ b : α
s t : Set α
f : α → β
hf : Injective f
inst✝ : DecidablePred fun x => x ∈ range f
g : α → M
a : α
⊢ (if h' : f a ∈ range f then g (Classical.choose h') else 1) = g a
[PROOFSTEP]
rw [dif_pos (Set.mem_range_self a), hf (Classical.choose_spec (Set.mem_range_self a))]
