-- Mathlib/Analysis/Normed/Field/Ultra.lean
/-- This technical lemma is used in the proof of
`isUltrametricDist_of_forall_norm_natCast_le_one`. -/
lemma isUltrametricDist_of_forall_pow_norm_le_nsmul_pow_max_one_norm
    (h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)) :
    IsUltrametricDist R

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

Tactic:
refine isUltrametricDist_of_forall_norm_add_one_le_max_norm_one fun x ↦ ?_

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

Proof state:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • (1 ⊔ ‖x‖ ^ m)
x : R
a : ℝ
ha : 1 ⊔ ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : ↑(m + 1) < a ^ m / (1 ⊔ ‖x‖) ^ m
⊢ 0 < (1 ⊔ ‖x‖) ^ m

Tactic:
positivity

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • (1 ⊔ ‖x‖ ^ m)
x : R
a : ℝ
ha : 1 ⊔ ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : (m + 1) • (1 ⊔ ‖x‖) ^ m < a ^ m
⊢ 1 ∈ {x | 0 ≤ x}

Tactic:
simp [zero_le_one]

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • (1 ⊔ ‖x‖ ^ m)
x : R
a : ℝ
ha : 1 ⊔ ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : (m + 1) • (1 ⊔ ‖x‖ ^ m) < a ^ m
hp : (1 ⊔ ‖x‖) ^ m = 1 ⊔ ‖x‖ ^ m
⊢ ‖x + 1‖ ≤ a

Tactic:
refine le_of_pow_le_pow_left₀ (fun h ↦ ?_) (zero_lt_one.trans ha').le ((h _ _).trans hm.le)

Result:
case intro
R : Type u_1
inst✝ : NormedDivisionRing R
h✝ : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • (1 ⊔ ‖x‖ ^ m)
x : R
a : ℝ
ha : 1 ⊔ ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : (m + 1) • (1 ⊔ ‖x‖ ^ m) < a ^ m
hp : (1 ⊔ ‖x‖) ^ m = 1 ⊔ ‖x‖ ^ m
h : m = 0
⊢ False

Proof state:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • (1 ⊔ ‖x‖ ^ m)
x : R
a : ℝ
ha : 1 ⊔ ‖x‖ < a
ha' : 1 < a
⊢ ∃ m, ↑(m + 1) < (a / (1 ⊔ ‖x‖)) ^ m

Tactic:
apply_mod_cast Real.exists_natCast_add_one_lt_pow_of_one_lt

Result:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • (1 ⊔ ‖x‖ ^ m)
x : R
a : ℝ
ha : 1 ⊔ ‖x‖ < a
ha' : 1 < a
⊢ 1 < a / (1 ⊔ ‖x‖)

Proof state:
case intro
R : Type u_1
inst✝ : NormedDivisionRing R
h✝ : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • (1 ⊔ ‖x‖ ^ m)
x : R
a : ℝ
ha : 1 ⊔ ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : (m + 1) • (1 ⊔ ‖x‖ ^ m) < a ^ m
hp : (1 ⊔ ‖x‖) ^ m = 1 ⊔ ‖x‖ ^ m
h : m = 0
⊢ False

Tactic:
simp only [h, zero_add, pow_zero, max_self, one_smul, lt_self_iff_false] at hm

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • (1 ⊔ ‖x‖ ^ m)
x : R
a : ℝ
ha : 1 ⊔ ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : ↑(m + 1) < (a / (1 ⊔ ‖x‖)) ^ m
⊢ ‖x + 1‖ ≤ a

Tactic:
rw [div_pow, lt_div_iff₀ (by positivity), ← nsmul_eq_mul] at hm

Result:
case intro
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • (1 ⊔ ‖x‖ ^ m)
x : R
a : ℝ
ha : 1 ⊔ ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : (m + 1) • (1 ⊔ ‖x‖) ^ m < a ^ m
⊢ ‖x + 1‖ ≤ a

Proof state:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • (1 ⊔ ‖x‖ ^ m)
x : R
a : ℝ
ha : 1 ⊔ ‖x‖ < a
ha' : 1 < a
⊢ 0 < 1 ⊔ ‖x‖

Tactic:
positivity

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • (1 ⊔ ‖x‖ ^ m)
x : R
a : ℝ
ha : 1 ⊔ ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : (m + 1) • (1 ⊔ ‖x‖) ^ m < a ^ m
⊢ ‖x + 1‖ ≤ a

Tactic:
have hp : max 1 ‖x‖ ^ m = max 1 (‖x‖ ^ m) := by
  rw [pow_left_monotoneOn.map_max (by simp [zero_le_one]) (norm_nonneg x), one_pow]

Result:
case intro
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • (1 ⊔ ‖x‖ ^ m)
x : R
a : ℝ
ha : 1 ⊔ ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : (m + 1) • (1 ⊔ ‖x‖) ^ m < a ^ m
hp : (1 ⊔ ‖x‖) ^ m = 1 ⊔ ‖x‖ ^ m
⊢ ‖x + 1‖ ≤ a

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

Tactic:
have ha' : 1 < a := (max_lt_iff.mp ha).left

Result:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • (1 ⊔ ‖x‖ ^ m)
x : R
a : ℝ
ha : 1 ⊔ ‖x‖ < a
ha' : 1 < a
⊢ ‖x + 1‖ ≤ a

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

Tactic:
refine le_of_forall_gt_imp_ge_of_dense fun a ha ↦ ?_

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

Proof state:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • (1 ⊔ ‖x‖ ^ m)
x : R
a : ℝ
ha : 1 ⊔ ‖x‖ < a
ha' : 1 < a
⊢ 1 < a / (1 ⊔ ‖x‖)

Tactic:
rwa [one_lt_div (by positivity)]

Result:
no goals

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

Tactic:
obtain ⟨m, hm⟩ : ∃ m : ℕ, ((m + 1) : ℕ) < (a / (max 1 ‖x‖)) ^ m := by
  apply_mod_cast Real.exists_natCast_add_one_lt_pow_of_one_lt
  rwa [one_lt_div (by positivity)]

Result:
case intro
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • (1 ⊔ ‖x‖ ^ m)
x : R
a : ℝ
ha : 1 ⊔ ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : ↑(m + 1) < (a / (1 ⊔ ‖x‖)) ^ m
⊢ ‖x + 1‖ ≤ a

Proof state:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • (1 ⊔ ‖x‖ ^ m)
x : R
a : ℝ
ha : 1 ⊔ ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : (m + 1) • (1 ⊔ ‖x‖) ^ m < a ^ m
⊢ (1 ⊔ ‖x‖) ^ m = 1 ⊔ ‖x‖ ^ m

Tactic:
rw [pow_left_monotoneOn.map_max (by simp [zero_le_one]) (norm_nonneg x), one_pow]

Result:
no goals

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

Tactic:
rw [max_comm]

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

Proof state:
case intro
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • (1 ⊔ ‖x‖ ^ m)
x : R
a : ℝ
ha : 1 ⊔ ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : (m + 1) • (1 ⊔ ‖x‖) ^ m < a ^ m
hp : (1 ⊔ ‖x‖) ^ m = 1 ⊔ ‖x‖ ^ m
⊢ ‖x + 1‖ ≤ a

Tactic:
rw [hp] at hm

Result:
case intro
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • (1 ⊔ ‖x‖ ^ m)
x : R
a : ℝ
ha : 1 ⊔ ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : (m + 1) • (1 ⊔ ‖x‖ ^ m) < a ^ m
hp : (1 ⊔ ‖x‖) ^ m = 1 ⊔ ‖x‖ ^ m
⊢ ‖x + 1‖ ≤ a