awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
this : ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₀ : ¬0 < b
linarith : -b ≤ 0 → b < -1 → b < 0 → b < 1 → -1 + (b - -1) + (-b - 0) = 0
linarith₁ : -b ≤ 0 → b < -1 → b < 0 → 1 < b → HMul.hMul (α := ℝ) 2 (-1) + (b - -1) + (1 - b) = 0
⊢ 0 < -b
have linarith₂ : -b ≤ 0 → b < -1 → b < 0 → 1 < b → GT.gt (α := ℝ) 2 0
Tactic: linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
this : ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₀ : ¬0 < b
linarith : -b ≤ 0 → b < -1 → b < 0 → b < 1 → -1 + (b - -1) + (-b - 0) = 0
linarith₁ : -b ≤ 0 → b < -1 → b < 0 → 1 < b → HMul.hMul (α := ℝ) 2 (-1) + (b - -1) + (1 - b) = 0
linarith₂ : -b ≤ 0 → b < -1 → b < 0 → 1 < b → GT.gt (α := ℝ) 2 0
⊢ 0 < -b
have linarith₃ : -b ≤ 0 → b < -1 → 0 < b → b < 1 → -1 + (b - -1) + (0 - b) = 0
Tactic: linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
this : ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₀ : ¬0 < b
linarith : -b ≤ 0 → b < -1 → b < 0 → b < 1 → -1 + (b - -1) + (-b - 0) = 0
linarith₁ : -b ≤ 0 → b < -1 → b < 0 → 1 < b → HMul.hMul (α := ℝ) 2 (-1) + (b - -1) + (1 - b) = 0
linarith₂ : -b ≤ 0 → b < -1 → b < 0 → 1 < b → GT.gt (α := ℝ) 2 0
linarith₃ : -b ≤ 0 → b < -1 → 0 < b → b < 1 → -1 + (b - -1) + (0 - b) = 0
⊢ 0 < -b
have linarith₄ : -b ≤ 0 → b < -1 → 0 < b → 1 < b → -1 + (b - -1) + (0 - b) = 0
Tactic: linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
this : ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₀ : ¬0 < b
linarith : -b ≤ 0 → b < -1 → b < 0 → b < 1 → -1 + (b - -1) + (-b - 0) = 0
linarith₁ : -b ≤ 0 → b < -1 → b < 0 → 1 < b → HMul.hMul (α := ℝ) 2 (-1) + (b - -1) + (1 - b) = 0
linarith₂ : -b ≤ 0 → b < -1 → b < 0 → 1 < b → GT.gt (α := ℝ) 2 0
linarith₃ : -b ≤ 0 → b < -1 → 0 < b → b < 1 → -1 + (b - -1) + (0 - b) = 0
linarith₄ : -b ≤ 0 → b < -1 → 0 < b → 1 < b → -1 + (b - -1) + (0 - b) = 0
⊢ 0 < -b
have linarith₅ : -b ≤ 0 → -1 < b → b < 0 → b < 1 → b - 0 + (-b - 0) = 0
Tactic: linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
this : ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₀ : ¬0 < b
linarith : -b ≤ 0 → b < -1 → b < 0 → b < 1 → -1 + (b - -1) + (-b - 0) = 0
linarith₁ : -b ≤ 0 → b < -1 → b < 0 → 1 < b → HMul.hMul (α := ℝ) 2 (-1) + (b - -1) + (1 - b) = 0
linarith₂ : -b ≤ 0 → b < -1 → b < 0 → 1 < b → GT.gt (α := ℝ) 2 0
linarith₃ : -b ≤ 0 → b < -1 → 0 < b → b < 1 → -1 + (b - -1) + (0 - b) = 0
linarith₄ : -b ≤ 0 → b < -1 → 0 < b → 1 < b → -1 + (b - -1) + (0 - b) = 0
linarith₅ : -b ≤ 0 → -1 < b → b < 0 → b < 1 → b - 0 + (-b - 0) = 0
⊢ 0 < -b
have linarith₆ : -b ≤ 0 → -1 < b → b < 0 → 1 < b → -1 - b + 2 * (b - 0) + (1 - b) = 0
Tactic: linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
this : ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₀ : ¬0 < b
linarith : -b ≤ 0 → b < -1 → b < 0 → b < 1 → -1 + (b - -1) + (-b - 0) = 0
linarith₁ : -b ≤ 0 → b < -1 → b < 0 → 1 < b → HMul.hMul (α := ℝ) 2 (-1) + (b - -1) + (1 - b) = 0
linarith₂ : -b ≤ 0 → b < -1 → b < 0 → 1 < b → GT.gt (α := ℝ) 2 0
linarith₃ : -b ≤ 0 → b < -1 → 0 < b → b < 1 → -1 + (b - -1) + (0 - b) = 0
linarith₄ : -b ≤ 0 → b < -1 → 0 < b → 1 < b → -1 + (b - -1) + (0 - b) = 0
linarith₅ : -b ≤ 0 → -1 < b → b < 0 → b < 1 → b - 0 + (-b - 0) = 0
linarith₆ : -b ≤ 0 → -1 < b → b < 0 → 1 < b → -1 - b + 2 * (b - 0) + (1 - b) = 0
⊢ 0 < -b
have linarith₇ : -b ≤ 0 → -1 < b → b < 0 → 1 < b → GT.gt (α := ℝ) 2 0
Tactic: linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
this : ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₀ : ¬0 < b
linarith : -b ≤ 0 → b < -1 → b < 0 → b < 1 → -1 + (b - -1) + (-b - 0) = 0
linarith₁ : -b ≤ 0 → b < -1 → b < 0 → 1 < b → HMul.hMul (α := ℝ) 2 (-1) + (b - -1) + (1 - b) = 0
linarith₂ : -b ≤ 0 → b < -1 → b < 0 → 1 < b → GT.gt (α := ℝ) 2 0
linarith₃ : -b ≤ 0 → b < -1 → 0 < b → b < 1 → -1 + (b - -1) + (0 - b) = 0
linarith₄ : -b ≤ 0 → b < -1 → 0 < b → 1 < b → -1 + (b - -1) + (0 - b) = 0
linarith₅ : -b ≤ 0 → -1 < b → b < 0 → b < 1 → b - 0 + (-b - 0) = 0
linarith₆ : -b ≤ 0 → -1 < b → b < 0 → 1 < b → -1 - b + 2 * (b - 0) + (1 - b) = 0
linarith₇ : -b ≤ 0 → -1 < b → b < 0 → 1 < b → GT.gt (α := ℝ) 2 0
⊢ 0 < -b
have linarith₈ : -b ≤ 0 → -1 < b → 0 < b → b < 1 → 0 - b + (b - 0) = 0
Tactic: linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
this : ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₀ : ¬0 < b
linarith : -b ≤ 0 → b < -1 → b < 0 → b < 1 → -1 + (b - -1) + (-b - 0) = 0
linarith₁ : -b ≤ 0 → b < -1 → b < 0 → 1 < b → HMul.hMul (α := ℝ) 2 (-1) + (b - -1) + (1 - b) = 0
linarith₂ : -b ≤ 0 → b < -1 → b < 0 → 1 < b → GT.gt (α := ℝ) 2 0
linarith₃ : -b ≤ 0 → b < -1 → 0 < b → b < 1 → -1 + (b - -1) + (0 - b) = 0
linarith₄ : -b ≤ 0 → b < -1 → 0 < b → 1 < b → -1 + (b - -1) + (0 - b) = 0
linarith₅ : -b ≤ 0 → -1 < b → b < 0 → b < 1 → b - 0 + (-b - 0) = 0
linarith₆ : -b ≤ 0 → -1 < b → b < 0 → 1 < b → -1 - b + 2 * (b - 0) + (1 - b) = 0
linarith₇ : -b ≤ 0 → -1 < b → b < 0 → 1 < b → GT.gt (α := ℝ) 2 0
linarith₈ : -b ≤ 0 → -1 < b → 0 < b → b < 1 → 0 - b + (b - 0) = 0
⊢ 0 < -b
have linarith₉ : -b ≤ 0 → -1 < b → 0 < b → 1 < b → -1 + (1 - b) + (b - 0) = 0
Tactic: linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b_1 b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
have inr : ∀
  (this :
    ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b) (hb₁ : 1 < b),
      Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop)
  (hb₁ : ¬1 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
Tactic: wlog hb₁ : 1 < b generalizing b
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b_1 b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
inr :
  ∀
    (this :
      ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b) (hb₁ : 1 < b),
        Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop)
    (hb₁ : ¬1 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
have wlog : ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b) (hb₁ : 1 < b),
  Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
Tactic: wlog hb₁ : 1 < b generalizing b
Cleared hypotheses: b, hb, hb₀
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b_1 b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
this :
  ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b) (hb₁ : 1 < b),
    Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₁ : ¬1 < b
⊢ b < 1
have linarith : 1 ≤ b → b < -1 → b < 0 → b < 1 → -1 + (b - -1) + (0 - b) = 0
Tactic: linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b_1 b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
this :
  ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b) (hb₁ : 1 < b),
    Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₁ : ¬1 < b
linarith : 1 ≤ b → b < -1 → b < 0 → b < 1 → -1 + (b - -1) + (0 - b) = 0
⊢ b < 1
have linarith₁ : 1 ≤ b → b < -1 → b < 0 → 1 < b → HMul.hMul (α := ℝ) 2 (-1) + (b - -1) + (1 - b) = 0
Tactic: linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b_1 b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
this :
  ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b) (hb₁ : 1 < b),
    Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₁ : ¬1 < b
linarith : 1 ≤ b → b < -1 → b < 0 → b < 1 → -1 + (b - -1) + (0 - b) = 0
linarith₁ : 1 ≤ b → b < -1 → b < 0 → 1 < b → HMul.hMul (α := ℝ) 2 (-1) + (b - -1) + (1 - b) = 0
⊢ b < 1
have linarith₂ : 1 ≤ b → b < -1 → b < 0 → 1 < b → GT.gt (α := ℝ) 2 0
Tactic: linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b_1 b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
this :
  ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b) (hb₁ : 1 < b),
    Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₁ : ¬1 < b
linarith : 1 ≤ b → b < -1 → b < 0 → b < 1 → -1 + (b - -1) + (0 - b) = 0
linarith₁ : 1 ≤ b → b < -1 → b < 0 → 1 < b → HMul.hMul (α := ℝ) 2 (-1) + (b - -1) + (1 - b) = 0
linarith₂ : 1 ≤ b → b < -1 → b < 0 → 1 < b → GT.gt (α := ℝ) 2 0
⊢ b < 1
have linarith₃ : 1 ≤ b → b < -1 → 0 < b → b < 1 → -1 + (b - -1) + (0 - b) = 0
Tactic: linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b_1 b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
this :
  ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b) (hb₁ : 1 < b),
    Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₁ : ¬1 < b
linarith : 1 ≤ b → b < -1 → b < 0 → b < 1 → -1 + (b - -1) + (0 - b) = 0
linarith₁ : 1 ≤ b → b < -1 → b < 0 → 1 < b → HMul.hMul (α := ℝ) 2 (-1) + (b - -1) + (1 - b) = 0
linarith₂ : 1 ≤ b → b < -1 → b < 0 → 1 < b → GT.gt (α := ℝ) 2 0
linarith₃ : 1 ≤ b → b < -1 → 0 < b → b < 1 → -1 + (b - -1) + (0 - b) = 0
⊢ b < 1
have linarith₄ : 1 ≤ b → b < -1 → 0 < b → 1 < b → -1 + (b - -1) + (0 - b) = 0
Tactic: linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b_1 b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
this :
  ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b) (hb₁ : 1 < b),
    Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₁ : ¬1 < b
linarith : 1 ≤ b → b < -1 → b < 0 → b < 1 → -1 + (b - -1) + (0 - b) = 0
linarith₁ : 1 ≤ b → b < -1 → b < 0 → 1 < b → HMul.hMul (α := ℝ) 2 (-1) + (b - -1) + (1 - b) = 0
linarith₂ : 1 ≤ b → b < -1 → b < 0 → 1 < b → GT.gt (α := ℝ) 2 0
linarith₃ : 1 ≤ b → b < -1 → 0 < b → b < 1 → -1 + (b - -1) + (0 - b) = 0
linarith₄ : 1 ≤ b → b < -1 → 0 < b → 1 < b → -1 + (b - -1) + (0 - b) = 0
⊢ b < 1
have linarith₅ : 1 ≤ b → -1 < b → b < 0 → b < 1 → b - 0 + (0 - b) = 0
Tactic: linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b_1 b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
this :
  ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b) (hb₁ : 1 < b),
    Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₁ : ¬1 < b
linarith : 1 ≤ b → b < -1 → b < 0 → b < 1 → -1 + (b - -1) + (0 - b) = 0
linarith₁ : 1 ≤ b → b < -1 → b < 0 → 1 < b → HMul.hMul (α := ℝ) 2 (-1) + (b - -1) + (1 - b) = 0
linarith₂ : 1 ≤ b → b < -1 → b < 0 → 1 < b → GT.gt (α := ℝ) 2 0
linarith₃ : 1 ≤ b → b < -1 → 0 < b → b < 1 → -1 + (b - -1) + (0 - b) = 0
linarith₄ : 1 ≤ b → b < -1 → 0 < b → 1 < b → -1 + (b - -1) + (0 - b) = 0
linarith₅ : 1 ≤ b → -1 < b → b < 0 → b < 1 → b - 0 + (0 - b) = 0
⊢ b < 1
have linarith₆ : 1 ≤ b → -1 < b → b < 0 → 1 < b → -1 - b + 2 * (b - 0) + (1 - b) = 0
Tactic: linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b_1 b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
this :
  ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b) (hb₁ : 1 < b),
    Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₁ : ¬1 < b
linarith : 1 ≤ b → b < -1 → b < 0 → b < 1 → -1 + (b - -1) + (0 - b) = 0
linarith₁ : 1 ≤ b → b < -1 → b < 0 → 1 < b → HMul.hMul (α := ℝ) 2 (-1) + (b - -1) + (1 - b) = 0
linarith₂ : 1 ≤ b → b < -1 → b < 0 → 1 < b → GT.gt (α := ℝ) 2 0
linarith₃ : 1 ≤ b → b < -1 → 0 < b → b < 1 → -1 + (b - -1) + (0 - b) = 0
linarith₄ : 1 ≤ b → b < -1 → 0 < b → 1 < b → -1 + (b - -1) + (0 - b) = 0
linarith₅ : 1 ≤ b → -1 < b → b < 0 → b < 1 → b - 0 + (0 - b) = 0
linarith₆ : 1 ≤ b → -1 < b → b < 0 → 1 < b → -1 - b + 2 * (b - 0) + (1 - b) = 0
⊢ b < 1
have linarith₇ : 1 ≤ b → -1 < b → b < 0 → 1 < b → GT.gt (α := ℝ) 2 0
Tactic: linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b_1 b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
this :
  ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b) (hb₁ : 1 < b),
    Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₁ : ¬1 < b
linarith : 1 ≤ b → b < -1 → b < 0 → b < 1 → -1 + (b - -1) + (0 - b) = 0
linarith₁ : 1 ≤ b → b < -1 → b < 0 → 1 < b → HMul.hMul (α := ℝ) 2 (-1) + (b - -1) + (1 - b) = 0
linarith₂ : 1 ≤ b → b < -1 → b < 0 → 1 < b → GT.gt (α := ℝ) 2 0
linarith₃ : 1 ≤ b → b < -1 → 0 < b → b < 1 → -1 + (b - -1) + (0 - b) = 0
linarith₄ : 1 ≤ b → b < -1 → 0 < b → 1 < b → -1 + (b - -1) + (0 - b) = 0
linarith₅ : 1 ≤ b → -1 < b → b < 0 → b < 1 → b - 0 + (0 - b) = 0
linarith₆ : 1 ≤ b → -1 < b → b < 0 → 1 < b → -1 - b + 2 * (b - 0) + (1 - b) = 0
linarith₇ : 1 ≤ b → -1 < b → b < 0 → 1 < b → GT.gt (α := ℝ) 2 0
⊢ b < 1
have linarith₈ : 1 ≤ b → -1 < b → 0 < b → b < 1 → b - 1 + (1 - b) = 0
Tactic: linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b_1 b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
this :
  ∀ {b : ℝ} (hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1) (hb₀ : 0 < b) (hb₁ : 1 < b),
    Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
hb₁ : ¬1 < b
linarith : 1 ≤ b → b < -1 → b < 0 → b < 1 → -1 + (b - -1) + (0 - b) = 0
linarith₁ : 1 ≤ b → b < -1 → b < 0 → 1 < b → HMul.hMul (α := ℝ) 2 (-1) + (b - -1) + (1 - b) = 0
linarith₂ : 1 ≤ b → b < -1 → b < 0 → 1 < b → GT.gt (α := ℝ) 2 0
linarith₃ : 1 ≤ b → b < -1 → 0 < b → b < 1 → -1 + (b - -1) + (0 - b) = 0
linarith₄ : 1 ≤ b → b < -1 → 0 < b → 1 < b → -1 + (b - -1) + (0 - b) = 0
linarith₅ : 1 ≤ b → -1 < b → b < 0 → b < 1 → b - 0 + (0 - b) = 0
linarith₆ : 1 ≤ b → -1 < b → b < 0 → 1 < b → -1 - b + 2 * (b - 0) + (1 - b) = 0
linarith₇ : 1 ≤ b → -1 < b → b < 0 → 1 < b → GT.gt (α := ℝ) 2 0
linarith₈ : 1 ≤ b → -1 < b → 0 < b → b < 1 → b - 1 + (1 - b) = 0
⊢ b < 1
have linarith₉ : 1 ≤ b → -1 < b → 0 < b → 1 < b → 1 - b + (b - 1) = 0
Tactic: linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b_1 b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
hb₁ : 1 < b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ |logb b x|) atTop atTop
have refine : logb b =ᶠ[atTop] fun (x : ℝ) ↦ |logb b x|
Tactic: refine (tendsto_logb_atTop hb₁).congr' ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b_1 b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
hb₁ : 1 < b
⊢ logb b =ᶠ[atTop] fun (x : ℝ) ↦ |logb b x|
have h : ∀ (x : ℝ) (hx₁ : 1 ≤ x), logb b x = |logb b x|
Tactic: filter_upwards [eventually_ge_atTop 1] with x hx₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b_1 b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
hb₁ : 1 < b
x : ℝ
hx₁ : 1 ≤ x
⊢ logb b x = |logb b x|
have h : 0 ≤ logb b x
Tactic: rw [abs_of_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
hb₀ : 0 < b
hb : b ≠ 1
⊢ ContinuousAt (logb b) x ↔ x ≠ 0
have refine : ContinuousAt (logb b) x → x ≠ 0
Tactic: refine ⟨?_, continuousAt_logb⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (hypothesis)
Goal:
b : ℝ
hb₀ : 0 < b
hb : b ≠ 1
h : ContinuousAt (logb b) 0
⊢ False
have x : b < 1 ∨ 1 < b
Tactic: cases lt_or_gt_of_ne hb with
  | inl hb₁ =>
      exact not_tendsto_nhds_of_tendsto_atTop (tendsto_logb_nhdsNE_zero_of_base_lt_one hb₀ hb₁)
        _ (h.tendsto.mono_left inf_le_left)
  | inr hb₁ =>
      exact not_tendsto_nhds_of_tendsto_atBot (tendsto_logb_nhdsNE_zero hb₁)
        _ (h.tendsto.mono_left inf_le_left)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ x ∈ s, f x ≠ 0
⊢ logb b (∏ i ∈ s, f i) = ∑ i ∈ s, logb b (f i)
have empty : ∀ (hf : ∀ (x : α), Membership.mem (γ := Finset α) ∅ x → f x ≠ 0), logb b (∏ i ∈ ∅, f i) = ∑ i ∈ ∅, logb b (f i)
Tactic: induction s using Finset.cons_induction_on with
  | empty => simp
  | cons => simp_all [logb_mul, Finset.prod_ne_zero_iff]
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ x ∈ s, f x ≠ 0
empty : ∀ (hf : ∀ (x : α), Membership.mem (γ := Finset α) ∅ x → f x ≠ 0), logb b (∏ i ∈ ∅, f i) = ∑ i ∈ ∅, logb b (f i)
⊢ logb b (∏ i ∈ s, f i) = ∑ i ∈ s, logb b (f i)
have cons : ∀ (a : α) (s : Finset α) (h : a ∉ s),
  (∀ (hf : ∀ x ∈ s, f x ≠ 0), logb b (∏ i ∈ s, f i) = ∑ i ∈ s, logb b (f i)) →
    ∀ (hf : ∀ x ∈ Finset.cons a s h, f x ≠ 0),
      logb b (∏ i ∈ Finset.cons a s h, f i) = ∑ i ∈ Finset.cons a s h, logb b (f i)
Tactic: induction s using Finset.cons_induction_on with
  | empty => simp
  | cons => simp_all [logb_mul, Finset.prod_ne_zero_iff]
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (hypothesis)
Goal:
b a c : ℝ
n : ℕ
ha : a ≠ 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ logb b x ^ n / (a * x + c)) atTop (𝓝 0)
have x : log b = 0 ∨ log b ≠ 0
Tactic: cases eq_or_ne (log b) 0 with
  | inl h => simpa [logb, h] using ((tendsto_mul_add_inv_atTop_nhds_zero _ _ ha).const_mul _)
  | inr h => apply (tendsto_pow_log_div_mul_add_atTop (a * (log b) ^ n) (c * (log b) ^ n) n
                (by positivity)).congr fun x ↦ by simp [field, div_pow, logb]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
n : ℕ
⊢ Asymptotics.IsLittleO (E := ℝ) atTop (fun (x : ℝ) ↦ logb b x ^ n) id
have rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ logb b x ^ n / id x) atTop (𝓝 0)
Tactic: rw [Asymptotics.isLittleO_iff_tendsto']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
n : ℕ
rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ logb b x ^ n / id x) atTop (𝓝 0)
⊢ Asymptotics.IsLittleO (E := ℝ) atTop (fun (x : ℝ) ↦ logb b x ^ n) id
have rw₁ : ∀ᶠ (x : ℝ) in atTop, id x = 0 → logb b x ^ n = 0
Tactic: rw [Asymptotics.isLittleO_iff_tendsto']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
n : ℕ
⊢ ∀ᶠ (x : ℝ) in atTop, id x = 0 → logb b x ^ n = 0
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ≠ 0) x} x →
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ id x = 0 → logb b x ^ n = 0) x} x}
    a
Tactic: filter_upwards [eventually_ne_atTop (0 : ℝ)] with x h₁ h₂ using (h₁ h₂).elim
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
n : ℕ
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ≠ 0) x} x →
          Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ id x = 0 → logb b x ^ n = 0) x} x}
      a
⊢ ∀ᶠ (x : ℝ) in atTop, id x = 0 → logb b x ^ n = 0
have h₁ : ∀ (a : ℝ), a ≠ 0 → id a = 0 → logb b a ^ n = 0
Tactic: filter_upwards [eventually_ne_atTop (0 : ℝ)] with x h₁ h₂ using (h₁ h₂).elim
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b c : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
⊢ Asymptotics.IsLittleO (E := ℝ) atTop (fun (x : ℝ) ↦ c) (logb b)
have rw : ¬c = 0 → Tendsto (Norm.norm ∘ logb b) atTop atTop
Tactic: rw [Asymptotics.isLittleO_const_left, or_iff_not_imp_left]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
⊢ logb b =O[⊤] log
have pos : ∀ (h : b = -1 ∨ b = 0 ∨ b = 1), logb b =O[⊤] log
Tactic: by_cases! h : b = -1 ∨ b = 0 ∨ b = 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
pos : ∀ (h : b = -1 ∨ b = 0 ∨ b = 1), logb b =O[⊤] log
⊢ logb b =O[⊤] log
have neg : ∀ (h : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1), logb b =O[⊤] log
Tactic: by_cases! h : b = -1 ∨ b = 0 ∨ b = 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
h : b = -1 ∨ b = 0 ∨ b = 1
⊢ logb b =O[⊤] log
have pos : logb (-1) =O[⊤] log
Tactic: obtain rfl | rfl | rfl := h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
h : b = -1 ∨ b = 0 ∨ b = 1
pos : logb (-1) =O[⊤] log
⊢ logb b =O[⊤] log
have pos₁ : logb 0 =O[⊤] log
Tactic: obtain rfl | rfl | rfl := h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
h : b = -1 ∨ b = 0 ∨ b = 1
pos : logb (-1) =O[⊤] log
pos₁ : logb 0 =O[⊤] log
⊢ logb b =O[⊤] log
have pos₂ : logb 1 =O[⊤] log
Tactic: obtain rfl | rfl | rfl := h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
c : ℝ
⊢ Asymptotics.IsBigO (E := ℝ) atTop (fun (x : ℝ) ↦ log (c * x)) log
have inl : Asymptotics.IsBigO (E := ℝ) atTop (fun (x : ℝ) ↦ log (0 * x)) log
Tactic: obtain rfl | hc := eq_or_ne c 0
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
c : ℝ
inl : Asymptotics.IsBigO (E := ℝ) atTop (fun (x : ℝ) ↦ log (0 * x)) log
⊢ Asymptotics.IsBigO (E := ℝ) atTop (fun (x : ℝ) ↦ log (c * x)) log
have inr : ∀ (hc : c ≠ 0), Asymptotics.IsBigO (E := ℝ) atTop (fun (x : ℝ) ↦ log (c * x)) log
Tactic: obtain rfl | hc := eq_or_ne c 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
c : ℝ
hc : c ≠ 0
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ log (c * x)) fun (x : ℝ) ↦ log c + log x
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 0 < x) x} x →
        Membership.mem (γ := Set ℝ)
          {x : ℝ | (fun (x : ℝ) ↦ Eq (α := ℝ) ((fun (x : ℝ) ↦ log (c * x)) x) ((fun (x : ℝ) ↦ log c + log x) x)) x} x}
    a
Tactic: filter_upwards [eventually_gt_atTop 0] with a ha using log_mul hc ha.ne'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
c : ℝ
hc : c ≠ 0
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 0 < x) x} x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ | (fun (x : ℝ) ↦ Eq (α := ℝ) ((fun (x : ℝ) ↦ log (c * x)) x) ((fun (x : ℝ) ↦ log c + log x) x)) x} x}
      a
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ log (c * x)) fun (x : ℝ) ↦ log c + log x
have h₁ : ∀ (a : ℝ), 0 < a → log (c * a) = log c + log a
Tactic: filter_upwards [eventually_gt_atTop 0] with a ha using log_mul hc ha.ne'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
c : ℝ
hc : c ≠ 0
⊢ Asymptotics.IsBigO (E := ℝ) atTop (fun (x : ℝ) ↦ log (c * x)) log
have calc : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ log (c * x)) fun (x : ℝ) ↦ log c + log x
Tactic: calc (fun x ↦ log (c * x))
      =ᶠ[atTop] (fun x => log c + log x) := by
          filter_upwards [eventually_gt_atTop 0] with a ha using log_mul hc ha.ne'
      _ =O[atTop] log :=
          isLittleO_const_log_atTop.isBigO.add (Asymptotics.isBigO_refl ..)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
this : ∀ (n : ℕ), ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x
x : ℝ
hx : x ≥ x₀
⊢ P x
have have : ∀ (hx' : 0 < x / x₀), P x
Tactic: have hx' : 0 < x / x₀ := div_pos (hx₀.trans_le hx) hx₀
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
this : ∀ (n : ℕ), ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x
x : ℝ
hx : x ≥ x₀
hx' : 0 < x / x₀
⊢ P x
have refine : x ∈ Ico x₀ (r ^ (⌊logb r (x / x₀)⌋₊ + 1) * x₀)
Tactic: refine this ⌊logb r (x / x₀)⌋₊ x ?_