-- Mathlib/Topology/MetricSpace/Lipschitz.lean
lemma cauchySeq_comp (hf : LipschitzOnWith K f s)
    {u : ℕ → α} (hu : CauchySeq u) (h'u : range u ⊆ s) :
    CauchySeq (f ∘ u)

Proof state:
case intro.intro.intro.refine_2
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : 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 (𝓝 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

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : 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 (𝓝 0)
n : ℕ
⊢ 0 ≤ ↑K

Tactic:
positivity

Result:
no goals

Proof state:
case intro.intro.intro.refine_2
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : 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 (𝓝 0)
n m N : ℕ
hn : N ≤ n
hm : N ≤ m
⊢ dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun n => ↑K * b n) N

Tactic:
have A n : u n ∈ s := h'u (mem_range_self _)

Result:
case intro.intro.intro.refine_2
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : 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 (𝓝 0)
n m N : ℕ
hn : N ≤ n
hm : N ≤ m
A : ∀ (n : ℕ), u n ∈ s
⊢ dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun n => ↑K * b n) N

Proof state:
case intro.intro.intro.refine_3
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : 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 (𝓝 0)
⊢ Tendsto (fun n => ↑K * b n) atTop (𝓝 (↑K * 0))

Tactic:
exact blim.const_mul _

Result:
no goals

Proof state:
case intro.intro.intro.refine_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : 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 (𝓝 0)
⊢ ∀ (n : ℕ), 0 ≤ (fun n => ↑K * b n) n

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

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : 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 (𝓝 0)
⊢ CauchySeq (f ∘ u)

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

Result:
case intro.intro.intro.refine_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : 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 (𝓝 0)
⊢ ∀ (n : ℕ), 0 ≤ (fun n => ↑K * b n) n

case intro.intro.intro.refine_2
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : 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 (𝓝 0)
⊢ ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun n => ↑K * b n) N

case intro.intro.intro.refine_3
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : 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 (𝓝 0)
⊢ Tendsto (fun n => ↑K * b n) atTop (𝓝 0)

Proof state:
case intro.intro.intro.refine_3
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : 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 (𝓝 0)
⊢ Tendsto (fun n => ↑K * b n) atTop (𝓝 0)

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

Result:
case intro.intro.intro.refine_3
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : 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 (𝓝 0)
⊢ Tendsto (fun n => ↑K * b n) atTop (𝓝 (↑K * 0))

Proof state:
case intro.intro.intro.refine_2
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : 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 (𝓝 0)
n m N : ℕ
hn : N ≤ n
hm : N ≤ m
A : ∀ (n : ℕ), u n ∈ s
⊢ dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun n => ↑K * b n) N

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

Result:
case intro.intro.intro.refine_2
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : 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 (𝓝 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

Proof state:
case intro.intro.intro.refine_2
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : 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 (𝓝 0)
⊢ ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun n => ↑K * b n) N

Tactic:
intro n m N hn hm

Result:
case intro.intro.intro.refine_2
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : 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 (𝓝 0)
n m N : ℕ
hn : N ≤ n
hm : N ≤ m
⊢ dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun n => ↑K * b n) N

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
⊢ CauchySeq (f ∘ u)

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

Result:
case intro.intro.intro
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : 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 (𝓝 0)
⊢ CauchySeq (f ∘ u)