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

Tactic:
revert hf

Result:
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

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]},
    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

Tactic:
intro _ _ ihp 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✝ * X).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 (C a✝ * X).leadingCoeff ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (C a✝ * X))) l atTop

Tactic:
rw [leadingCoeff_mul_X, leadingCoeff_C] at hc

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
hc : f a✝ ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (C a✝ * 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}, a ≠ 0 → f (C a * X).leadingCoeff ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) (C a * X))) l atTop

Tactic:
rintro _ - hc

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

Tactic:
simpa [abv_mul abv] using (ihp hf).atTop_mul_atTop₀ hz

Result:
no goals