-- Mathlib/Algebra/Order/Field/Basic.lean
theorem uniform_continuous_npow_on_bounded (B : α) {ε : α} (hε : 0 < ε) (n : ℕ) :
    ∃ δ > 0, ∀ q r : α, |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε

Tactic:
refine ⟨min 1 (ε / (1 + n * (B + 1) ^ (n - 1))), lt_min zero_lt_one (div_pos hε pos),
  fun q r hr hqr ↦ (abs_pow_sub_pow_le ..).trans_lt ?_⟩

Result:
α : Type u_2
inst✝ : LinearOrderedField α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ⊓ ε / (1 + ↑n * (B + 1) ^ (n - 1))
⊢ |q - r| * ↑n * (|q| ⊔ |r|) ^ (n - 1) < ε

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε

Tactic:
have pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1) := zero_lt_one.trans_le <| le_add_of_nonneg_right <|
  mul_nonneg n.cast_nonneg <| (pow_pos (B_pos.trans <| lt_add_of_pos_right _ zero_lt_one) _).le

Result:
α : Type u_2
inst✝ : LinearOrderedField α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε

Proof state:
case inr
α : Type u_2
inst✝ : LinearOrderedField α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * ↑n * (B + 1) ^ (n - 1) ≤ ε
h : 0 < |q - r|
⊢ |q| ≤ B + 1

Tactic:
exact add_sub_cancel r q ▸ (abs_add_le ..).trans (add_le_add hr hqr.1)

Result:
no goals

Proof state:
case inr
α : Type u_2
inst✝ : LinearOrderedField α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * ↑n * (B + 1) ^ (n - 1) ≤ ε
h : 0 < |q - r|
⊢ |q| ⊔ |r| ≤ B + 1

Tactic:
refine max_le ?_ (hr.trans <| le_add_of_nonneg_right zero_le_one)

Result:
case inr
α : Type u_2
inst✝ : LinearOrderedField α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * ↑n * (B + 1) ^ (n - 1) ≤ ε
h : 0 < |q - r|
⊢ |q| ≤ B + 1

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
B ε : α
hε : 0 < ε
n : ℕ
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε

Tactic:
wlog B_pos : 0 < B generalizing B

Result:
case inr
α : Type u_2
inst✝ : LinearOrderedField α
B ε : α
hε : 0 < ε
n : ℕ
this : ∀ (B : α), 0 < B → ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
B_pos : ¬0 < B
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε

α : Type u_2
inst✝ : LinearOrderedField α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε

Proof state:
case inr
α : Type u_2
inst✝ : LinearOrderedField α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * ↑n * (B + 1) ^ (n - 1) ≤ ε
h : 0 < |q - r|
⊢ |q - r| * ↑n * (|q| ⊔ |r|) ^ (n - 1) < ε

Tactic:
refine (lt_of_le_of_lt ?_ <| lt_add_of_pos_left _ h).trans_le hqr.2

Result:
case inr
α : Type u_2
inst✝ : LinearOrderedField α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * ↑n * (B + 1) ^ (n - 1) ≤ ε
h : 0 < |q - r|
⊢ |q - r| * ↑n * (|q| ⊔ |r|) ^ (n - 1) ≤ |q - r| * ↑n * (B + 1) ^ (n - 1)

Proof state:
case inr
α : Type u_2
inst✝ : LinearOrderedField α
B ε : α
hε : 0 < ε
n : ℕ
this : ∀ (B : α), 0 < B → ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
B_pos : ¬0 < B
δ : α
δ_pos : δ > 0
cont : ∀ (q r : α), |r| ≤ 1 → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε

Tactic:
exact ⟨δ, δ_pos, fun q r hr ↦ cont q r (hr.trans ((le_of_not_lt B_pos).trans zero_le_one))⟩

Result:
no goals

Proof state:
case inr
α : Type u_2
inst✝ : LinearOrderedField α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * ↑n * (B + 1) ^ (n - 1) ≤ ε
h : 0 < |q - r|
⊢ |q - r| * ↑n * (|q| ⊔ |r|) ^ (n - 1) ≤ |q - r| * ↑n * (B + 1) ^ (n - 1)

Tactic:
refine mul_le_mul_of_nonneg_left (pow_le_pow_left₀ ((abs_nonneg _).trans le_sup_left) ?_ _)
  (mul_nonneg (abs_nonneg _) n.cast_nonneg)

Result:
case inr
α : Type u_2
inst✝ : LinearOrderedField α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * ↑n * (B + 1) ^ (n - 1) ≤ ε
h : 0 < |q - r|
⊢ |q| ⊔ |r| ≤ B + 1

Proof state:
case inl
α : Type u_2
inst✝ : LinearOrderedField α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * ↑n * (B + 1) ^ (n - 1) ≤ ε
h : 0 = |q - r|
⊢ |q - r| * ↑n * (|q| ⊔ |r|) ^ (n - 1) < ε

Tactic:
simpa only [← h, zero_mul] using hε

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * ↑n * (B + 1) ^ (n - 1) ≤ ε
⊢ |q - r| * ↑n * (|q| ⊔ |r|) ^ (n - 1) < ε

Tactic:
obtain h | h := (abs_nonneg (q - r)).eq_or_lt

Result:
case inl
α : Type u_2
inst✝ : LinearOrderedField α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * ↑n * (B + 1) ^ (n - 1) ≤ ε
h : 0 = |q - r|
⊢ |q - r| * ↑n * (|q| ⊔ |r|) ^ (n - 1) < ε

case inr
α : Type u_2
inst✝ : LinearOrderedField α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * ↑n * (B + 1) ^ (n - 1) ≤ ε
h : 0 < |q - r|
⊢ |q - r| * ↑n * (|q| ⊔ |r|) ^ (n - 1) < ε

Proof state:
case inr
α : Type u_2
inst✝ : LinearOrderedField α
B ε : α
hε : 0 < ε
n : ℕ
this : ∀ (B : α), 0 < B → ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
B_pos : ¬0 < B
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε

Tactic:
have ⟨δ, δ_pos, cont⟩ := this 1 zero_lt_one

Result:
case inr
α : Type u_2
inst✝ : LinearOrderedField α
B ε : α
hε : 0 < ε
n : ℕ
this : ∀ (B : α), 0 < B → ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
B_pos : ¬0 < B
δ : α
δ_pos : δ > 0
cont : ∀ (q r : α), |r| ≤ 1 → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ⊓ ε / (1 + ↑n * (B + 1) ^ (n - 1))
⊢ |q - r| * ↑n * (|q| ⊔ |r|) ^ (n - 1) < ε

Tactic:
rw [le_inf_iff, le_div_iff₀ pos, mul_one_add, ← mul_assoc] at hqr

Result:
α : Type u_2
inst✝ : LinearOrderedField α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * ↑n * (B + 1) ^ (n - 1) ≤ ε
⊢ |q - r| * ↑n * (|q| ⊔ |r|) ^ (n - 1) < ε