awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
h : Nonempty α
⊢ dist f g = ⨆ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
(dist_le_iff_of_nonempty.mpr <| le_ciSup ?_).antisymm (ciSup_le dist_coe_le_dist)

Premises used: Iff.mpr, LE.le.antisymm, BoundedContinuousFunction.dist_coe_le_dist, BoundedContinuousFunction.dist_le_iff_of_nonempty, le_ciSup, ciSup_le
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
h : Nonempty α
inr : BddAbove (α := ℝ) (range fun (x : α) ↦ dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β))
⊢ dist f g = ⨆ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
refine (dist_le_iff_of_nonempty.mpr <| le_ciSup ?_).antisymm (ciSup_le dist_coe_le_dist)

Premises used: Iff.mpr, LE.le.antisymm, BoundedContinuousFunction.dist_coe_le_dist, BoundedContinuousFunction.dist_le_iff_of_nonempty, le_ciSup, ciSup_le
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
h : Nonempty α
⊢ BddAbove (α := ℝ) (range fun (x : α) ↦ dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β))

Tactic:
dist_set_exists.imp fun C hC => forall_mem_range.2 hC.2

Premises used: Iff.mpr, Set.forall_mem_range, Exists.imp, BddAbove, Set.Nonempty, BoundedContinuousFunction.dist_set_exists
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
h : Nonempty α
⊢ BddAbove (α := ℝ) (range fun (x : α) ↦ dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β))

Tactic:
exact dist_set_exists.imp fun C hC => forall_mem_range.2 hC.2

Premises used: Iff.mpr, Set.forall_mem_range, Exists.imp, BoundedContinuousFunction.dist_set_exists
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
simp_rw :
  ⨆ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) =
    (↑(⨆ (x : α), nndist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)) : ℝ)
simp_rw₁ :
  Eq (α := ℝ) (⨆ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β))
    (⨆ (i : α), (↑(nndist.{v} (α := β) ((f : (a : α) → β) i : β) ((g : (a : α) → β) i : β)) : ℝ))
⊢ Eq (α := ℝ) (⨆ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β))
    (↑(⨆ (x : α), nndist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)) : ℝ)

Tactic:
simp_rw [val_eq_coe, coe_iSup, coe_nndist]

Premises used: NNReal.coe_iSup, coe_nndist, NNReal.val_eq_coe
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
simp_rw :
  (↑(⨆ (x : α), nndist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)) : ENNReal) =
    ⨆ (x : α), (↑(nndist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)) : ENNReal)
⊢ edist f g = ⨆ (x : α), edist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
simp_rw [edist_nndist, nndist_eq_iSup]

Premises used: BoundedContinuousFunction.nndist_eq_iSup, edist_nndist
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
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)

Tactic:
ENNReal.coe_iSup ⟨nndist f g, ?_⟩

Premises used: NNDist.nndist, Exists.intro, ENNReal.coe_iSup
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
refine :
  Membership.mem (γ := Set ℝ≥0)
    (upperBounds (range fun (x : α) ↦ nndist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)))
    (nndist f g)
⊢ (↑(⨆ (x : α), nndist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)) : ENNReal) =
    ⨆ (x : α), (↑(nndist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)) : ENNReal)

Tactic:
refine ENNReal.coe_iSup ⟨nndist f g, ?_⟩

Premises used: NNDist.nndist, Exists.intro, ENNReal.coe_iSup
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
x : α
⊢ (fun (x : α) ↦ nndist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)) x ≤ nndist f g

Tactic:
nndist_coe_le_nndist x

Premises used: BoundedContinuousFunction.nndist_coe_le_nndist
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
x : α
⊢ (fun (x : α) ↦ nndist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)) x ≤ nndist f g

Tactic:
exact nndist_coe_le_nndist x

Premises used: BoundedContinuousFunction.nndist_coe_le_nndist
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
ι : Type u_2
F : ι → α →ᵇ β
f : α →ᵇ β
l : Filter ι
⊢ Tendsto F l (𝓝 f) ↔
    TendstoUniformly.{u, v, u_2} (α := α) (β := β) (fun (i : ι) ↦ (⇑(F i) : (a : α) → β)) (⇑f : (a : α) → β) l

Tactic:
Iff.intro
    (fun h =>
      tendstoUniformly_iff.2 fun ε ε0 =>
        (Metric.tendsto_nhds.mp h ε ε0).mp
          (Eventually.of_forall fun n hn x =>
            lt_of_le_of_lt (dist_coe_le_dist x) (dist_comm (F n) f ▸ hn)))
    fun h =>
    Metric.tendsto_nhds.mpr fun _ ε_pos =>
      (h _ (dist_mem_uniformity <| half_pos ε_pos)).mp
        (Eventually.of_forall fun n hn =>
          lt_of_le_of_lt
            ((dist_le (half_pos ε_pos).le).mpr fun x => dist_comm (f x) (F n x) ▸ le_of_lt (hn x))
            (half_lt_self ε_pos))

Premises used: half_lt_self, Iff.mpr, lt_of_le_of_lt, BoundedContinuousFunction.dist_le, half_pos, Metric.tendsto_nhds, setOf, le_of_lt, Eq.rec, HDiv.hDiv, LT.lt.le, Filter.Eventually.of_forall, dist_comm, BoundedContinuousFunction.dist_coe_le_dist, Prod.fst, Filter.Eventually.mp, LT.lt, Iff.intro, Iff.mp, Dist.dist, OfNat.ofNat, Prod.snd, DFunLike.coe, Metric.tendstoUniformly_iff, Metric.dist_mem_uniformity
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
rw :
  ∀ (x : α →ᵇ β),
    𝓝 x =
      comap (β := α →ᵤ β)
        (comp (β := α → β) (⇑UniformFun.ofFun : (a : α → β) → α →ᵤ β) (DFunLike.coe (β := fun (x : α) ↦ β)))
        (𝓝 (comp (β := α → β) (⇑UniformFun.ofFun : (a : α → β) → α →ᵤ β) (DFunLike.coe (β := fun (x : α) ↦ β)) x))
⊢ IsInducing (X := α →ᵇ β) (Y := α →ᵤ β)
    (comp (β := α → β) (⇑UniformFun.ofFun : (a : α → β) → α →ᵤ β) (DFunLike.coe (β := fun (x : α) ↦ β)))

Tactic:
rw [isInducing_iff_nhds]

Premises used: Topology.isInducing_iff_nhds
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
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))

Tactic:
fun f => eq_of_forall_le_iff fun l => ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
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))
⊢ ∀ (x : α →ᵇ β),
    𝓝 x =
      comap (β := α →ᵤ β)
        (comp (β := α → β) (⇑UniformFun.ofFun : (a : α → β) → α →ᵤ β) (DFunLike.coe (β := fun (x : α) ↦ β)))
        (𝓝 (comp (β := α → β) (⇑UniformFun.ofFun : (a : α → β) → α →ᵤ β) (DFunLike.coe (β := fun (x : α) ↦ β)) x))

Tactic:
refine fun f => eq_of_forall_le_iff fun l => ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f : α →ᵇ β
l : Filter (α →ᵇ β)
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
⊢ l ≤ 𝓝 f ↔
    l ≤
      comap (β := α →ᵤ β)
        (comp (β := α → β) (⇑UniformFun.ofFun : (a : α → β) → α →ᵤ β) (DFunLike.coe (β := fun (x : α) ↦ β)))
        (𝓝 (comp (β := α → β) (⇑UniformFun.ofFun : (a : α → β) → α →ᵤ β) (DFunLike.coe (β := fun (x : α) ↦ β)) f))

Tactic:
rw [← tendsto_iff_comap, ← tendsto_id', tendsto_iff_tendstoUniformly,
    UniformFun.tendsto_iff_tendstoUniformly]

Premises used: UniformFun.tendsto_iff_tendstoUniformly, Filter.tendsto_id', Filter.tendsto_iff_comap, BoundedContinuousFunction.tendsto_iff_tendstoUniformly
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f : α →ᵇ β
l : Filter (α →ᵇ β)
⊢ 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:
simp [comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
⊢ IsEmbedding (X := α →ᵇ β) (Y := α →ᵤ β)
    (comp (β := α → β) (⇑UniformFun.ofFun : (a : α → β) → α →ᵤ β) (DFunLike.coe (β := fun (x : α) ↦ β)))

Tactic:
⟨isInducing_coeFn, fun _ _ h => ext fun x => congr_fun h x⟩

Premises used: BoundedContinuousFunction.ext, congr_fun, BoundedContinuousFunction.isInducing_coeFn, Topology.IsEmbedding.mk
-- 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 g : α →ᵇ β
x : α
C : ℝ
b : β
⊢ ∀ (x y : α),
    dist (ContinuousMap.toFun (ContinuousMap.const α b) x) (ContinuousMap.toFun (ContinuousMap.const α b) y) ≤ 0

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
a : α
b : β
⊢ (const α b : (a : α) → β) a = b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
x : α
⊢ LipschitzWith (β := β) 1 fun (f : α →ᵇ β) ↦ (f : (a : α) → β) x

Tactic:
LipschitzWith.mk_one fun _ _ => dist_coe_le_dist x

Premises used: LipschitzWith.mk_one, BoundedContinuousFunction.dist_coe_le_dist
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
⊢ UniformContinuous (α := α →ᵇ β) (β := α → β) (DFunLike.coe (β := fun (x : α) ↦ β))

Tactic:
uniformContinuous_pi.2 fun x => (lipschitz_eval_const x).uniformContinuous

Premises used: Iff.mpr, LipschitzWith.uniformContinuous, uniformContinuous_pi, BoundedContinuousFunction.lipschitz_eval_const
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
⊢ Continuous[_, Pi.topologicalSpace] fun (f : α →ᵇ β) (x : α) ↦ (f : (a : α) → β) x

Tactic:
UniformContinuous.continuous uniformContinuous_coe

Premises used: BoundedContinuousFunction.uniformContinuous_coe, UniformContinuous.continuous
-- 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 g : α →ᵇ β
x : α
C : ℝ
⊢ ContinuousEvalConst (α →ᵇ β) α β

Tactic:
inferInstance

Premises used: inferInstance
-- 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 : α
C : ℝ
inst_3 : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
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)
⊢ ∃ (a : α →ᵇ β), Tendsto f atTop (𝓝 a)

Tactic:
rcases cauchySeq_iff_le_tendsto_0.1 hf with ⟨b, b0, b_bound, b_lim⟩

Premises used: cauchySeq_iff_le_tendsto_0, Iff.mp
-- 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 : α
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)
⊢ ∀ (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)
-- 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 : α
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
⊢ ∀ (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⟩
-- 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 : α
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
choose :
  ∀ (F : (x : α) → β) (hF : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (f n : (a : α) → β) x) atTop (𝓝 (F x))),
    ∃ (a : α →ᵇ β), Tendsto f atTop (𝓝 a)
⊢ ∃ (a : α →ᵇ β), Tendsto f atTop (𝓝 a)

Tactic:
choose F hF using fun x => cauchySeq_tendsto_of_complete (fx_cau x)

Premises used: cauchySeq_tendsto_of_complete
-- 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))
⊢ ∀ (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⟩)
-- 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
⊢ ∃ (a : α →ᵇ β), Tendsto f atTop (𝓝 a)

Tactic:
⟨⟨⟨F, ?_⟩, ?_⟩, ?_⟩

Premises used: ContinuousMap.mk, BoundedContinuousFunction.mk, Exists.intro
-- 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_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
refine_3 : Tendsto f atTop (𝓝 { toFun := F, continuous_toFun := ⋯, map_bounded' := ⋯ })
⊢ ∃ (a : α →ᵇ β), Tendsto f atTop (𝓝 a)

Tactic:
refine ⟨⟨⟨F, ?_⟩, ?_⟩, ?_⟩
-- 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:
Metric.tendstoUniformly_iff.2 fun ε ε0 => ?_

Premises used: Iff.mpr, Metric.tendstoUniformly_iff
-- 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 : ∀ (ε : ℝ) (ε0 : ε > 0), ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), dist (F x) ((f n : (a : α) → β) x) < ε
⊢ TendstoUniformly (fun (n : ℕ) (x : α) ↦ (f n : (a : α) → β) x) F atTop

Tactic:
refine Metric.tendstoUniformly_iff.2 fun ε ε0 => ?_

Premises used: Iff.mpr, Metric.tendstoUniformly_iff
-- 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
ε : ℝ
ε0 : ε > 0
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), dist (F x) ((f n : (a : α) → β) x) < ε

Tactic:
((tendsto_order.1 b_lim).2 ε ε0).mono fun n hn x => ?_

Premises used: tendsto_order, Filter.Eventually.mono, And.right, Iff.mp
-- 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
ε : ℝ
ε0 : ε > 0
refine : ∀ (n : ℕ) (hn : b n < ε) (x : α), dist (F x) ((f n : (a : α) → β) x) < ε
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), dist (F x) ((f n : (a : α) → β) x) < ε

Tactic:
refine ((tendsto_order.1 b_lim).2 ε ε0).mono fun n hn x => ?_

Premises used: tendsto_order, Filter.Eventually.mono, And.right, Iff.mp
-- 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 : α
rw : dist ((f n : (a : α) → β) x) (F x) < ε
⊢ dist (F x) ((f n : (a : α) → β) x) < ε

Tactic:
rw [dist_comm]

Premises used: dist_comm