From 64b93422e32f79f5b75cfa95ece892c6bf56cda5 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 23 Jul 2023 09:09:58 +0000
Subject: [PATCH 01/12] tidy universe variables

---
 Mathlib/Algebra/RingQuot.lean | 41 ++++++++++++++++++-----------------
 1 file changed, 21 insertions(+), 20 deletions(-)

diff --git a/Mathlib/Algebra/RingQuot.lean b/Mathlib/Algebra/RingQuot.lean
index 2fc9ffe0f419c3..8a79627f55957d 100644
--- a/Mathlib/Algebra/RingQuot.lean
+++ b/Mathlib/Algebra/RingQuot.lean
@@ -24,13 +24,14 @@ Since everything runs in parallel for quotients of `R`-algebras, we do that case
 -/
 
 
-universe u₁ u₂ u₃ u₄
+universe uR uS uT uA
 
-variable {R : Type u₁} [Semiring R]
+variable {R : Type uR} [Semiring R]
 
-variable {S : Type u₂} [CommSemiring S]
+variable {S : Type uS} [CommSemiring S]
+variable {T : Type uT}
 
-variable {A : Type u₃} [Semiring A] [Algebra S A]
+variable {A : Type uA} [Semiring A] [Algebra S A]
 
 namespace RingCon
 
@@ -66,15 +67,15 @@ theorem Rel.add_right {r : R → R → Prop} ⦃a b c : R⦄ (h : Rel r b c) : R
   exact Rel.add_left h
 #align ring_quot.rel.add_right RingQuot.Rel.add_right
 
-theorem Rel.neg {R : Type u₁} [Ring R] {r : R → R → Prop} ⦃a b : R⦄ (h : Rel r a b) :
+theorem Rel.neg {R : Type uR} [Ring R] {r : R → R → Prop} ⦃a b : R⦄ (h : Rel r a b) :
     Rel r (-a) (-b) := by simp only [neg_eq_neg_one_mul a, neg_eq_neg_one_mul b, Rel.mul_right h]
 #align ring_quot.rel.neg RingQuot.Rel.neg
 
-theorem Rel.sub_left {R : Type u₁} [Ring R] {r : R → R → Prop} ⦃a b c : R⦄ (h : Rel r a b) :
+theorem Rel.sub_left {R : Type uR} [Ring R] {r : R → R → Prop} ⦃a b c : R⦄ (h : Rel r a b) :
     Rel r (a - c) (b - c) := by simp only [sub_eq_add_neg, h.add_left]
 #align ring_quot.rel.sub_left RingQuot.Rel.sub_left
 
-theorem Rel.sub_right {R : Type u₁} [Ring R] {r : R → R → Prop} ⦃a b c : R⦄ (h : Rel r b c) :
+theorem Rel.sub_right {R : Type uR} [Ring R] {r : R → R → Prop} ⦃a b c : R⦄ (h : Rel r b c) :
     Rel r (a - b) (a - c) := by simp only [sub_eq_add_neg, h.neg.add_right]
 #align ring_quot.rel.sub_right RingQuot.Rel.sub_right
 
@@ -169,10 +170,10 @@ private irreducible_def add : RingQuot r → RingQuot r → RingQuot r
 private irreducible_def mul : RingQuot r → RingQuot r → RingQuot r
   | ⟨a⟩, ⟨b⟩ => ⟨Quot.map₂ (· * ·) Rel.mul_right Rel.mul_left a b⟩
 
-private irreducible_def neg {R : Type u₁} [Ring R] (r : R → R → Prop) : RingQuot r → RingQuot r
+private irreducible_def neg {R : Type uR} [Ring R] (r : R → R → Prop) : RingQuot r → RingQuot r
   | ⟨a⟩ => ⟨Quot.map (fun a ↦ -a) Rel.neg a⟩
 
-private irreducible_def sub {R : Type u₁} [Ring R] (r : R → R → Prop) :
+private irreducible_def sub {R : Type uR} [Ring R] (r : R → R → Prop) :
   RingQuot r → RingQuot r → RingQuot r
   | ⟨a⟩, ⟨b⟩ => ⟨Quot.map₂ Sub.sub Rel.sub_right Rel.sub_left a b⟩
 
@@ -213,10 +214,10 @@ instance : Mul (RingQuot r) :=
 instance : Pow (RingQuot r) ℕ :=
   ⟨fun x n ↦ npow r n x⟩
 
-instance {R : Type u₁} [Ring R] (r : R → R → Prop) : Neg (RingQuot r) :=
+instance {R : Type uR} [Ring R] (r : R → R → Prop) : Neg (RingQuot r) :=
   ⟨neg r⟩
 
-instance {R : Type u₁} [Ring R] (r : R → R → Prop) : Sub (RingQuot r) :=
+instance {R : Type uR} [Ring R] (r : R → R → Prop) : Sub (RingQuot r) :=
   ⟨sub r⟩
 
 instance [Algebra S R] : SMul S (RingQuot r) :=
@@ -247,14 +248,14 @@ theorem pow_quot {a} {n : ℕ} : (⟨Quot.mk _ a⟩ ^ n : RingQuot r) = ⟨Quot.
   rw [npow_def]
 #align ring_quot.pow_quot RingQuot.pow_quot
 
-theorem neg_quot {R : Type u₁} [Ring R] (r : R → R → Prop) {a} :
+theorem neg_quot {R : Type uR} [Ring R] (r : R → R → Prop) {a} :
     (-⟨Quot.mk _ a⟩ : RingQuot r) = ⟨Quot.mk _ (-a)⟩ := by
   show neg r _ = _
   rw [neg_def]
   rfl
 #align ring_quot.neg_quot RingQuot.neg_quot
 
-theorem sub_quot {R : Type u₁} [Ring R] (r : R → R → Prop) {a b} :
+theorem sub_quot {R : Type uR} [Ring R] (r : R → R → Prop) {a b} :
     (⟨Quot.mk _ a⟩ - ⟨Quot.mk _ b⟩ : RingQuot r) = ⟨Quot.mk _ (a - b)⟩ := by
   show sub r _ _ = _
   rw [sub_def]
@@ -337,7 +338,7 @@ instance instSemiring (r : R → R → Prop) : Semiring (RingQuot r) where
   __ := instAddCommMonoid r
   __ := instMonoidWithZero r
 
-instance instRing {R : Type u₁} [Ring R] (r : R → R → Prop) : Ring (RingQuot r) :=
+instance instRing {R : Type uR} [Ring R] (r : R → R → Prop) : Ring (RingQuot r) :=
   { RingQuot.instSemiring r with
     neg := Neg.neg
     add_left_neg := by
@@ -358,14 +359,14 @@ instance instRing {R : Type u₁} [Ring R] (r : R → R → Prop) : Ring (RingQu
       rintro n ⟨⟨⟩⟩
       simp [smul_quot, neg_quot, add_mul] }
 
-instance instCommSemiring {R : Type u₁} [CommSemiring R] (r : R → R → Prop) :
+instance instCommSemiring {R : Type uR} [CommSemiring R] (r : R → R → Prop) :
   CommSemiring (RingQuot r) :=
   { RingQuot.instSemiring r with
     mul_comm := by
       rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩
       simp [mul_quot, mul_comm] }
 
-instance {R : Type u₁} [CommRing R] (r : R → R → Prop) : CommRing (RingQuot r) :=
+instance {R : Type uR} [CommRing R] (r : R → R → Prop) : CommRing (RingQuot r) :=
   { RingQuot.instCommSemiring r, RingQuot.instRing r with }
 
 instance (r : R → R → Prop) : Inhabited (RingQuot r) :=
@@ -406,14 +407,14 @@ theorem mkRingHom_surjective (r : R → R → Prop) : Function.Surjective (mkRin
 #align ring_quot.mk_ring_hom_surjective RingQuot.mkRingHom_surjective
 
 @[ext 1100]
-theorem ringQuot_ext {T : Type u₄} [Semiring T] {r : R → R → Prop} (f g : RingQuot r →+* T)
+theorem ringQuot_ext [Semiring T] {r : R → R → Prop} (f g : RingQuot r →+* T)
     (w : f.comp (mkRingHom r) = g.comp (mkRingHom r)) : f = g := by
   ext x
   rcases mkRingHom_surjective r x with ⟨x, rfl⟩
   exact (RingHom.congr_fun w x : _)
 #align ring_quot.ring_quot_ext RingQuot.ringQuot_ext
 
-variable {T : Type u₄} [Semiring T]
+variable [Semiring T]
 
 irreducible_def preLift {r : R → R → Prop} { f : R →+* T } (h : ∀ ⦃x y⦄, r x y → f x = f y) :
   RingQuot r →+* T :=
@@ -482,7 +483,7 @@ agrees with the quotient by the appropriate ideal.
 -/
 
 
-variable {B : Type u₁} [CommRing B]
+variable {B : Type uR} [CommRing B]
 
 /-- The universal ring homomorphism from `RingQuot r` to `B ⧸ Ideal.ofRel r`. -/
 def ringQuotToIdealQuotient (r : B → B → Prop) : RingQuot r →+* B ⧸ Ideal.ofRel r :=
@@ -564,7 +565,7 @@ theorem star'_quot (hr : ∀ a b, r a b → r (star a) (star b)) {a} :
 #align ring_quot.star'_quot RingQuot.star'_quot
 
 /-- Transfer a star_ring instance through a quotient, if the quotient is invariant to `star` -/
-def starRing {R : Type u₁} [Semiring R] [StarRing R] (r : R → R → Prop)
+def starRing {R : Type uR} [Semiring R] [StarRing R] (r : R → R → Prop)
     (hr : ∀ a b, r a b → r (star a) (star b)) : StarRing (RingQuot r) where
   star := star' r hr
   star_involutive := by

From 23a1289cb60dfca085b1b6b2dd34e10d9943d7c5 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 23 Jul 2023 09:20:40 +0000
Subject: [PATCH 02/12] feat: add scalar tower instances for RingQuot and
 BilinForm

---
 Mathlib/Algebra/RingQuot.lean           |  8 ++++++++
 Mathlib/LinearAlgebra/BilinearForm.lean | 15 +++++++++++++++
 2 files changed, 23 insertions(+)

diff --git a/Mathlib/Algebra/RingQuot.lean b/Mathlib/Algebra/RingQuot.lean
index 8a79627f55957d..dc76659b04fc08 100644
--- a/Mathlib/Algebra/RingQuot.lean
+++ b/Mathlib/Algebra/RingQuot.lean
@@ -269,6 +269,14 @@ theorem smul_quot [Algebra S R] {n : S} {a : R} :
   rfl
 #align ring_quot.smul_quot RingQuot.smul_quot
 
+instance [CommSemiring T] [SMul S T] [Algebra S R] [Algebra T R] [IsScalarTower S T R] :
+    IsScalarTower S T (RingQuot r) :=
+  ⟨fun s t ⟨a⟩ => Quot.inductionOn a <| fun a' => by simp only [RingQuot.smul_quot, smul_assoc]⟩
+
+instance [CommSemiring T] [SMul S T] [Algebra S R] [Algebra T R] [SMulCommClass S T R] :
+    SMulCommClass S T (RingQuot r) :=
+  ⟨fun s t ⟨a⟩ => Quot.inductionOn a <| fun a' => by simp only [RingQuot.smul_quot, smul_comm]⟩
+
 instance instAddCommMonoid (r : R → R → Prop) : AddCommMonoid (RingQuot r) where
   add := (· + ·)
   zero := 0
diff --git a/Mathlib/LinearAlgebra/BilinearForm.lean b/Mathlib/LinearAlgebra/BilinearForm.lean
index 2e4e1f82eefe13..b742ee11034f6e 100644
--- a/Mathlib/LinearAlgebra/BilinearForm.lean
+++ b/Mathlib/LinearAlgebra/BilinearForm.lean
@@ -223,6 +223,21 @@ theorem smul_apply {α} [Monoid α] [DistribMulAction α R] [SMulCommClass α R
   rfl
 #align bilin_form.smul_apply BilinForm.smul_apply
 
+instance {α β} [Monoid α] [Monoid β] [DistribMulAction α R] [DistribMulAction β R]
+    [SMulCommClass α R R] [SMulCommClass β R R] [SMulCommClass α β R] :
+    SMulCommClass α β (BilinForm R M) :=
+  ⟨fun a b B => ext $ fun x y => smul_comm a b (B x y)⟩
+
+instance {α β} [Monoid α] [Monoid β] [SMul α β] [DistribMulAction α R] [DistribMulAction β R]
+    [SMulCommClass α R R] [SMulCommClass β R R] [IsScalarTower α β R] :
+    IsScalarTower α β (BilinForm R M) :=
+  ⟨fun a b B => ext $ fun x y => smul_assoc a b (B x y)⟩
+
+instance {α} [Monoid α] [DistribMulAction α R] [DistribMulAction αᵐᵒᵖ R]
+    [SMulCommClass α R R] [IsCentralScalar α R] :
+    IsCentralScalar α (BilinForm R M) :=
+  ⟨fun a B => ext $ fun x y => op_smul_eq_smul a (B x y)⟩
+
 instance : AddCommMonoid (BilinForm R M) :=
   Function.Injective.addCommMonoid _ coe_injective coe_zero coe_add fun _ _ => coe_smul _ _
 

From 534225e98015f87280501c1ffb493226de99abf4 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 23 Jul 2023 14:25:51 +0000
Subject: [PATCH 03/12] feat(Algebra/FreeAlgebra): support towers of algebras

This provide `Algebra R (FreeAlgebra A X)` when `Algebra R A`.
This also fixes some diamonds that would arise as a result of this new instance.
---
 Mathlib/Algebra/Algebra/Basic.lean |  5 +++-
 Mathlib/Algebra/FreeAlgebra.lean   | 40 +++++++++++++++++++++++-------
 Mathlib/Algebra/Module/Basic.lean  | 37 +++++++++++++++------------
 3 files changed, 56 insertions(+), 26 deletions(-)

diff --git a/Mathlib/Algebra/Algebra/Basic.lean b/Mathlib/Algebra/Algebra/Basic.lean
index ada2763daa8ebd..0420e918f71e8b 100644
--- a/Mathlib/Algebra/Algebra/Basic.lean
+++ b/Mathlib/Algebra/Algebra/Basic.lean
@@ -582,7 +582,10 @@ variable (R)
 See note [reducible non-instances]. -/
 @[reducible]
 def semiringToRing [Semiring A] [Algebra R A] : Ring A :=
-  { Module.addCommMonoidToAddCommGroup R, (inferInstance : Semiring A) with }
+  { Module.addCommMonoidToAddCommGroup R, (inferInstance : Semiring A) with
+    intCast := fun z => algebraMap R A z
+    intCast_ofNat := fun z => by simp only [Int.cast_ofNat, map_natCast]
+    intCast_negSucc := fun z => by simp }
 #align algebra.semiring_to_ring Algebra.semiringToRing
 
 end Ring
diff --git a/Mathlib/Algebra/FreeAlgebra.lean b/Mathlib/Algebra/FreeAlgebra.lean
index 4dfae3baba9e45..317432eef7042f 100644
--- a/Mathlib/Algebra/FreeAlgebra.lean
+++ b/Mathlib/Algebra/FreeAlgebra.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Adam Topaz
 -/
 import Mathlib.Algebra.Algebra.Subalgebra.Basic
+import Mathlib.Algebra.Algebra.Tower
 import Mathlib.Algebra.MonoidAlgebra.Basic
 import Mathlib.Algebra.Free
 
@@ -202,23 +203,44 @@ instance : Semiring (FreeAlgebra R X) where
 instance : Inhabited (FreeAlgebra R X) :=
   ⟨0⟩
 
-instance : SMul R (FreeAlgebra R X) where
-  smul r := Quot.map ((· * ·) ↑r) fun _ _ ↦ Rel.mul_compat_right
-
-instance : Algebra R (FreeAlgebra R X) where
-  toFun r := Quot.mk _ r
-  map_one' := rfl
-  map_mul' _ _ := Quot.sound Rel.mul_scalar
-  map_zero' := rfl
-  map_add' _ _ := Quot.sound Rel.add_scalar
+instance {A} [CommSemiring A] [Algebra R A] : SMul R (FreeAlgebra A X) where
+  smul r := Quot.map (algebraMap R A r * ·) fun _ _ ↦ Rel.mul_compat_right
+
+instance instAlgebra {A} [CommSemiring A] [Algebra R A] : Algebra R (FreeAlgebra A X) where
+  toRingHom := ({
+      toFun := fun r => Quot.mk _ r
+      map_one' := rfl
+      map_mul' := fun _ _ => Quot.sound Rel.mul_scalar
+      map_zero' := rfl
+      map_add' := fun _ _ => Quot.sound Rel.add_scalar } : A →+* FreeAlgebra A X).comp
+      (algebraMap R A)
   commutes' _ := by
     rintro ⟨⟩
     exact Quot.sound Rel.central_scalar
   smul_def' _ _ := rfl
 
+instance {R S A} [CommSemiring R] [CommSemiring S] [CommSemiring A]
+    [SMul R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] :
+    IsScalarTower R S (FreeAlgebra A X) where
+  smul_assoc r s x := by
+    change algebraMap S A (r • s) • x = algebraMap R A _ • (algebraMap S A _ • x)
+    rw [←smul_assoc]
+    congr
+    simp only [Algebra.algebraMap_eq_smul_one, smul_eq_mul]
+    rw [smul_assoc, ←smul_one_mul]
+
+instance {R S A} [CommSemiring R] [CommSemiring S] [CommSemiring A]
+    [Algebra R A] [Algebra S A] [SMulCommClass R S A] :
+    SMulCommClass R S (FreeAlgebra A X) where
+  smul_comm r s x := smul_comm (algebraMap R A r) (algebraMap S A s) x
+
 instance {S : Type _} [CommRing S] : Ring (FreeAlgebra S X) :=
   Algebra.semiringToRing S
 
+-- verify there is no diamond
+variable (S : Type) [CommRing S] in
+example : (algebraInt _ : Algebra ℤ (FreeAlgebra S X)) = instAlgebra _ _ := rfl
+
 variable {X}
 
 /-- The canonical function `X → FreeAlgebra R X`.
diff --git a/Mathlib/Algebra/Module/Basic.lean b/Mathlib/Algebra/Module/Basic.lean
index b85d707d9d6eeb..ab4556f543def7 100644
--- a/Mathlib/Algebra/Module/Basic.lean
+++ b/Mathlib/Algebra/Module/Basic.lean
@@ -209,22 +209,6 @@ theorem smul_add_one_sub_smul {R : Type _} [Ring R] [Module R M] {r : R} {m : M}
 
 end AddCommMonoid
 
-variable (R)
-
-/-- An `AddCommMonoid` that is a `Module` over a `Ring` carries a natural `AddCommGroup`
-structure.
-See note [reducible non-instances]. -/
-@[reducible]
-def Module.addCommMonoidToAddCommGroup [Ring R] [AddCommMonoid M] [Module R M] : AddCommGroup M :=
-  { (inferInstance : AddCommMonoid M) with
-    neg := fun a => (-1 : R) • a
-    add_left_neg := fun a =>
-      show (-1 : R) • a + a = 0 by
-        nth_rw 2 [← one_smul R a]
-        rw [← add_smul, add_left_neg, zero_smul] }
-#align module.add_comm_monoid_to_add_comm_group Module.addCommMonoidToAddCommGroup
-
-variable {R}
 
 section AddCommGroup
 
@@ -322,6 +306,27 @@ theorem sub_smul (r s : R) (y : M) : (r - s) • y = r • y - s • y := by
 
 end Module
 
+variable (R)
+
+/-- An `AddCommMonoid` that is a `Module` over a `Ring` carries a natural `AddCommGroup`
+structure.
+See note [reducible non-instances]. -/
+@[reducible]
+def Module.addCommMonoidToAddCommGroup [Ring R] [AddCommMonoid M] [Module R M] : AddCommGroup M :=
+  { (inferInstance : AddCommMonoid M) with
+    neg := fun a => (-1 : R) • a
+    add_left_neg := fun a =>
+      show (-1 : R) • a + a = 0 by
+        nth_rw 2 [← one_smul R a]
+        rw [← add_smul, add_left_neg, zero_smul]
+    zsmul := fun z a => (z : R) • a
+    zsmul_zero' := fun a => by simpa only [Int.cast_zero] using zero_smul R a
+    zsmul_succ' := fun z a => by simp [add_comm, add_smul]
+    zsmul_neg' := fun z a => by simp [←smul_assoc, neg_one_smul] }
+#align module.add_comm_monoid_to_add_comm_group Module.addCommMonoidToAddCommGroup
+
+variable {R}
+
 /-- A module over a `Subsingleton` semiring is a `Subsingleton`. We cannot register this
 as an instance because Lean has no way to guess `R`. -/
 protected theorem Module.subsingleton (R M : Type _) [Semiring R] [Subsingleton R] [AddCommMonoid M]

From 72ecf112c3dd2d2b4ee985a4c17e8c5480e15388 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 23 Jul 2023 14:59:16 +0000
Subject: [PATCH 04/12] wip

---
 Mathlib/Algebra/RingQuot.lean                 |  2 +-
 .../LinearAlgebra/TensorAlgebra/Basic.lean    | 21 +++++++++++++++++++
 2 files changed, 22 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/RingQuot.lean b/Mathlib/Algebra/RingQuot.lean
index dc76659b04fc08..79bd63c7b53486 100644
--- a/Mathlib/Algebra/RingQuot.lean
+++ b/Mathlib/Algebra/RingQuot.lean
@@ -273,7 +273,7 @@ instance [CommSemiring T] [SMul S T] [Algebra S R] [Algebra T R] [IsScalarTower
     IsScalarTower S T (RingQuot r) :=
   ⟨fun s t ⟨a⟩ => Quot.inductionOn a <| fun a' => by simp only [RingQuot.smul_quot, smul_assoc]⟩
 
-instance [CommSemiring T] [SMul S T] [Algebra S R] [Algebra T R] [SMulCommClass S T R] :
+instance [CommSemiring T] [Algebra S R] [Algebra T R] [SMulCommClass S T R] :
     SMulCommClass S T (RingQuot r) :=
   ⟨fun s t ⟨a⟩ => Quot.inductionOn a <| fun a' => by simp only [RingQuot.smul_quot, smul_comm]⟩
 
diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
index d1824544349160..4003a159e26a8b 100644
--- a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
+++ b/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
@@ -67,6 +67,27 @@ def TensorAlgebra :=
 -- Porting note: Expanded `deriving Inhabited, Semiring, Algebra`
 instance : Inhabited (TensorAlgebra R M) := RingQuot.instInhabitedRingQuot _
 instance : Semiring (TensorAlgebra R M) := RingQuot.instSemiring _
+
+-- `IsScalarTower` is not needed, but the instance isn't really canonical without it.
+@[nolint unusedArguments]
+instance {R A M} [CommSemiring R] [AddCommMonoid M] [CommSemiring A]
+  [Algebra R A] [Module R M] [Module A M]
+  [IsScalarTower R A M] :
+  Algebra R (TensorAlgebra A M) :=
+RingQuot.instAlgebraRingQuotInstSemiring _
+
+instance {R S A M} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [CommSemiring A]
+  [Algebra R A] [Algebra S A] [Module R M] [Module S M] [Module A M]
+  [IsScalarTower R A M] [IsScalarTower S A M] [SMulCommClass R S A] :
+  SMulCommClass R S (TensorAlgebra A M) :=
+RingQuot.instSMulCommClassRingQuotInstSMulRingQuotInstSMulRingQuot _
+
+instance {R S A M} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [CommSemiring A]
+  [SMul R S] [Algebra R A] [Algebra S A] [Module R M] [Module S M] [Module A M]
+  [IsScalarTower R A M] [IsScalarTower S A M] [IsScalarTower R S A] :
+  IsScalarTower R S (TensorAlgebra A M) :=
+RingQuot.instIsScalarTowerRingQuotInstSMulRingQuotInstSMulRingQuot _
+
 instance : Algebra R (TensorAlgebra R M) := RingQuot.instAlgebraRingQuotInstSemiring _
 
 namespace TensorAlgebra

From b81c037650df5b769f97cee27a64205d3467eb74 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 23 Jul 2023 15:33:41 +0000
Subject: [PATCH 05/12] fix more diamonds

---
 Mathlib/Algebra/FreeAlgebra.lean               |  2 ++
 Mathlib/Algebra/RingQuot.lean                  | 18 +++++++++++++++---
 Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean | 10 +++++++---
 3 files changed, 24 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Algebra/FreeAlgebra.lean b/Mathlib/Algebra/FreeAlgebra.lean
index 317432eef7042f..4db299193abcca 100644
--- a/Mathlib/Algebra/FreeAlgebra.lean
+++ b/Mathlib/Algebra/FreeAlgebra.lean
@@ -238,6 +238,8 @@ instance {S : Type _} [CommRing S] : Ring (FreeAlgebra S X) :=
   Algebra.semiringToRing S
 
 -- verify there is no diamond
+-- variable (S : Type) [CommSemiring S] in
+-- example : (algebraNat : Algebra ℕ (FreeAlgebra R X)) = instAlgebra _ _ := rfl
 variable (S : Type) [CommRing S] in
 example : (algebraInt _ : Algebra ℤ (FreeAlgebra S X)) = instAlgebra _ _ := rfl
 
diff --git a/Mathlib/Algebra/RingQuot.lean b/Mathlib/Algebra/RingQuot.lean
index 79bd63c7b53486..ce2ca5820574a6 100644
--- a/Mathlib/Algebra/RingQuot.lean
+++ b/Mathlib/Algebra/RingQuot.lean
@@ -196,7 +196,8 @@ private irreducible_def npow (n : ℕ) : RingQuot r → RingQuot r
             exact this)
         a⟩
 
-private irreducible_def smul [Algebra S R] (n : S) : RingQuot r → RingQuot r
+-- note: this cannot be irreducible, as otherwise diamonds don't commute.
+private def smul [Algebra S R] (n : S) : RingQuot r → RingQuot r
   | ⟨a⟩ => ⟨Quot.map (fun a ↦ n • a) (Rel.smul n) a⟩
 
 instance : Zero (RingQuot r) :=
@@ -265,7 +266,7 @@ theorem sub_quot {R : Type uR} [Ring R] (r : R → R → Prop) {a b} :
 theorem smul_quot [Algebra S R] {n : S} {a : R} :
     (n • ⟨Quot.mk _ a⟩ : RingQuot r) = ⟨Quot.mk _ (n • a)⟩ := by
   show smul r _ _ = _
-  rw [smul_def]
+  rw [smul]
   rfl
 #align ring_quot.smul_quot RingQuot.smul_quot
 
@@ -346,6 +347,10 @@ instance instSemiring (r : R → R → Prop) : Semiring (RingQuot r) where
   __ := instAddCommMonoid r
   __ := instMonoidWithZero r
 
+-- can't be irreducible, causes diamonds in ℤ-algebras
+private def intCast {R : Type uR} [Ring R] (r : R → R → Prop) (z : ℤ) : RingQuot r :=
+  ⟨Quot.mk _ z⟩
+
 instance instRing {R : Type uR} [Ring R] (r : R → R → Prop) : Ring (RingQuot r) :=
   { RingQuot.instSemiring r with
     neg := Neg.neg
@@ -365,7 +370,14 @@ instance instRing {R : Type uR} [Ring R] (r : R → R → Prop) : Ring (RingQuot
       simp [smul_quot, add_quot, add_mul, add_comm]
     zsmul_neg' := by
       rintro n ⟨⟨⟩⟩
-      simp [smul_quot, neg_quot, add_mul] }
+      simp [smul_quot, neg_quot, add_mul]
+    intCast := intCast r
+    intCast_ofNat := fun n => congrArg RingQuot.mk <| by
+      rw [natCast_def]
+      exact congrArg (Quot.mk _) (Int.cast_ofNat _)
+    intCast_negSucc := fun n => congrArg RingQuot.mk <| by
+      simp_rw [neg_def, natCast_def]
+      exact congrArg (Quot.mk _) (Int.cast_negSucc n) }
 
 instance instCommSemiring {R : Type uR} [CommSemiring R] (r : R → R → Prop) :
   CommSemiring (RingQuot r) :=
diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
index 4003a159e26a8b..e34dd8206a19ea 100644
--- a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
+++ b/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
@@ -70,7 +70,7 @@ instance : Semiring (TensorAlgebra R M) := RingQuot.instSemiring _
 
 -- `IsScalarTower` is not needed, but the instance isn't really canonical without it.
 @[nolint unusedArguments]
-instance {R A M} [CommSemiring R] [AddCommMonoid M] [CommSemiring A]
+instance instAlgebra {R A M} [CommSemiring R] [AddCommMonoid M] [CommSemiring A]
   [Algebra R A] [Module R M] [Module A M]
   [IsScalarTower R A M] :
   Algebra R (TensorAlgebra A M) :=
@@ -88,13 +88,17 @@ instance {R S A M} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [CommSemi
   IsScalarTower R S (TensorAlgebra A M) :=
 RingQuot.instIsScalarTowerRingQuotInstSMulRingQuotInstSMulRingQuot _
 
-instance : Algebra R (TensorAlgebra R M) := RingQuot.instAlgebraRingQuotInstSemiring _
-
 namespace TensorAlgebra
 
 instance {S : Type _} [CommRing S] [Module S M] : Ring (TensorAlgebra S M) :=
   RingQuot.instRing (Rel S M)
 
+-- verify there is no diamond
+variable (S M : Type) [CommRing S] [AddCommGroup M] [Module S M] in
+example : (algebraInt _ : Algebra ℤ (TensorAlgebra S M)) = instAlgebra := rfl
+
+-- example : (algebraNat : Algebra ℕ (TensorAlgebra R M)) = instAlgebra := rfl
+
 variable {M}
 
 /-- The canonical linear map `M →ₗ[R] TensorAlgebra R M`.

From 8514db78b30dd4000822c1f605d047f688824bd0 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 23 Jul 2023 15:48:11 +0000
Subject: [PATCH 06/12] sorried for now

---
 Mathlib/Algebra/FreeAlgebra.lean | 22 +++++++++++++++++++---
 1 file changed, 19 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Algebra/FreeAlgebra.lean b/Mathlib/Algebra/FreeAlgebra.lean
index 317432eef7042f..c9430de3444179 100644
--- a/Mathlib/Algebra/FreeAlgebra.lean
+++ b/Mathlib/Algebra/FreeAlgebra.lean
@@ -160,6 +160,9 @@ namespace FreeAlgebra
 attribute [local instance] Pre.hasCoeGenerator Pre.hasCoeSemiring Pre.hasMul Pre.hasAdd
   Pre.hasZero Pre.hasOne Pre.hasSmul
 
+instance {A} [CommSemiring A] [Algebra R A] : SMul R (FreeAlgebra A X) where
+  smul r := Quot.map (algebraMap R A r * ·) fun _ _ ↦ Rel.mul_compat_right
+
 instance : Semiring (FreeAlgebra R X) where
   add := Quot.map₂ (· + ·) (fun _ _ _ ↦ Rel.add_compat_right) fun _ _ _ ↦ Rel.add_compat_left
   add_assoc := by
@@ -199,13 +202,24 @@ instance : Semiring (FreeAlgebra R X) where
   mul_zero := by
     rintro ⟨⟩
     exact Quot.sound Rel.MulZeroClass.mul_zero
+  nsmul := (· • ·)
+  nsmul_zero := by
+    rintro ⟨⟩
+    change Quot.mk _ (_ * _) = _
+    rw [map_zero]
+    exact Quot.sound Rel.MulZeroClass.zero_mul
+  nsmul_succ n := by
+    rintro ⟨⟩
+    change Quot.mk _ (_ * _) = Quot.mk _ _
+    rw [map_add, map_one]
+    sorry
+  natCast n := Quot.mk _ (n : R)
+  natCast_zero := sorry
+  natCast_succ n := sorry
 
 instance : Inhabited (FreeAlgebra R X) :=
   ⟨0⟩
 
-instance {A} [CommSemiring A] [Algebra R A] : SMul R (FreeAlgebra A X) where
-  smul r := Quot.map (algebraMap R A r * ·) fun _ _ ↦ Rel.mul_compat_right
-
 instance instAlgebra {A} [CommSemiring A] [Algebra R A] : Algebra R (FreeAlgebra A X) where
   toRingHom := ({
       toFun := fun r => Quot.mk _ r
@@ -238,6 +252,8 @@ instance {S : Type _} [CommRing S] : Ring (FreeAlgebra S X) :=
   Algebra.semiringToRing S
 
 -- verify there is no diamond
+variable (S : Type) [CommSemiring S] in
+example : (algebraNat : Algebra ℕ (FreeAlgebra S X)) = instAlgebra _ _ := rfl
 variable (S : Type) [CommRing S] in
 example : (algebraInt _ : Algebra ℤ (FreeAlgebra S X)) = instAlgebra _ _ := rfl
 

From e1494c86ca27ea5cc86a6a0f6889057f93149e56 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 23 Jul 2023 16:43:26 +0000
Subject: [PATCH 07/12] fix diamonds

---
 Mathlib/Algebra/FreeAlgebra.lean | 92 +++++++++++++++++++++-----------
 1 file changed, 61 insertions(+), 31 deletions(-)

diff --git a/Mathlib/Algebra/FreeAlgebra.lean b/Mathlib/Algebra/FreeAlgebra.lean
index c9430de3444179..0b2da9791eb6ee 100644
--- a/Mathlib/Algebra/FreeAlgebra.lean
+++ b/Mathlib/Algebra/FreeAlgebra.lean
@@ -160,26 +160,31 @@ namespace FreeAlgebra
 attribute [local instance] Pre.hasCoeGenerator Pre.hasCoeSemiring Pre.hasMul Pre.hasAdd
   Pre.hasZero Pre.hasOne Pre.hasSmul
 
-instance {A} [CommSemiring A] [Algebra R A] : SMul R (FreeAlgebra A X) where
-  smul r := Quot.map (algebraMap R A r * ·) fun _ _ ↦ Rel.mul_compat_right
+/-! Define the basic operations-/
 
-instance : Semiring (FreeAlgebra R X) where
-  add := Quot.map₂ (· + ·) (fun _ _ _ ↦ Rel.add_compat_right) fun _ _ _ ↦ Rel.add_compat_left
-  add_assoc := by
-    rintro ⟨⟩ ⟨⟩ ⟨⟩
-    exact Quot.sound Rel.add_assoc
-  zero := Quot.mk _ 0
-  zero_add := by
-    rintro ⟨⟩
-    exact Quot.sound Rel.zero_add
-  add_zero := by
-    rintro ⟨⟩
-    change Quot.mk _ _ = _
-    rw [Quot.sound Rel.add_comm, Quot.sound Rel.zero_add]
-  add_comm := by
-    rintro ⟨⟩ ⟨⟩
-    exact Quot.sound Rel.add_comm
-  mul := Quot.map₂ (· * ·) (fun _ _ _ ↦ Rel.mul_compat_right) fun _ _ _ ↦ Rel.mul_compat_left
+instance instSMul {A} [CommSemiring A] [Algebra R A] : SMul R (FreeAlgebra A X) where
+  smul r := Quot.map (HMul.hMul (algebraMap R A r : Pre A X)) fun _ _ ↦ Rel.mul_compat_right
+
+instance instZero : Zero (FreeAlgebra R X) where zero := Quot.mk _ 0
+
+instance instOne : One (FreeAlgebra R X) where one := Quot.mk _ 1
+
+instance instAdd : Add (FreeAlgebra R X) where
+  add := Quot.map₂ HAdd.hAdd (fun _ _ _ ↦ Rel.add_compat_right) fun _ _ _ ↦ Rel.add_compat_left
+
+instance instMul : Mul (FreeAlgebra R X) where
+  mul := Quot.map₂ HMul.hMul (fun _ _ _ ↦ Rel.mul_compat_right) fun _ _ _ ↦ Rel.mul_compat_left
+
+-- `Quot.mk` is an implementation detail of `FreeAlgebra`, so this lemma is private
+private theorem mk_mul (x y : Pre R X) :
+    Quot.mk (Rel R X) (x * y) = (HMul.hMul (self := instHMul (α := FreeAlgebra R X))
+    (Quot.mk (Rel R X) x) (Quot.mk (Rel R X) y)) :=
+  rfl
+
+/-! Build the semiring structure. We do this one piece at a time as this is convenient for proving
+the `nsmul` fields. -/
+
+instance instMonoidWithZero : MonoidWithZero (FreeAlgebra R X) where
   mul_assoc := by
     rintro ⟨⟩ ⟨⟩ ⟨⟩
     exact Quot.sound Rel.mul_assoc
@@ -190,18 +195,35 @@ instance : Semiring (FreeAlgebra R X) where
   mul_one := by
     rintro ⟨⟩
     exact Quot.sound Rel.mul_one
+  zero_mul := by
+    rintro ⟨⟩
+    exact Quot.sound Rel.MulZeroClass.zero_mul
+  mul_zero := by
+    rintro ⟨⟩
+    exact Quot.sound Rel.MulZeroClass.mul_zero
+
+instance instDistrib : Distrib (FreeAlgebra R X) where
   left_distrib := by
     rintro ⟨⟩ ⟨⟩ ⟨⟩
     exact Quot.sound Rel.left_distrib
   right_distrib := by
     rintro ⟨⟩ ⟨⟩ ⟨⟩
     exact Quot.sound Rel.right_distrib
-  zero_mul := by
+
+instance instAddCommMonoid : AddCommMonoid (FreeAlgebra R X) where
+  add_assoc := by
+    rintro ⟨⟩ ⟨⟩ ⟨⟩
+    exact Quot.sound Rel.add_assoc
+  zero_add := by
     rintro ⟨⟩
-    exact Quot.sound Rel.MulZeroClass.zero_mul
-  mul_zero := by
+    exact Quot.sound Rel.zero_add
+  add_zero := by
     rintro ⟨⟩
-    exact Quot.sound Rel.MulZeroClass.mul_zero
+    change Quot.mk _ _ = _
+    rw [Quot.sound Rel.add_comm, Quot.sound Rel.zero_add]
+  add_comm := by
+    rintro ⟨⟩ ⟨⟩
+    exact Quot.sound Rel.add_comm
   nsmul := (· • ·)
   nsmul_zero := by
     rintro ⟨⟩
@@ -209,13 +231,19 @@ instance : Semiring (FreeAlgebra R X) where
     rw [map_zero]
     exact Quot.sound Rel.MulZeroClass.zero_mul
   nsmul_succ n := by
-    rintro ⟨⟩
-    change Quot.mk _ (_ * _) = Quot.mk _ _
-    rw [map_add, map_one]
-    sorry
+    rintro ⟨a⟩
+    dsimp only [HSMul.hSMul, instSMul, Quot.map]
+    rw [map_add, map_one, add_comm, mk_mul, mk_mul, ←one_add_mul (_ : FreeAlgebra R X)]
+    congr 1
+    exact Quot.sound Rel.add_scalar
+
+instance : Semiring (FreeAlgebra R X) where
+  __ := instMonoidWithZero R X
+  __ := instAddCommMonoid R X
+  __ := instDistrib R X
   natCast n := Quot.mk _ (n : R)
-  natCast_zero := sorry
-  natCast_succ n := sorry
+  natCast_zero := by simp; rfl
+  natCast_succ n := by simp; exact Quot.sound Rel.add_scalar
 
 instance : Inhabited (FreeAlgebra R X) :=
   ⟨0⟩
@@ -233,6 +261,10 @@ instance instAlgebra {A} [CommSemiring A] [Algebra R A] : Algebra R (FreeAlgebra
     exact Quot.sound Rel.central_scalar
   smul_def' _ _ := rfl
 
+-- verify there is no diamond
+variable (S : Type) [CommSemiring S] in
+example : (algebraNat : Algebra ℕ (FreeAlgebra S X)) = instAlgebra _ _ := rfl
+
 instance {R S A} [CommSemiring R] [CommSemiring S] [CommSemiring A]
     [SMul R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] :
     IsScalarTower R S (FreeAlgebra A X) where
@@ -252,8 +284,6 @@ instance {S : Type _} [CommRing S] : Ring (FreeAlgebra S X) :=
   Algebra.semiringToRing S
 
 -- verify there is no diamond
-variable (S : Type) [CommSemiring S] in
-example : (algebraNat : Algebra ℕ (FreeAlgebra S X)) = instAlgebra _ _ := rfl
 variable (S : Type) [CommRing S] in
 example : (algebraInt _ : Algebra ℤ (FreeAlgebra S X)) = instAlgebra _ _ := rfl
 

From 58ce2c852e4a50353d0b7aa630303835de12291a Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 23 Jul 2023 16:44:33 +0000
Subject: [PATCH 08/12] deduplicate

---
 Mathlib/Algebra/FreeAlgebra.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Mathlib/Algebra/FreeAlgebra.lean b/Mathlib/Algebra/FreeAlgebra.lean
index 14265d1c780897..0b2da9791eb6ee 100644
--- a/Mathlib/Algebra/FreeAlgebra.lean
+++ b/Mathlib/Algebra/FreeAlgebra.lean
@@ -284,8 +284,6 @@ instance {S : Type _} [CommRing S] : Ring (FreeAlgebra S X) :=
   Algebra.semiringToRing S
 
 -- verify there is no diamond
--- variable (S : Type) [CommSemiring S] in
--- example : (algebraNat : Algebra ℕ (FreeAlgebra R X)) = instAlgebra _ _ := rfl
 variable (S : Type) [CommRing S] in
 example : (algebraInt _ : Algebra ℤ (FreeAlgebra S X)) = instAlgebra _ _ := rfl
 

From 6a0b00282fc12852799d278b2ffdcc878dd517e5 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 23 Jul 2023 16:56:00 +0000
Subject: [PATCH 09/12] fixed

---
 Mathlib/Algebra/RingQuot.lean                  | 13 ++++++++-----
 Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean |  5 +++--
 2 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Algebra/RingQuot.lean b/Mathlib/Algebra/RingQuot.lean
index ce2ca5820574a6..4a9c6d387ec04c 100644
--- a/Mathlib/Algebra/RingQuot.lean
+++ b/Mathlib/Algebra/RingQuot.lean
@@ -155,7 +155,8 @@ namespace RingQuot
 
 variable (r : R → R → Prop)
 
-private irreducible_def natCast (n : ℕ) : RingQuot r :=
+-- can't be irreducible, causes diamonds in ℤ-algebras
+private def natCast (n : ℕ) : RingQuot r :=
   ⟨Quot.mk _ n⟩
 
 private irreducible_def zero : RingQuot r :=
@@ -200,6 +201,9 @@ private irreducible_def npow (n : ℕ) : RingQuot r → RingQuot r
 private def smul [Algebra S R] (n : S) : RingQuot r → RingQuot r
   | ⟨a⟩ => ⟨Quot.map (fun a ↦ n • a) (Rel.smul n) a⟩
 
+instance : NatCast (RingQuot r) :=
+  ⟨natCast r⟩
+
 instance : Zero (RingQuot r) :=
   ⟨zero r⟩
 
@@ -328,8 +332,8 @@ instance instMonoidWithZero (r : R → R → Prop) : MonoidWithZero (RingQuot r)
 
 instance instSemiring (r : R → R → Prop) : Semiring (RingQuot r) where
   natCast := natCast r
-  natCast_zero := by simp [Nat.cast, natCast_def, ← zero_quot]
-  natCast_succ := by simp [Nat.cast, natCast_def, ← one_quot, add_quot]
+  natCast_zero := by simp [Nat.cast, natCast, ← zero_quot]
+  natCast_succ := by simp [Nat.cast, natCast, ← one_quot, add_quot]
   left_distrib := by
     rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟩⟩
     simp only [mul_quot, add_quot, left_distrib]
@@ -373,10 +377,9 @@ instance instRing {R : Type uR} [Ring R] (r : R → R → Prop) : Ring (RingQuot
       simp [smul_quot, neg_quot, add_mul]
     intCast := intCast r
     intCast_ofNat := fun n => congrArg RingQuot.mk <| by
-      rw [natCast_def]
       exact congrArg (Quot.mk _) (Int.cast_ofNat _)
     intCast_negSucc := fun n => congrArg RingQuot.mk <| by
-      simp_rw [neg_def, natCast_def]
+      simp_rw [neg_def]
       exact congrArg (Quot.mk _) (Int.cast_negSucc n) }
 
 instance instCommSemiring {R : Type uR} [CommSemiring R] (r : R → R → Prop) :
diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
index e34dd8206a19ea..b0f54509a3c2bb 100644
--- a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
+++ b/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
@@ -76,6 +76,9 @@ instance instAlgebra {R A M} [CommSemiring R] [AddCommMonoid M] [CommSemiring A]
   Algebra R (TensorAlgebra A M) :=
 RingQuot.instAlgebraRingQuotInstSemiring _
 
+-- verify there is no diamond
+example : (algebraNat : Algebra ℕ (TensorAlgebra R M)) = instAlgebra := rfl
+
 instance {R S A M} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [CommSemiring A]
   [Algebra R A] [Algebra S A] [Module R M] [Module S M] [Module A M]
   [IsScalarTower R A M] [IsScalarTower S A M] [SMulCommClass R S A] :
@@ -97,8 +100,6 @@ instance {S : Type _} [CommRing S] [Module S M] : Ring (TensorAlgebra S M) :=
 variable (S M : Type) [CommRing S] [AddCommGroup M] [Module S M] in
 example : (algebraInt _ : Algebra ℤ (TensorAlgebra S M)) = instAlgebra := rfl
 
--- example : (algebraNat : Algebra ℕ (TensorAlgebra R M)) = instAlgebra := rfl
-
 variable {M}
 
 /-- The canonical linear map `M →ₗ[R] TensorAlgebra R M`.

From 747d39d1763db8d59972ff4e4332a423c78e483a Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 23 Jul 2023 18:24:44 +0000
Subject: [PATCH 10/12] feat(LinearAlgebra/CliffordAlgebra): support towers of
 algebras

---
 .../LinearAlgebra/CliffordAlgebra/Basic.lean  | 24 ++++++++++++++++++-
 1 file changed, 23 insertions(+), 1 deletion(-)

diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
index a7f18be72dcc3a..22f9ee0f0ed9a7 100644
--- a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
+++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
@@ -79,9 +79,31 @@ instance instInhabited : Inhabited (CliffordAlgebra Q) := RingQuot.instInhabited
 #align clifford_algebra.inhabited CliffordAlgebra.instInhabited
 instance instRing : Ring (CliffordAlgebra Q) := RingQuot.instRing _
 #align clifford_algebra.ring CliffordAlgebra.instRing
-instance instAlgebra: Algebra R (CliffordAlgebra Q) := RingQuot.instAlgebraRingQuotInstSemiring _
+
+
+instance instAlgebra {R A M} [CommSemiring R] [AddCommGroup M] [CommRing A]
+    [Algebra R A] [Module R M] [Module A M] (Q : QuadraticForm A M)
+    [IsScalarTower R A M] :
+    Algebra R (CliffordAlgebra Q) :=
+  RingQuot.instAlgebraRingQuotInstSemiring _
 #align clifford_algebra.algebra CliffordAlgebra.instAlgebra
 
+-- verify there are no diamonds
+example : (algebraNat : Algebra ℕ (CliffordAlgebra Q)) = instAlgebra _ := rfl
+example : (algebraInt _ : Algebra ℤ (CliffordAlgebra Q)) = instAlgebra _ := rfl
+
+instance {R S A M} [CommSemiring R] [CommSemiring S] [AddCommGroup M] [CommRing A]
+    [Algebra R A] [Algebra S A] [Module R M] [Module S M] [Module A M] (Q : QuadraticForm A M)
+    [IsScalarTower R A M] [IsScalarTower S A M] [SMulCommClass R S A] :
+    SMulCommClass R S (CliffordAlgebra Q) :=
+  RingQuot.instSMulCommClassRingQuotInstSMulRingQuotInstSMulRingQuot _
+
+instance {R S A M} [CommSemiring R] [CommSemiring S] [AddCommGroup M] [CommRing A]
+    [SMul R S] [Algebra R A] [Algebra S A] [Module R M] [Module S M] [Module A M]
+    [IsScalarTower R A M] [IsScalarTower S A M] [IsScalarTower R S A] (Q : QuadraticForm A M) :
+    IsScalarTower R S (CliffordAlgebra Q) :=
+  RingQuot.instIsScalarTowerRingQuotInstSMulRingQuotInstSMulRingQuot _
+
 /-- The canonical linear map `M →ₗ[R] CliffordAlgebra Q`.
 -/
 def ι : M →ₗ[R] CliffordAlgebra Q :=

From 7994589b420c14f6b78a34f035544405940c19e2 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 23 Jul 2023 18:26:35 +0000
Subject: [PATCH 11/12] fix indents

---
 .../LinearAlgebra/TensorAlgebra/Basic.lean    | 24 +++++++++----------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
index b0f54509a3c2bb..afdaa2c0c75df9 100644
--- a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
+++ b/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
@@ -71,25 +71,25 @@ instance : Semiring (TensorAlgebra R M) := RingQuot.instSemiring _
 -- `IsScalarTower` is not needed, but the instance isn't really canonical without it.
 @[nolint unusedArguments]
 instance instAlgebra {R A M} [CommSemiring R] [AddCommMonoid M] [CommSemiring A]
-  [Algebra R A] [Module R M] [Module A M]
-  [IsScalarTower R A M] :
-  Algebra R (TensorAlgebra A M) :=
-RingQuot.instAlgebraRingQuotInstSemiring _
+    [Algebra R A] [Module R M] [Module A M]
+    [IsScalarTower R A M] :
+    Algebra R (TensorAlgebra A M) :=
+  RingQuot.instAlgebraRingQuotInstSemiring _
 
 -- verify there is no diamond
 example : (algebraNat : Algebra ℕ (TensorAlgebra R M)) = instAlgebra := rfl
 
 instance {R S A M} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [CommSemiring A]
-  [Algebra R A] [Algebra S A] [Module R M] [Module S M] [Module A M]
-  [IsScalarTower R A M] [IsScalarTower S A M] [SMulCommClass R S A] :
-  SMulCommClass R S (TensorAlgebra A M) :=
-RingQuot.instSMulCommClassRingQuotInstSMulRingQuotInstSMulRingQuot _
+    [Algebra R A] [Algebra S A] [Module R M] [Module S M] [Module A M]
+    [IsScalarTower R A M] [IsScalarTower S A M] [SMulCommClass R S A] :
+    SMulCommClass R S (TensorAlgebra A M) :=
+  RingQuot.instSMulCommClassRingQuotInstSMulRingQuotInstSMulRingQuot _
 
 instance {R S A M} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [CommSemiring A]
-  [SMul R S] [Algebra R A] [Algebra S A] [Module R M] [Module S M] [Module A M]
-  [IsScalarTower R A M] [IsScalarTower S A M] [IsScalarTower R S A] :
-  IsScalarTower R S (TensorAlgebra A M) :=
-RingQuot.instIsScalarTowerRingQuotInstSMulRingQuotInstSMulRingQuot _
+    [SMul R S] [Algebra R A] [Algebra S A] [Module R M] [Module S M] [Module A M]
+    [IsScalarTower R A M] [IsScalarTower S A M] [IsScalarTower R S A] :
+    IsScalarTower R S (TensorAlgebra A M) :=
+  RingQuot.instIsScalarTowerRingQuotInstSMulRingQuotInstSMulRingQuot _
 
 namespace TensorAlgebra
 

From 0e3116dac1b75bfb40fa6b45098e8cf79ad0324d Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 23 Jul 2023 20:49:10 +0000
Subject: [PATCH 12/12] add shortcut instance

---
 Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
index 22f9ee0f0ed9a7..760b6668c5c942 100644
--- a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
+++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
@@ -80,17 +80,19 @@ instance instInhabited : Inhabited (CliffordAlgebra Q) := RingQuot.instInhabited
 instance instRing : Ring (CliffordAlgebra Q) := RingQuot.instRing _
 #align clifford_algebra.ring CliffordAlgebra.instRing
 
-
-instance instAlgebra {R A M} [CommSemiring R] [AddCommGroup M] [CommRing A]
+instance (priority := 900) instAlgebra' {R A M} [CommSemiring R] [AddCommGroup M] [CommRing A]
     [Algebra R A] [Module R M] [Module A M] (Q : QuadraticForm A M)
     [IsScalarTower R A M] :
     Algebra R (CliffordAlgebra Q) :=
   RingQuot.instAlgebraRingQuotInstSemiring _
-#align clifford_algebra.algebra CliffordAlgebra.instAlgebra
 
 -- verify there are no diamonds
-example : (algebraNat : Algebra ℕ (CliffordAlgebra Q)) = instAlgebra _ := rfl
-example : (algebraInt _ : Algebra ℤ (CliffordAlgebra Q)) = instAlgebra _ := rfl
+example : (algebraNat : Algebra ℕ (CliffordAlgebra Q)) = instAlgebra' _ := rfl
+example : (algebraInt _ : Algebra ℤ (CliffordAlgebra Q)) = instAlgebra' _ := rfl
+
+-- shortcut instance, as the other instance is slow
+instance instAlgebra : Algebra R (CliffordAlgebra Q) := instAlgebra' _
+#align clifford_algebra.algebra CliffordAlgebra.instAlgebra
 
 instance {R S A M} [CommSemiring R] [CommSemiring S] [AddCommGroup M] [CommRing A]
     [Algebra R A] [Algebra S A] [Module R M] [Module S M] [Module A M] (Q : QuadraticForm A M)