𝓕 : Type ?u.1109488
𝕜 : Type ?u.1109491
α : Type ?u.1109494
ι : Type ?u.1109497
κ : Type ?u.1109500
E : Type ?u.1109503
F : Type ?u.1109506
G : Type ?u.1109509
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
hr : 0 ≤ r
⊢ { val := r, property := hr } = ‖r‖₊
𝓕 : Type ?u.1109488
𝕜 : Type ?u.1109491
α : Type ?u.1109494
ι : Type ?u.1109497
κ : Type ?u.1109500
E : Type ?u.1109503
F : Type ?u.1109506
G : Type ?u.1109509
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
hr : 0 ≤ r
⊢ toNNReal r = ‖r‖₊
rw [Real.toNNReal_of_nonneg hr]
case a
𝓕 : Type ?u.1109488
𝕜 : Type ?u.1109491
α : Type ?u.1109494
ι : Type ?u.1109497
κ : Type ?u.1109500
E : Type ?u.1109503
F : Type ?u.1109506
G : Type ?u.1109509
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
hr : 0 ≤ r
⊢ ↑{ val := r, property := hr } = ↑‖r‖₊
𝓕 : Type ?u.1109488
𝕜 : Type ?u.1109491
α : Type ?u.1109494
ι : Type ?u.1109497
κ : Type ?u.1109500
E : Type ?u.1109503
F : Type ?u.1109506
G : Type ?u.1109509
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
hr : 0 ≤ r
⊢ { val := r, property := hr } = ‖r‖₊
ext
no goals
case a
𝓕 : Type ?u.1109488
𝕜 : Type ?u.1109491
α : Type ?u.1109494
ι : Type ?u.1109497
κ : Type ?u.1109500
E : Type ?u.1109503
F : Type ?u.1109506
G : Type ?u.1109509
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
hr : 0 ≤ r
⊢ ↑{ val := r, property := hr } = ↑‖r‖₊
rw [coe_mk, coe_nnnorm r, Real.norm_eq_abs r, abs_of_nonneg hr]