-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem dist_extend_extend (f : α ↪ δ) (g₁ g₂ : α →ᵇ β) (h₁ h₂ : δ →ᵇ β) :
    dist (g₁.extend f h₁) (g₂.extend f h₂) =
      max (dist g₁ g₂) (dist (h₁.restrict (range f)ᶜ) (h₂.restrict (range f)ᶜ))

Proof state:
case refine_3
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : ↑(range ⇑f)ᶜ
⊢ dist ((h₁.restrict (range ⇑f)ᶜ) x) ((h₂.restrict (range ⇑f)ᶜ) x) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)

Tactic:
calc
  dist (h₁ x) (h₂ x) = dist (extend f g₁ h₁ x) (extend f g₂ h₂ x) := by
    rw [extend_apply' x.coe_prop, extend_apply' x.coe_prop]
  _ ≤ _ := dist_coe_le_dist _

Result:
no goals

Proof state:
case refine_3
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
⊢ dist (h₁.restrict (range ⇑f)ᶜ) (h₂.restrict (range ⇑f)ᶜ) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)

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

Result:
case refine_3
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : ↑(range ⇑f)ᶜ
⊢ dist ((h₁.restrict (range ⇑f)ᶜ) x) ((h₂.restrict (range ⇑f)ᶜ) x) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)

Proof state:
case refine_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
⊢ dist g₁ g₂ ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)

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

Result:
case refine_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist (g₁ x) (g₂ x) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)

Proof state:
case refine_1.inr
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : δ
hx : ¬∃ y, f y = x
⊢ dist ((extend f g₁ h₁) x) ((extend f g₂ h₂) x) ≤ dist g₁ g₂ ⊔ dist (h₁.restrict (range ⇑f)ᶜ) (h₂.restrict (range ⇑f)ᶜ)

Tactic:
simp only [extend_apply' hx]

Result:
case refine_1.inr
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : δ
hx : ¬∃ y, f y = x
⊢ dist (h₁ x) (h₂ x) ≤ dist g₁ g₂ ⊔ dist (h₁.restrict (range ⇑f)ᶜ) (h₂.restrict (range ⇑f)ᶜ)

Proof state:
case refine_1.inr
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : δ
hx : ¬∃ y, f y = x
⊢ dist (h₁ x) (h₂ x) ≤ dist g₁ g₂ ⊔ dist (h₁.restrict (range ⇑f)ᶜ) (h₂.restrict (range ⇑f)ᶜ)

Tactic:
lift x to ((range f)ᶜ : Set δ) using hx

Result:
case refine_1.inr.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : { x // x ∈ (range ⇑f)ᶜ }
⊢ dist (h₁ ↑x) (h₂ ↑x) ≤ dist g₁ g₂ ⊔ dist (h₁.restrict (range ⇑f)ᶜ) (h₂.restrict (range ⇑f)ᶜ)

Proof state:
case refine_1.inl.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist ((extend f g₁ h₁) (f x)) ((extend f g₂ h₂) (f x)) ≤
    dist g₁ g₂ ⊔ dist (h₁.restrict (range ⇑f)ᶜ) (h₂.restrict (range ⇑f)ᶜ)

Tactic:
simp only [extend_apply]

Result:
case refine_1.inl.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist (g₁ x) (g₂ x) ≤ dist g₁ g₂ ⊔ dist (h₁.restrict (range ⇑f)ᶜ) (h₂.restrict (range ⇑f)ᶜ)

Proof state:
case refine_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist (g₁ x) (g₂ x) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)

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

Result:
case refine_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist ((extend f g₁ h₁) (f x)) ((extend f g₂ h₂) (f x)) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)

Proof state:
case refine_1.inl.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist (g₁ x) (g₂ x) ≤ dist g₁ g₂ ⊔ dist (h₁.restrict (range ⇑f)ᶜ) (h₂.restrict (range ⇑f)ᶜ)

Tactic:
exact (dist_coe_le_dist x).trans (le_max_left _ _)

Result:
no goals

Proof state:
case refine_1.inr.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : { x // x ∈ (range ⇑f)ᶜ }
⊢ dist (h₁ ↑x) (h₂ ↑x) ≤ dist g₁ g₂ ⊔ dist (h₁.restrict (range ⇑f)ᶜ) (h₂.restrict (range ⇑f)ᶜ)

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 _ _

Result:
no goals

Proof state:
case refine_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist ((extend f g₁ h₁) (f x)) ((extend f g₂ h₂) (f x)) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)

Tactic:
exact dist_coe_le_dist _

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : ↑(range ⇑f)ᶜ
⊢ dist (h₁ ↑x) (h₂ ↑x) = dist ((extend f g₁ h₁) ↑x) ((extend f g₂ h₂) ↑x)

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

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
⊢ dist (extend f g₁ h₁) (extend f g₂ h₂) = dist g₁ g₂ ⊔ dist (h₁.restrict (range ⇑f)ᶜ) (h₂.restrict (range ⇑f)ᶜ)

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

Result:
case refine_1
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : δ
⊢ dist ((extend f g₁ h₁) x) ((extend f g₂ h₂) x) ≤ dist g₁ g₂ ⊔ dist (h₁.restrict (range ⇑f)ᶜ) (h₂.restrict (range ⇑f)ᶜ)

case refine_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
⊢ dist g₁ g₂ ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)

case refine_3
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
⊢ dist (h₁.restrict (range ⇑f)ᶜ) (h₂.restrict (range ⇑f)ᶜ) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)