-- Mathlib/Analysis/Normed/Ring/WithAbs.lean
theorem extensionEmbedding_dist_eq_of_comp (h : ∀ x, ‖f x‖ = v x) (x y : v.Completion) :
    dist (extensionEmbedding_of_comp h x) (extensionEmbedding_of_comp h y) =
      dist x y

Proof state:
case refine_1
K : Type u_3
inst✝² : Field K
v : AbsoluteValue K ℝ
L : Type u_4
inst✝¹ : NormedField L
inst✝ : CompleteSpace L
f : WithAbs v →+* L
h : ∀ (x : WithAbs v), ‖f x‖ = v x
x y : v.Completion
⊢ Continuous fun x => dist ((extensionEmbedding_of_comp h) x.1) ((extensionEmbedding_of_comp h) x.2)

Tactic:
exact continuous_iff_continuous_dist.1 UniformSpace.Completion.continuous_extension

Result:
no goals

Proof state:
case refine_1
K : Type u_3
inst✝² : Field K
v : AbsoluteValue K ℝ
L : Type u_4
inst✝¹ : NormedField L
inst✝ : CompleteSpace L
f : WithAbs v →+* L
h : ∀ (x : WithAbs v), ‖f x‖ = v x
x y : v.Completion
⊢ IsClosed {x | dist ((extensionEmbedding_of_comp h) x.1) ((extensionEmbedding_of_comp h) x.2) = dist x.1 x.2}

Tactic:
refine isClosed_eq ?_ continuous_dist

Result:
case refine_1
K : Type u_3
inst✝² : Field K
v : AbsoluteValue K ℝ
L : Type u_4
inst✝¹ : NormedField L
inst✝ : CompleteSpace L
f : WithAbs v →+* L
h : ∀ (x : WithAbs v), ‖f x‖ = v x
x y : v.Completion
⊢ Continuous fun x => dist ((extensionEmbedding_of_comp h) x.1) ((extensionEmbedding_of_comp h) x.2)

Proof state:
K : Type u_3
inst✝² : Field K
v : AbsoluteValue K ℝ
L : Type u_4
inst✝¹ : NormedField L
inst✝ : CompleteSpace L
f : WithAbs v →+* L
h : ∀ (x : WithAbs v), ‖f x‖ = v x
x y : v.Completion
⊢ dist ((extensionEmbedding_of_comp h) x) ((extensionEmbedding_of_comp h) y) = dist x y

Tactic:
refine UniformSpace.Completion.induction_on₂ x y ?_ (fun x y => ?_)

Result:
case refine_1
K : Type u_3
inst✝² : Field K
v : AbsoluteValue K ℝ
L : Type u_4
inst✝¹ : NormedField L
inst✝ : CompleteSpace L
f : WithAbs v →+* L
h : ∀ (x : WithAbs v), ‖f x‖ = v x
x y : v.Completion
⊢ IsClosed {x | dist ((extensionEmbedding_of_comp h) x.1) ((extensionEmbedding_of_comp h) x.2) = dist x.1 x.2}

case refine_2
K : Type u_3
inst✝² : Field K
v : AbsoluteValue K ℝ
L : Type u_4
inst✝¹ : NormedField L
inst✝ : CompleteSpace L
f : WithAbs v →+* L
h : ∀ (x : WithAbs v), ‖f x‖ = v x
x✝ y✝ : v.Completion
x y : WithAbs v
⊢ dist ((extensionEmbedding_of_comp h) ↑x) ((extensionEmbedding_of_comp h) ↑y) = dist ↑x ↑y

Proof state:
case refine_2
K : Type u_3
inst✝² : Field K
v : AbsoluteValue K ℝ
L : Type u_4
inst✝¹ : NormedField L
inst✝ : CompleteSpace L
f : WithAbs v →+* L
h : ∀ (x : WithAbs v), ‖f x‖ = v x
x✝ y✝ : v.Completion
x y : WithAbs v
⊢ dist (f x) (f y) = dist ↑x ↑y

Tactic:
exact UniformSpace.Completion.dist_eq x y ▸ (WithAbs.isometry_of_comp h).dist_eq _ _

Result:
no goals

Proof state:
case refine_2
K : Type u_3
inst✝² : Field K
v : AbsoluteValue K ℝ
L : Type u_4
inst✝¹ : NormedField L
inst✝ : CompleteSpace L
f : WithAbs v →+* L
h : ∀ (x : WithAbs v), ‖f x‖ = v x
x✝ y✝ : v.Completion
x y : WithAbs v
⊢ dist ((extensionEmbedding_of_comp h) ↑x) ((extensionEmbedding_of_comp h) ↑y) = dist ↑x ↑y

Tactic:
simp only [extensionEmbedding_of_comp_coe]

Result:
case refine_2
K : Type u_3
inst✝² : Field K
v : AbsoluteValue K ℝ
L : Type u_4
inst✝¹ : NormedField L
inst✝ : CompleteSpace L
f : WithAbs v →+* L
h : ∀ (x : WithAbs v), ‖f x‖ = v x
x✝ y✝ : v.Completion
x y : WithAbs v
⊢ dist (f x) (f y) = dist ↑x ↑y