awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 g_1 : α →ᵇ β
x : α
C : ℝ
g : α →ᵇ β
toFun : α → β
continuous_toFun : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] toFun
map_bounded' :
  ∃ (C : ℝ),
    ∀ (x y : α),
      dist ({ toFun := toFun, continuous_toFun := continuous_toFun : C(α, β) }.toFun x)
          ({ toFun := toFun, continuous_toFun := continuous_toFun : C(α, β) }.toFun y) ≤
        C
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →ᵇ β) ↦ f.toFun)
      { toFun := toFun, continuous_toFun := continuous_toFun, map_bounded' := map_bounded' })
    ((fun (f : α →ᵇ β) ↦ f.toFun) g)
⊢ { toFun := toFun, continuous_toFun := continuous_toFun, map_bounded' := map_bounded' : α →ᵇ β } = g
have obtain : ∀ (toFun_1 : α → β) (continuous_toFun_1 : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] toFun_1)
  (map_bounded'_1 :
    ∃ (C : ℝ),
      ∀ (x y : α),
        dist ({ toFun := toFun_1, continuous_toFun := continuous_toFun_1 : C(α, β) }.toFun x)
            ({ toFun := toFun_1, continuous_toFun := continuous_toFun_1 : C(α, β) }.toFun y) ≤
          C)
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : α →ᵇ β) ↦ f.toFun)
        { toFun := toFun, continuous_toFun := continuous_toFun, map_bounded' := map_bounded' })
      ((fun (f : α →ᵇ β) ↦ f.toFun)
        { toFun := toFun_1, continuous_toFun := continuous_toFun_1, map_bounded' := map_bounded'_1 })),
  { toFun := toFun, continuous_toFun := continuous_toFun, map_bounded' := map_bounded' : α →ᵇ β } =
    { toFun := toFun_1, continuous_toFun := continuous_toFun_1, map_bounded' := map_bounded'_1 }
Tactic: obtain ⟨⟨_, _⟩, _⟩ := g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
⊢ ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ C
have 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
Tactic: rcases isBounded_iff.1 (f.isBounded_range.union g.isBounded_range) with ⟨C, hC⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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
have refine_1 : ∀ (x : α),
  Membership.mem.{v, v} (α := β) (γ := Set β)
    (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β) ∪ range.{v, u + 1} (ι := α) (⇑g : (a : α) → β))
    ((f : (a : α) → β) x : β)
Tactic: refine ⟨max 0 C, le_max_left _ _, fun x => (hC ?_ ?_).trans (le_max_right _ _)⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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 : β)
⊢ ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ C
have refine_2 : ∀ (x : α),
  Membership.mem.{v, v} (α := β) (γ := Set β)
    (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β) ∪ range.{v, u + 1} (ι := α) (⇑g : (a : α) → β))
    ((g : (a : α) → β) x : β)
Tactic: refine ⟨max 0 C, le_max_left _ _, fun x => (hC ?_ ?_).trans (le_max_right _ _)⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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 : α) → β) ∪ range.{v, u + 1} (ι := α) (⇑g : (a : α) → β))
    ((f : (a : α) → β) x : β)
have refine_1 : Membership.mem.{v, v} (α := β) (γ := Set β) (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β)) ((f : (a : α) → β) x : β)
Tactic: left
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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 : α) → β) ∪ range.{v, u + 1} (ι := α) (⇑g : (a : α) → β))
    ((g : (a : α) → β) x : β)
have refine_2 : Membership.mem.{v, v} (α := β) (γ := Set β) (range.{v, u + 1} (ι := α) (⇑g : (a : α) → β)) ((g : (a : α) → β) x : β)
Tactic: right
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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
have refine_1 : ∀ (x : α),
  Membership.mem.{v, v} (α := β) (γ := Set β) (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β)) ((f : (a : α) → β) x : β)
Tactic: refine ⟨max 0 C, le_max_left _ _, fun x => (hC ?_ ?_).trans (le_max_right _ _)⟩
    <;> [left; right]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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 : β)
⊢ ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ C
have refine_2 : ∀ (x : α),
  Membership.mem.{v, v} (α := β) (γ := Set β) (range.{v, u + 1} (ι := α) (⇑g : (a : α) → β)) ((g : (a : α) → β) x : β)
Tactic: refine ⟨max 0 C, le_max_left _ _, fun x => (hC ?_ ?_).trans (le_max_right _ _)⟩
    <;> [left; right]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (hypothesis)
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
⊢ dist f g < C
have 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
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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 : β)
⊢ dist f g < C
have obtain : ∀ (x : α)
  (le : IsMaxOn (β := ℝ) (fun (x : α) ↦ dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)) univ x),
  dist f g < C
Tactic: obtain ⟨x, -, le⟩ :=
    IsCompact.exists_isMaxOn isCompact_univ Set.univ_nonempty (Continuous.continuousOn c)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst_2 : CompactSpace α
C0 : 0 < C
⊢ dist f g < C ↔ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C
have mp : dist f g < C → ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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
⊢ dist f g < C ↔ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C
have mpr : (∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C) → dist f g < C
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst_2 : CompactSpace α
C0 : 0 < C
⊢ (∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C) → dist f g < C
have pos : ∀ (h : Nonempty α),
  (∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C) → dist f g < C
Tactic: by_cases h : Nonempty α
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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
⊢ (∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C) → dist f g < C
have neg : ∀ (h : ¬Nonempty α),
  (∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C) → dist f g < C
Tactic: by_cases h : Nonempty α
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst_2 : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ dist f g < C
have h₁ : dist f g = 0
Tactic: convert! C0
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst_2 : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ dist f g = 0
have apply : dist f g ≤ 0
Tactic: apply le_antisymm _ dist_nonneg'
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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
⊢ x_1 = y
have h : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((x_1 : (a : α) → β) x : β) ((y : (a : α) → β) x : β)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
⊢ 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}) : ℝ)
have 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)})
Tactic: rw [val_eq_coe, coe_sInf, coe_image]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
⊢ 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)})
have 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 sorry})
Tactic: simp_rw [mem_setOf_eq, ← NNReal.coe_le_coe, NNReal.coe_mk, exists_prop, coe_nndist]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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 ⋯})
⊢ 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)})
have 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 sorry) : ℝ)})
Tactic: simp_rw [mem_setOf_eq, ← NNReal.coe_le_coe, NNReal.coe_mk, exists_prop, coe_nndist]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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 ⋯) : ℝ)})
⊢ 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)})
have 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})
Tactic: simp_rw [mem_setOf_eq, ← NNReal.coe_le_coe, NNReal.coe_mk, exists_prop, coe_nndist]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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})
⊢ 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)})
have 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})
Tactic: simp_rw [mem_setOf_eq, ← NNReal.coe_le_coe, NNReal.coe_mk, exists_prop, coe_nndist]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
inst_2 : IsEmpty α
⊢ dist f g = 0
have rw : dist g g = 0
Tactic: rw [(ext isEmptyElim : f = g), dist_self]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
inst_2 : IsEmpty α
rw : dist g g = 0
⊢ dist f g = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [(ext isEmptyElim : f = g), dist_self]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
⊢ dist f g = ⨆ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
have inl : IsEmpty α → dist f g = ⨆ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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 : β)
⊢ dist f g = ⨆ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
have inr : Nonempty α → dist f g = ⨆ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
h : IsEmpty α
⊢ dist f g = ⨆ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
have inl : dist f g = sSup ∅
Tactic: rw [iSup_of_empty', Real.sSup_empty, dist_zero_of_empty]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
h : IsEmpty α
inl : dist f g = sSup ∅
⊢ dist f g = ⨆ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
have inl₁ : dist f g = 0
Tactic: rw [iSup_of_empty', Real.sSup_empty, dist_zero_of_empty]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
h : IsEmpty α
inl : dist f g = sSup ∅
inl₁ : dist f g = 0
⊢ dist f g = ⨆ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
have inl₂ : Eq (α := ℝ) 0 0
Tactic: rw [iSup_of_empty', Real.sSup_empty, dist_zero_of_empty]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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 : β)
have inr : BddAbove (α := ℝ) (range fun (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)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
⊢ Eq (α := ℝ) (⨆ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β))
    (↑(⨆ (x : α), nndist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)) : ℝ)
have simp_rw : ⨆ (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]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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 : β)) : ℝ)
⊢ Eq (α := ℝ) (⨆ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β))
    (↑(⨆ (x : α), nndist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)) : ℝ)
have simp_rw₁ : Eq (α := ℝ) (⨆ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β))
  (⨆ (i : α), (↑(nndist.{v} (α := β) ((f : (a : α) → β) i : β) ((g : (a : α) → β) i : β)) : ℝ))
Tactic: simp_rw [val_eq_coe, coe_iSup, coe_nndist]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
⊢ edist f g = ⨆ (x : α), edist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
have simp_rw : (↑(⨆ (x : α), nndist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)) : ENNReal) =
  ⨆ (x : α), (↑(nndist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)) : ENNReal)
Tactic: simp_rw [edist_nndist, nndist_eq_iSup]