case inl
𝓕 : Type ?u.1109820
𝕜 : Type ?u.1109823
α : Type ?u.1109826
ι : Type ?u.1109829
κ : Type ?u.1109832
E : Type ?u.1109835
F : Type ?u.1109838
G : Type ?u.1109841
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r✝ r₁ r₂ r : ℝ
hr : 0 ≤ r
⊢ ENNReal.ofReal r ≤ ↑‖r‖₊

case inr
𝓕 : Type ?u.1109820
𝕜 : Type ?u.1109823
α : Type ?u.1109826
ι : Type ?u.1109829
κ : Type ?u.1109832
E : Type ?u.1109835
F : Type ?u.1109838
G : Type ?u.1109841
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r✝ r₁ r₂ r : ℝ
hr : r ≤ 0
⊢ ENNReal.ofReal r ≤ ↑‖r‖₊
𝓕 : Type ?u.1109820
𝕜 : Type ?u.1109823
α : Type ?u.1109826
ι : Type ?u.1109829
κ : Type ?u.1109832
E : Type ?u.1109835
F : Type ?u.1109838
G : Type ?u.1109841
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r✝ r₁ r₂ r : ℝ
⊢ ENNReal.ofReal r ≤ ↑‖r‖₊
obtain hr | hr := le_total 0 r
no goals
case inl
𝓕 : Type ?u.1109820
𝕜 : Type ?u.1109823
α : Type ?u.1109826
ι : Type ?u.1109829
κ : Type ?u.1109832
E : Type ?u.1109835
F : Type ?u.1109838
G : Type ?u.1109841
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r✝ r₁ r₂ r : ℝ
hr : 0 ≤ r
⊢ ENNReal.ofReal r ≤ ↑‖r‖₊
exact (Real.ennnorm_eq_ofReal hr).ge
case inr
𝓕 : Type ?u.1109820
𝕜 : Type ?u.1109823
α : Type ?u.1109826
ι : Type ?u.1109829
κ : Type ?u.1109832
E : Type ?u.1109835
F : Type ?u.1109838
G : Type ?u.1109841
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r✝ r₁ r₂ r : ℝ
hr : r ≤ 0
⊢ 0 ≤ ↑‖r‖₊
case inr
𝓕 : Type ?u.1109820
𝕜 : Type ?u.1109823
α : Type ?u.1109826
ι : Type ?u.1109829
κ : Type ?u.1109832
E : Type ?u.1109835
F : Type ?u.1109838
G : Type ?u.1109841
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r✝ r₁ r₂ r : ℝ
hr : r ≤ 0
⊢ ENNReal.ofReal r ≤ ↑‖r‖₊
rw [ENNReal.ofReal_eq_zero.2 hr]
no goals
case inr
𝓕 : Type ?u.1109820
𝕜 : Type ?u.1109823
α : Type ?u.1109826
ι : Type ?u.1109829
κ : Type ?u.1109832
E : Type ?u.1109835
F : Type ?u.1109838
G : Type ?u.1109841
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r✝ r₁ r₂ r : ℝ
hr : r ≤ 0
⊢ 0 ≤ ↑‖r‖₊
exact bot_le