-- Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean
theorem ContDiff.euclidean_dist (hf : ContDiff ℝ n f) (hg : ContDiff ℝ n g) (h : ∀ x, f x ≠ g x) :
    ContDiff ℝ n fun x => Euclidean.dist (f x) (g x)

Proof state:
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : FiniteDimensional ℝ G
f g : F → G
n : ℕ∞
hf : ContDiff ℝ (↑n) f
hg : ContDiff ℝ (↑n) g
h : ∀ (x : F), f x ≠ g x
⊢ ContDiff ℝ ↑n fun x => Euclidean.dist (f x) (g x)

Tactic:
simp only [Euclidean.dist]

Result:
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : FiniteDimensional ℝ G
f g : F → G
n : ℕ∞
hf : ContDiff ℝ (↑n) f
hg : ContDiff ℝ (↑n) g
h : ∀ (x : F), f x ≠ g x
⊢ ContDiff ℝ ↑n fun x => Dist.dist (toEuclidean (f x)) (toEuclidean (g x))

Proof state:
case hf
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : FiniteDimensional ℝ G
f g : F → G
n : ℕ∞
hf : ContDiff ℝ (↑n) f
hg : ContDiff ℝ (↑n) g
h : ∀ (x : F), f x ≠ g x
⊢ ContDiff ℝ ↑n fun y => toEuclidean (f y)

case hg
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : FiniteDimensional ℝ G
f g : F → G
n : ℕ∞
hf : ContDiff ℝ (↑n) f
hg : ContDiff ℝ (↑n) g
h : ∀ (x : F), f x ≠ g x
⊢ ContDiff ℝ ↑n fun y => toEuclidean (g y)

case hne
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : FiniteDimensional ℝ G
f g : F → G
n : ℕ∞
hf : ContDiff ℝ (↑n) f
hg : ContDiff ℝ (↑n) g
h : ∀ (x : F), f x ≠ g x
⊢ ∀ (x : F), toEuclidean (f x) ≠ toEuclidean (g x)

Tactic:
exacts [(toEuclidean (E := G)).contDiff.comp hf,
  (toEuclidean (E := G)).contDiff.comp hg, fun x => toEuclidean.injective.ne (h x)]

Result:
no goals

Proof state:
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : FiniteDimensional ℝ G
f g : F → G
n : ℕ∞
hf : ContDiff ℝ (↑n) f
hg : ContDiff ℝ (↑n) g
h : ∀ (x : F), f x ≠ g x
⊢ ContDiff ℝ ↑n fun x => Dist.dist (toEuclidean (f x)) (toEuclidean (g x))

Tactic:
apply ContDiff.dist ℝ

Result:
case hf
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : FiniteDimensional ℝ G
f g : F → G
n : ℕ∞
hf : ContDiff ℝ (↑n) f
hg : ContDiff ℝ (↑n) g
h : ∀ (x : F), f x ≠ g x
⊢ ContDiff ℝ ↑n fun y => toEuclidean (f y)

case hg
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : FiniteDimensional ℝ G
f g : F → G
n : ℕ∞
hf : ContDiff ℝ (↑n) f
hg : ContDiff ℝ (↑n) g
h : ∀ (x : F), f x ≠ g x
⊢ ContDiff ℝ ↑n fun y => toEuclidean (g y)

case hne
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : FiniteDimensional ℝ G
f g : F → G
n : ℕ∞
hf : ContDiff ℝ (↑n) f
hg : ContDiff ℝ (↑n) g
h : ∀ (x : F), f x ≠ g x
⊢ ∀ (x : F), toEuclidean (f x) ≠ toEuclidean (g x)