From 1e68b864793dd7059188998c47ffe466b9189eb8 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Tue, 30 May 2023 22:38:20 -0500
Subject: [PATCH 1/7] feat: port Analysis.Quaternion


From 8e3a729a9d02bc6b01537f578ed0df81402d28bc Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Tue, 30 May 2023 22:38:20 -0500
Subject: [PATCH 2/7] Initial file copy from mathport

---
 Mathlib/Analysis/Quaternion.lean | 267 +++++++++++++++++++++++++++++++
 1 file changed, 267 insertions(+)
 create mode 100644 Mathlib/Analysis/Quaternion.lean

diff --git a/Mathlib/Analysis/Quaternion.lean b/Mathlib/Analysis/Quaternion.lean
new file mode 100644
index 0000000000000..a5401d508dffa
--- /dev/null
+++ b/Mathlib/Analysis/Quaternion.lean
@@ -0,0 +1,267 @@
+/-
+Copyright (c) 2020 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov, Eric Wieser
+
+! This file was ported from Lean 3 source module analysis.quaternion
+! leanprover-community/mathlib commit 07992a1d1f7a4176c6d3f160209608be4e198566
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathbin.Algebra.Quaternion
+import Mathbin.Analysis.InnerProductSpace.Basic
+import Mathbin.Analysis.InnerProductSpace.PiL2
+import Mathbin.Topology.Algebra.Algebra
+
+/-!
+# Quaternions as a normed algebra
+
+In this file we define the following structures on the space `ℍ := ℍ[ℝ]` of quaternions:
+
+* inner product space;
+* normed ring;
+* normed space over `ℝ`.
+
+We show that the norm on `ℍ[ℝ]` agrees with the euclidean norm of its components.
+
+## Notation
+
+The following notation is available with `open_locale quaternion`:
+
+* `ℍ` : quaternions
+
+## Tags
+
+quaternion, normed ring, normed space, normed algebra
+-/
+
+
+-- mathport name: quaternion.real
+scoped[Quaternion] notation "ℍ" => Quaternion ℝ
+
+open scoped RealInnerProductSpace
+
+namespace Quaternion
+
+instance : Inner ℝ ℍ :=
+  ⟨fun a b => (a * star b).re⟩
+
+theorem inner_self (a : ℍ) : ⟪a, a⟫ = normSq a :=
+  rfl
+#align quaternion.inner_self Quaternion.inner_self
+
+theorem inner_def (a b : ℍ) : ⟪a, b⟫ = (a * star b).re :=
+  rfl
+#align quaternion.inner_def Quaternion.inner_def
+
+noncomputable instance : NormedAddCommGroup ℍ :=
+  @InnerProductSpace.Core.toNormedAddCommGroup ℝ ℍ _ _ _
+    { toHasInner := inferInstance
+      conj_symm := fun x y => by simp [inner_def, mul_comm]
+      nonneg_re := fun x => normSq_nonneg
+      definite := fun x => normSq_eq_zero.1
+      add_left := fun x y z => by simp only [inner_def, add_mul, add_re]
+      smul_left := fun x y r => by simp [inner_def] }
+
+noncomputable instance : InnerProductSpace ℝ ℍ :=
+  InnerProductSpace.ofCore _
+
+theorem normSq_eq_normSq (a : ℍ) : normSq a = ‖a‖ * ‖a‖ := by
+  rw [← inner_self, real_inner_self_eq_norm_mul_norm]
+#align quaternion.norm_sq_eq_norm_sq Quaternion.normSq_eq_normSq
+
+instance : NormOneClass ℍ :=
+  ⟨by rw [norm_eq_sqrt_real_inner, inner_self, norm_sq.map_one, Real.sqrt_one]⟩
+
+@[simp, norm_cast]
+theorem norm_coe (a : ℝ) : ‖(a : ℍ)‖ = ‖a‖ := by
+  rw [norm_eq_sqrt_real_inner, inner_self, norm_sq_coe, Real.sqrt_sq_eq_abs, Real.norm_eq_abs]
+#align quaternion.norm_coe Quaternion.norm_coe
+
+@[simp, norm_cast]
+theorem nnnorm_coe (a : ℝ) : ‖(a : ℍ)‖₊ = ‖a‖₊ :=
+  Subtype.ext <| norm_coe a
+#align quaternion.nnnorm_coe Quaternion.nnnorm_coe
+
+@[simp]
+theorem norm_star (a : ℍ) : ‖star a‖ = ‖a‖ := by
+  simp_rw [norm_eq_sqrt_real_inner, inner_self, norm_sq_star]
+#align quaternion.norm_star Quaternion.norm_star
+
+@[simp]
+theorem nnnorm_star (a : ℍ) : ‖star a‖₊ = ‖a‖₊ :=
+  Subtype.ext <| norm_star a
+#align quaternion.nnnorm_star Quaternion.nnnorm_star
+
+noncomputable instance : NormedDivisionRing ℍ
+    where
+  dist_eq _ _ := rfl
+  norm_mul' a b :=
+    by
+    simp only [norm_eq_sqrt_real_inner, inner_self, norm_sq.map_mul]
+    exact Real.sqrt_mul norm_sq_nonneg _
+
+instance : NormedAlgebra ℝ ℍ where
+  norm_smul_le := norm_smul_le
+  toAlgebra := (Quaternion.algebra : Algebra ℝ ℍ)
+
+instance : CstarRing ℍ
+    where norm_star_mul_self x := (norm_mul _ _).trans <| congr_arg (· * ‖x‖) (norm_star x)
+
+instance : Coe ℂ ℍ :=
+  ⟨fun z => ⟨z.re, z.im, 0, 0⟩⟩
+
+@[simp, norm_cast]
+theorem coe_complex_re (z : ℂ) : (z : ℍ).re = z.re :=
+  rfl
+#align quaternion.coe_complex_re Quaternion.coe_complex_re
+
+@[simp, norm_cast]
+theorem coe_complex_imI (z : ℂ) : (z : ℍ).imI = z.im :=
+  rfl
+#align quaternion.coe_complex_im_i Quaternion.coe_complex_imI
+
+@[simp, norm_cast]
+theorem coe_complex_imJ (z : ℂ) : (z : ℍ).imJ = 0 :=
+  rfl
+#align quaternion.coe_complex_im_j Quaternion.coe_complex_imJ
+
+@[simp, norm_cast]
+theorem coe_complex_imK (z : ℂ) : (z : ℍ).imK = 0 :=
+  rfl
+#align quaternion.coe_complex_im_k Quaternion.coe_complex_imK
+
+@[simp, norm_cast]
+theorem coe_complex_add (z w : ℂ) : ↑(z + w) = (z + w : ℍ) := by ext <;> simp
+#align quaternion.coe_complex_add Quaternion.coe_complex_add
+
+@[simp, norm_cast]
+theorem coe_complex_mul (z w : ℂ) : ↑(z * w) = (z * w : ℍ) := by ext <;> simp
+#align quaternion.coe_complex_mul Quaternion.coe_complex_mul
+
+@[simp, norm_cast]
+theorem coe_complex_zero : ((0 : ℂ) : ℍ) = 0 :=
+  rfl
+#align quaternion.coe_complex_zero Quaternion.coe_complex_zero
+
+@[simp, norm_cast]
+theorem coe_complex_one : ((1 : ℂ) : ℍ) = 1 :=
+  rfl
+#align quaternion.coe_complex_one Quaternion.coe_complex_one
+
+@[simp, norm_cast]
+theorem coe_real_complex_mul (r : ℝ) (z : ℂ) : (r • z : ℍ) = ↑r * ↑z := by ext <;> simp
+#align quaternion.coe_real_complex_mul Quaternion.coe_real_complex_mul
+
+@[simp, norm_cast]
+theorem coe_complex_coe (r : ℝ) : ((r : ℂ) : ℍ) = r :=
+  rfl
+#align quaternion.coe_complex_coe Quaternion.coe_complex_coe
+
+/-- Coercion `ℂ →ₐ[ℝ] ℍ` as an algebra homomorphism. -/
+def ofComplex : ℂ →ₐ[ℝ] ℍ where
+  toFun := coe
+  map_one' := rfl
+  map_zero' := rfl
+  map_add' := coe_complex_add
+  map_mul' := coe_complex_mul
+  commutes' x := rfl
+#align quaternion.of_complex Quaternion.ofComplex
+
+@[simp]
+theorem coe_ofComplex : ⇑ofComplex = coe :=
+  rfl
+#align quaternion.coe_of_complex Quaternion.coe_ofComplex
+
+/-- The norm of the components as a euclidean vector equals the norm of the quaternion. -/
+theorem norm_piLp_equiv_symm_equivTuple (x : ℍ) :
+    ‖(PiLp.equiv 2 fun _ : Fin 4 => _).symm (equivTuple ℝ x)‖ = ‖x‖ :=
+  by
+  rw [norm_eq_sqrt_real_inner, norm_eq_sqrt_real_inner, inner_self, norm_sq_def', PiLp.inner_apply,
+    Fin.sum_univ_four]
+  simp_rw [IsROrC.inner_apply, starRingEnd_apply, star_trivial, ← sq]
+  rfl
+#align quaternion.norm_pi_Lp_equiv_symm_equiv_tuple Quaternion.norm_piLp_equiv_symm_equivTuple
+
+/-- `quaternion_algebra.linear_equiv_tuple` as a `linear_isometry_equiv`. -/
+@[simps apply symm_apply]
+noncomputable def linearIsometryEquivTuple : ℍ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 4) :=
+  {
+    (QuaternionAlgebra.linearEquivTuple (-1 : ℝ) (-1 : ℝ)).trans
+      (PiLp.linearEquiv 2 ℝ fun _ : Fin 4 =>
+          ℝ).symm with
+    toFun := fun a => (PiLp.equiv _ fun _ : Fin 4 => _).symm ![a.1, a.2, a.3, a.4]
+    invFun := fun a => ⟨a 0, a 1, a 2, a 3⟩
+    norm_map' := norm_piLp_equiv_symm_equivTuple }
+#align quaternion.linear_isometry_equiv_tuple Quaternion.linearIsometryEquivTuple
+
+@[continuity]
+theorem continuous_coe : Continuous (coe : ℝ → ℍ) :=
+  continuous_algebraMap ℝ ℍ
+#align quaternion.continuous_coe Quaternion.continuous_coe
+
+@[continuity]
+theorem continuous_normSq : Continuous (normSq : ℍ → ℝ) := by
+  simpa [← norm_sq_eq_norm_sq] using
+    (continuous_norm.mul continuous_norm : Continuous fun q : ℍ => ‖q‖ * ‖q‖)
+#align quaternion.continuous_norm_sq Quaternion.continuous_normSq
+
+@[continuity]
+theorem continuous_re : Continuous fun q : ℍ => q.re :=
+  (continuous_apply 0).comp linearIsometryEquivTuple.Continuous
+#align quaternion.continuous_re Quaternion.continuous_re
+
+@[continuity]
+theorem continuous_imI : Continuous fun q : ℍ => q.imI :=
+  (continuous_apply 1).comp linearIsometryEquivTuple.Continuous
+#align quaternion.continuous_im_i Quaternion.continuous_imI
+
+@[continuity]
+theorem continuous_imJ : Continuous fun q : ℍ => q.imJ :=
+  (continuous_apply 2).comp linearIsometryEquivTuple.Continuous
+#align quaternion.continuous_im_j Quaternion.continuous_imJ
+
+@[continuity]
+theorem continuous_imK : Continuous fun q : ℍ => q.imK :=
+  (continuous_apply 3).comp linearIsometryEquivTuple.Continuous
+#align quaternion.continuous_im_k Quaternion.continuous_imK
+
+@[continuity]
+theorem continuous_im : Continuous fun q : ℍ => q.im := by
+  simpa only [← sub_self_re] using continuous_id.sub (continuous_coe.comp continuous_re)
+#align quaternion.continuous_im Quaternion.continuous_im
+
+instance : CompleteSpace ℍ :=
+  haveI : UniformEmbedding linear_isometry_equiv_tuple.to_linear_equiv.to_equiv.symm :=
+    linear_isometry_equiv_tuple.to_continuous_linear_equiv.symm.uniform_embedding
+  (completeSpace_congr this).1 (by infer_instance)
+
+section infinite_sum
+
+variable {α : Type _}
+
+@[simp, norm_cast]
+theorem hasSum_coe {f : α → ℝ} {r : ℝ} : HasSum (fun a => (f a : ℍ)) (↑r : ℍ) ↔ HasSum f r :=
+  ⟨fun h => by simpa only using h.map (show ℍ →ₗ[ℝ] ℝ from QuaternionAlgebra.reₗ _ _) continuous_re,
+    fun h => by simpa only using h.map (algebraMap ℝ ℍ) (continuous_algebraMap _ _)⟩
+#align quaternion.has_sum_coe Quaternion.hasSum_coe
+
+@[simp, norm_cast]
+theorem summable_coe {f : α → ℝ} : (Summable fun a => (f a : ℍ)) ↔ Summable f := by
+  simpa only using
+    Summable.map_iff_of_leftInverse (algebraMap ℝ ℍ) (show ℍ →ₗ[ℝ] ℝ from QuaternionAlgebra.reₗ _ _)
+      (continuous_algebraMap _ _) continuous_re coe_re
+#align quaternion.summable_coe Quaternion.summable_coe
+
+@[norm_cast]
+theorem tsum_coe (f : α → ℝ) : (∑' a, (f a : ℍ)) = ↑(∑' a, f a) :=
+  by
+  by_cases hf : Summable f
+  · exact (has_sum_coe.mpr hf.has_sum).tsum_eq
+  · simp [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable (summable_coe.not.mpr hf)]
+#align quaternion.tsum_coe Quaternion.tsum_coe
+
+end infinite_sum
+
+end Quaternion
+

From 897d03948011bf6aa3a40822b34e3823ad92a8dc Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Tue, 30 May 2023 22:38:20 -0500
Subject: [PATCH 3/7] automated fixes

Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
---
 Mathlib.lean                     |  1 +
 Mathlib/Analysis/Quaternion.lean | 20 ++++++++------------
 2 files changed, 9 insertions(+), 12 deletions(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index 85eb824c31a03..ef62a4f9ea1a8 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -565,6 +565,7 @@ import Mathlib.Analysis.NormedSpace.Star.Multiplier
 import Mathlib.Analysis.NormedSpace.Units
 import Mathlib.Analysis.NormedSpace.WeakDual
 import Mathlib.Analysis.PSeries
+import Mathlib.Analysis.Quaternion
 import Mathlib.Analysis.Seminorm
 import Mathlib.Analysis.SpecialFunctions.Complex.Arg
 import Mathlib.Analysis.SpecialFunctions.Complex.Circle
diff --git a/Mathlib/Analysis/Quaternion.lean b/Mathlib/Analysis/Quaternion.lean
index a5401d508dffa..0eac7e56846c4 100644
--- a/Mathlib/Analysis/Quaternion.lean
+++ b/Mathlib/Analysis/Quaternion.lean
@@ -8,10 +8,10 @@ Authors: Yury Kudryashov, Eric Wieser
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
-import Mathbin.Algebra.Quaternion
-import Mathbin.Analysis.InnerProductSpace.Basic
-import Mathbin.Analysis.InnerProductSpace.PiL2
-import Mathbin.Topology.Algebra.Algebra
+import Mathlib.Algebra.Quaternion
+import Mathlib.Analysis.InnerProductSpace.Basic
+import Mathlib.Analysis.InnerProductSpace.PiL2
+import Mathlib.Topology.Algebra.Algebra
 
 /-!
 # Quaternions as a normed algebra
@@ -93,11 +93,9 @@ theorem nnnorm_star (a : ℍ) : ‖star a‖₊ = ‖a‖₊ :=
   Subtype.ext <| norm_star a
 #align quaternion.nnnorm_star Quaternion.nnnorm_star
 
-noncomputable instance : NormedDivisionRing ℍ
-    where
+noncomputable instance : NormedDivisionRing ℍ where
   dist_eq _ _ := rfl
-  norm_mul' a b :=
-    by
+  norm_mul' a b := by
     simp only [norm_eq_sqrt_real_inner, inner_self, norm_sq.map_mul]
     exact Real.sqrt_mul norm_sq_nonneg _
 
@@ -175,8 +173,7 @@ theorem coe_ofComplex : ⇑ofComplex = coe :=
 
 /-- The norm of the components as a euclidean vector equals the norm of the quaternion. -/
 theorem norm_piLp_equiv_symm_equivTuple (x : ℍ) :
-    ‖(PiLp.equiv 2 fun _ : Fin 4 => _).symm (equivTuple ℝ x)‖ = ‖x‖ :=
-  by
+    ‖(PiLp.equiv 2 fun _ : Fin 4 => _).symm (equivTuple ℝ x)‖ = ‖x‖ := by
   rw [norm_eq_sqrt_real_inner, norm_eq_sqrt_real_inner, inner_self, norm_sq_def', PiLp.inner_apply,
     Fin.sum_univ_four]
   simp_rw [IsROrC.inner_apply, starRingEnd_apply, star_trivial, ← sq]
@@ -254,8 +251,7 @@ theorem summable_coe {f : α → ℝ} : (Summable fun a => (f a : ℍ)) ↔ Summ
 #align quaternion.summable_coe Quaternion.summable_coe
 
 @[norm_cast]
-theorem tsum_coe (f : α → ℝ) : (∑' a, (f a : ℍ)) = ↑(∑' a, f a) :=
-  by
+theorem tsum_coe (f : α → ℝ) : (∑' a, (f a : ℍ)) = ↑(∑' a, f a) := by
   by_cases hf : Summable f
   · exact (has_sum_coe.mpr hf.has_sum).tsum_eq
   · simp [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable (summable_coe.not.mpr hf)]

From 149df4e04197169d2c1a0b7300958ce0c9d5bb42 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Tue, 30 May 2023 22:51:40 -0500
Subject: [PATCH 4/7] Fix compile

---
 Mathlib/Algebra/Quaternion.lean  |   2 +-
 Mathlib/Analysis/Quaternion.lean | 104 +++++++++++++++----------------
 2 files changed, 53 insertions(+), 53 deletions(-)

diff --git a/Mathlib/Algebra/Quaternion.lean b/Mathlib/Algebra/Quaternion.lean
index 73c0f219dcc86..6296a8ab0fcec 100644
--- a/Mathlib/Algebra/Quaternion.lean
+++ b/Mathlib/Algebra/Quaternion.lean
@@ -780,7 +780,7 @@ instance [SMul S T] [SMul S R] [SMul T R] [IsScalarTower S T R] : IsScalarTower
 instance [SMul S R] [SMul T R] [SMulCommClass S T R] : SMulCommClass S T ℍ[R] :=
   inferInstanceAs <| SMulCommClass S T ℍ[R,-1,-1]
 
-instance [CommSemiring S] [Algebra S R] : Algebra S ℍ[R] :=
+protected instance algebra [CommSemiring S] [Algebra S R] : Algebra S ℍ[R] :=
   inferInstanceAs <| Algebra S ℍ[R,-1,-1]
 
 -- porting note: added shortcut
diff --git a/Mathlib/Analysis/Quaternion.lean b/Mathlib/Analysis/Quaternion.lean
index 0eac7e56846c4..bc99a2797fe6d 100644
--- a/Mathlib/Analysis/Quaternion.lean
+++ b/Mathlib/Analysis/Quaternion.lean
@@ -56,7 +56,7 @@ theorem inner_def (a b : ℍ) : ⟪a, b⟫ = (a * star b).re :=
 
 noncomputable instance : NormedAddCommGroup ℍ :=
   @InnerProductSpace.Core.toNormedAddCommGroup ℝ ℍ _ _ _
-    { toHasInner := inferInstance
+    { toInner := inferInstance
       conj_symm := fun x y => by simp [inner_def, mul_comm]
       nonneg_re := fun x => normSq_nonneg
       definite := fun x => normSq_eq_zero.1
@@ -66,16 +66,16 @@ noncomputable instance : NormedAddCommGroup ℍ :=
 noncomputable instance : InnerProductSpace ℝ ℍ :=
   InnerProductSpace.ofCore _
 
-theorem normSq_eq_normSq (a : ℍ) : normSq a = ‖a‖ * ‖a‖ := by
+theorem normSq_eq_norm_mul_self (a : ℍ) : normSq a = ‖a‖ * ‖a‖ := by
   rw [← inner_self, real_inner_self_eq_norm_mul_norm]
-#align quaternion.norm_sq_eq_norm_sq Quaternion.normSq_eq_normSq
+#align quaternion.norm_sq_eq_norm_sq Quaternion.normSq_eq_norm_mul_self
 
 instance : NormOneClass ℍ :=
-  ⟨by rw [norm_eq_sqrt_real_inner, inner_self, norm_sq.map_one, Real.sqrt_one]⟩
+  ⟨by rw [norm_eq_sqrt_real_inner, inner_self, normSq.map_one, Real.sqrt_one]⟩
 
 @[simp, norm_cast]
 theorem norm_coe (a : ℝ) : ‖(a : ℍ)‖ = ‖a‖ := by
-  rw [norm_eq_sqrt_real_inner, inner_self, norm_sq_coe, Real.sqrt_sq_eq_abs, Real.norm_eq_abs]
+  rw [norm_eq_sqrt_real_inner, inner_self, normSq_coe, Real.sqrt_sq_eq_abs, Real.norm_eq_abs]
 #align quaternion.norm_coe Quaternion.norm_coe
 
 @[simp, norm_cast]
@@ -85,7 +85,7 @@ theorem nnnorm_coe (a : ℝ) : ‖(a : ℍ)‖₊ = ‖a‖₊ :=
 
 @[simp]
 theorem norm_star (a : ℍ) : ‖star a‖ = ‖a‖ := by
-  simp_rw [norm_eq_sqrt_real_inner, inner_self, norm_sq_star]
+  simp_rw [norm_eq_sqrt_real_inner, inner_self, normSq_star]
 #align quaternion.norm_star Quaternion.norm_star
 
 @[simp]
@@ -96,97 +96,98 @@ theorem nnnorm_star (a : ℍ) : ‖star a‖₊ = ‖a‖₊ :=
 noncomputable instance : NormedDivisionRing ℍ where
   dist_eq _ _ := rfl
   norm_mul' a b := by
-    simp only [norm_eq_sqrt_real_inner, inner_self, norm_sq.map_mul]
-    exact Real.sqrt_mul norm_sq_nonneg _
+    simp only [norm_eq_sqrt_real_inner, inner_self, normSq.map_mul]
+    exact Real.sqrt_mul normSq_nonneg _
 
-instance : NormedAlgebra ℝ ℍ where
+-- porting note: added `noncomputable`
+noncomputable instance : NormedAlgebra ℝ ℍ where
   norm_smul_le := norm_smul_le
-  toAlgebra := (Quaternion.algebra : Algebra ℝ ℍ)
+  toAlgebra := Quaternion.algebra
 
-instance : CstarRing ℍ
-    where norm_star_mul_self x := (norm_mul _ _).trans <| congr_arg (· * ‖x‖) (norm_star x)
+instance : CstarRing ℍ where
+  norm_star_mul_self {x} := (norm_mul _ _).trans <| congr_arg (· * ‖x‖) (norm_star x)
 
-instance : Coe ℂ ℍ :=
-  ⟨fun z => ⟨z.re, z.im, 0, 0⟩⟩
+/-- Coerction from `ℂ` to `ℍ`. -/
+@[coe] def coeComplex (z : ℂ) : ℍ := ⟨z.re, z.im, 0, 0⟩
+
+instance : Coe ℂ ℍ := ⟨coeComplex⟩
 
 @[simp, norm_cast]
-theorem coe_complex_re (z : ℂ) : (z : ℍ).re = z.re :=
+theorem coeComplex_re (z : ℂ) : (z : ℍ).re = z.re :=
   rfl
-#align quaternion.coe_complex_re Quaternion.coe_complex_re
+#align quaternion.coe_complex_re Quaternion.coeComplex_re
 
 @[simp, norm_cast]
-theorem coe_complex_imI (z : ℂ) : (z : ℍ).imI = z.im :=
+theorem coeComplex_imI (z : ℂ) : (z : ℍ).imI = z.im :=
   rfl
-#align quaternion.coe_complex_im_i Quaternion.coe_complex_imI
+#align quaternion.coe_complex_im_i Quaternion.coeComplex_imI
 
 @[simp, norm_cast]
-theorem coe_complex_imJ (z : ℂ) : (z : ℍ).imJ = 0 :=
+theorem coeComplex_imJ (z : ℂ) : (z : ℍ).imJ = 0 :=
   rfl
-#align quaternion.coe_complex_im_j Quaternion.coe_complex_imJ
+#align quaternion.coe_complex_im_j Quaternion.coeComplex_imJ
 
 @[simp, norm_cast]
-theorem coe_complex_imK (z : ℂ) : (z : ℍ).imK = 0 :=
+theorem coeComplex_imK (z : ℂ) : (z : ℍ).imK = 0 :=
   rfl
-#align quaternion.coe_complex_im_k Quaternion.coe_complex_imK
+#align quaternion.coe_complex_im_k Quaternion.coeComplex_imK
 
 @[simp, norm_cast]
-theorem coe_complex_add (z w : ℂ) : ↑(z + w) = (z + w : ℍ) := by ext <;> simp
-#align quaternion.coe_complex_add Quaternion.coe_complex_add
+theorem coeComplex_add (z w : ℂ) : ↑(z + w) = (z + w : ℍ) := by ext <;> simp
+#align quaternion.coe_complex_add Quaternion.coeComplex_add
 
 @[simp, norm_cast]
-theorem coe_complex_mul (z w : ℂ) : ↑(z * w) = (z * w : ℍ) := by ext <;> simp
-#align quaternion.coe_complex_mul Quaternion.coe_complex_mul
+theorem coeComplex_mul (z w : ℂ) : ↑(z * w) = (z * w : ℍ) := by ext <;> simp
+#align quaternion.coe_complex_mul Quaternion.coeComplex_mul
 
 @[simp, norm_cast]
-theorem coe_complex_zero : ((0 : ℂ) : ℍ) = 0 :=
+theorem coeComplex_zero : ((0 : ℂ) : ℍ) = 0 :=
   rfl
-#align quaternion.coe_complex_zero Quaternion.coe_complex_zero
+#align quaternion.coe_complex_zero Quaternion.coeComplex_zero
 
 @[simp, norm_cast]
-theorem coe_complex_one : ((1 : ℂ) : ℍ) = 1 :=
+theorem coeComplex_one : ((1 : ℂ) : ℍ) = 1 :=
   rfl
-#align quaternion.coe_complex_one Quaternion.coe_complex_one
+#align quaternion.coe_complex_one Quaternion.coeComplex_one
 
 @[simp, norm_cast]
 theorem coe_real_complex_mul (r : ℝ) (z : ℂ) : (r • z : ℍ) = ↑r * ↑z := by ext <;> simp
 #align quaternion.coe_real_complex_mul Quaternion.coe_real_complex_mul
 
 @[simp, norm_cast]
-theorem coe_complex_coe (r : ℝ) : ((r : ℂ) : ℍ) = r :=
+theorem coeComplex_coe (r : ℝ) : ((r : ℂ) : ℍ) = r :=
   rfl
-#align quaternion.coe_complex_coe Quaternion.coe_complex_coe
+#align quaternion.coe_complex_coe Quaternion.coeComplex_coe
 
 /-- Coercion `ℂ →ₐ[ℝ] ℍ` as an algebra homomorphism. -/
 def ofComplex : ℂ →ₐ[ℝ] ℍ where
-  toFun := coe
+  toFun := (↑)
   map_one' := rfl
   map_zero' := rfl
-  map_add' := coe_complex_add
-  map_mul' := coe_complex_mul
-  commutes' x := rfl
+  map_add' := coeComplex_add
+  map_mul' := coeComplex_mul
+  commutes' _ := rfl
 #align quaternion.of_complex Quaternion.ofComplex
 
 @[simp]
-theorem coe_ofComplex : ⇑ofComplex = coe :=
-  rfl
+theorem coe_ofComplex : ⇑ofComplex = coeComplex := rfl
 #align quaternion.coe_of_complex Quaternion.coe_ofComplex
 
 /-- The norm of the components as a euclidean vector equals the norm of the quaternion. -/
 theorem norm_piLp_equiv_symm_equivTuple (x : ℍ) :
     ‖(PiLp.equiv 2 fun _ : Fin 4 => _).symm (equivTuple ℝ x)‖ = ‖x‖ := by
-  rw [norm_eq_sqrt_real_inner, norm_eq_sqrt_real_inner, inner_self, norm_sq_def', PiLp.inner_apply,
+  rw [norm_eq_sqrt_real_inner, norm_eq_sqrt_real_inner, inner_self, normSq_def', PiLp.inner_apply,
     Fin.sum_univ_four]
   simp_rw [IsROrC.inner_apply, starRingEnd_apply, star_trivial, ← sq]
   rfl
+set_option linter.uppercaseLean3 false in
 #align quaternion.norm_pi_Lp_equiv_symm_equiv_tuple Quaternion.norm_piLp_equiv_symm_equivTuple
 
 /-- `quaternion_algebra.linear_equiv_tuple` as a `linear_isometry_equiv`. -/
 @[simps apply symm_apply]
 noncomputable def linearIsometryEquivTuple : ℍ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 4) :=
-  {
-    (QuaternionAlgebra.linearEquivTuple (-1 : ℝ) (-1 : ℝ)).trans
-      (PiLp.linearEquiv 2 ℝ fun _ : Fin 4 =>
-          ℝ).symm with
+  { (QuaternionAlgebra.linearEquivTuple (-1 : ℝ) (-1 : ℝ)).trans
+      (PiLp.linearEquiv 2 ℝ fun _ : Fin 4 => ℝ).symm with
     toFun := fun a => (PiLp.equiv _ fun _ : Fin 4 => _).symm ![a.1, a.2, a.3, a.4]
     invFun := fun a => ⟨a 0, a 1, a 2, a 3⟩
     norm_map' := norm_piLp_equiv_symm_equivTuple }
@@ -199,28 +200,28 @@ theorem continuous_coe : Continuous (coe : ℝ → ℍ) :=
 
 @[continuity]
 theorem continuous_normSq : Continuous (normSq : ℍ → ℝ) := by
-  simpa [← norm_sq_eq_norm_sq] using
+  simpa [← normSq_eq_norm_mul_self] using
     (continuous_norm.mul continuous_norm : Continuous fun q : ℍ => ‖q‖ * ‖q‖)
 #align quaternion.continuous_norm_sq Quaternion.continuous_normSq
 
 @[continuity]
 theorem continuous_re : Continuous fun q : ℍ => q.re :=
-  (continuous_apply 0).comp linearIsometryEquivTuple.Continuous
+  (continuous_apply 0).comp linearIsometryEquivTuple.continuous
 #align quaternion.continuous_re Quaternion.continuous_re
 
 @[continuity]
 theorem continuous_imI : Continuous fun q : ℍ => q.imI :=
-  (continuous_apply 1).comp linearIsometryEquivTuple.Continuous
+  (continuous_apply 1).comp linearIsometryEquivTuple.continuous
 #align quaternion.continuous_im_i Quaternion.continuous_imI
 
 @[continuity]
 theorem continuous_imJ : Continuous fun q : ℍ => q.imJ :=
-  (continuous_apply 2).comp linearIsometryEquivTuple.Continuous
+  (continuous_apply 2).comp linearIsometryEquivTuple.continuous
 #align quaternion.continuous_im_j Quaternion.continuous_imJ
 
 @[continuity]
 theorem continuous_imK : Continuous fun q : ℍ => q.imK :=
-  (continuous_apply 3).comp linearIsometryEquivTuple.Continuous
+  (continuous_apply 3).comp linearIsometryEquivTuple.continuous
 #align quaternion.continuous_im_k Quaternion.continuous_imK
 
 @[continuity]
@@ -229,8 +230,8 @@ theorem continuous_im : Continuous fun q : ℍ => q.im := by
 #align quaternion.continuous_im Quaternion.continuous_im
 
 instance : CompleteSpace ℍ :=
-  haveI : UniformEmbedding linear_isometry_equiv_tuple.to_linear_equiv.to_equiv.symm :=
-    linear_isometry_equiv_tuple.to_continuous_linear_equiv.symm.uniform_embedding
+  haveI : UniformEmbedding linearIsometryEquivTuple.toLinearEquiv.toEquiv.symm :=
+    linearIsometryEquivTuple.toContinuousLinearEquiv.symm.uniformEmbedding
   (completeSpace_congr this).1 (by infer_instance)
 
 section infinite_sum
@@ -253,11 +254,10 @@ theorem summable_coe {f : α → ℝ} : (Summable fun a => (f a : ℍ)) ↔ Summ
 @[norm_cast]
 theorem tsum_coe (f : α → ℝ) : (∑' a, (f a : ℍ)) = ↑(∑' a, f a) := by
   by_cases hf : Summable f
-  · exact (has_sum_coe.mpr hf.has_sum).tsum_eq
+  · exact (hasSum_coe.mpr hf.hasSum).tsum_eq
   · simp [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable (summable_coe.not.mpr hf)]
 #align quaternion.tsum_coe Quaternion.tsum_coe
 
 end infinite_sum
 
 end Quaternion
-

From 57762364e1c2c34c31b804041e8e97587108eea6 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Tue, 30 May 2023 22:52:06 -0500
Subject: [PATCH 5/7] auto: naming

---
 Mathlib/Analysis/Quaternion.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Analysis/Quaternion.lean b/Mathlib/Analysis/Quaternion.lean
index bc99a2797fe6d..5d47f46afed53 100644
--- a/Mathlib/Analysis/Quaternion.lean
+++ b/Mathlib/Analysis/Quaternion.lean
@@ -26,7 +26,7 @@ We show that the norm on `ℍ[ℝ]` agrees with the euclidean norm of its compon
 
 ## Notation
 
-The following notation is available with `open_locale quaternion`:
+The following notation is available with `open_locale Quaternion`:
 
 * `ℍ` : quaternions
 
@@ -183,7 +183,7 @@ theorem norm_piLp_equiv_symm_equivTuple (x : ℍ) :
 set_option linter.uppercaseLean3 false in
 #align quaternion.norm_pi_Lp_equiv_symm_equiv_tuple Quaternion.norm_piLp_equiv_symm_equivTuple
 
-/-- `quaternion_algebra.linear_equiv_tuple` as a `linear_isometry_equiv`. -/
+/-- `QuaternionAlgebra.linearEquivTuple` as a `LinearIsometryEquiv`. -/
 @[simps apply symm_apply]
 noncomputable def linearIsometryEquivTuple : ℍ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 4) :=
   { (QuaternionAlgebra.linearEquivTuple (-1 : ℝ) (-1 : ℝ)).trans

From 20d2ae27e721b0cb5cdd680d1a39b2e91b57f999 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Tue, 30 May 2023 22:56:15 -0500
Subject: [PATCH 6/7] Drop `open_locale`

---
 Mathlib/Algebra/Category/ModuleCat/Basic.lean        | 8 ++++----
 Mathlib/Algebra/Quaternion.lean                      | 2 +-
 Mathlib/Analysis/Quaternion.lean                     | 2 +-
 Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean | 2 +-
 Mathlib/Data/Matrix/Rank.lean                        | 2 +-
 5 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean
index bb114208630e1..d123c91501d69 100644
--- a/Mathlib/Algebra/Category/ModuleCat/Basic.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/Basic.lean
@@ -45,10 +45,10 @@ in the category of `R`-modules, we have to take care not to inadvertently end up
 Similarly, given `f : M ≃ₗ[R] N`, use `toModuleIso`, `toModuleIso'Left`, `toModuleIso'Right`
 or `toModuleIso'`, respectively.
 
-The arrow notations are localized, so you may have to `open_locale Module` to use them. Note that
-the notation for `asHomLeft` clashes with the notation used to promote functions between types to
-morphisms in the category `Type`, so to avoid confusion, it is probably a good idea to avoid having
-the locales `Module` and `CategoryTheory.Type` open at the same time.
+The arrow notations are localized, so you may have to `open ModuleCat` (or `open scoped ModuleCat`)
+to use them. Note that the notation for `asHomLeft` clashes with the notation used to promote
+functions between types to morphisms in the category `Type`, so to avoid confusion, it is probably a
+good idea to avoid having the locales `Module` and `CategoryTheory.Type` open at the same time.
 
 If you get an error when trying to apply a theorem and the `convert` tactic produces goals of the
 form `M = of R M`, then you probably used an incorrect variant of `asHom` or `toModuleIso`.
diff --git a/Mathlib/Algebra/Quaternion.lean b/Mathlib/Algebra/Quaternion.lean
index 6296a8ab0fcec..81c76c912f110 100644
--- a/Mathlib/Algebra/Quaternion.lean
+++ b/Mathlib/Algebra/Quaternion.lean
@@ -37,7 +37,7 @@ We also define the following algebraic structures on `ℍ[R]`:
 
 ## Notation
 
-The following notation is available with `open_locale Quaternion`.
+The following notation is available with `open Quaternion` or `open scoped Quaternion`.
 
 * `ℍ[R, c₁, c₂]` : `QuaternionAlgebra R c₁ c₂`
 * `ℍ[R]` : quaternions over `R`.
diff --git a/Mathlib/Analysis/Quaternion.lean b/Mathlib/Analysis/Quaternion.lean
index 5d47f46afed53..83956edc00b0a 100644
--- a/Mathlib/Analysis/Quaternion.lean
+++ b/Mathlib/Analysis/Quaternion.lean
@@ -26,7 +26,7 @@ We show that the norm on `ℍ[ℝ]` agrees with the euclidean norm of its compon
 
 ## Notation
 
-The following notation is available with `open_locale Quaternion`:
+The following notation is available with `open Quaternion` or `open scoped Quaternion`:
 
 * `ℍ` : quaternions
 
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean b/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
index 4a04f7ed0a033..f2439578956fe 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
@@ -407,7 +407,7 @@ theorem biproduct.bicone_ι (f : J → C) [HasBiproduct f] (b : J) :
 #align category_theory.limits.biproduct.bicone_ι CategoryTheory.Limits.biproduct.bicone_ι
 
 /-- Note that as this lemma has a `if` in the statement, we include a `DecidableEq` argument.
-This means you may not be able to `simp` using this lemma unless you `open_locale Classical`. -/
+This means you may not be able to `simp` using this lemma unless you `open Classical`. -/
 @[reassoc]
 theorem biproduct.ι_π [DecidableEq J] (f : J → C) [HasBiproduct f] (j j' : J) :
     biproduct.ι f j ≫ biproduct.π f j' = if h : j = j' then eqToHom (congr_arg f h) else 0 := by
diff --git a/Mathlib/Data/Matrix/Rank.lean b/Mathlib/Data/Matrix/Rank.lean
index e5b4528d86237..5ea6671dc1f19 100644
--- a/Mathlib/Data/Matrix/Rank.lean
+++ b/Mathlib/Data/Matrix/Rank.lean
@@ -171,7 +171,7 @@ end CommRing
 This section contains lemmas about the rank of `Matrix.transpose` and `Matrix.conjTranspose`.
 
 Unfortunately the proofs are essentially duplicated between the two; `ℚ` is a linearly-ordered ring
-but can't be a star-ordered ring, while `ℂ` is star-ordered (with `open_locale complex_order`) but
+but can't be a star-ordered ring, while `ℂ` is star-ordered (with `open ComplexOrder`) but
 not linearly ordered. For now we don't prove the transpose case for `ℂ`.
 
 TODO: the lemmas `Matrix.rank_transpose` and `Matrix.rank_conjTranspose` current follow a short

From 59b219637c3539c82a510357b0bb1750c895514f Mon Sep 17 00:00:00 2001
From: Parcly Taxel <reddeloostw@gmail.com>
Date: Wed, 31 May 2023 13:59:22 +0800
Subject: [PATCH 7/7] lint

---
 Mathlib/Analysis/Quaternion.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Analysis/Quaternion.lean b/Mathlib/Analysis/Quaternion.lean
index 83956edc00b0a..0592d4664d2a4 100644
--- a/Mathlib/Analysis/Quaternion.lean
+++ b/Mathlib/Analysis/Quaternion.lean
@@ -83,12 +83,12 @@ theorem nnnorm_coe (a : ℝ) : ‖(a : ℍ)‖₊ = ‖a‖₊ :=
   Subtype.ext <| norm_coe a
 #align quaternion.nnnorm_coe Quaternion.nnnorm_coe
 
-@[simp]
+@[simp, nolint simpNF] -- Porting note: simp cannot prove this
 theorem norm_star (a : ℍ) : ‖star a‖ = ‖a‖ := by
   simp_rw [norm_eq_sqrt_real_inner, inner_self, normSq_star]
 #align quaternion.norm_star Quaternion.norm_star
 
-@[simp]
+@[simp, nolint simpNF] -- Porting note: simp cannot prove this
 theorem nnnorm_star (a : ℍ) : ‖star a‖₊ = ‖a‖₊ :=
   Subtype.ext <| norm_star a
 #align quaternion.nnnorm_star Quaternion.nnnorm_star
@@ -150,7 +150,7 @@ theorem coeComplex_one : ((1 : ℂ) : ℍ) = 1 :=
   rfl
 #align quaternion.coe_complex_one Quaternion.coeComplex_one
 
-@[simp, norm_cast]
+@[simp, norm_cast, nolint simpNF] -- Porting note: simp cannot prove this
 theorem coe_real_complex_mul (r : ℝ) (z : ℂ) : (r • z : ℍ) = ↑r * ↑z := by ext <;> simp
 #align quaternion.coe_real_complex_mul Quaternion.coe_real_complex_mul