awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 * δ < ε
refine : ∀ (x : R) (hx : Membership.mem (γ := Set R) {x : R | norm x < δ} x), c * norm 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:
refine ⟨δ, δ0, fun x hx ↦ (hf _).trans_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 * δ < ε
x : R
hx : Membership.mem (γ := Set R) {x : R | norm x < δ} x
⊢ c * norm x < ε

Tactic:
(mul_le_mul_of_nonneg_left (le_of_lt hx) c0).trans_lt hδ

Premises used: le_of_lt, LE.le.trans_lt, mul_le_mul_of_nonneg_left
-- 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 * δ < ε
x : R
hx : Membership.mem (γ := Set R) {x : R | norm x < δ} x
⊢ c * norm x < ε

Tactic:
exact (mul_le_mul_of_nonneg_left (le_of_lt hx) c0).trans_lt hδ

Premises used: le_of_lt, LE.le.trans_lt, mul_le_mul_of_nonneg_left
-- 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:
have h0 : ∀ f : R → R, ∀ c ≥ (0 : 𝕜), (∀ x, norm (f x) ≤ c * norm x) →
      Tendsto f (𝓝 0) (𝓝 0) := by
    refine fun f c c0 hf ↦ (nhds_basis.tendsto_iff nhds_basis).2 fun ε ε0 ↦ ?_
    rcases exists_pos_mul_lt ε0 c with ⟨δ, δ0, hδ⟩
    refine ⟨δ, δ0, fun x hx ↦ (hf _).trans_lt ?_⟩
    exact (mul_le_mul_of_nonneg_left (le_of_lt hx) c0).trans_lt hδ
-- 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 < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
apply :
  Tendsto (β := R) (uncurry fun (x1 x2 : R) ↦ x1 * x2) (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)) (𝓝 0)
apply₁ : ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ x₀ * x) (𝓝 0) (𝓝 0)
apply₂ : ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ x * x₀) (𝓝 0) (𝓝 0)
⊢ IsTopologicalRing R

Tactic:
apply IsTopologicalRing.of_addGroup_of_nhds_zero

Premises used: IsTopologicalRing.of_addGroup_of_nhds_zero
-- 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 < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ Tendsto (β := R) (uncurry fun (x1 x2 : R) ↦ x1 * x2) (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)) (𝓝 0)

Tactic:
((nhds_basis.prod nhds_basis).tendsto_iff nhds_basis).2 fun ε ε0 ↦ ?_

Premises used: Iff.mpr, Filter.HasBasis.tendsto_iff, Filter.HasBasis.prod
-- 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 < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
refine :
  ∀ (ε : 𝕜) (ε0 : 0 < ε),
    ∃ (ia : 𝕜 × 𝕜),
      (0 < ia.1 ∧ 0 < ia.2) ∧
        ∀ x ∈ SProd.sprod (α := Set R) (β := Set R) {x : R | norm x < ia.1} {x : R | norm x < ia.2},
          Membership.mem (γ := Set R) {x : R | norm x < ε} (uncurry (fun (x1 x2 : R) ↦ x1 * x2) x)
⊢ Tendsto (β := R) (uncurry fun (x1 x2 : R) ↦ x1 * x2) (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)) (𝓝 0)

Tactic:
refine ((nhds_basis.prod nhds_basis).tendsto_iff nhds_basis).2 fun ε ε0 ↦ ?_

Premises used: Iff.mpr, Filter.HasBasis.tendsto_iff, Filter.HasBasis.prod
-- 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 < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
ε : 𝕜
ε0 : 0 < ε
⊢ ∃ (ia : 𝕜 × 𝕜),
    (0 < ia.1 ∧ 0 < ia.2) ∧
      ∀ x ∈ SProd.sprod (α := Set R) (β := Set R) {x : R | norm x < ia.1} {x : R | norm x < ia.2},
        Membership.mem (γ := Set R) {x : R | norm x < ε} (uncurry (fun (x1 x2 : R) ↦ x1 * x2) x)

Tactic:
⟨(1, ε), ⟨one_pos, ε0⟩, fun (x, y) ⟨hx, hy⟩ => ?_⟩

Premises used: HMul.hMul, setOf, Membership.mem, Prod.mk, _private.0.IsTopologicalRing.of_norm.match_1, And.intro, LT.lt, Exists.intro, Function.uncurry, OfNat.ofNat, one_pos, _private.0.IsTopologicalRing.of_norm.match_2
-- 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 < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
ε : 𝕜
ε0 : 0 < ε
refine :
  ∀ (x : R × R) (x y : R),
    (x, y) ∈ SProd.sprod (α := Set R) (β := Set R) {x : R | norm x < (1, ε).1} {x : R | norm x < (1, ε).2} →
      ∀ (hx : Membership.mem (γ := Set R) {x : R | norm x < (1, ε).1} (x, y).1)
        (hy : Membership.mem (γ := Set R) {x : R | norm x < (1, ε).2} (x, y).2),
        Membership.mem (γ := Set R) {x : R | norm x < ε} (uncurry (fun (x1 x2 : R) ↦ x1 * x2) (x, y))
⊢ ∃ (ia : 𝕜 × 𝕜),
    (0 < ia.1 ∧ 0 < ia.2) ∧
      ∀ x ∈ SProd.sprod (α := Set R) (β := Set R) {x : R | norm x < ia.1} {x : R | norm x < ia.2},
        Membership.mem (γ := Set R) {x : R | norm x < ε} (uncurry (fun (x1 x2 : R) ↦ x1 * x2) x)

Tactic:
refine ⟨(1, ε), ⟨one_pos, ε0⟩, fun (x, y) ⟨hx, hy⟩ => ?_⟩
-- 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 < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
ε : 𝕜
ε0 : 0 < ε
x_1 : R × R
x y : R
h : (x, y) ∈ SProd.sprod (α := Set R) (β := Set R) {x : R | norm x < 1} {x : R | norm x < ε}
hx : Membership.mem (γ := Set R) {x : R | norm x < 1} x
hy : Membership.mem (γ := Set R) {x : R | norm x < ε} y
⊢ norm (x * y) ≤ norm x * norm y

Tactic:
norm_mul_le _ _
-- 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 < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
ε : 𝕜
ε0 : 0 < ε
x_1 : R × R
x y : R
h : (x, y) ∈ SProd.sprod (α := Set R) (β := Set R) {x : R | norm x < 1} {x : R | norm x < ε}
hx : Membership.mem (γ := Set R) {x : R | norm x < 1} x
hy : Membership.mem (γ := Set R) {x : R | norm x < ε} y
⊢ norm x * norm y < ε

Tactic:
(mul_le_of_le_one_left (norm_nonneg _) hx.le).trans_lt hy

Premises used: LT.lt.le, mul_le_of_le_one_left, LE.le.trans_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 < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
ε : 𝕜
ε0 : 0 < ε
x_1 : R × R
x y : R
h : (x, y) ∈ SProd.sprod (α := Set R) (β := Set R) {x : R | norm x < 1} {x : R | norm x < ε}
hx : Membership.mem (γ := Set R) {x : R | norm x < 1} x
hy : Membership.mem (γ := Set R) {x : R | norm x < ε} y
⊢ Membership.mem (γ := Set R) {x : R | norm x < ε} (uncurry (fun (x1 x2 : R) ↦ x1 * x2) (x, y))

Tactic:
calc norm (x * y) ≤ norm x * norm y := norm_mul_le _ _
    _ < ε := (mul_le_of_le_one_left (norm_nonneg _) hx.le).trans_lt hy

Premises used: HMul.hMul, LT.lt.le, mul_le_of_le_one_left, LE.le.trans_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 < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ Tendsto (β := R) (uncurry fun (x1 x2 : R) ↦ x1 * x2) (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)) (𝓝 0)

Tactic:
case hmul =>
    refine ((nhds_basis.prod nhds_basis).tendsto_iff nhds_basis).2 fun ε ε0 ↦ ?_
    refine ⟨(1, ε), ⟨one_pos, ε0⟩, fun (x, y) ⟨hx, hy⟩ => ?_⟩
    simp only at *
    calc norm (x * y) ≤ norm x * norm y := norm_mul_le _ _
    _ < ε := (mul_le_of_le_one_left (norm_nonneg _) hx.le).trans_lt hy

Premises used: Iff.mpr, Filter.HasBasis.tendsto_iff, Filter.HasBasis.prod
-- 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 < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ x₀ * x) (𝓝 0) (𝓝 0)

Tactic:
fun x => h0 _ (norm x) (norm_nonneg _) (norm_mul_le x)

Premises used: HMul.hMul
-- 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 < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ x₀ * x) (𝓝 0) (𝓝 0)

Tactic:
exact fun x => h0 _ (norm x) (norm_nonneg _) (norm_mul_le x)

Premises used: HMul.hMul
-- 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 < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ x₀ * x) (𝓝 0) (𝓝 0)

Tactic:
case hmul_left => exact fun x => h0 _ (norm x) (norm_nonneg _) (norm_mul_le x)

Premises used: HMul.hMul
-- 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 < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ x * x₀) (𝓝 0) (𝓝 0)

Tactic:
fun y => h0 (· * y) (norm y) (norm_nonneg y) fun x =>
      (norm_mul_le x y).trans_eq (mul_comm _ _)

Premises used: HMul.hMul, LE.le.trans_eq, mul_comm
-- 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 < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ x * x₀) (𝓝 0) (𝓝 0)

Tactic:
exact fun y => h0 (· * y) (norm y) (norm_nonneg y) fun x =>
      (norm_mul_le x y).trans_eq (mul_comm _ _)

Premises used: HMul.hMul, LE.le.trans_eq, mul_comm
-- 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 < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ x * x₀) (𝓝 0) (𝓝 0)

Tactic:
case hmul_right =>
    exact fun y => h0 (· * y) (norm y) (norm_nonneg y) fun x =>
      (norm_mul_le x y).trans_eq (mul_comm _ _)

Premises used: HMul.hMul, LE.le.trans_eq, mul_comm
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
⊢ HasBasis (α := 𝕜) (𝓝 0) (fun (x : 𝕜) ↦ 0 < x) fun (ε : 𝕜) ↦ {x : 𝕜 | |x| < ε}

Tactic:
simpa using nhds_basis_abs_sub_lt (0 : 𝕜)

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

Tactic:
have := hf.atTop_mul_pos (neg_pos.2 hC) hg.neg
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
this : Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * -g x) l atTop
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * g x) l atBot

Tactic:
simpa only [Function.comp_def, neg_mul_eq_mul_neg, neg_neg] using
    tendsto_neg_atTop_atBot.comp this

Premises used: Filter.tendsto_neg_atTop_atBot, neg_neg, Function.comp_def, neg_mul_eq_mul_neg, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * g x) l atBot

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

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

Tactic:
have := (tendsto_neg_atBot_atTop.comp hf).atTop_mul_pos hC hg
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
this : Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ (Neg.neg ∘ f) x * g x) l atTop
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * g x) l atBot

Tactic:
simpa [Function.comp_def] using tendsto_neg_atTop_atBot.comp this

Premises used: Filter.tendsto_neg_atTop_atBot, Function.comp_def, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ (Neg.neg ∘ f) x * g x) l atBot

Tactic:
have := (tendsto_neg_atBot_atTop.comp hf).atTop_mul_neg hC hg
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
this : Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ (Neg.neg ∘ f) x * g x) l atBot
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * g x) l atTop

Tactic:
simpa [Function.comp_def] using tendsto_neg_atBot_atTop.comp this

Premises used: Filter.tendsto_neg_atBot_atTop, Function.comp_def, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
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 atBot
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * g x) l atBot

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

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

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

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

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

Tactic:
simp [inv_Iio₀ (inv_neg''.2 ha)]

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

Tactic:
rw [← inv_atBot₀, inv_inv]

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

Tactic:
inv_nhdsLT_zero.le

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

Tactic:
h.comp tendsto_inv_nhdsLT_zero

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

Tactic:
convert! h.comp tendsto_inv_nhdsLT_zero

Premises used: tendsto_inv_nhdsLT_zero, Filter.Tendsto.comp