merge lean-pr-testing-4231

leanprover-community · May 21, 2024 · 8ce9df4 · 8ce9df4
2 parents 8a26337 + c23f307
commit 8ce9df4
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/Batteries/Data/String/Lemmas.lean b/Batteries/Data/String/Lemmas.lean
@@ -18,8 +18,6 @@ namespace String
 
 theorem ext_iff {s₁ s₂ : String} : s₁ = s₂ ↔ s₁.data = s₂.data := ⟨fun h => h ▸ rfl, ext⟩
 
-theorem lt_irrefl (s : String) : ¬s < s := List.lt_irrefl' (α := Char) (fun _ => Nat.lt_irrefl _) _
-
 theorem lt_trans {s₁ s₂ s₃ : String} : s₁ < s₂ → s₂ < s₃ → s₁ < s₃ :=
   List.lt_trans' (α := Char) Nat.lt_trans
     (fun h1 h2 => Nat.not_lt.2 <| Nat.le_trans (Nat.not_lt.1 h2) (Nat.not_lt.1 h1))