no goals
𝓕 : Type ?u.1112225
𝕜 : Type ?u.1112228
α : Type ?u.1112231
ι : Type ?u.1112234
κ : Type ?u.1112237
E : Type ?u.1112240
F : Type ?u.1112243
G : Type ?u.1112246
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
n : ℤ
⊢ ↑↑(natAbs n) = ↑↑(natAbs n)
simp only [Int.cast_ofNat, NNReal.coe_nat_cast]
no goals
𝓕 : Type ?u.1112225
𝕜 : Type ?u.1112228
α : Type ?u.1112231
ι : Type ?u.1112234
κ : Type ?u.1112237
E : Type ?u.1112240
F : Type ?u.1112243
G : Type ?u.1112246
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
n : ℤ
⊢ ↑↑(natAbs n) = ↑(abs n)
simp only [Int.coe_natAbs, Int.cast_abs]