awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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⁻¹
⊢ (∀ a' < 1, ∀ᶠ (b : 𝕜) in 𝓝 1, a' < b⁻¹) ∧ ∀ a' > 1, ∀ᶠ (b : 𝕜) in 𝓝 1, b⁻¹ < a'
have refine_2 : ∀ (x : 𝕜) (hx : x > 1), ∀ᶠ (b : 𝕜) in 𝓝 1, b⁻¹ < x
Tactic: refine ⟨fun x hx => ?_, fun x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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
⊢ ∀ᶠ (b : 𝕜) in 𝓝 1, x < b⁻¹
have refine_1 : ∀ (x' : 𝕜) (h₀ : 0 < x') (hxx' : x ≤ x') (h₁ : x' < 1), ∀ᶠ (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⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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
⊢ ∀ᶠ (b : 𝕜) in 𝓝 1, x < b⁻¹
have h : ∀ (y : 𝕜) (hy : y ∈ Ioo 0 x'⁻¹), x < y⁻¹
Tactic: filter_upwards [Ioo_mem_nhds one_pos ((one_lt_inv₀ h₀).2 h₁)] with y hy
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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
⊢ ∀ᶠ (b : 𝕜) in 𝓝 1, b⁻¹ < x
have h : ∀ (y : 𝕜) (hy : y ∈ Ioi x⁻¹), y⁻¹ < x
Tactic: filter_upwards [Ioi_mem_nhds (inv_lt_one_of_one_lt₀ hx)] with y hy
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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)
have 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)
Tactic: refine fun f c c0 hf ↦ (nhds_basis.tendsto_iff nhds_basis).2 fun ε ε0 ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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 < ε
⊢ ∃ (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)
have 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)
Tactic: rcases exists_pos_mul_lt ε0 c with ⟨δ, δ0, hδ⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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)
have refine : ∀ (x : R) (hx : Membership.mem (γ := Set R) {x : R | norm x < δ} x), c * norm x < ε
Tactic: refine ⟨δ, δ0, fun x hx ↦ (hf _).trans_lt ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (hypothesis)
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 < ε}
⊢ IsTopologicalRing R
have h0 : ∀ (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δ
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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)
⊢ IsTopologicalRing R
have apply : Tendsto (β := R) (uncurry fun (x1 x2 : R) ↦ x1 * x2) (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)) (𝓝 0)
Tactic: apply IsTopologicalRing.of_addGroup_of_nhds_zero
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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)
⊢ IsTopologicalRing R
have apply₁ : ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ x₀ * x) (𝓝 0) (𝓝 0)
Tactic: apply IsTopologicalRing.of_addGroup_of_nhds_zero
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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)
⊢ IsTopologicalRing R
have apply₂ : ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ x * x₀) (𝓝 0) (𝓝 0)
Tactic: apply IsTopologicalRing.of_addGroup_of_nhds_zero
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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)
have 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)
Tactic: refine ((nhds_basis.prod nhds_basis).tendsto_iff nhds_basis).2 fun ε ε0 ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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)
have 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))
Tactic: refine ⟨(1, ε), ⟨one_pos, ε0⟩, fun (x, y) ⟨hx, hy⟩ => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (hypothesis)
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 atBot
have this : 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (hypothesis)
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 : α) ↦ f x * g x) l atBot
have this : 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (hypothesis)
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 : α) ↦ f x * g x) l atTop
have this : 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
⊢ Eq.{u_1 + 1} (α := Filter 𝕜) (𝓝[<] 0)⁻¹ atBot
have rw : Eq.{u_1 + 1} (α := Filter 𝕜) atBot⁻¹⁻¹ atBot
Tactic: rw [← inv_atBot₀, inv_inv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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
⊢ Eq.{u_1 + 1} (α := Filter 𝕜) (𝓝[<] 0)⁻¹ atBot
have rw₁ : Eq.{u_1 + 1} (α := Filter 𝕜) atBot atBot
Tactic: rw [← inv_atBot₀, inv_inv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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 f (𝓝[<] 0) l
have h₁ : f = (fun (x : 𝕜) ↦ f x⁻¹) ∘ fun (x : 𝕜) ↦ x⁻¹
Tactic: convert! h.comp tendsto_inv_nhdsLT_zero
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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 : α → 𝕜
a : 𝕜
h : Tendsto f l (𝓝 a)
hg : Tendsto g l atTop
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x / g x) l (𝓝 0)
have simp : Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * (g x)⁻¹) l (𝓝 0)
Tactic: simp only [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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 : α → 𝕜
a : 𝕜
h : Tendsto f l (𝓝 a)
hg : Tendsto g l atBot
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x / g x) l (𝓝 0)
have simp : Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * (g x)⁻¹) l (𝓝 0)
Tactic: simp only [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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 : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * g x) l (𝓝 0)
have rw : Tendsto.{u_2, u_1} (β := 𝕜) (abs ∘ fun (x : α) ↦ f x * g x) l (𝓝 0)
Tactic: rw [tendsto_zero_iff_abs_tendsto_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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 : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ |C * g x|) l (𝓝 0)
have h : 0 = |C * 0|
Tactic: convert! (hg.const_mul C).abs
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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 : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
⊢ 0 = |C * 0|
have h : Eq.{u_1 + 1} (α := 𝕜) 0 |0|
Tactic: simp_rw [mul_zero, abs_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (hypothesis)
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 : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (abs ∘ fun (x : α) ↦ f x * g x) l (𝓝 0)
have hC : Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ |C * g x|) l (𝓝 0)
Tactic: have hC : Tendsto (fun x ↦ |C * g x|) l (𝓝 0) := by
    convert! (hg.const_mul C).abs
    simp_rw [mul_zero, abs_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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 : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ |C * g x|) l (𝓝 0)
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (abs ∘ fun (x : α) ↦ f x * g x) l (𝓝 0)
have hgf : ∀ᶠ (b : α) in l, LE.le.{u_1} (α := 𝕜) 0 ((abs ∘ fun (x : α) ↦ f x * g x) b)
Tactic: apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hC
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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 : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ |C * g x|) l (𝓝 0)
hgf : ∀ᶠ (b : α) in l, LE.le.{u_1} (α := 𝕜) 0 ((abs ∘ fun (x : α) ↦ f x * g x) b)
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (abs ∘ fun (x : α) ↦ f x * g x) l (𝓝 0)
have hfh : ∀ᶠ (b : α) in l, (abs ∘ fun (x : α) ↦ f x * g x) b ≤ |C * g b|
Tactic: apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hC
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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 : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ |C * g x|) l (𝓝 0)
⊢ ∀ᶠ (b : α) in l, LE.le.{u_1} (α := 𝕜) 0 ((abs ∘ fun (x : α) ↦ f x * g x) b)
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ |f x| ≤ C) x} x →
        Membership.mem (γ := Set α)
          {x : α | (fun (b : α) ↦ LE.le.{u_1} (α := 𝕜) 0 ((abs ∘ fun (x : α) ↦ f x * g x) b)) x} x}
    a
Tactic: filter_upwards [hf] with x _ using abs_nonneg _
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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 : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ |C * g x|) l (𝓝 0)
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ |f x| ≤ C) x} x →
          Membership.mem (γ := Set α)
            {x : α | (fun (b : α) ↦ LE.le.{u_1} (α := 𝕜) 0 ((abs ∘ fun (x : α) ↦ f x * g x) b)) x} x}
      a
⊢ ∀ᶠ (b : α) in l, LE.le.{u_1} (α := 𝕜) 0 ((abs ∘ fun (x : α) ↦ f x * g x) b)
have h₁ : ∀ (a : α), |f a| ≤ C → LE.le.{u_1} (α := 𝕜) 0 ((abs ∘ fun (x : α) ↦ f x * g x) a)
Tactic: filter_upwards [hf] with x _ using abs_nonneg _
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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 : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ |C * g x|) l (𝓝 0)
⊢ ∀ᶠ (b : α) in l, (abs ∘ fun (x : α) ↦ f x * g x) b ≤ |C * g b|
have h : ∀ (x : α) (hx : |f x| ≤ C), (abs ∘ fun (x : α) ↦ f x * g x) x ≤ |C * g x|
Tactic: filter_upwards [hf] with x hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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 : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ |C * g x|) l (𝓝 0)
x : α
hx : |f x| ≤ C
⊢ (abs ∘ fun (x : α) ↦ f x * g x) x ≤ |C * g x|
have h : |f x| * |g x| ≤ |C| * |g x|
Tactic: simp only [comp_apply, abs_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (hypothesis)
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 : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l (𝓝 0)
C : 𝕜 := max |b| |B|
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * g x) l (𝓝 0)
have hbC : -C ≤ b
Tactic: have hbC : -C ≤ b := neg_le.mpr (le_max_of_le_left (neg_le_abs b))
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (hypothesis)
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 : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l (𝓝 0)
C : 𝕜 := max |b| |B|
hbC : -C ≤ b
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * g x) l (𝓝 0)
have hBC : B ≤ C
Tactic: have hBC : B ≤ C := le_max_of_le_right (le_abs_self B)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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 : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l (𝓝 0)
C : 𝕜 := max |b| |B|
hbC : -C ≤ b
hBC : B ≤ C
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * g x) l (𝓝 0)
have apply : ∀ᶠ (x : α) in l, |f x| ≤ C
Tactic: apply bdd_le_mul_tendsto_zero' C _ hg
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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 : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l (𝓝 0)
C : 𝕜 := max |b| |B|
hbC : -C ≤ b
hBC : B ≤ C
⊢ ∀ᶠ (x : α) in l, |f x| ≤ C
have h : ∀ (a : α), b ≤ f a → f a ≤ B → |f a| ≤ C
Tactic: filter_upwards [hb, hB]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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 : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l atTop
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x / g x) l (𝓝 0)
have simp : Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * (g x)⁻¹) l (𝓝 0)
Tactic: simp only [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℕ
c d : 𝕜
⊢ Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
have inl : Tendsto (fun (x : 𝕜) ↦ c * HPow.hPow (β := ℕ) x 0) atTop (𝓝 d) ↔ (c = 0 ∨ Eq (α := ℕ) 0 0) ∧ c = d
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℕ
c d : 𝕜
inl : Tendsto (fun (x : 𝕜) ↦ c * HPow.hPow (β := ℕ) x 0) atTop (𝓝 d) ↔ (c = 0 ∨ Eq (α := ℕ) 0 0) ∧ c = d
⊢ Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
have inr : ∀ (hn : n ≠ 0), Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
Tactic: rcases eq_or_ne n 0 with (rfl | hn)