no goals
𝓕 : Type ?u.1111633
𝕜 : Type ?u.1111636
α : Type ?u.1111639
ι : Type ?u.1111642
κ : Type ?u.1111645
E : Type ?u.1111648
F : Type ?u.1111651
G : Type ?u.1111654
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
n : ℕ
⊢ ‖↑n‖ = ↑n
simp [Int.norm_eq_abs]