awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
K : Type u_4
val : NontriviallyNormedField K
h : IsComplete.{u_4} (α := K) (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ ‖u n‖)) k
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq (α := K) ((fun (x_1 : K) ↦ x_1 / x) ∘ u)
hb : ∀ (n : ℕ), Membership.mem (γ := Set K) (closedBall 0 1) (((fun (x_1 : K) ↦ x_1 / x) ∘ u) n)
mpr : ∀ (a : K) (ha' : Tendsto ((fun (x_1 : K) ↦ x_1 / x) ∘ u) atTop (𝓝 a)), ∃ (a : K), Tendsto u atTop (𝓝 a)
⊢ ∃ (a : K), Tendsto u atTop (𝓝 a)

Tactic:
obtain ⟨a, -, ha'⟩ := cauchySeq_tendsto_of_isComplete h hb hu'

Premises used: cauchySeq_tendsto_of_isComplete
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
K : Type u_4
val : NontriviallyNormedField K
h : IsComplete.{u_4} (α := K) (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ ‖u n‖)) k
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq (α := K) ((fun (x_1 : K) ↦ x_1 / x) ∘ u)
hb : ∀ (n : ℕ), Membership.mem (γ := Set K) (closedBall 0 1) (((fun (x_1 : K) ↦ x_1 / x) ∘ u) n)
a : K
ha' : Tendsto ((fun (x_1 : K) ↦ x_1 / x) ∘ u) atTop (𝓝 a)
⊢ ∃ (a : K), Tendsto u atTop (𝓝 a)

Tactic:
⟨a * x, (((continuous_mul_const x).tendsto a).comp ha').congr ?_⟩

Premises used: HMul.hMul, Continuous.tendsto, Exists.intro, Filter.Tendsto.congr, Filter.Tendsto.comp, continuous_mul_const
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
K : Type u_4
val : NontriviallyNormedField K
h : IsComplete.{u_4} (α := K) (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ ‖u n‖)) k
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq (α := K) ((fun (x_1 : K) ↦ x_1 / x) ∘ u)
hb : ∀ (n : ℕ), Membership.mem (γ := Set K) (closedBall 0 1) (((fun (x_1 : K) ↦ x_1 / x) ∘ u) n)
a : K
ha' : Tendsto ((fun (x_1 : K) ↦ x_1 / x) ∘ u) atTop (𝓝 a)
mpr : ∀ (x_1 : ℕ), ((fun (x_2 : K) ↦ x_2 * x) ∘ (fun (x_2 : K) ↦ x_2 / x) ∘ u) x_1 = u x_1
⊢ ∃ (a : K), Tendsto u atTop (𝓝 a)

Tactic:
refine ⟨a * x, (((continuous_mul_const x).tendsto a).comp ha').congr ?_⟩
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
K : Type u_4
val : NontriviallyNormedField K
h : IsComplete.{u_4} (α := K) (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ ‖u n‖)) k
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq (α := K) ((fun (x_1 : K) ↦ x_1 / x) ∘ u)
hb : ∀ (n : ℕ), Membership.mem (γ := Set K) (closedBall 0 1) (((fun (x_1 : K) ↦ x_1 / x) ∘ u) n)
a : K
ha' : Tendsto ((fun (x_1 : K) ↦ x_1 / x) ∘ u) atTop (𝓝 a)
contrapose! : ∀ (hx : x = 0), ‖x‖ ≤ k
⊢ x ≠ 0

Tactic:
contrapose! hx
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
K : Type u_4
val : NontriviallyNormedField K
h : IsComplete.{u_4} (α := K) (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ ‖u n‖)) k
kpos : 0 ≤ k
x : K
hu' : CauchySeq (α := K) ((fun (x_1 : K) ↦ x_1 / x) ∘ u)
hb : ∀ (n : ℕ), Membership.mem (γ := Set K) (closedBall 0 1) (((fun (x_1 : K) ↦ x_1 / x) ∘ u) n)
a : K
ha' : Tendsto ((fun (x_1 : K) ↦ x_1 / x) ∘ u) atTop (𝓝 a)
hx : x = 0
⊢ ‖x‖ ≤ k

Tactic:
simp [hx, kpos]
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
K : Type u_4
val : NontriviallyNormedField K
h : IsComplete.{u_4} (α := K) (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ ‖u n‖)) k
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq (α := K) ((fun (x_1 : K) ↦ x_1 / x) ∘ u)
hb : ∀ (n : ℕ), Membership.mem (γ := Set K) (closedBall 0 1) (((fun (x_1 : K) ↦ x_1 / x) ∘ u) n)
a : K
ha' : Tendsto ((fun (x_1 : K) ↦ x_1 / x) ∘ u) atTop (𝓝 a)
⊢ x ≠ 0

Tactic:
have hx' : x ≠ 0 := by
    contrapose! hx
    simp [hx, kpos]
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
K : Type u_4
val : NontriviallyNormedField K
h : IsComplete.{u_4} (α := K) (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ ‖u n‖)) k
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq (α := K) ((fun (x_1 : K) ↦ x_1 / x) ∘ u)
hb : ∀ (n : ℕ), Membership.mem (γ := Set K) (closedBall 0 1) (((fun (x_1 : K) ↦ x_1 / x) ∘ u) n)
a : K
ha' : Tendsto ((fun (x_1 : K) ↦ x_1 / x) ∘ u) atTop (𝓝 a)
hx' : x ≠ 0
⊢ ∀ (x_1 : ℕ), ((fun (x_2 : K) ↦ x_2 * x) ∘ (fun (x_2 : K) ↦ x_2 / x) ∘ u) x_1 = u x_1

Tactic:
simp [div_mul_cancel₀ _ hx']

Premises used: div_mul_cancel₀
-- Module: Mathlib.Analysis.Normed.Field.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : WeaklyLocallyCompactSpace 𝕜
rcases : ∀ (r : ℝ) (rpos : 0 < r) (hr : IsCompact.{u_1} (X := 𝕜) (closedBall 0 r)), ProperSpace 𝕜
⊢ ProperSpace 𝕜

Tactic:
rcases exists_isCompact_closedBall (0 : 𝕜) with ⟨r, rpos, hr⟩

Premises used: Metric.exists_isCompact_closedBall, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Field.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact.{u_1} (X := 𝕜) (closedBall 0 r)
rcases : ∀ (c : 𝕜) (hc : 1 < ‖c‖), ProperSpace 𝕜
⊢ ProperSpace 𝕜

Tactic:
rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩

Premises used: NormedField.exists_one_lt_norm
-- Module: Mathlib.Analysis.Normed.Field.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact.{u_1} (X := 𝕜) (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
h : c = 0
⊢ False

Tactic:
simp [h, zero_le_one.not_gt] at hc

Premises used: zero_le_one, LE.le.not_gt
-- Module: Mathlib.Analysis.Normed.Field.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact.{u_1} (X := 𝕜) (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
⊢ c ^ n ≠ 0

Tactic:
have : c ^ n ≠ 0 := pow_ne_zero _ <| fun h ↦ by simp [h, zero_le_one.not_gt] at hc
-- Module: Mathlib.Analysis.Normed.Field.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact.{u_1} (X := 𝕜) (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
this : c ^ n ≠ 0
⊢ IsCompact (HSMul.hSMul (β := Set 𝕜) (c ^ n) (closedBall 0 r))

Tactic:
hr.smul (c ^ n)

Premises used: HPow.hPow, IsCompact.smul
-- Module: Mathlib.Analysis.Normed.Field.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact.{u_1} (X := 𝕜) (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
this : c ^ n ≠ 0
h : closedBall 0 (‖c‖ ^ n * r) = HSMul.hSMul (β := Set 𝕜) (c ^ n) (closedBall 0 r)
⊢ IsCompact.{u_1} (X := 𝕜) (closedBall 0 (‖c‖ ^ n * r))

Tactic:
convert! hr.smul (c ^ n)

Premises used: HPow.hPow, IsCompact.smul
-- Module: Mathlib.Analysis.Normed.Field.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact.{u_1} (X := 𝕜) (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
this : c ^ n ≠ 0
h :
  ∀ (x : 𝕜),
    Membership.mem (γ := Set 𝕜) (closedBall 0 (‖c‖ ^ n * r)) x ↔ x ∈ HSMul.hSMul (β := Set 𝕜) (c ^ n) (closedBall 0 r)
⊢ closedBall 0 (‖c‖ ^ n * r) = HSMul.hSMul (β := Set 𝕜) (c ^ n) (closedBall 0 r)

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Field.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact.{u_1} (X := 𝕜) (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
this : c ^ n ≠ 0
x : 𝕜
⊢ 0 < ‖c‖ ^ n

Tactic:
simpa only [norm_pow] using norm_pos_iff.mpr this

Premises used: Iff.mpr, norm_pos_iff, norm_pow
-- Module: Mathlib.Analysis.Normed.Field.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact.{u_1} (X := 𝕜) (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
this : c ^ n ≠ 0
x : 𝕜
⊢ Membership.mem (γ := Set 𝕜) (closedBall 0 (‖c‖ ^ n * r)) x ↔ x ∈ HSMul.hSMul (β := Set 𝕜) (c ^ n) (closedBall 0 r)

Tactic:
simp only [mem_closedBall, dist_zero_right, Set.mem_smul_set_iff_inv_smul_mem₀ this,
      smul_eq_mul, norm_mul, norm_inv, norm_pow,
      inv_mul_le_iff₀ (by simpa only [norm_pow] using norm_pos_iff.mpr this)]

Premises used: norm_pow, norm_mul, norm_inv, inv_mul_le_iff₀, Metric.mem_closedBall, smul_eq_mul, dist_zero_right, Set.mem_smul_set_iff_inv_smul_mem₀
-- Module: Mathlib.Analysis.Normed.Field.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact.{u_1} (X := 𝕜) (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
⊢ ∀ (n : ℕ), IsCompact.{u_1} (X := 𝕜) (closedBall 0 (‖c‖ ^ n * r))

Tactic:
have hC n : IsCompact (closedBall (0 : 𝕜) (‖c‖ ^ n * r)) := by
    have : c ^ n ≠ 0 := pow_ne_zero _ <| fun h ↦ by simp [h, zero_le_one.not_gt] at hc
    convert! hr.smul (c ^ n)
    ext
    simp only [mem_closedBall, dist_zero_right, Set.mem_smul_set_iff_inv_smul_mem₀ this,
      smul_eq_mul, norm_mul, norm_inv, norm_pow,
      inv_mul_le_iff₀ (by simpa only [norm_pow] using norm_pos_iff.mpr this)]
-- Module: Mathlib.Analysis.Normed.Field.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact.{u_1} (X := 𝕜) (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
hC : ∀ (n : ℕ), IsCompact.{u_1} (X := 𝕜) (closedBall 0 (‖c‖ ^ n * r))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c‖ ^ n * r) atTop atTop

Tactic:
have hTop : Tendsto (fun n ↦ ‖c‖ ^ n * r) atTop atTop :=
    Tendsto.atTop_mul_const rpos (tendsto_pow_atTop_atTop_of_one_lt hc)
-- Module: Mathlib.Analysis.Normed.Field.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact.{u_1} (X := 𝕜) (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
hC : ∀ (n : ℕ), IsCompact.{u_1} (X := 𝕜) (closedBall 0 (‖c‖ ^ n * r))
hTop : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c‖ ^ n * r) atTop atTop
⊢ ProperSpace 𝕜

Tactic:
.of_seq_closedBall hTop (Eventually.of_forall hC)

Premises used: ProperSpace.of_seq_closedBall, Filter.Eventually.of_forall
-- Module: Mathlib.Analysis.Normed.Field.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact.{u_1} (X := 𝕜) (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
hC : ∀ (n : ℕ), IsCompact.{u_1} (X := 𝕜) (closedBall 0 (‖c‖ ^ n * r))
hTop : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c‖ ^ n * r) atTop atTop
⊢ ProperSpace 𝕜

Tactic:
exact .of_seq_closedBall hTop (Eventually.of_forall hC)
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x + 1‖ ≤ max ‖x‖ 1
⊢ IsUltrametricDist R

Tactic:
isUltrametricDist_of_forall_norm_add_le_max_norm (fun x y ↦ ?_)

Premises used: IsUltrametricDist.isUltrametricDist_of_forall_norm_add_le_max_norm
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x + 1‖ ≤ max ‖x‖ 1
refine : ∀ (x y : R), ‖x + y‖ ≤ max ‖x‖ ‖y‖
⊢ IsUltrametricDist R

Tactic:
refine isUltrametricDist_of_forall_norm_add_le_max_norm (fun x y ↦ ?_)

Premises used: IsUltrametricDist.isUltrametricDist_of_forall_norm_add_le_max_norm
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x + 1‖ ≤ max ‖x‖ 1
x y : R
inl : ‖x + 0‖ ≤ max ‖x‖ (norm.{u_1} (E := R) 0)
inr : ∀ (hy : y ≠ 0), ‖x + y‖ ≤ max ‖x‖ ‖y‖
⊢ ‖x + y‖ ≤ max ‖x‖ ‖y‖

Tactic:
rcases eq_or_ne y 0 with rfl | hy

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x + 1‖ ≤ max ‖x‖ 1
x : R
⊢ ‖x + 0‖ ≤ max ‖x‖ (norm.{u_1} (E := R) 0)

Tactic:
simpa only [add_zero] using le_max_left _ _

Premises used: add_zero, le_max_left
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x + 1‖ ≤ max ‖x‖ 1
x y : R
hy : y ≠ 0
⊢ 0 < ‖y‖

Tactic:
have p : 0 < ‖y‖ := norm_pos_iff.mpr hy
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x + 1‖ ≤ max ‖x‖ 1
x y : R
hy : y ≠ 0
p : 0 < ‖y‖
⊢ ‖x + y‖ ≤ max ‖x‖ ‖y‖

Tactic:
simpa only [div_add_one hy, norm_div, div_le_iff₀ p, max_mul_of_nonneg _ _ p.le, one_mul,
      div_mul_cancel₀ _ p.ne'] using h (x / y)

Premises used: div_le_iff₀, div_mul_cancel₀, max_mul_of_nonneg, HDiv.hDiv, LT.lt.le, LT.lt.ne', div_add_one, norm_div, one_mul
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
⊢ IsUltrametricDist R

Tactic:
isUltrametricDist_of_forall_norm_add_one_le_max_norm_one fun x ↦ ?_

Premises used: IsUltrametricDist.isUltrametricDist_of_forall_norm_add_one_le_max_norm_one
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
refine : ∀ (x : R), ‖x + 1‖ ≤ max ‖x‖ 1
⊢ IsUltrametricDist R

Tactic:
refine isUltrametricDist_of_forall_norm_add_one_le_max_norm_one fun x ↦ ?_

Premises used: IsUltrametricDist.isUltrametricDist_of_forall_norm_add_one_le_max_norm_one
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
inl : ∀ (H : ‖x‖ ≤ 1), ‖x + 1‖ ≤ max ‖x‖ 1
inr : ∀ (H : 1 < ‖x‖), ‖x + 1‖ ≤ max ‖x‖ 1
⊢ ‖x + 1‖ ≤ max ‖x‖ 1

Tactic:
rcases le_or_gt ‖x‖ 1 with H | H

Premises used: Norm.norm, le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : ‖x‖ ≤ 1
⊢ ‖x + 1‖ ≤ max ‖x‖ 1

Tactic:
(h _ H).trans (le_max_right _ _)

Premises used: le_max_right, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : ‖x‖ ≤ 1
⊢ ‖x + 1‖ ≤ max ‖x‖ 1

Tactic:
exact (h _ H).trans (le_max_right _ _)

Premises used: le_max_right, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : 1 < ‖x‖
inr : ‖x + 1‖ ≤ ‖x‖
⊢ ‖x + 1‖ ≤ max ‖x‖ 1

Tactic:
suffices ‖x + 1‖ ≤ ‖x‖ from this.trans (le_max_left _ _)
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : 1 < ‖x‖
⊢ 0 < ‖x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : 1 < ‖x‖
⊢ x ≠ 0

Tactic:
simpa using H.trans' zero_lt_one

Premises used: LT.lt.trans', zero_lt_one
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : 1 < ‖x‖
inr : ‖1 / x + 1‖ ≤ 1
⊢ ‖x + 1‖ ≤ ‖x‖

Tactic:
rw [← div_le_one (by positivity), ← norm_div, add_div,
      div_self (by simpa using H.trans' zero_lt_one), add_comm]

Premises used: add_comm, div_le_one, norm_div, div_self, add_div
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : 1 < ‖x‖
inr : ‖1 / x‖ ≤ 1
⊢ ‖1 / x + 1‖ ≤ 1

Tactic:
apply h
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : 1 < ‖x‖
⊢ ‖1 / x‖ ≤ 1

Tactic:
simp [inv_le_one_iff₀, H.le]

Premises used: inv_le_one_iff₀, LT.lt.le
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x - 1‖ ≤ 1
x : R
hx : ‖x‖ ≤ 1
⊢ ‖x + 1‖ ≤ 1

Tactic:
simpa only [← neg_add', norm_neg] using h (-x) (norm_neg x ▸ hx)

Premises used: Eq.rec, neg_add', norm_neg, Eq.symm, Neg.neg
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x - 1‖ ≤ 1
⊢ ∀ (x : R) (hx : ‖x‖ ≤ 1), ‖x + 1‖ ≤ 1

Tactic:
have (x : R) (hx : ‖x‖ ≤ 1) : ‖x + 1‖ ≤ 1 := by
    simpa only [← neg_add', norm_neg] using h (-x) (norm_neg x ▸ hx)
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x - 1‖ ≤ 1
this : ∀ (x : R) (hx : ‖x‖ ≤ 1), ‖x + 1‖ ≤ 1
⊢ IsUltrametricDist R

Tactic:
isUltrametricDist_of_forall_norm_add_one_of_norm_le_one this

Premises used: IsUltrametricDist.isUltrametricDist_of_forall_norm_add_one_of_norm_le_one
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x - 1‖ ≤ 1
this : ∀ (x : R) (hx : ‖x‖ ≤ 1), ‖x + 1‖ ≤ 1
⊢ IsUltrametricDist R

Tactic:
exact isUltrametricDist_of_forall_norm_add_one_of_norm_le_one this

Premises used: IsUltrametricDist.isUltrametricDist_of_forall_norm_add_one_of_norm_le_one
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
⊢ IsUltrametricDist R

Tactic:
isUltrametricDist_of_forall_norm_add_one_le_max_norm_one fun x ↦ ?_

Premises used: IsUltrametricDist.isUltrametricDist_of_forall_norm_add_one_le_max_norm_one
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
refine : ∀ (x : R), ‖x + 1‖ ≤ max ‖x‖ 1
⊢ IsUltrametricDist R

Tactic:
refine isUltrametricDist_of_forall_norm_add_one_le_max_norm_one fun x ↦ ?_

Premises used: IsUltrametricDist.isUltrametricDist_of_forall_norm_add_one_le_max_norm_one
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
x : R
rw : ‖x + 1‖ ≤ max 1 ‖x‖
⊢ ‖x + 1‖ ≤ max ‖x‖ 1

Tactic:
rw [max_comm]

Premises used: max_comm
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
x : R
⊢ ‖x + 1‖ ≤ max 1 ‖x‖

Tactic:
le_of_forall_gt_imp_ge_of_dense fun a ha ↦ ?_

Premises used: le_of_forall_gt_imp_ge_of_dense
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
x : R
refine : ∀ (a : ℝ) (ha : max 1 ‖x‖ < a), ‖x + 1‖ ≤ a
⊢ ‖x + 1‖ ≤ max 1 ‖x‖

Tactic:
refine le_of_forall_gt_imp_ge_of_dense fun a ha ↦ ?_

Premises used: le_of_forall_gt_imp_ge_of_dense
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
x : R
a : ℝ
ha : max 1 ‖x‖ < a
⊢ 1 < a

Tactic:
have ha' : 1 < a := (max_lt_iff.mp ha).left
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
x : R
a : ℝ
ha : max 1 ‖x‖ < a
ha' : 1 < a
apply_mod_cast : 1 < a / max 1 ‖x‖
⊢ ∃ (m : ℕ), (↑(m + 1) : ℝ) < (a / max 1 ‖x‖) ^ m

Tactic:
apply_mod_cast Real.exists_natCast_add_one_lt_pow_of_one_lt

Premises used: Real.exists_natCast_add_one_lt_pow_of_one_lt
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
x : R
a : ℝ
ha : max 1 ‖x‖ < a
ha' : 1 < a
⊢ 0 < max 1 ‖x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
x : R
a : ℝ
ha : max 1 ‖x‖ < a
ha' : 1 < a
rwa rwa₁ rwa₂ rwa₃ : max 1 ‖x‖ < a
⊢ 1 < a / max 1 ‖x‖

Tactic:
rwa [one_lt_div (by positivity)]

Premises used: one_lt_div
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
x : R
a : ℝ
ha : max 1 ‖x‖ < a
ha' : 1 < a
obtain : ∀ (m : ℕ) (hm : (↑(m + 1) : ℝ) < (a / max 1 ‖x‖) ^ m), ‖x + 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)]

Premises used: Norm.norm, HDiv.hDiv, Max.max, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
x : R
a : ℝ
ha : max 1 ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : (↑(m + 1) : ℝ) < a ^ m / max 1 ‖x‖ ^ m
⊢ 0 < max 1 ‖x‖ ^ m

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
x : R
a : ℝ
ha : max 1 ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : (↑(m + 1) : ℝ) < (a / max 1 ‖x‖) ^ m
⊢ (m + 1) • max 1 ‖x‖ ^ m < a ^ m

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

Premises used: lt_div_iff₀, div_pow, nsmul_eq_mul
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
x : R
a : ℝ
ha : max 1 ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : (m + 1) • max 1 ‖x‖ ^ m < a ^ m
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | 0 ≤ x} 1

Tactic:
simp [zero_le_one]

Premises used: zero_le_one
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
x : R
a : ℝ
ha : max 1 ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : (m + 1) • max 1 ‖x‖ ^ m < a ^ m
rw : max (HPow.hPow (α := ℝ) 1 m) (‖x‖ ^ m) = max 1 (‖x‖ ^ m)
rw₁ rw₂ : max 1 (‖x‖ ^ m) = max 1 (‖x‖ ^ m)
⊢ max 1 ‖x‖ ^ m = max 1 (‖x‖ ^ m)

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

Premises used: one_pow, pow_left_monotoneOn, MonotoneOn.map_max
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
x : R
a : ℝ
ha : max 1 ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : (m + 1) • max 1 ‖x‖ ^ m < a ^ m
⊢ max 1 ‖x‖ ^ m = max 1 (‖x‖ ^ m)

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]
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
x : R
a : ℝ
ha : max 1 ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : (m + 1) • max 1 ‖x‖ ^ m < a ^ m
hp : max 1 ‖x‖ ^ m = max 1 (‖x‖ ^ m)
⊢ (m + 1) • max 1 (‖x‖ ^ m) < a ^ m

Tactic:
rw [hp] at hm
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
x : R
a : ℝ
ha : max 1 ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : (m + 1) • max 1 ‖x‖ ^ m < a ^ m
hp : max 1 ‖x‖ ^ m = max 1 (‖x‖ ^ m)
hm₁ : (m + 1) • max 1 (‖x‖ ^ m) < a ^ m
⊢ max 1 ‖x‖ ^ m = max 1 (‖x‖ ^ m)

Tactic:
rw [hp] at hm
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
x : R
a : ℝ
ha : max 1 ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : (m + 1) • max 1 (‖x‖ ^ m) < a ^ m
hp : max 1 ‖x‖ ^ m = max 1 (‖x‖ ^ m)
⊢ ‖x + 1‖ ≤ a

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

Premises used: LT.lt.le, zero_lt_one, LT.lt.trans, le_of_pow_le_pow_left₀, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
x : R
a : ℝ
ha : max 1 ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : (m + 1) • max 1 (‖x‖ ^ m) < a ^ m
hp : max 1 ‖x‖ ^ m = max 1 (‖x‖ ^ m)
refine : ∀ (h : m = 0), False
⊢ ‖x + 1‖ ≤ a

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

Premises used: LT.lt.le, zero_lt_one, LT.lt.trans, le_of_pow_le_pow_left₀, LE.le.trans