feat(data/fin): mem_find_iff (#1307)

* feat(data/fin): mem_find_iff

* add find_eq_some_iff (#1308)

Author: ChrisHughes24

src/data/fin.lean

@@ -304,14 +304,24 @@ begin
         exact fin.eta _ _⟩ } }
 end
 
+lemma mem_find_iff {p : fin n → Prop} [decidable_pred p] {i : fin n} : 
+  i ∈ fin.find p ↔ p i ∧ ∀ j, p j → i ≤ j :=
+⟨λ hi, ⟨find_spec _ hi, λ _, find_min' hi⟩, 
+  begin
+    rintros ⟨hpi, hj⟩,
+    cases hfp : fin.find p,
+    { rw [find_eq_none_iff] at hfp,
+      exact (hfp _ hpi).elim },
+    { exact option.some_inj.2 (le_antisymm (find_min' hfp hpi) (hj _ (find_spec _ hfp))) }
+  end⟩
+
+lemma find_eq_some_iff {p : fin n → Prop} [decidable_pred p] {i : fin n} : 
+  fin.find p = some i ↔ p i ∧ ∀ j, p j → i ≤ j :=
+ mem_find_iff
+
 lemma mem_find_of_unique {p : fin n → Prop} [decidable_pred p]
   (h : ∀ i j, p i → p j → i = j) {i : fin n} (hi : p i) : i ∈ fin.find p :=
-begin
-  cases hfp : fin.find p,
-  { rw [find_eq_none_iff] at hfp,
-    exact (hfp _ hi).elim },
-  { exact option.some_inj.2 (h _ _ (find_spec _ hfp) hi) }
-end
+mem_find_iff.2 ⟨hi, λ j hj, le_of_eq $ h i j hi hj⟩
 
 end find