From aab08fbc381a9b26b4e2d5dcaa4a8d3bc195e1c7 Mon Sep 17 00:00:00 2001
From: Felix Cherubini <felix.cherubini@posteo.de>
Date: Wed, 7 Feb 2024 11:01:40 +0100
Subject: [PATCH] simplify

---
 Cubical/Algebra/Ring/Quotient.agda               |  1 -
 Cubical/Algebra/ZariskiLattice/Base.agda         |  1 -
 .../Algebra/ZariskiLattice/StructureSheaf.agda   | 12 +++---------
 .../ZariskiLattice/StructureSheafPullback.agda   | 16 +++-------------
 .../ZariskiLattice/UniversalProperty.agda        |  1 -
 5 files changed, 6 insertions(+), 25 deletions(-)

diff --git a/Cubical/Algebra/Ring/Quotient.agda b/Cubical/Algebra/Ring/Quotient.agda
index 587050d8ac..a8ce89ad88 100644
--- a/Cubical/Algebra/Ring/Quotient.agda
+++ b/Cubical/Algebra/Ring/Quotient.agda
@@ -18,7 +18,6 @@ open import Cubical.HITs.SetQuotients.Properties
 open import Cubical.Algebra.Ring
 open import Cubical.Algebra.Ring.Ideal
 open import Cubical.Algebra.Ring.Kernel
-open import Cubical.Tactics.CommRingSolver
 
 private
   variable
diff --git a/Cubical/Algebra/ZariskiLattice/Base.agda b/Cubical/Algebra/ZariskiLattice/Base.agda
index 92720354c6..06bb4f7909 100644
--- a/Cubical/Algebra/ZariskiLattice/Base.agda
+++ b/Cubical/Algebra/ZariskiLattice/Base.agda
@@ -33,7 +33,6 @@ open import Cubical.Algebra.CommRing.Ideal
 open import Cubical.Algebra.CommRing.Ideal.Sum
 open import Cubical.Algebra.CommRing.FGIdeal
 open import Cubical.Algebra.CommRing.RadicalIdeal
-open import Cubical.Tactics.CommRingSolver
 open import Cubical.Algebra.Semilattice
 open import Cubical.Algebra.Lattice
 open import Cubical.Algebra.DistLattice
diff --git a/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda b/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda
index b43bd3de6b..78f2aca287 100644
--- a/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda
+++ b/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda
@@ -304,10 +304,7 @@ module _ {ℓ : Level} (R' : CommRing ℓ) where
           instance
            h⁻ᵐ : (h ^ m) /1 ∈ₚ (R[1/ h ]AsCommRing ˣ)
            h⁻ᵐ = [ 1r , h ^ m , ∣ m , refl ∣₁ ]
-               , eq/ _ _ ((1r , containsOne) , path (h ^ m))
-            where
-            path : ∀ x → 1r · (x · 1r) · 1r ≡ 1r · 1r · (1r · x)
-            path _ = solve! R'
+               , eq/ _ _ ((1r , containsOne) , solve! R')
 
           β : FinVec R[1/ h ] (suc n)
           β i = ((h ^ m) /1) ⁻¹ · α i /1
@@ -360,12 +357,9 @@ module _ {ℓ : Level} (R' : CommRing ℓ) where
       pres1 (snd (coneOut /1/1Cone (pair i j i<j))) = refl
       pres+ (snd (coneOut /1/1Cone (pair i j i<j))) x y =
         cong [_] (≡-× (cong [_] (≡-×
-                      (cong₂ _+_ (useSolver x) (useSolver y))
-                      (Σ≡Prop (λ _ → isPropPropTrunc) (useSolver 1r))))
+                      (cong₂ _+_ (solve! R') (solve! R'))
+                      (Σ≡Prop (λ _ → isPropPropTrunc) (solve! R'))))
                       (Σ≡Prop (λ _ → isPropPropTrunc) (sym (·IdR 1r))))
-        where
-        useSolver : ∀ a → a ≡ a · 1r · (1r · 1r)
-        useSolver _ = solve! R'
       pres· (snd (coneOut /1/1Cone (pair i j i<j))) x y =
         cong [_] (≡-× (cong [_] (≡-× refl
                       (Σ≡Prop (λ _ → isPropPropTrunc) (sym (·IdR 1r)))))
diff --git a/Cubical/Algebra/ZariskiLattice/StructureSheafPullback.agda b/Cubical/Algebra/ZariskiLattice/StructureSheafPullback.agda
index 3104a95f09..a01e5d6971 100644
--- a/Cubical/Algebra/ZariskiLattice/StructureSheafPullback.agda
+++ b/Cubical/Algebra/ZariskiLattice/StructureSheafPullback.agda
@@ -314,16 +314,9 @@ module _ (R' : CommRing ℓ) where
         path = eq/ _ _ ((1r , ∣ 0 , refl ∣₁) , bigPath)
              ∙ cong (β zero · (f /1) +_) (sym (+IdR (β (suc zero) · (g /1))))
          where
-         useSolver1 : ∀ hn → 1r · 1r · ((hn · 1r) · (hn · 1r)) ≡ hn · hn
-         useSolver1 _ = solve! R'
-
-         useSolver2 : ∀ az f hn as g → hn · (az · f + (as · g + 0r))
-                                      ≡ 1r · (az · f · (hn · 1r) + as · g · (hn · 1r)) · 1r
-         useSolver2 _ _ _ _ _ = solve! R'
-
          bigPath : 1r · 1r · ((h ^ n · 1r) · (h ^ n · 1r))
                  ≡ 1r · (α zero · f · (h ^ n · 1r) + α (suc zero) · g · (h ^ n · 1r)) · 1r
-         bigPath = useSolver1 (h ^ n) ∙ cong (h ^ n ·_) p ∙ useSolver2 _ _ _ _ _
+         bigPath = solve! R' ∙ cong (h ^ n ·_) p ∙ solve! R'
 
     {-
 
@@ -371,12 +364,9 @@ module _ (R' : CommRing ℓ) where
     pres0 (snd /1/1AsCommRingHomFG) = refl
     pres1 (snd /1/1AsCommRingHomFG) = refl
     pres+ (snd /1/1AsCommRingHomFG) x y = cong [_] (≡-× (cong [_] (≡-×
-                                         (cong₂ _+_ (useSolver x) (useSolver y))
-                                         (Σ≡Prop (λ _ → isPropPropTrunc) (useSolver 1r))))
+                                         (cong₂ _+_ (solve! R') (solve! R'))
+                                         (Σ≡Prop (λ _ → isPropPropTrunc) (solve! R'))))
                                          (Σ≡Prop (λ _ → isPropPropTrunc) (sym (·IdR 1r))))
-      where
-      useSolver : ∀ a → a ≡ a · 1r · (1r · 1r)
-      useSolver _ = solve! R'
     pres· (snd /1/1AsCommRingHomFG) x y = cong [_] (≡-× (cong [_] (≡-× refl
                                             (Σ≡Prop (λ _ → isPropPropTrunc) (sym (·IdR 1r)))))
                                             (Σ≡Prop (λ _ → isPropPropTrunc) (sym (·IdR 1r))))
diff --git a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda b/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda
index 72d15765ce..3983ab834e 100644
--- a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda
+++ b/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda
@@ -33,7 +33,6 @@ open import Cubical.Algebra.CommRing.BinomialThm
 open import Cubical.Algebra.CommRing.Ideal
 open import Cubical.Algebra.CommRing.FGIdeal
 open import Cubical.Algebra.CommRing.RadicalIdeal
-open import Cubical.Tactics.CommRingSolver
 open import Cubical.Algebra.Semilattice
 open import Cubical.Algebra.Lattice
 open import Cubical.Algebra.DistLattice