chore(LinearAlgebra/CliffordAlgebra): remove Q := Q (#6780)

The removal of a FunLike instance for `Module.Dual` made these unnecessary.

Author: eric-wieser

Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean

@@ -89,27 +89,24 @@ def reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q :=
           unop_injective <| by simp⟩).toLinearMap
 #align clifford_algebra.reverse CliffordAlgebra.reverse
 
--- porting note: can't infer `Q`
 @[simp]
-theorem reverse_ι (m : M) : reverse (Q := Q) (ι Q m) = ι Q m := by simp [reverse]
+theorem reverse_ι (m : M) : reverse (ι Q m) = ι Q m := by simp [reverse]
 #align clifford_algebra.reverse_ι CliffordAlgebra.reverse_ι
 
 @[simp]
 theorem reverse.commutes (r : R) :
-    -- porting note: can't infer `Q`
-    reverse (Q := Q) (algebraMap R (CliffordAlgebra Q) r) = algebraMap R _ r := by simp [reverse]
+    reverse (algebraMap R (CliffordAlgebra Q) r) = algebraMap R _ r := by simp [reverse]
 #align clifford_algebra.reverse.commutes CliffordAlgebra.reverse.commutes
 
--- porting note: can't infer `Q`
 @[simp]
-theorem reverse.map_one : reverse (Q := Q) (1 : CliffordAlgebra Q) = 1 := by
+theorem reverse.map_one : reverse (1 : CliffordAlgebra Q) = 1 := by
   convert reverse.commutes (Q := Q) (1 : R) <;> simp
 #align clifford_algebra.reverse.map_one CliffordAlgebra.reverse.map_one
 
 @[simp]
 theorem reverse.map_mul (a b : CliffordAlgebra Q) :
   -- porting note: can't infer `Q`
-  reverse (Q := Q) (a * b) = reverse (Q := Q) b * reverse (Q := Q) a := by
+  reverse (a * b) = reverse b * reverse a := by
   simp [reverse]
 #align clifford_algebra.reverse.map_mul CliffordAlgebra.reverse.map_mul
 
@@ -131,9 +128,8 @@ theorem reverse_involutive : Function.Involutive (reverse (Q := Q)) :=
   LinearMap.congr_fun reverse_comp_reverse
 #align clifford_algebra.reverse_involutive CliffordAlgebra.reverse_involutive
 
--- porting note: can't infer `Q`
 @[simp]
-theorem reverse_reverse : ∀ a : CliffordAlgebra Q, reverse (Q := Q) (reverse (Q := Q) a) = a :=
+theorem reverse_reverse : ∀ a : CliffordAlgebra Q, reverse (reverse a) = a :=
   reverse_involutive
 #align clifford_algebra.reverse_reverse CliffordAlgebra.reverse_reverse
 
@@ -162,8 +158,7 @@ theorem reverse_involute_commute : Function.Commute (reverse (Q := Q)) involute
 #align clifford_algebra.reverse_involute_commute CliffordAlgebra.reverse_involute_commute
 
 theorem reverse_involute :
-    -- porting note: can't infer `Q`
-    ∀ a : CliffordAlgebra Q, reverse (Q := Q) (involute a) = involute (reverse (Q := Q) a) :=
+    ∀ a : CliffordAlgebra Q, reverse (involute a) = involute (reverse a) :=
   reverse_involute_commute
 #align clifford_algebra.reverse_involute CliffordAlgebra.reverse_involute
 
@@ -180,7 +175,7 @@ section List
 taking the product of the reverse of that list. -/
 theorem reverse_prod_map_ι :
   -- porting note: can't infer `Q`
-    ∀ l : List M, reverse (Q := Q) (l.map <| ι Q).prod = (l.map <| ι Q).reverse.prod
+    ∀ l : List M, reverse (l.map <| ι Q).prod = (l.map <| ι Q).reverse.prod
   | [] => by simp
   | x::xs => by simp [reverse_prod_map_ι xs]
 #align clifford_algebra.reverse_prod_map_ι CliffordAlgebra.reverse_prod_map_ι
@@ -316,7 +311,7 @@ theorem involute_mem_evenOdd_iff {x : CliffordAlgebra Q} {n : ZMod 2} :
 @[simp]
 theorem reverse_mem_evenOdd_iff {x : CliffordAlgebra Q} {n : ZMod 2} :
     -- porting note: cannot infer `Q`
-    reverse (Q := Q) x ∈ evenOdd Q n ↔ x ∈ evenOdd Q n :=
+    reverse x ∈ evenOdd Q n ↔ x ∈ evenOdd Q n :=
   SetLike.ext_iff.mp (evenOdd_comap_reverse Q n) x
 #align clifford_algebra.reverse_mem_even_odd_iff CliffordAlgebra.reverse_mem_evenOdd_iff
 

Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean

@@ -114,8 +114,8 @@ def contractRight : CliffordAlgebra Q →ₗ[R] Module.Dual R M →ₗ[R] Cliffo
 #align clifford_algebra.contract_right CliffordAlgebra.contractRight
 
 theorem contractRight_eq (x : CliffordAlgebra Q) :
-    contractRight (Q := Q) x d = reverse (Q := Q)
-    (contractLeft (R := R) (M := M) d <| reverse (Q := Q) x) :=
+    contractRight (Q := Q) x d = reverse
+    (contractLeft (R := R) (M := M) d <| reverse x) :=
   rfl
 #align clifford_algebra.contract_right_eq CliffordAlgebra.contractRight_eq
 

Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean

@@ -241,7 +241,7 @@ def equivEven : CliffordAlgebra Q ≃ₐ[R] CliffordAlgebra.even (Q' Q) :=
 /-- The representation of the clifford conjugate (i.e. the reverse of the involute) in the even
 subalgebra is just the reverse of the representation. -/
 theorem coe_toEven_reverse_involute (x : CliffordAlgebra Q) :
-    ↑(toEven Q (reverse (Q := Q) (involute x))) =
+    ↑(toEven Q (reverse (involute x))) =
       reverse (Q := Q' Q) (toEven Q x : CliffordAlgebra (Q' Q)) := by
   induction x using CliffordAlgebra.induction
   case h_grade0 r => simp only [AlgHom.commutes, Subalgebra.coe_algebraMap, reverse.commutes]

Mathlib/LinearAlgebra/CliffordAlgebra/Fold.lean

@@ -99,15 +99,13 @@ def foldl (f : M →ₗ[R] N →ₗ[R] N) (hf : ∀ m x, f m (f m x) = Q m • x
 
 @[simp]
 theorem foldl_reverse (f : M →ₗ[R] N →ₗ[R] N) (hf) (n : N) (x : CliffordAlgebra Q) :
-    -- porting note: cannot infer `Q`
-    foldl Q f hf n (reverse (Q := Q) x) = foldr Q f hf n x :=
+    foldl Q f hf n (reverse x) = foldr Q f hf n x :=
   FunLike.congr_arg (foldr Q f hf n) <| reverse_reverse _
 #align clifford_algebra.foldl_reverse CliffordAlgebra.foldl_reverse
 
 @[simp]
 theorem foldr_reverse (f : M →ₗ[R] N →ₗ[R] N) (hf) (n : N) (x : CliffordAlgebra Q) :
-    -- porting note: cannot infer `Q`
-    foldr Q f hf n (reverse (Q := Q) x) = foldl Q f hf n x :=
+    foldr Q f hf n (reverse x) = foldl Q f hf n x :=
   rfl
 #align clifford_algebra.foldr_reverse CliffordAlgebra.foldr_reverse
 

Mathlib/LinearAlgebra/CliffordAlgebra/Star.lean

@@ -34,20 +34,17 @@ variable {Q : QuadraticForm R M}
 namespace CliffordAlgebra
 
 instance instStarRing : StarRing (CliffordAlgebra Q) where
-  -- porting note: cannot infer `Q`
-  star x := reverse (Q := Q) (involute x)
+  star x := reverse (involute x)
   star_involutive x := by
     simp only [reverse_involute_commute.eq, reverse_reverse, involute_involute]
   star_mul x y := by simp only [map_mul, reverse.map_mul]
   star_add x y := by simp only [map_add]
 
--- porting note: cannot infer `Q`
-theorem star_def (x : CliffordAlgebra Q) : star x = reverse (Q := Q) (involute x) :=
+theorem star_def (x : CliffordAlgebra Q) : star x = reverse (involute x) :=
   rfl
 #align clifford_algebra.star_def CliffordAlgebra.star_def
 
--- porting note: cannot infer `Q`
-theorem star_def' (x : CliffordAlgebra Q) : star x = involute (reverse (Q := Q) x) :=
+theorem star_def' (x : CliffordAlgebra Q) : star x = involute (reverse x) :=
   reverse_involute _
 #align clifford_algebra.star_def' CliffordAlgebra.star_def'