-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem dist_lt_iff_of_compact [CompactSpace α] (C0 : (0 : ℝ) < C) :
    dist f g < C ↔ ∀ x : α, dist (f x) (g x) < C

Proof state:
case mpr
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
⊢ (∀ (x : α), dist (f x) (g x) < C) → dist f g < C

Tactic:
by_cases h : Nonempty α

Result:
case pos
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : Nonempty α
⊢ (∀ (x : α), dist (f x) (g x) < C) → dist f g < C

case neg
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ (∀ (x : α), dist (f x) (g x) < C) → dist f g < C

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ sInf {C | 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C} ≤ 0

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

Result:
no goals

Proof state:
case h.e'_3
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ dist f g = 0

Tactic:
apply le_antisymm _ dist_nonneg'

Result:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ dist f g ≤ 0

Proof state:
case mp
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
w : dist f g < C
x : α
⊢ dist (f x) (g x) < C

Tactic:
exact lt_of_le_of_lt (dist_coe_le_dist x) w

Result:
no goals

Proof state:
case pos
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : Nonempty α
⊢ (∀ (x : α), dist (f x) (g x) < C) → dist f g < C

Tactic:
exact dist_lt_of_nonempty_compact

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
⊢ dist f g < C ↔ ∀ (x : α), dist (f x) (g x) < C

Tactic:
fconstructor

Result:
case mp
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
⊢ dist f g < C → ∀ (x : α), dist (f x) (g x) < C

case mpr
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
⊢ (∀ (x : α), dist (f x) (g x) < C) → dist f g < C

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ dist f g ≤ 0

Tactic:
rw [dist_eq]

Result:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ sInf {C | 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C} ≤ 0

Proof state:
case neg
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ (∀ (x : α), dist (f x) (g x) < C) → dist f g < C

Tactic:
rintro -

Result:
case neg
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ dist f g < C

Proof state:
case mp
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
⊢ dist f g < C → ∀ (x : α), dist (f x) (g x) < C

Tactic:
intro w x

Result:
case mp
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
w : dist f g < C
x : α
⊢ dist (f x) (g x) < C

Proof state:
case neg
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ dist f g < C

Tactic:
convert C0

Result:
case h.e'_3
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ dist f g = 0