awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f g : ℝ → ℝ
hg_1 : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ ‖g x‖) u ∈ Set.Icc (c₃ * (fun (x : ℝ) ↦ ‖g x‖) x) (c₄ * (fun (x : ℝ) ↦ ‖g x‖) x)
h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃
h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹
c₂_cancel : c₂⁻¹ * c₂ = 1
c₁_cancel : c₁⁻¹ * c₁ = 1
x : ℝ
hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖
h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖
hg_bound_1 : ∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hbx : b * x ≤ x
hg_bound : ∀ u ∈ Set.Icc (b * x) x, ‖g u‖ ∈ Set.Icc (c₃ * ‖g x‖) (c₄ * ‖g x‖)
⊢ f u ≤ c₂ * c₄ * c₁⁻¹ * f x
have f₁ : f u ≤ c₂ * ‖g u‖
Tactic: calc
    f u ≤ c₂ * ‖g u‖ := by rw [← Real.norm_of_nonneg (hf_pos u hu.1)]; exact h_ub u hu.1
      _ ≤ c₂ * (c₄ * ‖g x‖) := by gcongr; exact (hg_bound u hu).2
      _ = c₂ * c₄ * (c₁⁻¹ * c₁) * ‖g x‖ := by simp [c₁_cancel]; ring
      _ = c₂ * c₄ * c₁⁻¹ * (c₁ * ‖g x‖) := by ring
      _ ≤ c₂ * c₄ * c₁⁻¹ * f x := by
                gcongr
                rw [← Real.norm_of_nonneg (hf_pos x hbx)]
                exact h_lb x hbx
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f g : ℝ → ℝ
hg_1 : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ ‖g x‖) u ∈ Set.Icc (c₃ * (fun (x : ℝ) ↦ ‖g x‖) x) (c₄ * (fun (x : ℝ) ↦ ‖g x‖) x)
h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃
h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹
c₂_cancel : c₂⁻¹ * c₂ = 1
c₁_cancel : c₁⁻¹ * c₁ = 1
x : ℝ
hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖
h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖
hg_bound_1 : ∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hbx : b * x ≤ x
hg_bound : ∀ u ∈ Set.Icc (b * x) x, ‖g u‖ ∈ Set.Icc (c₃ * ‖g x‖) (c₄ * ‖g x‖)
f₁ : f u ≤ c₂ * ‖g u‖
⊢ f u ≤ c₂ * c₄ * c₁⁻¹ * f x
have f₂ : c₂ * ‖g u‖ ≤ c₂ * (c₄ * ‖g x‖)
Tactic: calc
    f u ≤ c₂ * ‖g u‖ := by rw [← Real.norm_of_nonneg (hf_pos u hu.1)]; exact h_ub u hu.1
      _ ≤ c₂ * (c₄ * ‖g x‖) := by gcongr; exact (hg_bound u hu).2
      _ = c₂ * c₄ * (c₁⁻¹ * c₁) * ‖g x‖ := by simp [c₁_cancel]; ring
      _ = c₂ * c₄ * c₁⁻¹ * (c₁ * ‖g x‖) := by ring
      _ ≤ c₂ * c₄ * c₁⁻¹ * f x := by
                gcongr
                rw [← Real.norm_of_nonneg (hf_pos x hbx)]
                exact h_lb x hbx
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f g : ℝ → ℝ
hg_1 : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ ‖g x‖) u ∈ Set.Icc (c₃ * (fun (x : ℝ) ↦ ‖g x‖) x) (c₄ * (fun (x : ℝ) ↦ ‖g x‖) x)
h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃
h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹
c₂_cancel : c₂⁻¹ * c₂ = 1
c₁_cancel : c₁⁻¹ * c₁ = 1
x : ℝ
hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖
h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖
hg_bound_1 : ∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hbx : b * x ≤ x
hg_bound : ∀ u ∈ Set.Icc (b * x) x, ‖g u‖ ∈ Set.Icc (c₃ * ‖g x‖) (c₄ * ‖g x‖)
f₁ : f u ≤ c₂ * ‖g u‖
f₂ : c₂ * ‖g u‖ ≤ c₂ * (c₄ * ‖g x‖)
⊢ f u ≤ c₂ * c₄ * c₁⁻¹ * f x
have f₃ : c₂ * (c₄ * ‖g x‖) = c₂ * c₄ * (c₁⁻¹ * c₁) * ‖g x‖
Tactic: calc
    f u ≤ c₂ * ‖g u‖ := by rw [← Real.norm_of_nonneg (hf_pos u hu.1)]; exact h_ub u hu.1
      _ ≤ c₂ * (c₄ * ‖g x‖) := by gcongr; exact (hg_bound u hu).2
      _ = c₂ * c₄ * (c₁⁻¹ * c₁) * ‖g x‖ := by simp [c₁_cancel]; ring
      _ = c₂ * c₄ * c₁⁻¹ * (c₁ * ‖g x‖) := by ring
      _ ≤ c₂ * c₄ * c₁⁻¹ * f x := by
                gcongr
                rw [← Real.norm_of_nonneg (hf_pos x hbx)]
                exact h_lb x hbx
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f g : ℝ → ℝ
hg_1 : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ ‖g x‖) u ∈ Set.Icc (c₃ * (fun (x : ℝ) ↦ ‖g x‖) x) (c₄ * (fun (x : ℝ) ↦ ‖g x‖) x)
h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃
h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹
c₂_cancel : c₂⁻¹ * c₂ = 1
c₁_cancel : c₁⁻¹ * c₁ = 1
x : ℝ
hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖
h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖
hg_bound_1 : ∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hbx : b * x ≤ x
hg_bound : ∀ u ∈ Set.Icc (b * x) x, ‖g u‖ ∈ Set.Icc (c₃ * ‖g x‖) (c₄ * ‖g x‖)
f₁ : f u ≤ c₂ * ‖g u‖
f₂ : c₂ * ‖g u‖ ≤ c₂ * (c₄ * ‖g x‖)
f₃ : c₂ * (c₄ * ‖g x‖) = c₂ * c₄ * (c₁⁻¹ * c₁) * ‖g x‖
⊢ f u ≤ c₂ * c₄ * c₁⁻¹ * f x
have f₄ : c₂ * c₄ * (c₁⁻¹ * c₁) * ‖g x‖ = c₂ * c₄ * c₁⁻¹ * (c₁ * ‖g x‖)
Tactic: calc
    f u ≤ c₂ * ‖g u‖ := by rw [← Real.norm_of_nonneg (hf_pos u hu.1)]; exact h_ub u hu.1
      _ ≤ c₂ * (c₄ * ‖g x‖) := by gcongr; exact (hg_bound u hu).2
      _ = c₂ * c₄ * (c₁⁻¹ * c₁) * ‖g x‖ := by simp [c₁_cancel]; ring
      _ = c₂ * c₄ * c₁⁻¹ * (c₁ * ‖g x‖) := by ring
      _ ≤ c₂ * c₄ * c₁⁻¹ * f x := by
                gcongr
                rw [← Real.norm_of_nonneg (hf_pos x hbx)]
                exact h_lb x hbx
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f g : ℝ → ℝ
hg_1 : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ ‖g x‖) u ∈ Set.Icc (c₃ * (fun (x : ℝ) ↦ ‖g x‖) x) (c₄ * (fun (x : ℝ) ↦ ‖g x‖) x)
h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃
h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹
c₂_cancel : c₂⁻¹ * c₂ = 1
c₁_cancel : c₁⁻¹ * c₁ = 1
x : ℝ
hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖
h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖
hg_bound_1 : ∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hbx : b * x ≤ x
hg_bound : ∀ u ∈ Set.Icc (b * x) x, ‖g u‖ ∈ Set.Icc (c₃ * ‖g x‖) (c₄ * ‖g x‖)
f₁ : f u ≤ c₂ * ‖g u‖
f₂ : c₂ * ‖g u‖ ≤ c₂ * (c₄ * ‖g x‖)
f₃ : c₂ * (c₄ * ‖g x‖) = c₂ * c₄ * (c₁⁻¹ * c₁) * ‖g x‖
f₄ : c₂ * c₄ * (c₁⁻¹ * c₁) * ‖g x‖ = c₂ * c₄ * c₁⁻¹ * (c₁ * ‖g x‖)
⊢ f u ≤ c₂ * c₄ * c₁⁻¹ * f x
have f₅ : c₂ * c₄ * c₁⁻¹ * (c₁ * ‖g x‖) ≤ c₂ * c₄ * c₁⁻¹ * f x
Tactic: calc
    f u ≤ c₂ * ‖g u‖ := by rw [← Real.norm_of_nonneg (hf_pos u hu.1)]; exact h_ub u hu.1
      _ ≤ c₂ * (c₄ * ‖g x‖) := by gcongr; exact (hg_bound u hu).2
      _ = c₂ * c₄ * (c₁⁻¹ * c₁) * ‖g x‖ := by simp [c₁_cancel]; ring
      _ = c₂ * c₄ * c₁⁻¹ * (c₁ * ‖g x‖) := by ring
      _ ≤ c₂ * c₄ * c₁⁻¹ * f x := by
                gcongr
                rw [← Real.norm_of_nonneg (hf_pos x hbx)]
                exact h_lb x hbx
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f g : ℝ → ℝ
hg_1 : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ ‖g x‖) u ∈ Set.Icc (c₃ * (fun (x : ℝ) ↦ ‖g x‖) x) (c₄ * (fun (x : ℝ) ↦ ‖g x‖) x)
h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃
h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹
c₂_cancel : c₂⁻¹ * c₂ = 1
c₁_cancel : c₁⁻¹ * c₁ = 1
x : ℝ
hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖
h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖
hg_bound_1 : ∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hbx : b * x ≤ x
hg_bound : ∀ u ∈ Set.Icc (b * x) x, ‖g u‖ ∈ Set.Icc (c₃ * ‖g x‖) (c₄ * ‖g x‖)
⊢ f u ≤ c₂ * c₄ * c₁⁻¹ * f x
have case : f u ≤ c₂ * ‖g u‖
Tactic: case ub => calc
    f u ≤ c₂ * ‖g u‖ := by rw [← Real.norm_of_nonneg (hf_pos u hu.1)]; exact h_ub u hu.1
      _ ≤ c₂ * (c₄ * ‖g x‖) := by gcongr; exact (hg_bound u hu).2
      _ = c₂ * c₄ * (c₁⁻¹ * c₁) * ‖g x‖ := by simp [c₁_cancel]; ring
      _ = c₂ * c₄ * c₁⁻¹ * (c₁ * ‖g x‖) := by ring
      _ ≤ c₂ * c₄ * c₁⁻¹ * f x := by
                gcongr
                rw [← Real.norm_of_nonneg (hf_pos x hbx)]
                exact h_lb x hbx
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f g : ℝ → ℝ
hg_1 : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ ‖g x‖) u ∈ Set.Icc (c₃ * (fun (x : ℝ) ↦ ‖g x‖) x) (c₄ * (fun (x : ℝ) ↦ ‖g x‖) x)
h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃
h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹
c₂_cancel : c₂⁻¹ * c₂ = 1
c₁_cancel : c₁⁻¹ * c₁ = 1
x : ℝ
hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖
h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖
hg_bound_1 : ∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hbx : b * x ≤ x
hg_bound : ∀ u ∈ Set.Icc (b * x) x, ‖g u‖ ∈ Set.Icc (c₃ * ‖g x‖) (c₄ * ‖g x‖)
case : f u ≤ c₂ * ‖g u‖
⊢ f u ≤ c₂ * c₄ * c₁⁻¹ * f x
have case₁ : c₂ * ‖g u‖ ≤ c₂ * (c₄ * ‖g x‖)
Tactic: case ub => calc
    f u ≤ c₂ * ‖g u‖ := by rw [← Real.norm_of_nonneg (hf_pos u hu.1)]; exact h_ub u hu.1
      _ ≤ c₂ * (c₄ * ‖g x‖) := by gcongr; exact (hg_bound u hu).2
      _ = c₂ * c₄ * (c₁⁻¹ * c₁) * ‖g x‖ := by simp [c₁_cancel]; ring
      _ = c₂ * c₄ * c₁⁻¹ * (c₁ * ‖g x‖) := by ring
      _ ≤ c₂ * c₄ * c₁⁻¹ * f x := by
                gcongr
                rw [← Real.norm_of_nonneg (hf_pos x hbx)]
                exact h_lb x hbx
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f g : ℝ → ℝ
hg_1 : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ ‖g x‖) u ∈ Set.Icc (c₃ * (fun (x : ℝ) ↦ ‖g x‖) x) (c₄ * (fun (x : ℝ) ↦ ‖g x‖) x)
h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃
h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹
c₂_cancel : c₂⁻¹ * c₂ = 1
c₁_cancel : c₁⁻¹ * c₁ = 1
x : ℝ
hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖
h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖
hg_bound_1 : ∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hbx : b * x ≤ x
hg_bound : ∀ u ∈ Set.Icc (b * x) x, ‖g u‖ ∈ Set.Icc (c₃ * ‖g x‖) (c₄ * ‖g x‖)
case : f u ≤ c₂ * ‖g u‖
case₁ : c₂ * ‖g u‖ ≤ c₂ * (c₄ * ‖g x‖)
⊢ f u ≤ c₂ * c₄ * c₁⁻¹ * f x
have case₂ : c₂ * (c₄ * ‖g x‖) = c₂ * c₄ * (c₁⁻¹ * c₁) * ‖g x‖
Tactic: case ub => calc
    f u ≤ c₂ * ‖g u‖ := by rw [← Real.norm_of_nonneg (hf_pos u hu.1)]; exact h_ub u hu.1
      _ ≤ c₂ * (c₄ * ‖g x‖) := by gcongr; exact (hg_bound u hu).2
      _ = c₂ * c₄ * (c₁⁻¹ * c₁) * ‖g x‖ := by simp [c₁_cancel]; ring
      _ = c₂ * c₄ * c₁⁻¹ * (c₁ * ‖g x‖) := by ring
      _ ≤ c₂ * c₄ * c₁⁻¹ * f x := by
                gcongr
                rw [← Real.norm_of_nonneg (hf_pos x hbx)]
                exact h_lb x hbx
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f g : ℝ → ℝ
hg_1 : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ ‖g x‖) u ∈ Set.Icc (c₃ * (fun (x : ℝ) ↦ ‖g x‖) x) (c₄ * (fun (x : ℝ) ↦ ‖g x‖) x)
h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃
h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹
c₂_cancel : c₂⁻¹ * c₂ = 1
c₁_cancel : c₁⁻¹ * c₁ = 1
x : ℝ
hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖
h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖
hg_bound_1 : ∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hbx : b * x ≤ x
hg_bound : ∀ u ∈ Set.Icc (b * x) x, ‖g u‖ ∈ Set.Icc (c₃ * ‖g x‖) (c₄ * ‖g x‖)
case : f u ≤ c₂ * ‖g u‖
case₁ : c₂ * ‖g u‖ ≤ c₂ * (c₄ * ‖g x‖)
case₂ : c₂ * (c₄ * ‖g x‖) = c₂ * c₄ * (c₁⁻¹ * c₁) * ‖g x‖
⊢ f u ≤ c₂ * c₄ * c₁⁻¹ * f x
have case₃ : c₂ * c₄ * (c₁⁻¹ * c₁) * ‖g x‖ = c₂ * c₄ * c₁⁻¹ * (c₁ * ‖g x‖)
Tactic: case ub => calc
    f u ≤ c₂ * ‖g u‖ := by rw [← Real.norm_of_nonneg (hf_pos u hu.1)]; exact h_ub u hu.1
      _ ≤ c₂ * (c₄ * ‖g x‖) := by gcongr; exact (hg_bound u hu).2
      _ = c₂ * c₄ * (c₁⁻¹ * c₁) * ‖g x‖ := by simp [c₁_cancel]; ring
      _ = c₂ * c₄ * c₁⁻¹ * (c₁ * ‖g x‖) := by ring
      _ ≤ c₂ * c₄ * c₁⁻¹ * f x := by
                gcongr
                rw [← Real.norm_of_nonneg (hf_pos x hbx)]
                exact h_lb x hbx
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f g : ℝ → ℝ
hg_1 : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ ‖g x‖) u ∈ Set.Icc (c₃ * (fun (x : ℝ) ↦ ‖g x‖) x) (c₄ * (fun (x : ℝ) ↦ ‖g x‖) x)
h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃
h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹
c₂_cancel : c₂⁻¹ * c₂ = 1
c₁_cancel : c₁⁻¹ * c₁ = 1
x : ℝ
hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖
h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖
hg_bound_1 : ∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hbx : b * x ≤ x
hg_bound : ∀ u ∈ Set.Icc (b * x) x, ‖g u‖ ∈ Set.Icc (c₃ * ‖g x‖) (c₄ * ‖g x‖)
case : f u ≤ c₂ * ‖g u‖
case₁ : c₂ * ‖g u‖ ≤ c₂ * (c₄ * ‖g x‖)
case₂ : c₂ * (c₄ * ‖g x‖) = c₂ * c₄ * (c₁⁻¹ * c₁) * ‖g x‖
case₃ : c₂ * c₄ * (c₁⁻¹ * c₁) * ‖g x‖ = c₂ * c₄ * c₁⁻¹ * (c₁ * ‖g x‖)
⊢ f u ≤ c₂ * c₄ * c₁⁻¹ * f x
have case₄ : c₂ * c₄ * c₁⁻¹ * (c₁ * ‖g x‖) ≤ c₂ * c₄ * c₁⁻¹ * f x
Tactic: case ub => calc
    f u ≤ c₂ * ‖g u‖ := by rw [← Real.norm_of_nonneg (hf_pos u hu.1)]; exact h_ub u hu.1
      _ ≤ c₂ * (c₄ * ‖g x‖) := by gcongr; exact (hg_bound u hu).2
      _ = c₂ * c₄ * (c₁⁻¹ * c₁) * ‖g x‖ := by simp [c₁_cancel]; ring
      _ = c₂ * c₄ * c₁⁻¹ * (c₁ * ‖g x‖) := by ring
      _ ≤ c₂ * c₄ * c₁⁻¹ * f x := by
                gcongr
                rw [← Real.norm_of_nonneg (hf_pos x hbx)]
                exact h_lb x hbx
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
⊢ f = g + (f - g)
have h : ∀ (x : ℝ), f x = (g + (f - g)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
Goal:
f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
⊢ GrowsPolynomially f
have this : f = g + (f - g)
Tactic: have : f = g + (f - g) := by ext; simp
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
this : f = g + (f - g)
⊢ GrowsPolynomially f
have rw : GrowsPolynomially (g + (f - g))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑n : ℝ) * (HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2)⁻¹) fun (n : ℕ) ↦
    HMul.hMul (α := ℝ) (↑n : ℝ) 1⁻¹
have refine : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2)⁻¹) fun (n : ℕ) ↦ 1⁻¹
Tactic: refine IsBigO.mul_isLittleO (isBigO_refl _ _) ?_
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2)⁻¹) fun (n : ℕ) ↦ 1⁻¹
have refine : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ 1) fun (n : ℕ) ↦ HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
Tactic: refine IsLittleO.inv_rev ?_ (by simp)
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ 1) fun (n : ℕ) ↦ HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
have _ : Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ 1) fun (x : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℕ) 1 2
Tactic: calc
        _ = (fun (_ : ℕ) => ((1 : ℝ) ^ 2)) := by simp
        _ =o[atTop] (fun (n : ℕ) => (log n) ^ 2) :=
          IsLittleO.pow (IsLittleO.natCast_atTop <| isLittleO_const_log_atTop) (by norm_num)
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
⊢ Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ) 1⁻¹) fun (n : ℕ) ↦ (↑n : ℝ)
have h : ∀ (x : ℕ), HMul.hMul (α := ℝ) (↑x : ℝ) 1⁻¹ = (↑x : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2) fun (n : ℕ) ↦
    (↑n : ℝ)
have calc : Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2) fun (n : ℕ) ↦
  (↑n : ℝ) * (HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2)⁻¹
Tactic: calc (fun (n : ℕ) => (n : ℝ) / log n ^ 2)
    _ = fun (n : ℕ) => (n : ℝ) * ((log n) ^ 2)⁻¹ := by simp_rw [div_eq_mul_inv]
    _ =o[atTop] fun (n : ℕ) => (n : ℝ) * 1⁻¹ := by
      refine IsBigO.mul_isLittleO (isBigO_refl _ _) ?_
      refine IsLittleO.inv_rev ?_ (by simp)
      calc
        _ = (fun (_ : ℕ) => ((1 : ℝ) ^ 2)) := by simp
        _ =o[atTop] (fun (n : ℕ) => (log n) ^ 2) :=
          IsLittleO.pow (IsLittleO.natCast_atTop <| isLittleO_const_log_atTop) (by norm_num)
    _ = (fun (n : ℕ) => (n : ℝ)) := by ext; simp
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
calc :
  Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2) fun (n : ℕ) ↦
    (↑n : ℝ) * (HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2)⁻¹
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2) fun (n : ℕ) ↦
    (↑n : ℝ)
have calc₁ : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑n : ℝ) * (HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2)⁻¹) fun (n : ℕ) ↦
  HMul.hMul (α := ℝ) (↑n : ℝ) 1⁻¹
Tactic: calc (fun (n : ℕ) => (n : ℝ) / log n ^ 2)
    _ = fun (n : ℕ) => (n : ℝ) * ((log n) ^ 2)⁻¹ := by simp_rw [div_eq_mul_inv]
    _ =o[atTop] fun (n : ℕ) => (n : ℝ) * 1⁻¹ := by
      refine IsBigO.mul_isLittleO (isBigO_refl _ _) ?_
      refine IsLittleO.inv_rev ?_ (by simp)
      calc
        _ = (fun (_ : ℕ) => ((1 : ℝ) ^ 2)) := by simp
        _ =o[atTop] (fun (n : ℕ) => (log n) ^ 2) :=
          IsLittleO.pow (IsLittleO.natCast_atTop <| isLittleO_const_log_atTop) (by norm_num)
    _ = (fun (n : ℕ) => (n : ℝ)) := by ext; simp
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
calc :
  Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2) fun (n : ℕ) ↦
    (↑n : ℝ) * (HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2)⁻¹
calc₁ :
  IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑n : ℝ) * (HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2)⁻¹) fun (n : ℕ) ↦
    HMul.hMul (α := ℝ) (↑n : ℝ) 1⁻¹
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2) fun (n : ℕ) ↦
    (↑n : ℝ)
have calc₂ : Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ) 1⁻¹) fun (n : ℕ) ↦ (↑n : ℝ)
Tactic: calc (fun (n : ℕ) => (n : ℝ) / log n ^ 2)
    _ = fun (n : ℕ) => (n : ℝ) * ((log n) ^ 2)⁻¹ := by simp_rw [div_eq_mul_inv]
    _ =o[atTop] fun (n : ℕ) => (n : ℝ) * 1⁻¹ := by
      refine IsBigO.mul_isLittleO (isBigO_refl _ _) ?_
      refine IsLittleO.inv_rev ?_ (by simp)
      calc
        _ = (fun (_ : ℕ) => ((1 : ℝ) ^ 2)) := by simp
        _ =o[atTop] (fun (n : ℕ) => (log n) ^ 2) :=
          IsLittleO.pow (IsLittleO.natCast_atTop <| isLittleO_const_log_atTop) (by norm_num)
    _ = (fun (n : ℕ) => (n : ℝ)) := by ext; simp
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
have rw : ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, ‖(↑(r i x) : ℝ) - b i * (↑x : ℝ)‖ ≤ (↑x : ℝ) / HPow.hPow (β := ℕ) (log (↑x : ℝ)) 2
Tactic: rw [Filter.eventually_all]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), b i * (↑n : ℝ) - (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2 ≤ (↑(r i n) : ℝ)
have h : ∀ (n : ℕ) (hn : ∀ (i : α), ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2) (i : α),
  b i * (↑n : ℝ) - (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2 ≤ (↑(r i n) : ℝ)
Tactic: filter_upwards [R.dist_r_b'] with n hn i
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : ∀ (i : α), ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
i : α
⊢ b i * (↑n : ℝ) - (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2 ≤ (↑(r i n) : ℝ)
have h₁ : 0 ≤ b i
Tactic: have h₁ : 0 ≤ b i := le_of_lt <| R.b_pos _