awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.NonUnitalAlgebra
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : TopologicalSpace A
inst_2 : NonUnitalSemiring A
inst_3 : Module R A
inst_4 : ContinuousConstSMul R A
inst_5 : IsSemitopologicalSemiring A
inst_6 : TopologicalSpace B
inst_7 : NonUnitalSemiring B
inst_8 : Module R B
inst_9 : IsTopologicalSemiring B
inst_10 : ContinuousConstSMul R B
s : NonUnitalSubalgebra R A
φ : A →ₙₐ[R] B
hφ : IsClosedMap.{u_2, u_3} (X := A) (Y := B) (⇑φ : (a : A) → B)
hφ' : Continuous.{u_2, u_3} (X := A) (Y := B) (⇑φ : (a : A) → B)
⊢ Eq.{u_3 + 1} (α := NonUnitalSubalgebra R B) (topologicalClosure (map φ s)) (map φ s.topologicalClosure)

Tactic:
SetLike.coe_injective <| hφ.closure_image_eq_of_continuous hφ' _

Premises used: SetLike.coe_injective, IsClosedMap.closure_image_eq_of_continuous
-- Module: Mathlib.Topology.Algebra.NonUnitalAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : TopologicalSpace A
inst_2 : NonUnitalSemiring A
inst_3 : Module R A
inst_4 : ContinuousConstSMul R A
inst_5 : IsSemitopologicalSemiring A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R A A
inst_8 : T2Space A
s : Set A
⊢ LE.le (α := NonUnitalSubalgebra R A) (topologicalClosure (adjoin R s)) (centralizer R (↑(centralizer R s) : Set A))

Tactic:
topologicalClosure_minimal (adjoin_le_centralizer_centralizer R s) (Set.isClosed_centralizer _)

Premises used: NonUnitalSubalgebra.topologicalClosure_minimal, NonUnitalAlgebra.adjoin_le_centralizer_centralizer, Set.isClosed_centralizer
-- Module: Mathlib.Topology.Algebra.NonUnitalAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace A
inst_2 : NonUnitalRing A
inst_3 : Module R A
inst_4 : ContinuousConstSMul R A
inst_5 : IsTopologicalRing A
s : NonUnitalSubalgebra R A
⊢ IsTopologicalRing.{u_2} ↥s

Tactic:
s.toNonUnitalSubring.instIsTopologicalRing

Premises used: NonUnitalSubring.instIsTopologicalRing, Set.Mem, NonUnitalSubalgebra.toNonUnitalSubring
-- Module: Mathlib.Topology.Algebra.NonUnitalAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace A
inst_2 : NonUnitalRing A
inst_3 : Module R A
inst_4 : ContinuousConstSMul R A
inst_5 : IsSemitopologicalRing A
s : NonUnitalSubalgebra R A
⊢ IsSemitopologicalRing.{u_2} ↥s

Tactic:
s.toNonUnitalSubring.instIsSemitopologicalRing

Premises used: Set.Mem, NonUnitalSubring.instIsSemitopologicalRing, NonUnitalSubalgebra.toNonUnitalSubring
-- Module: Mathlib.Topology.Algebra.NonUnitalAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
inst_5 : TopologicalSpace A
inst_6 : IsSemitopologicalSemiring A
inst_7 : ContinuousConstSMul R A
x : A
⊢ Membership.mem (γ := NonUnitalSubalgebra R A) (elemental R x) x

Tactic:
le_topologicalClosure _ <| self_mem_adjoin_singleton R x

Premises used: NonUnitalAlgebra.self_mem_adjoin_singleton, Set.Mem, NonUnitalSubalgebra.le_topologicalClosure
-- Module: Mathlib.Topology.Algebra.NonUnitalAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
inst_5 : TopologicalSpace A
inst_6 : IsSemitopologicalSemiring A
inst_7 : ContinuousConstSMul R A
x : A
s : NonUnitalSubalgebra R A
hs : IsClosed (↑s : Set A)
hx : x ∈ s
⊢ {x} ⊆ (↑s : Set A)

Tactic:
simpa using hx
-- Module: Mathlib.Topology.Algebra.NonUnitalAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
inst_5 : TopologicalSpace A
inst_6 : IsSemitopologicalSemiring A
inst_7 : ContinuousConstSMul R A
x : A
s : NonUnitalSubalgebra R A
hs : IsClosed (↑s : Set A)
⊢ elemental R x ≤ s ↔ x ∈ s

Tactic:
⟨fun h ↦ h (self_mem R x), fun h ↦ le_of_mem hs h⟩

Premises used: NonUnitalAlgebra.elemental.le_of_mem, Iff.intro, NonUnitalAlgebra.elemental.self_mem
-- Module: Mathlib.Topology.Algebra.NonUnitalAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
inst_5 : TopologicalSpace A
inst_6 : IsSemitopologicalSemiring A
inst_7 : ContinuousConstSMul R A
x : A
⊢ IsClosed (↑(elemental R x) : Set A)

Tactic:
isClosed_topologicalClosure _

Premises used: NonUnitalSubalgebra.isClosed_topologicalClosure
-- Module: Mathlib.Topology.Algebra.NonUnitalAlgebra
Goal:
R : Type u_1
A_1 : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A_1
inst_2 : Module R A_1
inst_3 : IsScalarTower R A_1 A_1
inst_4 : SMulCommClass R A_1 A_1
inst_5 : TopologicalSpace A_1
inst_6 : IsSemitopologicalSemiring A_1
inst_7 : ContinuousConstSMul R A_1
A : Type u_3
inst_8 : UniformSpace A
inst_9 : CompleteSpace A
inst_10 : NonUnitalSemiring A
inst_11 : IsSemitopologicalSemiring A
inst_12 : Module R A
inst_13 : IsScalarTower R A A
inst_14 : SMulCommClass R A A
inst_15 : ContinuousConstSMul R A
x : A
⊢ CompleteSpace.{u_3} ↥(elemental R x)

Tactic:
isClosed_closure.completeSpace_coe

Premises used: Set.Mem, setOf, closure, IsClosed.completeSpace_coe, Set.sInter
-- Module: Mathlib.Topology.Algebra.NonUnitalAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
inst_5 : TopologicalSpace A
inst_6 : IsSemitopologicalSemiring A
inst_7 : ContinuousConstSMul R A
x : A
⊢ IsClosed.{u_2} (X := A)
    (Set.range (ι := ↥(elemental R x))
      (Subtype.val (p := fun (x_1 : A) ↦ Membership.mem (γ := NonUnitalSubalgebra R A) (elemental R x) x_1)))

Tactic:
simpa using isClosed R x

Premises used: NonUnitalAlgebra.elemental.isClosed
-- Module: Mathlib.Topology.Algebra.NonUnitalAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
inst_5 : TopologicalSpace A
inst_6 : IsSemitopologicalSemiring A
inst_7 : ContinuousConstSMul R A
inst_8 : T2Space A
x : A
⊢ LE.le (α := NonUnitalSubalgebra R A) (elemental R x) (centralizer R (↑(centralizer R {x}) : Set A))

Tactic:
topologicalClosure_adjoin_le_centralizer_centralizer R {x}

Premises used: Set.Mem, NonUnitalSubalgebra.topologicalClosure_adjoin_le_centralizer_centralizer, Singleton.singleton
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * g x) l atTop

Tactic:
tendsto_atTop_mono' _ ?_ (hf.atTop_mul_const (half_pos hC))

Premises used: Filter.Tendsto.atTop_mul_const, half_pos, Filter.tendsto_atTop_mono'
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
refine : EventuallyLE.{u_2, u_1} (β := 𝕜) l (fun (x : α) ↦ f x * (C / 2)) fun (x : α) ↦ f x * g x
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * g x) l atTop

Tactic:
refine tendsto_atTop_mono' _ ?_ (hf.atTop_mul_const (half_pos hC))

Premises used: Filter.Tendsto.atTop_mul_const, half_pos, Filter.tendsto_atTop_mono'
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf_1 : Tendsto f l atTop
hg_1 : Tendsto g l (𝓝 C)
x : α
hg : C / 2 < g x
hf : 0 ≤ f x
⊢ f x * (C / 2) ≤ f x * g x

Tactic:
mul_le_mul_of_nonneg_left hg.le hf

Premises used: LT.lt.le, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ C / 2 < g x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ 0 ≤ f x) x} x →
                Membership.mem (γ := Set α)
                  {x : α |
                    (fun (x : α) ↦ LE.le.{u_1} (α := 𝕜) ((fun (x : α) ↦ f x * (C / 2)) x) ((fun (x : α) ↦ f x * g x) x))
                      x}
                  x}
            x}
      a
h₁ h₂ : ∀ (x : α) (hg : C / 2 < g x) (hf : 0 ≤ f x), f x * (C / 2) ≤ f x * g x
⊢ EventuallyLE.{u_2, u_1} (β := 𝕜) l (fun (x : α) ↦ f x * (C / 2)) fun (x : α) ↦ f x * g x

Tactic:
filter_upwards [hg.eventually (lt_mem_nhds (half_lt_self hC)), hf.eventually_ge_atTop 0] with x hg
    hf using mul_le_mul_of_nonneg_left hg.le hf

Premises used: half_lt_self, Filter.Tendsto.eventually, OfNat.ofNat, Filter.Tendsto.eventually_ge_atTop, lt_mem_nhds
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * g x) l atTop

Tactic:
simpa only [mul_comm] using hg.atTop_mul_pos hC hf

Premises used: mul_comm, Filter.Tendsto.atTop_mul_pos
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
⊢ ∀ (i : 𝕜), 0 < i ↔ ((fun (x : 𝕜) ↦ 0 < x) ∘ Inv.inv) i

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
a : 𝕜
ha : 0 < a
⊢ Ioo 0 a = ((fun (i : 𝕜) ↦ Inv.inv '' Ioi i) ∘ Inv.inv) a

Tactic:
simp [inv_Ioi₀ (inv_pos.2 ha)]

Premises used: Iff.mpr, inv_pos, Set.inv_Ioi₀
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
rw : Eq.{u_1 + 1} (α := Filter 𝕜) atTop⁻¹⁻¹ atTop
rw₁ rw₂ : Eq.{u_1 + 1} (α := Filter 𝕜) atTop atTop
⊢ Eq.{u_1 + 1} (α := Filter 𝕜) (𝓝[>] 0)⁻¹ atTop

Tactic:
rw [← inv_atTop₀, inv_inv]

Premises used: inv_atTop₀, inv_inv
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ x⁻¹) (𝓝[>] 0) atTop

Tactic:
inv_nhdsGT_zero.le

Premises used: Set.Mem, Eq.le, inv_nhdsGT_zero, Filter.Tendsto
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
⊢ Tendsto (β := 𝕜) (fun (r : 𝕜) ↦ r⁻¹) atTop (𝓝[>] 0)

Tactic:
inv_atTop₀.le

Premises used: inv_atTop₀, Set.Mem, Eq.le, Filter.Tendsto
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
h : Tendsto (fun (x : 𝕜) ↦ f x⁻¹) atTop l
⊢ Tendsto.{u_1, u_2} (α := 𝕜) ((fun (x : 𝕜) ↦ f x⁻¹) ∘ fun (x : 𝕜) ↦ x⁻¹) (𝓝[>] 0) l

Tactic:
h.comp tendsto_inv_nhdsGT_zero

Premises used: tendsto_inv_nhdsGT_zero, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
h : Tendsto (fun (x : 𝕜) ↦ f x⁻¹) atTop l
h₁ : f = (fun (x : 𝕜) ↦ f x⁻¹) ∘ fun (x : 𝕜) ↦ x⁻¹
⊢ Tendsto f (𝓝[>] 0) l

Tactic:
convert! h.comp tendsto_inv_nhdsGT_zero

Premises used: tendsto_inv_nhdsGT_zero, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
h : Tendsto (fun (x : 𝕜) ↦ f x⁻¹) atTop l
⊢ f = (fun (x : 𝕜) ↦ f x⁻¹) ∘ fun (x : 𝕜) ↦ x⁻¹

Tactic:
grind [inv_inv]

Premises used: inv_inv
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
⊢ Tendsto (β := 𝕜) (fun (r : 𝕜) ↦ r⁻¹) atTop (𝓝 0)

Tactic:
tendsto_inv_atTop_nhdsGT_zero.mono_right inf_le_left

Premises used: tendsto_inv_atTop_nhdsGT_zero, inf_le_left, Filter.Tendsto.mono_right
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f : α → 𝕜
h : Tendsto f l atTop
⊢ Tendsto f⁻¹ l (𝓝 0)

Tactic:
tendsto_inv_atTop_zero.comp h

Premises used: tendsto_inv_atTop_zero, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f : α → 𝕜
h : Tendsto f l (𝓝[>] 0)
⊢ Tendsto f⁻¹ l atTop

Tactic:
tendsto_inv_nhdsGT_zero.comp h

Premises used: tendsto_inv_nhdsGT_zero, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℕ
hn : n ≠ 0
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ HPow.hPow (β := ℤ) x (-(↑n : ℤ))) atTop (𝓝 0)

Tactic:
simpa only [zpow_neg, zpow_natCast] using (tendsto_pow_atTop (α := 𝕜) hn).inv_tendsto_atTop

Premises used: zpow_natCast, zpow_neg, Filter.Tendsto.inv_tendsto_atTop, Filter.tendsto_pow_atTop
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℤ
hn : n < 0
⊢ 0 ≤ -n

Tactic:
le_of_lt (neg_pos.mpr hn)

Premises used: Iff.mpr, neg_pos, le_of_lt
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℤ
hn : n < 0
lift : ∀ (N : ℕ) (h : (↑N : ℤ) = -n), Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) atTop (𝓝 0)
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) atTop (𝓝 0)

Tactic:
lift -n to ℕ using le_of_lt (neg_pos.mpr hn) with N h

Premises used: Iff.mpr, neg_pos, le_of_lt
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℤ
hn : n < 0
N : ℕ
h : (↑N : ℤ) = -n
rw : ∀ (N : ℕ) (hn : 0 < N) (h : (↑N : ℤ) = -n), Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) atTop (𝓝 0)
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) atTop (𝓝 0)

Tactic:
rw [← neg_pos, ← h, Nat.cast_pos] at hn

Premises used: Nat.cast_pos, neg_pos
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℤ
N : ℕ
hn : 0 < N
h : (↑N : ℤ) = -n
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) atTop (𝓝 0)

Tactic:
simpa only [h, neg_neg] using tendsto_pow_neg_atTop hn.ne'

Premises used: neg_neg, LT.lt.ne', tendsto_pow_neg_atTop
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
inst_5 : ContinuousMul 𝕜
⊢ (∀ a' < 1, ∀ᶠ (b : 𝕜) in 𝓝 1, a' < b⁻¹) ∧ ∀ a' > 1, ∀ᶠ (b : 𝕜) in 𝓝 1, b⁻¹ < a'

Tactic:
⟨fun x hx => ?_, fun x hx => ?_⟩

Premises used: And.intro
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
inst_5 : ContinuousMul 𝕜
refine_1 : ∀ (x : 𝕜) (hx : x < 1), ∀ᶠ (b : 𝕜) in 𝓝 1, x < b⁻¹
refine_2 : ∀ (x : 𝕜) (hx : x > 1), ∀ᶠ (b : 𝕜) in 𝓝 1, b⁻¹ < x
⊢ (∀ a' < 1, ∀ᶠ (b : 𝕜) in 𝓝 1, a' < b⁻¹) ∧ ∀ a' > 1, ∀ᶠ (b : 𝕜) in 𝓝 1, b⁻¹ < a'

Tactic:
refine ⟨fun x hx => ?_, fun x hx => ?_⟩
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
inst_5 : ContinuousMul 𝕜
x : 𝕜
hx : x < 1
⊢ ∃ (x' : 𝕜), 0 < x' ∧ x ≤ x' ∧ x' < 1

Tactic:
⟨max x (1 / 2), one_half_pos.trans_le (le_max_right _ _), le_max_left _ _,
        max_lt hx one_half_lt_one⟩

Premises used: le_max_right, one_half_lt_one, HDiv.hDiv, max_lt, one_half_pos, Max.max, LT.lt.trans_le, And.intro, Exists.intro, OfNat.ofNat, le_max_left
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
inst_5 : ContinuousMul 𝕜
x : 𝕜
hx : x < 1
refine_1 : ∀ (x' : 𝕜) (h₀ : 0 < x') (hxx' : x ≤ x') (h₁ : x' < 1), ∀ᶠ (b : 𝕜) in 𝓝 1, x < b⁻¹
⊢ ∀ᶠ (b : 𝕜) in 𝓝 1, x < b⁻¹

Tactic:
obtain ⟨x', h₀, hxx', h₁⟩ : ∃ x', 0 < x' ∧ x ≤ x' ∧ x' < 1 :=
      ⟨max x (1 / 2), one_half_pos.trans_le (le_max_right _ _), le_max_left _ _,
        max_lt hx one_half_lt_one⟩
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
inst_5 : ContinuousMul 𝕜
x : 𝕜
hx : x < 1
x' : 𝕜
h₀ : 0 < x'
hxx' : x ≤ x'
h₁ : x' < 1
h : ∀ (y : 𝕜) (hy : y ∈ Ioo 0 x'⁻¹), x < y⁻¹
⊢ ∀ᶠ (b : 𝕜) in 𝓝 1, x < b⁻¹

Tactic:
filter_upwards [Ioo_mem_nhds one_pos ((one_lt_inv₀ h₀).2 h₁)] with y hy

Premises used: Iff.mpr, Ioo_mem_nhds, one_pos, one_lt_inv₀
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
inst_5 : ContinuousMul 𝕜
x : 𝕜
hx : x < 1
x' : 𝕜
h₀ : 0 < x'
hxx' : x ≤ x'
h₁ : x' < 1
y : 𝕜
hy : y ∈ Ioo 0 x'⁻¹
⊢ x < y⁻¹

Tactic:
hxx'.trans_lt <| lt_inv_of_lt_inv₀ hy.1 hy.2

Premises used: lt_inv_of_lt_inv₀, And.right, And.left, LE.le.trans_lt
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
inst_5 : ContinuousMul 𝕜
x : 𝕜
hx : x < 1
x' : 𝕜
h₀ : 0 < x'
hxx' : x ≤ x'
h₁ : x' < 1
y : 𝕜
hy : y ∈ Ioo 0 x'⁻¹
⊢ x < y⁻¹

Tactic:
exact hxx'.trans_lt <| lt_inv_of_lt_inv₀ hy.1 hy.2

Premises used: lt_inv_of_lt_inv₀, And.right, And.left, LE.le.trans_lt
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
inst_5 : ContinuousMul 𝕜
x : 𝕜
hx : x > 1
h : ∀ (y : 𝕜) (hy : y ∈ Ioi x⁻¹), y⁻¹ < x
⊢ ∀ᶠ (b : 𝕜) in 𝓝 1, b⁻¹ < x

Tactic:
filter_upwards [Ioi_mem_nhds (inv_lt_one_of_one_lt₀ hx)] with y hy

Premises used: Ioi_mem_nhds, inv_lt_one_of_one_lt₀
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
inst_5 : ContinuousMul 𝕜
x : 𝕜
hx : x > 1
y : 𝕜
hy : y ∈ Ioi x⁻¹
⊢ 0 < x

Tactic:
positivity
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
inst_5 : ContinuousMul 𝕜
x : 𝕜
hx : x > 1
y : 𝕜
hy : y ∈ Ioi x⁻¹
⊢ y⁻¹ < x

Tactic:
exact inv_lt_of_inv_lt₀ (by positivity) hy

Premises used: inv_lt_of_inv_lt₀
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
R : Type u_1
𝕜 : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : TopologicalSpace R
inst_5 : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : HasBasis.{u_1, u_2 + 1} (α := R) (𝓝 0) (fun (x : 𝕜) ↦ 0 < x) fun (ε : 𝕜) ↦ {x : R | norm x < ε}
⊢ ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)

Tactic:
fun f c c0 hf ↦ (nhds_basis.tendsto_iff nhds_basis).2 fun ε ε0 ↦ ?_

Premises used: Iff.mpr, Filter.HasBasis.tendsto_iff
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
R : Type u_1
𝕜 : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : TopologicalSpace R
inst_5 : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : HasBasis.{u_1, u_2 + 1} (α := R) (𝓝 0) (fun (x : 𝕜) ↦ 0 < x) fun (ε : 𝕜) ↦ {x : R | norm x < ε}
refine :
  ∀ (f : R → R) (c : 𝕜) (c0 : c ≥ 0) (hf : ∀ (x : R), norm (f x) ≤ c * norm x) (ε : 𝕜) (ε0 : 0 < ε),
    ∃ (ia : 𝕜),
      0 < ia ∧
        ∀ (x : R),
          Membership.mem (γ := Set R) {x : R | norm x < ia} x → Membership.mem (γ := Set R) {x : R | norm x < ε} (f x)
⊢ ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)

Tactic:
refine fun f c c0 hf ↦ (nhds_basis.tendsto_iff nhds_basis).2 fun ε ε0 ↦ ?_

Premises used: Iff.mpr, Filter.HasBasis.tendsto_iff
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
R : Type u_1
𝕜 : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : TopologicalSpace R
inst_5 : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : HasBasis.{u_1, u_2 + 1} (α := R) (𝓝 0) (fun (x : 𝕜) ↦ 0 < x) fun (ε : 𝕜) ↦ {x : R | norm x < ε}
f : R → R
c : 𝕜
c0 : c ≥ 0
hf : ∀ (x : R), norm (f x) ≤ c * norm x
ε : 𝕜
ε0 : 0 < ε
rcases :
  ∀ (δ : 𝕜) (δ0 : 0 < δ) (hδ : c * δ < ε),
    ∃ (ia : 𝕜),
      0 < ia ∧
        ∀ (x : R),
          Membership.mem (γ := Set R) {x : R | norm x < ia} x → Membership.mem (γ := Set R) {x : R | norm x < ε} (f x)
⊢ ∃ (ia : 𝕜),
    0 < ia ∧
      ∀ (x : R),
        Membership.mem (γ := Set R) {x : R | norm x < ia} x → Membership.mem (γ := Set R) {x : R | norm x < ε} (f x)

Tactic:
rcases exists_pos_mul_lt ε0 c with ⟨δ, δ0, hδ⟩

Premises used: exists_pos_mul_lt
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
R : Type u_1
𝕜 : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : TopologicalSpace R
inst_5 : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : HasBasis.{u_1, u_2 + 1} (α := R) (𝓝 0) (fun (x : 𝕜) ↦ 0 < x) fun (ε : 𝕜) ↦ {x : R | norm x < ε}
f : R → R
c : 𝕜
c0 : c ≥ 0
hf : ∀ (x : R), norm (f x) ≤ c * norm x
ε : 𝕜
ε0 : 0 < ε
δ : 𝕜
δ0 : 0 < δ
hδ : c * δ < ε
⊢ ∃ (ia : 𝕜),
    0 < ia ∧
      ∀ (x : R),
        Membership.mem (γ := Set R) {x : R | norm x < ia} x → Membership.mem (γ := Set R) {x : R | norm x < ε} (f x)

Tactic:
⟨δ, δ0, fun x hx ↦ (hf _).trans_lt ?_⟩

Premises used: And.intro, Exists.intro, LE.le.trans_lt