awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf_2 : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h₁ : 0 < |f u|
⊢ c₂⁻¹ * |f x|⁻¹ ≤ |f u|⁻¹
have rw : (c₂ * |f x|)⁻¹ ≤ |f u|⁻¹
Tactic: rw [← mul_inv]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf_2 : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h₁ : 0 < |f u|
⊢ (c₂ * |f x|)⁻¹ ≤ |f u|⁻¹
have hba : |f u| ≤ c₂ * |f x|
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf_2 : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h₁ : 0 < |f u|
⊢ |f u|⁻¹ ≤ c₁⁻¹ * |f x|⁻¹
have rw : |f u|⁻¹ ≤ (c₁ * |f x|)⁻¹
Tactic: rw [← mul_inv]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf_2 : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h₁ : 0 < |f u|
⊢ |f u|⁻¹ ≤ (c₁ * |f x|)⁻¹
have hba : c₁ * |f x| ≤ |f u|
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf_2 : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h₁ : 0 < |f u|
⊢ |f u|⁻¹ ≤ c₁⁻¹ * |f x|⁻¹
have case : |f u|⁻¹ ≤ (c₁ * |f x|)⁻¹
Tactic: case ub =>
      rw [← mul_inv]
      gcongr
      exact (hx u hu).1
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf_2 : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h₁ : 0 < |f u|
case case₁ case₂ : |f u|⁻¹ ≤ (c₁ * |f x|)⁻¹
⊢ |f u|⁻¹ ≤ c₁⁻¹ * |f x|⁻¹
have hba : c₁ * |f x| ≤ |f u|
Tactic: case ub =>
      rw [← mul_inv]
      gcongr
      exact (hx u hu).1
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
⊢ GrowsPolynomially fun (x : ℝ) ↦ (f x)⁻¹
have x : (∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
Tactic: cases hf.eventually_atTop_zero_or_pos_or_neg with
  | inl hf' =>
    refine fun b hb => ⟨1, by simp, 1, by simp, ?_⟩
    have hb_pos := hb.1
    filter_upwards [hf', (tendsto_id.const_mul_atTop hb_pos).eventually_forall_ge_atTop hf']
      with x hx hx'
    intro u hu
    simp only [hx, inv_zero, mul_zero, Set.Icc_self, Set.mem_singleton_iff, hx' u hu.1]
  | inr hf_pos_or_neg =>
    suffices GrowsPolynomially fun x => |(f x)⁻¹| by
      cases hf_pos_or_neg with
      | inl hf' =>
        have hmain : (fun x => (f x)⁻¹) =ᶠ[atTop] fun x => |(f x)⁻¹| := by
          filter_upwards [hf'] with x hx₁
          rw [abs_of_nonneg (inv_nonneg_of_nonneg (le_of_lt hx₁))]
        rwa [iff_eventuallyEq hmain]
      | inr hf' =>
        have hmain : (fun x => (f x)⁻¹) =ᶠ[atTop] fun x => -|(f x)⁻¹| := by
          filter_upwards [hf'] with x hx₁
          simp [abs_of_nonpos (inv_nonpos.mpr (le_of_lt hx₁))]
        rw [iff_eventuallyEq hmain]
        exact this.neg
    have hf' : ∀ᶠ x in atTop, f x ≠ 0 := by
      cases hf_pos_or_neg with
      | inl H => filter_upwards [H] with _ hx; exact (ne_of_lt hx).symm
      | inr H => filter_upwards [H] with _ hx; exact (ne_of_gt hx).symm
    simp only [abs_inv]
    have hf := hf.abs
    intro b hb
    have hb_pos := hb.1
    obtain ⟨c₁, hc₁_mem, c₂, hc₂_mem, hf⟩ := hf b hb
    refine ⟨c₂⁻¹, by change 0 < c₂⁻¹; positivity, ?_⟩
    refine ⟨c₁⁻¹, by change 0 < c₁⁻¹; positivity, ?_⟩
    filter_upwards [hf, hf', (tendsto_id.const_mul_atTop hb_pos).eventually_forall_ge_atTop hf']
      with x hx hx' hx''
    intro u hu
    have h₁ : 0 < |f u| := by rw [abs_pos]; exact hx'' u hu.1
    refine ⟨?lb, ?ub⟩
    case lb =>
      rw [← mul_inv]
      gcongr
      exact (hx u hu).2
    case ub =>
      rw [← mul_inv]
      gcongr
      exact (hx u hu).1
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
⊢ Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ f x / g x) fun (x : ℝ) ↦ f x * (g x)⁻¹
have h : ∀ (x : ℝ), f x / g x = f x * (g x)⁻¹
Tactic: ext
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
x : ℝ
⊢ f x / g x = f x * (g x)⁻¹
have h : f x * (g x)⁻¹ = f x * (g x)⁻¹
Tactic: rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
⊢ GrowsPolynomially fun (x : ℝ) ↦ f x / g x
have this : Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ f x / g x) fun (x : ℝ) ↦ f x * (g x)⁻¹
Tactic: have : (fun x => f x / g x) = fun x => f x * (g x)⁻¹ := by ext; rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun (x : ℝ) ↦ f x ^ p) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ f x ^ p) x) (c₂ * (fun (x : ℝ) ↦ f x ^ p) x)
have obtain : ∀ (c₁ : ℝ) (hc₁_mem : 0 < c₁) (c₂ : ℝ) (hc₂_mem : c₂ > 0)
  (hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)),
  ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun (x : ℝ) ↦ f x ^ p) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ f x ^ p) x) (c₂ * (fun (x : ℝ) ↦ f x ^ p) x)
Tactic: obtain ⟨c₁, (hc₁_mem : 0 < c₁), c₂, hc₂_mem, hfnew⟩ := hf b hb
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun (x : ℝ) ↦ f x ^ p) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ f x ^ p) x) (c₂ * (fun (x : ℝ) ↦ f x ^ p) x)
have hc₁p : 0 < c₁ ^ p
Tactic: have hc₁p : 0 < c₁ ^ p := Real.rpow_pos_of_pos hc₁_mem _
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun (x : ℝ) ↦ f x ^ p) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ f x ^ p) x) (c₂ * (fun (x : ℝ) ↦ f x ^ p) x)
have hc₂p : 0 < c₂ ^ p
Tactic: have hc₂p : 0 < c₂ ^ p := Real.rpow_pos_of_pos hc₂_mem _
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun (x : ℝ) ↦ f x ^ p) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ f x ^ p) x) (c₂ * (fun (x : ℝ) ↦ f x ^ p) x)
have inl : ∃ c₂ > 0,
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ f x ^ p) u ∈ Set.Icc (c₁ ^ p * (fun (x : ℝ) ↦ f x ^ p) x) (c₂ * (fun (x : ℝ) ↦ f x ^ p) x)
Tactic: refine ⟨c₁^p, hc₁p, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
⊢ ∃ c₂ > 0,
    ∀ᶠ (x : ℝ) in atTop,
      ∀ u ∈ Set.Icc (b * x) x,
        (fun (x : ℝ) ↦ f x ^ p) u ∈ Set.Icc (c₁ ^ p * (fun (x : ℝ) ↦ f x ^ p) x) (c₂ * (fun (x : ℝ) ↦ f x ^ p) x)
have inl : ∀ᶠ (x : ℝ) in atTop,
  ∀ u ∈ Set.Icc (b * x) x,
    (fun (x : ℝ) ↦ f x ^ p) u ∈ Set.Icc (c₁ ^ p * (fun (x : ℝ) ↦ f x ^ p) x) (c₂ ^ p * (fun (x : ℝ) ↦ f x ^ p) x)
Tactic: refine ⟨c₂^p, hc₂p, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
⊢ ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ f x ^ p) u ∈ Set.Icc (c₁ ^ p * (fun (x : ℝ) ↦ f x ^ p) x) (c₂ ^ p * (fun (x : ℝ) ↦ f x ^ p) x)
have h : ∀ (x : ℝ),
  0 < x →
    ∀ (hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)) (hf_nonneg : 0 ≤ f x)
      (hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y),
      ∀ u ∈ Set.Icc (b * x) x, f u ^ p ∈ Set.Icc (c₁ ^ p * f x ^ p) (c₂ ^ p * f x ^ p)
Tactic: filter_upwards [eventually_gt_atTop 0, hfnew, hf_nonneg,
        (tendsto_id.const_mul_atTop hb.1).eventually_forall_ge_atTop hf_nonneg]
        with x _ hf₁ hf_nonneg hf_nonneg₂
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ f u ^ p ∈ Set.Icc (c₁ ^ p * f x ^ p) (c₂ ^ p * f x ^ p)
have fu_nonneg : 0 ≤ f u
Tactic: have fu_nonneg : 0 ≤ f u := hf_nonneg₂ u hu.1
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
⊢ f u ^ p ∈ Set.Icc (c₁ ^ p * f x ^ p) (c₂ ^ p * f x ^ p)
have refine : c₁ ^ p * f x ^ p ≤ f u ^ p
Tactic: refine ⟨?lb, ?ub⟩
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
refine : c₁ ^ p * f x ^ p ≤ f u ^ p
⊢ f u ^ p ∈ Set.Icc (c₁ ^ p * f x ^ p) (c₂ ^ p * f x ^ p)
have refine₁ : f u ^ p ≤ c₂ ^ p * f x ^ p
Tactic: refine ⟨?lb, ?ub⟩
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
⊢ c₁ ^ p * f x ^ p = (c₁ * f x) ^ p
have rw : c₁ ^ p * f x ^ p = c₁ ^ p * f x ^ p
Tactic: rw [mul_rpow (le_of_lt hc₁_mem) hf_nonneg]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
⊢ (c₁ * f x) ^ p ≤ f u ^ p
have h₁ : c₁ * f x ≤ f u
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
⊢ c₁ ^ p * f x ^ p ≤ f u ^ p
have c₃ : c₁ ^ p * f x ^ p = (c₁ * f x) ^ p
Tactic: calc
      c₁ ^ p * (f x) ^ p = (c₁ * f x) ^ p := by rw [mul_rpow (le_of_lt hc₁_mem) hf_nonneg]
        _ ≤ _ := by gcongr; exact (hf₁ u hu).1
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
c₃ : c₁ ^ p * f x ^ p = (c₁ * f x) ^ p
⊢ c₁ ^ p * f x ^ p ≤ f u ^ p
have c₄ : (c₁ * f x) ^ p ≤ f u ^ p
Tactic: calc
      c₁ ^ p * (f x) ^ p = (c₁ * f x) ^ p := by rw [mul_rpow (le_of_lt hc₁_mem) hf_nonneg]
        _ ≤ _ := by gcongr; exact (hf₁ u hu).1
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
⊢ f u ^ p ≤ (c₂ * f x) ^ p
have h₁ : f u ≤ c₂ * f x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
⊢ (c₂ * f x) ^ p = c₂ ^ p * f x ^ p
have rw : (c₂ * f x) ^ p = (c₂ * f x) ^ p
Tactic: rw [← mul_rpow (le_of_lt hc₂_mem) hf_nonneg]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
⊢ f u ^ p ≤ c₂ ^ p * f x ^ p
have p₁ : f u ^ p ≤ (c₂ * f x) ^ p
Tactic: calc
      (f u) ^ p ≤ (c₂ * f x) ^ p := by gcongr; exact (hf₁ u hu).2
        _ = _ := by rw [← mul_rpow (le_of_lt hc₂_mem) hf_nonneg]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
p₁ : f u ^ p ≤ (c₂ * f x) ^ p
⊢ f u ^ p ≤ c₂ ^ p * f x ^ p
have p₂ : (c₂ * f x) ^ p = c₂ ^ p * f x ^ p
Tactic: calc
      (f u) ^ p ≤ (c₂ * f x) ^ p := by gcongr; exact (hf₁ u hu).2
        _ = _ := by rw [← mul_rpow (le_of_lt hc₂_mem) hf_nonneg]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
⊢ f u ^ p ≤ c₂ ^ p * f x ^ p
have case : f u ^ p ≤ (c₂ * f x) ^ p
Tactic: case ub => calc
      (f u) ^ p ≤ (c₂ * f x) ^ p := by gcongr; exact (hf₁ u hu).2
        _ = _ := by rw [← mul_rpow (le_of_lt hc₂_mem) hf_nonneg]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
case : f u ^ p ≤ (c₂ * f x) ^ p
⊢ f u ^ p ≤ c₂ ^ p * f x ^ p
have case₁ : (c₂ * f x) ^ p = c₂ ^ p * f x ^ p
Tactic: case ub => calc
      (f u) ^ p ≤ (c₂ * f x) ^ p := by gcongr; exact (hf₁ u hu).2
        _ = _ := by rw [← mul_rpow (le_of_lt hc₂_mem) hf_nonneg]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
hp : p < 0
hzero : ∀ᶠ (x : ℝ) in atTop, f x = 0
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun (x : ℝ) ↦ f x ^ p) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ f x ^ p) x) (c₂ * (fun (x : ℝ) ↦ f x ^ p) x)
have refine : ∀ᶠ (x : ℝ) in atTop,
  ∀ u ∈ Set.Icc (b * x) x,
    (fun (x : ℝ) ↦ f x ^ p) u ∈
      Set.Icc (HMul.hMul (α := ℝ) 1 ((fun (x : ℝ) ↦ f x ^ p) x)) (HMul.hMul (α := ℝ) 1 ((fun (x : ℝ) ↦ f x ^ p) x))
Tactic: refine ⟨1, by norm_num, 1, by norm_num, ?_⟩