chore(data/finset/basic): erase_inj_on (#6769)

Quick follow-up to #6737
leanprover-community · Mar 19, 2021 · c65146d · c65146d
1 parent 2d2929f
commit c65146d
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/data/finset/basic.lean b/src/data/finset/basic.lean
@@ -906,6 +906,9 @@ begin
   simp,
 end
 
+lemma erase_inj_on (s : finset α) : set.inj_on s.erase s :=
+λ _ _ _ _, (erase_inj s ‹_›).mp
+
 /-! ### sdiff -/
 
 /-- `s \ t` is the set consisting of the elements of `s` that are not in `t`. -/