fix problems caused by earlier PRs' changes

Author: datokrat

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

@@ -30,7 +30,7 @@ theorem Iter.forIn_eq_forIn_toIterM {α β : Type w} [Iterator α Id β]
     ForIn.forIn it init f = letI : MonadLift Id m := ⟨pure⟩; ForIn.forIn it.toIterM init f := by
   rfl
 
-theorem Iter.forIn_of_step {α β : Type w} [Iterator α Id β]
+theorem Iter.forIn_eq_match_step {α β : Type w} [Iterator α Id β]
     [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
     [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
     {γ : Type w} {it : Iter (α := α) β} {init : γ}
@@ -43,10 +43,10 @@ theorem Iter.forIn_of_step {α β : Type w} [Iterator α Id β]
         | .done c => return c
       | .skip it' _ => ForIn.forIn it' init f
       | .done _ => return init) := by
-  rw [Iter.forIn_eq_forIn_toIterM, @IterM.forIn_of_step, Iter.step]
+  rw [Iter.forIn_eq_forIn_toIterM, @IterM.forIn_eq_match_step, Iter.step]
   simp only [liftM, monadLift, pure_bind]
   generalize it.toIterM.step = step
-  cases step.casesHelper
+  cases step using PlausibleIterStep.casesOn
   · apply bind_congr
     intro forInStep
     rfl
@@ -61,13 +61,11 @@ theorem Iter.forIn_toList {α β : Type w} [Iterator α Id β]
     {f : β → γ → m (ForInStep γ)} :
     ForIn.forIn it.toList init f = ForIn.forIn it init f := by
   rw [List.forIn_eq_foldlM]
-  revert init
-  induction it using Iter.induct with case step it ihy ihs =>
-  intro init
-  rw [forIn_of_step, Iter.toList_of_step]
+  induction it using Iter.inductSteps generalizing init with case step it ihy ihs =>
+  rw [forIn_eq_match_step, Iter.toList_eq_match_step]
   simp only [map_eq_pure_bind]
   generalize it.step = step
-  cases step.casesHelper
+  cases step using PlausibleIterStep.casesOn
   · rename_i it' out h
     simp only [List.foldlM_cons, bind_pure_comp, map_bind]
     apply bind_congr
@@ -95,17 +93,17 @@ theorem Iter.forIn_yield_eq_foldM {α β γ δ : Type w} [Iterator α Id β]
       it.foldM (fun b c => g c b <$> f c b) init := by
   simp [Iter.foldM_eq_forIn]
 
-theorem Iter.foldM_of_step {α β γ : Type w} [Iterator α Id β] [Finite α Id]
+theorem Iter.foldM_eq_match_step {α β γ : Type w} [Iterator α Id β] [Finite α Id]
     {m : Type w → Type w'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m]
     [LawfulIteratorLoop α Id m] {f : γ → β → m γ} {init : γ} {it : Iter (α := α) β} :
     it.foldM (init := init) f = (do
       match it.step with
       | .yield it' out _ => it'.foldM (init := ← f init out) f
       | .skip it' _ => it'.foldM (init := init) f
       | .done _ => return init) := by
-  rw [Iter.foldM_eq_forIn, Iter.forIn_of_step]
+  rw [Iter.foldM_eq_forIn, Iter.forIn_eq_match_step]
   generalize it.step = step
-  cases step.casesHelper <;> simp [foldM_eq_forIn]
+  cases step using PlausibleIterStep.casesOn <;> simp [foldM_eq_forIn]
 
 theorem Iter.foldlM_toList {α β γ : Type w} [Iterator α Id β] [Finite α Id] {m : Type w → Type w'}
     [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
@@ -148,17 +146,17 @@ theorem Iter.forIn_yield_eq_fold {α β γ : Type w} [Iterator α Id β]
       it.fold (fun b c => f c b) init := by
   simp [Iter.fold_eq_forIn]
 
-theorem Iter.fold_of_step {α β γ : Type w} [Iterator α Id β] [Finite α Id]
+theorem Iter.fold_eq_match_step {α β γ : Type w} [Iterator α Id β] [Finite α Id]
     [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
     {f : γ → β → γ} {init : γ} {it : Iter (α := α) β} :
     it.fold (init := init) f = (match it.step with
       | .yield it' out _ => it'.fold (init := f init out) f
       | .skip it' _ => it'.fold (init := init) f
       | .done _ => init) := by
-  rw [fold_eq_foldM, foldM_of_step]
+  rw [fold_eq_foldM, foldM_eq_match_step]
   simp only [fold_eq_foldM]
   generalize it.step = step
-  cases step.casesHelper <;> simp
+  cases step using PlausibleIterStep.casesOn <;> simp
 
 theorem Iter.foldl_toList {α β γ : Type w} [Iterator α Id β] [Finite α Id]
     [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]

src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean

@@ -12,7 +12,7 @@ import Std.Data.Iterators.Lemmas.Consumers.Monadic.Collect
 
 namespace Std.Iterators
 
-theorem IterM.DefaultConsumers.forIn_of_step {α β : Type w} {m : Type w → Type w'}
+theorem IterM.DefaultConsumers.forIn_eq_match_step {α β : Type w} {m : Type w → Type w'}
     [Iterator α m β]
     {n : Type w → Type w''} [Monad n]
     {lift : ∀ γ, m γ → n γ} {γ : Type w}
@@ -31,7 +31,7 @@ theorem IterM.DefaultConsumers.forIn_of_step {α β : Type w} {m : Type w → Ty
   rw [forIn]
   apply bind_congr
   intro step
-  cases step.casesHelper <;> rfl
+  cases step using PlausibleIterStep.casesOn <;> rfl
 
 theorem IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
     {n : Type w → Type w''} [Monad n] [IteratorLoop α m n] [hl : LawfulIteratorLoop α m n]
@@ -41,7 +41,7 @@ theorem IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m
         IteratorLoop.wellFounded_of_finite it init ((⟨·, .intro⟩) <$> f · ·) := by
   cases hl.lawful; rfl
 
-theorem IterM.forIn_of_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
+theorem IterM.forIn_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
     [Finite α m] {n : Type w → Type w''} [Monad n] [LawfulMonad n]
     [IteratorLoop α m n] [LawfulIteratorLoop α m n]
     [MonadLiftT m n] {γ : Type w} {it : IterM (α := α) m β} {init : γ}
@@ -54,10 +54,10 @@ theorem IterM.forIn_of_step {α β : Type w} {m : Type w → Type w'} [Iterator
         | .done c => return c
       | .skip it' _ => ForIn.forIn it' init f
       | .done _ => return init) := by
-  rw [IterM.forIn_eq, DefaultConsumers.forIn_of_step]
+  rw [IterM.forIn_eq, DefaultConsumers.forIn_eq_match_step]
   apply bind_congr
   intro step
-  cases step.casesHelper
+  cases step using PlausibleIterStep.casesOn
   · simp only [map_eq_pure_bind, bind_assoc]
     apply bind_congr
     intro forInStep
@@ -79,18 +79,18 @@ theorem IterM.forIn_yield_eq_foldM {α β γ δ : Type w} {m : Type w → Type w
       it.foldM (fun b c => g c b <$> f c b) init := by
   simp [IterM.foldM_eq_forIn]
 
-theorem IterM.foldM_of_step {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
+theorem IterM.foldM_eq_match_step {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
     {n : Type w → Type w''} [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n]
     [MonadLiftT m n] {f : γ → β → n γ} {init : γ} {it : IterM (α := α) m β} :
     it.foldM (init := init) f = (do
       match ← it.step with
       | .yield it' out _ => it'.foldM (init := ← f init out) f
       | .skip it' _ => it'.foldM (init := init) f
       | .done _ => return init) := by
-  rw [IterM.foldM_eq_forIn, IterM.forIn_of_step]
+  rw [IterM.foldM_eq_forIn, IterM.forIn_eq_match_step]
   apply bind_congr
   intro step
-  cases step.casesHelper <;> simp [foldM_eq_forIn]
+  cases step using PlausibleIterStep.casesOn <;> simp [foldM_eq_forIn]
 
 theorem IterM.fold_eq_forIn {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β]
     [Finite α m] [Monad m]
@@ -113,19 +113,19 @@ theorem IterM.forIn_pure_yield_eq_fold {α β γ : Type w} {m : Type w → Type
       it.fold (fun b c => f c b) init := by
   simp [IterM.fold_eq_forIn]
 
-theorem IterM.fold_of_step {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
+theorem IterM.fold_eq_match_step {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
     [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
     {f : γ → β → γ} {init : γ} {it : IterM (α := α) m β} :
     it.fold (init := init) f = (do
       match ← it.step with
       | .yield it' out _ => it'.fold (init := f init out) f
       | .skip it' _ => it'.fold (init := init) f
       | .done _ => return init) := by
-  rw [fold_eq_foldM, foldM_of_step]
+  rw [fold_eq_foldM, foldM_eq_match_step]
   simp only [fold_eq_foldM]
   apply bind_congr
   intro step
-  cases step.casesHelper <;> simp
+  cases step using PlausibleIterStep.casesOn <;> simp
 
 theorem IterM.toList_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
     [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
@@ -136,13 +136,13 @@ theorem IterM.toList_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator
       it.fold (init := l') (fun l out => l ++ [out]) by
     specialize h []
     simpa using h
-  induction it using IterM.induct with | step it ihy ihs =>
+  induction it using IterM.inductSteps with | step it ihy ihs =>
   intro l'
-  rw [IterM.toList_of_step, IterM.fold_of_step]
+  rw [IterM.toList_eq_match_step, IterM.fold_eq_match_step]
   simp only [map_eq_pure_bind, bind_assoc]
   apply bind_congr
   intro step
-  cases step.casesHelper
+  cases step using PlausibleIterStep.casesOn
   · rename_i it' out h
     specialize ihy h (l' ++ [out])
     simpa using ihy
@@ -165,28 +165,28 @@ theorem IterM.drain_eq_forIn {α β : Type w} {m : Type w → Type w'}  [Iterato
     it.drain = ForIn.forIn (m := m) it PUnit.unit (fun _ _ => pure (ForInStep.yield .unit)) := by
   simp [IterM.drain_eq_fold, IterM.fold_eq_forIn]
 
-theorem IterM.drain_of_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
+theorem IterM.drain_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
     [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
     {it : IterM (α := α) m β} :
     it.drain = (do
       match ← it.step with
       | .yield it' _ _ => it'.drain
       | .skip it' _ => it'.drain
       | .done _ => return .unit) := by
-  rw [IterM.drain_eq_fold, IterM.fold_of_step]
+  rw [IterM.drain_eq_fold, IterM.fold_eq_match_step]
   simp [IterM.drain_eq_fold]
 
 theorem IterM.drain_eq_map_toList {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
     [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
     [IteratorCollect α m] [LawfulIteratorCollect α m]
     {it : IterM (α := α) m β} :
     it.drain = (fun _ => .unit) <$> it.toList := by
-  induction it using IterM.induct with | step it ihy ihs =>
-  rw [IterM.drain_of_step, IterM.toList_of_step]
+  induction it using IterM.inductSteps with | step it ihy ihs =>
+  rw [IterM.drain_eq_match_step, IterM.toList_eq_match_step]
   simp only [map_eq_pure_bind, bind_assoc]
   apply bind_congr
   intro step
-  cases step.casesHelper
+  cases step using PlausibleIterStep.casesOn
   · rename_i it' out h
     simp [ihy h]
   · rename_i it' h