awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain :
  ∀ (m : ℕ) (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) * x₀) →
        f z = 0
⊢ logb 2 (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) 1)) ≤ logb 2 (x / x₀)
have rw : -logb 2 (x / x₀) ≤ -(↑(HSub.hSub (α := ℤ) (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) 1) : ℝ)
Tactic: rw [← rpow_intCast, logb_rpow (by norm_num) (by norm_num), ← neg_le_neg_iff]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain :
  ∀ (m : ℕ) (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) * x₀) →
        f z = 0
⊢ -logb 2 (x / x₀) ≤ -(↑(HSub.hSub (α := ℤ) (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) 1) : ℝ)
have simp : -logb 2 (x / x₀) ≤ HAdd.hAdd (α := ℝ) 1 (↑⌊-logb 2 (x / x₀)⌋₊ : ℝ)
Tactic: simp only [Int.cast_sub, Int.cast_neg, Int.cast_natCast, Int.cast_one, neg_sub, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain :
  ∀ (m : ℕ) (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) * x₀) →
        f z = 0
⊢ (↑⌈-logb 2 (x / x₀)⌉₊ : ℝ) ≤ HAdd.hAdd (α := ℝ) 1 (↑⌊-logb 2 (x / x₀)⌋₊ : ℝ)
have rw : (↑⌈-logb 2 (x / x₀)⌉₊ : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑⌊-logb 2 (x / x₀)⌋₊ : ℝ) 1
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain :
  ∀ (m : ℕ) (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) * x₀) →
        f z = 0
⊢ -logb 2 (x / x₀) ≤ HAdd.hAdd (α := ℝ) 1 (↑⌊-logb 2 (x / x₀)⌋₊ : ℝ)
have calc : (↑⌈-logb 2 (x / x₀)⌉₊ : ℝ) ≤ HAdd.hAdd (α := ℝ) 1 (↑⌊-logb 2 (x / x₀)⌋₊ : ℝ)
Tactic: calc -logb 2 (x / x₀) ≤ ⌈-logb 2 (x / x₀)⌉₊ := Nat.le_ceil (-logb 2 (x / x₀))
         _ ≤ _ := by rw [add_comm]; exact_mod_cast Nat.ceil_le_floor_add_one _
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain :
  ∀ (m : ℕ) (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) * x₀) →
        f z = 0
⊢ x ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) * x₀
have rw : x / x₀ ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ))
Tactic: rw [← div_le_iff₀ x₀_pos]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain :
  ∀ (m : ℕ) (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) * x₀) →
        f z = 0
⊢ x / x₀ ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ))
have refine : logb 2 (x / x₀) ≤ logb 2 (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)))
Tactic: refine (logb_le_logb (b := 2) (by norm_num) (by positivity)
      (zpow_pos (by norm_num) _)).mp ?_
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain :
  ∀ (m : ℕ) (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) * x₀) →
        f z = 0
⊢ logb 2 (x / x₀) ≤ logb 2 (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)))
have rw : -(↑(-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) : ℝ) ≤ -logb 2 (x / x₀)
Tactic: rw [← rpow_intCast, logb_rpow (by norm_num) (by norm_num), ← neg_le_neg_iff]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain :
  ∀ (m : ℕ) (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) * x₀) →
        f z = 0
⊢ -(↑(-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) : ℝ) ≤ -logb 2 (x / x₀)
have simp : (↑⌊-logb 2 (x / x₀)⌋₊ : ℝ) ≤ -logb 2 (x / x₀)
Tactic: simp only [Int.cast_neg, Int.cast_natCast, neg_neg]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain :
  ∀ (m : ℕ) (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) * x₀) →
        f z = 0
⊢ 0 ≤ -logb 2 (x / x₀)
have rw : logb 2 (x / x₀) ≤ 0
Tactic: rw [neg_nonneg]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain :
  ∀ (m : ℕ) (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) * x₀) →
        f z = 0
⊢ logb 2 (x / x₀) ≤ 0
have refine : x / x₀ ≤ 1
Tactic: refine logb_nonpos (by norm_num) (by positivity) ?_
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain :
  ∀ (m : ℕ) (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) * x₀) →
        f z = 0
⊢ x / x₀ ≤ 1
have rw : x ≤ x₀
Tactic: rw [div_le_one x₀_pos]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain :
  ∀ (m : ℕ) (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) * x₀) →
        f z = 0
⊢ (↑⌊-logb 2 (x / x₀)⌋₊ : ℝ) ≤ -logb 2 (x / x₀)
have this : 0 ≤ -logb 2 (x / x₀)
Tactic: have : 0 ≤ -logb 2 (x / x₀) := by
      rw [neg_nonneg]
      refine logb_nonpos (by norm_num) (by positivity) ?_
      rw [div_le_one x₀_pos]
      exact le_of_max_le_left hx₀_ge
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain :
  ∀ (m : ℕ) (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) * x₀) →
        f z = 0
⊢ x ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) * x₀
have case : x / x₀ ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ))
Tactic: case ub =>
    rw [← div_le_iff₀ x₀_pos]
    refine (logb_le_logb (b := 2) (by norm_num) (by positivity)
      (zpow_pos (by norm_num) _)).mp ?_
    rw [← rpow_intCast, logb_rpow (by norm_num) (by norm_num), ← neg_le_neg_iff]
    simp only [Int.cast_neg, Int.cast_natCast, neg_neg]
    have : 0 ≤ -logb 2 (x / x₀) := by
      rw [neg_nonneg]
      refine logb_nonpos (by norm_num) (by positivity) ?_
      rw [div_le_one x₀_pos]
      exact le_of_max_le_left hx₀_ge
    exact_mod_cast Nat.floor_le this
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain :
  ∀ (m : ℕ) (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) * x₀) →
        f z = 0
case case₁ case₂ : x / x₀ ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ))
⊢ x ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) * x₀
have case₃ : logb 2 (x / x₀) ≤ logb 2 (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)))
Tactic: case ub =>
    rw [← div_le_iff₀ x₀_pos]
    refine (logb_le_logb (b := 2) (by norm_num) (by positivity)
      (zpow_pos (by norm_num) _)).mp ?_
    rw [← rpow_intCast, logb_rpow (by norm_num) (by norm_num), ← neg_le_neg_iff]
    simp only [Int.cast_neg, Int.cast_natCast, neg_neg]
    have : 0 ≤ -logb 2 (x / x₀) := by
      rw [neg_nonneg]
      refine logb_nonpos (by norm_num) (by positivity) ?_
      rw [div_le_one x₀_pos]
      exact le_of_max_le_left hx₀_ge
    exact_mod_cast Nat.floor_le this
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain :
  ∀ (m : ℕ) (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) * x₀) →
        f z = 0
case case₁ case₂ : x / x₀ ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ))
case₃ : logb 2 (x / x₀) ≤ logb 2 (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)))
⊢ x ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) * x₀
have case₄ : -(↑(-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) : ℝ) ≤ -logb 2 (x / x₀)
Tactic: case ub =>
    rw [← div_le_iff₀ x₀_pos]
    refine (logb_le_logb (b := 2) (by norm_num) (by positivity)
      (zpow_pos (by norm_num) _)).mp ?_
    rw [← rpow_intCast, logb_rpow (by norm_num) (by norm_num), ← neg_le_neg_iff]
    simp only [Int.cast_neg, Int.cast_natCast, neg_neg]
    have : 0 ≤ -logb 2 (x / x₀) := by
      rw [neg_nonneg]
      refine logb_nonpos (by norm_num) (by positivity) ?_
      rw [div_le_one x₀_pos]
      exact le_of_max_le_left hx₀_ge
    exact_mod_cast Nat.floor_le this
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain :
  ∀ (m : ℕ) (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) * x₀) →
        f z = 0
case case₁ case₂ : x / x₀ ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ))
case₃ : logb 2 (x / x₀) ≤ logb 2 (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)))
case₄ : -(↑(-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) : ℝ) ≤ -logb 2 (x / x₀)
⊢ x ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) * x₀
have case₅ : (↑⌊-logb 2 (x / x₀)⌋₊ : ℝ) ≤ -logb 2 (x / x₀)
Tactic: case ub =>
    rw [← div_le_iff₀ x₀_pos]
    refine (logb_le_logb (b := 2) (by norm_num) (by positivity)
      (zpow_pos (by norm_num) _)).mp ?_
    rw [← rpow_intCast, logb_rpow (by norm_num) (by norm_num), ← neg_le_neg_iff]
    simp only [Int.cast_neg, Int.cast_natCast, neg_neg]
    have : 0 ≤ -logb 2 (x / x₀) := by
      rw [neg_nonneg]
      refine logb_nonpos (by norm_num) (by positivity) ?_
      rw [div_le_one x₀_pos]
      exact le_of_max_le_left hx₀_ge
    exact_mod_cast Nat.floor_le this
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain :
  ∀ (m : ℕ) (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) * x₀) →
        f z = 0
case case₁ case₂ : x / x₀ ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ))
case₃ : logb 2 (x / x₀) ≤ logb 2 (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)))
case₄ : -(↑(-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) : ℝ) ≤ -logb 2 (x / x₀)
case₅ : (↑⌊-logb 2 (x / x₀)⌋₊ : ℝ) ≤ -logb 2 (x / x₀)
⊢ x ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) * x₀
have case₆ : ∀ (this : 0 ≤ -logb 2 (x / x₀)), (↑⌊-logb 2 (x / x₀)⌋₊ : ℝ) ≤ -logb 2 (x / x₀)
Tactic: case ub =>
    rw [← div_le_iff₀ x₀_pos]
    refine (logb_le_logb (b := 2) (by norm_num) (by positivity)
      (zpow_pos (by norm_num) _)).mp ?_
    rw [← rpow_intCast, logb_rpow (by norm_num) (by norm_num), ← neg_le_neg_iff]
    simp only [Int.cast_neg, Int.cast_natCast, neg_neg]
    have : 0 ≤ -logb 2 (x / x₀) := by
      rw [neg_nonneg]
      refine logb_nonpos (by norm_num) (by positivity) ?_
      rw [div_le_one x₀_pos]
      exact le_of_max_le_left hx₀_ge
    exact_mod_cast Nat.floor_le this
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
⊢ (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
have obtain : ∀ c₁ > 0,
  ∀ c₂ > 0,
    ∀ (h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)),
      (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
Tactic: obtain ⟨c₁, _, c₂, _, h⟩ := hf (1 / 2) (by norm_num)
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
⊢ (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
have h₁ : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
Tactic: left
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
⊢ ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
have h₁ : ∀ (x : ℝ) (hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)) (hx_nonneg : 0 ≤ x), 0 ≤ f x
Tactic: filter_upwards [h, eventually_ge_atTop 0] with x hx hx_nonneg
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
⊢ 1 / 2 * x ≤ 3 / 4 * x
have hbc : 1 / 2 ≤ 3 / 4
Tactic: gcongr ?_ * x
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
⊢ 3 / 4 * x ≤ x
have linarith : x < 3 / 4 * x → 4 / 4 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
linarith : x < 3 / 4 * x → 4 / 4 = 1
⊢ 3 / 4 * x ≤ x
have linarith₁ : x < 3 / 4 * x → HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
linarith : x < 3 / 4 * x → 4 / 4 = 1
linarith₁ : x < 3 / 4 * x → HMul.hMul (α := ℝ) 1 4 = 4
⊢ 3 / 4 * x ≤ x
have linarith₂ : x < 3 / 4 * x → HMul.hMul (α := ℝ) 4 1 = 4
Tactic: linarith
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
linarith : x < 3 / 4 * x → 4 / 4 = 1
linarith₁ : x < 3 / 4 * x → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : x < 3 / 4 * x → HMul.hMul (α := ℝ) 4 1 = 4
⊢ 3 / 4 * x ≤ x
have linarith₃ : x < 3 / 4 * x → GT.gt (α := ℝ) 4 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
linarith : x < 3 / 4 * x → 4 / 4 = 1
linarith₁ : x < 3 / 4 * x → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : x < 3 / 4 * x → HMul.hMul (α := ℝ) 4 1 = 4
linarith₃ : x < 3 / 4 * x → GT.gt (α := ℝ) 4 0
⊢ 3 / 4 * x ≤ x
have linarith₄ : x < 3 / 4 * x → 0 - x + (4 * x - HMul.hMul (α := ℝ) 1 3 * (1 * x)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
⊢ 0 ≤ f x
have h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
Tactic: have h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x := by
      rw [Set.mem_Icc]
      exact ⟨by gcongr ?_ * x; norm_num, by linarith⟩
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
⊢ 0 ≤ f x
have hu : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
Tactic: have hu := hx (3 / 4 * x) h'
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ 0 ≤ f x
have hu₁ : (Set.Icc (c₁ * f x) (c₂ * f x)).Nonempty
Tactic: have hu := Set.nonempty_of_mem hu