awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℝ
δ : Type u_2
inst_3 : TopologicalSpace δ
inst_4 : DiscreteTopology δ
f : α ↪ δ
g : α →ᵇ β
h : δ →ᵇ β
rw :
  Bornology.IsBounded.{v} (α := β)
    (range.{v, u + 1} (ι := α) (⇑g : (a : α) → β) ∪
      image.{u_2, v} (α := δ) (⇑h : (a : δ) → β) (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ)
⊢ ∃ (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

Tactic:
rw [← isBounded_range_iff, range_extend f.injective]

Premises used: Function.Embedding.injective, Set.range_extend, Metric.isBounded_range_iff
-- 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 : ℝ
δ : Type u_2
inst_3 : TopologicalSpace δ
inst_4 : DiscreteTopology δ
f : α ↪ δ
g : α →ᵇ β
h : δ →ᵇ β
⊢ Bornology.IsBounded.{v} (α := β)
    (range.{v, u + 1} (ι := α) (⇑g : (a : α) → β) ∪
      image.{u_2, v} (α := δ) (⇑h : (a : δ) → β) (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ)

Tactic:
g.isBounded_range.union (h.isBounded_image _)

Premises used: BoundedContinuousFunction.isBounded_range, BoundedContinuousFunction.isBounded_image, Bornology.IsBounded.union
-- 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 : ℝ
δ : Type u_2
inst_3 : TopologicalSpace δ
inst_4 : DiscreteTopology δ
f : α ↪ δ
g : α →ᵇ β
h : δ →ᵇ β
⊢ Bornology.IsBounded.{v} (α := β)
    (range.{v, u + 1} (ι := α) (⇑g : (a : α) → β) ∪
      image.{u_2, v} (α := δ) (⇑h : (a : δ) → β) (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ)

Tactic:
exact g.isBounded_range.union (h.isBounded_image _)

Premises used: BoundedContinuousFunction.isBounded_range, BoundedContinuousFunction.isBounded_image, Bornology.IsBounded.union
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g : α →ᵇ β
h : δ →ᵇ β
x : α
⊢ Eq.{v + 1} (α := β) ((extend f g h : (a : δ) → β) ((f : (a : α) → δ) x : δ) : β) ((g : (a : α) → β) x : β)

Tactic:
f.injective.extend_apply _ _ _

Premises used: Function.Injective.extend_apply, dite, Function.extend, Function.Embedding.injective
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g : α →ᵇ β
h : δ →ᵇ β
⊢ Eq (α := α → β) (Function.comp.{u + 1, u_2 + 1, v + 1} (β := δ) (⇑(extend f g h) : (a : δ) → β) (⇑f : (a : α) → δ))
    (⇑g : (a : α) → β)

Tactic:
extend_comp f.injective _ _

Premises used: dite, Function.extend, Function.extend_comp, Function.Embedding.injective
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
x : δ
hx : x ∉ range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ)
g : α →ᵇ β
h : δ →ᵇ β
⊢ Eq.{v + 1} (α := β) ((extend f g h : (a : δ) → β) x : β) ((h : (a : δ) → β) x : β)

Tactic:
extend_apply' _ _ _ hx

Premises used: dite, Function.extend, Function.extend_apply'
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
inst_4 : IsEmpty α
f : α ↪ δ
g : α →ᵇ β
h : δ →ᵇ β
⊢ extend f g h = h

Tactic:
DFunLike.coe_injective <| Function.extend_of_isEmpty f g h

Premises used: DFunLike.coe_injective, Function.extend_of_isEmpty, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
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 : α) → δ))ᶜ))

Tactic:
le_antisymm ((dist_le <| le_max_iff.2 <| Or.inl dist_nonneg).2 fun x => ?_) (max_le ?_ ?_)

Premises used: Iff.mpr, BoundedContinuousFunction.dist_le, dist_nonneg, le_antisymm, max_le, Or.inl, le_max_iff
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
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 : α) → δ))ᶜ))
refine_2 : dist g₁ g₂ ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)
refine_3 :
  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₂)
⊢ 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 : α) → δ))ᶜ))

Tactic:
refine le_antisymm ((dist_le <| le_max_iff.2 <| Or.inl dist_nonneg).2 fun x => ?_) (max_le ?_ ?_)

Premises used: Iff.mpr, BoundedContinuousFunction.dist_le, dist_nonneg, le_antisymm, max_le, Or.inl, le_max_iff
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : δ
refine_1 :
  ∀ (x : α),
    dist.{v} (α := β) ((extend f g₁ h₁ : (a : δ) → β) ((f : (a : α) → δ) x : δ) : β)
        ((extend f g₂ h₂ : (a : δ) → β) ((f : (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 : α) → δ))ᶜ))
refine_1₁ :
  ∀ (hx : ¬∃ (y : α), (f : (a : α) → δ) y = 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.{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:
rcases em (∃ y, f y = x) with (⟨x, rfl⟩ | hx)

Premises used: Exists, em, Eq, DFunLike.coe, rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
refine_1 :
  dist.{v} (α := β) ((g₁ : (a : α) → β) x : β) ((g₂ : (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.{v} (α := β) ((extend f g₁ h₁ : (a : δ) → β) ((f : (a : α) → δ) x : δ) : β)
      ((extend f g₂ h₂ : (a : δ) → β) ((f : (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:
simp only [extend_apply]

Premises used: BoundedContinuousFunction.extend_apply
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist.{v} (α := β) ((g₁ : (a : α) → β) x : β) ((g₂ : (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:
(dist_coe_le_dist x).trans (le_max_left _ _)

Premises used: BoundedContinuousFunction.dist_coe_le_dist, LE.le.trans, le_max_left
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist.{v} (α := β) ((g₁ : (a : α) → β) x : β) ((g₂ : (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:
exact (dist_coe_le_dist x).trans (le_max_left _ _)

Premises used: BoundedContinuousFunction.dist_coe_le_dist, LE.le.trans, le_max_left
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : δ
hx : ¬∃ (y : α), (f : (a : α) → δ) y = x
refine_1 :
  dist.{v} (α := β) ((h₁ : (a : δ) → β) x : β) ((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.{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:
simp only [extend_apply' hx]

Premises used: BoundedContinuousFunction.extend_apply'
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : δ
hx : ¬∃ (y : α), (f : (a : α) → δ) y = x
⊢ Membership.mem (γ := Set δ) (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ x

Tactic:
hx

Premises used: Set.Mem, setOf, Set.range, Not
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : δ
hx : ¬∃ (y : α), (f : (a : α) → δ) y = x
refine_1 :
  ∀ (x : { x : δ // Membership.mem (γ := Set δ) (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ x }),
    dist.{v} (α := β) ((h₁ : (a : δ) → β) (↑x : δ) : β) ((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.{v} (α := β) ((h₁ : (a : δ) → β) x : β) ((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:
lift x to ((range f)ᶜ : Set δ) using hx

Premises used: Compl.compl, Set.range, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : { x : δ // Membership.mem (γ := Set δ) (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ x }
⊢ dist.{v} (α := β) ((h₁ : (a : δ) → β) (↑x : δ) : β) ((h₂ : (a : δ) → β) (↑x : δ) : β) =
    dist.{v} (α := β)
      ((h₁.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ :
            (a : (↑(range (⇑f : (a : α) → δ))ᶜ : Type u_2)) → β)
          x :
        β)
      ((h₂.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ :
            (a : (↑(range (⇑f : (a : α) → δ))ᶜ : Type u_2)) → β)
          x :
        β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : { x : δ // Membership.mem (γ := Set δ) (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ x }
⊢ dist.{v} (α := β)
      ((h₁.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ :
            (a : (↑(range (⇑f : (a : α) → δ))ᶜ : Type u_2)) → β)
          x :
        β)
      ((h₂.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ :
            (a : (↑(range (⇑f : (a : α) → δ))ᶜ : Type u_2)) → β)
          x :
        β) ≤
    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:
dist_coe_le_dist x

Premises used: setOf, BoundedContinuousFunction.dist_coe_le_dist
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : { x : δ // Membership.mem (γ := Set δ) (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ x }
⊢ 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 : α) → δ))ᶜ) ≤
    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:
le_max_right _ _

Premises used: le_max_right
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : { x : δ // Membership.mem (γ := Set δ) (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ x }
⊢ dist.{v} (α := β) ((h₁ : (a : δ) → β) (↑x : δ) : β) ((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:
calc
        dist (h₁ x) (h₂ x) = dist (h₁.restrict (range f)ᶜ x) (h₂.restrict (range f)ᶜ x) := rfl
        _ ≤ dist (h₁.restrict (range f)ᶜ) (h₂.restrict (range f)ᶜ) := dist_coe_le_dist x
        _ ≤ _ := le_max_right _ _

Premises used: le_max_right, Compl.compl, BoundedContinuousFunction.dist_coe_le_dist, Dist.dist, Set.range, Subtype.val, DFunLike.coe, rfl, BoundedContinuousFunction.restrict
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
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 g₁ g₂ ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)

Tactic:
(dist_le dist_nonneg).2 fun x => ?_

Premises used: Iff.mpr, BoundedContinuousFunction.dist_le, dist_nonneg
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
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_2 :
  ∀ (x : α),
    dist.{v} (α := β) ((g₁ : (a : α) → β) x : β) ((g₂ : (a : α) → β) x : β) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)
⊢ dist g₁ g₂ ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)

Tactic:
refine (dist_le dist_nonneg).2 fun x => ?_

Premises used: Iff.mpr, BoundedContinuousFunction.dist_le, dist_nonneg
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
refine_2 :
  dist.{v} (α := β) ((extend f g₁ h₁ : (a : δ) → β) ((f : (a : α) → δ) x : δ) : β)
      ((extend f g₂ h₂ : (a : δ) → β) ((f : (a : α) → δ) x : δ) : β) ≤
    dist (extend f g₁ h₁) (extend f g₂ h₂)
⊢ dist.{v} (α := β) ((g₁ : (a : α) → β) x : β) ((g₂ : (a : α) → β) x : β) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)

Tactic:
rw [← extend_apply f g₁ h₁, ← extend_apply f g₂ h₂]

Premises used: BoundedContinuousFunction.extend_apply
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist.{v} (α := β) ((extend f g₁ h₁ : (a : δ) → β) ((f : (a : α) → δ) x : δ) : β)
      ((extend f g₂ h₂ : (a : δ) → β) ((f : (a : α) → δ) x : δ) : β) ≤
    dist (extend f g₁ h₁) (extend f g₂ h₂)

Tactic:
dist_coe_le_dist _

Premises used: BoundedContinuousFunction.dist_coe_le_dist
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist.{v} (α := β) ((extend f g₁ h₁ : (a : δ) → β) ((f : (a : α) → δ) x : δ) : β)
      ((extend f g₂ h₂ : (a : δ) → β) ((f : (a : α) → δ) x : δ) : β) ≤
    dist (extend f g₁ h₁) (extend f g₂ h₂)

Tactic:
exact dist_coe_le_dist _

Premises used: BoundedContinuousFunction.dist_coe_le_dist
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
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 (α := 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₂)

Tactic:
(dist_le dist_nonneg).2 fun x => ?_

Premises used: Iff.mpr, BoundedContinuousFunction.dist_le, dist_nonneg
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
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_3 :
  ∀ (x : (↑(range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ : Type u_2)),
    dist.{v} (α := β)
        ((h₁.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ :
              (a : (↑(range (⇑f : (a : α) → δ))ᶜ : Type u_2)) → β)
            x :
          β)
        ((h₂.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ :
              (a : (↑(range (⇑f : (a : α) → δ))ᶜ : Type u_2)) → β)
            x :
          β) ≤
      dist (extend f g₁ h₁) (extend f g₂ h₂)
⊢ 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₂)

Tactic:
refine (dist_le dist_nonneg).2 fun x => ?_

Premises used: Iff.mpr, BoundedContinuousFunction.dist_le, dist_nonneg
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : (↑(range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ : Type u_2)
rw :
  dist.{v} (α := β) ((h₁ : (a : δ) → β) (↑x : δ) : β) ((h₂ : (a : δ) → β) (↑x : δ) : β) =
    dist.{v} (α := β) ((h₁ : (a : δ) → β) (↑x : δ) : β) ((extend f g₂ h₂ : (a : δ) → β) (↑x : δ) : β)
rw₁ rw₂ :
  dist.{v} (α := β) ((h₁ : (a : δ) → β) (↑x : δ) : β) ((h₂ : (a : δ) → β) (↑x : δ) : β) =
    dist.{v} (α := β) ((h₁ : (a : δ) → β) (↑x : δ) : β) ((h₂ : (a : δ) → β) (↑x : δ) : β)
⊢ dist.{v} (α := β) ((h₁ : (a : δ) → β) (↑x : δ) : β) ((h₂ : (a : δ) → β) (↑x : δ) : β) =
    dist.{v} (α := β) ((extend f g₁ h₁ : (a : δ) → β) (↑x : δ) : β) ((extend f g₂ h₂ : (a : δ) → β) (↑x : δ) : β)

Tactic:
rw [extend_apply' x.coe_prop, extend_apply' x.coe_prop]

Premises used: Subtype.coe_prop, BoundedContinuousFunction.extend_apply'
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : (↑(range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ : Type u_2)
⊢ dist.{v} (α := β) ((extend f g₁ h₁ : (a : δ) → β) (↑x : δ) : β) ((extend f g₂ h₂ : (a : δ) → β) (↑x : δ) : β) ≤
    dist (extend f g₁ h₁) (extend f g₂ h₂)

Tactic:
dist_coe_le_dist _

Premises used: BoundedContinuousFunction.dist_coe_le_dist