case refine'_1
F : Type ?u.548018
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_1
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : δ
⊢ dist (↑(extend f g₁ h₁) x) (↑(extend f g₂ h₂) x) ≤
    max (dist g₁ g₂) (dist (restrict h₁ (range ↑fᶜ)) (restrict h₂ (range ↑fᶜ)))

case refine'_2
F : Type ?u.548018
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
δ : Type u_1
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
⊢ dist g₁ g₂ ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)

case refine'_3
F : Type ?u.548018
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
δ : Type u_1
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
⊢ dist (restrict h₁ (range ↑fᶜ)) (restrict h₂ (range ↑fᶜ)) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)
F : Type ?u.548018
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
δ : Type u_1
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
⊢ dist (extend f g₁ h₁) (extend f g₂ h₂) = max (dist g₁ g₂) (dist (restrict h₁ (range ↑fᶜ)) (restrict h₂ (range ↑fᶜ)))
refine' le_antisymm ((dist_le <| le_max_iff.2 <| Or.inl dist_nonneg).2 fun x => _) (max_le _ _)
case refine'_1.inl.intro
F : Type ?u.548018
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_1
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist (↑(extend f g₁ h₁) (↑f x)) (↑(extend f g₂ h₂) (↑f x)) ≤
    max (dist g₁ g₂) (dist (restrict h₁ (range ↑fᶜ)) (restrict h₂ (range ↑fᶜ)))

case refine'_1.inr
F : Type ?u.548018
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_1
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) ≤
    max (dist g₁ g₂) (dist (restrict h₁ (range ↑fᶜ)) (restrict h₂ (range ↑fᶜ)))
case refine'_1
F : Type ?u.548018
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_1
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : δ
⊢ dist (↑(extend f g₁ h₁) x) (↑(extend f g₂ h₂) x) ≤
    max (dist g₁ g₂) (dist (restrict h₁ (range ↑fᶜ)) (restrict h₂ (range ↑fᶜ)))
rcases _root_.em (∃ y, f y = x) with (⟨x, rfl⟩ | hx)
case refine'_1.inl.intro
F : Type ?u.548018
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_1
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist (↑g₁ x) (↑g₂ x) ≤ max (dist g₁ g₂) (dist (restrict h₁ (range ↑fᶜ)) (restrict h₂ (range ↑fᶜ)))
case refine'_1.inl.intro
F : Type ?u.548018
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_1
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist (↑(extend f g₁ h₁) (↑f x)) (↑(extend f g₂ h₂) (↑f x)) ≤
    max (dist g₁ g₂) (dist (restrict h₁ (range ↑fᶜ)) (restrict h₂ (range ↑fᶜ)))
simp only [extend_apply]
no goals
case refine'_1.inl.intro
F : Type ?u.548018
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_1
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist (↑g₁ x) (↑g₂ x) ≤ max (dist g₁ g₂) (dist (restrict h₁ (range ↑fᶜ)) (restrict h₂ (range ↑fᶜ)))
exact (dist_coe_le_dist x).trans (le_max_left _ _)
case refine'_1.inr
F : Type ?u.548018
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_1
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : δ
hx : ¬∃ y, ↑f y = x
⊢ dist (↑h₁ x) (↑h₂ x) ≤ max (dist g₁ g₂) (dist (restrict h₁ (range ↑fᶜ)) (restrict h₂ (range ↑fᶜ)))
case refine'_1.inr
F : Type ?u.548018
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_1
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) ≤
    max (dist g₁ g₂) (dist (restrict h₁ (range ↑fᶜ)) (restrict h₂ (range ↑fᶜ)))
simp only [extend_apply' hx]
case refine'_1.inr.intro
F : Type ?u.548018
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_1
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : { x // x ∈ range ↑fᶜ }
⊢ dist (↑h₁ ↑x) (↑h₂ ↑x) ≤ max (dist g₁ g₂) (dist (restrict h₁ (range ↑fᶜ)) (restrict h₂ (range ↑fᶜ)))
case refine'_1.inr
F : Type ?u.548018
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_1
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : δ
hx : ¬∃ y, ↑f y = x
⊢ dist (↑h₁ x) (↑h₂ x) ≤ max (dist g₁ g₂) (dist (restrict h₁ (range ↑fᶜ)) (restrict h₂ (range ↑fᶜ)))
lift x to (range fᶜ : Set δ) using hx
no goals
case refine'_1.inr.intro
F : Type ?u.548018
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_1
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : { x // x ∈ range ↑fᶜ }
⊢ dist (↑h₁ ↑x) (↑h₂ ↑x) ≤ max (dist g₁ g₂) (dist (restrict h₁ (range ↑fᶜ)) (restrict h₂ (range ↑fᶜ)))
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 _ _
case refine'_2
F : Type ?u.548018
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_1
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist (↑g₁ x) (↑g₂ x) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)
case refine'_2
F : Type ?u.548018
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
δ : Type u_1
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
⊢ dist g₁ g₂ ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)
refine' (dist_le dist_nonneg).2 fun x => _
case refine'_2
F : Type ?u.548018
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_1
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₂)
case refine'_2
F : Type ?u.548018
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_1
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist (↑g₁ x) (↑g₂ x) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)
rw [← extend_apply f g₁ h₁, ← extend_apply f g₂ h₂]
no goals
case refine'_2
F : Type ?u.548018
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_1
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₂)
exact dist_coe_le_dist _
case refine'_3
F : Type ?u.548018
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_1
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : ↑(range ↑fᶜ)
⊢ dist (↑(restrict h₁ (range ↑fᶜ)) x) (↑(restrict h₂ (range ↑fᶜ)) x) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)
case refine'_3
F : Type ?u.548018
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
δ : Type u_1
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
⊢ dist (restrict h₁ (range ↑fᶜ)) (restrict h₂ (range ↑fᶜ)) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)
refine' (dist_le dist_nonneg).2 fun x => _
no goals
case refine'_3
F : Type ?u.548018
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_1
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : ↑(range ↑fᶜ)
⊢ dist (↑(restrict h₁ (range ↑fᶜ)) x) (↑(restrict h₂ (range ↑fᶜ)) x) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)
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 _
no goals
F : Type ?u.548018
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C : ℝ
δ : Type u_1
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)
rw [extend_apply' x.coe_prop, extend_apply' x.coe_prop]