R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
p : R[X]
hd : 0 < degree p
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ↑f (leadingCoeff p) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p)) l atTop
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
p : R[X]
hd : 0 < degree p
hf : ↑f (leadingCoeff p) ≠ 0
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ Tendsto (fun x => abv (eval₂ f (z x) p)) l atTop
revert hf
case refine'_1
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {a : R}, a ≠ 0 → ↑f (leadingCoeff (↑C a * X)) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) (↑C a * X))) l atTop

case refine'_2
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {p : R[X]},
    0 < degree p →
      (↑f (leadingCoeff p) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p)) l atTop) →
        ↑f (leadingCoeff (p * X)) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) (p * X))) l atTop

case refine'_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {p : R[X]} {a : R},
    0 < degree p →
      (↑f (leadingCoeff p) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p)) l atTop) →
        ↑f (leadingCoeff (p + ↑C a)) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) (p + ↑C a))) l atTop
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
p : R[X]
hd : 0 < degree p
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ↑f (leadingCoeff p) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p)) l atTop
refine' degree_pos_induction_on p hd _ _ _ <;> clear hd p
case refine'_1
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
a✝ : R
hc : ↑f (leadingCoeff (↑C a✝ * X)) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (↑C a✝ * X))) l atTop
case refine'_1
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {a : R}, a ≠ 0 → ↑f (leadingCoeff (↑C a * X)) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) (↑C a * X))) l atTop
rintro _ - hc
case refine'_1
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
a✝ : R
hc : ↑f a✝ ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (↑C a✝ * X))) l atTop
case refine'_1
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
a✝ : R
hc : ↑f (leadingCoeff (↑C a✝ * X)) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (↑C a✝ * X))) l atTop
rw [leadingCoeff_mul_X, leadingCoeff_C] at hc
no goals
case refine'_1
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
a✝ : R
hc : ↑f a✝ ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (↑C a✝ * X))) l atTop
simpa [abv_mul abv] using hz.const_mul_atTop ((abv_pos abv).2 hc)
case refine'_2
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a✝ : 0 < degree p✝
ihp : ↑f (leadingCoeff p✝) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : ↑f (leadingCoeff (p✝ * X)) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ * X))) l atTop
case refine'_2
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {p : R[X]},
    0 < degree p →
      (↑f (leadingCoeff p) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p)) l atTop) →
        ↑f (leadingCoeff (p * X)) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) (p * X))) l atTop
intro _ _ ihp hf
case refine'_2
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a✝ : 0 < degree p✝
ihp : ↑f (leadingCoeff p✝) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : ↑f (leadingCoeff p✝) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ * X))) l atTop
case refine'_2
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a✝ : 0 < degree p✝
ihp : ↑f (leadingCoeff p✝) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : ↑f (leadingCoeff (p✝ * X)) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ * X))) l atTop
rw [leadingCoeff_mul_X] at hf
no goals
case refine'_2
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a✝ : 0 < degree p✝
ihp : ↑f (leadingCoeff p✝) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : ↑f (leadingCoeff p✝) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ * X))) l atTop
simpa [abv_mul abv] using (ihp hf).atTop_mul_atTop hz
case refine'_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a : R
hd : 0 < degree p✝
ihp : ↑f (leadingCoeff p✝) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : ↑f (leadingCoeff (p✝ + ↑C a)) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ + ↑C a))) l atTop
case refine'_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {p : R[X]} {a : R},
    0 < degree p →
      (↑f (leadingCoeff p) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p)) l atTop) →
        ↑f (leadingCoeff (p + ↑C a)) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) (p + ↑C a))) l atTop
intro _ a hd ihp hf
case refine'_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a : R
hd : 0 < degree p✝
ihp : ↑f (leadingCoeff p✝) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : ↑f (leadingCoeff p✝) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ + ↑C a))) l atTop
case refine'_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a : R
hd : 0 < degree p✝
ihp : ↑f (leadingCoeff p✝) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : ↑f (leadingCoeff (p✝ + ↑C a)) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ + ↑C a))) l atTop
rw [add_comm, leadingCoeff_add_of_degree_lt (degree_C_le.trans_lt hd)] at hf
case refine'_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a : R
hd : 0 < degree p✝
ihp : ↑f (leadingCoeff p✝) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : ↑f (leadingCoeff p✝) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ + ↑C a)) + abv (-↑f a)) l atTop
case refine'_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a : R
hd : 0 < degree p✝
ihp : ↑f (leadingCoeff p✝) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : ↑f (leadingCoeff p✝) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ + ↑C a))) l atTop
refine' tendsto_atTop_of_add_const_right (abv (-f a)) _
case refine'_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a : R
hd : 0 < degree p✝
ihp : ↑f (leadingCoeff p✝) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : ↑f (leadingCoeff p✝) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ + ↑C a) + -↑f a)) l atTop
case refine'_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a : R
hd : 0 < degree p✝
ihp : ↑f (leadingCoeff p✝) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : ↑f (leadingCoeff p✝) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ + ↑C a)) + abv (-↑f a)) l atTop
refine' tendsto_atTop_mono (fun _ => abv_add abv _ _) _
no goals
case refine'_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a : R
hd : 0 < degree p✝
ihp : ↑f (leadingCoeff p✝) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : ↑f (leadingCoeff p✝) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ + ↑C a) + -↑f a)) l atTop
simpa using ihp hf