chore: weekly lints for 2026-01-05 (#245)

As identified by [this
workflow](https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Weekly.20linting.20log/near/566277830).

Author: chenson2018

Cslib/Computability/Automata/NA/Concat.lean

@@ -49,7 +49,6 @@ lemma concat_run_left {xs : ωSequence Symbol} {ss : ωSequence (State1 ⊕ Stat
     obtain ⟨t1, h_mtr, _⟩ := h_ind (by grind)
     obtain ⟨t1', h_tr, _⟩ : ∃ t1', na1.Tr t1 (xs n) t1' ∧ ss (n + 1) = inl t1' := by
       grind [concat, hc.trans n]
-    use t1'
     grind [LTS.MTr.stepR na1.toLTS h_mtr h_tr]
 
 lemma concat_run_left_right {xs : ωSequence Symbol} {ss : ωSequence (State1 ⊕ State2)}

Cslib/Computability/Automata/NA/Loop.lean

@@ -53,13 +53,11 @@ lemma loop_run_left_right {xs : ωSequence Symbol} {ss : ωSequence (Unit ⊕ St
     obtain ⟨t, _⟩ := isRight_iff.mp <| h2 1 (by grind) (by grind)
     obtain ⟨s, _⟩ : ∃ s, na.Tr s (xs 0) t ∧ s ∈ na.start := by
       grind [FinAcc.loop, h.start, h.trans 0]
-    use s, t
     grind
   case succ m h_ind =>
     obtain ⟨s, t, h_mtr, _⟩ := h_ind (by grind) (by grind)
     obtain ⟨t', _⟩ := isRight_iff.mp <|h2 (m + 1 + 1) (by grind) (by grind)
     have h_tr : na.Tr t (xs (m + 1)) t' := by grind [FinAcc.loop, h.trans (m + 1)]
-    use s, t'
     grind [LTS.MTr.stepR na.toLTS h_mtr h_tr]
 
 lemma loop_run_left_right_left {xs : ωSequence Symbol} {ss : ωSequence (Unit ⊕ State)}