𝓕 : Type ?u.737054
𝕜 : Type ?u.737057
α : Type ?u.737060
ι : Type u_1
κ : Type ?u.737066
E : Type u_2
F : Type ?u.737072
G : Type ?u.737075
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
s : Finset ι
f : ι → E
⊢ ↑Multiplicative.ofAdd ‖∏ i in s, f i‖ ≤ ∏ i in s, ↑Multiplicative.ofAdd ‖f i‖
𝓕 : Type ?u.737054
𝕜 : Type ?u.737057
α : Type ?u.737060
ι : Type u_1
κ : Type ?u.737066
E : Type u_2
F : Type ?u.737072
G : Type ?u.737075
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
s : Finset ι
f : ι → E
⊢ ‖∏ i in s, f i‖ ≤ ∑ i in s, ‖f i‖
rw [← Multiplicative.ofAdd_le, ofAdd_sum]
case refine'_1
𝓕 : Type ?u.737054
𝕜 : Type ?u.737057
α : Type ?u.737060
ι : Type u_1
κ : Type ?u.737066
E : Type u_2
F : Type ?u.737072
G : Type ?u.737075
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
s : Finset ι
f : ι → E
⊢ (↑Multiplicative.ofAdd ∘ norm) 1 = 1

case refine'_2
𝓕 : Type ?u.737054
𝕜 : Type ?u.737057
α : Type ?u.737060
ι : Type u_1
κ : Type ?u.737066
E : Type u_2
F : Type ?u.737072
G : Type ?u.737075
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
s : Finset ι
f : ι → E
x y : E
⊢ (↑Multiplicative.ofAdd ∘ norm) (x * y) ≤ (↑Multiplicative.ofAdd ∘ norm) x * (↑Multiplicative.ofAdd ∘ norm) y
𝓕 : Type ?u.737054
𝕜 : Type ?u.737057
α : Type ?u.737060
ι : Type u_1
κ : Type ?u.737066
E : Type u_2
F : Type ?u.737072
G : Type ?u.737075
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
s : Finset ι
f : ι → E
⊢ ↑Multiplicative.ofAdd ‖∏ i in s, f i‖ ≤ ∏ i in s, ↑Multiplicative.ofAdd ‖f i‖
refine' Finset.le_prod_of_submultiplicative (Multiplicative.ofAdd ∘ norm) _ (fun x y => _) _ _
no goals
case refine'_1
𝓕 : Type ?u.737054
𝕜 : Type ?u.737057
α : Type ?u.737060
ι : Type u_1
κ : Type ?u.737066
E : Type u_2
F : Type ?u.737072
G : Type ?u.737075
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
s : Finset ι
f : ι → E
⊢ (↑Multiplicative.ofAdd ∘ norm) 1 = 1
simp only [comp_apply, norm_one', ofAdd_zero]
no goals
case refine'_2
𝓕 : Type ?u.737054
𝕜 : Type ?u.737057
α : Type ?u.737060
ι : Type u_1
κ : Type ?u.737066
E : Type u_2
F : Type ?u.737072
G : Type ?u.737075
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
s : Finset ι
f : ι → E
x y : E
⊢ (↑Multiplicative.ofAdd ∘ norm) (x * y) ≤ (↑Multiplicative.ofAdd ∘ norm) x * (↑Multiplicative.ofAdd ∘ norm) y
exact norm_mul_le' x y