case pos
G : Type ?u.84392
M : Type u_1
N : Type u_2
α : Sort u_3
β : Sort ?u.84404
ι : Sort ?u.84407
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)

case neg
G : Type ?u.84392
M : Type u_1
N : Type u_2
α : Sort u_3
β : Sort ?u.84404
ι : Sort ?u.84407
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)
G : Type ?u.84392
M : Type u_1
N : Type u_2
α : Sort u_3
β : Sort ?u.84404
ι : Sort ?u.84407
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)
by_cases hg : (mulSupport <| g ∘ PLift.down).Finite
case neg.hnc
G : Type ?u.84392
M : Type u_1
N : Type u_2
α : Sort u_3
β : Sort ?u.84404
ι : Sort ?u.84407
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.84392
M : Type u_1
N : Type u_2
α : Sort u_3
β : Sort ?u.84404
ι : Sort ?u.84407
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))
case neg
G : Type ?u.84392
M : Type u_1
N : Type u_2
α : Sort u_3
β : Sort ?u.84404
ι : Sort ?u.84407
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)
rw [finprod, dif_neg, f.map_one, finprod, dif_neg]
no goals
case neg.hnc
G : Type ?u.84392
M : Type u_1
N : Type u_2
α : Sort u_3
β : Sort ?u.84404
ι : Sort ?u.84407
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.84392
M : Type u_1
N : Type u_2
α : Sort u_3
β : Sort ?u.84404
ι : Sort ?u.84407
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))
exacts [Infinite.mono (fun x hx => mt (hf (g x.down)) hx) hg, hg]
no goals
case pos
G : Type ?u.84392
M : Type u_1
N : Type u_2
α : Sort u_3
β : Sort ?u.84404
ι : Sort ?u.84407
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)
exact f.map_finprod_pLift g hg