awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Order.Support
Goal:
X : Type u_1
M : Type u_2
inst : TopologicalSpace X
inst_1 : One M
inst_2 : SemilatticeSup M
f g : X → M
hf : HasCompactMulSupport f
hg : HasCompactMulSupport g
⊢ Function.mulSupport (f ⊔ g) ⊆ Function.mulSupport f ∪ Function.mulSupport g

Tactic:
Function.mulSupport_sup f g

Premises used: Function.mulSupport_sup
-- Module: Mathlib.Topology.Algebra.Order.Support
Goal:
X : Type u_1
M : Type u_2
inst : TopologicalSpace X
inst_1 : One M
inst_2 : SemilatticeSup M
f g : X → M
hf : HasCompactMulSupport f
hg : HasCompactMulSupport g
⊢ Function.mulSupport (f ⊔ g) ⊆ Function.mulSupport f ∪ Function.mulSupport g

Tactic:
exact Function.mulSupport_sup f g

Premises used: Function.mulSupport_sup
-- Module: Mathlib.Topology.Algebra.Order.Support
Goal:
X : Type u_1
M : Type u_2
inst : TopologicalSpace X
inst_1 : One M
inst_2 : SemilatticeInf M
f g : X → M
hf : HasCompactMulSupport f
hg : HasCompactMulSupport g
apply : mulTSupport (f ⊓ g) ⊆ mulTSupport f ∪ mulTSupport g
⊢ HasCompactMulSupport (f ⊓ g)

Tactic:
apply IsCompact.of_isClosed_subset (IsCompact.union hf hg) (isClosed_mulTSupport _)

Premises used: isClosed_mulTSupport, IsCompact.of_isClosed_subset, IsCompact.union
-- Module: Mathlib.Topology.Algebra.Order.Support
Goal:
X : Type u_1
M : Type u_2
inst : TopologicalSpace X
inst_1 : One M
inst_2 : SemilatticeInf M
f g : X → M
hf : HasCompactMulSupport f
hg : HasCompactMulSupport g
rw : closure (Function.mulSupport (f ⊓ g)) ⊆ closure (Function.mulSupport f ∪ Function.mulSupport g)
⊢ mulTSupport (f ⊓ g) ⊆ mulTSupport f ∪ mulTSupport g

Tactic:
rw [mulTSupport, mulTSupport, mulTSupport, ← closure_union]

Premises used: closure_union, mulTSupport
-- Module: Mathlib.Topology.Algebra.Order.Support
Goal:
X : Type u_1
M : Type u_2
inst : TopologicalSpace X
inst_1 : One M
inst_2 : SemilatticeInf M
f g : X → M
hf : HasCompactMulSupport f
hg : HasCompactMulSupport g
h : Function.mulSupport (f ⊓ g) ⊆ Function.mulSupport f ∪ Function.mulSupport g
⊢ closure (Function.mulSupport (f ⊓ g)) ⊆ closure (Function.mulSupport f ∪ Function.mulSupport g)

Tactic:
apply closure_mono

Premises used: closure_mono
-- Module: Mathlib.Topology.Algebra.Order.Support
Goal:
X : Type u_1
M : Type u_2
inst : TopologicalSpace X
inst_1 : One M
inst_2 : SemilatticeInf M
f g : X → M
hf : HasCompactMulSupport f
hg : HasCompactMulSupport g
⊢ Function.mulSupport (f ⊓ g) ⊆ Function.mulSupport f ∪ Function.mulSupport g

Tactic:
Function.mulSupport_inf f g

Premises used: Function.mulSupport_inf
-- Module: Mathlib.Topology.Algebra.Order.Support
Goal:
X : Type u_1
M : Type u_2
inst : TopologicalSpace X
inst_1 : One M
inst_2 : SemilatticeInf M
f g : X → M
hf : HasCompactMulSupport f
hg : HasCompactMulSupport g
⊢ Function.mulSupport (f ⊓ g) ⊆ Function.mulSupport f ∪ Function.mulSupport g

Tactic:
exact Function.mulSupport_inf f g

Premises used: Function.mulSupport_inf
-- Module: Mathlib.Topology.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : Preorder α
inst_3 : IsOrderedMonoid α
inst_4 : ContinuousConstSMul α α
s : Set α
h : IsUpperSet s
x y : α
hxy : x ≤ y
hx : x ∈ closure s
rw : y ∈ (y / x) • closure s
⊢ y ∈ closure ((y / x) • s)

Tactic:
rw [closure_smul]

Premises used: closure_smul
-- Module: Mathlib.Topology.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : Preorder α
inst_3 : IsOrderedMonoid α
inst_4 : ContinuousConstSMul α α
s : Set α
h : IsUpperSet s
x y : α
hxy : x ≤ y
hx : x ∈ closure s
⊢ y ∈ (y / x) • closure s

Tactic:
⟨x, hx, div_mul_cancel _ _⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, div_mul_cancel
-- Module: Mathlib.Topology.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : Preorder α
inst_3 : IsOrderedMonoid α
inst_4 : ContinuousConstSMul α α
s : Set α
h : IsUpperSet s
x y : α
hxy : x ≤ y
hx : x ∈ closure s
⊢ y ∈ (y / x) • closure s

Tactic:
exact ⟨x, hx, div_mul_cancel _ _⟩
-- Module: Mathlib.Topology.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : Preorder α
inst_3 : IsOrderedMonoid α
inst_4 : ContinuousConstSMul α α
s : Set α
h : IsLowerSet s
x y : α
hxy : y ≤ x
hx : x ∈ closure s
rw : y ∈ (y / x) • closure s
⊢ y ∈ closure ((y / x) • s)

Tactic:
rw [closure_smul]

Premises used: closure_smul
-- Module: Mathlib.Topology.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : Preorder α
inst_3 : IsOrderedMonoid α
inst_4 : ContinuousConstSMul α α
s : Set α
h : IsLowerSet s
x y : α
hxy : y ≤ x
hx : x ∈ closure s
⊢ y ∈ (y / x) • closure s

Tactic:
⟨x, hx, div_mul_cancel _ _⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, div_mul_cancel
-- Module: Mathlib.Topology.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : Preorder α
inst_3 : IsOrderedMonoid α
inst_4 : ContinuousConstSMul α α
s : Set α
h : IsLowerSet s
x y : α
hxy : y ≤ x
hx : x ∈ closure s
⊢ y ∈ (y / x) • closure s

Tactic:
exact ⟨x, hx, div_mul_cancel _ _⟩
-- Module: Mathlib.Topology.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : Preorder α
inst_3 : IsOrderedMonoid α
inst_4 : ContinuousConstSMul α α
s : Set α
hs : IsOpen s
rw : IsOpen (s * (↑(upperClosure 1) : Set α))
⊢ IsOpen (↑(upperClosure s) : Set α)

Tactic:
rw [← mul_one s, ← mul_upperClosure]

Premises used: mul_one, mul_upperClosure
-- Module: Mathlib.Topology.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : Preorder α
inst_3 : IsOrderedMonoid α
inst_4 : ContinuousConstSMul α α
s : Set α
hs : IsOpen s
⊢ IsOpen (s * (↑(upperClosure 1) : Set α))

Tactic:
hs.mul_right

Premises used: IsOpen.mul_right
-- Module: Mathlib.Topology.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : Preorder α
inst_3 : IsOrderedMonoid α
inst_4 : ContinuousConstSMul α α
s : Set α
hs : IsOpen s
⊢ IsOpen (s * (↑(upperClosure 1) : Set α))

Tactic:
exact hs.mul_right

Premises used: IsOpen.mul_right
-- Module: Mathlib.Topology.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : Preorder α
inst_3 : IsOrderedMonoid α
inst_4 : ContinuousConstSMul α α
s : Set α
hs : IsOpen s
rw : IsOpen (s * (↑(lowerClosure 1) : Set α))
⊢ IsOpen (↑(lowerClosure s) : Set α)

Tactic:
rw [← mul_one s, ← mul_lowerClosure]

Premises used: mul_one, mul_lowerClosure
-- Module: Mathlib.Topology.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : Preorder α
inst_3 : IsOrderedMonoid α
inst_4 : ContinuousConstSMul α α
s : Set α
hs : IsOpen s
⊢ IsOpen (s * (↑(lowerClosure 1) : Set α))

Tactic:
hs.mul_right

Premises used: IsOpen.mul_right
-- Module: Mathlib.Topology.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : Preorder α
inst_3 : IsOrderedMonoid α
inst_4 : ContinuousConstSMul α α
s : Set α
hs : IsOpen s
⊢ IsOpen (s * (↑(lowerClosure 1) : Set α))

Tactic:
exact hs.mul_right

Premises used: IsOpen.mul_right
-- Module: Mathlib.Topology.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : HasUpperLowerClosure α
s : Set α
⊢ IsUpperSet s → IsUpperSet (closure s)

Tactic:
HasUpperLowerClosure.isUpperSet_closure _

Premises used: HasUpperLowerClosure.isUpperSet_closure
-- Module: Mathlib.Topology.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : HasUpperLowerClosure α
s : Set α
⊢ IsLowerSet s → IsLowerSet (closure s)

Tactic:
HasUpperLowerClosure.isLowerSet_closure _

Premises used: HasUpperLowerClosure.isLowerSet_closure
-- Module: Mathlib.Topology.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : HasUpperLowerClosure α
s : Set α
⊢ IsOpen s → IsOpen (↑(upperClosure s) : Set α)

Tactic:
HasUpperLowerClosure.isOpen_upperClosure _

Premises used: HasUpperLowerClosure.isOpen_upperClosure
-- Module: Mathlib.Topology.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : HasUpperLowerClosure α
s : Set α
⊢ IsOpen s → IsOpen (↑(lowerClosure s) : Set α)

Tactic:
HasUpperLowerClosure.isOpen_lowerClosure _

Premises used: HasUpperLowerClosure.isOpen_lowerClosure
-- Module: Mathlib.Topology.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : HasUpperLowerClosure α
s : Set α
h : IsUpperSet s
rw : IsLowerSet (closure sᶜ)
⊢ IsUpperSet (interior s)

Tactic:
rw [← isLowerSet_compl, ← closure_compl]

Premises used: isLowerSet_compl, closure_compl
-- Module: Mathlib.Topology.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : HasUpperLowerClosure α
s : Set α
h : IsUpperSet s
⊢ IsLowerSet (closure sᶜ)

Tactic:
h.compl.closure

Premises used: IsUpperSet.compl, IsLowerSet.closure
-- Module: Mathlib.Topology.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : HasUpperLowerClosure α
s : Set α
h : IsUpperSet s
⊢ IsLowerSet (closure sᶜ)

Tactic:
exact h.compl.closure

Premises used: IsUpperSet.compl, IsLowerSet.closure
-- Module: Mathlib.Topology.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : HasUpperLowerClosure α
s : Set α
h : IsLowerSet s
⊢ IsLowerSet (interior s)

Tactic:
h.toDual.interior

Premises used: Set.Mem, IsUpperSet.interior, setOf, Set.preimage, IsLowerSet, IsLowerSet.toDual, OrderDual
-- Module: Mathlib.Topology.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : HasUpperLowerClosure α
s : Set α
h : s.OrdConnected
rw : (interior (↑(upperClosure s) : Set α) ∩ interior (↑(lowerClosure s) : Set α)).OrdConnected
⊢ (interior s).OrdConnected

Tactic:
rw [← h.upperClosure_inter_lowerClosure, interior_inter]

Premises used: interior_inter, Set.OrdConnected.upperClosure_inter_lowerClosure
-- Module: Mathlib.Topology.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : HasUpperLowerClosure α
s : Set α
h : s.OrdConnected
⊢ (interior (↑(upperClosure s) : Set α) ∩ interior (↑(lowerClosure s) : Set α)).OrdConnected

Tactic:
(upperClosure s).upper.interior.ordConnected.inter (lowerClosure s).lower.interior.ordConnected

Premises used: IsLowerSet.ordConnected, IsUpperSet.interior, upperClosure, IsUpperSet.ordConnected, Set.OrdConnected.inter, UpperSet.upper, LowerSet.lower, lowerClosure, IsLowerSet.interior
-- Module: Mathlib.Topology.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : HasUpperLowerClosure α
s : Set α
h : s.OrdConnected
⊢ (interior (↑(upperClosure s) : Set α) ∩ interior (↑(lowerClosure s) : Set α)).OrdConnected

Tactic:
exact
    (upperClosure s).upper.interior.ordConnected.inter (lowerClosure s).lower.interior.ordConnected

Premises used: IsLowerSet.ordConnected, IsUpperSet.interior, upperClosure, IsUpperSet.ordConnected, Set.OrdConnected.inter, UpperSet.upper, LowerSet.lower, lowerClosure, IsLowerSet.interior
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
inst_3 : Semiring S
p : S[X]
f : S →+* R
simp :
  Continuous (Y := R) fun (x : R) ↦ p.sum fun (e : ℕ) (a : S) ↦ HMul.hMul (α := R) ((f : (a : S) → R) a : R) (x ^ e)
⊢ Continuous (Y := R) fun (x : R) ↦ eval₂ f x p

Tactic:
simp only [eval₂_eq_sum]

Premises used: Polynomial.eval₂_eq_sum
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
inst_3 : Semiring S
p : S[X]
f : S →+* R
⊢ Continuous (Y := R) fun (x : R) ↦ p.sum fun (e : ℕ) (a : S) ↦ HMul.hMul (α := R) ((f : (a : S) → R) a : R) (x ^ e)

Tactic:
continuous_finsetSum _ fun c _ => continuous_const.mul (continuous_pow _)

Premises used: Polynomial.sum, continuous_const, Continuous.mul, continuous_finsetSum, continuous_pow
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
inst_3 : Semiring S
p : S[X]
f : S →+* R
⊢ Continuous (Y := R) fun (x : R) ↦ p.sum fun (e : ℕ) (a : S) ↦ HMul.hMul (α := R) ((f : (a : S) → R) a : R) (x ^ e)

Tactic:
exact continuous_finsetSum _ fun c _ => continuous_const.mul (continuous_pow _)

Premises used: continuous_const, Continuous.mul, continuous_finsetSum, continuous_pow
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
p : R[X]
⊢ Continuous (Y := R) fun (x : R) ↦ eval x p

Tactic:
p.continuous_eval₂ _

Premises used: Polynomial.eval, Polynomial.continuous_eval₂
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
p : R[X]
a : R
⊢ ContinuousAt (Y := R) (fun (x : R) ↦ eval x p) a

Tactic:
p.continuous.continuousAt

Premises used: Polynomial.continuous, Continuous.continuousAt
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
p : R[X]
s : Set R
a : R
⊢ ContinuousWithinAt (Y := R) (fun (x : R) ↦ eval x p) s a

Tactic:
p.continuous.continuousWithinAt

Premises used: Polynomial.continuous, Continuous.continuousWithinAt
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
p : R[X]
s : Set R
⊢ ContinuousOn (Y := R) (fun (x : R) ↦ eval x p) s

Tactic:
p.continuous.continuousOn

Premises used: Polynomial.continuous, Continuous.continuousOn
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalSemiring A
p : R[X]
⊢ Continuous (Y := A) fun (x : A) ↦ (aeval x : (a : R[X]) → A) p

Tactic:
p.continuous_eval₂ _

Premises used: Polynomial.continuous_eval₂
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalSemiring A
p : R[X]
a : A
⊢ ContinuousAt (Y := A) (fun (x : A) ↦ (aeval x : (a : R[X]) → A) p) a

Tactic:
p.continuous_aeval.continuousAt

Premises used: Polynomial.continuous_aeval, Continuous.continuousAt
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalSemiring A
p : R[X]
s : Set A
a : A
⊢ ContinuousWithinAt (Y := A) (fun (x : A) ↦ (aeval x : (a : R[X]) → A) p) s a

Tactic:
p.continuous_aeval.continuousWithinAt

Premises used: Polynomial.continuous_aeval, Continuous.continuousWithinAt
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalSemiring A
p : R[X]
s : Set A
⊢ ContinuousOn (Y := A) (fun (x : A) ↦ (aeval x : (a : R[X]) → A) p) s

Tactic:
p.continuous_aeval.continuousOn

Premises used: Polynomial.continuous_aeval, Continuous.continuousOn
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst : Semiring R
inst_1 : Ring S
inst_2 : Field k
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst_5 : IsAbsoluteValue abv
p : R[X]
hd : 0 < p.degree
hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
revert :
  ∀ (hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)),
    Tendsto.{u_4, u_3} (β := k) (fun (x : α) ↦ abv (eval₂ f (z x) p)) l atTop
⊢ Tendsto.{u_4, u_3} (β := k) (fun (x : α) ↦ abv (eval₂ f (z x) p)) l atTop

Tactic:
revert hf
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst : Semiring R
inst_1 : Ring S
inst_2 : Field k
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst_5 : IsAbsoluteValue abv
p : R[X]
hd : 0 < p.degree
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ (hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)),
    Tendsto.{u_4, u_3} (β := k) (fun (x : α) ↦ abv (eval₂ f (z x) p)) l atTop

Tactic:
degree_pos_induction_on p hd ?_ ?_ ?_

Premises used: Polynomial.degree_pos_induction_on
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst : Semiring R
inst_1 : Ring S
inst_2 : Field k
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst_5 : IsAbsoluteValue abv
p : R[X]
hd : 0 < p.degree
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
refine_1 :
  ∀ {a : R},
    a ≠ 0 →
      ∀
        (hf :
          Ne.{u_2 + 1} (α := S)
            ((f : (a : R) → S) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).leadingCoeff : S)
            (0 : S)),
        Tendsto.{u_4, u_3} (β := k)
          (fun (x : α) ↦ abv (eval₂ f (z x) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X))) l
          atTop
refine_2 :
  ∀ {p : R[X]},
    0 < p.degree →
      (∀ (hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)),
          Tendsto.{u_4, u_3} (β := k) (fun (x : α) ↦ abv (eval₂ f (z x) p)) l atTop) →
        ∀ (hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) (p * X).leadingCoeff : S) (0 : S)),
          Tendsto.{u_4, u_3} (β := k) (fun (x : α) ↦ abv (eval₂ f (z x) (p * X))) l atTop
refine_3 :
  ∀ {p : R[X]} {a : R},
    0 < p.degree →
      (∀ (hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)),
          Tendsto.{u_4, u_3} (β := k) (fun (x : α) ↦ abv (eval₂ f (z x) p)) l atTop) →
        ∀
          (hf :
            Ne.{u_2 + 1} (α := S)
              ((f : (a : R) → S) (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).leadingCoeff : S) (0 : S)),
          Tendsto.{u_4, u_3} (β := k)
            (fun (x : α) ↦ abv (eval₂ f (z x) (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])))) l atTop
⊢ ∀ (hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)),
    Tendsto.{u_4, u_3} (β := k) (fun (x : α) ↦ abv (eval₂ f (z x) p)) l atTop

Tactic:
refine degree_pos_induction_on p hd ?_ ?_ ?_
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst : Semiring R
inst_1 : Ring S
inst_2 : Field k
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst_5 : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
a : R
hc :
  Ne.{u_2 + 1} (α := S)
    ((f : (a : R) → S) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).leadingCoeff : S) (0 : S)
⊢ Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)

Tactic:
rw [leadingCoeff_mul_X, leadingCoeff_C] at hc

Premises used: Polynomial.leadingCoeff_mul_X, Polynomial.leadingCoeff_C
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst : Semiring R
inst_1 : Ring S
inst_2 : Field k
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst_5 : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
a : R
hc : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
⊢ Tendsto.{u_4, u_3} (β := k)
    (fun (x : α) ↦ abv (eval₂ f (z x) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X))) l atTop

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

Premises used: Iff.mpr, Filter.Tendsto.const_mul_atTop, IsAbsoluteValue.abv_mul, IsAbsoluteValue.abv_pos
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst : Semiring R
inst_1 : Ring S
inst_2 : Field k
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst_5 : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p : R[X]
refine_2 :
  0 < p.degree →
    (∀ (hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)),
        Tendsto.{u_4, u_3} (β := k) (fun (x : α) ↦ abv (eval₂ f (z x) p)) l atTop) →
      ∀ (hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) (p * X).leadingCoeff : S) (0 : S)),
        Tendsto.{u_4, u_3} (β := k) (fun (x : α) ↦ abv (eval₂ f (z x) (p * X))) l atTop
⊢ 0 < p.degree →
    (∀ (hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)),
        Tendsto.{u_4, u_3} (β := k) (fun (x : α) ↦ abv (eval₂ f (z x) p)) l atTop) →
      ∀ (hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) (p * X).leadingCoeff : S) (0 : S)),
        Tendsto.{u_4, u_3} (β := k) (fun (x : α) ↦ abv (eval₂ f (z x) (p * X))) l atTop

Tactic:
_
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst : Semiring R
inst_1 : Ring S
inst_2 : Field k
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst_5 : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p : R[X]
h : 0 < p.degree
ihp :
  ∀ (hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)),
    Tendsto.{u_4, u_3} (β := k) (fun (x : α) ↦ abv (eval₂ f (z x) p)) l atTop
hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) (p * X).leadingCoeff : S) (0 : S)
⊢ Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)

Tactic:
rw [leadingCoeff_mul_X] at hf

Premises used: Polynomial.leadingCoeff_mul_X
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst : Semiring R
inst_1 : Ring S
inst_2 : Field k
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst_5 : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p : R[X]
h : 0 < p.degree
ihp :
  ∀ (hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)),
    Tendsto.{u_4, u_3} (β := k) (fun (x : α) ↦ abv (eval₂ f (z x) p)) l atTop
hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
⊢ Tendsto.{u_4, u_3} (β := k) (fun (x : α) ↦ abv (eval₂ f (z x) (p * X))) l atTop

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

Premises used: Filter.Tendsto.atTop_mul_atTop₀, IsAbsoluteValue.abv_mul
-- Module: Mathlib.Topology.Algebra.Polynomial
Goal:
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst : Semiring R
inst_1 : Ring S
inst_2 : Field k
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst_5 : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p : R[X]
a : R
hd : 0 < p.degree
ihp :
  ∀ (hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)),
    Tendsto.{u_4, u_3} (β := k) (fun (x : α) ↦ abv (eval₂ f (z x) p)) l atTop
hf :
  Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).leadingCoeff : S)
    (0 : S)
⊢ Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)

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

Premises used: add_comm, Polynomial.leadingCoeff_add_of_degree_lt, LE.le.trans_lt, Polynomial.degree_C_le