awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
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|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)

Tactic:
have hf := hf.abs b hb
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hg : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hf :
  ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (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)
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (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)

Tactic:
have hg := hg.abs b hb
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hg_1 : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hf :
  ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (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)
hg :
  ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (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)
obtain :
  ∀ (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)),
    ∃ c₁ > 0,
      ∃ c₂ > 0,
        ∀ᶠ (x : ℝ) in atTop,
          ∀ u ∈ Set.Icc (b * x) x,
            (fun (x : ℝ) ↦ |f x| * |g x|) u ∈
              Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x| * |g x|) x) (c₂ * (fun (x : ℝ) ↦ |f x| * |g x|) x)
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun (x : ℝ) ↦ |f x| * |g x|) u ∈
            Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x| * |g x|) x) (c₂ * (fun (x : ℝ) ↦ |f x| * |g x|) x)

Tactic:
obtain ⟨c₁, hc₁_mem, c₂, hc₂_mem, hf⟩ := hf
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hg_1 : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hg :
  ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (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)
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)
obtain :
  ∀ (c₃ : ℝ) (hc₃_mem : c₃ > 0) (c₄ : ℝ) (hc₄_mem : c₄ > 0)
    (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)),
    ∃ c₁ > 0,
      ∃ c₂ > 0,
        ∀ᶠ (x : ℝ) in atTop,
          ∀ u ∈ Set.Icc (b * x) x,
            (fun (x : ℝ) ↦ |f x| * |g x|) u ∈
              Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x| * |g x|) x) (c₂ * (fun (x : ℝ) ↦ |f x| * |g x|) x)
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun (x : ℝ) ↦ |f x| * |g x|) u ∈
            Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x| * |g x|) x) (c₂ * (fun (x : ℝ) ↦ |f x| * |g x|) x)

Tactic:
obtain ⟨c₃, hc₃_mem, c₄, hc₄_mem, hg⟩ := hg
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hg_1 : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) 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)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
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)
⊢ 0 < c₁ * c₃

Tactic:
positivity
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hg_1 : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) 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)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
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)
refine :
  ∃ c₂ > 0,
    ∀ᶠ (x : ℝ) in atTop,
      ∀ u ∈ Set.Icc (b * x) x,
        (fun (x : ℝ) ↦ |f x| * |g x|) u ∈
          Set.Icc (c₁ * c₃ * (fun (x : ℝ) ↦ |f x| * |g x|) x) (c₂ * (fun (x : ℝ) ↦ |f x| * |g x|) x)
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun (x : ℝ) ↦ |f x| * |g x|) u ∈
            Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x| * |g x|) x) (c₂ * (fun (x : ℝ) ↦ |f x| * |g x|) x)

Tactic:
refine ⟨c₁ * c₃, by change 0 < c₁ * c₃; positivity, ?_⟩
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hg_1 : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) 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)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
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)
⊢ 0 < c₂ * c₄

Tactic:
positivity
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hg_1 : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) 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)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
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)
refine :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x| * |g x|) u ∈
        Set.Icc (c₁ * c₃ * (fun (x : ℝ) ↦ |f x| * |g x|) x) (c₂ * c₄ * (fun (x : ℝ) ↦ |f x| * |g x|) x)
⊢ ∃ c₂ > 0,
    ∀ᶠ (x : ℝ) in atTop,
      ∀ u ∈ Set.Icc (b * x) x,
        (fun (x : ℝ) ↦ |f x| * |g x|) u ∈
          Set.Icc (c₁ * c₃ * (fun (x : ℝ) ↦ |f x| * |g x|) x) (c₂ * (fun (x : ℝ) ↦ |f x| * |g x|) x)

Tactic:
refine ⟨c₂ * c₄, by change 0 < c₂ * c₄; positivity, ?_⟩
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hg_1 : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) 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)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
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 :
  ∀ (x : ℝ) (hf : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|))
    (hg : ∀ u ∈ Set.Icc (b * x) x, |g u| ∈ Set.Icc (c₃ * |g x|) (c₄ * |g x|)),
    ∀ u ∈ Set.Icc (b * x) x, |f u| * |g u| ∈ Set.Icc (c₁ * c₃ * (|f x| * |g x|)) (c₂ * c₄ * (|f x| * |g x|))
⊢ ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x| * |g x|) u ∈
        Set.Icc (c₁ * c₃ * (fun (x : ℝ) ↦ |f x| * |g x|) x) (c₂ * c₄ * (fun (x : ℝ) ↦ |f x| * |g x|) x)

Tactic:
filter_upwards [hf, hg] with x hf hg
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hg_1 : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf_2 :
  ∀ᶠ (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)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
hg_2 :
  ∀ᶠ (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)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hg : ∀ u ∈ Set.Icc (b * x) x, |g u| ∈ Set.Icc (c₃ * |g x|) (c₄ * |g x|)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ |f u| * |g u| ∈ Set.Icc (c₁ * c₃ * (|f x| * |g x|)) (c₂ * c₄ * (|f x| * |g x|))

Tactic:
⟨?lb, ?ub⟩

Premises used: Set.Mem, setOf, Set.Icc, And.intro
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hg_1 : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf_2 :
  ∀ᶠ (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)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
hg_2 :
  ∀ᶠ (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)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hg : ∀ u ∈ Set.Icc (b * x) x, |g u| ∈ Set.Icc (c₃ * |g x|) (c₄ * |g x|)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
refine : c₁ * c₃ * (|f x| * |g x|) ≤ |f u| * |g u|
refine₁ : |f u| * |g u| ≤ c₂ * c₄ * (|f x| * |g x|)
⊢ |f u| * |g u| ∈ Set.Icc (c₁ * c₃ * (|f x| * |g x|)) (c₂ * c₄ * (|f x| * |g x|))

Tactic:
refine ⟨?lb, ?ub⟩
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hg_1 : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf_2 :
  ∀ᶠ (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)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
hg_2 :
  ∀ᶠ (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)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hg : ∀ u ∈ Set.Icc (b * x) x, |g u| ∈ Set.Icc (c₃ * |g x|) (c₄ * |g x|)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ c₁ * c₃ * (|f x| * |g x|) = c₁ * |f x| * (c₃ * |g x|)

Tactic:
ring
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hg_1 : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf_2 :
  ∀ᶠ (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)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
hg_2 :
  ∀ᶠ (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)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hg : ∀ u ∈ Set.Icc (b * x) x, |g u| ∈ Set.Icc (c₃ * |g x|) (c₄ * |g x|)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h₁ : c₁ * |f x| ≤ |f u|
h₂ : c₃ * |g x| ≤ |g u|
⊢ c₁ * |f x| * (c₃ * |g x|) ≤ |f u| * |g u|

Tactic:
gcongr
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hg_1 : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf_2 :
  ∀ᶠ (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)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
hg_2 :
  ∀ᶠ (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)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hg : ∀ u ∈ Set.Icc (b * x) x, |g u| ∈ Set.Icc (c₃ * |g x|) (c₄ * |g x|)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ c₁ * |f x| ≤ |f u|

Tactic:
(hf u hu).1

Premises used: And.left
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hg_1 : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf_2 :
  ∀ᶠ (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)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
hg_2 :
  ∀ᶠ (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)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hg : ∀ u ∈ Set.Icc (b * x) x, |g u| ∈ Set.Icc (c₃ * |g x|) (c₄ * |g x|)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ c₁ * |f x| ≤ |f u|

Tactic:
exact (hf u hu).1

Premises used: And.left
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hg_1 : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf_2 :
  ∀ᶠ (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)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
hg_2 :
  ∀ᶠ (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)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hg : ∀ u ∈ Set.Icc (b * x) x, |g u| ∈ Set.Icc (c₃ * |g x|) (c₄ * |g x|)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ c₃ * |g x| ≤ |g u|

Tactic:
(hg u hu).1

Premises used: And.left
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hg_1 : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf_2 :
  ∀ᶠ (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)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
hg_2 :
  ∀ᶠ (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)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hg : ∀ u ∈ Set.Icc (b * x) x, |g u| ∈ Set.Icc (c₃ * |g x|) (c₄ * |g x|)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ c₃ * |g x| ≤ |g u|

Tactic:
exact (hg u hu).1

Premises used: And.left
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hg_1 : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf_2 :
  ∀ᶠ (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)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
hg_2 :
  ∀ᶠ (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)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hg : ∀ u ∈ Set.Icc (b * x) x, |g u| ∈ Set.Icc (c₃ * |g x|) (c₄ * |g x|)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
c₅ : c₁ * c₃ * (|f x| * |g x|) = c₁ * |f x| * (c₃ * |g x|)
c₆ : c₁ * |f x| * (c₃ * |g x|) ≤ |f u| * |g u|
⊢ c₁ * c₃ * (|f x| * |g x|) ≤ |f u| * |g u|

Tactic:
calc
    c₁ * c₃ * (|f x| * |g x|) = (c₁ * |f x|) * (c₃ * |g x|) := by ring
    _ ≤ |f u| * |g u| := by
           gcongr
           · exact (hf u hu).1
           · exact (hg u hu).1

Premises used: HMul.hMul, abs
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hg_1 : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf_2 :
  ∀ᶠ (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)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
hg_2 :
  ∀ᶠ (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)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hg : ∀ u ∈ Set.Icc (b * x) x, |g u| ∈ Set.Icc (c₃ * |g x|) (c₄ * |g x|)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ c₁ * c₃ * (|f x| * |g x|) ≤ |f u| * |g u|

Tactic:
case lb => calc
    c₁ * c₃ * (|f x| * |g x|) = (c₁ * |f x|) * (c₃ * |g x|) := by ring
    _ ≤ |f u| * |g u| := by
           gcongr
           · exact (hf u hu).1
           · exact (hg u hu).1

Premises used: HMul.hMul, abs
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hg_1 : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf_2 :
  ∀ᶠ (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)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
hg_2 :
  ∀ᶠ (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)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hg : ∀ u ∈ Set.Icc (b * x) x, |g u| ∈ Set.Icc (c₃ * |g x|) (c₄ * |g x|)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h₁ : |f u| ≤ c₂ * |f x|
h₂ : |g u| ≤ c₄ * |g x|
⊢ |f u| * |g u| ≤ c₂ * |f x| * (c₄ * |g x|)

Tactic:
gcongr
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hg_1 : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf_2 :
  ∀ᶠ (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)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
hg_2 :
  ∀ᶠ (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)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hg : ∀ u ∈ Set.Icc (b * x) x, |g u| ∈ Set.Icc (c₃ * |g x|) (c₄ * |g x|)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ |f u| ≤ c₂ * |f x|

Tactic:
(hf u hu).2

Premises used: And.right
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hg_1 : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf_2 :
  ∀ᶠ (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)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
hg_2 :
  ∀ᶠ (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)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hg : ∀ u ∈ Set.Icc (b * x) x, |g u| ∈ Set.Icc (c₃ * |g x|) (c₄ * |g x|)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ |f u| ≤ c₂ * |f x|

Tactic:
exact (hf u hu).2

Premises used: And.right
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hg_1 : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf_2 :
  ∀ᶠ (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)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
hg_2 :
  ∀ᶠ (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)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hg : ∀ u ∈ Set.Icc (b * x) x, |g u| ∈ Set.Icc (c₃ * |g x|) (c₄ * |g x|)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ |g u| ≤ c₄ * |g x|

Tactic:
(hg u hu).2

Premises used: And.right
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hg_1 : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf_2 :
  ∀ᶠ (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)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
hg_2 :
  ∀ᶠ (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)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hg : ∀ u ∈ Set.Icc (b * x) x, |g u| ∈ Set.Icc (c₃ * |g x|) (c₄ * |g x|)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ |g u| ≤ c₄ * |g x|

Tactic:
exact (hg u hu).2

Premises used: And.right
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hg_1 : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf_2 :
  ∀ᶠ (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)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
hg_2 :
  ∀ᶠ (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)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hg : ∀ u ∈ Set.Icc (b * x) x, |g u| ∈ Set.Icc (c₃ * |g x|) (c₄ * |g x|)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ c₂ * |f x| * (c₄ * |g x|) = c₂ * c₄ * (|f x| * |g x|)

Tactic:
ring
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hg_1 : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf_2 :
  ∀ᶠ (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)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
hg_2 :
  ∀ᶠ (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)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hg : ∀ u ∈ Set.Icc (b * x) x, |g u| ∈ Set.Icc (c₃ * |g x|) (c₄ * |g x|)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
exact : |f u| * |g u| ≤ c₂ * |f x| * (c₄ * |g x|)
exact₁ : c₂ * |f x| * (c₄ * |g x|) = c₂ * c₄ * (|f x| * |g x|)
⊢ |f u| * |g u| ≤ c₂ * c₄ * (|f x| * |g x|)

Tactic:
calc
    |f u| * |g u| ≤ (c₂ * |f x|) * (c₄ * |g x|) := by
           gcongr
           · exact (hf u hu).2
           · exact (hg u hu).2
    _ = c₂ * c₄ * (|f x| * |g x|) := by ring

Premises used: HMul.hMul, abs