refactor(analysis/normed_space/add_torsor): Kill `seminormed_add_tors…

…or` (#11795)

Delete `normed_add_torsor` in favor of the equivalent `seminormed_add_torsor` and rename `seminormed_add_torsor` to `normed_add_torsor`.

src/analysis/normed_space/add_torsor.lean

@@ -20,44 +20,23 @@ noncomputable theory
 open_locale nnreal topological_space
 open filter
 
-/-- A `semi_normed_add_torsor V P` is a torsor of an additive seminormed group
+/-- A `normed_add_torsor V P` is a torsor of an additive seminormed group
 action by a `semi_normed_group V` on points `P`. We bundle the pseudometric space
 structure and require the distance to be the same as results from the
 norm (which in fact implies the distance yields a pseudometric space, but
 bundling just the distance and using an instance for the pseudometric space
 results in type class problems). -/
-class semi_normed_add_torsor (V : out_param $ Type*) (P : Type*)
-  [out_param $ semi_normed_group V] [pseudo_metric_space P]
-  extends add_torsor V P :=
-(dist_eq_norm' : ∀ (x y : P), dist x y = ∥(x -ᵥ y : V)∥)
-
-/-- A `normed_add_torsor V P` is a torsor of an additive normed group
-action by a `normed_group V` on points `P`. We bundle the metric space
-structure and require the distance to be the same as results from the
-norm (which in fact implies the distance yields a metric space, but
-bundling just the distance and using an instance for the metric space
-results in type class problems). -/
 class normed_add_torsor (V : out_param $ Type*) (P : Type*)
-  [out_param $ normed_group V] [metric_space P]
+  [out_param $ semi_normed_group V] [pseudo_metric_space P]
   extends add_torsor V P :=
 (dist_eq_norm' : ∀ (x y : P), dist x y = ∥(x -ᵥ y : V)∥)
 
-/-- A `normed_add_torsor` is a `semi_normed_add_torsor`. -/
-@[priority 100]
-instance normed_add_torsor.to_semi_normed_add_torsor {V P : Type*} [normed_group V] [metric_space P]
-  [β : normed_add_torsor V P] : semi_normed_add_torsor V P := { ..β }
-
-variables {α V P : Type*} [semi_normed_group V] [pseudo_metric_space P] [semi_normed_add_torsor V P]
+variables {α V P : Type*} [semi_normed_group V] [pseudo_metric_space P] [normed_add_torsor V P]
 variables {W Q : Type*} [normed_group W] [metric_space Q] [normed_add_torsor W Q]
 
-/-- A `semi_normed_group` is a `semi_normed_add_torsor` over itself. -/
-@[priority 100]
-instance semi_normed_group.normed_add_torsor : semi_normed_add_torsor V V :=
-{ dist_eq_norm' := dist_eq_norm }
-
-/-- A `normed_group` is a `normed_add_torsor` over itself. -/
+/-- A `semi_normed_group` is a `normed_add_torsor` over itself. -/
 @[priority 100]
-instance normed_group.normed_add_torsor : normed_add_torsor W W :=
+instance semi_normed_group.to_normed_add_torsor : normed_add_torsor V V :=
 { dist_eq_norm' := dist_eq_norm }
 
 include V
@@ -69,9 +48,7 @@ variables (V W)
 /-- The distance equals the norm of subtracting two points. In this
 lemma, it is necessary to have `V` as an explicit argument; otherwise
 `rw dist_eq_norm_vsub` sometimes doesn't work. -/
-lemma dist_eq_norm_vsub (x y : P) :
-  dist x y = ∥(x -ᵥ y)∥ :=
-semi_normed_add_torsor.dist_eq_norm' x y
+lemma dist_eq_norm_vsub (x y : P) : dist x y = ∥x -ᵥ y∥ := normed_add_torsor.dist_eq_norm' x y
 
 end
 
@@ -224,8 +201,7 @@ lemma uniform_continuous_vadd : uniform_continuous (λ x : V × P, x.1 +ᵥ x.2)
 lemma uniform_continuous_vsub : uniform_continuous (λ x : P × P, x.1 -ᵥ x.2) :=
 (lipschitz_with.prod_fst.vsub lipschitz_with.prod_snd).uniform_continuous
 
-@[priority 100] instance semi_normed_add_torsor.has_continuous_vadd :
-  has_continuous_vadd V P :=
+@[priority 100] instance normed_add_torsor.to_has_continuous_vadd : has_continuous_vadd V P :=
 { continuous_vadd := uniform_continuous_vadd.continuous }
 
 lemma continuous_vsub : continuous (λ x : P × P, x.1 -ᵥ x.2) :=

src/analysis/normed_space/affine_isometry.lean

@@ -17,7 +17,7 @@ We also prove basic lemmas and provide convenience constructors.  The choice of
 constructors is closely modelled on those for the `linear_isometry` and `affine_map` theories.
 
 Since many elementary properties don't require `∥x∥ = 0 → x = 0` we initially set up the theory for
-`semi_normed_add_torsor` and specialize to `normed_add_torsor` only when needed.
+`semi_normed_group` and specialize to `normed_group` only when needed.
 
 ## Notation
 
@@ -32,14 +32,14 @@ open function set
 
 variables (𝕜 : Type*) {V V₁ V₂ V₃ V₄ : Type*} {P₁ : Type*} (P P₂ : Type*) {P₃ P₄ : Type*}
     [normed_field 𝕜]
-  [semi_normed_group V] [normed_group V₁] [semi_normed_group V₂] [semi_normed_group V₃]
+  [semi_normed_group V] [semi_normed_group V₁] [semi_normed_group V₂] [semi_normed_group V₃]
     [semi_normed_group V₄]
   [normed_space 𝕜 V] [normed_space 𝕜 V₁] [normed_space 𝕜 V₂] [normed_space 𝕜 V₃]
     [normed_space 𝕜 V₄]
   [pseudo_metric_space P] [metric_space P₁] [pseudo_metric_space P₂] [pseudo_metric_space P₃]
     [pseudo_metric_space P₄]
-  [semi_normed_add_torsor V P] [normed_add_torsor V₁ P₁] [semi_normed_add_torsor V₂ P₂]
-    [semi_normed_add_torsor V₃ P₃] [semi_normed_add_torsor V₄ P₄]
+  [normed_add_torsor V P] [normed_add_torsor V₁ P₁] [normed_add_torsor V₂ P₂]
+    [normed_add_torsor V₃ P₃] [normed_add_torsor V₄ P₄]
 
 include V V₂
 

src/analysis/normed_space/finite_dimension.lean

@@ -87,7 +87,7 @@ variables {𝕜 : Type*} {V₁ V₂  : Type*} {P₁ P₂ : Type*}
   [normed_group V₁] [semi_normed_group V₂]
   [normed_space 𝕜 V₁] [normed_space 𝕜 V₂]
   [metric_space P₁] [pseudo_metric_space P₂]
-  [normed_add_torsor V₁ P₁] [semi_normed_add_torsor V₂ P₂]
+  [normed_add_torsor V₁ P₁] [normed_add_torsor V₂ P₂]
 
 variables [finite_dimensional 𝕜 V₁] [finite_dimensional 𝕜 V₂]
 

src/geometry/euclidean/basic.lean

@@ -980,8 +980,8 @@ lemma dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd {s : affine_subspace ℝ
     dist p1 p2 * dist p1 p2 + (r1 - r2) * (r1 - r2) * (∥v∥ * ∥v∥) :=
 calc dist (r1 • v +ᵥ p1) (r2 • v +ᵥ p2) * dist (r1 • v +ᵥ p1) (r2 • v +ᵥ p2)
     = ∥(p1 -ᵥ p2) + (r1 - r2) • v∥ * ∥(p1 -ᵥ p2) + (r1 - r2) • v∥
-  : by { rw [dist_eq_norm_vsub V (r1 • v +ᵥ p1), vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, sub_smul],
-         abel }
+  : by rw [dist_eq_norm_vsub V (r1 • v +ᵥ p1), vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, sub_smul,
+      add_comm, add_sub_assoc]
 ... = ∥p1 -ᵥ p2∥ * ∥p1 -ᵥ p2∥ + ∥(r1 - r2) • v∥ * ∥(r1 - r2) • v∥
   : norm_add_sq_eq_norm_sq_add_norm_sq_real
       (submodule.inner_right_of_mem_orthogonal (vsub_mem_direction hp1 hp2)