awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F_1 : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f_1 g : α →ᵇ β
x_1 : α
C : ℝ
inst_3 : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd :
  ∀ (x : α) (n m N : ℕ) (hn : N ≤ n) (hm : N ≤ m),
    dist.{v} (α := β) ((f n : (a : α) → β) x : β) ((f m : (a : α) → β) x : β) ≤ b N
fx_cau : ∀ (x : α), CauchySeq.{v, 0} (α := β) fun (n : ℕ) ↦ (f n : (a : α) → β) x
F : (x : α) → β
hF : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (f n : (a : α) → β) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist ((f N : (a : α) → β) x) (F x) ≤ b N
ε : ℝ
ε0 : ε > 0
n : ℕ
hn : b n < ε
x : α
⊢ dist ((f n : (a : α) → β) x) (F x) < ε

Tactic:
lt_of_le_of_lt (fF_bdd x n) hn

Premises used: lt_of_le_of_lt
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F_1 : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f_1 g : α →ᵇ β
x_1 : α
C : ℝ
inst_3 : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd :
  ∀ (x : α) (n m N : ℕ) (hn : N ≤ n) (hm : N ≤ m),
    dist.{v} (α := β) ((f n : (a : α) → β) x : β) ((f m : (a : α) → β) x : β) ≤ b N
fx_cau : ∀ (x : α), CauchySeq.{v, 0} (α := β) fun (n : ℕ) ↦ (f n : (a : α) → β) x
F : (x : α) → β
hF : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (f n : (a : α) → β) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist ((f N : (a : α) → β) x) (F x) ≤ b N
ε : ℝ
ε0 : ε > 0
n : ℕ
hn : b n < ε
x : α
⊢ dist ((f n : (a : α) → β) x) (F x) < ε

Tactic:
exact lt_of_le_of_lt (fF_bdd x n) hn

Premises used: lt_of_le_of_lt
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F_1 : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f_1 g : α →ᵇ β
x : α
C : ℝ
inst_3 : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd :
  ∀ (x : α) (n m N : ℕ) (hn : N ≤ n) (hm : N ≤ m),
    dist.{v} (α := β) ((f n : (a : α) → β) x : β) ((f m : (a : α) → β) x : β) ≤ b N
fx_cau : ∀ (x : α), CauchySeq.{v, 0} (α := β) fun (n : ℕ) ↦ (f n : (a : α) → β) x
F : (x : α) → β
hF : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (f n : (a : α) → β) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist ((f N : (a : α) → β) x) (F x) ≤ b N
⊢ TendstoUniformly (fun (n : ℕ) (x : α) ↦ (f n : (a : α) → β) x) F atTop

Tactic:
have : TendstoUniformly (fun n x => f n x) F atTop := by
        refine Metric.tendstoUniformly_iff.2 fun ε ε0 => ?_
        refine ((tendsto_order.1 b_lim).2 ε ε0).mono fun n hn x => ?_
        rw [dist_comm]
        exact lt_of_le_of_lt (fF_bdd x n) hn
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F_1 : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f_1 g : α →ᵇ β
x : α
C : ℝ
inst_3 : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd :
  ∀ (x : α) (n m N : ℕ) (hn : N ≤ n) (hm : N ≤ m),
    dist.{v} (α := β) ((f n : (a : α) → β) x : β) ((f m : (a : α) → β) x : β) ≤ b N
fx_cau : ∀ (x : α), CauchySeq.{v, 0} (α := β) fun (n : ℕ) ↦ (f n : (a : α) → β) x
F : (x : α) → β
hF : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (f n : (a : α) → β) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist ((f N : (a : α) → β) x) (F x) ≤ b N
this : TendstoUniformly (fun (n : ℕ) (x : α) ↦ (f n : (a : α) → β) x) F atTop
⊢ Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F

Tactic:
this.continuous (Frequently.of_forall fun N => (f N).continuous)

Premises used: Filter.Frequently.of_forall, BoundedContinuousFunction.continuous, TendstoUniformly.continuous
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F_1 : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f_1 g : α →ᵇ β
x : α
C : ℝ
inst_3 : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd :
  ∀ (x : α) (n m N : ℕ) (hn : N ≤ n) (hm : N ≤ m),
    dist.{v} (α := β) ((f n : (a : α) → β) x : β) ((f m : (a : α) → β) x : β) ≤ b N
fx_cau : ∀ (x : α), CauchySeq.{v, 0} (α := β) fun (n : ℕ) ↦ (f n : (a : α) → β) x
F : (x : α) → β
hF : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (f n : (a : α) → β) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist ((f N : (a : α) → β) x) (F x) ≤ b N
this : TendstoUniformly (fun (n : ℕ) (x : α) ↦ (f n : (a : α) → β) x) F atTop
⊢ Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F

Tactic:
exact this.continuous (Frequently.of_forall fun N => (f N).continuous)

Premises used: Filter.Frequently.of_forall, BoundedContinuousFunction.continuous, TendstoUniformly.continuous
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F_1 : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f_1 g : α →ᵇ β
x : α
C : ℝ
inst_3 : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd :
  ∀ (x : α) (n m N : ℕ) (hn : N ≤ n) (hm : N ≤ m),
    dist.{v} (α := β) ((f n : (a : α) → β) x : β) ((f m : (a : α) → β) x : β) ≤ b N
fx_cau : ∀ (x : α), CauchySeq.{v, 0} (α := β) fun (n : ℕ) ↦ (f n : (a : α) → β) x
F : (x : α) → β
hF : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (f n : (a : α) → β) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist ((f N : (a : α) → β) x) (F x) ≤ b N
refine_2 :
  ∀ (C : ℝ) (hC : ∀ (x y : α), dist.{v} (α := β) ((f 0 : (a : α) → β) x : β) ((f 0 : (a : α) → β) y : β) ≤ C),
    ∃ (C : ℝ),
      ∀ (x y : α),
        dist (ContinuousMap.toFun { toFun := F, continuous_toFun := ⋯ : C(α, β) } x)
            (ContinuousMap.toFun { toFun := F, continuous_toFun := ⋯ : C(α, β) } y) ≤
          C
⊢ ∃ (C : ℝ),
    ∀ (x y : α),
      dist (ContinuousMap.toFun { toFun := F, continuous_toFun := ⋯ : C(α, β) } x)
          (ContinuousMap.toFun { toFun := F, continuous_toFun := ⋯ : C(α, β) } y) ≤
        C

Tactic:
rcases (f 0).bounded with ⟨C, hC⟩

Premises used: BoundedContinuousFunction.bounded, OfNat.ofNat
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F_1 : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f_1 g : α →ᵇ β
x : α
C_1 : ℝ
inst_3 : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd :
  ∀ (x : α) (n m N : ℕ) (hn : N ≤ n) (hm : N ≤ m),
    dist.{v} (α := β) ((f n : (a : α) → β) x : β) ((f m : (a : α) → β) x : β) ≤ b N
fx_cau : ∀ (x : α), CauchySeq.{v, 0} (α := β) fun (n : ℕ) ↦ (f n : (a : α) → β) x
F : (x : α) → β
hF : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (f n : (a : α) → β) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist ((f N : (a : α) → β) x) (F x) ≤ b N
C : ℝ
hC : ∀ (x y : α), dist.{v} (α := β) ((f 0 : (a : α) → β) x : β) ((f 0 : (a : α) → β) y : β) ≤ C
⊢ ∃ (C : ℝ),
    ∀ (x y : α),
      dist (ContinuousMap.toFun { toFun := F, continuous_toFun := ⋯ : C(α, β) } x)
          (ContinuousMap.toFun { toFun := F, continuous_toFun := ⋯ : C(α, β) } y) ≤
        C

Tactic:
⟨C + (b 0 + b 0), fun x y => ?_⟩

Premises used: HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F_1 : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f_1 g : α →ᵇ β
x : α
C_1 : ℝ
inst_3 : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd :
  ∀ (x : α) (n m N : ℕ) (hn : N ≤ n) (hm : N ≤ m),
    dist.{v} (α := β) ((f n : (a : α) → β) x : β) ((f m : (a : α) → β) x : β) ≤ b N
fx_cau : ∀ (x : α), CauchySeq.{v, 0} (α := β) fun (n : ℕ) ↦ (f n : (a : α) → β) x
F : (x : α) → β
hF : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (f n : (a : α) → β) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist ((f N : (a : α) → β) x) (F x) ≤ b N
C : ℝ
hC : ∀ (x y : α), dist.{v} (α := β) ((f 0 : (a : α) → β) x : β) ((f 0 : (a : α) → β) y : β) ≤ C
refine_2 :
  ∀ (x y : α),
    dist (ContinuousMap.toFun { toFun := F, continuous_toFun := ⋯ : C(α, β) } x)
        (ContinuousMap.toFun { toFun := F, continuous_toFun := ⋯ : C(α, β) } y) ≤
      C + (b 0 + b 0)
⊢ ∃ (C : ℝ),
    ∀ (x y : α),
      dist (ContinuousMap.toFun { toFun := F, continuous_toFun := ⋯ : C(α, β) } x)
          (ContinuousMap.toFun { toFun := F, continuous_toFun := ⋯ : C(α, β) } y) ≤
        C

Tactic:
refine ⟨C + (b 0 + b 0), fun x y => ?_⟩
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F_1 : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f_1 g : α →ᵇ β
x_1 : α
C_1 : ℝ
inst_3 : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd :
  ∀ (x : α) (n m N : ℕ) (hn : N ≤ n) (hm : N ≤ m),
    dist.{v} (α := β) ((f n : (a : α) → β) x : β) ((f m : (a : α) → β) x : β) ≤ b N
fx_cau : ∀ (x : α), CauchySeq.{v, 0} (α := β) fun (n : ℕ) ↦ (f n : (a : α) → β) x
F : (x : α) → β
hF : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (f n : (a : α) → β) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist ((f N : (a : α) → β) x) (F x) ≤ b N
C : ℝ
hC : ∀ (x y : α), dist.{v} (α := β) ((f 0 : (a : α) → β) x : β) ((f 0 : (a : α) → β) y : β) ≤ C
x y : α
⊢ dist (F x) (F y) ≤
    dist.{v} (α := β) ((f 0 : (a : α) → β) x : β) ((f 0 : (a : α) → β) y : β) +
      (dist ((f 0 : (a : α) → β) x) (F x) + dist ((f 0 : (a : α) → β) y) (F y))

Tactic:
dist_triangle4_left _ _ _ _

Premises used: dist_triangle4_left
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F_1 : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f_1 g : α →ᵇ β
x_1 : α
C_1 : ℝ
inst_3 : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd :
  ∀ (x : α) (n m N : ℕ) (hn : N ≤ n) (hm : N ≤ m),
    dist.{v} (α := β) ((f n : (a : α) → β) x : β) ((f m : (a : α) → β) x : β) ≤ b N
fx_cau : ∀ (x : α), CauchySeq.{v, 0} (α := β) fun (n : ℕ) ↦ (f n : (a : α) → β) x
F : (x : α) → β
hF : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (f n : (a : α) → β) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist ((f N : (a : α) → β) x) (F x) ≤ b N
C : ℝ
hC : ∀ (x y : α), dist.{v} (α := β) ((f 0 : (a : α) → β) x : β) ((f 0 : (a : α) → β) y : β) ≤ C
x y : α
⊢ dist.{v} (α := β) ((f 0 : (a : α) → β) x : β) ((f 0 : (a : α) → β) y : β) +
      (dist ((f 0 : (a : α) → β) x) (F x) + dist ((f 0 : (a : α) → β) y) (F y)) ≤
    C + (b 0 + b 0)

Tactic:
add_le_add (hC x y) (add_le_add (fF_bdd x 0) (fF_bdd y 0))

Premises used: add_le_add, OfNat.ofNat
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F_1 : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f_1 g : α →ᵇ β
x_1 : α
C_1 : ℝ
inst_3 : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd :
  ∀ (x : α) (n m N : ℕ) (hn : N ≤ n) (hm : N ≤ m),
    dist.{v} (α := β) ((f n : (a : α) → β) x : β) ((f m : (a : α) → β) x : β) ≤ b N
fx_cau : ∀ (x : α), CauchySeq.{v, 0} (α := β) fun (n : ℕ) ↦ (f n : (a : α) → β) x
F : (x : α) → β
hF : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (f n : (a : α) → β) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist ((f N : (a : α) → β) x) (F x) ≤ b N
C : ℝ
hC : ∀ (x y : α), dist.{v} (α := β) ((f 0 : (a : α) → β) x : β) ((f 0 : (a : α) → β) y : β) ≤ C
x y : α
⊢ dist (ContinuousMap.toFun { toFun := F, continuous_toFun := ⋯ : C(α, β) } x)
      (ContinuousMap.toFun { toFun := F, continuous_toFun := ⋯ : C(α, β) } y) ≤
    C + (b 0 + b 0)

Tactic:
calc
        dist (F x) (F y) ≤ dist (f 0 x) (f 0 y) + (dist (f 0 x) (F x) + dist (f 0 y) (F y)) :=
          dist_triangle4_left _ _ _ _
        _ ≤ C + (b 0 + b 0) := add_le_add (hC x y) (add_le_add (fF_bdd x 0) (fF_bdd y 0))

Premises used: add_le_add, HAdd.hAdd, dist_triangle4_left, Dist.dist, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F_1 : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f_1 g : α →ᵇ β
x : α
C : ℝ
inst_3 : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd :
  ∀ (x : α) (n m N : ℕ) (hn : N ≤ n) (hm : N ≤ m),
    dist.{v} (α := β) ((f n : (a : α) → β) x : β) ((f m : (a : α) → β) x : β) ≤ b N
fx_cau : ∀ (x : α), CauchySeq.{v, 0} (α := β) fun (n : ℕ) ↦ (f n : (a : α) → β) x
F : (x : α) → β
hF : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (f n : (a : α) → β) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist ((f N : (a : α) → β) x) (F x) ≤ b N
⊢ Tendsto f atTop (𝓝 { toFun := F, continuous_toFun := ⋯, map_bounded' := ⋯ })

Tactic:
tendsto_iff_dist_tendsto_zero.2 (squeeze_zero (fun _ => dist_nonneg) ?_ b_lim)

Premises used: Iff.mpr, squeeze_zero, dist_nonneg, tendsto_iff_dist_tendsto_zero
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F_1 : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f_1 g : α →ᵇ β
x : α
C : ℝ
inst_3 : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd :
  ∀ (x : α) (n m N : ℕ) (hn : N ≤ n) (hm : N ≤ m),
    dist.{v} (α := β) ((f n : (a : α) → β) x : β) ((f m : (a : α) → β) x : β) ≤ b N
fx_cau : ∀ (x : α), CauchySeq.{v, 0} (α := β) fun (n : ℕ) ↦ (f n : (a : α) → β) x
F : (x : α) → β
hF : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (f n : (a : α) → β) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist ((f N : (a : α) → β) x) (F x) ≤ b N
refine_3 : ∀ (t : ℕ), dist (f t) { toFun := F, continuous_toFun := ⋯, map_bounded' := ⋯ : α →ᵇ β } ≤ b t
⊢ Tendsto f atTop (𝓝 { toFun := F, continuous_toFun := ⋯, map_bounded' := ⋯ })

Tactic:
refine tendsto_iff_dist_tendsto_zero.2 (squeeze_zero (fun _ => dist_nonneg) ?_ b_lim)

Premises used: Iff.mpr, squeeze_zero, dist_nonneg, tendsto_iff_dist_tendsto_zero
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F_1 : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f_1 g : α →ᵇ β
x : α
C : ℝ
inst_3 : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd :
  ∀ (x : α) (n m N : ℕ) (hn : N ≤ n) (hm : N ≤ m),
    dist.{v} (α := β) ((f n : (a : α) → β) x : β) ((f m : (a : α) → β) x : β) ≤ b N
fx_cau : ∀ (x : α), CauchySeq.{v, 0} (α := β) fun (n : ℕ) ↦ (f n : (a : α) → β) x
F : (x : α) → β
hF : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (f n : (a : α) → β) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist ((f N : (a : α) → β) x) (F x) ≤ b N
⊢ ∀ (t : ℕ), dist (f t) { toFun := F, continuous_toFun := ⋯, map_bounded' := ⋯ : α →ᵇ β } ≤ b t

Tactic:
fun N => (dist_le (b0 _)).2 fun x => fF_bdd x N

Premises used: Iff.mpr, BoundedContinuousFunction.dist_le
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F_1 : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f_1 g : α →ᵇ β
x : α
C : ℝ
inst_3 : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd :
  ∀ (x : α) (n m N : ℕ) (hn : N ≤ n) (hm : N ≤ m),
    dist.{v} (α := β) ((f n : (a : α) → β) x : β) ((f m : (a : α) → β) x : β) ≤ b N
fx_cau : ∀ (x : α), CauchySeq.{v, 0} (α := β) fun (n : ℕ) ↦ (f n : (a : α) → β) x
F : (x : α) → β
hF : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (f n : (a : α) → β) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist ((f N : (a : α) → β) x) (F x) ≤ b N
⊢ ∀ (t : ℕ), dist (f t) { toFun := F, continuous_toFun := ⋯, map_bounded' := ⋯ : α →ᵇ β } ≤ b t

Tactic:
exact fun N => (dist_le (b0 _)).2 fun x => fF_bdd x N

Premises used: Iff.mpr, BoundedContinuousFunction.dist_le
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
f : α →ᵇ β
g : C(δ, α)
⊢ Eq (α := (a : δ) → β) (⇑(f.compContinuous g) : (a : δ) → β)
    (comp.{u_2 + 1, u + 1, v + 1} (β := α) (⇑f : (a : α) → β) (⇑g : (a : δ) → α))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
f : α →ᵇ β
g : C(δ, α)
x : δ
⊢ Eq.{v + 1} (α := β) ((f.compContinuous g : (a : δ) → β) x : β) ((f : (a : α) → β) ((g : (a : δ) → α) x : α) : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
g : C(δ, α)
⊢ LipschitzWith (β := δ →ᵇ β) 1 fun (f : α →ᵇ β) ↦ f.compContinuous g

Tactic:
LipschitzWith.mk_one fun _ _ => (dist_le dist_nonneg).2 fun x => dist_coe_le_dist (g x)

Premises used: Iff.mpr, LipschitzWith.mk_one, BoundedContinuousFunction.dist_le, dist_nonneg, BoundedContinuousFunction.dist_coe_le_dist, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
g : C(δ, α)
⊢ Continuous (Y := δ →ᵇ β) fun (f : α →ᵇ β) ↦ f.compContinuous g

Tactic:
(lipschitz_compContinuous g).continuous

Premises used: LipschitzWith.continuous, BoundedContinuousFunction.lipschitz_compContinuous
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f : α →ᵇ β
s : Set α
⊢ Eq (α := (a : (↑s : Type u)) → β) (⇑(f.restrict s) : (a : (↑s : Type u)) → β)
    ((⇑f : (a : α) → β) ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f : α →ᵇ β
s : Set α
x : (↑s : Type u)
⊢ Eq.{v + 1} (α := β) ((f.restrict s : (a : (↑s : Type u)) → β) x : β) ((f : (a : α) → β) (↑x : α) : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f_1 g : α →ᵇ β
x_1 : α
C_1 : ℝ
G : β → γ
C : ℝ≥0
H : LipschitzWith C G
f : α →ᵇ β
D : ℝ
hD : ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ D
x y : α
hbc : C ≤ max C 0
⊢ (↑C : ℝ) * dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤
    (↑(max C 0) : ℝ) * dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)

Tactic:
gcongr
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f_1 g : α →ᵇ β
x_1 : α
C_1 : ℝ
G : β → γ
C : ℝ≥0
H : LipschitzWith C G
f : α →ᵇ β
D : ℝ
hD : ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ D
x y : α
⊢ C ≤ max C 0

Tactic:
apply le_max_left

Premises used: le_max_left
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f_1 g : α →ᵇ β
x_1 : α
C_1 : ℝ
G : β → γ
C : ℝ≥0
H : LipschitzWith C G
f : α →ᵇ β
D : ℝ
hD : ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ D
x y : α
hbc : dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ D
⊢ (↑(max C 0) : ℝ) * dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ (↑(max C 0) : ℝ) * D

Tactic:
gcongr
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f_1 g : α →ᵇ β
x_1 : α
C_1 : ℝ
G : β → γ
C : ℝ≥0
H : LipschitzWith C G
f : α →ᵇ β
D : ℝ
hD : ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ D
x y : α
⊢ dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ D

Tactic:
apply hD
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
G : β → γ
C : ℝ≥0
H : LipschitzWith C G
f : α →ᵇ β
a : α
⊢ (comp G H f : (a : α) → γ) a = G ((f : (a : α) → β) a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
G : β → γ
C : ℝ≥0
H : LipschitzWith C G
f g : α →ᵇ β
x : α
hbc : dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ dist f g
⊢ (↑C : ℝ) * dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ (↑C : ℝ) * dist f g

Tactic:
gcongr
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
G : β → γ
C : ℝ≥0
H : LipschitzWith C G
f g : α →ᵇ β
x : α
⊢ dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ dist f g

Tactic:
apply dist_coe_le_dist

Premises used: BoundedContinuousFunction.dist_coe_le_dist
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
G : β → γ
C : ℝ≥0
H : LipschitzWith C G
⊢ UniformContinuous (α := α →ᵇ β) (comp G H)

Tactic:
(lipschitz_comp H).uniformContinuous

Premises used: BoundedContinuousFunction.lipschitz_comp, LipschitzWith.uniformContinuous
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
G : β → γ
C : ℝ≥0
H : LipschitzWith C G
⊢ Continuous (X := α →ᵇ β) (comp G H)

Tactic:
(lipschitz_comp H).continuous

Premises used: BoundedContinuousFunction.lipschitz_comp, LipschitzWith.continuous