case inl
α : Type u_1
β : Type ?u.183015
ι : Type ?u.183018
G : Type ?u.183021
M : Type u_2
N : Type ?u.183027
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

case inr
α : Type u_1
β : Type ?u.183015
ι : Type ?u.183018
G : Type ?u.183021
M : Type u_2
N : Type ?u.183027
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f : α → M
inst✝ : Decidable (Set.Finite (mulSupport f))
h : ¬Set.Finite (mulSupport f)
⊢ (∏ᶠ (i : α), f i) = 1
α : Type u_1
β : Type ?u.183015
ι : Type ?u.183018
G : Type ?u.183021
M : Type u_2
N : Type ?u.183027
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
split_ifs with h
no goals
case inl
α : Type u_1
β : Type ?u.183015
ι : Type ?u.183018
G : Type ?u.183021
M : Type u_2
N : Type ?u.183027
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
exact finprod_eq_prod_of_mulSupport_toFinset_subset _ h (Finset.Subset.refl _)
case inr.hnc
α : Type u_1
β : Type ?u.183015
ι : Type ?u.183018
G : Type ?u.183021
M : Type u_2
N : Type ?u.183027
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))
case inr
α : Type u_1
β : Type ?u.183015
ι : Type ?u.183018
G : Type ?u.183021
M : Type u_2
N : Type ?u.183027
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f : α → M
inst✝ : Decidable (Set.Finite (mulSupport f))
h : ¬Set.Finite (mulSupport f)
⊢ (∏ᶠ (i : α), f i) = 1
rw [finprod, dif_neg]
case inr.hnc
α : Type u_1
β : Type ?u.183015
ι : Type ?u.183018
G : Type ?u.183021
M : Type u_2
N : Type ?u.183027
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)
case inr.hnc
α : Type u_1
β : Type ?u.183015
ι : Type ?u.183018
G : Type ?u.183021
M : Type u_2
N : Type ?u.183027
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))
rw [mulSupport_comp_eq_preimage]
no goals
case inr.hnc
α : Type u_1
β : Type ?u.183015
ι : Type ?u.183018
G : Type ?u.183021
M : Type u_2
N : Type ?u.183027
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)
exact mt (fun hf => hf.of_preimage Equiv.plift.surjective) h