awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : IsLinearTopology R M
ι : Type u_4
f : Filter ι
a : ι → R
m : ι → M
ha : Tendsto m f (𝓝 0)
rw :
  ∀
    (ha :
      ∀ (i : Submodule R M), Membership.mem (γ := Filter M) (𝓝 0) (↑i : Set M) → ∀ᶠ (x : ι) in f, m x ∈ (↑i : Set M))
    (i : Submodule R M), Membership.mem (γ := Filter M) (𝓝 0) (↑i : Set M) → ∀ᶠ (x : ι) in f, (a • m) x ∈ (↑i : Set M)
⊢ Tendsto (a • m) f (𝓝 0)

Tactic:
rw [hasBasis_submodule R |>.tendsto_right_iff] at ha ⊢

Premises used: IsLinearTopology.hasBasis_submodule, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : IsLinearTopology R M
ι : Type u_4
f : Filter ι
a : ι → R
m : ι → M
ha : ∀ (i : Submodule R M), Membership.mem (γ := Filter M) (𝓝 0) (↑i : Set M) → ∀ᶠ (x : ι) in f, m x ∈ (↑i : Set M)
I : Submodule R M
hI : Membership.mem (γ := Filter M) (𝓝 0) (↑I : Set M)
h : ∀ (i : ι) (ai_mem : m i ∈ (↑I : Set M)), (a • m) i ∈ (↑I : Set M)
⊢ ∀ᶠ (x : ι) in f, (a • m) x ∈ (↑I : Set M)

Tactic:
filter_upwards [ha I hI] with i ai_mem
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : IsLinearTopology R M
ι : Type u_4
f : Filter ι
a : ι → R
m : ι → M
ha : ∀ (i : Submodule R M), Membership.mem (γ := Filter M) (𝓝 0) (↑i : Set M) → ∀ᶠ (x : ι) in f, m x ∈ (↑i : Set M)
I : Submodule R M
hI : Membership.mem (γ := Filter M) (𝓝 0) (↑I : Set M)
i : ι
ai_mem : m i ∈ (↑I : Set M)
⊢ (a • m) i ∈ (↑I : Set M)

Tactic:
I.smul_mem _ ai_mem

Premises used: Set.Mem, Submodule.smul_mem
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : IsLinearTopology R M
ι : Type u_4
f : Filter ι
a : ι → R
m : ι → M
ha : ∀ (i : Submodule R M), Membership.mem (γ := Filter M) (𝓝 0) (↑i : Set M) → ∀ᶠ (x : ι) in f, m x ∈ (↑i : Set M)
I : Submodule R M
hI : Membership.mem (γ := Filter M) (𝓝 0) (↑I : Set M)
i : ι
ai_mem : m i ∈ (↑I : Set M)
⊢ (a • m) i ∈ (↑I : Set M)

Tactic:
exact I.smul_mem _ ai_mem

Premises used: Submodule.smul_mem
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : Module.{u_1, u_3} Rᵐᵒᵖ M
inst_5 : IsCentralScalar R M
mp : IsLinearTopology.{u_1, u_3} Rᵐᵒᵖ M → IsLinearTopology R M
mpr : IsLinearTopology R M → IsLinearTopology.{u_1, u_3} Rᵐᵒᵖ M
⊢ IsLinearTopology.{u_1, u_3} Rᵐᵒᵖ M ↔ IsLinearTopology R M

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : Module.{u_1, u_3} Rᵐᵒᵖ M
inst_5 : IsCentralScalar R M
H : IsLinearTopology.{u_1, u_3} Rᵐᵒᵖ M
⊢ IsLinearTopology R M

Tactic:
mk_of_hasBasis' R (IsLinearTopology.hasBasis_submodule Rᵐᵒᵖ)
      fun S r m hm ↦ op_smul_eq_smul r m ▸ S.smul_mem _ hm

Premises used: IsLinearTopology.mk_of_hasBasis', MulOpposite, IsLinearTopology.hasBasis_submodule, Eq.rec, IsCentralScalar.op_smul_eq_smul, Submodule.smul_mem, MulOpposite.op
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : Module.{u_1, u_3} Rᵐᵒᵖ M
inst_5 : IsCentralScalar R M
H : IsLinearTopology.{u_1, u_3} Rᵐᵒᵖ M
⊢ IsLinearTopology R M

Tactic:
exact mk_of_hasBasis' R (IsLinearTopology.hasBasis_submodule Rᵐᵒᵖ)
      fun S r m hm ↦ op_smul_eq_smul r m ▸ S.smul_mem _ hm

Premises used: IsLinearTopology.mk_of_hasBasis', MulOpposite, IsLinearTopology.hasBasis_submodule
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : Module.{u_1, u_3} Rᵐᵒᵖ M
inst_5 : IsCentralScalar R M
H : IsLinearTopology R M
⊢ IsLinearTopology.{u_1, u_3} Rᵐᵒᵖ M

Tactic:
mk_of_hasBasis' Rᵐᵒᵖ (IsLinearTopology.hasBasis_submodule R)
      fun S r m hm ↦ unop_smul_eq_smul r m ▸ S.smul_mem _ hm

Premises used: IsCentralScalar.unop_smul_eq_smul, IsLinearTopology.mk_of_hasBasis', MulOpposite, IsLinearTopology.hasBasis_submodule, Eq.rec, MulOpposite.unop, Submodule.smul_mem
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : Module.{u_1, u_3} Rᵐᵒᵖ M
inst_5 : IsCentralScalar R M
H : IsLinearTopology R M
⊢ IsLinearTopology.{u_1, u_3} Rᵐᵒᵖ M

Tactic:
exact mk_of_hasBasis' Rᵐᵒᵖ (IsLinearTopology.hasBasis_submodule R)
      fun S r m hm ↦ unop_smul_eq_smul r m ▸ S.smul_mem _ hm

Premises used: IsLinearTopology.mk_of_hasBasis', MulOpposite, IsLinearTopology.hasBasis_submodule
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
⊢ HasBasis (α := R) (𝓝 0) (fun (I : Ideal R) ↦ Membership.mem (γ := Filter R) (𝓝 0) (↑I : Set R)) fun (I : Ideal R) ↦
    (↑I : Set R)

Tactic:
hasBasis_submodule R

Premises used: Set.Mem, IsLinearTopology.hasBasis_submodule
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : ContinuousAdd R
inst_3 : IsLinearTopology R R
⊢ HasBasis (α := R) (𝓝 0) (fun (I : Ideal R) ↦ IsOpen[inst_1] (↑I : Set R)) fun (I : Ideal R) ↦ (↑I : Set R)

Tactic:
hasBasis_open_submodule R

Premises used: IsLinearTopology.hasBasis_open_submodule
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
⊢ IsLinearTopology R R ↔
    HasBasis (α := R) (𝓝 0) (fun (I : Ideal R) ↦ Membership.mem (γ := Filter R) (𝓝 0) (↑I : Set R)) fun (I : Ideal R) ↦
      (↑I : Set R)

Tactic:
isLinearTopology_iff_hasBasis_submodule

Premises used: Set.Mem, isLinearTopology_iff_hasBasis_submodule
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
⊢ IsLinearTopology R R ↔
    HasBasis (α := R) (𝓝 0) (fun (I : Ideal R) ↦ IsOpen[inst_1] (↑I : Set R)) fun (I : Ideal R) ↦ (↑I : Set R)

Tactic:
isLinearTopology_iff_hasBasis_open_submodule

Premises used: isLinearTopology_iff_hasBasis_open_submodule
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology Rᵐᵒᵖ R
⊢ HasBasis (α := R) (𝓝 0) (fun (I : Submodule Rᵐᵒᵖ R) ↦ Membership.mem (γ := Filter R) (𝓝 0) (↑I : Set R))
    fun (I : Submodule Rᵐᵒᵖ R) ↦ (↑I : Set R)

Tactic:
hasBasis_submodule Rᵐᵒᵖ

Premises used: Set.Mem, MulOpposite, IsLinearTopology.hasBasis_submodule
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
inst_3 : IsLinearTopology Rᵐᵒᵖ R
I : AddSubgroup R
h :
  Membership.mem (γ := Filter R) (𝓝 0) (↑I : Set R) ∧
    (∀ (r x : R), x ∈ I → r • x ∈ I) ∧ ∀ (r' : Rᵐᵒᵖ), ∀ x ∈ I, r' • x ∈ I
hI : Membership.mem (γ := Filter R) (𝓝 0) (↑I : Set R)
hRI : ∀ (r x : R), x ∈ I → r • x ∈ I
hRI' : ∀ (r' : Rᵐᵒᵖ), ∀ x ∈ I, r' • x ∈ I
⊢ Membership.mem (γ := Filter R) (𝓝 0) (↑(TwoSidedIdeal.mk' (↑I : Set R) ⋯ ⋯ ⋯ ⋯ ⋯) : Set R)

Tactic:
simpa using hI
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
inst_3 : IsLinearTopology Rᵐᵒᵖ R
I : AddSubgroup R
h :
  Membership.mem (γ := Filter R) (𝓝 0) (↑I : Set R) ∧
    (∀ (r x : R), x ∈ I → r • x ∈ I) ∧ ∀ (r' : Rᵐᵒᵖ), ∀ x ∈ I, r' • x ∈ I
hI : Membership.mem (γ := Filter R) (𝓝 0) (↑I : Set R)
hRI : ∀ (r x : R), x ∈ I → r • x ∈ I
hRI' : ∀ (r' : Rᵐᵒᵖ), ∀ x ∈ I, r' • x ∈ I
⊢ (↑(TwoSidedIdeal.mk' (↑I : Set R) ⋯ ⋯ ⋯ ⋯ ⋯) : Set R) ⊆ (↑I : Set R)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : ContinuousAdd R
inst_3 : IsLinearTopology R R
inst_4 : IsLinearTopology Rᵐᵒᵖ R
⊢ HasBasis (α := R) (𝓝 0) (fun (I : TwoSidedIdeal R) ↦ IsOpen[inst_1] (↑I : Set R)) fun (I : TwoSidedIdeal R) ↦
    (↑I : Set R)

Tactic:
hasBasis_twoSidedIdeal.congr
    (fun I ↦ ⟨I.asIdeal.toAddSubgroup.isOpen_of_mem_nhds, fun hI ↦ hI.mem_nhds (zero_mem I)⟩)
    (fun _ _ ↦ rfl)

Premises used: TwoSidedIdeal.asIdeal, IsLinearTopology.hasBasis_twoSidedIdeal, AddSubgroup.isOpen_of_mem_nhds, Submodule.toAddSubgroup, IsOpen.mem_nhds, Iff.intro, ZeroMemClass.zero_mem, DFunLike.coe, Filter.HasBasis.congr, rfl
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
⊢ IsLinearTopology R R ∧ IsLinearTopology Rᵐᵒᵖ R ↔
    HasBasis (α := R) (𝓝 0) (fun (I : TwoSidedIdeal R) ↦ Membership.mem (γ := Filter R) (𝓝 0) (↑I : Set R))
      fun (I : TwoSidedIdeal R) ↦ (↑I : Set R)

Tactic:
⟨fun ⟨_, _⟩ ↦ hasBasis_twoSidedIdeal, fun h ↦
    ⟨.mk_of_hasBasis' R h fun I r x hx ↦ I.mul_mem_left r x hx,
      .mk_of_hasBasis' Rᵐᵒᵖ h fun I r x hx ↦ I.mul_mem_right x r.unop hx⟩⟩

Premises used: TwoSidedIdeal.mul_mem_right, TwoSidedIdeal.mul_mem_left, IsLinearTopology.mk_of_hasBasis', MulOpposite, IsLinearTopology.hasBasis_twoSidedIdeal, Membership.mem, nhds, Filter.HasBasis, SetLike.coe, And.intro, Iff.intro, MulOpposite.unop, OfNat.ofNat, _private.0.isLinearTopology_iff_hasBasis_twoSidedIdeal.match_1
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : ContinuousAdd R
⊢ IsLinearTopology R R ∧ IsLinearTopology Rᵐᵒᵖ R ↔
    HasBasis (α := R) (𝓝 0) (fun (I : TwoSidedIdeal R) ↦ IsOpen[inst_1] (↑I : Set R)) fun (I : TwoSidedIdeal R) ↦
      (↑I : Set R)

Tactic:
⟨fun ⟨_, _⟩ ↦ hasBasis_open_twoSidedIdeal, fun h ↦
    ⟨.mk_of_hasBasis' R h fun I r x hx ↦ I.mul_mem_left r x hx,
      .mk_of_hasBasis' Rᵐᵒᵖ h fun I r x hx ↦ I.mul_mem_right x r.unop hx⟩⟩

Premises used: TwoSidedIdeal.mul_mem_right, TwoSidedIdeal.mul_mem_left, IsLinearTopology.mk_of_hasBasis', MulOpposite, nhds, Filter.HasBasis, SetLike.coe, And.intro, Iff.intro, MulOpposite.unop, IsOpen, OfNat.ofNat, _private.0.isLinearTopology_iff_hasBasis_twoSidedIdeal.match_1, IsLinearTopology.hasBasis_open_twoSidedIdeal
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology Rᵐᵒᵖ R
ι : Type u_2
f : Filter ι
a b : ι → R
ha : Tendsto a f (𝓝 0)
⊢ Tendsto (a * b) f (𝓝 0)

Tactic:
tendsto_smul_zero (R := Rᵐᵒᵖ) _ _ ha

Premises used: MulOpposite, MulOpposite.unop, IsLinearTopology.tendsto_smul_zero
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
ι : Type u_2
f : Filter ι
a b : ι → R
hb : Tendsto b f (𝓝 0)
⊢ Tendsto (a * b) f (𝓝 0)

Tactic:
tendsto_smul_zero (R := R) _ _ hb

Premises used: IsLinearTopology.tendsto_smul_zero
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 rwa rwa₁ rwa₂ rwa₃ : IsLinearTopology R R
⊢ IsLinearTopology Rᵐᵒᵖ R

Tactic:
rwa [IsCentralScalar.isLinearTopology_iff]

Premises used: IsCentralScalar.isLinearTopology_iff
-- Module: Mathlib.Topology.Algebra.Localization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
M : Submonoid R
⊢ IsTopologicalRing.{u_1} (Localization (M := R) M)

Tactic:
Localization.ringTopology.toIsTopologicalRing

Premises used: RingTopology.toIsTopologicalRing, Localization.ringTopology
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
u : ℕ → α
hu : CauchySeq u
rcases :
  ∀ (b : ℕ → ℝ) (b_nonneg : ∀ (n : ℕ), 0 ≤ b n) (hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N)
    (blim : Tendsto b atTop (nhds 0)), CauchySeq (f ∘ u)
⊢ CauchySeq (f ∘ u)

Tactic:
rcases cauchySeq_iff_le_tendsto_0.1 hu with ⟨b, b_nonneg, hb, blim⟩

Premises used: cauchySeq_iff_le_tendsto_0, Iff.mp
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
u : ℕ → α
hu : CauchySeq u
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
⊢ CauchySeq (f ∘ u)

Tactic:
cauchySeq_iff_le_tendsto_0.2 ⟨fun n ↦ K * b n, ?_, ?_, ?_⟩

Premises used: Iff.mpr, HMul.hMul, cauchySeq_iff_le_tendsto_0, And.intro, Exists.intro, NNReal.toReal
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
u : ℕ → α
hu : CauchySeq u
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
refine_1 : ∀ (n : ℕ), LE.le (α := ℝ) 0 ((fun (n : ℕ) ↦ (↑K : ℝ) * b n) n)
refine_2 : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun (n : ℕ) ↦ (↑K : ℝ) * b n) N
refine_3 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑K : ℝ) * b n) atTop (nhds 0)
⊢ CauchySeq (f ∘ u)

Tactic:
refine cauchySeq_iff_le_tendsto_0.2 ⟨fun n ↦ K * b n, ?_, ?_, ?_⟩

Premises used: Iff.mpr, HMul.hMul, cauchySeq_iff_le_tendsto_0, And.intro, Exists.intro, NNReal.toReal
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
u : ℕ → α
hu : CauchySeq u
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
n : ℕ
⊢ 0 ≤ (↑K : ℝ)

Tactic:
positivity
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
u : ℕ → α
hu : CauchySeq u
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
⊢ ∀ (n : ℕ), LE.le (α := ℝ) 0 ((fun (n : ℕ) ↦ (↑K : ℝ) * b n) n)

Tactic:
exact fun n ↦ mul_nonneg (by positivity) (b_nonneg n)

Premises used: mul_nonneg
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
u : ℕ → α
hu : CauchySeq u
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
⊢ ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun (n : ℕ) ↦ (↑K : ℝ) * b n) N

Tactic:
fun n m N hn hm ↦ hf.dist_le_mul_of_le (hb n m N hn hm)

Premises used: LipschitzWith.dist_le_mul_of_le
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
u : ℕ → α
hu : CauchySeq u
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
⊢ ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun (n : ℕ) ↦ (↑K : ℝ) * b n) N

Tactic:
exact fun n m N hn hm ↦ hf.dist_le_mul_of_le (hb n m N hn hm)

Premises used: LipschitzWith.dist_le_mul_of_le
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
u : ℕ → α
hu : CauchySeq u
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
refine_3 : Tendsto (fun (n : ℕ) ↦ (↑K : ℝ) * b n) atTop (nhds ((↑K : ℝ) * 0))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑K : ℝ) * b n) atTop (nhds 0)

Tactic:
rw [← mul_zero (K : ℝ)]

Premises used: MulZeroClass.mul_zero, NNReal.toReal
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
u : ℕ → α
hu : CauchySeq u
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
⊢ Tendsto (fun (n : ℕ) ↦ (↑K : ℝ) * b n) atTop (nhds ((↑K : ℝ) * 0))

Tactic:
blim.const_mul _

Premises used: Filter.Tendsto.const_mul
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
u : ℕ → α
hu : CauchySeq u
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
⊢ Tendsto (fun (n : ℕ) ↦ (↑K : ℝ) * b n) atTop (nhds ((↑K : ℝ) * 0))

Tactic:
exact blim.const_mul _

Premises used: Filter.Tendsto.const_mul
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
rcases :
  ∀ (b : ℕ → ℝ) (b_nonneg : ∀ (n : ℕ), 0 ≤ b n) (hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N)
    (blim : Tendsto b atTop (nhds 0)), CauchySeq (f ∘ u)
⊢ CauchySeq (f ∘ u)

Tactic:
rcases cauchySeq_iff_le_tendsto_0.1 hu with ⟨b, b_nonneg, hb, blim⟩

Premises used: cauchySeq_iff_le_tendsto_0, Iff.mp
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
⊢ CauchySeq (f ∘ u)

Tactic:
cauchySeq_iff_le_tendsto_0.2 ⟨fun n ↦ K * b n, ?_, ?_, ?_⟩

Premises used: Iff.mpr, HMul.hMul, cauchySeq_iff_le_tendsto_0, And.intro, Exists.intro, NNReal.toReal
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
refine_1 : ∀ (n : ℕ), LE.le (α := ℝ) 0 ((fun (n : ℕ) ↦ (↑K : ℝ) * b n) n)
refine_2 : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun (n : ℕ) ↦ (↑K : ℝ) * b n) N
refine_3 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑K : ℝ) * b n) atTop (nhds 0)
⊢ CauchySeq (f ∘ u)

Tactic:
refine cauchySeq_iff_le_tendsto_0.2 ⟨fun n ↦ K * b n, ?_, ?_, ?_⟩

Premises used: Iff.mpr, HMul.hMul, cauchySeq_iff_le_tendsto_0, And.intro, Exists.intro, NNReal.toReal
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
n : ℕ
⊢ 0 ≤ (↑K : ℝ)

Tactic:
positivity
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
⊢ ∀ (n : ℕ), LE.le (α := ℝ) 0 ((fun (n : ℕ) ↦ (↑K : ℝ) * b n) n)

Tactic:
exact fun n ↦ mul_nonneg (by positivity) (b_nonneg n)

Premises used: mul_nonneg
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
n m N : ℕ
hn : N ≤ n
hm : N ≤ m
⊢ ∀ (n : ℕ), u n ∈ s

Tactic:
have A n : u n ∈ s := h'u (mem_range_self _)
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
n m N : ℕ
hn : N ≤ n
hm : N ≤ m
A : ∀ (n : ℕ), u n ∈ s
refine_2 : (↑K : ℝ) * dist (u n) (u m) ≤ (fun (n : ℕ) ↦ (↑K : ℝ) * b n) N
⊢ dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun (n : ℕ) ↦ (↑K : ℝ) * b n) N

Tactic:
apply (hf.dist_le_mul _ (A n) _ (A m)).trans

Premises used: LipschitzOnWith.dist_le_mul, LE.le.trans
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
n m N : ℕ
hn : N ≤ n
hm : N ≤ m
A : ∀ (n : ℕ), u n ∈ s
⊢ (↑K : ℝ) * dist (u n) (u m) ≤ (fun (n : ℕ) ↦ (↑K : ℝ) * b n) N

Tactic:
mul_le_mul_of_nonneg_left (hb n m N hn hm) K.2

Premises used: mul_le_mul_of_nonneg_left, Subtype.property
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
n m N : ℕ
hn : N ≤ n
hm : N ≤ m
A : ∀ (n : ℕ), u n ∈ s
⊢ (↑K : ℝ) * dist (u n) (u m) ≤ (fun (n : ℕ) ↦ (↑K : ℝ) * b n) N

Tactic:
exact mul_le_mul_of_nonneg_left (hb n m N hn hm) K.2

Premises used: mul_le_mul_of_nonneg_left, Subtype.property
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
refine_3 : Tendsto (fun (n : ℕ) ↦ (↑K : ℝ) * b n) atTop (nhds ((↑K : ℝ) * 0))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑K : ℝ) * b n) atTop (nhds 0)

Tactic:
rw [← mul_zero (K : ℝ)]

Premises used: MulZeroClass.mul_zero, NNReal.toReal
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
⊢ Tendsto (fun (n : ℕ) ↦ (↑K : ℝ) * b n) atTop (nhds ((↑K : ℝ) * 0))

Tactic:
blim.const_mul _

Premises used: Filter.Tendsto.const_mul
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
⊢ Tendsto (fun (n : ℕ) ↦ (↑K : ℝ) * b n) atTop (nhds ((↑K : ℝ) * 0))

Tactic:
exact blim.const_mul _

Premises used: Filter.Tendsto.const_mul