𝓕 : Type ?u.1114918
𝕜 : Type ?u.1114921
α : Type ?u.1114924
ι : Type ?u.1114927
κ : Type ?u.1114930
E : Type ?u.1114933
F : Type ?u.1114936
G : Type ?u.1114939
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
m : ℤ
⊢ ‖↑↑m‖ = ‖↑m‖
𝓕 : Type ?u.1114918
𝕜 : Type ?u.1114921
α : Type ?u.1114924
ι : Type ?u.1114927
κ : Type ?u.1114930
E : Type ?u.1114933
F : Type ?u.1114936
G : Type ?u.1114939
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
m : ℤ
⊢ ‖↑m‖ = ‖m‖
rw [← Rat.norm_cast_real, ← Int.norm_cast_real]
no goals
𝓕 : Type ?u.1114918
𝕜 : Type ?u.1114921
α : Type ?u.1114924
ι : Type ?u.1114927
κ : Type ?u.1114930
E : Type ?u.1114933
F : Type ?u.1114936
G : Type ?u.1114939
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
m : ℤ
⊢ ‖↑↑m‖ = ‖↑m‖
congr 1