awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (hypothesis)
Goal:
f : ℕ → ℝ
hf : Tendsto f atTop atBot
⊢ (ofSeq f).InfiniteNeg
have hf₁ : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) atBot
Tactic: replace hf := hf.mono_left Nat.hyperfilter_le_atTop
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
f : ℕ → ℝ
hf : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) atBot
⊢ (ofSeq f).InfiniteNeg
have rw : ofSeq f < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk (ofSeq f)) 0
Tactic: rw [infiniteNeg_iff]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
r : ℝ
⊢ ¬(↑r : ℝ*).Infinite
have rw : ∃ (r_1 : ℝ) (s : ℝ), (↑r_1 : ℝ*) < (↑r : ℝ*) ∧ (↑r : ℝ*) < (↑s : ℝ*)
Tactic: rw [not_infinite_iff_exist_lt_gt]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
⊢ (-x).st = -x.st
have pos : ∀ (h : x.Infinite), (-x).st = -x.st
Tactic: by_cases h : Infinite x
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
pos : ∀ (h : x.Infinite), (-x).st = -x.st
⊢ (-x).st = -x.st
have neg : ∀ (h : ¬x.Infinite), (-x).st = -x.st
Tactic: by_cases h : Infinite x
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
h : x.Infinite
⊢ (-x).st = -x.st
have pos : (-x).st = -0
Tactic: rw [h.st_eq, (infinite_neg.2 h).st_eq, neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
h : x.Infinite
pos : (-x).st = -0
⊢ (-x).st = -x.st
have pos₁ : Eq (α := ℝ) 0 (-0)
Tactic: rw [h.st_eq, (infinite_neg.2 h).st_eq, neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
h : x.Infinite
pos : (-x).st = -0
pos₁ : Eq (α := ℝ) 0 (-0)
⊢ (-x).st = -x.st
have pos₂ : Eq (α := ℝ) 0 0
Tactic: rw [h.st_eq, (infinite_neg.2 h).st_eq, neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
⊢ (-x).st = -x.st
have pos : ∀ (h : x.Infinite), (-x).st = -x.st
Tactic: classical
  by_cases h : Infinite x
  · rw [h.st_eq, (infinite_neg.2 h).st_eq, neg_zero]
  · exact (isSt_st' (not_infinite_neg h)).unique (isSt_st' h).neg
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
pos : ∀ (h : x.Infinite), (-x).st = -x.st
⊢ (-x).st = -x.st
have neg : ∀ (h : ¬x.Infinite), (-x).st = -x.st
Tactic: classical
  by_cases h : Infinite x
  · rw [h.st_eq, (infinite_neg.2 h).st_eq, neg_zero]
  · exact (isSt_st' (not_infinite_neg h)).unique (isSt_st' h).neg
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
⊢ x.InfinitePos ↔ x⁻¹.Infinitesimal ∧ 0 < x⁻¹
have rw : 0 < x ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0 ↔
  LT.lt (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x⁻¹) ∧ 0 < x⁻¹
Tactic: rw [infinitePos_iff, infinitesimal_iff]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
⊢ x.InfiniteNeg ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
have rw : (-x).InfinitePos ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
Tactic: rw [← infinitePos_neg, infinitePos_iff_infinitesimal_inv_pos, inv_neg, neg_pos, infinitesimal_neg]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
rw : (-x).InfinitePos ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
⊢ x.InfiniteNeg ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
have rw₁ : (-x)⁻¹.Infinitesimal ∧ 0 < (-x)⁻¹ ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
Tactic: rw [← infinitePos_neg, infinitePos_iff_infinitesimal_inv_pos, inv_neg, neg_pos, infinitesimal_neg]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
rw : (-x).InfinitePos ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
rw₁ : (-x)⁻¹.Infinitesimal ∧ 0 < (-x)⁻¹ ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
⊢ x.InfiniteNeg ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
have rw₂ : (-x⁻¹).Infinitesimal ∧ 0 < -x⁻¹ ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
Tactic: rw [← infinitePos_neg, infinitePos_iff_infinitesimal_inv_pos, inv_neg, neg_pos, infinitesimal_neg]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
rw : (-x).InfinitePos ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
rw₁ : (-x)⁻¹.Infinitesimal ∧ 0 < (-x)⁻¹ ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
rw₂ : (-x⁻¹).Infinitesimal ∧ 0 < -x⁻¹ ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
⊢ x.InfiniteNeg ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
have rw₃ : (-x⁻¹).Infinitesimal ∧ x⁻¹ < 0 ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
Tactic: rw [← infinitePos_neg, infinitePos_iff_infinitesimal_inv_pos, inv_neg, neg_pos, infinitesimal_neg]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
rw : (-x).InfinitePos ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
rw₁ : (-x)⁻¹.Infinitesimal ∧ 0 < (-x)⁻¹ ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
rw₂ : (-x⁻¹).Infinitesimal ∧ 0 < -x⁻¹ ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
rw₃ : (-x⁻¹).Infinitesimal ∧ x⁻¹ < 0 ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
⊢ x.InfiniteNeg ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
have rw₄ : x⁻¹.Infinitesimal ∧ x⁻¹ < 0 ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
Tactic: rw [← infinitePos_neg, infinitePos_iff_infinitesimal_inv_pos, inv_neg, neg_pos, infinitesimal_neg]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
h0 : x ≠ 0
hi : x⁻¹.Infinitesimal
⊢ x.Infinite
have inl : ∀ (hn : x < 0), x.Infinite
Tactic: rcases lt_or_gt_of_ne h0 with hn | hp
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
h0 : x ≠ 0
hi : x⁻¹.Infinitesimal
inl : ∀ (hn : x < 0), x.Infinite
⊢ x.Infinite
have inr : ∀ (hp : 0 < x), x.Infinite
Tactic: rcases lt_or_gt_of_ne h0 with hn | hp
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
⊢ x⁻¹⁻¹.Infinitesimal ∧ 0 < x⁻¹⁻¹ ↔ x.Infinitesimal ∧ 0 < x
have rw : x.Infinitesimal ∧ 0 < x ↔ x.Infinitesimal ∧ 0 < x
Tactic: rw [inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
⊢ x⁻¹⁻¹.Infinitesimal ∧ x⁻¹⁻¹ < 0 ↔ x.Infinitesimal ∧ x < 0
have rw : x.Infinitesimal ∧ x < 0 ↔ x.Infinitesimal ∧ x < 0
Tactic: rw [inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
h : x ≠ 0
⊢ x.Infinitesimal ↔ x⁻¹⁻¹.Infinitesimal
have rw : x.Infinitesimal ↔ x.Infinitesimal
Tactic: rw [inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (hypothesis)
Goal:
x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
⊢ (↑r : ℝ*) < x * y
have hy₁' : ∃ (x : ℝ), ¬(0 < x → -(↑x : ℝ*) < y ∧ y < (↑x : ℝ*))
Tactic: have hy₁' := not_forall.mp (mt infinitesimal_def.2 hy₁)
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ (x : ℝ), ¬(0 < x → -(↑x : ℝ*) < y ∧ y < (↑x : ℝ*))
⊢ (↑r : ℝ*) < x * y
have let : ∀ (r₁ : ℝ) (hy₁'' : ¬(0 < r₁ → -(↑r₁ : ℝ*) < y ∧ y < (↑r₁ : ℝ*))), (↑r : ℝ*) < x * y
Tactic: let ⟨r₁, hy₁''⟩ := hy₁'
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ (x : ℝ), ¬(0 < x → -(↑x : ℝ*) < y ∧ y < (↑x : ℝ*))
r₁ : ℝ
hy₁'' : ¬(0 < r₁ → -(↑r₁ : ℝ*) < y ∧ y < (↑r₁ : ℝ*))
⊢ 0 < r₁ ∧ (↑r₁ : ℝ*) ≤ y
have rwa : ∀ (hy₁'' : 0 < r₁ ∧ ¬(-(↑r₁ : ℝ*) < y ∧ y < (↑r₁ : ℝ*))), 0 < r₁ ∧ (↑r₁ : ℝ*) ≤ y
Tactic: rwa [Classical.not_imp, ← abs_lt, not_lt, abs_of_pos hy₂] at hy₁''
Cleared hypotheses: hy₁''
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ (x : ℝ), ¬(0 < x → -(↑x : ℝ*) < y ∧ y < (↑x : ℝ*))
r₁ : ℝ
hy₁'' : ¬(0 < r₁ → -(↑r₁ : ℝ*) < y ∧ y < (↑r₁ : ℝ*))
rwa : ∀ (hy₁'' : 0 < r₁ ∧ ¬(-(↑r₁ : ℝ*) < y ∧ y < (↑r₁ : ℝ*))), 0 < r₁ ∧ (↑r₁ : ℝ*) ≤ y
⊢ 0 < r₁ ∧ (↑r₁ : ℝ*) ≤ y
have rwa₁ : ∀ (hy₁'' : 0 < r₁ ∧ ¬|y| < (↑r₁ : ℝ*)), 0 < r₁ ∧ (↑r₁ : ℝ*) ≤ y
Tactic: rwa [Classical.not_imp, ← abs_lt, not_lt, abs_of_pos hy₂] at hy₁''
Cleared hypotheses: hy₁''
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ (x : ℝ), ¬(0 < x → -(↑x : ℝ*) < y ∧ y < (↑x : ℝ*))
r₁ : ℝ
hy₁'' : ¬(0 < r₁ → -(↑r₁ : ℝ*) < y ∧ y < (↑r₁ : ℝ*))
rwa : ∀ (hy₁'' : 0 < r₁ ∧ ¬(-(↑r₁ : ℝ*) < y ∧ y < (↑r₁ : ℝ*))), 0 < r₁ ∧ (↑r₁ : ℝ*) ≤ y
rwa₁ : ∀ (hy₁'' : 0 < r₁ ∧ ¬|y| < (↑r₁ : ℝ*)), 0 < r₁ ∧ (↑r₁ : ℝ*) ≤ y
⊢ 0 < r₁ ∧ (↑r₁ : ℝ*) ≤ y
have rwa₂ : ∀ (hy₁'' : 0 < r₁ ∧ (↑r₁ : ℝ*) ≤ |y|), 0 < r₁ ∧ (↑r₁ : ℝ*) ≤ y
Tactic: rwa [Classical.not_imp, ← abs_lt, not_lt, abs_of_pos hy₂] at hy₁''
Cleared hypotheses: hy₁''
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ (x : ℝ), ¬(0 < x → -(↑x : ℝ*) < y ∧ y < (↑x : ℝ*))
r₁ : ℝ
hy₁'' : ¬(0 < r₁ → -(↑r₁ : ℝ*) < y ∧ y < (↑r₁ : ℝ*))
rwa : ∀ (hy₁'' : 0 < r₁ ∧ ¬(-(↑r₁ : ℝ*) < y ∧ y < (↑r₁ : ℝ*))), 0 < r₁ ∧ (↑r₁ : ℝ*) ≤ y
rwa₁ : ∀ (hy₁'' : 0 < r₁ ∧ ¬|y| < (↑r₁ : ℝ*)), 0 < r₁ ∧ (↑r₁ : ℝ*) ≤ y
rwa₂ : ∀ (hy₁'' : 0 < r₁ ∧ (↑r₁ : ℝ*) ≤ |y|), 0 < r₁ ∧ (↑r₁ : ℝ*) ≤ y
⊢ 0 < r₁ ∧ (↑r₁ : ℝ*) ≤ y
have rwa₃ : ∀ (hy₁'' : 0 < r₁ ∧ (↑r₁ : ℝ*) ≤ y), 0 < r₁ ∧ (↑r₁ : ℝ*) ≤ y
Tactic: rwa [Classical.not_imp, ← abs_lt, not_lt, abs_of_pos hy₂] at hy₁''
Cleared hypotheses: hy₁''
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (hypothesis)
Goal:
x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ (x : ℝ), ¬(0 < x → -(↑x : ℝ*) < y ∧ y < (↑x : ℝ*))
r₁ : ℝ
hy₁'' : ¬(0 < r₁ → -(↑r₁ : ℝ*) < y ∧ y < (↑r₁ : ℝ*))
⊢ (↑r : ℝ*) < x * y
have hyr : 0 < r₁ ∧ (↑r₁ : ℝ*) ≤ y
Tactic: have hyr : 0 < r₁ ∧ ↑r₁ ≤ y := by
    rwa [Classical.not_imp, ← abs_lt, not_lt, abs_of_pos hy₂] at hy₁''
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ (x : ℝ), ¬(0 < x → -(↑x : ℝ*) < y ∧ y < (↑x : ℝ*))
r₁ : ℝ
hy₁'' : ¬(0 < r₁ → -(↑r₁ : ℝ*) < y ∧ y < (↑r₁ : ℝ*))
hyr : 0 < r₁ ∧ (↑r₁ : ℝ*) ≤ y
⊢ (↑r : ℝ*) < x * y
have rw : (↑(r / r₁) : ℝ*) * (↑r₁ : ℝ*) < x * y
Tactic: rw [← div_mul_cancel₀ r (ne_of_gt hyr.1), coe_mul]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x y : ℝ*
⊢ x.InfiniteNeg → ¬y.Infinitesimal → y < 0 → (x * y).InfinitePos
have rw : (-x).InfinitePos → ¬(-y).Infinitesimal → 0 < -y → (-x * -y).InfinitePos
Tactic: rw [← infinitePos_neg, ← neg_pos, ← neg_mul_neg, ← infinitesimal_neg]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x y : ℝ*
⊢ x.InfinitePos → ¬y.Infinitesimal → y < 0 → (x * y).InfiniteNeg
have rw : x.InfinitePos → ¬(-y).Infinitesimal → 0 < -y → (x * -y).InfinitePos
Tactic: rw [← infinitePos_neg, ← neg_pos, neg_mul_eq_mul_neg, ← infinitesimal_neg]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x y : ℝ*
⊢ x.InfiniteNeg → ¬y.Infinitesimal → 0 < y → (x * y).InfiniteNeg
have rw : (-x).InfinitePos → ¬y.Infinitesimal → 0 < y → (-x * y).InfinitePos
Tactic: rw [← infinitePos_neg, ← infinitePos_neg, neg_mul_eq_neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x y : ℝ*
hx : ¬x.Infinitesimal
hp : 0 < x
hy : y.InfiniteNeg
⊢ (x * y).InfiniteNeg
have rw : (y * x).InfiniteNeg
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x y : ℝ*
hx : ¬x.Infinitesimal
hy : y.Infinite
⊢ (x * y).Infinite
have rw : (y * x).Infinite
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
digits : ℕ → Fin b
n : ℕ
⊢ ofDigitsTerm digits n ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1))⁻¹
have obtain : ∀ (c : ℕ) {digits : ℕ → Fin (c + 1)},
  ofDigitsTerm digits n ≤ HSub.hSub (α := ℝ) (↑(c + 1) : ℝ) 1 * (HPow.hPow (α := ℝ) (↑(c + 1) : ℝ) (n + 1))⁻¹
Tactic: obtain ⟨c, rfl⟩ := Nat.exists_add_one_eq.mpr (b_pos digits)
Cleared hypotheses: b, digits
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
n c : ℕ
digits : ℕ → Fin (c + 1)
⊢ (↑(↑(digits n) : ℕ) : ℝ) * (HPow.hPow (α := ℝ) (↑(c + 1) : ℝ) (n + 1))⁻¹ ≤
    HSub.hSub (α := ℝ) (↑(c + 1) : ℝ) 1 * (HPow.hPow (α := ℝ) (↑(c + 1) : ℝ) (n + 1))⁻¹
have hbc : (↑(↑(digits n) : ℕ) : ℝ) ≤ HSub.hSub (α := ℝ) (↑(c + 1) : ℝ) 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
n c : ℕ
digits : ℕ → Fin (c + 1)
⊢ (↑(↑(digits n) : ℕ) : ℝ) ≤ HSub.hSub (α := ℝ) (↑(c + 1) : ℝ) 1
have hbc : (↑(digits n) : ℕ) ≤ c
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
digits : ℕ → Fin b
⊢ Summable (ofDigitsTerm digits)
have refine : Summable (α := ℝ) fun (x : ℕ) ↦ HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (x + 1))⁻¹
Tactic: refine Summable.of_nonneg_of_le (fun _ ↦ ofDigitsTerm_nonneg) (fun _ ↦ ofDigitsTerm_le) ?_
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
digits : ℕ → Fin b
⊢ Summable (α := ℝ) fun (x : ℕ) ↦ HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (x + 1))⁻¹
have inl : ∀ {digits : ℕ → Fin 1},
  Summable (α := ℝ) fun (x : ℕ) ↦ HSub.hSub (α := ℝ) (↑1 : ℝ) 1 * (HPow.hPow (α := ℝ) (↑1 : ℝ) (x + 1))⁻¹
Tactic: obtain rfl | hb := (Nat.one_le_of_lt (b_pos digits)).eq_or_lt
Cleared hypotheses: b, digits
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
digits : ℕ → Fin b
inl :
  ∀ {digits : ℕ → Fin 1},
    Summable (α := ℝ) fun (x : ℕ) ↦ HSub.hSub (α := ℝ) (↑1 : ℝ) 1 * (HPow.hPow (α := ℝ) (↑1 : ℝ) (x + 1))⁻¹
⊢ Summable (α := ℝ) fun (x : ℕ) ↦ HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (x + 1))⁻¹
have inr : ∀ (hb : 1 < b), Summable (α := ℝ) fun (x : ℕ) ↦ HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (x + 1))⁻¹
Tactic: obtain rfl | hb := (Nat.one_le_of_lt (b_pos digits)).eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
digits : ℕ → Fin b
hb : 1 < b
⊢ Summable (α := ℝ) fun (x : ℕ) ↦ HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (x + 1))⁻¹
have inr : Summable (α := ℝ) fun (x : ℕ) ↦ HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (↑b : ℝ)⁻¹ * HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ x
Tactic: simp_rw [pow_succ', mul_inv, ← inv_pow, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
digits : ℕ → Fin b
hb : 1 < b
⊢ Summable (α := ℝ) fun (x : ℕ) ↦ HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (↑b : ℝ)⁻¹ * HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ x
have inr : LT.lt (α := ℝ) (↑b : ℝ)⁻¹ 1
Tactic: refine Summable.mul_left _ (summable_geometric_of_lt_one (by positivity) ?_)
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
digits : ℕ → Fin b
⊢ ofDigits digits ≤ 1
have inl : ∀ (digits : ℕ → Fin 1), ofDigits digits ≤ 1
Tactic: obtain rfl | hb := (Nat.one_le_of_lt (b_pos digits)).eq_or_lt
Cleared hypotheses: b, digits
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
digits : ℕ → Fin b
inl : ∀ (digits : ℕ → Fin 1), ofDigits digits ≤ 1
⊢ ofDigits digits ≤ 1
have inr : ∀ (hb : 1 < b), ofDigits digits ≤ 1
Tactic: obtain rfl | hb := (Nat.one_le_of_lt (b_pos digits)).eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (hypothesis)
Goal:
b : ℕ
digits : ℕ → Fin b
hb : 1 < b
⊢ ofDigits digits ≤ 1
have hb₁ : LT.lt (α := ℝ) 1 (↑b : ℝ)
Tactic: rify at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
digits : ℕ → Fin b
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ ofDigits digits ≤ 1
have h : Eq (α := ℝ) 1 (∑' (n : ℕ), HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1))⁻¹)
Tactic: convert! Summable.tsum_mono summable_ofDigitsTerm _ (fun _ ↦ ofDigitsTerm_le)
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
digits : ℕ → Fin b
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
h : Eq (α := ℝ) 1 (∑' (n : ℕ), HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1))⁻¹)
⊢ ofDigits digits ≤ 1
have inr : Summable (α := ℝ) fun (x : ℕ) ↦ HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (x + 1))⁻¹
Tactic: convert! Summable.tsum_mono summable_ofDigitsTerm _ (fun _ ↦ ofDigitsTerm_le)
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
digits : ℕ → Fin b
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ Eq (α := ℝ) 1 (∑' (n : ℕ), HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1))⁻¹)
have h : Eq (α := ℝ) 1 (∑' (n : ℕ), HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (↑b : ℝ)⁻¹ * HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ n)
Tactic: simp_rw [pow_succ', mul_inv, ← inv_pow, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
digits : ℕ → Fin b
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ Eq (α := ℝ) 1 (∑' (n : ℕ), HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (↑b : ℝ)⁻¹ * HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ n)
have h : 1 = HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (↑b : ℝ)⁻¹ * (HSub.hSub (α := ℝ) 1 (↑b : ℝ)⁻¹)⁻¹
Tactic: rw [tsum_mul_left, tsum_geometric_of_lt_one (by positivity) (by simp [inv_lt_one_iff₀, hb])]
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (hypothesis)
Goal:
b : ℕ
digits : ℕ → Fin b
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ 1 = HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (↑b : ℝ)⁻¹ * (HSub.hSub (α := ℝ) 1 (↑b : ℝ)⁻¹)⁻¹
have this : 0 < HSub.hSub (α := ℝ) (↑b : ℝ) 1
Tactic: have := sub_pos.mpr hb
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
digits : ℕ → Fin b
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ Summable (α := ℝ) fun (x : ℕ) ↦ HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (x + 1))⁻¹
have inr : Summable (α := ℝ) fun (x : ℕ) ↦ HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (↑b : ℝ)⁻¹ * HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ x
Tactic: simp_rw [pow_succ', mul_inv, ← inv_pow, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
digits : ℕ → Fin b
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ Summable (α := ℝ) fun (x : ℕ) ↦ HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (↑b : ℝ)⁻¹ * HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ x
have inr : LT.lt (α := ℝ) (↑b : ℝ)⁻¹ 1
Tactic: refine Summable.mul_left _ (summable_geometric_of_lt_one (by positivity) ?_)
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
a : ℕ → Fin b
n : ℕ
⊢ ∑' (n : ℕ), ofDigitsTerm a n =
    ∑ n ∈ Finset.range n, ofDigitsTerm a n +
      (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹ * ∑' (n_1 : ℕ), ofDigitsTerm (b := b) (fun (i : ℕ) ↦ a (i + n)) n_1
have rw : HAdd.hAdd (α := ℝ) (∑ i ∈ Finset.range n, ofDigitsTerm a i) (∑' (i : ℕ), ofDigitsTerm a (i + n)) =
  HAdd.hAdd (α := ℝ) (∑ n ∈ Finset.range n, ofDigitsTerm a n)
    (∑' (i : ℕ), (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹ * ofDigitsTerm (b := b) (fun (i : ℕ) ↦ a (i + n)) i)
Tactic: rw [← Summable.sum_add_tsum_nat_add n summable_ofDigitsTerm,
    ← Summable.tsum_mul_left _ summable_ofDigitsTerm]
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
a : ℕ → Fin b
n : ℕ
⊢ HAdd.hAdd (α := ℝ) (∑ i ∈ Finset.range n, ofDigitsTerm a i) (∑' (i : ℕ), ofDigitsTerm a (i + n)) =
    HAdd.hAdd (α := ℝ) (∑ n ∈ Finset.range n, ofDigitsTerm a n)
      (∑' (i : ℕ), (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹ * ofDigitsTerm (b := b) (fun (i : ℕ) ↦ a (i + n)) i)
have e_a : Eq (α := ℕ → ℝ) (fun (i : ℕ) ↦ ofDigitsTerm a (i + n)) fun (i : ℕ) ↦
  (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹ * ofDigitsTerm (b := b) (fun (i : ℕ) ↦ a (i + n)) i
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
a : ℕ → Fin b
n : ℕ
⊢ Eq (α := ℕ → ℝ) (fun (i : ℕ) ↦ ofDigitsTerm a (i + n)) fun (i : ℕ) ↦
    (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹ * ofDigitsTerm (b := b) (fun (i : ℕ) ↦ a (i + n)) i
have e_a : ∀ (i : ℕ),
  ofDigitsTerm a (i + n) = (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹ * ofDigitsTerm (b := b) (fun (i : ℕ) ↦ a (i + n)) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
a : ℕ → Fin b
n i : ℕ
⊢ ofDigitsTerm a (i + n) = (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹ * ofDigitsTerm (b := b) (fun (i : ℕ) ↦ a (i + n)) i
have e_a : (↑(↑(a (i + n)) : ℕ) : ℝ) * (HPow.hPow (α := ℝ) (↑b : ℝ) (i + n + 1))⁻¹ =
  (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹ * ((↑(↑(a (i + n)) : ℕ) : ℝ) * (HPow.hPow (α := ℝ) (↑b : ℝ) (i + 1))⁻¹)
Tactic: simp only [ofDigitsTerm]
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
x y : ℕ → Fin b
n : ℕ
hxy : ∀ i < n, x i = y i
⊢ |ofDigits x - ofDigits y| ≤ (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹
have rw : |(∑ i ∈ Finset.range n, ofDigitsTerm x i +
        (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹ * ofDigits (b := b) fun (i : ℕ) ↦ x (i + n)) -
      (∑ i ∈ Finset.range n, ofDigitsTerm y i +
        (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹ * ofDigits (b := b) fun (i : ℕ) ↦ y (i + n))| ≤
  (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹
Tactic: rw [ofDigits_eq_sum_add_ofDigits x n, ofDigits_eq_sum_add_ofDigits y n]
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (hypothesis)
Goal:
b : ℕ
x y : ℕ → Fin b
n : ℕ
hxy : ∀ i < n, x i = y i
⊢ |(∑ i ∈ Finset.range n, ofDigitsTerm x i +
          (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹ * ofDigits (b := b) fun (i : ℕ) ↦ x (i + n)) -
        (∑ i ∈ Finset.range n, ofDigitsTerm y i +
          (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹ * ofDigits (b := b) fun (i : ℕ) ↦ y (i + n))| ≤
    (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹
have this : Eq (α := ℝ) (∑ i ∈ Finset.range n, ofDigitsTerm x i) (∑ i ∈ Finset.range n, ofDigitsTerm y i)
Tactic: have : ∑ i ∈ Finset.range n, ofDigitsTerm x i = ∑ i ∈ Finset.range n, ofDigitsTerm y i :=
    Finset.sum_congr rfl fun i hi ↦ by simp [ofDigitsTerm, hxy i (Finset.mem_range.mp hi)]
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
x y : ℕ → Fin b
n : ℕ
hxy : ∀ i < n, x i = y i
this : Eq (α := ℝ) (∑ i ∈ Finset.range n, ofDigitsTerm x i) (∑ i ∈ Finset.range n, ofDigitsTerm y i)
⊢ |(∑ i ∈ Finset.range n, ofDigitsTerm x i +
          (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹ * ofDigits (b := b) fun (i : ℕ) ↦ x (i + n)) -
        (∑ i ∈ Finset.range n, ofDigitsTerm y i +
          (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹ * ofDigits (b := b) fun (i : ℕ) ↦ y (i + n))| ≤
    (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹
have rw : (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹ *
    |(ofDigits (b := b) fun (i : ℕ) ↦ x (i + n)) - ofDigits (b := b) fun (i : ℕ) ↦ y (i + n)| ≤
  (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹
Tactic: rw [this, add_sub_add_left_eq_sub, ← mul_sub, abs_mul, abs_of_nonneg (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
x y : ℕ → Fin b
n : ℕ
hxy : ∀ i < n, x i = y i
this : Eq (α := ℝ) (∑ i ∈ Finset.range n, ofDigitsTerm x i) (∑ i ∈ Finset.range n, ofDigitsTerm y i)
⊢ (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹ *
      |(ofDigits (b := b) fun (i : ℕ) ↦ x (i + n)) - ofDigits (b := b) fun (i : ℕ) ↦ y (i + n)| ≤
    (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹
have apply : |(ofDigits (b := b) fun (i : ℕ) ↦ x (i + n)) - ofDigits (b := b) fun (i : ℕ) ↦ y (i + n)| ≤ 1
Tactic: apply mul_le_of_le_one_right (by positivity)
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
x y : ℕ → Fin b
n : ℕ
hxy : ∀ i < n, x i = y i
this : Eq (α := ℝ) (∑ i ∈ Finset.range n, ofDigitsTerm x i) (∑ i ∈ Finset.range n, ofDigitsTerm y i)
⊢ |(ofDigits (b := b) fun (i : ℕ) ↦ x (i + n)) - ofDigits (b := b) fun (i : ℕ) ↦ y (i + n)| ≤ 1
have h : 1 = HSub.hSub (α := ℝ) 1 0
Tactic: convert!
    abs_sub_le_of_le_of_le (ofDigits_nonneg _) (ofDigits_le_one _) (ofDigits_nonneg _)
      (ofDigits_le_one _)
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (hypothesis)
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
n : ℕ
⊢ HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i =
    (↑⌊HPow.hPow (α := ℝ) (↑b : ℝ) n * x⌋₊ : ℝ)
have this : b ≠ 0
Tactic: have := NeZero.ne b
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
this : b ≠ 0
n : ℕ
ih :
  HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i =
    (↑⌊HPow.hPow (α := ℝ) (↑b : ℝ) n * x⌋₊ : ℝ)
⊢ HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1) * ∑ i ∈ Finset.range (n + 1), ofDigitsTerm (x.digits b) i =
    (↑⌊HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1) * x⌋₊ : ℝ)
have succ : HMul.hMul (α := ℝ) (↑b : ℝ) (↑⌊HPow.hPow (α := ℝ) (↑b : ℝ) n * x⌋₊ : ℝ) +
    (↑(↑(Fin.ofNat b ⌊(↑b : ℝ) * (HPow.hPow (α := ℝ) (↑b : ℝ) n * x)⌋₊) : ℕ) : ℝ) =
  (↑⌊(↑b : ℝ) * (HPow.hPow (α := ℝ) (↑b : ℝ) n * x)⌋₊ : ℝ)
Tactic: rw [Finset.sum_range_succ, mul_add, pow_succ', mul_assoc, ih, ofDigitsTerm, digits, ← pow_succ',
      mul_left_comm, mul_inv_cancel₀ (by positivity), mul_one, mul_comm x, pow_succ', mul_assoc]