case mk.mk
α✝ : Type ?u.116719
β : Type ?u.116722
γ : Type ?u.116725
ι : Type u_2
inst✝¹ : SeminormedRing α✝
α : Type u_1
inst✝ : NormedCommRing α
f : ι → α
val✝ : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk Setoid.r l)
hs : Finset.Nonempty { val := Quot.mk Setoid.r l, nodup := hl }
⊢ ‖∏ 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.116719
β : Type ?u.116722
γ : Type ?u.116725
ι : Type u_2
inst✝¹ : SeminormedRing α✝
α : Type u_1
inst✝ : NormedCommRing α
s : Finset ι
hs : Finset.Nonempty s
f : ι → α
⊢ ‖∏ i in s, f i‖ ≤ ∏ i in s, ‖f i‖
rcases s with ⟨⟨l⟩, hl⟩
case mk.mk
α✝ : Type ?u.116719
β : Type ?u.116722
γ : Type ?u.116725
ι : Type u_2
inst✝¹ : SeminormedRing α✝
α : Type u_1
inst✝ : NormedCommRing α
f : ι → α
val✝ : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk Setoid.r l)
hs : Finset.Nonempty { val := Quot.mk Setoid.r l, nodup := hl }
this : List.map f 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‖
case mk.mk
α✝ : Type ?u.116719
β : Type ?u.116722
γ : Type ?u.116725
ι : Type u_2
inst✝¹ : SeminormedRing α✝
α : Type u_1
inst✝ : NormedCommRing α
f : ι → α
val✝ : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk Setoid.r l)
hs : Finset.Nonempty { val := Quot.mk Setoid.r l, nodup := hl }
⊢ ‖∏ i in { val := Quot.mk Setoid.r l, nodup := hl }, f i‖ ≤ ∏ i in { val := Quot.mk Setoid.r l, nodup := hl }, ‖f i‖
have : l.map f ≠ [] := by simpa using hs
no goals
case mk.mk
α✝ : Type ?u.116719
β : Type ?u.116722
γ : Type ?u.116725
ι : Type u_2
inst✝¹ : SeminormedRing α✝
α : Type u_1
inst✝ : NormedCommRing α
f : ι → α
val✝ : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk Setoid.r l)
hs : Finset.Nonempty { val := Quot.mk Setoid.r l, nodup := hl }
this : List.map f 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 List.norm_prod_le' this
no goals
α✝ : Type ?u.116719
β : Type ?u.116722
γ : Type ?u.116725
ι : Type u_2
inst✝¹ : SeminormedRing α✝
α : Type u_1
inst✝ : NormedCommRing α
f : ι → α
val✝ : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk Setoid.r l)
hs : Finset.Nonempty { val := Quot.mk Setoid.r l, nodup := hl }
⊢ List.map f l ≠ []
simpa using hs