diff --git a/Cslib/Computability/Languages/OmegaLanguage.lean b/Cslib/Computability/Languages/OmegaLanguage.lean
index 679a0297..a761e718 100644
--- a/Cslib/Computability/Languages/OmegaLanguage.lean
+++ b/Cslib/Computability/Languages/OmegaLanguage.lean
@@ -322,7 +322,6 @@ theorem omegaPow_coind' [Inhabited α] (h_nn : [] ∉ l) (h_le : p ≤ l * p) :
   intro s h_s
   have h_nxt m (hm : s.drop m ∈ p) : ∃ n > m, s.extract m n ∈ l ∧ s.drop n ∈ p := by
     obtain ⟨k, _⟩ := hmul_seq_prop ▸ h_le hm
-    use m + k
     grind [extract_eq_drop_take]
   choose nxt_n nxt_p using h_nxt
   let f := iter_helper (fun n ↦ s.drop n ∈ p) nxt_n
diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index 028e9b40..4ce6c4ca 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -417,7 +417,6 @@ theorem LTS.Total.mTr_ωTr [Inhabited Label] [ht : lts.Total] {μl : List Label}
     (hm : lts.MTr s μl t) : ∃ μs ss, lts.ωTr ss (μl ++ω μs) ∧ ss 0 = s ∧ ss μl.length = t := by
   let μs : ωSequence Label := .const default
   obtain ⟨ss', ho, h0⟩ := LTS.Total.ωTr_exists (h := ht) t μs
-  use μs
   grind [LTS.ωTr.append hm ho h0]
 
 /-- `LTS.totalize` constructs a total LTS from any given LTS by adding a sink state. -/
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean
index f8ba3b93..fb611d1b 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean
@@ -92,7 +92,6 @@ lemma para_to_redex (para : M ⭢ₚ N) : M ↠βᶠ N := by
   case fvar => constructor
   case app L L' R R' l_para m_para redex_l redex_m =>
     have : L.app R ↠βᶠ L'.app R := by grind
-    have : L'.app R ↠βᶠ L'.app R' := by grind
     grind [ReductionSystem.MRed.trans]
   case abs t t' xs _ ih =>
     apply redex_abs_cong xs