chore: fix port of join_filter_isEmpty_eq_false (#10951)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/Computability/Language.lean

@@ -179,11 +179,10 @@ lemma mem_kstar_iff_exists_nonempty {x : List α} :
     x ∈ l∗ ↔ ∃ S : List (List α), x = S.join ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ [] := by
   constructor
   · rintro ⟨S, rfl, h⟩
-    refine' ⟨S.filter fun l ↦ ¬List.isEmpty l, by simp, fun y hy ↦ _⟩
+    refine' ⟨S.filter fun l ↦ !List.isEmpty l, by simp, fun y hy ↦ _⟩
     -- Porting note: The previous code was:
     -- rw [mem_filter, empty_iff_eq_nil] at hy
-    rw [mem_filter, decide_not, Bool.decide_coe, Bool.not_eq_true', ← Bool.bool_iff_false,
-      isEmpty_iff_eq_nil] at hy
+    rw [mem_filter, Bool.not_eq_true', ← Bool.bool_iff_false, isEmpty_iff_eq_nil] at hy
     exact ⟨h y hy.1, hy.2⟩
   · rintro ⟨S, hx, h⟩
     exact ⟨S, hx, fun y hy ↦ (h y hy).1⟩

Mathlib/Data/List/Join.lean

@@ -42,23 +42,22 @@ theorem join_append (L₁ L₂ : List (List α)) : join (L₁ ++ L₂) = join L
 theorem join_concat (L : List (List α)) (l : List α) : join (L.concat l) = join L ++ l := by simp
 #align list.join_concat List.join_concat
 
--- Porting note: `ff/tt` should be translated to `false/true`.
--- Porting note: `List.filter` now takes a `Bool` not a `Prop`.
---     Should the correct spelling now be `== false` instead?
 @[simp]
-theorem join_filter_isEmpty_eq_false [DecidablePred fun l : List α => l.isEmpty = false] :
-    ∀ {L : List (List α)}, join (L.filter fun l => l.isEmpty = false) = L.join
+theorem join_filter_not_isEmpty  :
+    ∀ {L : List (List α)}, join (L.filter fun l => !l.isEmpty) = L.join
   | [] => rfl
   | [] :: L => by
-      simp [join_filter_isEmpty_eq_false (L := L), isEmpty_iff_eq_nil]
+      simp [join_filter_not_isEmpty (L := L), isEmpty_iff_eq_nil]
   | (a :: l) :: L => by
-      simp [join_filter_isEmpty_eq_false (L := L)]
-#align list.join_filter_empty_eq_ff List.join_filter_isEmpty_eq_false
+      simp [join_filter_not_isEmpty (L := L)]
+#align list.join_filter_empty_eq_ff List.join_filter_not_isEmpty
+
+@[deprecated] alias join_filter_isEmpty_eq_false := join_filter_not_isEmpty
 
 @[simp]
 theorem join_filter_ne_nil [DecidablePred fun l : List α => l ≠ []] {L : List (List α)} :
     join (L.filter fun l => l ≠ []) = L.join := by
-  simp [join_filter_isEmpty_eq_false, ← isEmpty_iff_eq_nil]
+  simp only [Ne.def, join_filter_not_isEmpty, ← isEmpty_iff_eq_nil, decide_not, Bool.decide_coe]
 #align list.join_filter_ne_nil List.join_filter_ne_nil
 
 theorem join_join (l : List (List (List α))) : l.join.join = (l.map join).join := by