fixes / FIXMEs

Author: kim-em

src/Init/Data/Array/OfFn.lean

@@ -129,7 +129,6 @@ theorem ofFnM_pure [Monad m] [LawfulMonad m] {n} {f : Fin n → α} :
 
 @[simp, grind =] theorem idRun_ofFnM {f : Fin n → Id α} :
     Id.run (ofFnM f) = ofFn (fun i => Id.run (f i)) := by
-  unfold Id.run
   induction n with
   | zero => simp
   | succ n ih => simp [ofFnM_succ', ofFn_succ', ih]

src/Init/Data/List/OfFn.lean

@@ -173,7 +173,6 @@ theorem ofFnM_pure [Monad m] [LawfulMonad m] {n} {f : Fin n → α} :
 
 @[simp, grind =] theorem idRun_ofFnM {f : Fin n → Id α} :
     Id.run (ofFnM f) = ofFn (fun i => Id.run (f i)) := by
-  unfold Id.run
   induction n with
   | zero => simp
   | succ n ih => simp [-ofFn_succ, ofFnM_succ_last, ofFn_succ_last, ih]

src/Init/Data/Vector/OfFn.lean

@@ -154,7 +154,6 @@ theorem ofFnM_pure [Monad m] [LawfulMonad m] {n} {f : Fin n → α} :
 
 @[simp, grind =] theorem idRun_ofFnM {f : Fin n → Id α} :
     Id.run (ofFnM f) = ofFn (fun i => Id.run (f i)) := by
-  unfold Id.run
   induction n with
   | zero => simp
   | succ n ih => simp [ofFnM_succ', ofFn_succ', ih]

src/Std/Data/Iterators/Lemmas/Consumers/Collect.lean

@@ -41,20 +41,21 @@ theorem IterM.toListRev_toIter {α β} [Iterator α Id β] [Finite α Id]
 theorem Iter.toList_toArray {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id]
     [LawfulIteratorCollect α Id] {it : Iter (α := α) β} :
     it.toArray.toList = it.toList := by
-  simp only [toArray_eq_toArray_toIterM, toList_eq_toList_toIterM, ← IterM.toList_toArray,
-    Id.map_eq]
+  simp only [toArray_eq_toArray_toIterM, toList_eq_toList_toIterM, ← IterM.toList_toArray]
+  rfl -- FIXME: defeq abuse of `Id`.
 
 theorem Iter.toArray_toList {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id]
     [LawfulIteratorCollect α Id] {it : Iter (α := α) β} :
     it.toList.toArray = it.toArray := by
-  simp only [toArray_eq_toArray_toIterM, toList_eq_toList_toIterM, ← IterM.toArray_toList,
-    Id.map_eq]
-
+  simp only [toArray_eq_toArray_toIterM, toList_eq_toList_toIterM, ← IterM.toArray_toList]
+  rfl -- FIXME: defeq abuse of `Id`.
 theorem Iter.toListRev_eq {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id]
     [LawfulIteratorCollect α Id] {it : Iter (α := α) β} :
     it.toListRev = it.toList.reverse := by
   simp [Iter.toListRev_eq_toListRev_toIterM, Iter.toList_eq_toList_toIterM, IterM.toListRev_eq]
+  rfl -- FIXME: defeq abuse of
 
+set_option linter.deprecated false in -- FIXME: defeq abuse of `Id`.
 theorem Iter.toArray_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id]
     [LawfulIteratorCollect α Id] {it : Iter (α := α) β} :
     it.toArray = match it.step with
@@ -63,7 +64,7 @@ theorem Iter.toArray_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [I
       | .done _ => #[] := by
   simp only [Iter.toArray_eq_toArray_toIterM, Iter.step]
   rw [IterM.toArray_eq_match_step]
-  simp only [Id.map_eq, Id.pure_eq, Id.bind_eq, Id.run]
+  simp only [Id.run_map, Id.pure_eq, Id.bind_eq, Id.run]
   generalize it.toIterM.step = step
   cases step using PlausibleIterStep.casesOn <;> simp
 
@@ -76,6 +77,7 @@ theorem Iter.toList_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [It
   rw [← Iter.toList_toArray, Iter.toArray_eq_match_step]
   split <;> simp [Iter.toList_toArray]
 
+set_option linter.deprecated false in -- FIXME: defeq abuse of `Id`.
 theorem Iter.toListRev_eq_match_step {α β} [Iterator α Id β] [Finite α Id] {it : Iter (α := α) β} :
     it.toListRev = match it.step with
       | .yield it' out _ => it'.toListRev ++ [out]