Skip to content

Commit

Permalink
merge lean-pr-testing-5285
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em committed Sep 10, 2024
2 parents cb0d039 + 9feaefc commit 4dc6beb
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions Batteries/Data/List/Perm.lean
Original file line number Diff line number Diff line change
Expand Up @@ -235,8 +235,8 @@ theorem subperm_append_diff_self_of_count_le {l₁ l₂ : List α}
| nil => simp
| cons hd tl IH =>
have : hd ∈ l₂ := by
rw [← count_pos_iff_mem]
exact Nat.lt_of_lt_of_le (count_pos_iff_mem.mpr (.head _)) (h hd (.head _))
rw [← count_pos_iff]
exact Nat.lt_of_lt_of_le (count_pos_iff.mpr (.head _)) (h hd (.head _))
have := perm_cons_erase this
refine Perm.trans ?_ this.symm
rw [cons_append, diff_cons, perm_cons]
Expand Down

0 comments on commit 4dc6beb

Please sign in to comment.