awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
hi : ¬x.Infinitesimal
hr : x.IsSt 0
⊢ False

Tactic:
hi hr
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
hi : ¬x.Infinitesimal
hr : x.IsSt 0
⊢ False

Tactic:
exact hi hr
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ x⁻¹.st = x.st⁻¹

Tactic:
simp [st_eq]

Premises used: Hyperreal.st_eq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
⊢ ω.InfinitePos

Tactic:
infinitePos_iff_infinitesimal_inv_pos.mpr ⟨infinitesimal_epsilon, epsilon_pos⟩

Premises used: Iff.mpr, Hyperreal.infinitePos_iff_infinitesimal_inv_pos, And.intro, Hyperreal.infinitesimal_epsilon, Hyperreal.epsilon_pos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
⊢ ω.Infinite

Tactic:
(infinite_iff_infinitesimal_inv omega_ne_zero).mpr infinitesimal_epsilon

Premises used: Iff.mpr, Hyperreal.infinite_iff_infinitesimal_inv, Hyperreal.omega_ne_zero, Hyperreal.infinitesimal_epsilon
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
⊢ ∃ (x : ℝ), ¬(0 < x → -(↑x : ℝ*) < y ∧ y < (↑x : ℝ*))

Tactic:
have hy₁' := not_forall.mp (mt infinitesimal_def.2 hy₁)
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ (x : ℝ), ¬(0 < x → -(↑x : ℝ*) < y ∧ y < (↑x : ℝ*))
let : ∀ (r₁ : ℝ) (hy₁'' : ¬(0 < r₁ → -(↑r₁ : ℝ*) < y ∧ y < (↑r₁ : ℝ*))), (↑r : ℝ*) < x * y
⊢ (↑r : ℝ*) < x * y

Tactic:
let ⟨r₁, hy₁''⟩ := hy₁'
-- Module: Mathlib.Analysis.Real.Hyperreal
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
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (hy₁'' : 0 < r₁ ∧ (↑r₁ : ℝ*) ≤ y), 0 < r₁ ∧ (↑r₁ : ℝ*) ≤ y
⊢ 0 < r₁ ∧ (↑r₁ : ℝ*) ≤ y

Tactic:
rwa [Classical.not_imp, ← abs_lt, not_lt, abs_of_pos hy₂] at hy₁''

Premises used: not_lt, Classical.not_imp, abs_lt, abs_of_pos
-- Module: Mathlib.Analysis.Real.Hyperreal
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

Tactic:
have hyr : 0 < r₁ ∧ ↑r₁ ≤ y := by
    rwa [Classical.not_imp, ← abs_lt, not_lt, abs_of_pos hy₂] at hy₁''
-- Module: Mathlib.Analysis.Real.Hyperreal
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
rw : (↑(r / r₁) : ℝ*) * (↑r₁ : ℝ*) < x * y
⊢ (↑r : ℝ*) < x * y

Tactic:
rw [← div_mul_cancel₀ r (ne_of_gt hyr.1), coe_mul]

Premises used: div_mul_cancel₀, ne_of_gt, And.left, Hyperreal.coe_mul
-- Module: Mathlib.Analysis.Real.Hyperreal
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 / r₁) : ℝ*) * (↑r₁ : ℝ*) < x * y

Tactic:
mul_lt_mul (hx (r / r₁)) hyr.2 (coe_lt_coe.2 hyr.1) (le_of_lt (hx 0))

Premises used: Iff.mpr, mul_lt_mul, le_of_lt, HDiv.hDiv, And.right, And.left, OfNat.ofNat, Hyperreal.coe_lt_coe
-- Module: Mathlib.Analysis.Real.Hyperreal
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 / r₁) : ℝ*) * (↑r₁ : ℝ*) < x * y

Tactic:
exact mul_lt_mul (hx (r / r₁)) hyr.2 (coe_lt_coe.2 hyr.1) (le_of_lt (hx 0))

Premises used: Iff.mpr, mul_lt_mul, le_of_lt, HDiv.hDiv, And.right, And.left, OfNat.ofNat, Hyperreal.coe_lt_coe
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
⊢ ¬x.Infinitesimal → 0 < x → y.InfinitePos → (x * y).InfinitePos

Tactic:
fun hx hp hy =>
  mul_comm y x ▸ infinitePos_mul_of_infinitePos_not_infinitesimal_pos hy hx hp

Premises used: Hyperreal.infinitePos_mul_of_infinitePos_not_infinitesimal_pos, Eq.rec, mul_comm
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
rw : (-x).InfinitePos → ¬(-y).Infinitesimal → 0 < -y → (-x * -y).InfinitePos
⊢ x.InfiniteNeg → ¬y.Infinitesimal → y < 0 → (x * y).InfinitePos

Tactic:
rw [← infinitePos_neg, ← neg_pos, ← neg_mul_neg, ← infinitesimal_neg]

Premises used: neg_pos, Hyperreal.infinitePos_neg, neg_mul_neg, Hyperreal.infinitesimal_neg
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
⊢ (-x).InfinitePos → ¬(-y).Infinitesimal → 0 < -y → (-x * -y).InfinitePos

Tactic:
infinitePos_mul_of_infinitePos_not_infinitesimal_pos

Premises used: Hyperreal.infinitePos_mul_of_infinitePos_not_infinitesimal_pos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
⊢ (-x).InfinitePos → ¬(-y).Infinitesimal → 0 < -y → (-x * -y).InfinitePos

Tactic:
exact infinitePos_mul_of_infinitePos_not_infinitesimal_pos

Premises used: Hyperreal.infinitePos_mul_of_infinitePos_not_infinitesimal_pos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
⊢ ¬x.Infinitesimal → x < 0 → y.InfiniteNeg → (x * y).InfinitePos

Tactic:
fun hx hp hy =>
  mul_comm y x ▸ infinitePos_mul_of_infiniteNeg_not_infinitesimal_neg hy hx hp

Premises used: Hyperreal.infinitePos_mul_of_infiniteNeg_not_infinitesimal_neg, Eq.rec, mul_comm
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
rw : x.InfinitePos → ¬(-y).Infinitesimal → 0 < -y → (x * -y).InfinitePos
⊢ x.InfinitePos → ¬y.Infinitesimal → y < 0 → (x * y).InfiniteNeg

Tactic:
rw [← infinitePos_neg, ← neg_pos, neg_mul_eq_mul_neg, ← infinitesimal_neg]

Premises used: neg_pos, Hyperreal.infinitePos_neg, neg_mul_eq_mul_neg, Hyperreal.infinitesimal_neg
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
⊢ x.InfinitePos → ¬(-y).Infinitesimal → 0 < -y → (x * -y).InfinitePos

Tactic:
infinitePos_mul_of_infinitePos_not_infinitesimal_pos

Premises used: Hyperreal.infinitePos_mul_of_infinitePos_not_infinitesimal_pos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
⊢ x.InfinitePos → ¬(-y).Infinitesimal → 0 < -y → (x * -y).InfinitePos

Tactic:
exact infinitePos_mul_of_infinitePos_not_infinitesimal_pos

Premises used: Hyperreal.infinitePos_mul_of_infinitePos_not_infinitesimal_pos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
⊢ ¬x.Infinitesimal → x < 0 → y.InfinitePos → (x * y).InfiniteNeg

Tactic:
fun hx hp hy =>
  mul_comm y x ▸ infiniteNeg_mul_of_infinitePos_not_infinitesimal_neg hy hx hp

Premises used: Eq.rec, mul_comm, Hyperreal.infiniteNeg_mul_of_infinitePos_not_infinitesimal_neg
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
rw : (-x).InfinitePos → ¬y.Infinitesimal → 0 < y → (-x * y).InfinitePos
⊢ x.InfiniteNeg → ¬y.Infinitesimal → 0 < y → (x * y).InfiniteNeg

Tactic:
rw [← infinitePos_neg, ← infinitePos_neg, neg_mul_eq_neg_mul]

Premises used: Hyperreal.infinitePos_neg, neg_mul_eq_neg_mul
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
⊢ (-x).InfinitePos → ¬y.Infinitesimal → 0 < y → (-x * y).InfinitePos

Tactic:
infinitePos_mul_of_infinitePos_not_infinitesimal_pos

Premises used: Hyperreal.infinitePos_mul_of_infinitePos_not_infinitesimal_pos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
⊢ (-x).InfinitePos → ¬y.Infinitesimal → 0 < y → (-x * y).InfinitePos

Tactic:
exact infinitePos_mul_of_infinitePos_not_infinitesimal_pos

Premises used: Hyperreal.infinitePos_mul_of_infinitePos_not_infinitesimal_pos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
hx : ¬x.Infinitesimal
hp : 0 < x
hy : y.InfiniteNeg
rw : (y * x).InfiniteNeg
⊢ (x * y).InfiniteNeg

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
hx : ¬x.Infinitesimal
hp : 0 < x
hy : y.InfiniteNeg
⊢ (y * x).InfiniteNeg

Tactic:
infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos hy hx hp

Premises used: Hyperreal.infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
hx : ¬x.Infinitesimal
hp : 0 < x
hy : y.InfiniteNeg
⊢ (y * x).InfiniteNeg

Tactic:
exact infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos hy hx hp

Premises used: Hyperreal.infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
⊢ x.InfinitePos → y.InfinitePos → (x * y).InfinitePos

Tactic:
fun hx hy =>
  infinitePos_mul_of_infinitePos_not_infinitesimal_pos hx hy.not_infinitesimal (hy 0)

Premises used: Hyperreal.infinitePos_mul_of_infinitePos_not_infinitesimal_pos, Hyperreal.InfinitePos.not_infinitesimal, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
⊢ x.InfiniteNeg → y.InfiniteNeg → (x * y).InfinitePos

Tactic:
fun hx hy =>
  infinitePos_mul_of_infiniteNeg_not_infinitesimal_neg hx hy.not_infinitesimal (hy 0)

Premises used: Hyperreal.InfiniteNeg.not_infinitesimal, Hyperreal.infinitePos_mul_of_infiniteNeg_not_infinitesimal_neg, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
⊢ x.InfinitePos → y.InfiniteNeg → (x * y).InfiniteNeg

Tactic:
fun hx hy =>
  infiniteNeg_mul_of_infinitePos_not_infinitesimal_neg hx hy.not_infinitesimal (hy 0)

Premises used: Hyperreal.InfiniteNeg.not_infinitesimal, Hyperreal.infiniteNeg_mul_of_infinitePos_not_infinitesimal_neg, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
⊢ x.InfiniteNeg → y.InfinitePos → (x * y).InfiniteNeg

Tactic:
fun hx hy =>
  infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos hx hy.not_infinitesimal (hy 0)

Premises used: Hyperreal.InfinitePos.not_infinitesimal, Hyperreal.infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
⊢ x.Infinite → ¬y.Infinitesimal → (x * y).Infinite

Tactic:
fun hx hy =>
  have h0 : y < 0 ∨ 0 < y := lt_or_gt_of_ne fun H0 => hy (Eq.substr H0 (isSt_refl_real 0))
  hx.elim
    (h0.elim
      (fun H0 Hx => Or.inr (infiniteNeg_mul_of_infinitePos_not_infinitesimal_neg Hx hy H0))
      fun H0 Hx => Or.inl (infinitePos_mul_of_infinitePos_not_infinitesimal_pos Hx hy H0))
    (h0.elim
      (fun H0 Hx => Or.inl (infinitePos_mul_of_infiniteNeg_not_infinitesimal_neg Hx hy H0))
      fun H0 Hx => Or.inr (infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos Hx hy H0))

Premises used: lt_or_gt_of_ne, Hyperreal.infinitePos_mul_of_infinitePos_not_infinitesimal_pos, Hyperreal.infinitePos_mul_of_infiniteNeg_not_infinitesimal_neg, Eq.substr, Hyperreal.infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos, Or.inl, Or.elim, Hyperreal.infiniteNeg_mul_of_infinitePos_not_infinitesimal_neg, Or.inr
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
hx : ¬x.Infinitesimal
hy : y.Infinite
rw : (y * x).Infinite
⊢ (x * y).Infinite

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
hx : ¬x.Infinitesimal
hy : y.Infinite
⊢ (y * x).Infinite

Tactic:
infinite_mul_of_infinite_not_infinitesimal hy hx

Premises used: Hyperreal.infinite_mul_of_infinite_not_infinitesimal
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
hx : ¬x.Infinitesimal
hy : y.Infinite
⊢ (y * x).Infinite

Tactic:
exact infinite_mul_of_infinite_not_infinitesimal hy hx

Premises used: Hyperreal.infinite_mul_of_infinite_not_infinitesimal
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
⊢ x.Infinite → y.Infinite → (x * y).Infinite

Tactic:
fun hx hy =>
  infinite_mul_of_infinite_not_infinitesimal hx hy.not_infinitesimal

Premises used: Hyperreal.infinite_mul_of_infinite_not_infinitesimal, Hyperreal.Infinite.not_infinitesimal
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
digits : ℕ → Fin b
n : ℕ
⊢ 0 ≤ (↑(↑(digits n) : ℕ) : ℝ) * (HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1))⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
digits : ℕ → Fin b
⊢ 0 < b

Tactic:
Fin.pos (digits 0)

Premises used: Fin.pos, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
digits : ℕ → Fin b
n : ℕ
obtain :
  ∀ (c : ℕ) {digits : ℕ → Fin (c + 1)},
    ofDigitsTerm digits n ≤ HSub.hSub (α := ℝ) (↑(c + 1) : ℝ) 1 * (HPow.hPow (α := ℝ) (↑(c + 1) : ℝ) (n + 1))⁻¹
⊢ ofDigitsTerm digits n ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1))⁻¹

Tactic:
obtain ⟨c, rfl⟩ := Nat.exists_add_one_eq.mpr (b_pos digits)

Premises used: Iff.mpr, _private.0.Real.b_pos, Nat.exists_add_one_eq, rfl
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
n c : ℕ
digits : ℕ → Fin (c + 1)
hbc : (↑(↑(digits n) : ℕ) : ℝ) ≤ HSub.hSub (α := ℝ) (↑(c + 1) : ℝ) 1
⊢ (↑(↑(digits n) : ℕ) : ℝ) * (HPow.hPow (α := ℝ) (↑(c + 1) : ℝ) (n + 1))⁻¹ ≤
    HSub.hSub (α := ℝ) (↑(c + 1) : ℝ) 1 * (HPow.hPow (α := ℝ) (↑(c + 1) : ℝ) (n + 1))⁻¹

Tactic:
gcongr
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
n c : ℕ
digits : ℕ → Fin (c + 1)
hbc : (↑(digits n) : ℕ) ≤ c
⊢ (↑(↑(digits n) : ℕ) : ℝ) ≤ HSub.hSub (α := ℝ) (↑(c + 1) : ℝ) 1

Tactic:
simp
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
n c : ℕ
digits : ℕ → Fin (c + 1)
⊢ (↑(digits n) : ℕ) ≤ c

Tactic:
grind
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
digits : ℕ → Fin b
⊢ Summable (ofDigitsTerm digits)

Tactic:
Summable.of_nonneg_of_le (fun _ ↦ ofDigitsTerm_nonneg) (fun _ ↦ ofDigitsTerm_le) ?_

Premises used: Real.ofDigitsTerm_le, Summable.of_nonneg_of_le, Real.ofDigitsTerm_nonneg
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
digits : ℕ → Fin b
refine : Summable (α := ℝ) fun (x : ℕ) ↦ HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (x + 1))⁻¹
⊢ Summable (ofDigitsTerm digits)

Tactic:
refine Summable.of_nonneg_of_le (fun _ ↦ ofDigitsTerm_nonneg) (fun _ ↦ ofDigitsTerm_le) ?_

Premises used: Real.ofDigitsTerm_le, Summable.of_nonneg_of_le, Real.ofDigitsTerm_nonneg
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
digits : ℕ → Fin b
inl :
  ∀ {digits : ℕ → Fin 1},
    Summable (α := ℝ) fun (x : ℕ) ↦ HSub.hSub (α := ℝ) (↑1 : ℝ) 1 * (HPow.hPow (α := ℝ) (↑1 : ℝ) (x + 1))⁻¹
inr :
  ∀ (hb : 1 < b),
    Summable (α := ℝ) fun (x : ℕ) ↦ HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (x + 1))⁻¹
⊢ 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

Premises used: LE.le.eq_or_lt, _private.0.Real.b_pos, Nat.one_le_of_lt, rfl
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
digits : ℕ → Fin 1
⊢ Summable (α := ℝ) fun (x : ℕ) ↦ HSub.hSub (α := ℝ) (↑1 : ℝ) 1 * (HPow.hPow (α := ℝ) (↑1 : ℝ) (x + 1))⁻¹

Tactic:
simp
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
digits : ℕ → Fin b
hb : 1 < b
inr : Summable (α := ℝ) fun (x : ℕ) ↦ HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (↑b : ℝ)⁻¹ * HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ x
⊢ Summable (α := ℝ) fun (x : ℕ) ↦ HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (x + 1))⁻¹

Tactic:
simp_rw [pow_succ', mul_inv, ← inv_pow, ← mul_assoc]

Premises used: mul_inv, mul_assoc, inv_pow, pow_succ'
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
digits : ℕ → Fin b
hb : 1 < b
⊢ LE.le (α := ℝ) 0 (↑b : ℝ)⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
digits : ℕ → Fin b
hb : 1 < b
inr : LT.lt (α := ℝ) (↑b : ℝ)⁻¹ 1
⊢ Summable (α := ℝ) fun (x : ℕ) ↦ HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (↑b : ℝ)⁻¹ * HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ x

Tactic:
refine Summable.mul_left _ (summable_geometric_of_lt_one (by positivity) ?_)

Premises used: Summable.mul_left, summable_geometric_of_lt_one
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
digits : ℕ → Fin b
hb : 1 < b
⊢ LT.lt (α := ℝ) (↑b : ℝ)⁻¹ 1

Tactic:
simp [inv_lt_one_iff₀, hb]

Premises used: inv_lt_one_iff₀
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
digits : ℕ → Fin b
⊢ LE.le (α := ℝ) 0 (∑' (n : ℕ), ofDigitsTerm digits n)

Tactic:
tsum_nonneg fun _ ↦ ofDigitsTerm_nonneg

Premises used: Real.ofDigitsTerm_nonneg, tsum_nonneg
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
digits : ℕ → Fin b
⊢ LE.le (α := ℝ) 0 (∑' (n : ℕ), ofDigitsTerm digits n)

Tactic:
exact tsum_nonneg fun _ ↦ ofDigitsTerm_nonneg

Premises used: Real.ofDigitsTerm_nonneg, tsum_nonneg
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
digits : ℕ → Fin b
inl : ∀ (digits : ℕ → Fin 1), ofDigits digits ≤ 1
inr : ∀ (hb : 1 < b), ofDigits digits ≤ 1
⊢ ofDigits digits ≤ 1

Tactic:
obtain rfl | hb := (Nat.one_le_of_lt (b_pos digits)).eq_or_lt

Premises used: LE.le.eq_or_lt, _private.0.Real.b_pos, Nat.one_le_of_lt, rfl
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
digits : ℕ → Fin 1
⊢ ofDigits digits ≤ 1

Tactic:
simp [ofDigits, ofDigitsTerm]

Premises used: Real.ofDigitsTerm, Real.ofDigits
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
digits : ℕ → Fin b
hb : 1 < b
⊢ LT.lt (α := ℝ) 1 (↑b : ℝ)

Tactic:
rify at hb
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
digits : ℕ → Fin b
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ LE.le (α := ℝ) (∑' (n : ℕ), ofDigitsTerm digits n)
    (∑' (n : ℕ), HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1))⁻¹)

Tactic:
Summable.tsum_mono summable_ofDigitsTerm _ (fun _ ↦ ofDigitsTerm_le)

Premises used: Real.summable_ofDigitsTerm, Real.ofDigitsTerm_le, Summable.tsum_mono
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
digits : ℕ → Fin b
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
h : Eq (α := ℝ) 1 (∑' (n : ℕ), HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1))⁻¹)
inr : Summable (α := ℝ) fun (x : ℕ) ↦ HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (x + 1))⁻¹
⊢ ofDigits digits ≤ 1

Tactic:
convert! Summable.tsum_mono summable_ofDigitsTerm _ (fun _ ↦ ofDigitsTerm_le)

Premises used: Real.summable_ofDigitsTerm, Real.ofDigitsTerm_le, Summable.tsum_mono
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
digits : ℕ → Fin b
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
h : Eq (α := ℝ) 1 (∑' (n : ℕ), HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (↑b : ℝ)⁻¹ * HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ n)
⊢ Eq (α := ℝ) 1 (∑' (n : ℕ), HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1))⁻¹)

Tactic:
simp_rw [pow_succ', mul_inv, ← inv_pow, ← mul_assoc]

Premises used: mul_inv, mul_assoc, inv_pow, pow_succ'
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
digits : ℕ → Fin b
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ LE.le (α := ℝ) 0 (↑b : ℝ)⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
digits : ℕ → Fin b
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ LT.lt (α := ℝ) (↑b : ℝ)⁻¹ 1

Tactic:
simp [inv_lt_one_iff₀, hb]

Premises used: inv_lt_one_iff₀
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
digits : ℕ → Fin b
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
h : 1 = HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (↑b : ℝ)⁻¹ * (HSub.hSub (α := ℝ) 1 (↑b : ℝ)⁻¹)⁻¹
⊢ Eq (α := ℝ) 1 (∑' (n : ℕ), HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (↑b : ℝ)⁻¹ * HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ n)

Tactic:
rw [tsum_mul_left, tsum_geometric_of_lt_one (by positivity) (by simp [inv_lt_one_iff₀, hb])]

Premises used: tsum_geometric_of_lt_one, tsum_mul_left
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
digits : ℕ → Fin b
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ 0 < HSub.hSub (α := ℝ) (↑b : ℝ) 1

Tactic:
have := sub_pos.mpr hb
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
digits : ℕ → Fin b
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
this : 0 < HSub.hSub (α := ℝ) (↑b : ℝ) 1
⊢ 1 = HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (↑b : ℝ)⁻¹ * (HSub.hSub (α := ℝ) 1 (↑b : ℝ)⁻¹)⁻¹

Tactic:
field
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
digits : ℕ → Fin b
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
inr : Summable (α := ℝ) fun (x : ℕ) ↦ HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (↑b : ℝ)⁻¹ * HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ x
⊢ Summable (α := ℝ) fun (x : ℕ) ↦ HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (x + 1))⁻¹

Tactic:
simp_rw [pow_succ', mul_inv, ← inv_pow, ← mul_assoc]

Premises used: mul_inv, mul_assoc, inv_pow, pow_succ'
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
digits : ℕ → Fin b
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
inr : LT.lt (α := ℝ) (↑b : ℝ)⁻¹ 1
⊢ Summable (α := ℝ) fun (x : ℕ) ↦ HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (↑b : ℝ)⁻¹ * HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ x

Tactic:
refine Summable.mul_left _ (summable_geometric_of_lt_one (by positivity) ?_)

Premises used: Summable.mul_left, summable_geometric_of_lt_one
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
a : ℕ → Fin b
n : ℕ
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)
⊢ ∑' (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

Tactic:
rw [← Summable.sum_add_tsum_nat_add n summable_ofDigitsTerm,
    ← Summable.tsum_mul_left _ summable_ofDigitsTerm]

Premises used: Real.summable_ofDigitsTerm, Summable.tsum_mul_left, Summable.sum_add_tsum_nat_add
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
a : ℕ → Fin b
n : ℕ
e_a :
  Eq (α := ℕ → ℝ) (fun (i : ℕ) ↦ ofDigitsTerm a (i + n)) fun (i : ℕ) ↦
    (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹ * ofDigitsTerm (b := b) (fun (i : ℕ) ↦ a (i + n)) i
⊢ 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:
congr
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
a : ℕ → Fin b
n : ℕ
e_a :
  ∀ (i : ℕ),
    ofDigitsTerm a (i + n) = (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹ * ofDigitsTerm (b := b) (fun (i : ℕ) ↦ a (i + n)) i
⊢ Eq (α := ℕ → ℝ) (fun (i : ℕ) ↦ ofDigitsTerm a (i + n)) fun (i : ℕ) ↦
    (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹ * ofDigitsTerm (b := b) (fun (i : ℕ) ↦ a (i + n)) i

Tactic:
ext i
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
a : ℕ → Fin b
n i : ℕ
e_a :
  (↑(↑(a (i + n)) : ℕ) : ℝ) * (HPow.hPow (α := ℝ) (↑b : ℝ) (i + n + 1))⁻¹ =
    (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹ * ((↑(↑(a (i + n)) : ℕ) : ℝ) * (HPow.hPow (α := ℝ) (↑b : ℝ) (i + 1))⁻¹)
⊢ ofDigitsTerm a (i + n) = (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹ * ofDigitsTerm (b := b) (fun (i : ℕ) ↦ a (i + n)) i

Tactic:
simp only [ofDigitsTerm]

Premises used: Real.ofDigitsTerm
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
a : ℕ → Fin b
n i : ℕ
⊢ (↑(↑(a (i + n)) : ℕ) : ℝ) * (HPow.hPow (α := ℝ) (↑b : ℝ) (i + n + 1))⁻¹ =
    (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹ * ((↑(↑(a (i + n)) : ℕ) : ℝ) * (HPow.hPow (α := ℝ) (↑b : ℝ) (i + 1))⁻¹)

Tactic:
ring
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
x y : ℕ → Fin b
n : ℕ
hxy : ∀ i < n, x i = y i
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)⁻¹
⊢ |ofDigits x - ofDigits y| ≤ (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹

Tactic:
rw [ofDigits_eq_sum_add_ofDigits x n, ofDigits_eq_sum_add_ofDigits y n]

Premises used: Real.ofDigits_eq_sum_add_ofDigits
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
x y : ℕ → Fin b
n : ℕ
hxy : ∀ i < n, x i = y i
i : ℕ
hi : i ∈ Finset.range n
⊢ ofDigitsTerm x i = ofDigitsTerm y i

Tactic:
simp [ofDigitsTerm, hxy i (Finset.mem_range.mp hi)]

Premises used: Finset.mem_range, Real.ofDigitsTerm, Iff.mp
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
x y : ℕ → Fin b
n : ℕ
hxy : ∀ i < n, x i = y i
⊢ 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)]
-- Module: Mathlib.Analysis.Real.OfDigits
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)
⊢ 0 ≤ (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹

Tactic:
positivity