𝓕 : Type ?u.694205
𝕜 : Type ?u.694208
α : Type ?u.694211
ι : Type ?u.694214
κ : Type ?u.694217
E : Type u_1
F : Type ?u.694223
G : Type ?u.694226
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
m : Multiset E
⊢ ↑Multiplicative.ofAdd ‖Multiset.prod m‖ ≤ Multiset.prod (Multiset.map (↑Multiplicative.ofAdd ∘ fun x => ‖x‖) m)
𝓕 : Type ?u.694205
𝕜 : Type ?u.694208
α : Type ?u.694211
ι : Type ?u.694214
κ : Type ?u.694217
E : Type u_1
F : Type ?u.694223
G : Type ?u.694226
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
m : Multiset E
⊢ ‖Multiset.prod m‖ ≤ Multiset.sum (Multiset.map (fun x => ‖x‖) m)
rw [← Multiplicative.ofAdd_le, ofAdd_multiset_prod, Multiset.map_map]
case refine'_1
𝓕 : Type ?u.694205
𝕜 : Type ?u.694208
α : Type ?u.694211
ι : Type ?u.694214
κ : Type ?u.694217
E : Type u_1
F : Type ?u.694223
G : Type ?u.694226
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
m : Multiset E
⊢ (↑Multiplicative.ofAdd ∘ norm) 1 = 1

case refine'_2
𝓕 : Type ?u.694205
𝕜 : Type ?u.694208
α : Type ?u.694211
ι : Type ?u.694214
κ : Type ?u.694217
E : Type u_1
F : Type ?u.694223
G : Type ?u.694226
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
m : Multiset E
x y : E
⊢ (↑Multiplicative.ofAdd ∘ norm) (x * y) ≤ (↑Multiplicative.ofAdd ∘ norm) x * (↑Multiplicative.ofAdd ∘ norm) y
𝓕 : Type ?u.694205
𝕜 : Type ?u.694208
α : Type ?u.694211
ι : Type ?u.694214
κ : Type ?u.694217
E : Type u_1
F : Type ?u.694223
G : Type ?u.694226
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
m : Multiset E
⊢ ↑Multiplicative.ofAdd ‖Multiset.prod m‖ ≤ Multiset.prod (Multiset.map (↑Multiplicative.ofAdd ∘ fun x => ‖x‖) m)
refine' Multiset.le_prod_of_submultiplicative (Multiplicative.ofAdd ∘ norm) _ (fun x y => _) _
no goals
case refine'_1
𝓕 : Type ?u.694205
𝕜 : Type ?u.694208
α : Type ?u.694211
ι : Type ?u.694214
κ : Type ?u.694217
E : Type u_1
F : Type ?u.694223
G : Type ?u.694226
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
m : Multiset E
⊢ (↑Multiplicative.ofAdd ∘ norm) 1 = 1
simp only [comp_apply, norm_one', ofAdd_zero]
no goals
case refine'_2
𝓕 : Type ?u.694205
𝕜 : Type ?u.694208
α : Type ?u.694211
ι : Type ?u.694214
κ : Type ?u.694217
E : Type u_1
F : Type ?u.694223
G : Type ?u.694226
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
m : Multiset E
x y : E
⊢ (↑Multiplicative.ofAdd ∘ norm) (x * y) ≤ (↑Multiplicative.ofAdd ∘ norm) x * (↑Multiplicative.ofAdd ∘ norm) y
exact norm_mul_le' x y