case mk.mk
α✝ : Type ?u.121829
β : Type ?u.121832
γ : Type ?u.121835
ι : Type u_2
inst✝² : SeminormedRing α✝
α : Type u_1
inst✝¹ : NormedCommRing α
inst✝ : NormOneClass α
f : ι → α
val✝ : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk Setoid.r l)
⊢ ‖∏ i in { val := Quot.mk Setoid.r l, nodup := hl }, f i‖ ≤ ∏ i in { val := Quot.mk Setoid.r l, nodup := hl }, ‖f i‖
α✝ : Type ?u.121829
β : Type ?u.121832
γ : Type ?u.121835
ι : Type u_2
inst✝² : SeminormedRing α✝
α : Type u_1
inst✝¹ : NormedCommRing α
inst✝ : NormOneClass α
s : Finset ι
f : ι → α
⊢ ‖∏ i in s, f i‖ ≤ ∏ i in s, ‖f i‖
rcases s with ⟨⟨l⟩, hl⟩
no goals
case mk.mk
α✝ : Type ?u.121829
β : Type ?u.121832
γ : Type ?u.121835
ι : Type u_2
inst✝² : SeminormedRing α✝
α : Type u_1
inst✝¹ : NormedCommRing α
inst✝ : NormOneClass α
f : ι → α
val✝ : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk Setoid.r l)
⊢ ‖∏ i in { val := Quot.mk Setoid.r l, nodup := hl }, f i‖ ≤ ∏ i in { val := Quot.mk Setoid.r l, nodup := hl }, ‖f i‖
simpa using (l.map f).norm_prod_le