-- Mathlib/Topology/Algebra/Polynomial.lean
theorem tendsto_abv_eval₂_atTop {R S k α : Type*} [Semiring R] [Ring S] [LinearOrderedField k]
    (f : R →+* S) (abv : S → k) [IsAbsoluteValue abv] (p : R[X]) (hd : 0 < degree p)
    (hf : f p.leadingCoeff ≠ 0) {l : Filter α} {z : α → S} (hz : Tendsto (abv ∘ z) l atTop) :
    Tendsto (fun x => abv (p.eval₂ f (z x))) l atTop

Proof state:
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 < p✝.degree
ihp : f p✝.leadingCoeff ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : f p✝.leadingCoeff ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ + C a)) + abv (-f a)) l atTop

Tactic:
refine tendsto_atTop_mono (fun _ => abv_add abv _ _) ?_

Result:
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 < p✝.degree
ihp : f p✝.leadingCoeff ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : f p✝.leadingCoeff ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ + C a) + -f a)) l atTop

Proof state:
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 < p✝.degree
ihp : f p✝.leadingCoeff ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : f p✝.leadingCoeff ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ + C a) + -f a)) l atTop

Tactic:
simpa using ihp hf

Result:
no goals

Proof state:
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 < p.degree →
      (f p.leadingCoeff ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p)) l atTop) →
        f (p + C a).leadingCoeff ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) (p + C a))) l atTop

Tactic:
intro _ a hd ihp hf

Result:
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 < p✝.degree
ihp : f p✝.leadingCoeff ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : f (p✝ + C a).leadingCoeff ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ + C a))) l atTop

Proof state:
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 < p✝.degree
ihp : f p✝.leadingCoeff ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : f (p✝ * X).leadingCoeff ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ * X))) l atTop

Tactic:
rw [leadingCoeff_mul_X] at hf

Result:
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 < p✝.degree
ihp : f p✝.leadingCoeff ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : f p✝.leadingCoeff ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ * X))) l atTop

Proof state:
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

Tactic:
simpa [abv_mul abv] using hz.const_mul_atTop ((abv_pos abv).2 hc)

Result:
no goals

Proof state:
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 < p✝.degree
ihp : f p✝.leadingCoeff ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : f p✝.leadingCoeff ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ + C a))) l atTop

Tactic:
refine .atTop_of_add_const (abv (-f a)) ?_

Result:
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 < p✝.degree
ihp : f p✝.leadingCoeff ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : f p✝.leadingCoeff ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ + C a)) + abv (-f a)) l atTop

Proof state:
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 < p✝.degree
ihp : f p✝.leadingCoeff ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : f (p✝ + C a).leadingCoeff ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ + C a))) l atTop

Tactic:
rw [add_comm, leadingCoeff_add_of_degree_lt (degree_C_le.trans_lt hd)] at hf

Result:
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 < p✝.degree
ihp : f p✝.leadingCoeff ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : f p✝.leadingCoeff ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ + C a))) l atTop

Proof state:
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 < p.degree
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ f p.leadingCoeff ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p)) l atTop

Tactic:
refine degree_pos_induction_on p hd ?_ ?_ ?_ <;> clear hd p

Result:
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 (C a * X).leadingCoeff ≠ 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 < p.degree →
      (f p.leadingCoeff ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p)) l atTop) →
        f (p * X).leadingCoeff ≠ 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 < p.degree →
      (f p.leadingCoeff ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p)) l atTop) →
        f (p + C a).leadingCoeff ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) (p + C a))) l atTop