Minor: fix some build linter issues (#326)

Two very minor changes that resolve some linter warnings which occur during the build.
teorth · Oct 5, 2024 · 45aa093 · 45aa093
1 parent 35e22b0
commit 45aa093
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/equational_theories/CentralGroupoids.lean b/equational_theories/CentralGroupoids.lean
@@ -36,8 +36,8 @@ def MagmaA2 : Magma (Fin 3 × Fin 3) where
   op (p1 p2 : Fin 3 × Fin 3) : Fin 3 × Fin 3 :=
   match p1, p2 with
   | (a, b), (⟨0, _⟩, _) => (MagmaA21.op a b, ⟨0, by decide⟩)
-  | (a, b), (c, ⟨0, _⟩) => (b, MagmaA21.op b c)
-  | (a, b), (c, d)     => (b, c)
+  | (_, b), (c, ⟨0, _⟩) => (b, MagmaA21.op b c)
+  | (_, b), (c, _)     => (b, c)
 
 /-- A magma isomorphic to A2, given as an optable. -/
 def MagmaA2T : Magma (Fin 9) where

diff --git a/equational_theories/InfModel.lean b/equational_theories/InfModel.lean
@@ -76,7 +76,7 @@ theorem Equation374794_not_implies_Equation2 : ∃ (G : Type) (_ : Magma G), Equ
     · apply ne_of_lt
       simp only [← PNat.coe_lt_coe, PNat.val_ofNat, PNat.pow_coe]
       apply lt_self_pow (by simp)
-      apply one_lt_pow (by simp) (by simp)
+      apply one_lt_pow₀ (by simp) (by simp)
     · trivial
   simp only [Ne.symm hx, ↓reduceIte, PNat.pow_coe, PNat.val_ofNat, padicValNat.prime_pow,
     PNat.coe_toPNat']