𝓕 : Type ?u.915521
𝕜 : Type ?u.915524
α : Type ?u.915527
ι : Type ?u.915530
κ : Type ?u.915533
E : Type u_1
F : Type ?u.915539
G : Type ?u.915542
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
n : ℕ
hn : 0 < n
h : ‖a / b‖ < r
⊢ ‖(a / b) ^ n‖ < n • r
𝓕 : Type ?u.915521
𝕜 : Type ?u.915524
α : Type ?u.915527
ι : Type ?u.915530
κ : Type ?u.915533
E : Type u_1
F : Type ?u.915539
G : Type ?u.915542
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
n : ℕ
hn : 0 < n
h : a ∈ ball b r
⊢ a ^ n ∈ ball (b ^ n) (n • r)
simp only [mem_ball, dist_eq_norm_div, ← div_pow] at h⊢
𝓕 : Type ?u.915521
𝕜 : Type ?u.915524
α : Type ?u.915527
ι : Type ?u.915530
κ : Type ?u.915533
E : Type u_1
F : Type ?u.915539
G : Type ?u.915542
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
n : ℕ
hn : 0 < n
h : ‖a / b‖ < r
⊢ ↑n * ‖a / b‖ < n • r
𝓕 : Type ?u.915521
𝕜 : Type ?u.915524
α : Type ?u.915527
ι : Type ?u.915530
κ : Type ?u.915533
E : Type u_1
F : Type ?u.915539
G : Type ?u.915542
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
n : ℕ
hn : 0 < n
h : ‖a / b‖ < r
⊢ ‖(a / b) ^ n‖ < n • r
refine' lt_of_le_of_lt (norm_pow_le_mul_norm n (a / b)) _
case hn
𝓕 : Type ?u.915521
𝕜 : Type ?u.915524
α : Type ?u.915527
ι : Type ?u.915530
κ : Type ?u.915533
E : Type u_1
F : Type ?u.915539
G : Type ?u.915542
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
n : ℕ
hn : 0 < n
h : ‖a / b‖ < r
⊢ 0 < ↑n

𝓕 : Type ?u.915521
𝕜 : Type ?u.915524
α : Type ?u.915527
ι : Type ?u.915530
κ : Type ?u.915533
E : Type u_1
F : Type ?u.915539
G : Type ?u.915542
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
n : ℕ
h : ‖a / b‖ < r
hn : 0 < ↑n
⊢ ↑n * ‖a / b‖ < n • r
𝓕 : Type ?u.915521
𝕜 : Type ?u.915524
α : Type ?u.915527
ι : Type ?u.915530
κ : Type ?u.915533
E : Type u_1
F : Type ?u.915539
G : Type ?u.915542
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
n : ℕ
hn : 0 < n
h : ‖a / b‖ < r
⊢ ↑n * ‖a / b‖ < n • r
replace hn : 0 < (n : ℝ)
𝓕 : Type ?u.915521
𝕜 : Type ?u.915524
α : Type ?u.915527
ι : Type ?u.915530
κ : Type ?u.915533
E : Type u_1
F : Type ?u.915539
G : Type ?u.915542
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
n : ℕ
h : ‖a / b‖ < r
hn : 0 < ↑n
⊢ ↑n * ‖a / b‖ < ↑n * r
𝓕 : Type ?u.915521
𝕜 : Type ?u.915524
α : Type ?u.915527
ι : Type ?u.915530
κ : Type ?u.915533
E : Type u_1
F : Type ?u.915539
G : Type ?u.915542
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
n : ℕ
h : ‖a / b‖ < r
hn : 0 < ↑n
⊢ ↑n * ‖a / b‖ < n • r
rw [nsmul_eq_mul]
no goals
𝓕 : Type ?u.915521
𝕜 : Type ?u.915524
α : Type ?u.915527
ι : Type ?u.915530
κ : Type ?u.915533
E : Type u_1
F : Type ?u.915539
G : Type ?u.915542
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
n : ℕ
h : ‖a / b‖ < r
hn : 0 < ↑n
⊢ ↑n * ‖a / b‖ < ↑n * r
nlinarith
no goals
case hn
𝓕 : Type ?u.915521
𝕜 : Type ?u.915524
α : Type ?u.915527
ι : Type ?u.915530
κ : Type ?u.915533
E : Type u_1
F : Type ?u.915539
G : Type ?u.915542
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
n : ℕ
hn : 0 < n
h : ‖a / b‖ < r
⊢ 0 < ↑n
norm_cast