awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
⊢ (↑(⨆ (x : α), nndist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)) : ENNReal) =
    ⨆ (x : α), (↑(nndist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)) : ENNReal)
have refine : Membership.mem (γ := Set ℝ≥0)
  (upperBounds (range fun (x : α) ↦ nndist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)))
  (nndist f g)
Tactic: refine ENNReal.coe_iSup ⟨nndist f g, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
⊢ IsInducing (X := α →ᵇ β) (Y := α →ᵤ β)
    (comp (β := α → β) (⇑UniformFun.ofFun : (a : α → β) → α →ᵤ β) (DFunLike.coe (β := fun (x : α) ↦ β)))
have rw : ∀ (x : α →ᵇ β),
  𝓝 x =
    comap (β := α →ᵤ β)
      (comp (β := α → β) (⇑UniformFun.ofFun : (a : α → β) → α →ᵤ β) (DFunLike.coe (β := fun (x : α) ↦ β)))
      (𝓝 (comp (β := α → β) (⇑UniformFun.ofFun : (a : α → β) → α →ᵤ β) (DFunLike.coe (β := fun (x : α) ↦ β)) x))
Tactic: rw [isInducing_iff_nhds]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
⊢ ∀ (x : α →ᵇ β),
    𝓝 x =
      comap (β := α →ᵤ β)
        (comp (β := α → β) (⇑UniformFun.ofFun : (a : α → β) → α →ᵤ β) (DFunLike.coe (β := fun (x : α) ↦ β)))
        (𝓝 (comp (β := α → β) (⇑UniformFun.ofFun : (a : α → β) → α →ᵤ β) (DFunLike.coe (β := fun (x : α) ↦ β)) x))
have refine : ∀ (f : α →ᵇ β) (l : Filter (α →ᵇ β)),
  l ≤ 𝓝 f ↔
    l ≤
      comap (β := α →ᵤ β)
        (comp (β := α → β) (⇑UniformFun.ofFun : (a : α → β) → α →ᵤ β) (DFunLike.coe (β := fun (x : α) ↦ β)))
        (𝓝 (comp (β := α → β) (⇑UniformFun.ofFun : (a : α → β) → α →ᵤ β) (DFunLike.coe (β := fun (x : α) ↦ β)) f))
Tactic: refine fun f => eq_of_forall_le_iff fun l => ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f : α →ᵇ β
l : Filter (α →ᵇ β)
⊢ l ≤ 𝓝 f ↔
    l ≤
      comap (β := α →ᵤ β)
        (comp (β := α → β) (⇑UniformFun.ofFun : (a : α → β) → α →ᵤ β) (DFunLike.coe (β := fun (x : α) ↦ β)))
        (𝓝 (comp (β := α → β) (⇑UniformFun.ofFun : (a : α → β) → α →ᵤ β) (DFunLike.coe (β := fun (x : α) ↦ β)) f))
have rw : TendstoUniformly (α := α) (β := β) (fun (i : α →ᵇ β) ↦ (⇑(id i) : (a : α) → β)) (⇑f : (a : α) → β) l ↔
  TendstoUniformly (α := α) (β := β)
    (comp (β := α →ᵤ β) (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β)
      (comp (β := α → β) (⇑UniformFun.ofFun : (a : α → β) → α →ᵤ β) (DFunLike.coe (β := fun (x : α) ↦ β))))
    ((UniformFun.toFun : (a : α →ᵤ β) → α → β)
      (comp (β := α → β) (⇑UniformFun.ofFun : (a : α → β) → α →ᵤ β) (DFunLike.coe (β := fun (x : α) ↦ β)) f))
    l
Tactic: rw [← tendsto_iff_comap, ← tendsto_id', tendsto_iff_tendstoUniformly,
    UniformFun.tendsto_iff_tendstoUniformly]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
F : 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
⊢ ∃ (a : α →ᵇ β), Tendsto f atTop (𝓝 a)
have rcases : ∀ (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)), ∃ (a : α →ᵇ β), Tendsto f atTop (𝓝 a)
Tactic: rcases cauchySeq_iff_le_tendsto_0.1 hf with ⟨b, b0, b_bound, b_lim⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (hypothesis)
Goal:
F : 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)
⊢ ∃ (a : α →ᵇ β), Tendsto f atTop (𝓝 a)
have f_bdd : ∀ (x : α) (n m N : ℕ) (hn : N ≤ n) (hm : N ≤ m),
  dist.{v} (α := β) ((f n : (a : α) → β) x : β) ((f m : (a : α) → β) x : β) ≤ b N
Tactic: have f_bdd := fun x n m N hn hm => le_trans (dist_coe_le_dist x) (b_bound n m N hn hm)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (hypothesis)
Goal:
F : 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
⊢ ∃ (a : α →ᵇ β), Tendsto f atTop (𝓝 a)
have fx_cau : ∀ (x : α), CauchySeq.{v, 0} (α := β) fun (n : ℕ) ↦ (f n : (a : α) → β) x
Tactic: have fx_cau : ∀ x, CauchySeq fun n => f n x :=
      fun x => cauchySeq_iff_le_tendsto_0.2 ⟨b, b0, f_bdd x, b_lim⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
F : 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
⊢ ∃ (a : α →ᵇ β), Tendsto f atTop (𝓝 a)
have choose : ∀ (F : (x : α) → β) (hF : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (f n : (a : α) → β) x) atTop (𝓝 (F x))),
  ∃ (a : α →ᵇ β), Tendsto f atTop (𝓝 a)
Tactic: choose F hF using fun x => cauchySeq_tendsto_of_complete (fx_cau x)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (hypothesis)
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))
⊢ ∃ (a : α →ᵇ β), Tendsto f atTop (𝓝 a)
have fF_bdd : ∀ (x : α) (N : ℕ), dist ((f N : (a : α) → β) x) (F x) ≤ b N
Tactic: have fF_bdd : ∀ x N, dist (f N x) (F x) ≤ b N :=
      fun x N => le_of_tendsto (tendsto_const_nhds.dist (hF x))
        (Filter.eventually_atTop.2 ⟨N, fun n hn => f_bdd x N n N (le_refl N) hn⟩)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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
⊢ ∃ (a : α →ᵇ β), Tendsto f atTop (𝓝 a)
have refine_1 : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F
Tactic: refine ⟨⟨⟨F, ?_⟩, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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_1 : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F
⊢ ∃ (a : α →ᵇ β), Tendsto f atTop (𝓝 a)
have refine_2 : ∃ (C : ℝ),
  ∀ (x y : α),
    dist (ContinuousMap.toFun { toFun := F, continuous_toFun := sorry : C(α, β) } x)
        (ContinuousMap.toFun { toFun := F, continuous_toFun := sorry : C(α, β) } y) ≤
      C
Tactic: refine ⟨⟨⟨F, ?_⟩, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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_1 : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F
refine_2 :
  ∃ (C : ℝ),
    ∀ (x y : α),
      dist (ContinuousMap.toFun { toFun := F, continuous_toFun := ⋯ : C(α, β) } x)
          (ContinuousMap.toFun { toFun := F, continuous_toFun := ⋯ : C(α, β) } y) ≤
        C
⊢ ∃ (a : α →ᵇ β), Tendsto f atTop (𝓝 a)
have refine_3 : Tendsto f atTop (𝓝 { toFun := F, continuous_toFun := sorry, map_bounded' := sorry })
Tactic: refine ⟨⟨⟨F, ?_⟩, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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
have refine : ∀ (ε : ℝ) (ε0 : ε > 0), ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), dist (F x) ((f n : (a : α) → β) x) < ε
Tactic: refine Metric.tendstoUniformly_iff.2 fun ε ε0 => ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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
ε : ℝ
ε0 : ε > 0
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), dist (F x) ((f n : (a : α) → β) x) < ε
have refine : ∀ (n : ℕ) (hn : b n < ε) (x : α), dist (F x) ((f n : (a : α) → β) x) < ε
Tactic: refine ((tendsto_order.1 b_lim).2 ε ε0).mono fun n hn x => ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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 x) ((f n : (a : α) → β) x) < ε
have rw : dist ((f n : (a : α) → β) x) (F x) < ε
Tactic: rw [dist_comm]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (hypothesis)
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
⊢ Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F
have this : 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
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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
⊢ ∃ (C : ℝ),
    ∀ (x y : α),
      dist (ContinuousMap.toFun { toFun := F, continuous_toFun := ⋯ : C(α, β) } x)
          (ContinuousMap.toFun { toFun := F, continuous_toFun := ⋯ : C(α, β) } y) ≤
        C
have 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 := sorry : C(α, β) } x)
          (ContinuousMap.toFun { toFun := F, continuous_toFun := sorry : C(α, β) } y) ≤
        C
Tactic: rcases (f 0).bounded with ⟨C, hC⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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
have refine_2 : ∀ (x y : α),
  dist (ContinuousMap.toFun { toFun := F, continuous_toFun := sorry : C(α, β) } x)
      (ContinuousMap.toFun { toFun := F, continuous_toFun := sorry : C(α, β) } y) ≤
    C + (b 0 + b 0)
Tactic: refine ⟨C + (b 0 + b 0), fun x y => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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' := ⋯ })
have refine_3 : ∀ (t : ℕ), dist (f t) { toFun := F, continuous_toFun := sorry, map_bounded' := sorry : α →ᵇ β } ≤ b t
Tactic: refine tendsto_iff_dist_tendsto_zero.2 (squeeze_zero (fun _ => dist_nonneg) ?_ b_lim)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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 : ℝ) * dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤
    (↑(max C 0) : ℝ) * dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)
have hbc : C ≤ max C 0
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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 : α
⊢ (↑(max C 0) : ℝ) * dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ (↑(max C 0) : ℝ) * D
have hbc : dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ D
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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 : α
⊢ (↑C : ℝ) * dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ (↑C : ℝ) * dist f g
have hbc : dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ dist f g
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f_1 g_1 : α →ᵇ β
x : α
C : ℝ
δ : Type u_2
inst_3 : TopologicalSpace δ
inst_4 : DiscreteTopology δ
f : α ↪ δ
g : α →ᵇ β
h : δ →ᵇ β
⊢ ∃ (C : ℝ),
    ∀ (x y : δ),
      dist.{v} (α := β)
          (Function.extend.{u + 1, u_2 + 1, v + 1} (α := α) (⇑f : (a : α) → δ) (⇑g : (a : α) → β) (⇑h : (a : δ) → β) x)
          (Function.extend.{u + 1, u_2 + 1, v + 1} (α := α) (⇑f : (a : α) → δ) (⇑g : (a : α) → β) (⇑h : (a : δ) → β)
            y) ≤
        C
have rw : Bornology.IsBounded.{v} (α := β)
  (range.{v, u + 1} (ι := α) (⇑g : (a : α) → β) ∪
    image.{u_2, v} (α := δ) (⇑h : (a : δ) → β) (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ)
Tactic: rw [← isBounded_range_iff, range_extend f.injective]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
⊢ dist (extend f g₁ h₁) (extend f g₂ h₂) =
    max (dist g₁ g₂)
      (dist (α := BoundedContinuousFunction.{u_2, v} (↑(range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ : Type u_2) β)
        (h₁.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ)
        (h₂.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ))
have refine_1 : ∀ (x : δ),
  dist.{v} (α := β) ((extend f g₁ h₁ : (a : δ) → β) x : β) ((extend f g₂ h₂ : (a : δ) → β) x : β) ≤
    max (dist g₁ g₂)
      (dist (α := BoundedContinuousFunction.{u_2, v} (↑(range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ : Type u_2) β)
        (h₁.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ)
        (h₂.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ))
Tactic: refine le_antisymm ((dist_le <| le_max_iff.2 <| Or.inl dist_nonneg).2 fun x => ?_) (max_le ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
refine_1 :
  ∀ (x : δ),
    dist.{v} (α := β) ((extend f g₁ h₁ : (a : δ) → β) x : β) ((extend f g₂ h₂ : (a : δ) → β) x : β) ≤
      max (dist g₁ g₂)
        (dist (α :=
          BoundedContinuousFunction.{u_2, v} (↑(range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ : Type u_2) β)
          (h₁.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ)
          (h₂.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ))
⊢ dist (extend f g₁ h₁) (extend f g₂ h₂) =
    max (dist g₁ g₂)
      (dist (α := BoundedContinuousFunction.{u_2, v} (↑(range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ : Type u_2) β)
        (h₁.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ)
        (h₂.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ))
have refine_2 : dist g₁ g₂ ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)
Tactic: refine le_antisymm ((dist_le <| le_max_iff.2 <| Or.inl dist_nonneg).2 fun x => ?_) (max_le ?_ ?_)