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 : α →ᵇ β
rcases :
  ∀ (C : ℝ)
    (hC :
      ∀ ⦃x : β⦄,
        Membership.mem (γ := Set β)
            (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β) ∪ range.{v, u + 1} (ι := α) (⇑g : (a : α) → β)) x →
          ∀ ⦃y : β⦄,
            Membership.mem (γ := Set β)
                (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β) ∪ range.{v, u + 1} (ι := α) (⇑g : (a : α) → β)) y →
              dist x y ≤ C),
    ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ C
⊢ ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ C

Tactic:
rcases isBounded_iff.1 (f.isBounded_range.union g.isBounded_range) with ⟨C, hC⟩

Premises used: BoundedContinuousFunction.isBounded_range, Metric.isBounded_iff, Iff.mp, Bornology.IsBounded.union
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
hC :
  ∀ ⦃x : β⦄,
    Membership.mem (γ := Set β)
        (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β) ∪ range.{v, u + 1} (ι := α) (⇑g : (a : α) → β)) x →
      ∀ ⦃y : β⦄,
        Membership.mem (γ := Set β)
            (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β) ∪ range.{v, u + 1} (ι := α) (⇑g : (a : α) → β)) y →
          dist x y ≤ C
⊢ ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ C

Tactic:
⟨max 0 C, le_max_left _ _, fun x => (hC ?_ ?_).trans (le_max_right _ _)⟩

Premises used: le_max_right, Max.max, And.intro, Exists.intro, LE.le.trans, OfNat.ofNat, le_max_left
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
hC :
  ∀ ⦃x : β⦄,
    Membership.mem (γ := Set β)
        (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β) ∪ range.{v, u + 1} (ι := α) (⇑g : (a : α) → β)) x →
      ∀ ⦃y : β⦄,
        Membership.mem (γ := Set β)
            (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β) ∪ range.{v, u + 1} (ι := α) (⇑g : (a : α) → β)) y →
          dist x y ≤ C
refine_1 :
  ∀ (x : α),
    Membership.mem.{v, v} (α := β) (γ := Set β)
      (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β) ∪ range.{v, u + 1} (ι := α) (⇑g : (a : α) → β))
      ((f : (a : α) → β) x : β)
refine_2 :
  ∀ (x : α),
    Membership.mem.{v, v} (α := β) (γ := Set β)
      (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β) ∪ range.{v, u + 1} (ι := α) (⇑g : (a : α) → β))
      ((g : (a : α) → β) x : β)
⊢ ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ C

Tactic:
refine ⟨max 0 C, le_max_left _ _, fun x => (hC ?_ ?_).trans (le_max_right _ _)⟩
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
hC :
  ∀ ⦃x : β⦄,
    Membership.mem (γ := Set β)
        (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β) ∪ range.{v, u + 1} (ι := α) (⇑g : (a : α) → β)) x →
      ∀ ⦃y : β⦄,
        Membership.mem (γ := Set β)
            (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β) ∪ range.{v, u + 1} (ι := α) (⇑g : (a : α) → β)) y →
          dist x y ≤ C
x : α
refine_1 :
  Membership.mem.{v, v} (α := β) (γ := Set β) (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β)) ((f : (a : α) → β) x : β)
⊢ Membership.mem.{v, v} (α := β) (γ := Set β)
    (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β) ∪ range.{v, u + 1} (ι := α) (⇑g : (a : α) → β))
    ((f : (a : α) → β) x : β)

Tactic:
left
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
hC :
  ∀ ⦃x : β⦄,
    Membership.mem (γ := Set β)
        (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β) ∪ range.{v, u + 1} (ι := α) (⇑g : (a : α) → β)) x →
      ∀ ⦃y : β⦄,
        Membership.mem (γ := Set β)
            (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β) ∪ range.{v, u + 1} (ι := α) (⇑g : (a : α) → β)) y →
          dist x y ≤ C
x : α
refine_2 :
  Membership.mem.{v, v} (α := β) (γ := Set β) (range.{v, u + 1} (ι := α) (⇑g : (a : α) → β)) ((g : (a : α) → β) x : β)
⊢ Membership.mem.{v, v} (α := β) (γ := Set β)
    (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β) ∪ range.{v, u + 1} (ι := α) (⇑g : (a : α) → β))
    ((g : (a : α) → β) x : β)

Tactic:
right
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
hC :
  ∀ ⦃x : β⦄,
    Membership.mem (γ := Set β)
        (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β) ∪ range.{v, u + 1} (ι := α) (⇑g : (a : α) → β)) x →
      ∀ ⦃y : β⦄,
        Membership.mem (γ := Set β)
            (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β) ∪ range.{v, u + 1} (ι := α) (⇑g : (a : α) → β)) y →
          dist x y ≤ C
refine_1 :
  ∀ (x : α),
    Membership.mem.{v, v} (α := β) (γ := Set β) (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β)) ((f : (a : α) → β) x : β)
refine_2 :
  ∀ (x : α),
    Membership.mem.{v, v} (α := β) (γ := Set β) (range.{v, u + 1} (ι := α) (⇑g : (a : α) → β)) ((g : (a : α) → β) x : β)
⊢ ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ C

Tactic:
refine ⟨max 0 C, le_max_left _ _, fun x => (hC ?_ ?_).trans (le_max_right _ _)⟩
    <;> [left; right]
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
hC :
  ∀ ⦃x : β⦄,
    Membership.mem (γ := Set β)
        (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β) ∪ range.{v, u + 1} (ι := α) (⇑g : (a : α) → β)) x →
      ∀ ⦃y : β⦄,
        Membership.mem (γ := Set β)
            (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β) ∪ range.{v, u + 1} (ι := α) (⇑g : (a : α) → β)) y →
          dist x y ≤ C
x : α
⊢ Membership.mem.{v, v} (α := β) (γ := Set β) (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β)) ((f : (a : α) → β) x : β)

Tactic:
apply mem_range_self

Premises used: Set.mem_range_self
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
hC :
  ∀ ⦃x : β⦄,
    Membership.mem (γ := Set β)
        (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β) ∪ range.{v, u + 1} (ι := α) (⇑g : (a : α) → β)) x →
      ∀ ⦃y : β⦄,
        Membership.mem (γ := Set β)
            (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β) ∪ range.{v, u + 1} (ι := α) (⇑g : (a : α) → β)) y →
          dist x y ≤ C
x : α
⊢ Membership.mem.{v, v} (α := β) (γ := Set β) (range.{v, u + 1} (ι := α) (⇑g : (a : α) → β)) ((g : (a : α) → β) x : β)

Tactic:
apply mem_range_self

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

Tactic:
le_csInf dist_set_exists fun _ hb => hb.2 x

Premises used: le_csInf, And.right, BoundedContinuousFunction.dist_set_exists
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
⊢ 0 ≤ dist f g

Tactic:
le_csInf dist_set_exists fun _ => And.left

Premises used: le_csInf, And.left, BoundedContinuousFunction.dist_set_exists
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
C0 : 0 ≤ C
⊢ dist f g ≤ C ↔ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ C

Tactic:
⟨fun h x => le_trans (dist_coe_le_dist x) h, fun H => csInf_le ⟨0, fun _ => And.left⟩ ⟨C0, H⟩⟩

Premises used: BoundedContinuousFunction.dist_coe_le_dist, And.left, And.intro, Iff.intro, Exists.intro, OfNat.ofNat, csInf_le, le_trans
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst_2 : Nonempty α
⊢ dist f g ≤ C ↔ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ C

Tactic:
⟨fun h x => le_trans (dist_coe_le_dist x) h,
    fun w => (dist_le (le_trans dist_nonneg (w (Nonempty.some ‹_›)))).mpr w⟩

Premises used: Iff.mpr, BoundedContinuousFunction.dist_le, dist_nonneg, Nonempty.some, BoundedContinuousFunction.dist_coe_le_dist, Iff.intro, le_trans
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst_2 : Nonempty α
inst_3 : CompactSpace α
w : ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C
⊢ Continuous[inst, _] fun (x : α) ↦ dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
fun_prop
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst_2 : Nonempty α
inst_3 : CompactSpace α
w : ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C
⊢ Continuous[inst, _] fun (x : α) ↦ dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
have c : Continuous fun x => dist (f x) (g x) := by fun_prop
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst_2 : Nonempty α
inst_3 : CompactSpace α
w : ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C
c : Continuous[inst, _] fun (x : α) ↦ dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
obtain :
  ∀ (x : α)
    (le :
      IsMaxOn (β := ℝ) (fun (x : α) ↦ dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)) univ x),
    dist f g < C
⊢ dist f g < C

Tactic:
obtain ⟨x, -, le⟩ :=
    IsCompact.exists_isMaxOn isCompact_univ Set.univ_nonempty (Continuous.continuousOn c)

Premises used: Continuous.continuousOn, Set.univ_nonempty, isCompact_univ, IsCompact.exists_isMaxOn
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst_2 : Nonempty α
inst_3 : CompactSpace α
w : ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C
c : Continuous[inst, _] fun (x : α) ↦ dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
x : α
le : IsMaxOn (β := ℝ) (fun (x : α) ↦ dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)) univ x
⊢ dist f g < C

Tactic:
lt_of_le_of_lt (dist_le_iff_of_nonempty.mpr fun y => le trivial) (w x)

Premises used: Iff.mpr, lt_of_le_of_lt, trivial, BoundedContinuousFunction.dist_le_iff_of_nonempty
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst_2 : Nonempty α
inst_3 : CompactSpace α
w : ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C
c : Continuous[inst, _] fun (x : α) ↦ dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
x : α
le : IsMaxOn (β := ℝ) (fun (x : α) ↦ dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)) univ x
⊢ dist f g < C

Tactic:
exact lt_of_le_of_lt (dist_le_iff_of_nonempty.mpr fun y => le trivial) (w x)

Premises used: Iff.mpr, lt_of_le_of_lt, trivial, BoundedContinuousFunction.dist_le_iff_of_nonempty
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst_2 : CompactSpace α
C0 : 0 < C
mp : dist f g < C → ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C
mpr : (∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C) → dist f g < C
⊢ dist f g < C ↔ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C

Tactic:
fconstructor
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst_2 : CompactSpace α
C0 : 0 < C
w : dist f g < C
x : α
⊢ dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C

Tactic:
lt_of_le_of_lt (dist_coe_le_dist x) w

Premises used: lt_of_le_of_lt, BoundedContinuousFunction.dist_coe_le_dist
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst_2 : CompactSpace α
C0 : 0 < C
w : dist f g < C
x : α
⊢ dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C

Tactic:
exact lt_of_le_of_lt (dist_coe_le_dist x) w

Premises used: lt_of_le_of_lt, BoundedContinuousFunction.dist_coe_le_dist
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst_2 : CompactSpace α
C0 : 0 < C
pos :
  ∀ (h : Nonempty α),
    (∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C) → dist f g < C
neg :
  ∀ (h : ¬Nonempty α),
    (∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C) → dist f g < C
⊢ (∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C) → dist f g < C

Tactic:
by_cases h : Nonempty α

Premises used: Nonempty
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst_2 : CompactSpace α
C0 : 0 < C
h : Nonempty α
⊢ (∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C) → dist f g < C

Tactic:
dist_lt_of_nonempty_compact

Premises used: BoundedContinuousFunction.dist_lt_of_nonempty_compact
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst_2 : CompactSpace α
C0 : 0 < C
h : Nonempty α
⊢ (∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C) → dist f g < C

Tactic:
exact dist_lt_of_nonempty_compact

Premises used: BoundedContinuousFunction.dist_lt_of_nonempty_compact
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst_2 : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ 0 < C

Tactic:
C0
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst_2 : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
h₁ : dist f g = 0
⊢ dist f g < C

Tactic:
convert! C0
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst_2 : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
apply : dist f g ≤ 0
⊢ dist f g = 0

Tactic:
apply le_antisymm _ dist_nonneg'

Premises used: le_antisymm, _private.0.BoundedContinuousFunction.dist_nonneg'
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst_2 : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ LE.le (α := ℝ)
    (sInf {C : ℝ | 0 ≤ C ∧ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ C}) 0

Tactic:
csInf_le ⟨0, fun C => And.left⟩ ⟨le_rfl, fun x => False.elim (h (Nonempty.intro x))⟩

Premises used: le_rfl, False.elim, Nonempty.intro, And.left, And.intro, Exists.intro, OfNat.ofNat, csInf_le
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst_2 : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ LE.le (α := ℝ)
    (sInf {C : ℝ | 0 ≤ C ∧ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ C}) 0

Tactic:
exact csInf_le ⟨0, fun C => And.left⟩ ⟨le_rfl, fun x => False.elim (h (Nonempty.intro x))⟩

Premises used: le_rfl, False.elim, Nonempty.intro, And.left, And.intro, Exists.intro, OfNat.ofNat, csInf_le
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst_2 : Nonempty α
inst_3 : CompactSpace α
⊢ dist f g < C ↔ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C

Tactic:
⟨fun w x => lt_of_le_of_lt (dist_coe_le_dist x) w, dist_lt_of_nonempty_compact⟩

Premises used: lt_of_le_of_lt, BoundedContinuousFunction.dist_coe_le_dist, Iff.intro, BoundedContinuousFunction.dist_lt_of_nonempty_compact
-- 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 : ℝ
f : α →ᵇ β
x : α
⊢ dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) x : β) ≤ 0

Tactic:
simp
-- 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_1 : α →ᵇ β
x : α
C : ℝ
f g : α →ᵇ β
⊢ dist f g = dist g f

Tactic:
simp [dist_eq, dist_comm]

Premises used: BoundedContinuousFunction.dist_eq, dist_comm
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β_1 : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β_1
inst_2 : PseudoMetricSpace γ
f g : α →ᵇ β_1
x : α
C : ℝ
β : Type u_2
inst_3 : MetricSpace β
x_1 y : α →ᵇ β
hfg : dist x_1 y = 0
h : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((x_1 : (a : α) → β) x : β) ((y : (a : α) → β) x : β)
⊢ x_1 = y

Tactic:
ext x
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β_1 : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β_1
inst_2 : PseudoMetricSpace γ
f g : α →ᵇ β_1
x_1 : α
C : ℝ
β : Type u_2
inst_3 : MetricSpace β
x_2 y : α →ᵇ β
hfg : dist x_2 y = 0
x : α
⊢ Eq.{u_2 + 1} (α := β) ((x_2 : (a : α) → β) x : β) ((y : (a : α) → β) x : β)

Tactic:
eq_of_dist_eq_zero (le_antisymm (hfg ▸ dist_coe_le_dist _) dist_nonneg)

Premises used: dist_nonneg, eq_of_dist_eq_zero, le_antisymm
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β_1 : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β_1
inst_2 : PseudoMetricSpace γ
f g : α →ᵇ β_1
x_1 : α
C : ℝ
β : Type u_2
inst_3 : MetricSpace β
x_2 y : α →ᵇ β
hfg : dist x_2 y = 0
x : α
⊢ Eq.{u_2 + 1} (α := β) ((x_2 : (a : α) → β) x : β) ((y : (a : α) → β) x : β)

Tactic:
exact eq_of_dist_eq_zero (le_antisymm (hfg ▸ dist_coe_le_dist _) dist_nonneg)

Premises used: dist_nonneg, eq_of_dist_eq_zero, le_antisymm
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
rw :
  Eq (α := ℝ)
    (sInf {C : ℝ | 0 ≤ C ∧ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ C})
    (sInf
      {x : ℝ |
        ∃ (h : 0 ≤ x),
          Membership.mem (γ := Set ℝ≥0)
            {C : ℝ≥0 | ∀ (x : α), nndist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ C}
            (NNReal.mk x h)})
⊢ Eq (α := ℝ)
    (sInf {C : ℝ | 0 ≤ C ∧ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ C})
    (↑(sInf {C : ℝ≥0 | ∀ (x : α), nndist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ C}) : ℝ)

Tactic:
rw [val_eq_coe, coe_sInf, coe_image]

Premises used: NNReal.val_eq_coe, NNReal.coe_image, NNReal.coe_sInf
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
simp_rw :
  Eq (α := ℝ)
    (sInf {C : ℝ | 0 ≤ C ∧ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ C})
    (sInf
      {x : ℝ |
        ∃ (h : 0 ≤ x),
          ∀ (x_1 : α), nndist.{v} (α := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) ≤ NNReal.mk x ⋯})
simp_rw₁ :
  Eq (α := ℝ)
    (sInf {C : ℝ | 0 ≤ C ∧ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ C})
    (sInf
      {x : ℝ |
        ∃ (h : 0 ≤ x),
          ∀ (x_1 : α),
            (↑(nndist.{v} (α := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)) : ℝ) ≤
              (↑(NNReal.mk x ⋯) : ℝ)})
simp_rw₂ :
  Eq (α := ℝ)
    (sInf {C : ℝ | 0 ≤ C ∧ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ C})
    (sInf
      {x : ℝ |
        ∃ (_ : 0 ≤ x),
          ∀ (x_1 : α), (↑(nndist.{v} (α := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)) : ℝ) ≤ x})
simp_rw₃ :
  Eq (α := ℝ)
    (sInf {C : ℝ | 0 ≤ C ∧ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ C})
    (sInf
      {x : ℝ |
        0 ≤ x ∧ ∀ (x_1 : α), (↑(nndist.{v} (α := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)) : ℝ) ≤ x})
⊢ Eq (α := ℝ)
    (sInf {C : ℝ | 0 ≤ C ∧ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ C})
    (sInf
      {x : ℝ |
        ∃ (h : 0 ≤ x),
          Membership.mem (γ := Set ℝ≥0)
            {C : ℝ≥0 | ∀ (x : α), nndist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ C}
            (NNReal.mk x h)})

Tactic:
simp_rw [mem_setOf_eq, ← NNReal.coe_le_coe, NNReal.coe_mk, exists_prop, coe_nndist]

Premises used: coe_nndist, NNReal.coe_mk, Set.mem_setOf_eq, exists_prop, NNReal.coe_le_coe
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
⊢ ∃ (C : ℝ≥0), ∀ (x : α), nndist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ C

Tactic:
Subtype.exists.mpr <| dist_set_exists.imp fun _ ⟨ha, h⟩ => ⟨ha, h⟩

Premises used: Iff.mpr, Subtype.exists, NNReal, Exists.imp, BoundedContinuousFunction.dist_set_exists
-- 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 : β) ≤ nndist f g

Tactic:
dist_coe_le_dist x

Premises used: BoundedContinuousFunction.dist_coe_le_dist
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
inst_2 : IsEmpty α
rw : dist g g = 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ dist f g = 0

Tactic:
rw [(ext isEmptyElim : f = g), dist_self]

Premises used: BoundedContinuousFunction.ext, isEmptyElim, dist_self
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
inl : IsEmpty α → dist f g = ⨆ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
inr : Nonempty α → dist f g = ⨆ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
⊢ dist f g = ⨆ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
h : IsEmpty α
inl : dist f g = sSup ∅
inl₁ : dist f g = 0
inl₂ inl₃ : Eq (α := ℝ) 0 0
⊢ dist f g = ⨆ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
rw [iSup_of_empty', Real.sSup_empty, dist_zero_of_empty]

Premises used: Real.sSup_empty, BoundedContinuousFunction.dist_zero_of_empty, iSup_of_empty'