-- Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean
protected lemma GrowsPolynomially.inv {f : ℝ → ℝ} (hf : GrowsPolynomially f) :
    GrowsPolynomially fun x => (f x)⁻¹

Proof state:
case h
f : ℝ → ℝ
hf✝¹ : 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✝ : GrowsPolynomially fun x => |f x|
b : ℝ
hb : b ∈ Set.Ioo 0 1
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|⁻¹ ∈ Set.Icc (c₂⁻¹ * |f x|⁻¹) (c₁⁻¹ * |f x|⁻¹)

Tactic:
refine ⟨?lb, ?ub⟩

Result:
case lb
f : ℝ → ℝ
hf✝¹ : 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✝ : GrowsPolynomially fun x => |f x|
b : ℝ
hb : b ∈ Set.Ioo 0 1
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|⁻¹

case ub
f : ℝ → ℝ
hf✝¹ : 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✝ : GrowsPolynomially fun x => |f x|
b : ℝ
hb : b ∈ Set.Ioo 0 1
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|⁻¹

Proof state:
f : ℝ → ℝ
hf✝¹ : 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✝ : GrowsPolynomially fun x => |f x|
b : ℝ
hb : b ∈ Set.Ioo 0 1
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)
⊢ c₂⁻¹ > 0

Tactic:
show 0 < c₂⁻¹

Result:
f : ℝ → ℝ
hf✝¹ : 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✝ : GrowsPolynomially fun x => |f x|
b : ℝ
hb : b ∈ Set.Ioo 0 1
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)
⊢ 0 < c₂⁻¹

Proof state:
case inl
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x = 0
⊢ GrowsPolynomially fun x => (f x)⁻¹

Tactic:
refine fun b hb => ⟨1, by simp, 1, by simp, ?_⟩

Result:
case inl
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x = 0
b : ℝ
hb : b ∈ Set.Ioo 0 1
⊢ ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x => (f x)⁻¹) u ∈ Set.Icc (1 * (fun x => (f x)⁻¹) x) (1 * (fun x => (f x)⁻¹) x)

Proof state:
case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
this : GrowsPolynomially fun x => |(f x)⁻¹|
hf' : ∀ᶠ (x : ℝ) in atTop, f x < 0
hmain : (fun x => (f x)⁻¹) =ᶠ[atTop] fun x => -|(f x)⁻¹|
⊢ GrowsPolynomially fun x => -|(f x)⁻¹|

Tactic:
exact this.neg

Result:
no goals

Proof state:
case inr
f : ℝ → ℝ
hf : 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
⊢ GrowsPolynomially fun x => |(f x)⁻¹|

Tactic:
simp only [abs_inv]

Result:
case inr
f : ℝ → ℝ
hf : 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
⊢ GrowsPolynomially fun x => |f x|⁻¹

Proof state:
case inr.intro.intro.intro.intro
f : ℝ → ℝ
hf✝¹ : 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✝ : GrowsPolynomially fun x => |f x|
b : ℝ
hb : b ∈ Set.Ioo 0 1
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 : ℝ) 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:
filter_upwards [hf, hf', (tendsto_id.const_mul_atTop hb_pos).eventually_forall_ge_atTop hf']
  with x hx hx' hx''

Result:
case h
f : ℝ → ℝ
hf✝¹ : 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✝ : GrowsPolynomially fun x => |f x|
b : ℝ
hb : b ∈ Set.Ioo 0 1
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 ∈ Set.Icc (b * x) x, |f u|⁻¹ ∈ Set.Icc (c₂⁻¹ * |f x|⁻¹) (c₁⁻¹ * |f x|⁻¹)

Proof state:
case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
this : GrowsPolynomially fun x => |(f x)⁻¹|
hf' : ∀ᶠ (x : ℝ) in atTop, f x < 0
hmain : (fun x => (f x)⁻¹) =ᶠ[atTop] fun x => -|(f x)⁻¹|
⊢ GrowsPolynomially fun x => (f x)⁻¹

Tactic:
rw [iff_eventuallyEq hmain]

Result:
case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
this : GrowsPolynomially fun x => |(f x)⁻¹|
hf' : ∀ᶠ (x : ℝ) in atTop, f x < 0
hmain : (fun x => (f x)⁻¹) =ᶠ[atTop] fun x => -|(f x)⁻¹|
⊢ GrowsPolynomially fun x => -|(f x)⁻¹|

Proof state:
case h
f : ℝ → ℝ
hf : GrowsPolynomially f
H : ∀ᶠ (x : ℝ) in atTop, 0 < f x
a✝ : ℝ
hx : 0 < f a✝
⊢ f a✝ ≠ 0

Tactic:
exact (ne_of_lt hx).symm

Result:
no goals

Proof state:
case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
this : GrowsPolynomially fun x => |(f x)⁻¹|
hf' : ∀ᶠ (x : ℝ) in atTop, f x < 0
⊢ GrowsPolynomially fun x => (f x)⁻¹

Tactic:
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₁))]

Result:
case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
this : GrowsPolynomially fun x => |(f x)⁻¹|
hf' : ∀ᶠ (x : ℝ) in atTop, f x < 0
hmain : (fun x => (f x)⁻¹) =ᶠ[atTop] fun x => -|(f x)⁻¹|
⊢ GrowsPolynomially fun x => (f x)⁻¹