awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst : Preorder ι
s : ι → Set α
inst_1 : (i : ι) → DecidablePred fun (x : α) ↦ x ∈ s i
inst_2 : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x
hs : Monotone s
f g : (a : α) → β a
a : α
ha : ¬∃ (i : ι), a ∈ s i
i : ι
⊢ (s i).piecewise (β := β) f g a = piecewise (β := β) (⋃ (i : ι), s i) f g a

Tactic:
simp only [Set.piecewise_eq_of_notMem, not_exists.1 ha i, mt mem_iUnion.1 ha,
      not_false_eq_true]

Premises used: Set.piecewise_eq_of_notMem, Set.mem_iUnion, not_exists, mt, Iff.mp, not_false_eq_true
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst : Preorder ι
s : ι → Set α
inst_1 : (i : ι) → DecidablePred fun (x : α) ↦ x ∈ s i
inst_2 : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋂ (i : ι), s i) x
hs : Antitone s
f g : (a : α) → β a
a : α
⊢ ∀ᶠ (i : ι) in atTop, ((compl ∘ s) i).piecewise (β := β) g f a = piecewise (β := β) (⋃ (i : ι), (compl ∘ s) i) g f a

Tactic:
(compl_anti.comp hs).piecewise_eventually_eq_iUnion g f a

Premises used: compl_anti, Antitone.comp, Monotone.piecewise_eventually_eq_iUnion
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst : Preorder ι
s : ι → Set α
inst_1 : (i : ι) → DecidablePred fun (x : α) ↦ x ∈ s i
inst_2 : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋂ (i : ι), s i) x
hs : Antitone s
f g : (a : α) → β a
a : α
h : ∀ (x : ι), ((compl ∘ s) x).piecewise (β := β) g f a = (s x).piecewise (β := β) f g a
h₁ : ∀ (x : ι), piecewise (β := β) (⋃ (i : ι), (compl ∘ s) i) g f a = piecewise (β := β) (⋂ (i : ι), s i) f g a
⊢ ∀ᶠ (i : ι) in atTop, (s i).piecewise (β := β) f g a = piecewise (β := β) (⋂ (i : ι), s i) f g a

Tactic:
convert! ← (compl_anti.comp hs).piecewise_eventually_eq_iUnion g f a using 3

Premises used: compl_anti, Antitone.comp, Monotone.piecewise_eventually_eq_iUnion
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst : Preorder ι
s : ι → Set α
inst_1 : (i : ι) → DecidablePred fun (x : α) ↦ x ∈ s i
inst_2 : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋂ (i : ι), s i) x
hs : Antitone s
f g : (a : α) → β a
a : α
x : ι
⊢ (s x)ᶜ.piecewise (β := β) g f a = (s x).piecewise (β := β) f g a

Tactic:
congr_fun (Set.piecewise_compl (s _) g f) a

Premises used: Set.piecewise_compl, congr_fun
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst : Preorder ι
s : ι → Set α
inst_1 : (i : ι) → DecidablePred fun (x : α) ↦ x ∈ s i
inst_2 : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋂ (i : ι), s i) x
hs : Antitone s
f g : (a : α) → β a
a : α
x : ι
⊢ ((compl ∘ s) x).piecewise (β := β) g f a = (s x).piecewise (β := β) f g a

Tactic:
convert! congr_fun (Set.piecewise_compl (s _) g f) a

Premises used: Set.piecewise_compl, congr_fun
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst : Preorder ι
s : ι → Set α
inst_1 : (i : ι) → DecidablePred fun (x : α) ↦ x ∈ s i
inst_2 : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋂ (i : ι), s i) x
hs : Antitone s
f g : (a : α) → β a
a : α
x : ι
⊢ piecewise (β := β) (⋃ (i : ι), (compl ∘ s) i) g f a = piecewise (β := β) (⋂ (i : ι), s i) f g a

Tactic:
simp only [(· ∘ ·), ← compl_iInter, Set.piecewise_compl]

Premises used: Set.compl_iInter, Function.comp, Set.piecewise_compl
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst : Preorder ι
s : ι → Set α
inst_1 : (i : ι) → DecidablePred fun (x : α) ↦ x ∈ s i
inst_2 : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋂ (i : ι), s i) x
hs : Antitone s
f g : (a : α) → β a
a : α
h : ∀ (x : ι), ((compl ∘ s) x).piecewise (β := β) g f a = (s x).piecewise (β := β) f g a
h₁ h₂ : ∀ (x : ι), piecewise (β := β) (⋃ (i : ι), (compl ∘ s) i) g f a = piecewise (β := β) (⋂ (i : ι), s i) f g a
⊢ ∀ᶠ (i : ι) in atTop, (s i).piecewise (β := β) f g a = piecewise (β := β) (⋂ (i : ι), s i) f g a

Tactic:
classical
  convert! ← (compl_anti.comp hs).piecewise_eventually_eq_iUnion g f a using 3
  · convert! congr_fun (Set.piecewise_compl (s _) g f) a
  · simp only [(· ∘ ·), ← compl_iInter, Set.piecewise_compl]

Premises used: Set.compl_iInter, Function.comp, Set.piecewise_compl, congr_fun
-- Module: Mathlib.Order.Filter.AtTopBot.Disjoint
Goal:
α : Type u_3
inst : Preorder α
x : α
⊢ Disjoint atBot (𝓟 (Ioi x))

Tactic:
disjoint_of_disjoint_of_mem (Iic_disjoint_Ioi le_rfl) (Iic_mem_atBot x) (mem_principal_self _)

Premises used: Filter.mem_principal_self, le_rfl, Set.Iic_disjoint_Ioi, Filter.disjoint_of_disjoint_of_mem, Filter.Iic_mem_atBot
-- Module: Mathlib.Order.Filter.AtTopBot.Disjoint
Goal:
α : Type u_3
inst : Preorder α
inst_1 : NoTopOrder α
x : α
⊢ Disjoint atTop (𝓟 (Iic x))

Tactic:
disjoint_of_disjoint_of_mem (Iic_disjoint_Ioi le_rfl).symm (Ioi_mem_atTop x)
    (mem_principal_self _)

Premises used: Filter.mem_principal_self, le_rfl, Set.Iic_disjoint_Ioi, Filter.Ioi_mem_atTop, Filter.disjoint_of_disjoint_of_mem, Disjoint.symm
-- Module: Mathlib.Order.Filter.AtTopBot.Disjoint
Goal:
α : Type u_3
inst : Preorder α
inst_1 : NoTopOrder α
x : α
⊢ Disjoint (pure x) atTop

Tactic:
Disjoint.symm <| (disjoint_atTop_principal_Iic x).mono_right <| le_principal_iff.2 <|
    mem_pure.2 self_mem_Iic

Premises used: Iff.mpr, Filter.le_principal_iff, Set.self_mem_Iic, Disjoint.symm, Filter.disjoint_atTop_principal_Iic, Disjoint.mono_right, Filter.mem_pure
-- Module: Mathlib.Order.Filter.AtTopBot.Disjoint
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : Nontrivial α
rcases : ∀ (x y : α) (hne : x ≠ y), Disjoint.{u_3} (α := Filter α) atBot atTop
⊢ Disjoint.{u_3} (α := Filter α) atBot atTop

Tactic:
rcases exists_pair_ne α with ⟨x, y, hne⟩

Premises used: exists_pair_ne
-- Module: Mathlib.Order.Filter.AtTopBot.Disjoint
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : Nontrivial α
x y : α
hne : x ≠ y
pos : ∀ (hle : x ≤ y), Disjoint.{u_3} (α := Filter α) atBot atTop
neg : ∀ (hle : ¬x ≤ y), Disjoint.{u_3} (α := Filter α) atBot atTop
⊢ Disjoint.{u_3} (α := Filter α) atBot atTop

Tactic:
by_cases hle : x ≤ y
-- Module: Mathlib.Order.Filter.AtTopBot.Disjoint
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : Nontrivial α
x y : α
hne : x ≠ y
hle : x ≤ y
⊢ Disjoint.{u_3} (α := Filter α) atBot atTop

Tactic:
disjoint_of_disjoint_of_mem ?_ (Iic_mem_atBot x) (Ici_mem_atTop y)

Premises used: Filter.disjoint_of_disjoint_of_mem, Filter.Iic_mem_atBot, Filter.Ici_mem_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Disjoint
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : Nontrivial α
x y : α
hne : x ≠ y
hle : x ≤ y
pos : Disjoint (Iic x) (Ici y)
⊢ Disjoint.{u_3} (α := Filter α) atBot atTop

Tactic:
refine disjoint_of_disjoint_of_mem ?_ (Iic_mem_atBot x) (Ici_mem_atTop y)

Premises used: Filter.disjoint_of_disjoint_of_mem, Filter.Iic_mem_atBot, Filter.Ici_mem_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Disjoint
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : Nontrivial α
x y : α
hne : x ≠ y
hle : x ≤ y
⊢ Disjoint (Iic x) (Ici y)

Tactic:
Iic_disjoint_Ici.2 (hle.lt_of_ne hne).not_ge

Premises used: Iff.mpr, LE.le.lt_of_ne, Set.Iic_disjoint_Ici, LT.lt.not_ge
-- Module: Mathlib.Order.Filter.AtTopBot.Disjoint
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : Nontrivial α
x y : α
hne : x ≠ y
hle : x ≤ y
⊢ Disjoint (Iic x) (Ici y)

Tactic:
exact Iic_disjoint_Ici.2 (hle.lt_of_ne hne).not_ge

Premises used: Iff.mpr, LE.le.lt_of_ne, Set.Iic_disjoint_Ici, LT.lt.not_ge
-- Module: Mathlib.Order.Filter.AtTopBot.Disjoint
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : Nontrivial α
x y : α
hne : x ≠ y
hle : ¬x ≤ y
⊢ Disjoint.{u_3} (α := Filter α) atBot atTop

Tactic:
disjoint_of_disjoint_of_mem ?_ (Iic_mem_atBot y) (Ici_mem_atTop x)

Premises used: Filter.disjoint_of_disjoint_of_mem, Filter.Iic_mem_atBot, Filter.Ici_mem_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Disjoint
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : Nontrivial α
x y : α
hne : x ≠ y
hle : ¬x ≤ y
neg : Disjoint (Iic y) (Ici x)
⊢ Disjoint.{u_3} (α := Filter α) atBot atTop

Tactic:
refine disjoint_of_disjoint_of_mem ?_ (Iic_mem_atBot y) (Ici_mem_atTop x)

Premises used: Filter.disjoint_of_disjoint_of_mem, Filter.Iic_mem_atBot, Filter.Ici_mem_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Disjoint
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : Nontrivial α
x y : α
hne : x ≠ y
hle : ¬x ≤ y
⊢ Disjoint (Iic y) (Ici x)

Tactic:
Iic_disjoint_Ici.2 hle

Premises used: Iff.mpr, Set.Iic_disjoint_Ici
-- Module: Mathlib.Order.Filter.AtTopBot.Disjoint
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : Nontrivial α
x y : α
hne : x ≠ y
hle : ¬x ≤ y
⊢ Disjoint (Iic y) (Ici x)

Tactic:
exact Iic_disjoint_Ici.2 hle

Premises used: Iff.mpr, Set.Iic_disjoint_Ici
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : 0 < r
h : Tendsto f l atTop
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r⁻¹ * (r * f x)) l atTop

Tactic:
simpa only [inv_mul_cancel_left₀ hr.ne']

Premises used: inv_mul_cancel_left₀, LT.lt.ne'
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : 0 < r
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * r) l atTop ↔ Tendsto f l atTop

Tactic:
simpa only [mul_comm] using tendsto_const_mul_atTop_of_pos hr

Premises used: mul_comm, Filter.tendsto_const_mul_atTop_of_pos
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : 0 < r
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x / r) l atTop ↔ Tendsto f l atTop

Tactic:
simpa only [div_eq_mul_inv] using tendsto_mul_const_atTop_of_pos (inv_pos.2 hr)

Premises used: Iff.mpr, inv_pos, div_eq_mul_inv, Filter.tendsto_mul_const_atTop_of_pos
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
h : Tendsto f l atTop
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atTop ↔ 0 < r

Tactic:
⟨fun hrf => not_le.mp fun hr => ?_, fun hr => (tendsto_const_mul_atTop_of_pos hr).mpr h⟩

Premises used: not_le, Iff.mpr, Iff.intro, Iff.mp, Filter.tendsto_const_mul_atTop_of_pos
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
h : Tendsto f l atTop
refine : ∀ (hrf : Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atTop) (hr : r ≤ 0), False
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atTop ↔ 0 < r

Tactic:
refine ⟨fun hrf => not_le.mp fun hr => ?_, fun hr => (tendsto_const_mul_atTop_of_pos hr).mpr h⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
h : Tendsto f l atTop
hrf : Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atTop
hr : r ≤ 0
rcases : ∀ (x : β) (hx : 0 ≤ f x) (hrx : 0 < r * f x), False
⊢ False

Tactic:
rcases ((h.eventually_ge_atTop 0).and (hrf.eventually_gt_atTop 0)).exists with ⟨x, hx, hrx⟩

Premises used: Filter.Eventually.and, Filter.Eventually.exists, OfNat.ofNat, Filter.Tendsto.eventually_ge_atTop, Filter.Tendsto.eventually_gt_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
h : Tendsto f l atTop
hrf : Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atTop
hr : r ≤ 0
x : β
hx : 0 ≤ f x
hrx : 0 < r * f x
⊢ False

Tactic:
(mul_nonpos_of_nonpos_of_nonneg hr hx).not_gt hrx

Premises used: mul_nonpos_of_nonpos_of_nonneg, LE.le.not_gt
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
h : Tendsto f l atTop
hrf : Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atTop
hr : r ≤ 0
x : β
hx : 0 ≤ f x
hrx : 0 < r * f x
⊢ False

Tactic:
exact (mul_nonpos_of_nonpos_of_nonneg hr hx).not_gt hrx

Premises used: mul_nonpos_of_nonpos_of_nonneg, LE.le.not_gt
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
h : Tendsto f l atTop
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * r) l atTop ↔ 0 < r

Tactic:
simp only [mul_comm _ r, tendsto_const_mul_atTop_iff_pos h]

Premises used: Filter.tendsto_const_mul_atTop_iff_pos, mul_comm
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
h : Tendsto f l atTop
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x / r) l atTop ↔ 0 < r

Tactic:
simp only [div_eq_mul_inv, tendsto_mul_const_atTop_iff_pos h, inv_pos]

Premises used: inv_pos, Filter.tendsto_mul_const_atTop_iff_pos, div_eq_mul_inv
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atTop

Tactic:
(tendsto_const_mul_atTop_of_pos hr).2 hf

Premises used: Iff.mpr, Filter.tendsto_const_mul_atTop_of_pos
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * r) l atTop

Tactic:
(tendsto_mul_const_atTop_of_pos hr).2 hf

Premises used: Iff.mpr, Filter.tendsto_mul_const_atTop_of_pos
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x / r) l atTop

Tactic:
simpa only [div_eq_mul_inv] using hf.atTop_mul_const (inv_pos.2 hr)

Premises used: Iff.mpr, Filter.Tendsto.atTop_mul_const, inv_pos, div_eq_mul_inv
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
c : α
n : ℕ
hn : n ≠ 0
hc : 0 < c
⊢ Tendsto (β := α) (fun (x : α) ↦ c * x ^ n) atTop atTop

Tactic:
Tendsto.const_mul_atTop hc (tendsto_pow_atTop hn)

Premises used: Filter.Tendsto.const_mul_atTop, Filter.tendsto_pow_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
c : α
n : ℕ
⊢ Tendsto (β := α) (fun (x : α) ↦ c * x ^ n) atTop atTop ↔ n ≠ 0 ∧ 0 < c

Tactic:
⟨fun h => ⟨?_, ?_⟩, fun h => tendsto_const_mul_pow_atTop h.1 h.2⟩

Premises used: Filter.tendsto_const_mul_pow_atTop, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
c : α
n : ℕ
refine_1 : ∀ (h : Tendsto (β := α) (fun (x : α) ↦ c * x ^ n) atTop atTop), n ≠ 0
refine_2 : ∀ (h : Tendsto (β := α) (fun (x : α) ↦ c * x ^ n) atTop atTop), 0 < c
⊢ Tendsto (β := α) (fun (x : α) ↦ c * x ^ n) atTop atTop ↔ n ≠ 0 ∧ 0 < c

Tactic:
refine ⟨fun h => ⟨?_, ?_⟩, fun h => tendsto_const_mul_pow_atTop h.1 h.2⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
c : α
h : Tendsto (β := α) (fun (x : α) ↦ c * HPow.hPow (β := ℕ) x 0) atTop atTop
⊢ False

Tactic:
simp only [pow_zero, not_tendsto_const_atTop] at h

Premises used: pow_zero, Filter.not_tendsto_const_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
c : α
n : ℕ
h : Tendsto (β := α) (fun (x : α) ↦ c * x ^ n) atTop atTop
refine_2 : ∀ (k : α) (hck : 0 < c * k ^ n) (hk : 0 ≤ k), 0 < c
⊢ 0 < c

Tactic:
rcases ((h.eventually_gt_atTop 0).and (eventually_ge_atTop 0)).exists with ⟨k, hck, hk⟩

Premises used: Filter.Eventually.and, Filter.Eventually.exists, Filter.eventually_ge_atTop, OfNat.ofNat, Filter.Tendsto.eventually_gt_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
c : α
n : ℕ
h : Tendsto (β := α) (fun (x : α) ↦ c * x ^ n) atTop atTop
k : α
hck : 0 < c * k ^ n
hk : 0 ≤ k
⊢ 0 < c

Tactic:
pos_of_mul_pos_left hck (pow_nonneg hk _)

Premises used: pow_nonneg, pos_of_mul_pos_left
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
c : α
n : ℕ
h : Tendsto (β := α) (fun (x : α) ↦ c * x ^ n) atTop atTop
k : α
hck : 0 < c * k ^ n
hk : 0 ≤ k
⊢ 0 < c

Tactic:
exact pos_of_mul_pos_left hck (pow_nonneg hk _)

Premises used: pow_nonneg, pos_of_mul_pos_left
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n : ℤ
hn : 0 < n
⊢ 0 ≤ n

Tactic:
hn.le

Premises used: LT.lt.le
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n : ℤ
hn : 0 < n
lift :
  ∀ (n : ℕ) (hn : LT.lt (α := ℤ) 0 (↑n : ℤ)), Tendsto (β := α) (fun (x : α) ↦ HPow.hPow (β := ℤ) x (↑n : ℤ)) atTop atTop
⊢ Tendsto (β := α) (fun (x : α) ↦ x ^ n) atTop atTop

Tactic:
lift n to ℕ using hn.le

Premises used: LT.lt.le
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n : ℕ
hn : LT.lt (α := ℤ) 0 (↑n : ℤ)
⊢ Tendsto (β := α) (fun (x : α) ↦ HPow.hPow (β := ℤ) x (↑n : ℤ)) atTop atTop

Tactic:
simp [(Int.natCast_pos.mp hn).ne']

Premises used: LT.lt.ne', Iff.mp, Int.natCast_pos
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k : α
hk : 0 < k
a b : α
h : b ≥ 1
rw rw₁ : a ≤ k * b ↔ a ≤ (fun (b : α) ↦ k * b) b
⊢ a / k ≤ b ↔ a ≤ (fun (b : α) ↦ k * b) b

Tactic:
rw [div_le_iff₀' hk]

Premises used: div_le_iff₀'
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k : α
hk : 0 < k
b : α
h : b ≥ 1
hb : k ≠ 0
⊢ b ≤ (fun (b : α) ↦ k * b) b / k

Tactic:
rw [mul_div_assoc, mul_div_cancel₀]

Premises used: mul_div_assoc, mul_div_cancel₀
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k : α
hk : 0 < k
b : α
h : b ≥ 1
⊢ k ≠ 0

Tactic:
ne_of_gt hk

Premises used: ne_of_gt
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k : α
hk : 0 < k
b : α
h : b ≥ 1
⊢ k ≠ 0

Tactic:
exact ne_of_gt hk

Premises used: ne_of_gt
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : 0 < r
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atBot ↔ Tendsto f l atBot

Tactic:
simpa only [← mul_neg, ← tendsto_neg_atTop_iff] using tendsto_const_mul_atTop_of_pos hr

Premises used: Filter.tendsto_const_mul_atTop_of_pos, Filter.tendsto_neg_atTop_iff, mul_neg
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : 0 < r
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * r) l atBot ↔ Tendsto f l atBot

Tactic:
simpa only [mul_comm] using tendsto_const_mul_atBot_of_pos hr

Premises used: mul_comm, Filter.tendsto_const_mul_atBot_of_pos
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : 0 < r
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x / r) l atBot ↔ Tendsto f l atBot

Tactic:
simp [div_eq_mul_inv, tendsto_mul_const_atBot_of_pos, hr]

Premises used: div_eq_mul_inv, Filter.tendsto_mul_const_atBot_of_pos
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : r < 0
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atTop ↔ Tendsto f l atBot

Tactic:
simpa only [neg_mul, tendsto_neg_atBot_iff] using tendsto_const_mul_atBot_of_pos (neg_pos.2 hr)

Premises used: Iff.mpr, neg_pos, Filter.tendsto_neg_atBot_iff, neg_mul, Filter.tendsto_const_mul_atBot_of_pos
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : r < 0
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * r) l atTop ↔ Tendsto f l atBot

Tactic:
simpa only [mul_comm] using tendsto_const_mul_atTop_of_neg hr

Premises used: Filter.tendsto_const_mul_atTop_of_neg, mul_comm
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : r < 0
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x / r) l atTop ↔ Tendsto f l atBot

Tactic:
simp [div_eq_mul_inv, tendsto_mul_const_atTop_of_neg, hr]

Premises used: Filter.tendsto_mul_const_atTop_of_neg, div_eq_mul_inv
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : r < 0
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atBot ↔ Tendsto f l atTop

Tactic:
simpa only [neg_mul, tendsto_neg_atTop_iff] using tendsto_const_mul_atTop_of_pos (neg_pos.2 hr)

Premises used: Iff.mpr, neg_pos, neg_mul, Filter.tendsto_const_mul_atTop_of_pos, Filter.tendsto_neg_atTop_iff
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : r < 0
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * r) l atBot ↔ Tendsto f l atTop

Tactic:
simpa only [mul_comm] using tendsto_const_mul_atBot_of_neg hr

Premises used: Filter.tendsto_const_mul_atBot_of_neg, mul_comm
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : r < 0
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x / r) l atBot ↔ Tendsto f l atTop

Tactic:
simp [div_eq_mul_inv, tendsto_mul_const_atBot_of_neg, hr]

Premises used: div_eq_mul_inv, Filter.tendsto_mul_const_atBot_of_neg
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
inl :
  ∀ (hr : r < 0),
    Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
inr :
  Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ 0 * f x) l atTop ↔
    LT.lt.{u_1} (α := α) 0 0 ∧ Tendsto f l atTop ∨ LT.lt.{u_1} (α := α) 0 0 ∧ Tendsto f l atBot
inr₁ :
  ∀ (hr : 0 < r),
    Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

Tactic:
rcases lt_trichotomy r 0 with (hr | rfl | hr)

Premises used: OfNat.ofNat, rfl, lt_trichotomy