From a907e0d06192d385f7cddef2bce22cb2d584ec80 Mon Sep 17 00:00:00 2001
From: matzemathics <60295901+matzemathics@users.noreply.github.com>
Date: Fri, 19 Apr 2024 14:18:13 +0000
Subject: [PATCH] Update FormalSystems/Preliminaries/Language.lean

---
 FormalSystems/Preliminaries/Language.lean | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/FormalSystems/Preliminaries/Language.lean b/FormalSystems/Preliminaries/Language.lean
index fe3cb80..443bf0e 100644
--- a/FormalSystems/Preliminaries/Language.lean
+++ b/FormalSystems/Preliminaries/Language.lean
@@ -234,11 +234,8 @@ theorem Sigma.kleene_contains_all : ∀(w : Word α), w ∈ (Σ)∗
   | [] => by exists 0
   | x::xs => by
     have ⟨n, hn⟩ := Sigma.kleene_contains_all xs
-    exists (n + 1)
-    rw [pow_succ] 
-    conv => right; right; rw [← pow_one (Σ)]
-    rw [npow_mul_comm]
-    simp
+    exists (1 + n)
+    simp [pow_add]
     exists [x]
     exists xs