theorem Std.Iterators.IterM.Intermediate.dropWhileM_eq_dropWhileWithPostcondition {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [Iterator α m β] {it : IterM m β} {P : β → m (ULift Bool)} {dropping : Bool} : dropWhileM P dropping it = dropWhileWithPostcondition (PostconditionT.lift ∘ P) dropping it

theorem Std.Iterators.IterM.Intermediate.dropWhile_eq_dropWhileM {dropping : Bool} {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [Iterator α m β] {it : IterM m β} {P : β → Bool} : dropWhile P dropping it = dropWhileM (pure ∘ ULift.up ∘ P) dropping it

theorem Std.Iterators.IterM.dropWhileWithPostcondition_eq_intermediateDropWhileWithPostcondition {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Iterator α m β] {it : IterM m β} {P : β → PostconditionT m (ULift Bool)} : dropWhileWithPostcondition P it = Intermediate.dropWhileWithPostcondition P true it

theorem Std.Iterators.IterM.dropWhileM_eq_intermediateDropWhileM {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [Iterator α m β] {it : IterM m β} {P : β → m (ULift Bool)} : dropWhileM P it = Intermediate.dropWhileM P true it

theorem Std.Iterators.IterM.dropWhile_eq_intermediateDropWhile {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [Iterator α m β] {it : IterM m β} {P : β → Bool} : dropWhile P it = Intermediate.dropWhile P true it

theorem Std.Iterators.IterM.step_intermediateDropWhileWithPostcondition {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [Iterator α m β] {it : IterM m β} {P : β → PostconditionT m (ULift Bool)} {dropping : Bool} : (Intermediate.dropWhileWithPostcondition P dropping it).step = do let __do_lift ← it.step match __do_lift with | ⟨IterStep.yield it' out, h⟩ => if h' : dropping = true then do let __do_lift ← (P out).operation match __do_lift with | ⟨{ down := true }, h''⟩ => pure (PlausibleIterStep.skip (Intermediate.dropWhileWithPostcondition P true it') ⋯) | ⟨{ down := false }, h''⟩ => pure (PlausibleIterStep.yield (Intermediate.dropWhileWithPostcondition P false it') out ⋯) else pure (PlausibleIterStep.yield (Intermediate.dropWhileWithPostcondition P false it') out ⋯) | ⟨IterStep.skip it', h⟩ => pure (PlausibleIterStep.skip (Intermediate.dropWhileWithPostcondition P dropping it') ⋯) | ⟨IterStep.done, h⟩ => pure (PlausibleIterStep.done ⋯)

theorem Std.Iterators.IterM.step_dropWhileWithPostcondition {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [Iterator α m β] {it : IterM m β} {P : β → PostconditionT m (ULift Bool)} : (dropWhileWithPostcondition P it).step = do let __do_lift ← it.step match __do_lift with | ⟨IterStep.yield it' out, h⟩ => do let __do_lift ← (P out).operation match __do_lift with | ⟨{ down := true }, h''⟩ => pure (PlausibleIterStep.skip (Intermediate.dropWhileWithPostcondition P true it') ⋯) | ⟨{ down := false }, h''⟩ => pure (PlausibleIterStep.yield (Intermediate.dropWhileWithPostcondition P false it') out ⋯) | ⟨IterStep.skip it', h⟩ => pure (PlausibleIterStep.skip (Intermediate.dropWhileWithPostcondition P true it') ⋯) | ⟨IterStep.done, h⟩ => pure (PlausibleIterStep.done ⋯)

theorem Std.Iterators.IterM.step_intermediateDropWhileM {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [LawfulMonad m] [Iterator α m β] {it : IterM m β} {P : β → m (ULift Bool)} {dropping : Bool} : (Intermediate.dropWhileM P dropping it).step = do let __do_lift ← it.step match __do_lift with | ⟨IterStep.yield it' out, h⟩ => if h' : dropping = true then do let __do_lift ← P out match __do_lift with | { down := true } => pure (PlausibleIterStep.skip (Intermediate.dropWhileM P true it') ⋯) | { down := false } => pure (PlausibleIterStep.yield (Intermediate.dropWhileM P false it') out ⋯) else pure (PlausibleIterStep.yield (Intermediate.dropWhileM P false it') out ⋯) | ⟨IterStep.skip it', h⟩ => pure (PlausibleIterStep.skip (Intermediate.dropWhileM P dropping it') ⋯) | ⟨IterStep.done, h⟩ => pure (PlausibleIterStep.done ⋯)

theorem Std.Iterators.IterM.step_dropWhileM {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [LawfulMonad m] [Iterator α m β] {it : IterM m β} {P : β → m (ULift Bool)} : (dropWhileM P it).step = do let __do_lift ← it.step match __do_lift with | ⟨IterStep.yield it' out, h⟩ => do let __do_lift ← P out match __do_lift with | { down := true } => pure (PlausibleIterStep.skip (Intermediate.dropWhileM P true it') ⋯) | { down := false } => pure (PlausibleIterStep.yield (Intermediate.dropWhileM P false it') out ⋯) | ⟨IterStep.skip it', h⟩ => pure (PlausibleIterStep.skip (Intermediate.dropWhileM P true it') ⋯) | ⟨IterStep.done, h⟩ => pure (PlausibleIterStep.done ⋯)

theorem Std.Iterators.IterM.step_intermediateDropWhile {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [LawfulMonad m] [Iterator α m β] {it : IterM m β} {P : β → Bool} {dropping : Bool} : (Intermediate.dropWhile P dropping it).step = do let __do_lift ← it.step match __do_lift with | ⟨IterStep.yield it' out, h⟩ => if h' : dropping = true then match P out with | true => pure (PlausibleIterStep.skip (Intermediate.dropWhile P true it') ⋯) | false => pure (PlausibleIterStep.yield (Intermediate.dropWhile P false it') out ⋯) else pure (PlausibleIterStep.yield (Intermediate.dropWhile P false it') out ⋯) | ⟨IterStep.skip it', h⟩ => pure (PlausibleIterStep.skip (Intermediate.dropWhile P dropping it') ⋯) | ⟨IterStep.done, h⟩ => pure (PlausibleIterStep.done ⋯)

theorem Std.Iterators.IterM.step_dropWhile {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [LawfulMonad m] [Iterator α m β] {it : IterM m β} {P : β → Bool} : (dropWhile P it).step = do let __do_lift ← it.step match __do_lift with | ⟨IterStep.yield it' out, h⟩ => match P out with | true => pure (PlausibleIterStep.skip (Intermediate.dropWhile P true it') ⋯) | false => pure (PlausibleIterStep.yield (Intermediate.dropWhile P false it') out ⋯) | ⟨IterStep.skip it', h⟩ => pure (PlausibleIterStep.skip (Intermediate.dropWhile P true it') ⋯) | ⟨IterStep.done, h⟩ => pure (PlausibleIterStep.done ⋯)