awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hu : (Set.Icc (c₁ * f x) (c₂ * f x)).Nonempty
⊢ 0 ≤ f x
have hu₁ : c₁ * f x ≤ c₂ * f x
Tactic: rw [Set.nonempty_Icc] at hu
Cleared hypotheses: hu
-- 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
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu_1 : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hu : c₁ * f x ≤ c₂ * f x
⊢ 0 ≤ (c₂ - c₁) * f x
have linarith : (c₂ - c₁) * f x < 0 → c₁ * f x - c₂ * f x + ((c₂ - c₁) * f x - 0) = 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
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu_1 : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hu : c₁ * f x ≤ c₂ * f x
⊢ 0 ≤ f x
have hu' : 0 ≤ (c₂ - c₁) * f x
Tactic: have hu' : 0 ≤ (c₂ - c₁) * f x := by 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
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu_1 : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hu : c₁ * f x ≤ c₂ * f x
hu' : 0 ≤ (c₂ - c₁) * f x
⊢ 0 < c₂ - c₁
have linarith : c₂ - c₁ ≤ 0 → c₁ - c₂ + (c₂ - c₁ - 0) = 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)
hgt : c₂ < c₁
⊢ (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
have h₁ : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
Tactic: right
-- 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)
hgt : c₂ < c₁
⊢ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
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), f x ≤ 0
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)
hgt : 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)
hgt : 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)
hgt : 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)
hgt : 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)
hgt : 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)
hgt : 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)
hgt : 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
⊢ f x ≤ 0
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)
hgt : 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
⊢ f x ≤ 0
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)
hgt : 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)
⊢ f x ≤ 0
have hu₁ : (Set.Icc (c₁ * f x) (c₂ * f x)).Nonempty
Tactic: have hu := Set.nonempty_of_mem hu
-- 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)
hgt : 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_1 : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hu : (Set.Icc (c₁ * f x) (c₂ * f x)).Nonempty
⊢ f x ≤ 0
have hu₁ : c₁ * f x ≤ c₂ * f x
Tactic: rw [Set.nonempty_Icc] at hu
Cleared hypotheses: hu
-- 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)
hgt : 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_1 : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hu : c₁ * f x ≤ c₂ * f x
⊢ (c₁ - c₂) * f x ≤ 0
have linarith : 0 < (c₁ - c₂) * f x → c₁ * f x - c₂ * f x + (0 - (c₁ - c₂) * f 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)
hgt : 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_1 : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hu : c₁ * f x ≤ c₂ * f x
⊢ f x ≤ 0
have hu' : (c₁ - c₂) * f x ≤ 0
Tactic: have hu' : (c₁ - c₂) * f x ≤ 0 := by 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)
hgt : 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_1 : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hu : c₁ * f x ≤ c₂ * f x
hu' : (c₁ - c₂) * f x ≤ 0
⊢ 0 < c₁ - c₂
have linarith : c₁ - c₂ ≤ 0 → c₂ - c₁ + (c₁ - c₂ - 0) = 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)
heq : c₁ = c₂
⊢ ∃ (c : ℝ), ∀ᶠ (x : ℝ) in atTop, f x = c
have h₁ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u = c₂ * f x
Tactic: simp only [heq, Set.Icc_self, Set.mem_singleton_iff] at h
Cleared hypotheses: 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
heq : c₁ = c₂
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u = c₂ * f x
⊢ ∃ (c : ℝ), ∀ᶠ (x : ℝ) in atTop, f x = c
have h₁ : ∃ (a : ℝ), ∀ b ≥ a, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
Tactic: rw [eventually_atTop] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
heq : c₁ = c₂
h : ∃ (a : ℝ), ∀ b ≥ a, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
⊢ ∃ (c : ℝ), ∀ᶠ (x : ℝ) in atTop, f x = c
have obtain : ∀ (n₀ : ℝ) (hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b), ∃ (c : ℝ), ∀ᶠ (x : ℝ) in atTop, f x = c
Tactic: obtain ⟨n₀, hn₀⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
⊢ ∃ (c : ℝ), ∀ᶠ (x : ℝ) in atTop, f x = c
have refine : ∀ᶠ (x : ℝ) in atTop, f x = f (max n₀ 2)
Tactic: refine ⟨f (max n₀ 2), ?_⟩
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
⊢ ∀ᶠ (x : ℝ) in atTop, f x = f (max n₀ 2)
have rw : ∃ (a : ℝ), ∀ b ≥ a, f b = f (max n₀ 2)
Tactic: rw [eventually_atTop]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
⊢ ∃ (a : ℝ), ∀ b ≥ a, f b = f (max n₀ 2)
have refine : ∀ b ≥ max n₀ 2, f b = f (max n₀ 2)
Tactic: refine ⟨max n₀ 2, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
⊢ ∀ b ≥ max n₀ 2, f b = f (max n₀ 2)
have refine : ∀ x ∈ Set.Ico (max n₀ 2) (2 * max n₀ 2), f x = f (max n₀ 2)
Tactic: refine Real.induction_Ico_mul _ 2 (by norm_num) (by positivity) ?base ?step
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
refine : ∀ x ∈ Set.Ico (max n₀ 2) (2 * max n₀ 2), f x = f (max n₀ 2)
⊢ ∀ b ≥ max n₀ 2, f b = f (max n₀ 2)
have refine₁ : ∀ n ≥ 1,
  (∀ z ∈ Set.Ico (max n₀ 2) (HPow.hPow (α := ℝ) 2 n * max n₀ 2), f z = f (max n₀ 2)) →
    ∀ z ∈ Set.Ico (HPow.hPow (α := ℝ) 2 n * max n₀ 2) (HPow.hPow (α := ℝ) 2 (n + 1) * max n₀ 2), f z = f (max n₀ 2)
Tactic: refine Real.induction_Ico_mul _ 2 (by norm_num) (by positivity) ?base ?step
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
n : ℕ
h : n ≥ 1
h_1 : ∀ z ∈ Set.Ico (max n₀ 2) (HPow.hPow (α := ℝ) 2 n * max n₀ 2), f z = f (max n₀ 2)
z : ℝ
h_2 : z ∈ Set.Ico (HPow.hPow (α := ℝ) 2 n * max n₀ 2) (HPow.hPow (α := ℝ) 2 (n + 1) * max n₀ 2)
⊢ f z = f (max n₀ 2)
have le_2n : max n₀ 2 ≤ HPow.hPow (α := ℝ) 2 n * max n₀ 2
Tactic: have le_2n : max n₀ 2 ≤ (2 : ℝ) ^ n * max n₀ 2 := by
          simp [one_le_pow₀ (show (1 : ℝ) ≤ 2 by norm_num1)]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
n : ℕ
h : n ≥ 1
h_1 : ∀ z ∈ Set.Ico (max n₀ 2) (HPow.hPow (α := ℝ) 2 n * max n₀ 2), f z = f (max n₀ 2)
z : ℝ
h_2 : z ∈ Set.Ico (HPow.hPow (α := ℝ) 2 n * max n₀ 2) (HPow.hPow (α := ℝ) 2 (n + 1) * max n₀ 2)
le_2n : max n₀ 2 ≤ HPow.hPow (α := ℝ) 2 n * max n₀ 2
⊢ f z = f (max n₀ 2)
have half_z_to_base : f (1 / 2 * z) = f (max n₀ 2)
Tactic: have half_z_to_base : f (1 / 2 * z) = f (max n₀ 2) := by
          grind [mul_assoc]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
case case₁ case₂ case₃ case₄ :
  ∀ n ≥ 1,
    (∀ z ∈ Set.Ico (max n₀ 2) (HPow.hPow (α := ℝ) 2 n * max n₀ 2), f z = f (max n₀ 2)) →
      ∀ z ∈ Set.Ico (HPow.hPow (α := ℝ) 2 n * max n₀ 2) (HPow.hPow (α := ℝ) 2 (n + 1) * max n₀ 2), f z = f (max n₀ 2)
⊢ ∀ n ≥ 1,
    (∀ z ∈ Set.Ico (max n₀ 2) (HPow.hPow (α := ℝ) 2 n * max n₀ 2), f z = f (max n₀ 2)) →
      ∀ z ∈ Set.Ico (HPow.hPow (α := ℝ) 2 n * max n₀ 2) (HPow.hPow (α := ℝ) 2 (n + 1) * max n₀ 2), f z = f (max n₀ 2)
have case₅ : ∀ n ≥ 1,
  (∀ z ∈ Set.Ico (max n₀ 2) (HPow.hPow (α := ℝ) 2 n * max n₀ 2), f z = f (max n₀ 2)) →
    ∀ z ∈ Set.Ico (HPow.hPow (α := ℝ) 2 n * max n₀ 2) (HPow.hPow (α := ℝ) 2 (n + 1) * max n₀ 2),
      ∀ (le_2n : max n₀ 2 ≤ HPow.hPow (α := ℝ) 2 n * max n₀ 2), f z = f (max n₀ 2)
Tactic: case step =>
        intro n _ _ z _
        have le_2n : max n₀ 2 ≤ (2 : ℝ) ^ n * max n₀ 2 := by
          simp [one_le_pow₀ (show (1 : ℝ) ≤ 2 by norm_num1)]
        have half_z_to_base : f (1 / 2 * z) = f (max n₀ 2) := by
          grind [mul_assoc]
        grind
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
case case₁ case₂ case₃ case₄ :
  ∀ n ≥ 1,
    (∀ z ∈ Set.Ico (max n₀ 2) (HPow.hPow (α := ℝ) 2 n * max n₀ 2), f z = f (max n₀ 2)) →
      ∀ z ∈ Set.Ico (HPow.hPow (α := ℝ) 2 n * max n₀ 2) (HPow.hPow (α := ℝ) 2 (n + 1) * max n₀ 2), f z = f (max n₀ 2)
case₅ :
  ∀ n ≥ 1,
    (∀ z ∈ Set.Ico (max n₀ 2) (HPow.hPow (α := ℝ) 2 n * max n₀ 2), f z = f (max n₀ 2)) →
      ∀ z ∈ Set.Ico (HPow.hPow (α := ℝ) 2 n * max n₀ 2) (HPow.hPow (α := ℝ) 2 (n + 1) * max n₀ 2),
        ∀ (le_2n : max n₀ 2 ≤ HPow.hPow (α := ℝ) 2 n * max n₀ 2), f z = f (max n₀ 2)
⊢ ∀ n ≥ 1,
    (∀ z ∈ Set.Ico (max n₀ 2) (HPow.hPow (α := ℝ) 2 n * max n₀ 2), f z = f (max n₀ 2)) →
      ∀ z ∈ Set.Ico (HPow.hPow (α := ℝ) 2 n * max n₀ 2) (HPow.hPow (α := ℝ) 2 (n + 1) * max n₀ 2), f z = f (max n₀ 2)
have case₆ : ∀ n ≥ 1,
  (∀ z ∈ Set.Ico (max n₀ 2) (HPow.hPow (α := ℝ) 2 n * max n₀ 2), f z = f (max n₀ 2)) →
    ∀ z ∈ Set.Ico (HPow.hPow (α := ℝ) 2 n * max n₀ 2) (HPow.hPow (α := ℝ) 2 (n + 1) * max n₀ 2),
      ∀ (le_2n : max n₀ 2 ≤ HPow.hPow (α := ℝ) 2 n * max n₀ 2) (half_z_to_base : f (1 / 2 * z) = f (max n₀ 2)),
        f z = f (max n₀ 2)
Tactic: case step =>
        intro n _ _ z _
        have le_2n : max n₀ 2 ≤ (2 : ℝ) ^ n * max n₀ 2 := by
          simp [one_le_pow₀ (show (1 : ℝ) ≤ 2 by norm_num1)]
        have half_z_to_base : f (1 / 2 * z) = f (max n₀ 2) := by
          grind [mul_assoc]
        grind
-- 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)
heq : c₁ = c₂
⊢ (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
have hmain : ∃ (c : ℝ), ∀ᶠ (x : ℝ) in atTop, f x = c
Tactic: have hmain : ∃ c, ∀ᶠ x in atTop, f x = c := by
      simp only [heq, Set.Icc_self, Set.mem_singleton_iff] at h
      rw [eventually_atTop] at h
      obtain ⟨n₀, hn₀⟩ := h
      refine ⟨f (max n₀ 2), ?_⟩
      rw [eventually_atTop]
      refine ⟨max n₀ 2, ?_⟩
      refine Real.induction_Ico_mul _ 2 (by norm_num) (by positivity) ?base ?step
      case base => grind
      case step =>
        intro n _ _ z _
        have le_2n : max n₀ 2 ≤ (2 : ℝ) ^ n * max n₀ 2 := by
          simp [one_le_pow₀ (show (1 : ℝ) ≤ 2 by norm_num1)]
        have half_z_to_base : f (1 / 2 * z) = f (max n₀ 2) := by
          grind [mul_assoc]
        grind
-- 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)
heq : c₁ = c₂
hmain : ∃ (c : ℝ), ∀ᶠ (x : ℝ) in atTop, f x = c
⊢ (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
have obtain : ∀ (c : ℝ) (hc : ∀ᶠ (x : ℝ) in atTop, f x = c), (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
Tactic: obtain ⟨c, hc⟩ := hmain
Cleared hypotheses: hmain
-- 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)
heq : c₁ = c₂
c : ℝ
hc : ∀ᶠ (x : ℝ) in atTop, f x = c
hpos : 0 ≤ c
⊢ ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
have h₁ : ∀ (a : ℝ) (hc : f a = c), 0 ≤ f a
Tactic: filter_upwards [hc] with _ hc
-- 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)
heq : c₁ = c₂
c : ℝ
hc : ∀ᶠ (x : ℝ) in atTop, f x = c
hneg : c < 0
⊢ (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
have inr : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
Tactic: right
-- 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)
heq : c₁ = c₂
c : ℝ
hc : ∀ᶠ (x : ℝ) in atTop, f x = c
hneg : c < 0
⊢ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
have h₁ : ∀ (x : ℝ) (hc : f x = c), f x ≤ 0
Tactic: filter_upwards [hc] with x hc
-- 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)
heq : c₁ = c₂
c : ℝ
hc : ∀ᶠ (x : ℝ) in atTop, f x = c
⊢ (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
have x : 0 ≤ c ∨ c < 0
Tactic: cases le_or_gt 0 c with
    | inl hpos =>
      exact Or.inl <| by filter_upwards [hc] with _ hc; simpa only [hc]
    | inr hneg =>
      right
      filter_upwards [hc] with x hc
      exact le_of_lt <| by simpa only [hc]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
⊢ (∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
have pos : ∀ (h : ∃ᶠ (x : ℝ) in atTop, f x = 0),
  (∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
Tactic: by_cases! h : ∃ᶠ x in atTop, f x = 0
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
pos :
  ∀ (h : ∃ᶠ (x : ℝ) in atTop, f x = 0),
    (∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
⊢ (∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
have neg : ∀ (h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0),
  (∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
Tactic: by_cases! h : ∃ᶠ x in atTop, f x = 0
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ (∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
have neg : ∀ᶠ (x : ℝ) in atTop, 0 < f x
Tactic: refine Or.inr (Or.inl ?_)
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ ∀ᶠ (x : ℝ) in atTop, 0 < f x
have neg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x ∧ 0 ≠ f x
Tactic: simp only [lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x ∧ 0 ≠ f x
have neg : (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∧ ∀ᶠ (x : ℝ) in atTop, 0 ≠ f x
Tactic: rw [eventually_and]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ ∀ᶠ (x : ℝ) in atTop, 0 ≠ f x
have h₁ : ∀ (x : ℝ) (hx : f x ≠ 0), 0 ≠ f x
Tactic: filter_upwards [h] with x hx