awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f g : ℝ → ℝ
hfg : f =ᶠ[atTop] g
hg : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hg' : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)
x : ℝ
hx₁ : ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)
hx₂ : ∀ (y : ℝ), b * id x ≤ y → f y = g y
hx₃ : f x = g x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
have h : g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)
Tactic: rw [hx₂ u hu.1, hx₃]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hf : GrowsPolynomially f
⊢ ∃ c > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ≤ c * f x
have obtain : ∀ c₁ > 0,
  ∀ (c₂ : ℝ) (hc₂ : c₂ > 0) (h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)),
    ∃ c > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ≤ c * f x
Tactic: obtain ⟨c₁, _, c₂, hc₂, h⟩ := hf b hb
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
hc₂ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∃ c > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ≤ c * f x
have refine : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ≤ c₂ * f x
Tactic: refine ⟨c₂, hc₂, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
hc₂ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ≤ c₂ * f x
have h₁ : ∀ (a : ℝ), (∀ u ∈ Set.Icc (b * a) a, f u ∈ Set.Icc (c₁ * f a) (c₂ * f a)) → ∀ u ∈ Set.Icc (b * a) a, f u ≤ c₂ * f a
Tactic: filter_upwards [h]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hf : GrowsPolynomially f
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * (↑n : ℝ)) (↑n : ℝ), f u ≤ c * f (↑n : ℝ)
have obtain : ∀ (c : ℝ) (hc_mem : c > 0) (hc : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ≤ c * f x),
  ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * (↑n : ℝ)) (↑n : ℝ), f u ≤ c * f (↑n : ℝ)
Tactic: obtain ⟨c, hc_mem, hc⟩ := hf.eventually_atTop_le hb
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hf : GrowsPolynomially f
⊢ ∃ c > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, c * f x ≤ f u
have obtain : ∀ (c₁ : ℝ) (hc₁ : c₁ > 0),
  ∀ c₂ > 0,
    ∀ (h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)),
      ∃ c > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, c * f x ≤ f u
Tactic: obtain ⟨c₁, hc₁, c₂, _, h⟩ := hf b hb
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hf : GrowsPolynomially f
c₁ : ℝ
hc₁ : c₁ > 0
c₂ : ℝ
left : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∃ c > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, c * f x ≤ f u
have refine : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, c₁ * f x ≤ f u
Tactic: refine ⟨c₁, hc₁, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hf : GrowsPolynomially f
c₁ : ℝ
hc₁ : c₁ > 0
c₂ : ℝ
left : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, c₁ * f x ≤ f u
have h₁ : ∀ (a : ℝ), (∀ u ∈ Set.Icc (b * a) a, f u ∈ Set.Icc (c₁ * f a) (c₂ * f a)) → ∀ u ∈ Set.Icc (b * a) a, c₁ * f a ≤ f u
Tactic: filter_upwards [h]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hf : GrowsPolynomially f
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * (↑n : ℝ)) (↑n : ℝ), c * f (↑n : ℝ) ≤ f u
have obtain : ∀ (c : ℝ) (hc_mem : c > 0) (hc : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, c * f x ≤ f u),
  ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * (↑n : ℝ)) (↑n : ℝ), c * f (↑n : ℝ) ≤ f u
Tactic: obtain ⟨c, hc_mem, hc⟩ := hf.eventually_atTop_ge hb
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∃ᶠ (x : ℝ) in atTop, f x = 0
⊢ ∀ᶠ (x : ℝ) in atTop, f x = 0
have obtain : ∀ (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 : ℝ) in atTop, f x = 0
Tactic: obtain ⟨c₁, hc₁_mem, c₂, hc₂_mem, hf⟩ := hf (1 / 2) (by norm_num)
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∃ᶠ (x : ℝ) in atTop, f x = 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 : ℝ) in atTop, f x = 0
have rw : ∀ (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 : ℝ) in atTop, f x = 0
Tactic: rw [frequently_atTop] at hf'
Cleared hypotheses: hf', c₁, hc₁_mem, c₂, hc₂_mem, hf
-- 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 : ℝ) in atTop, f x = 0
have h : ∀ (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),
  f x = 0
Tactic: filter_upwards [eventually_forall_ge_atTop.mpr hf, eventually_gt_atTop 0] with x hx hx_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
⊢ f x = 0
have h : ∀ (x₀ : ℝ) (hx₀_ge : x₀ ≥ max x 1) (hx₀ : f x₀ = 0), f x = 0
Tactic: obtain ⟨x₀, hx₀_ge, hx₀⟩ := hf' (max x 1)
-- 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
⊢ f x = 0
have x₀_pos : 0 < x₀
Tactic: have x₀_pos := calc
    0 < 1 := by norm_num
    _ ≤ x₀ := le_of_max_le_right 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₀
⊢ ∀ (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑0 : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑0 : ℤ)) * x₀) →
        f z = 0
have zero : ∀ (z : ℝ), x ≤ z → z ∈ Set.Icc (HPow.hPow (α := ℝ) (β := ℤ) 2 (-1) * x₀) x₀ → f z = 0
Tactic: simp only [CharP.cast_eq_zero, neg_zero, zero_sub, zpow_zero, one_mul] at *
-- 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₀
⊢ ∀ (z : ℝ), x ≤ z → z ∈ Set.Icc (HPow.hPow (α := ℝ) (β := ℤ) 2 (-1) * x₀) x₀ → f z = 0
have hx₁ : ∀ u ∈ Set.Icc (1 / 2 * x₀) x₀, f u ∈ Set.Icc (c₁ * f x₀) (c₂ * f x₀)
Tactic: specialize hx x₀ (le_of_max_le_left hx₀_ge)
Cleared hypotheses: hx
-- 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₀
hx : ∀ u ∈ Set.Icc (1 / 2 * x₀) x₀, f u ∈ Set.Icc (c₁ * f x₀) (c₂ * f x₀)
⊢ ∀ (z : ℝ), x ≤ z → z ∈ Set.Icc (HPow.hPow (α := ℝ) (β := ℤ) 2 (-1) * x₀) x₀ → f z = 0
have hx₁ : ∀ u ∈ Set.Icc (1 / 2 * x₀) x₀, f u = 0
Tactic: simp only [hx₀, 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₀
hx : ∀ u ∈ Set.Icc (1 / 2 * x₀) x₀, f u = 0
⊢ ∀ (z : ℝ), x ≤ z → z ∈ Set.Icc (HPow.hPow (α := ℝ) (β := ℤ) 2 (-1) * x₀) x₀ → f z = 0
have zero : ∀ (z : ℝ), x ≤ z → ∀ (hz : z ∈ Set.Icc (HPow.hPow (α := ℝ) (β := ℤ) 2 (-1) * x₀) x₀), z ∈ Set.Icc (1 / 2 * x₀) x₀
Tactic: refine fun z _ hz => hx _ ?_
-- 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₀
hx : ∀ u ∈ Set.Icc (1 / 2 * x₀) x₀, f u = 0
z : ℝ
h : x ≤ z
hz : z ∈ Set.Icc (HPow.hPow (α := ℝ) (β := ℤ) 2 (-1) * x₀) x₀
⊢ z ∈ Set.Icc (1 / 2 * x₀) x₀
have hz₁ : z ∈ Set.Icc (2⁻¹ * x₀) x₀
Tactic: simp only [zpow_neg, zpow_one] at hz
Cleared hypotheses: hz
-- 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₀
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 : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑(k + 1) : ℤ)) 1) * x₀)
      (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑(k + 1) : ℤ)) * x₀)
⊢ f z = 0
have hz₁ : z ∈
  Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
    (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
Tactic: simp only [Nat.cast_add, Nat.cast_one] at *
Cleared hypotheses: hz
-- 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₀
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 : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
⊢ z ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
have hz₁ : z ∈
  Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 - 1) * x₀)
    (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀)
Tactic: simp only [neg_add, ← sub_eq_add_neg] at hz
Cleared hypotheses: hz
-- 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₀
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 : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
⊢ x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
have calc : z ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
Tactic: calc x ≤ z := hxz
          _ ≤ _ := by simp only [neg_add, ← sub_eq_add_neg] at hz; exact hz.2
-- 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₀
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 : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
⊢ f z = 0
have hx' : x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
Tactic: 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
-- 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₀
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 : ℝ
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₀
⊢ 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 ∈
    Set.Icc (c₁ * f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
      (c₂ * f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
Tactic: specialize hx ((2 : ℝ) ^ (-(k : ℤ) - 1) * x₀) hx' z
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 : ℕ
ih :
  ∀ (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑k : ℤ)) * x₀) →
        f z = 0
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₀))
⊢ f z = 0
have specialize : HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀ ∈
  Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀)
    (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑k : ℤ)) * x₀)
Tactic: specialize ih ((2 : ℝ) ^ (-(k : ℤ) - 1) * x₀) hx' ?ineq
-- 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 : ℕ
ih :
  ∀ (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑k : ℤ)) * x₀) →
        f z = 0
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₀))
specialize :
  HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀ ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀)
      (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑k : ℤ)) * x₀)
⊢ f z = 0
have succ : ∀ (ih : f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) = 0), f z = 0
Tactic: specialize ih ((2 : ℝ) ^ (-(k : ℤ) - 1) * x₀) hx' ?ineq
Cleared hypotheses: ih
-- 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 : ℕ
ih :
  ∀ (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑k : ℤ)) * x₀) →
        f z = 0
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₀))
⊢ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀ ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀)
      (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑k : ℤ)) * x₀)
have rw : HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀ ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑k : ℤ)) * x₀
Tactic: rw [Set.left_mem_Icc]
-- 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 : ℕ
ih :
  ∀ (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑k : ℤ)) * x₀) →
        f z = 0
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₀))
⊢ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀ ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑k : ℤ)) * x₀
have hbc : LE.le (α := ℝ) 1 2
Tactic: gcongr
-- 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 : ℕ
ih :
  ∀ (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑k : ℤ)) * x₀) →
        f z = 0
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₀))
hbc : LE.le (α := ℝ) 1 2
⊢ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀ ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑k : ℤ)) * x₀
have hbc₁ : HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 ≤ -(↑k : ℤ)
Tactic: gcongr