awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (hypothesis)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
⊢ ‖(1 - t)⁻¹ʳ‖ ≤ (norm.{u_1} (E := R) 1 + 1) * norm (E := ℝ) 1
have ht' : ‖t‖ < 1
Tactic: have ht' : ‖t‖ < 1 := by linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
⊢ ‖(1 - t)⁻¹ʳ‖ ≤ (norm.{u_1} (E := R) 1 + 1) * norm (E := ℝ) 1
have simp : ‖(↑(Units.oneSub t ht')⁻¹ : R)‖ ≤ norm.{u_1} (E := R) 1 + 1
Tactic: simp only [inverse_one_sub t ht', norm_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
⊢ ‖(↑(Units.oneSub t ht')⁻¹ : R)‖ ≤ norm.{u_1} (E := R) 1 + 1
have change : norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) ≤ norm.{u_1} (E := R) 1 + 1
Tactic: change ‖∑' n : ℕ, t ^ n‖ ≤ _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (hypothesis)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
⊢ norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) ≤ norm.{u_1} (E := R) 1 + 1
have this : norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) ≤ norm.{u_1} (E := R) 1 - 1 + (1 - ‖t‖)⁻¹
Tactic: have := tsum_geometric_le_of_norm_lt_one t ht'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this : norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) ≤ norm.{u_1} (E := R) 1 - 1 + (1 - ‖t‖)⁻¹
⊢ 2⁻¹ ≤ 1 - ‖t‖
have linarith : 1 - ‖t‖ < 2⁻¹ → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this : norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) ≤ norm.{u_1} (E := R) 1 - 1 + (1 - ‖t‖)⁻¹
linarith : 1 - ‖t‖ < 2⁻¹ → 2 / 2 = 1
⊢ 2⁻¹ ≤ 1 - ‖t‖
have linarith₁ : 1 - ‖t‖ < 2⁻¹ → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this : norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) ≤ norm.{u_1} (E := R) 1 - 1 + (1 - ‖t‖)⁻¹
linarith : 1 - ‖t‖ < 2⁻¹ → 2 / 2 = 1
linarith₁ : 1 - ‖t‖ < 2⁻¹ → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 2⁻¹ ≤ 1 - ‖t‖
have linarith₂ : 1 - ‖t‖ < 2⁻¹ → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this : norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) ≤ norm.{u_1} (E := R) 1 - 1 + (1 - ‖t‖)⁻¹
linarith : 1 - ‖t‖ < 2⁻¹ → 2 / 2 = 1
linarith₁ : 1 - ‖t‖ < 2⁻¹ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 - ‖t‖ < 2⁻¹ → GT.gt (α := ℝ) 2 0
linarith₃ : 1 - ‖t‖ < 2⁻¹ → 2 / 2 = 1
linarith₄ : 1 - ‖t‖ < 2⁻¹ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : 1 - ‖t‖ < 2⁻¹ → GT.gt (α := ℝ) 2 0
⊢ 2⁻¹ ≤ 1 - ‖t‖
have linarith₆ : 1 - ‖t‖ < 2⁻¹ → 2 * ‖t‖ - HMul.hMul (α := ℝ) 1 1 + (HMul.hMul (α := ℝ) 2 1 - 2 * ‖t‖ - HMul.hMul (α := ℝ) 1 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (hypothesis)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this : norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) ≤ norm.{u_1} (E := R) 1 - 1 + (1 - ‖t‖)⁻¹
⊢ norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) ≤ norm.{u_1} (E := R) 1 + 1
have this₁ : (1 - ‖t‖)⁻¹ ≤ 2
Tactic: have : (1 - ‖t‖)⁻¹ ≤ 2 := inv_le_of_inv_le₀ (by simp) (by linarith)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this_1 : norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) ≤ norm.{u_1} (E := R) 1 - 1 + (1 - ‖t‖)⁻¹
this : (1 - ‖t‖)⁻¹ ≤ 2
⊢ norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) ≤ norm.{u_1} (E := R) 1 + 1
have linarith : norm.{u_1} (E := R) 1 + 1 < norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this_1 : norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) ≤ norm.{u_1} (E := R) 1 - 1 + (1 - ‖t‖)⁻¹
this : (1 - ‖t‖)⁻¹ ≤ 2
linarith : norm.{u_1} (E := R) 1 + 1 < norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) → 2 / 2 = 1
⊢ norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) ≤ norm.{u_1} (E := R) 1 + 1
have linarith₁ : norm.{u_1} (E := R) 1 + 1 < norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this_1 : norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) ≤ norm.{u_1} (E := R) 1 - 1 + (1 - ‖t‖)⁻¹
this : (1 - ‖t‖)⁻¹ ≤ 2
linarith : norm.{u_1} (E := R) 1 + 1 < norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) → 2 / 2 = 1
linarith₁ : norm.{u_1} (E := R) 1 + 1 < norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) ≤ norm.{u_1} (E := R) 1 + 1
have linarith₂ : norm.{u_1} (E := R) 1 + 1 < norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this_1 : norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) ≤ norm.{u_1} (E := R) 1 - 1 + (1 - ‖t‖)⁻¹
this : (1 - ‖t‖)⁻¹ ≤ 2
linarith : norm.{u_1} (E := R) 1 + 1 < norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) → 2 / 2 = 1
linarith₁ : norm.{u_1} (E := R) 1 + 1 < norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : norm.{u_1} (E := R) 1 + 1 < norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) → GT.gt (α := ℝ) 2 0
⊢ norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) ≤ norm.{u_1} (E := R) 1 + 1
have linarith₃ : norm.{u_1} (E := R) 1 + 1 < norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) →
  1 * norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) - (1 * norm.{u_1} (E := R) 1 - HMul.hMul (α := ℝ) 1 1 + 1 * (1 - ‖t‖)⁻¹) +
        (1 * (1 - ‖t‖)⁻¹ - HMul.hMul (α := ℝ) 1 2) +
      (norm.{u_1} (E := R) 1 + 1 - norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n)) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
⊢ IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (t : R) ↦ ((↑x : R) + t)⁻¹ʳ) fun (_t : R) ↦ 1
have refine : IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (x_1 : R) ↦ (1 + (↑x⁻¹ : R) * x_1)⁻¹ʳ * (↑x⁻¹ : R)) fun (_t : R) ↦
  HMul.hMul (α := ℝ) 1 1
Tactic: refine EventuallyEq.trans_isBigO (inverse_add x) (one_mul (1 : ℝ) ▸ ?_)