-- Mathlib/Analysis/Normed/Field/Ultra.lean
/-- To prove that a normed division ring is nonarchimedean, it suffices to prove that the norm
of the image of any natural is less than or equal to one. -/
lemma isUltrametricDist_of_forall_norm_natCast_le_one
    (h : ∀ n : ℕ, ‖(n : R)‖ ≤ 1) : IsUltrametricDist R

Proof state:
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
⊢ ‖x + 1‖ ^ m ≤ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k

Tactic:
simpa only [← norm_pow, (Commute.one_right x).add_pow, one_pow, mul_one, nsmul_eq_mul,
  Nat.cast_comm] using (norm_sum_le _ _).trans (Finset.sum_le_sum fun _ _ ↦ h _ _)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (n : ℕ), ‖↑n‖ ≤ 1
x✝ : R
m : ℕ
x : R
n : ℕ
⊢ ‖↑n‖ * ‖x‖ ≤ ‖x‖

Tactic:
rcases (norm_nonneg x).eq_or_lt with hx | hx

Result:
case inl
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (n : ℕ), ‖↑n‖ ≤ 1
x✝ : R
m : ℕ
x : R
n : ℕ
hx : 0 = ‖x‖
⊢ ‖↑n‖ * ‖x‖ ≤ ‖x‖

case inr
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (n : ℕ), ‖↑n‖ ≤ 1
x✝ : R
m : ℕ
x : R
n : ℕ
hx : 0 < ‖x‖
⊢ ‖↑n‖ * ‖x‖ ≤ ‖x‖

Proof state:
case inr.intro
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : 1 ⊔ ‖x‖ ^ m = ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
hx : ‖x‖ < 1
⊢ ‖x‖ ^ m ≤ 1

Tactic:
exact pow_le_one₀ (norm_nonneg _) hx.le

Result:
no goals

Proof state:
case inl.intro.inr
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm✝ : 1 ⊔ ‖x‖ ^ m = 1
hx : ‖x‖ ^ m ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
hm : m ≠ 0
⊢ ‖x‖ ^ i ≤ 1

Tactic:
rw [pow_le_one_iff_of_nonneg (norm_nonneg _) hm] at hx

Result:
case inl.intro.inr
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm✝ : 1 ⊔ ‖x‖ ^ m = 1
hx : ‖x‖ ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
hm : m ≠ 0
⊢ ‖x‖ ^ i ≤ 1

Proof state:
case inr.intro
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : 1 ⊔ ‖x‖ ^ m = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ 1 ≤ ‖x‖

Tactic:
contrapose! hx

Result:
case inr.intro
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : 1 ⊔ ‖x‖ ^ m = ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
hx : ‖x‖ < 1
⊢ ‖x‖ ^ m ≤ 1

Proof state:
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
⊢ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k ≤ (m + 1) • (1 ⊔ ‖x‖ ^ m)

Tactic:
rw [← Finset.card_range (m + 1), ← Finset.sum_const, Finset.card_range]

Result:
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
⊢ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k ≤ ∑ _x ∈ Finset.range (m + 1), 1 ⊔ ‖x‖ ^ m

Proof state:
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
⊢ ‖x + 1‖ ^ m ≤ (m + 1) • (1 ⊔ ‖x‖ ^ m)

Tactic:
transitivity ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k

Result:
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
⊢ ‖x + 1‖ ^ m ≤ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k

R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
⊢ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k ≤ (m + 1) • (1 ⊔ ‖x‖ ^ m)

Proof state:
case inl
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (n : ℕ), ‖↑n‖ ≤ 1
x✝ : R
m : ℕ
x : R
n : ℕ
hx : 0 = ‖x‖
⊢ ‖↑n‖ * ‖x‖ ≤ ‖x‖

Tactic:
simp only [← hx, mul_zero, le_refl]

Result:
no goals

Proof state:
case inl.intro.inr
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm✝ : 1 ⊔ ‖x‖ ^ m = 1
hx : ‖x‖ ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
hm : m ≠ 0
⊢ ‖x‖ ^ i ≤ 1

Tactic:
exact pow_le_one₀ (norm_nonneg _) hx

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : 1 ⊔ ‖x‖ ^ m = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ i ≤ m

Tactic:
simpa only [Finset.mem_range, Nat.lt_succ] using hi

Result:
no goals

Proof state:
case inl.intro
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : 1 ⊔ ‖x‖ ^ m = 1
hx : ‖x‖ ^ m ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ ‖x‖ ^ i ≤ 1

Tactic:
rcases eq_or_ne m 0 with rfl | hm

Result:
case inl.intro.inl
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
i : ℕ
hm : 1 ⊔ ‖x‖ ^ 0 = 1
hx : ‖x‖ ^ 0 ≤ 1
hi : i ∈ Finset.range (0 + 1)
⊢ ‖x‖ ^ i ≤ 1

case inl.intro.inr
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm✝ : 1 ⊔ ‖x‖ ^ m = 1
hx : ‖x‖ ^ m ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
hm : m ≠ 0
⊢ ‖x‖ ^ i ≤ 1

Proof state:
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
i : ℕ
hm : 1 ⊔ ‖x‖ ^ 0 = 1
hx : ‖x‖ ^ 0 ≤ 1
hi : i ∈ Finset.range (0 + 1)
⊢ i = 0

Tactic:
simpa only [zero_add, Finset.range_one, Finset.mem_singleton] using hi

Result:
no goals

Proof state:
case inl.intro.inl
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
i : ℕ
hm : 1 ⊔ ‖x‖ ^ 0 = 1
hx : ‖x‖ ^ 0 ≤ 1
hi : i ∈ Finset.range (0 + 1)
⊢ ‖x‖ ^ i ≤ 1

Tactic:
simp only [pow_zero, le_refl,
  show i = 0 by simpa only [zero_add, Finset.range_one, Finset.mem_singleton] using hi]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
⊢ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k ≤ ∑ _x ∈ Finset.range (m + 1), 1 ⊔ ‖x‖ ^ m

Tactic:
rcases max_cases 1 (‖x‖ ^ m) with (⟨hm, hx⟩|⟨hm, hx⟩) <;> rw [hm] <;>
refine Finset.sum_le_sum fun i hi ↦ ?_

Result:
case inl.intro
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : 1 ⊔ ‖x‖ ^ m = 1
hx : ‖x‖ ^ m ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ ‖x‖ ^ i ≤ 1

case inr.intro
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : 1 ⊔ ‖x‖ ^ m = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ ‖x‖ ^ i ≤ ‖x‖ ^ m

Proof state:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (n : ℕ), ‖↑n‖ ≤ 1
x✝ : R
m : ℕ
x : R
n : ℕ
⊢ ‖n • x‖ ≤ ‖x‖

Tactic:
rw [nsmul_eq_mul, norm_mul]

Result:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (n : ℕ), ‖↑n‖ ≤ 1
x✝ : R
m : ℕ
x : R
n : ℕ
⊢ ‖↑n‖ * ‖x‖ ≤ ‖x‖

Proof state:
case inr.intro
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : 1 ⊔ ‖x‖ ^ m = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ ‖x‖ ^ i ≤ ‖x‖ ^ m

Tactic:
refine pow_le_pow_right₀ ?_ (by simpa only [Finset.mem_range, Nat.lt_succ] using hi)

Result:
case inr.intro
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : 1 ⊔ ‖x‖ ^ m = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ 1 ≤ ‖x‖

Proof state:
case inr
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (n : ℕ), ‖↑n‖ ≤ 1
x✝ : R
m : ℕ
x : R
n : ℕ
hx : 0 < ‖x‖
⊢ ‖↑n‖ * ‖x‖ ≤ ‖x‖

Tactic:
simpa only [mul_le_iff_le_one_left hx] using h _

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (n : ℕ), ‖↑n‖ ≤ 1
⊢ IsUltrametricDist R

Tactic:
refine isUltrametricDist_of_forall_pow_norm_le_nsmul_pow_max_one_norm (fun x m ↦ ?_)

Result:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (n : ℕ), ‖↑n‖ ≤ 1
x : R
m : ℕ
⊢ ‖x + 1‖ ^ m ≤ (m + 1) • (1 ⊔ ‖x‖ ^ m)