awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
k : ℕ
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
hx' : x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
hx :
  z ∈
      Set.Icc (1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) →
    f z ∈
      Set.Icc (c₁ * f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (c₂ * f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
ih : f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) = 0
⊢ f z = 0
have hx₁ : z ∈
    Set.Icc (1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
      (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) →
  f z = 0
Tactic: simp only [ih, mul_zero, Set.Icc_self, Set.mem_singleton_iff] at hx
Cleared hypotheses: hx
-- 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_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
k : ℕ
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
hx' : x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
ih : f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) = 0
hx :
  z ∈
      Set.Icc (1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) →
    f z = 0
⊢ f z = 0
have refine : 1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) ≤ z
Tactic: refine hx ⟨?lb₁, ?ub₁⟩
-- 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_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
k : ℕ
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
hx' : x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
ih : f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) = 0
hx :
  z ∈
      Set.Icc (1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) →
    f z = 0
refine : 1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) ≤ z
⊢ f z = 0
have refine₁ : z ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
Tactic: refine hx ⟨?lb₁, ?ub₁⟩
-- 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_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
k : ℕ
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
hx' : x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
ih : f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) = 0
hx :
  z ∈
      Set.Icc (1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) →
    f z = 0
⊢ 1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) ≤ z
have rw : HPow.hPow (α := ℝ) 2 (-1 + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀ ≤ z
Tactic: rw [one_div, ← zpow_neg_one, ← mul_assoc, ← zpow_add₀ (by norm_num)]
-- 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_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
k : ℕ
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
hx' : x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
ih : f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) = 0
hx :
  z ∈
      Set.Icc (1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) →
    f z = 0
⊢ HPow.hPow (α := ℝ) 2 (-1 + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀ ≤ z
have h₁ : -1 + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
Tactic: have h₁ : (-1 : ℤ) + (-k - 1) = -k - 2 := by ring
-- 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_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
k : ℕ
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
hx' : x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
ih : f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) = 0
hx :
  z ∈
      Set.Icc (1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) →
    f z = 0
h₁ : -1 + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
⊢ HPow.hPow (α := ℝ) 2 (-1 + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀ ≤ z
have h₂ : -HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
Tactic: have h₂ : -(k + (1 : ℤ)) - 1 = -k - 2 := by ring
-- 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_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
k : ℕ
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
hx' : x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
ih : f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) = 0
hx :
  z ∈
      Set.Icc (1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) →
    f z = 0
h₁ : -1 + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
h₂ : -HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
⊢ HPow.hPow (α := ℝ) 2 (-1 + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀ ≤ z
have rw : HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2) * x₀ ≤ z
Tactic: rw [h₁]
-- 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_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
k : ℕ
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
hx' : x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
ih : f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) = 0
hx :
  z ∈
      Set.Icc (1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) →
    f z = 0
h₁ : -1 + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
h₂ : -HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
⊢ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2) * x₀ ≤ z
have hz₁ : z ∈
  Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2) * x₀)
    (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
Tactic: rw [h₂] at hz
Cleared hypotheses: hz, hx', ih, hx, h₁, h₂
-- 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_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
k : ℕ
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
hx' : x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
ih : f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) = 0
hx :
  z ∈
      Set.Icc (1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) →
    f z = 0
⊢ z ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
have this : z ≤ HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀
Tactic: have := hz.2
-- 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_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
k : ℕ
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
hx' : x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
ih : f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) = 0
hx :
  z ∈
      Set.Icc (1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) →
    f z = 0
⊢ z ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
have case : ∀ (this : z ≤ HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀),
  z ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
Tactic: case ub₁ =>
        have := hz.2
        simp only [neg_add, ← sub_eq_add_neg] at this
        exact 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_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
k : ℕ
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
hx' : x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
ih : f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) = 0
hx :
  z ∈
      Set.Icc (1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) →
    f z = 0
case case₁ case₂ :
  ∀ (this : z ≤ HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀),
    z ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
⊢ z ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
have case₃ : ∀ (this : z ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀),
  z ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
Tactic: case ub₁ =>
        have := hz.2
        simp only [neg_add, ← sub_eq_add_neg] at this
        exact 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₀
m : ℕ
⊢ ∀ (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) * x₀) →
        f z = 0
have zero : ∀ (z : ℝ),
  x ≤ z →
    z ∈
        Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑0 : ℤ)) 1) * x₀)
          (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑0 : ℤ)) * x₀) →
      f z = 0
Tactic: induction m with
    | zero =>
      simp only [CharP.cast_eq_zero, neg_zero, zero_sub, zpow_zero, one_mul] at *
      specialize hx x₀ (le_of_max_le_left hx₀_ge)
      simp only [hx₀, mul_zero, Set.Icc_self, Set.mem_singleton_iff] at hx
      refine fun z _ hz => hx _ ?_
      simp only [zpow_neg, zpow_one] at hz
      simp only [one_div, hz]
    | succ k ih =>
      intro z hxz hz
      simp only [Nat.cast_add, Nat.cast_one] at *
      have hx' : x ≤ (2 : ℝ) ^ (-(k : ℤ) - 1) * x₀ := by
        calc x ≤ z := hxz
          _ ≤ _ := by simp only [neg_add, ← sub_eq_add_neg] at hz; exact hz.2
      specialize hx ((2 : ℝ) ^ (-(k : ℤ) - 1) * x₀) hx' z
      specialize ih ((2 : ℝ) ^ (-(k : ℤ) - 1) * x₀) hx' ?ineq
      case ineq =>
        rw [Set.left_mem_Icc]
        gcongr
        · norm_num
        · lia
      simp only [ih, mul_zero, Set.Icc_self, Set.mem_singleton_iff] at hx
      refine hx ⟨?lb₁, ?ub₁⟩
      case lb₁ =>
        rw [one_div, ← zpow_neg_one, ← mul_assoc, ← zpow_add₀ (by norm_num)]
        have h₁ : (-1 : ℤ) + (-k - 1) = -k - 2 := by ring
        have h₂ : -(k + (1 : ℤ)) - 1 = -k - 2 := by ring
        rw [h₁]
        rw [h₂] at hz
        exact hz.1
      case ub₁ =>
        have := hz.2
        simp only [neg_add, ← sub_eq_add_neg] at this
        exact this
Cleared hypotheses: m
-- 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₀
m : ℕ
zero :
  ∀ (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑0 : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑0 : ℤ)) * x₀) →
        f z = 0
⊢ ∀ (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) * x₀) →
        f z = 0
have succ : ∀ (k : ℕ)
  (ih :
    ∀ (z : ℝ),
      x ≤ z →
        z ∈
            Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀)
              (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑k : ℤ)) * x₀) →
          f z = 0)
  (z : ℝ),
  x ≤ z →
    z ∈
        Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑(k + 1) : ℤ)) 1) * x₀)
          (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑(k + 1) : ℤ)) * x₀) →
      f z = 0
Tactic: induction m with
    | zero =>
      simp only [CharP.cast_eq_zero, neg_zero, zero_sub, zpow_zero, one_mul] at *
      specialize hx x₀ (le_of_max_le_left hx₀_ge)
      simp only [hx₀, mul_zero, Set.Icc_self, Set.mem_singleton_iff] at hx
      refine fun z _ hz => hx _ ?_
      simp only [zpow_neg, zpow_one] at hz
      simp only [one_div, hz]
    | succ k ih =>
      intro z hxz hz
      simp only [Nat.cast_add, Nat.cast_one] at *
      have hx' : x ≤ (2 : ℝ) ^ (-(k : ℤ) - 1) * x₀ := by
        calc x ≤ z := hxz
          _ ≤ _ := by simp only [neg_add, ← sub_eq_add_neg] at hz; exact hz.2
      specialize hx ((2 : ℝ) ^ (-(k : ℤ) - 1) * x₀) hx' z
      specialize ih ((2 : ℝ) ^ (-(k : ℤ) - 1) * x₀) hx' ?ineq
      case ineq =>
        rw [Set.left_mem_Icc]
        gcongr
        · norm_num
        · lia
      simp only [ih, mul_zero, Set.Icc_self, Set.mem_singleton_iff] at hx
      refine hx ⟨?lb₁, ?ub₁⟩
      case lb₁ =>
        rw [one_div, ← zpow_neg_one, ← mul_assoc, ← zpow_add₀ (by norm_num)]
        have h₁ : (-1 : ℤ) + (-k - 1) = -k - 2 := by ring
        have h₂ : -(k + (1 : ℤ)) - 1 = -k - 2 := by ring
        rw [h₁]
        rw [h₂] at hz
        exact hz.1
      case ub₁ =>
        have := hz.2
        simp only [neg_add, ← sub_eq_add_neg] at this
        exact this
Cleared hypotheses: m
-- 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₀
⊢ f x = 0
have hmain : ∀ (m : ℕ) (z : ℝ),
  x ≤ z →
    z ∈
        Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * x₀)
          (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) * x₀) →
      f z = 0
Tactic: have hmain : ∀ (m : ℕ) (z : ℝ), x ≤ z →
      z ∈ Set.Icc ((2 : ℝ) ^ (-(m : ℤ) - 1) * x₀) ((2 : ℝ) ^ (-(m : ℤ)) * x₀) → f z = 0 := by
    intro m
    induction m with
    | zero =>
      simp only [CharP.cast_eq_zero, neg_zero, zero_sub, zpow_zero, one_mul] at *
      specialize hx x₀ (le_of_max_le_left hx₀_ge)
      simp only [hx₀, mul_zero, Set.Icc_self, Set.mem_singleton_iff] at hx
      refine fun z _ hz => hx _ ?_
      simp only [zpow_neg, zpow_one] at hz
      simp only [one_div, hz]
    | succ k ih =>
      intro z hxz hz
      simp only [Nat.cast_add, Nat.cast_one] at *
      have hx' : x ≤ (2 : ℝ) ^ (-(k : ℤ) - 1) * x₀ := by
        calc x ≤ z := hxz
          _ ≤ _ := by simp only [neg_add, ← sub_eq_add_neg] at hz; exact hz.2
      specialize hx ((2 : ℝ) ^ (-(k : ℤ) - 1) * x₀) hx' z
      specialize ih ((2 : ℝ) ^ (-(k : ℤ) - 1) * x₀) hx' ?ineq
      case ineq =>
        rw [Set.left_mem_Icc]
        gcongr
        · norm_num
        · lia
      simp only [ih, mul_zero, Set.Icc_self, Set.mem_singleton_iff] at hx
      refine hx ⟨?lb₁, ?ub₁⟩
      case lb₁ =>
        rw [one_div, ← zpow_neg_one, ← mul_assoc, ← zpow_add₀ (by norm_num)]
        have h₁ : (-1 : ℤ) + (-k - 1) = -k - 2 := by ring
        have h₂ : -(k + (1 : ℤ)) - 1 = -k - 2 := by ring
        rw [h₁]
        rw [h₂] at hz
        exact hz.1
      case ub₁ =>
        have := hz.2
        simp only [neg_add, ← sub_eq_add_neg] at this
        exact 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
⊢ f x = 0
have refine : HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) 1) * x₀ ≤ x
Tactic: refine hmain ⌊-logb 2 (x / x₀)⌋₊ x le_rfl ⟨?lb, ?ub⟩
-- 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
refine : HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) 1) * x₀ ≤ x
⊢ f x = 0
have refine₁ : x ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) * x₀
Tactic: refine hmain ⌊-logb 2 (x / x₀)⌋₊ x le_rfl ⟨?lb, ?ub⟩
-- 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
⊢ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) 1) * x₀ ≤ x
have rw : HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) 1) ≤ x / x₀
Tactic: rw [← le_div_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
⊢ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) 1) ≤ x / x₀
have refine : logb 2 (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) 1)) ≤ logb 2 (x / x₀)
Tactic: refine (logb_le_logb (b := 2) (by norm_num) (zpow_pos (by norm_num) _)
      (by positivity)).mp ?_