From 7844b2a0a6019b3feeb6cde892447b644a3aaa77 Mon Sep 17 00:00:00 2001
From: Terence Tao <tao@math.ucla.edu>
Date: Thu, 26 Sep 2024 10:49:21 -0700
Subject: [PATCH] more renaming

---
 equational_theories/Basic.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/equational_theories/Basic.lean b/equational_theories/Basic.lean
index f6316439..d2728607 100644
--- a/equational_theories/Basic.lean
+++ b/equational_theories/Basic.lean
@@ -83,7 +83,7 @@ theorem Equation1_true (G: Type*) [Magma G] : Equation1 G :=
 
 /- Counterexamples -/
 
-theorem Equation46_not_implies_Equation3 : ∃ (G: Type) (_: Magma G), Equation46 G ∧ ¬ Equation4 G := by
+theorem Equation46_not_implies_Equation4 : ∃ (G: Type) (_: Magma G), Equation46 G ∧ ¬ Equation4 G := by
   let hG : Magma Nat := {
     op := fun _ _ => 0
   }
@@ -96,7 +96,7 @@ theorem Equation46_not_implies_Equation3 : ∃ (G: Type) (_: Magma G), Equation4
   dsimp [hG] at h
   linarith
 
-theorem Equation3_not_implies_Equation4582 : ∃ (G: Type) (_: Magma G), Equation4 G ∧ ¬ Equation4582 G := by
+theorem Equation4_not_implies_Equation4582 : ∃ (G: Type) (_: Magma G), Equation4 G ∧ ¬ Equation4582 G := by
   let hG : Magma Nat := {
     op := fun x _ => x
   }
@@ -109,7 +109,7 @@ theorem Equation3_not_implies_Equation4582 : ∃ (G: Type) (_: Magma G), Equatio
   dsimp [hG] at h
   linarith
 
-theorem Equation3_not_implies_Equation43 : ∃ (G: Type) (_: Magma G), Equation4 G ∧ ¬ Equation43 G := by
+theorem Equation4_not_implies_Equation43 : ∃ (G: Type) (_: Magma G), Equation4 G ∧ ¬ Equation43 G := by
   let hG : Magma Nat := {
     op := fun x _ => x
   }