wait-for-type, simplify

agda · Feb 6, 2024 · c7f6277 · c7f6277
1 parent 33f40fc
commit c7f6277
Show file tree

Hide file tree

Showing 12 changed files with 30 additions and 134 deletions.
diff --git a/Cubical/Algebra/CommAlgebra/Instances/Unit.agda b/Cubical/Algebra/CommAlgebra/Instances/Unit.agda
@@ -49,16 +49,11 @@ module _ (R : CommRing ℓ) where
 
       1≡0→isContr : isContr ⟨ A ⟩
       1≡0→isContr = 0a , λ a →
-        0a      ≡⟨ step1 a ⟩
+        0a      ≡⟨ solve! S ⟩
         a · 0a  ≡⟨ cong (λ b → a · b) (sym 1≡0) ⟩
-        a · 1a  ≡⟨ step2 a ⟩
+        a · 1a  ≡⟨ solve! S ⟩
         a       ∎
           where S = CommAlgebra→CommRing A
-                open CommRingStr (snd S) renaming (_·_ to _·s_)
-                step1 : (x : ⟨ A ⟩) → 0r ≡ x ·s 0r
-                step1 x = solve! S
-                step2 : (x : ⟨ A ⟩) → x ·s 1r ≡ x
-                step2 x = solve! S
 
       equivFrom1≡0 : CommAlgebraEquiv A UnitCommAlgebra
       equivFrom1≡0 = isContr→Equiv 1≡0→isContr isContrUnit*  ,

diff --git a/Cubical/Algebra/CommAlgebra/Localisation.agda b/Cubical/Algebra/CommAlgebra/Localisation.agda
@@ -308,10 +308,7 @@ module DoubleAlgLoc (R : CommRing ℓ) (f g : (fst R)) where
      helper2 : (α : FinVec (fst R) 1)
              → x ^ n ≡ linearCombination R α (replicateFinVec 1 y)
              → x ∈ᵢ √ ⟨ y · x ⟩
-     helper2 α p = ∣ (suc n) , ∣ α , cong (x ·_) p ∙ useSolver x y (α zero) ∣₁ ∣₁
-      where
-      useSolver : ∀ x y a → x · (a · y + 0r) ≡ a · (y · x) + 0r
-      useSolver _ _ _ = solve! R
+     helper2 α p = ∣ (suc n) , ∣ α , cong (x ·_) p ∙ solve! R ∣₁ ∣₁
 
   toUnit2 : ∀ s → s ∈ [_ⁿ|n≥0] R g → s ⋆ 1a ∈ R[1/fg]ˣ
   toUnit2 s s∈[gⁿ|n≥0] = subst-∈ R[1/fg]ˣ (sym (·IdR (s /1ᶠᵍ)))

diff --git a/Cubical/Algebra/CommAlgebra/LocalisationAlgebra.agda b/Cubical/Algebra/CommAlgebra/LocalisationAlgebra.agda
@@ -28,8 +28,6 @@ open import Cubical.Algebra.CommRing as CommRing hiding (_ˣ;module Units)
 open import Cubical.Algebra.CommRing.Localisation using (isMultClosedSubset)
 open import Cubical.Algebra.Ring
 
-open import Cubical.Tactics.CommRingSolver
-
 module Cubical.Algebra.CommAlgebra.LocalisationAlgebra
   {ℓR : Level}
   (R : CommRing ℓR)

diff --git a/Cubical/Algebra/CommAlgebra/QuotientAlgebra.agda b/Cubical/Algebra/CommAlgebra/QuotientAlgebra.agda
@@ -242,8 +242,6 @@ module _
     unfolding quotientHom
 
     isZeroFromIdeal : (x : ⟨ A ⟩) → x ∈ (fst I) → fst (quotientHom A I) x ≡ CommAlgebraStr.0a (snd (A / I))
-    isZeroFromIdeal x x∈I = eq/ x 0a (subst (_∈ fst I) (step x) x∈I )
+    isZeroFromIdeal x x∈I = eq/ x 0a (subst (_∈ fst I) (solve! (CommAlgebra→CommRing A)) x∈I )
       where
         open CommAlgebraStr (snd A)
-        step : (x : ⟨ A ⟩) → x ≡ x - 0a
-        step x = solve! (CommAlgebra→CommRing A)
diff --git a/Cubical/Algebra/CommRing/BinomialThm.agda b/Cubical/Algebra/CommRing/BinomialThm.agda
@@ -85,20 +85,14 @@ module BinomialThm (R' : CommRing ℓ) where
   xVec : FinVec R (suc n)
   xVec i = (n choose (toℕ i)) · x ^ (suc (toℕ i)) · y ^ (n ∸ toℕ i)
 
-  solve1 : ∀ x nci xⁱ yⁿ⁻ⁱ → x · (nci · xⁱ · yⁿ⁻ⁱ) ≡ nci · (x · xⁱ) · yⁿ⁻ⁱ
-  solve1 x nci xⁱ yⁿ⁻ⁱ = solve! R'
-
   xVecPath : ∀ (i : Fin (suc n)) → x · ((n choose (toℕ i)) · x ^ (toℕ i) · y ^ (n ∸ toℕ i)) ≡ xVec i
-  xVecPath i = solve1 _ _ _ _
+  xVecPath i = solve! R'
 
   yVec : FinVec R (suc n)
   yVec i = (n choose (toℕ i)) · x ^ (toℕ i) · y ^ (suc (n ∸ toℕ i))
 
-  solve2 : ∀ y nci xⁱ yⁿ⁻ⁱ → y · (nci · xⁱ · yⁿ⁻ⁱ) ≡ nci · xⁱ · (y · yⁿ⁻ⁱ)
-  solve2 y nci xⁱ yⁿ⁻ⁱ = solve! R'
-
   yVecPath : ∀ (i : Fin (suc n)) → y · ((n choose (toℕ i)) · x ^ (toℕ i) · y ^ (n ∸ toℕ i)) ≡ yVec i
-  yVecPath i = solve2 _ _ _ _
+  yVecPath i = solve! R'
 
   xⁿ⁺¹ : R
   xⁿ⁺¹ = xVec (fromℕ n)
@@ -122,11 +116,8 @@ module BinomialThm (R' : CommRing ℓ) where
    + (n choose suc (weakenRespToℕ i j)) · (x · x ^ (weakenRespToℕ i j)) · sym yHelper j
    ≡ ((n choose suc (toℕ (weakenFin i))) + (n choose toℕ (weakenFin i)))
    · (x · x ^ toℕ (weakenFin i)) · y ^ (n ∸ toℕ (weakenFin i)))
-   (solve4 _ _ _ _)
+   (solve! R')
    where
    yHelper : (y · y ^ (n ∸ suc (toℕ i))) ≡ y ^ (n ∸ toℕ (weakenFin i))
    yHelper = cong (λ m → y · y ^ (n ∸ suc m)) (sym (weakenRespToℕ i))
            ∙ cong (y ^_) (≤-∸-suc (subst (λ m → suc m ≤ n) (sym (weakenRespToℕ _)) (toℕ<n i)))
-
-   solve4 : ∀ nci ncsi xxⁱ yⁿ⁻ⁱ → nci · xxⁱ · yⁿ⁻ⁱ + ncsi · xxⁱ · yⁿ⁻ⁱ ≡ (ncsi + nci) · xxⁱ · yⁿ⁻ⁱ
-   solve4 nci ncsi xxⁱ yⁿ⁻ⁱ = solve! R'
diff --git a/Cubical/Algebra/CommRing/Ideal/Base.agda b/Cubical/Algebra/CommRing/Ideal/Base.agda
@@ -82,9 +82,7 @@ module CommIdeal (R' : CommRing ℓ) where
 
  -Closed : (I : CommIdeal) (x : R)
          → x ∈ I → (- x) ∈ I
- -Closed I x x∈I = subst (_∈ I) useSolver (·Closed (snd I) (- 1r) x∈I)
-   where useSolver : - 1r · x ≡ - x
-         useSolver = solve! R'
+ -Closed I x x∈I = subst (_∈ I) (solve! R') (·Closed (snd I) (- 1r) x∈I)
 
  ∑Closed : (I : CommIdeal) {n : ℕ} (V : FinVec R n)
          → (∀ i → V i ∈ I) → ∑ V ∈ I
@@ -129,10 +127,8 @@ module _ {R : CommRing ℓ} where
   CommIdeal→Ideal : IdealsIn R → IdealsInRing (CommRing→Ring R)
   fst (CommIdeal→Ideal I) = fst I
   +-closed (snd (CommIdeal→Ideal I)) = +Closed (snd I)
-  -closed (snd (CommIdeal→Ideal I)) =  λ x∈pI → subst-∈p (fst I) (useSolver _)
+  -closed (snd (CommIdeal→Ideal I)) =  λ x∈pI → subst-∈p (fst I) (solve! R)
                                                            (·Closed (snd I) (- 1r) x∈pI)
-                                         where useSolver : (x : fst R) → - 1r · x ≡ - x
-                                               useSolver _ = solve! R
   0r-closed (snd (CommIdeal→Ideal I)) = contains0 (snd I)
   ·-closedLeft (snd (CommIdeal→Ideal I)) = ·Closed (snd I)
   ·-closedRight (snd (CommIdeal→Ideal I)) = λ r x∈pI →

diff --git a/Cubical/Algebra/CommRing/LocalRing.agda b/Cubical/Algebra/CommRing/LocalRing.agda
@@ -123,10 +123,7 @@ module _ (R : CommRing ℓ) where
     +Closed nonInvertiblesFormIdeal {x = x} {y = y} xNonInv yNonInv x+yInv =
       ∥_∥₁.rec isProp⊥ (⊎.rec xNonInv yNonInv) (invertibleInBinarySum x+yInv)
     contains0 nonInvertiblesFormIdeal (x , 0x≡1) =
-      1≢0 (sym 0x≡1 ∙ useSolver)
-      where
-        useSolver : 0r · x ≡ 0r
-        useSolver = solve! R
+      1≢0 (sym 0x≡1 ∙ solve! R)
     ·Closed nonInvertiblesFormIdeal {x = x} r xNonInv rxInv =
       xNonInv (snd (RˣMultDistributing r x rxInv))
 
@@ -205,11 +202,8 @@ module _ (R : CommRing ℓ) where
       private
         binSum→OneMinus : BinSum.BinSum → OneMinus
         binSum→OneMinus binSum x =
-          binSum x (1r - x) (subst (_∈ R ˣ) (1≡x+1-x) RˣContainsOne)
-          where
-          1≡x+1-x : 1r ≡ x + (1r - x)
-          1≡x+1-x = solve! R
-          open Units R
+          binSum x (1r - x) (subst (_∈ R ˣ) (solve! R) RˣContainsOne)
+          where open Units R
 
         oneMinus→BinSum : OneMinus → BinSum.BinSum
         oneMinus→BinSum oneMinus x y (s⁻¹ , ss⁻¹≡1) =
@@ -219,12 +213,10 @@ module _ (R : CommRing ℓ) where
               (fst ∘ RˣMultDistributing y s⁻¹ ∘ subst (_∈ R ˣ) 1-xs⁻¹≡ys⁻¹))
             (oneMinus (x · s⁻¹))
           where
-          solveStep : (a b c : ⟨ R ⟩) → (a + b) · c - a · c ≡ b · c
-          solveStep _ _ _ = solve! R
           1-xs⁻¹≡ys⁻¹ : 1r - x · s⁻¹ ≡ y · s⁻¹
           1-xs⁻¹≡ys⁻¹ =
             (1r - x · s⁻¹)             ≡⟨ cong (_- _) (sym ss⁻¹≡1) ⟩
-            ((x + y) · s⁻¹ - x · s⁻¹)  ≡⟨ solveStep x y s⁻¹ ⟩
+            ((x + y) · s⁻¹ - x · s⁻¹)  ≡⟨ solve! R ⟩
             (y · s⁻¹)                  ∎
           open Units R
 

diff --git a/Cubical/Algebra/CommRing/Localisation/Base.agda b/Cubical/Algebra/CommRing/Localisation/Base.agda
@@ -131,11 +131,7 @@ module Loc (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultCl
   where
   +ₗ-assoc[] : (a b c : R × S) → [ a ] +ₗ ([ b ] +ₗ [ c ]) ≡ ([ a ] +ₗ [ b ]) +ₗ [ c ]
   +ₗ-assoc[] (r , s , s∈S) (r' , s' , s'∈S) (r'' , s'' , s''∈S) =
-     cong [_] (ΣPathP ((path r s r' s' r'' s'') , Σ≡Prop (λ x → ∈-isProp S' x) (·Assoc _ _ _)))
-     where
-     path : (r s r' s' r'' s'' : R)
-          → r · (s' · s'') + (r' · s'' + r'' · s') · s ≡ (r · s' + r' · s) · s'' + r'' · (s · s')
-     path r s r' s' r'' s'' = solve! R'
+     cong [_] (ΣPathP ((solve! R') , Σ≡Prop (λ x → ∈-isProp S' x) (·Assoc _ _ _)))
 
  0ₗ : S⁻¹R
  0ₗ = [ 0r , 1r , SMultClosedSubset .containsOne ]
@@ -146,13 +142,10 @@ module Loc (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultCl
   +ₗ-rid[] : (a : R × S) → [ a ] +ₗ 0ₗ ≡ [ a ]
   +ₗ-rid[] (r , s , s∈S) = path
    where
-   eq1 : (r s : R) → r · 1r + 0r · s ≡ r
-   eq1 r s = solve! R'
-
    path : [ r · 1r + 0r · s , s · 1r , SMultClosedSubset .multClosed s∈S
                                       (SMultClosedSubset .containsOne) ]
         ≡ [ r , s , s∈S ]
-   path = cong [_] (ΣPathP (eq1 r s , Σ≡Prop (λ x → ∈-isProp S' x) (·IdR _)))
+   path = cong [_] (ΣPathP (solve! R' , Σ≡Prop (λ x → ∈-isProp S' x) (·IdR _)))
 
  -ₗ_ : S⁻¹R → S⁻¹R
  -ₗ_ = SQ.rec squash/ -ₗ[] -ₗWellDef
@@ -163,23 +156,14 @@ module Loc (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultCl
   -ₗWellDef : (a b : R × S) → a ≈ b → -ₗ[] a ≡ -ₗ[] b
   -ₗWellDef (r , s , _) (r' , s' , _) ((u , u∈S) , p) = eq/ _ _ ((u , u∈S) , path)
    where
-   eq1 : (u r s' : R) → u · - r · s' ≡ - (u · r · s')
-   eq1 u r s' = solve! R'
-
-   eq2 : (u r' s : R) → - (u · r' · s) ≡ u · - r' · s
-   eq2 u r' s = solve! R'
-
    path : u · - r · s' ≡ u · - r' · s
-   path = eq1 u r s' ∙∙ cong -_ p ∙∙ eq2 u r' s
+   path = (solve! R') ∙∙ cong -_ p ∙∙ (solve! R')
 
  +ₗ-rinv : (x : S⁻¹R) → x +ₗ (-ₗ x) ≡ 0ₗ
  +ₗ-rinv = SQ.elimProp (λ _ → squash/ _ _) +ₗ-rinv[]
   where
   +ₗ-rinv[] : (a : R × S) → ([ a ] +ₗ (-ₗ [ a ])) ≡ 0ₗ
-  +ₗ-rinv[] (r , s , s∈S) = eq/ _ _ ((1r , SMultClosedSubset .containsOne) , path r s)
-   where
-   path : (r s : R) → 1r · (r · s + - r · s) · 1r ≡ 1r · 0r · (s · s)
-   path r s = solve! R'
+  +ₗ-rinv[] (r , s , s∈S) = eq/ _ _ ((1r , SMultClosedSubset .containsOne) , solve! R')
 
  +ₗ-comm : (x y : S⁻¹R) → x +ₗ y ≡ y +ₗ x
  +ₗ-comm = SQ.elimProp2 (λ _ _ → squash/ _ _) +ₗ-comm[]
@@ -205,16 +189,8 @@ module Loc (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultCl
   θ : (a a' b : R × S) → a ≈ a' → (a ·ₚ b) ≈ (a' ·ₚ b)
   θ (r₁ , s₁ , s₁∈S) (r'₁ , s'₁ , s'₁∈S) (r₂ , s₂ , s₂∈S) ((s , s∈S) , p) = (s , s∈S) , path
    where
-   eq1 : (r₁ s₁ r'₁ s'₁ r₂ s₂ s : R)
-       → s · (r₁ · r₂) · (s'₁ · s₂) ≡ s · r₁ · s'₁ · r₂ · s₂
-   eq1 r₁ s₁ r'₁ s'₁ r₂ s₂ s = solve! R'
-
-   eq2 : (r₁ s₁ r'₁ s'₁ r₂ s₂ s : R)
-       → s · r'₁ · s₁ · r₂ · s₂ ≡ s · (r'₁ · r₂) · (s₁ · s₂)
-   eq2 r₁ s₁ r'₁ s'₁ r₂ s₂ s = solve! R'
-
    path : s · (r₁ · r₂) · (s'₁ · s₂) ≡ s · (r'₁ · r₂) · (s₁ · s₂)
-   path = eq1 r₁ s₁ r'₁ s'₁ r₂ s₂ s ∙∙ cong (λ x → x · r₂ · s₂) p ∙∙ eq2 r₁ s₁ r'₁ s'₁ r₂ s₂ s
+   path = solve! R' ∙∙ cong (λ x → x · r₂ · s₂) p ∙∙ solve! R'
 
 
  -- checking laws for multiplication
@@ -240,13 +216,7 @@ module Loc (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultCl
    where
    ·ₗ-rdist-+ₗ[] : (a b c : R × S) → [ a ] ·ₗ ([ b ] +ₗ [ c ]) ≡ ([ a ] ·ₗ [ b ]) +ₗ ([ a ] ·ₗ [ c ])
    ·ₗ-rdist-+ₗ[] (r , s , s∈S) (r' , s' , s'∈S) (r'' , s'' , s''∈S) =
-      eq/ _ _ ((1r , (SMultClosedSubset .containsOne)) , path r s r' s' r'' s'')
-      where
-      -- could be shortened even further
-      path : (r s r' s' r'' s'' : R)
-           → 1r · (r · (r' · s'' + r'' · s')) · (s · s' · (s · s''))
-           ≡ 1r · (r · r' · (s · s'') + r · r'' · (s · s')) · (s · (s' · s''))
-      path r s r' s' r'' s'' = solve! R'
+      eq/ _ _ ((1r , (SMultClosedSubset .containsOne)) , solve! R')
 
  ·ₗ-comm : (x y : S⁻¹R) → x ·ₗ y ≡ y ·ₗ x
  ·ₗ-comm = SQ.elimProp2 (λ _ _ → squash/ _ _) ·ₗ-comm[]

diff --git a/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda b/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda
@@ -84,10 +84,7 @@ module InvertingElementsBase (R' : CommRing ℓ) where
  isContrR[1/0] : isContr R[1/ 0r ]
  fst isContrR[1/0] = [ 1r , 0r , ∣ 1 , sym (·IdR 0r) ∣₁ ] -- everything is equal to 1/0
  snd isContrR[1/0] = elimProp (λ _ → squash/ _ _)
-                               λ _ → eq/ _ _ ((0r , ∣ 1 , sym (·IdR 0r) ∣₁) , useSolver _ _)
-  where
-  useSolver : ∀ s r → 0r · 1r · s ≡ 0r · r · 0r
-  useSolver _ _ = solve! R'
+                               λ _ → eq/ _ _ ((0r , ∣ 1 , sym (·IdR 0r) ∣₁) , (solve! R'))
 
  R[1/_]AsCommRing : R → CommRing ℓ
  R[1/ f ]AsCommRing = Loc.S⁻¹RAsCommRing R' [ f ⁿ|n≥0] (powersFormMultClosedSubset f)
@@ -316,13 +313,7 @@ module RadicalLemma (R' : CommRing ℓ) (f g : (fst R')) where
   ℕhelper n = PT.rec isPropGoal -- fⁿ≡αg → g⁻¹≡α/fⁿ
        λ (α , p) → [ (α zero) , (f ^ n) , ∣ n , refl ∣₁ ]
                  , eq/ _ _ ((1r , powersFormMultClosedSubset f .containsOne)
-                 , useSolver1 _ _ ∙ sym p ∙ useSolver2 _)
-   where
-   useSolver1 : ∀ x y → 1r · (x · y) · 1r ≡  y · x + 0r
-   useSolver1 _ _ = solve! R'
-
-   useSolver2 : ∀ x → x ≡ 1r · 1r · (1r · x)
-   useSolver2 _ = solve! R'
+                 , (solve! R') ∙ sym p ∙ (solve! R'))
 
  toUnit : f ∈ᵢ √ ⟨ g ⟩
        → ∀ s → s ∈ [ g ⁿ|n≥0] → (s /1) ∈ R[1/ f ]AsCommRing ˣ

diff --git a/Cubical/Algebra/CommRing/Localisation/Limit.agda b/Cubical/Algebra/CommRing/Localisation/Limit.agda
@@ -172,13 +172,8 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
                         , eq/ _ _ ((1r , powersFormMultClosedSubset (f i · f j) .containsOne)
                         , path m)
      where
-     useSolver1 : ∀ a b → 1r · (a · b) · 1r ≡ a · b
-     useSolver1 _ _ = solve! R'
-     useSolver2 : ∀ a → a ≡ (1r · 1r) · (1r · a)
-     useSolver2 _ = solve! R'
-
      path : (n : ℕ) → 1r · (f i ^ n · f j ^ n) · 1r ≡ (1r · 1r) · (1r · ((f i · f j) ^ n))
-     path n = useSolver1 _ _ ∙ sym (^-ldist-· (f i) (f j) n) ∙ useSolver2 _
+     path n = solve! R' ∙ sym (^-ldist-· (f i) (f j) n) ∙ solve! R'
 
  χˡ : (i j : Fin (suc n)) → CommRingHom R[1/ f i ]AsCommRing R[1/ f i · f j ]AsCommRing
  χˡ i j = χˡUnique i j .fst .fst
@@ -194,13 +189,8 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
                         , eq/ _ _ ((1r , powersFormMultClosedSubset (f i · f j) .containsOne)
                         , path m)
      where
-     useSolver1 : ∀ a b → 1r · (a · b) · 1r ≡ b · a
-     useSolver1 _ _ = solve! R'
-     useSolver2 : ∀ a → a ≡ (1r · 1r) · (1r · a)
-     useSolver2 _ = solve! R'
-
      path : (n : ℕ) → 1r · (f j ^ n · f i ^ n) · 1r ≡ (1r · 1r) · (1r · ((f i · f j) ^ n))
-     path n = useSolver1 _ _ ∙ sym (^-ldist-· (f i) (f j) n) ∙ useSolver2 _
+     path n = solve! R' ∙ sym (^-ldist-· (f i) (f j) n) ∙ solve! R'
 
  χʳ : (i j : Fin (suc n)) → CommRingHom R[1/ f j ]AsCommRing R[1/ f i · f j ]AsCommRing
  χʳ i j = χʳUnique i j .fst .fst
@@ -337,7 +327,7 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
 
              r i · f j ^ m · ((f i · f j) ^ m · (f i · f j) ^ l i j)
 
-           ≡⟨ useSolver _ _ _ _ ⟩
+           ≡⟨ solve! R' ⟩
 
              (f i · f j) ^ l i j · r i · f j ^ m · (f i · f j) ^ m
 
@@ -353,16 +343,13 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
 
             (f i · f j) ^ l i j  · r j · f i ^ m · (f i · f j) ^ m
 
-           ≡⟨ sym (useSolver _ _ _ _) ⟩
+           ≡⟨ sym (solve! R') ⟩
 
              r j · f i ^ m · ((f i · f j) ^ m · (f i · f j) ^ l i j)
 
            ≡⟨ cong (r j · f i ^ m ·_) (·-of-^-is-^-of-+ _ _ _) ⟩
 
              r j · f i ^ m · (f i · f j) ^ (m +ℕ l i j) ∎
-           where
-           useSolver : ∀ a b c d → a · b · (c · d) ≡ d · a · b · c
-           useSolver _ _ _ _ = solve! R'
 
          paths : ∀ i j → r i · f j ^ m · (f i · f j) ^ (m +ℕ k)
                         ≡ r j · f i ^ m · (f i · f j) ^ (m +ℕ k)

diff --git a/Cubical/Algebra/CommRing/Localisation/PullbackSquare.agda b/Cubical/Algebra/CommRing/Localisation/PullbackSquare.agda
@@ -131,13 +131,8 @@ module _ (R' : CommRing ℓ) (f g : (fst R')) where
                         , eq/ _ _ ((1r , powersFormMultClosedSubset (f · g) .containsOne)
                         , path n)
     where
-    useSolver1 : ∀ a b → 1r · (a · b) · 1r ≡ a · b
-    useSolver1 _ _ = solve! R'
-    useSolver2 : ∀ a → a ≡ (1r · 1r) · (1r · a)
-    useSolver2 _ = solve! R'
-
     path : (n : ℕ) → 1r · (f ^ n · g ^ n) · 1r ≡ (1r · 1r) · (1r · ((f · g) ^ n))
-    path n = useSolver1 _ _ ∙ sym (^-ldist-· f g n) ∙ useSolver2 _
+    path n = solve! R' ∙ sym (^-ldist-· f g n) ∙ solve! R'
 
   χ₂ : CommRingHom R[1/ g ]AsCommRing R[1/ (f · g) ]AsCommRing
   χ₂ = R[1/g]HasUniversalProp _ /1ᶠᵍAsCommRingHom unitHelper .fst .fst
@@ -148,13 +143,8 @@ module _ (R' : CommRing ℓ) (f g : (fst R')) where
                         , eq/ _ _ ((1r , powersFormMultClosedSubset (f · g) .containsOne)
                               , path n)
     where
-    useSolver1 : ∀ a b → 1r · (a · b) · 1r ≡ b · a
-    useSolver1 _ _ = solve! R'
-    useSolver2 : ∀ a → a ≡ (1r · 1r) · (1r · a)
-    useSolver2 _ = solve! R'
-
     path : (n : ℕ) → 1r · (g ^ n · f ^ n) · 1r ≡ (1r · 1r) · (1r · ((f · g) ^ n))
-    path n = useSolver1 _ _ ∙ sym (^-ldist-· f g n) ∙ useSolver2 _
+    path n = solve! R' ∙ sym (^-ldist-· f g n) ∙ solve! R'
 
 
 
@@ -351,21 +341,11 @@ module _ (R' : CommRing ℓ) (f g : (fst R')) where
       z/1≡x/fⁿ : (z /1ᶠ) ≡ [ x , f ^ n , ∣ n , refl ∣₁ ]
       z/1≡x/fⁿ = eq/ _ _ ((f ^ (n +ℕ m) , ∣ n +ℕ m , refl ∣₁) , path)
        where
-       useSolver1 : ∀ x y α₀ α₁ fⁿ⁺ᵐ gⁿ⁺ᵐ fⁿ
-                  → fⁿ⁺ᵐ · (α₀ · x · fⁿ⁺ᵐ + α₁ · y · gⁿ⁺ᵐ) · fⁿ
-                  ≡ fⁿ⁺ᵐ · (α₀ · x · (fⁿ · fⁿ⁺ᵐ)) + α₁ · (y · fⁿ · (fⁿ⁺ᵐ · gⁿ⁺ᵐ))
-       useSolver1 _ _ _ _ _ _ _ = solve! R'
-
-       useSolver2 : ∀ x α₀ α₁ fⁿ⁺ᵐ g²ⁿ⁺ᵐ f²ⁿ⁺ᵐ
-                  → fⁿ⁺ᵐ · (α₀ · x · f²ⁿ⁺ᵐ) + α₁ · (x · fⁿ⁺ᵐ · g²ⁿ⁺ᵐ)
-                  ≡ fⁿ⁺ᵐ · x · (α₀ · f²ⁿ⁺ᵐ + α₁ · g²ⁿ⁺ᵐ)
-       useSolver2 _ _ _ _ _ _ = solve! R'
-
        path : f ^ (n +ℕ m) · z · f ^ n ≡ f ^ (n +ℕ m) · x · 1r
        path =
            f ^ (n +ℕ m) · z · f ^ n
 
-         ≡⟨ useSolver1 _ _ _ _ _ _ _ ⟩
+         ≡⟨ solve! R' ⟩
 
            f ^ (n +ℕ m) · (α₀ · x · (f ^ n · f ^ (n +ℕ m))) + α₁ · (y · f ^ n · (f ^ (n +ℕ m) · g ^ (n +ℕ m)))
 
@@ -392,7 +372,7 @@ module _ (R' : CommRing ℓ) (f g : (fst R')) where
 
            f ^ (n +ℕ m) · (α₀ · x · (f ^ 2n+m)) + α₁ · (x · f ^ (n +ℕ m) · g ^ 2n+m)
 
-         ≡⟨ useSolver2 _ _ _ _ _ _ ⟩
+         ≡⟨ solve! R' ⟩
 
            f ^ (n +ℕ m) · x · (α₀ · f ^ 2n+m + α₁ · g ^ 2n+m)
 

diff --git a/Cubical/Tactics/CommRingSolver/Reflection.agda b/Cubical/Tactics/CommRingSolver/Reflection.agda
@@ -193,6 +193,7 @@ private
       goal ← inferType hole >>= normalise
       names ← findRingNames commRing
 
+      wait-for-type goal
       just (lhs , rhs) ← get-boundary goal
         where
           nothing