awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
K : Type u_4
inst : NormedField K
h : IsComplete.{u_4} (α := K) (closedBall 0 1)
h_1 : DiscreteTopology K
⊢ CompleteSpace K
have mpr : IsComplete.{u_4} (α := K) Set.univ
Tactic: rwa [completeSpace_iff_isComplete_univ,
         ← NormedDivisionRing.unitClosedBall_eq_univ_of_discrete]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
K : Type u_4
val : NontriviallyNormedField K
h : IsComplete.{u_4} (α := K) (closedBall 0 1)
⊢ CompleteSpace K
have mpr : ∀ (u : ℕ → K) (hu : CauchySeq u), ∃ (a : K), Tendsto u atTop (𝓝 a)
Tactic: refine Metric.complete_of_cauchySeq_tendsto fun u hu ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
K : Type u_4
val : NontriviallyNormedField K
h : IsComplete.{u_4} (α := K) (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
⊢ ∃ (a : K), Tendsto u atTop (𝓝 a)
have mpr : ∀ (k : ℝ) (hk : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ ‖u n‖)) k),
  ∃ (a : K), Tendsto u atTop (𝓝 a)
Tactic: obtain ⟨k, hk⟩ := hu.norm_bddAbove
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (hypothesis)
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
⊢ ∃ (a : K), Tendsto u atTop (𝓝 a)
have kpos : 0 ≤ k
Tactic: have kpos : 0 ≤ k := (_root_.norm_nonneg (u 0)).trans (hk (by simp))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
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
⊢ ∃ (a : K), Tendsto u atTop (𝓝 a)
have mpr : ∀ (x : K) (hx : k < ‖x‖), ∃ (a : K), Tendsto u atTop (𝓝 a)
Tactic: obtain ⟨x, hx⟩ := NormedField.exists_lt_norm K k
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (hypothesis)
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‖
⊢ ∃ (a : K), Tendsto u atTop (𝓝 a)
have hu' : CauchySeq (α := K) ((fun (x_1 : K) ↦ x_1 / x) ∘ u)
Tactic: have hu' : CauchySeq ((· / x) ∘ u) := (uniformContinuous_div_const' x).comp_cauchySeq hu
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
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)
n : ℕ
⊢ Membership.mem (γ := Set K) (closedBall 0 1) (((fun (x_1 : K) ↦ x_1 / x) ∘ u) n)
have simp : ‖u n‖ / ‖x‖ ≤ 1
Tactic: simp only [Function.comp_apply, Metric.mem_closedBall, dist_zero_right, norm_div]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
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)
n : ℕ
⊢ ‖u n‖ / ‖x‖ ≤ 1
have rw : ‖u n‖ ≤ ‖x‖
Tactic: rw [div_le_one (kpos.trans_lt hx)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (hypothesis)
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)
⊢ ∃ (a : K), Tendsto u atTop (𝓝 a)
have hb : ∀ (n : ℕ), Membership.mem (γ := Set K) (closedBall 0 1) (((fun (x_1 : K) ↦ x_1 / x) ∘ u) n)
Tactic: have hb : ∀ n, ((· / x) ∘ u) n ∈ Metric.closedBall 0 1 := by
    intro
    simp only [Function.comp_apply, Metric.mem_closedBall, dist_zero_right, norm_div]
    rw [div_le_one (kpos.trans_lt hx)]
    exact hx.le.trans' (hk (by simp))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
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), Tendsto u atTop (𝓝 a)
have mpr : ∀ (a : K) (ha' : Tendsto ((fun (x_1 : K) ↦ x_1 / x) ∘ u) atTop (𝓝 a)), ∃ (a : K), Tendsto u atTop (𝓝 a)
Tactic: obtain ⟨a, -, ha'⟩ := cauchySeq_tendsto_of_isComplete h hb hu'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
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)
have mpr : ∀ (x_1 : ℕ), ((fun (x_2 : K) ↦ x_2 * x) ∘ (fun (x_2 : K) ↦ x_2 / x) ∘ u) x_1 = u x_1
Tactic: refine ⟨a * x, (((continuous_mul_const x).tendsto a).comp ha').congr ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
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
have contrapose! : ∀ (hx : x = 0), ‖x‖ ≤ k
Tactic: contrapose! hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (hypothesis)
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_1 : ℕ), ((fun (x_2 : K) ↦ x_2 * x) ∘ (fun (x_2 : K) ↦ x_2 / x) ∘ u) x_1 = u x_1
have hx' : x ≠ 0
Tactic: have hx' : x ≠ 0 := by
    contrapose! hx
    simp [hx, kpos]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.ProperSpace (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : WeaklyLocallyCompactSpace 𝕜
⊢ ProperSpace 𝕜
have rcases : ∀ (r : ℝ) (rpos : 0 < r) (hr : IsCompact.{u_1} (X := 𝕜) (closedBall 0 r)), ProperSpace 𝕜
Tactic: rcases exists_isCompact_closedBall (0 : 𝕜) with ⟨r, rpos, hr⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.ProperSpace (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact.{u_1} (X := 𝕜) (closedBall 0 r)
⊢ ProperSpace 𝕜
have rcases : ∀ (c : 𝕜) (hc : 1 < ‖c‖), ProperSpace 𝕜
Tactic: rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.ProperSpace (hypothesis)
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))
have this : c ^ n ≠ 0
Tactic: have : c ^ n ≠ 0 := pow_ne_zero _ <| fun h ↦ by simp [h, zero_le_one.not_gt] at hc
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.ProperSpace (goal)
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.{u_1} (X := 𝕜) (closedBall 0 (‖c‖ ^ n * r))
have h : closedBall 0 (‖c‖ ^ n * r) = HSMul.hSMul (β := Set 𝕜) (c ^ n) (closedBall 0 r)
Tactic: convert! hr.smul (c ^ n)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.ProperSpace (goal)
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
⊢ closedBall 0 (‖c‖ ^ n * r) = HSMul.hSMul (β := Set 𝕜) (c ^ n) (closedBall 0 r)
have h : ∀ (x : 𝕜),
  Membership.mem (γ := Set 𝕜) (closedBall 0 (‖c‖ ^ n * r)) x ↔ x ∈ HSMul.hSMul (β := Set 𝕜) (c ^ n) (closedBall 0 r)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.ProperSpace (hypothesis)
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‖
⊢ ProperSpace 𝕜
have hC : ∀ (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)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.ProperSpace (hypothesis)
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))
⊢ ProperSpace 𝕜
have hTop : 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)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x + 1‖ ≤ max ‖x‖ 1
⊢ IsUltrametricDist R
have refine : ∀ (x y : R), ‖x + y‖ ≤ max ‖x‖ ‖y‖
Tactic: refine isUltrametricDist_of_forall_norm_add_le_max_norm (fun x y ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x + 1‖ ≤ max ‖x‖ 1
x y : R
⊢ ‖x + y‖ ≤ max ‖x‖ ‖y‖
have inl : ‖x + 0‖ ≤ max ‖x‖ (norm.{u_1} (E := R) 0)
Tactic: rcases eq_or_ne y 0 with rfl | hy
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
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)
⊢ ‖x + y‖ ≤ max ‖x‖ ‖y‖
have inr : ∀ (hy : y ≠ 0), ‖x + y‖ ≤ max ‖x‖ ‖y‖
Tactic: rcases eq_or_ne y 0 with rfl | hy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (hypothesis)
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x + 1‖ ≤ max ‖x‖ 1
x y : R
hy : y ≠ 0
⊢ ‖x + y‖ ≤ max ‖x‖ ‖y‖
have p : 0 < ‖y‖
Tactic: have p : 0 < ‖y‖ := norm_pos_iff.mpr hy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
⊢ IsUltrametricDist R
have refine : ∀ (x : R), ‖x + 1‖ ≤ max ‖x‖ 1
Tactic: refine isUltrametricDist_of_forall_norm_add_one_le_max_norm_one fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
⊢ ‖x + 1‖ ≤ max ‖x‖ 1
have inl : ∀ (H : ‖x‖ ≤ 1), ‖x + 1‖ ≤ max ‖x‖ 1
Tactic: rcases le_or_gt ‖x‖ 1 with H | H
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
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
⊢ ‖x + 1‖ ≤ max ‖x‖ 1
have inr : ∀ (H : 1 < ‖x‖), ‖x + 1‖ ≤ max ‖x‖ 1
Tactic: rcases le_or_gt ‖x‖ 1 with H | H
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : 1 < ‖x‖
⊢ ‖x + 1‖ ≤ max ‖x‖ 1
have inr : ‖x + 1‖ ≤ ‖x‖
Tactic: suffices ‖x + 1‖ ≤ ‖x‖ from this.trans (le_max_left _ _)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : 1 < ‖x‖
⊢ ‖x + 1‖ ≤ ‖x‖
have inr : ‖1 / x + 1‖ ≤ 1
Tactic: rw [← div_le_one (by positivity), ← norm_div, add_div,
      div_self (by simpa using H.trans' zero_lt_one), add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : 1 < ‖x‖
⊢ ‖1 / x + 1‖ ≤ 1
have inr : ‖1 / x‖ ≤ 1
Tactic: apply h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (hypothesis)
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x - 1‖ ≤ 1
⊢ IsUltrametricDist R
have this : ∀ (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)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
⊢ IsUltrametricDist R
have refine : ∀ (x : R), ‖x + 1‖ ≤ max ‖x‖ 1
Tactic: refine isUltrametricDist_of_forall_norm_add_one_le_max_norm_one fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
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 ‖x‖ 1
have rw : ‖x + 1‖ ≤ max 1 ‖x‖
Tactic: rw [max_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
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‖
have refine : ∀ (a : ℝ) (ha : max 1 ‖x‖ < a), ‖x + 1‖ ≤ a
Tactic: refine le_of_forall_gt_imp_ge_of_dense fun a ha ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (hypothesis)
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
⊢ ‖x + 1‖ ≤ a
have ha' : 1 < a
Tactic: have ha' : 1 < a := (max_lt_iff.mp ha).left
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
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 : ℕ), (↑(m + 1) : ℝ) < (a / max 1 ‖x‖) ^ m
have apply_mod_cast : 1 < a / max 1 ‖x‖
Tactic: apply_mod_cast Real.exists_natCast_add_one_lt_pow_of_one_lt
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
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
⊢ ‖x + 1‖ ≤ a
have obtain : ∀ (m : ℕ) (hm : (↑(m + 1) : ℝ) < (a / max 1 ‖x‖) ^ m), ‖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)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (hypothesis)
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
⊢ ‖x + 1‖ ≤ a
have hm₁ : (m + 1) • max 1 ‖x‖ ^ m < a ^ m
Tactic: rw [div_pow, lt_div_iff₀ (by positivity), ← nsmul_eq_mul] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
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)
have rw : max (HPow.hPow (α := ℝ) 1 m) (‖x‖ ^ m) = max 1 (‖x‖ ^ m)
Tactic: rw [pow_left_monotoneOn.map_max (by simp [zero_le_one]) (norm_nonneg x), one_pow]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
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)
⊢ max 1 ‖x‖ ^ m = max 1 (‖x‖ ^ m)
have rw₁ : 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (hypothesis)
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
⊢ ‖x + 1‖ ≤ a
have hp : 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (hypothesis)
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
have hm₁ : (m + 1) • max 1 (‖x‖ ^ m) < a ^ m
Tactic: rw [hp] at hm
Cleared hypotheses: hm, hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
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
have refine : ∀ (h : m = 0), False
Tactic: refine le_of_pow_le_pow_left₀ (fun h ↦ ?_) (zero_lt_one.trans ha').le ((h _ _).trans hm.le)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (n : ℕ), norm.{u_1} (E := R) (↑n : R) ≤ 1
⊢ IsUltrametricDist R
have refine : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
Tactic: refine isUltrametricDist_of_forall_pow_norm_le_nsmul_pow_max_one_norm (fun x m ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (n : ℕ), norm.{u_1} (E := R) (↑n : R) ≤ 1
x_1 : R
m : ℕ
x : R
n : ℕ
⊢ ‖n • x‖ ≤ ‖x‖
have rw : norm.{u_1} (E := R) (↑n : R) * ‖x‖ ≤ ‖x‖
Tactic: rw [nsmul_eq_mul, norm_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (n : ℕ), norm.{u_1} (E := R) (↑n : R) ≤ 1
x_1 : R
m : ℕ
x : R
n : ℕ
⊢ norm.{u_1} (E := R) (↑n : R) * ‖x‖ ≤ ‖x‖
have inl : ∀ (hx : 0 = ‖x‖), norm.{u_1} (E := R) (↑n : R) * ‖x‖ ≤ ‖x‖
Tactic: rcases (norm_nonneg x).eq_or_lt with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (n : ℕ), norm.{u_1} (E := R) (↑n : R) ≤ 1
x_1 : R
m : ℕ
x : R
n : ℕ
inl : ∀ (hx : 0 = ‖x‖), norm.{u_1} (E := R) (↑n : R) * ‖x‖ ≤ ‖x‖
⊢ norm.{u_1} (E := R) (↑n : R) * ‖x‖ ≤ ‖x‖
have inr : ∀ (hx : 0 < ‖x‖), norm.{u_1} (E := R) (↑n : R) * ‖x‖ ≤ ‖x‖
Tactic: rcases (norm_nonneg x).eq_or_lt with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (hypothesis)
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (n : ℕ), norm.{u_1} (E := R) (↑n : R) ≤ 1
x : R
m : ℕ
⊢ ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
have h₁ : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
Tactic: replace h (x : R) (n : ℕ) : ‖n • x‖ ≤ ‖x‖ := by
    rw [nsmul_eq_mul, norm_mul]
    rcases (norm_nonneg x).eq_or_lt with hx | hx
    · simp only [← hx, mul_zero, le_refl]
    · simpa only [mul_le_iff_le_one_left hx] using h _
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
⊢ ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
have transitivity : ‖x + 1‖ ^ m ≤ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k
Tactic: transitivity ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
transitivity : ‖x + 1‖ ^ m ≤ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k
⊢ ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
have transitivity₁ : ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k ≤ (m + 1) • max 1 (‖x‖ ^ m)
Tactic: transitivity ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
Goal:
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) • max 1 (‖x‖ ^ m)
have rw : LE.le (α := ℝ) (∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k) (∑ _x ∈ Finset.range (m + 1), max 1 (‖x‖ ^ m))
Tactic: rw [← Finset.card_range (m + 1), ← Finset.sum_const, Finset.card_range]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
⊢ LE.le (α := ℝ) (∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k) (∑ _x ∈ Finset.range (m + 1), max 1 (‖x‖ ^ m))
have inl : ∀ (hm : max 1 (‖x‖ ^ m) = 1) (hx : ‖x‖ ^ m ≤ 1),
  LE.le (α := ℝ) (∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k) (∑ _x ∈ Finset.range (m + 1), max 1 (‖x‖ ^ m))
Tactic: rcases max_cases 1 (‖x‖ ^ m) with (⟨hm, hx⟩ | ⟨hm, hx⟩)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
inl :
  ∀ (hm : max 1 (‖x‖ ^ m) = 1) (hx : ‖x‖ ^ m ≤ 1),
    LE.le (α := ℝ) (∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k) (∑ _x ∈ Finset.range (m + 1), max 1 (‖x‖ ^ m))
⊢ LE.le (α := ℝ) (∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k) (∑ _x ∈ Finset.range (m + 1), max 1 (‖x‖ ^ m))
have inr : ∀ (hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m) (hx : 1 < ‖x‖ ^ m),
  LE.le (α := ℝ) (∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k) (∑ _x ∈ Finset.range (m + 1), max 1 (‖x‖ ^ m))
Tactic: rcases max_cases 1 (‖x‖ ^ m) with (⟨hm, hx⟩ | ⟨hm, hx⟩)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = 1
hx : ‖x‖ ^ m ≤ 1
⊢ LE.le (α := ℝ) (∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k) (∑ _x ∈ Finset.range (m + 1), max 1 (‖x‖ ^ m))
have inl : LE.le (α := ℝ) (∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k) (∑ _x ∈ Finset.range (m + 1), 1)
Tactic: rw [hm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
⊢ LE.le (α := ℝ) (∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k) (∑ _x ∈ Finset.range (m + 1), max 1 (‖x‖ ^ m))
have inr : LE.le (α := ℝ) (∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k) (∑ _x ∈ Finset.range (m + 1), ‖x‖ ^ m)
Tactic: rw [hm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = 1
hx : ‖x‖ ^ m ≤ 1
⊢ LE.le (α := ℝ) (∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k) (∑ _x ∈ Finset.range (m + 1), 1)
have inl : ∀ (i : ℕ) (hi : i ∈ Finset.range (m + 1)), ‖x‖ ^ i ≤ 1
Tactic: gcongr with i hi
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
⊢ LE.le (α := ℝ) (∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k) (∑ _x ∈ Finset.range (m + 1), ‖x‖ ^ m)
have inr : ∀ (i : ℕ) (hi : i ∈ Finset.range (m + 1)), 1 ≤ ‖x‖
Tactic: gcongr with i hi