diff --git a/equational_theories/CentralGroupoids.lean b/equational_theories/CentralGroupoids.lean
index 3d2c2714..f543d86b 100644
--- 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
index b3df4461..74fc44a6 100644
--- 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']