awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P) atTop atTop
this : 0 < P.degree ∧ 0 < P.leadingCoeff
⊢ 0 < P.degree ∧ 0 ≤ P.leadingCoeff

Tactic:
⟨this.1, this.2.le⟩

Premises used: LT.lt.le, And.right, And.left, And.intro
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P) atTop atTop
this : 0 < P.degree ∧ 0 < P.leadingCoeff
⊢ 0 < P.degree ∧ 0 ≤ P.leadingCoeff

Tactic:
exact ⟨this.1, this.2.le⟩
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P) atTop atBot ↔ 0 < P.degree ∧ P.leadingCoeff ≤ 0

Tactic:
simp only [← tendsto_neg_atTop_iff, ← eval_neg, tendsto_atTop_iff_leadingCoeff_nonneg,
    degree_neg, leadingCoeff_neg, neg_nonneg]

Premises used: Polynomial.tendsto_atTop_iff_leadingCoeff_nonneg, neg_nonneg, Polynomial.degree_neg, Polynomial.eval_neg, Filter.tendsto_neg_atTop_iff, Polynomial.leadingCoeff_neg
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : 0 < P.degree
hnps : P.leadingCoeff ≤ 0
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P) atTop atBot

Tactic:
P.tendsto_atBot_iff_leadingCoeff_nonpos.2 ⟨hdeg, hnps⟩

Premises used: Iff.mpr, Polynomial.tendsto_atBot_iff_leadingCoeff_nonpos, And.intro
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : 0 < P.degree
inl : ∀ (hP : 0 ≤ P.leadingCoeff), Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P|) atTop atTop
inr : ∀ (hP : P.leadingCoeff ≤ 0), Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P|) atTop atTop
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P|) atTop atTop

Tactic:
rcases le_total 0 P.leadingCoeff with hP | hP

Premises used: Polynomial.leadingCoeff, le_total, OfNat.ofNat
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : 0 < P.degree
hP : 0 ≤ P.leadingCoeff
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P|) atTop atTop

Tactic:
exact tendsto_abs_atTop_atTop.comp (P.tendsto_atTop_of_leadingCoeff_nonneg hdeg hP)

Premises used: Polynomial.tendsto_atTop_of_leadingCoeff_nonneg, Filter.Tendsto.comp, Filter.tendsto_abs_atTop_atTop
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : 0 < P.degree
hP : P.leadingCoeff ≤ 0
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P|) atTop atTop

Tactic:
tendsto_abs_atBot_atTop.comp (P.tendsto_atBot_of_leadingCoeff_nonpos hdeg hP)

Premises used: abs, Filter.tendsto_abs_atBot_atTop, Polynomial.tendsto_atBot_of_leadingCoeff_nonpos, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : 0 < P.degree
hP : P.leadingCoeff ≤ 0
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P|) atTop atTop

Tactic:
exact tendsto_abs_atBot_atTop.comp (P.tendsto_atBot_of_leadingCoeff_nonpos hdeg hP)

Premises used: Filter.tendsto_abs_atBot_atTop, Polynomial.tendsto_atBot_of_leadingCoeff_nonpos, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
⊢ (IsBoundedUnder (fun (x1 x2 : 𝕜) ↦ x1 ≤ x2) atTop fun (x : 𝕜) ↦ |eval x P|) ↔ P.degree ≤ 0

Tactic:
⟨fun h => ?_, fun h => ⟨|P.coeff 0|, eventually_map.mpr (Eventually.of_forall
    (forall_imp (fun _ => le_of_eq) fun x => congr_arg abs <| _root_.trans (congr_arg (eval x)
    (eq_C_of_degree_le_zero h)) eval_C))⟩⟩

Premises used: Iff.mpr, Polynomial.eval, trans, Polynomial.eval_C, abs, Filter.Eventually.of_forall, Filter.eventually_map, Polynomial.coeff, congr_arg, Polynomial.eq_C_of_degree_le_zero, forall_imp, Iff.intro, Exists.intro, le_of_eq, OfNat.ofNat
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
refine : ∀ (h : IsBoundedUnder (fun (x1 x2 : 𝕜) ↦ x1 ≤ x2) atTop fun (x : 𝕜) ↦ |eval x P|), P.degree ≤ 0
⊢ (IsBoundedUnder (fun (x1 x2 : 𝕜) ↦ x1 ≤ x2) atTop fun (x : 𝕜) ↦ |eval x P|) ↔ P.degree ≤ 0

Tactic:
refine ⟨fun h => ?_, fun h => ⟨|P.coeff 0|, eventually_map.mpr (Eventually.of_forall
    (forall_imp (fun _ => le_of_eq) fun x => congr_arg abs <| _root_.trans (congr_arg (eval x)
    (eq_C_of_degree_le_zero h)) eval_C))⟩⟩
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : IsBoundedUnder (fun (x1 x2 : 𝕜) ↦ x1 ≤ x2) atTop fun (x : 𝕜) ↦ |eval x P|
contrapose! : ∀ (h : 0 < P.degree), ¬IsBoundedUnder (fun (x1 x2 : 𝕜) ↦ x1 ≤ x2) atTop fun (x : 𝕜) ↦ |eval x P|
⊢ P.degree ≤ 0

Tactic:
contrapose! h
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : 0 < P.degree
⊢ ¬IsBoundedUnder (fun (x1 x2 : 𝕜) ↦ x1 ≤ x2) atTop fun (x : 𝕜) ↦ |eval x P|

Tactic:
not_isBoundedUnder_of_tendsto_atTop (abs_tendsto_atTop P h)

Premises used: Filter.not_isBoundedUnder_of_tendsto_atTop, Polynomial.abs_tendsto_atTop
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : 0 < P.degree
⊢ ¬IsBoundedUnder (fun (x1 x2 : 𝕜) ↦ x1 ≤ x2) atTop fun (x : 𝕜) ↦ |eval x P|

Tactic:
exact not_isBoundedUnder_of_tendsto_atTop (abs_tendsto_atTop P h)

Premises used: Filter.not_isBoundedUnder_of_tendsto_atTop, Polynomial.abs_tendsto_atTop
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P|) atTop atTop ↔ 0 < P.degree

Tactic:
⟨fun h ↦ not_le.mp (mt (isBoundedUnder_abs_atTop_iff P).mpr
    (not_isBoundedUnder_of_tendsto_atTop h)), abs_tendsto_atTop P⟩

Premises used: not_le, Iff.mpr, Filter.not_isBoundedUnder_of_tendsto_atTop, Polynomial.abs_tendsto_atTop, mt, Polynomial.isBoundedUnder_abs_atTop_iff, Iff.intro, Iff.mp
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
c : 𝕜
⊢ Tendsto (fun (x : 𝕜) ↦ eval x P) atTop (𝓝 c) ↔ P.leadingCoeff = c ∧ P.degree ≤ 0

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
c : 𝕜
refine_1 : ∀ (h : Tendsto (fun (x : 𝕜) ↦ eval x P) atTop (𝓝 c)), P.leadingCoeff = c ∧ P.degree ≤ 0
refine_2 : ∀ (h : P.leadingCoeff = c ∧ P.degree ≤ 0), Tendsto (fun (x : 𝕜) ↦ eval x P) atTop (𝓝 c)
⊢ Tendsto (fun (x : 𝕜) ↦ eval x P) atTop (𝓝 c) ↔ P.leadingCoeff = c ∧ P.degree ≤ 0

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun (x : 𝕜) ↦ eval x P) atTop (𝓝 c)
⊢ Tendsto (fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)

Tactic:
have := P.isEquivalent_atTop_lead.tendsto_nhds h
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun (x : 𝕜) ↦ eval x P) atTop (𝓝 c)
this : Tendsto (fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
pos : ∀ (hP : P.leadingCoeff = 0), P.leadingCoeff = c ∧ P.degree ≤ 0
neg : ∀ (hP : ¬P.leadingCoeff = 0), P.leadingCoeff = c ∧ P.degree ≤ 0
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0

Tactic:
by_cases hP : P.leadingCoeff = 0

Premises used: Polynomial.leadingCoeff
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun (x : 𝕜) ↦ eval x P) atTop (𝓝 c)
this : Tendsto (fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
hP : P.leadingCoeff = 0
⊢ 0 = c

Tactic:
simp only [hP, zero_mul, tendsto_const_nhds_iff] at this

Premises used: MulZeroClass.zero_mul, tendsto_const_nhds_iff
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun (x : 𝕜) ↦ eval x P) atTop (𝓝 c)
hP : P.leadingCoeff = 0
this : 0 = c
⊢ P.degree ≤ 0

Tactic:
simp [leadingCoeff_eq_zero.1 hP]

Premises used: Iff.mp, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun (x : 𝕜) ↦ eval x P) atTop (𝓝 c)
hP : P.leadingCoeff = 0
this : 0 = c
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0

Tactic:
exact ⟨_root_.trans hP this, by simp [leadingCoeff_eq_zero.1 hP]⟩
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun (x : 𝕜) ↦ eval x P) atTop (𝓝 c)
this : Tendsto (fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
hP : ¬P.leadingCoeff = 0
⊢ P.degree ≤ 0 ∧ P.leadingCoeff = c

Tactic:
rw [tendsto_const_mul_pow_nhds_iff hP, natDegree_eq_zero_iff_degree_le_zero] at this

Premises used: tendsto_const_mul_pow_nhds_iff, Polynomial.natDegree_eq_zero_iff_degree_le_zero
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun (x : 𝕜) ↦ eval x P) atTop (𝓝 c)
this : Tendsto (fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
hP : ¬P.leadingCoeff = 0
this₁ : P.degree ≤ 0 ∧ P.leadingCoeff = c
⊢ ¬P.leadingCoeff = 0

Tactic:
rw [tendsto_const_mul_pow_nhds_iff hP, natDegree_eq_zero_iff_degree_le_zero] at this

Premises used: tendsto_const_mul_pow_nhds_iff, Polynomial.natDegree_eq_zero_iff_degree_le_zero
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun (x : 𝕜) ↦ eval x P) atTop (𝓝 c)
this : P.degree ≤ 0 ∧ P.leadingCoeff = c
hP : ¬P.leadingCoeff = 0
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0

Tactic:
this.symm

Premises used: And.symm
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun (x : 𝕜) ↦ eval x P) atTop (𝓝 c)
this : P.degree ≤ 0 ∧ P.leadingCoeff = c
hP : ¬P.leadingCoeff = 0
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0

Tactic:
exact this.symm

Premises used: And.symm
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
c : 𝕜
h : P.leadingCoeff = c ∧ P.degree ≤ 0
⊢ Tendsto (fun (x : 𝕜) ↦ eval x P) atTop (𝓝 c)

Tactic:
P.isEquivalent_atTop_lead.symm.tendsto_nhds ?_

Premises used: Asymptotics.IsEquivalent.tendsto_nhds, Polynomial.isEquivalent_atTop_lead, Asymptotics.IsEquivalent.symm
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
c : 𝕜
h : P.leadingCoeff = c ∧ P.degree ≤ 0
refine_2 : Tendsto (fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
⊢ Tendsto (fun (x : 𝕜) ↦ eval x P) atTop (𝓝 c)

Tactic:
refine P.isEquivalent_atTop_lead.symm.tendsto_nhds ?_

Premises used: Asymptotics.IsEquivalent.tendsto_nhds, Polynomial.isEquivalent_atTop_lead, Asymptotics.IsEquivalent.symm
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
c : 𝕜
h : P.leadingCoeff = c ∧ P.degree ≤ 0
⊢ P.natDegree = 0

Tactic:
have : P.natDegree = 0 := natDegree_eq_zero_iff_degree_le_zero.2 h.2
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
c : 𝕜
h : P.leadingCoeff = c ∧ P.degree ≤ 0
this : P.natDegree = 0
refine_2 : Tendsto (fun (x : 𝕜) ↦ c) atTop (𝓝 c)
⊢ Tendsto (fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)

Tactic:
simp only [h.1, this, pow_zero, mul_one]

Premises used: pow_zero, And.left, mul_one
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
c : 𝕜
h : P.leadingCoeff = c ∧ P.degree ≤ 0
this : P.natDegree = 0
⊢ Tendsto (fun (x : 𝕜) ↦ c) atTop (𝓝 c)

Tactic:
tendsto_const_nhds

Premises used: tendsto_const_nhds
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
c : 𝕜
h : P.leadingCoeff = c ∧ P.degree ≤ 0
this : P.natDegree = 0
⊢ Tendsto (fun (x : 𝕜) ↦ c) atTop (𝓝 c)

Tactic:
exact tendsto_const_nhds

Premises used: tendsto_const_nhds
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
⊢ IsEquivalent.{u_1, u_1} (α := 𝕜) (E' := 𝕜) atBot ((fun (x : 𝕜) ↦ eval x (P.comp (-X))) ∘ Neg.neg)
    ((fun (x : 𝕜) ↦ (P.comp (-X)).leadingCoeff * x ^ (P.comp (-X)).natDegree) ∘ Neg.neg)

Tactic:
(P.comp (-X)).isEquivalent_atTop_lead.comp_tendsto tendsto_neg_atBot_atTop

Premises used: Filter.tendsto_neg_atBot_atTop, Polynomial.isEquivalent_atTop_lead, Asymptotics.IsEquivalent.comp_tendsto, Polynomial.X, Polynomial.comp, Neg.neg
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : ∀ (x : 𝕜), eval x P = ((fun (x : 𝕜) ↦ eval x (P.comp (-X))) ∘ Neg.neg) x
h₁ :
  ∀ (x : 𝕜),
    P.leadingCoeff * x ^ P.natDegree =
      ((fun (x : 𝕜) ↦ (P.comp (-X)).leadingCoeff * x ^ (P.comp (-X)).natDegree) ∘ Neg.neg) x
⊢ IsEquivalent (E' := 𝕜) atBot (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree

Tactic:
convert! (P.comp (-X)).isEquivalent_atTop_lead.comp_tendsto tendsto_neg_atBot_atTop using 2

Premises used: Filter.tendsto_neg_atBot_atTop, Polynomial.isEquivalent_atTop_lead, Asymptotics.IsEquivalent.comp_tendsto, Polynomial.X, Polynomial.comp, Neg.neg
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
x : 𝕜
⊢ eval x P = ((fun (x : 𝕜) ↦ eval x (P.comp (-X))) ∘ Neg.neg) x

Tactic:
simp
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
x : 𝕜
h :
  P.leadingCoeff * x ^ P.natDegree =
    (-x) ^ (P.comp (-X)).natDegree * HPow.hPow (α := 𝕜) (-1) P.natDegree * P.leadingCoeff
⊢ P.leadingCoeff * x ^ P.natDegree =
    ((fun (x : 𝕜) ↦ (P.comp (-X)).leadingCoeff * x ^ (P.comp (-X)).natDegree) ∘ Neg.neg) x

Tactic:
rw [Function.comp_apply, comp_neg_X_leadingCoeff_eq, ← mul_rotate]

Premises used: Polynomial.comp_neg_X_leadingCoeff_eq, Function.comp_apply, mul_rotate
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
x : 𝕜
⊢ P.leadingCoeff * x ^ P.natDegree =
    (-x) ^ (P.comp (-X)).natDegree * HPow.hPow (α := 𝕜) (-1) P.natDegree * P.leadingCoeff

Tactic:
simp [natDegree_comp, ← mul_pow, mul_comm]

Premises used: Polynomial.natDegree_comp, mul_comm, mul_pow
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : 0 < P.degree
⊢ 0 < (P.comp (-X)).degree

Tactic:
simp [hdeg]
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : 0 < P.degree
h : ∀ (x : 𝕜), |eval x P| = ((fun (x : 𝕜) ↦ |eval x (P.comp (-X))|) ∘ Neg.neg) x
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P|) atBot atTop

Tactic:
convert! ((P.comp (-X)).abs_tendsto_atTop (by simp [hdeg])).comp tendsto_neg_atBot_atTop using 2

Premises used: Filter.tendsto_neg_atBot_atTop, Polynomial.abs_tendsto_atTop, Filter.Tendsto.comp, Polynomial.X, Polynomial.comp, Neg.neg
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : 0 < P.degree
x : 𝕜
⊢ |eval x P| = ((fun (x : 𝕜) ↦ |eval x (P.comp (-X))|) ∘ Neg.neg) x

Tactic:
simp
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
⊢ (IsBoundedUnder (fun (x1 x2 : 𝕜) ↦ x1 ≤ x2) atBot fun (x : 𝕜) ↦ |eval x P|) ↔ P.degree ≤ 0

Tactic:
⟨fun h ↦ ?_, fun h ↦ ⟨|P.coeff 0|, eventually_map.mpr (Eventually.of_forall
    (forall_imp (fun _ ↦ le_of_eq) fun x ↦ congr_arg abs <| _root_.trans (congr_arg (eval x)
    (eq_C_of_degree_le_zero h)) eval_C))⟩⟩

Premises used: Iff.mpr, Polynomial.eval, trans, Polynomial.eval_C, abs, Filter.Eventually.of_forall, Filter.eventually_map, Polynomial.coeff, congr_arg, Polynomial.eq_C_of_degree_le_zero, forall_imp, Iff.intro, Exists.intro, le_of_eq, OfNat.ofNat
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
refine : ∀ (h : IsBoundedUnder (fun (x1 x2 : 𝕜) ↦ x1 ≤ x2) atBot fun (x : 𝕜) ↦ |eval x P|), P.degree ≤ 0
⊢ (IsBoundedUnder (fun (x1 x2 : 𝕜) ↦ x1 ≤ x2) atBot fun (x : 𝕜) ↦ |eval x P|) ↔ P.degree ≤ 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ⟨|P.coeff 0|, eventually_map.mpr (Eventually.of_forall
    (forall_imp (fun _ ↦ le_of_eq) fun x ↦ congr_arg abs <| _root_.trans (congr_arg (eval x)
    (eq_C_of_degree_le_zero h)) eval_C))⟩⟩
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : IsBoundedUnder (fun (x1 x2 : 𝕜) ↦ x1 ≤ x2) atBot fun (x : 𝕜) ↦ |eval x P|
contrapose! : ∀ (h : 0 < P.degree), ¬IsBoundedUnder (fun (x1 x2 : 𝕜) ↦ x1 ≤ x2) atBot fun (x : 𝕜) ↦ |eval x P|
⊢ P.degree ≤ 0

Tactic:
contrapose! h
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : 0 < P.degree
⊢ ¬IsBoundedUnder (fun (x1 x2 : 𝕜) ↦ x1 ≤ x2) atBot fun (x : 𝕜) ↦ |eval x P|

Tactic:
not_isBoundedUnder_of_tendsto_atTop (abs_tendsto_atBot P h)

Premises used: Filter.not_isBoundedUnder_of_tendsto_atTop, Polynomial.abs_tendsto_atBot
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : 0 < P.degree
⊢ ¬IsBoundedUnder (fun (x1 x2 : 𝕜) ↦ x1 ≤ x2) atBot fun (x : 𝕜) ↦ |eval x P|

Tactic:
exact not_isBoundedUnder_of_tendsto_atTop (abs_tendsto_atBot P h)

Premises used: Filter.not_isBoundedUnder_of_tendsto_atTop, Polynomial.abs_tendsto_atBot
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P|) atBot atTop ↔ 0 < P.degree

Tactic:
⟨fun h ↦ not_le.mp (mt (isBoundedUnder_abs_atBot_iff P).mpr
    (not_isBoundedUnder_of_tendsto_atTop h)), abs_tendsto_atBot P⟩

Premises used: not_le, Iff.mpr, Filter.not_isBoundedUnder_of_tendsto_atTop, mt, Polynomial.isBoundedUnder_abs_atBot_iff, Iff.intro, Iff.mp, Polynomial.abs_tendsto_atBot
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
pos :
  ∀ (hP : P = 0),
    IsEquivalent (E' := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P / eval x Q) fun (x : 𝕜) ↦
      P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)
neg :
  ∀ (hP : ¬P = 0),
    IsEquivalent (E' := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P / eval x Q) fun (x : 𝕜) ↦
      P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)
⊢ IsEquivalent (E' := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P / eval x Q) fun (x : 𝕜) ↦
    P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)

Tactic:
by_cases hP : P = 0
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hP : P = 0
⊢ IsEquivalent (E' := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P / eval x Q) fun (x : 𝕜) ↦
    P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)

Tactic:
simp [hP, IsEquivalent.refl]

Premises used: Asymptotics.IsEquivalent.refl
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hP : ¬P = 0
pos :
  ∀ (hQ : Q = 0),
    IsEquivalent (E' := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P / eval x Q) fun (x : 𝕜) ↦
      P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)
neg :
  ∀ (hQ : ¬Q = 0),
    IsEquivalent (E' := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P / eval x Q) fun (x : 𝕜) ↦
      P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)
⊢ IsEquivalent (E' := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P / eval x Q) fun (x : 𝕜) ↦
    P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)

Tactic:
by_cases hQ : Q = 0
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hP : ¬P = 0
hQ : Q = 0
⊢ IsEquivalent (E' := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P / eval x Q) fun (x : 𝕜) ↦
    P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)

Tactic:
simp [hQ, IsEquivalent.refl]

Premises used: Asymptotics.IsEquivalent.refl
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hP : ¬P = 0
hQ : ¬Q = 0
⊢ IsEquivalent (E' := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P / eval x Q) fun (x : 𝕜) ↦
    P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)

Tactic:
(P.isEquivalent_atTop_lead.symm.div Q.isEquivalent_atTop_lead.symm).symm.trans
      (EventuallyEq.isEquivalent ((eventually_gt_atTop 0).mono fun x hx => ?_))

Premises used: Polynomial.isEquivalent_atTop_lead, Filter.Eventually.mono, Asymptotics.IsEquivalent.div, Asymptotics.IsEquivalent.trans, Filter.EventuallyEq.isEquivalent, OfNat.ofNat, Asymptotics.IsEquivalent.symm, Filter.eventually_gt_atTop