From 8ed6b30084dfc1d2fe303dbc7a8d1c435dac6655 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 23 Feb 2026 11:23:03 +0100
Subject: [PATCH] refactor: cleanups after #12538 (#12643)

This PR removes some spurious comments after #12538.
---
 .../Combinators/Monadic/FilterMap.lean        |  1 -
 .../Iterators/Lemmas/Combinators/FlatMap.lean | 29 -------------------
 src/Init/Data/Range/Polymorphic/SInt.lean     |  2 ++
 3 files changed, 2 insertions(+), 30 deletions(-)

diff --git a/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean b/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean
index e5e78c303d..369053160d 100644
--- a/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean
+++ b/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean
@@ -280,7 +280,6 @@ For each value emitted by the base iterator `it`, this combinator calls `f`.
 @[inline, expose]
 def IterM.mapWithPostcondition {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
     [Monad n] [MonadLiftT m n] [Iterator α m β] (f : β → PostconditionT n γ)
-    -- TODO: eta expand `lift`?
     (it : IterM (α := α) m β) : IterM (α := Map α m n (fun ⦃_⦄ => monadLift) f) n γ :=
   InternalCombinators.map (fun {_} => monadLift) f it
 
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean
index 475381f1be..af874ee622 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean
@@ -232,35 +232,6 @@ public theorem Iter.toArray_flatMapM {α α₂ β γ : Type w} {m : Type w → T
     (it₁.flatMapM f).toArray = Array.flatten <$> (it₁.mapM fun b => do (← f b).toArray).toArray := by
   simp [flatMapM, toArray_flatMapAfterM]
 
--- public theorem Iter.toList_flatMapAfter {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
---     [Finite α Id] [Finite α₂ Id]
---     {f : β → Iter (α := α₂) γ} {it₁ : Iter (α := α) β} {it₂ : Option (Iter (α := α₂) γ)} :
---     (it₁.flatMapAfter f it₂).toList = match it₂ with
---       | none => (it₁.map fun b => (f b).toList).toList.flatten
---       | some it₂ => it₂.toList ++
---           (it₁.map fun b => (f b).toList).toList.flatten := by
---   unfold Iter.toList
---   simp only [flatMapAfter, Iter.toList, toIterM_toIter, IterM.toList_flatMapAfter]
---   cases it₂ <;>
---     simp only [map, toIterM_toIter]
---   · -- Here, we rewrite with `Id.pure_run`, making the RHS ill-typed in `reducible` transparency because the `Types.Map.instIterator` instance is *not* rewritten. However, not applying `pure_run` doesn't allow progress, either. `+instances` would help.
---     -- Could we have `congr` lemmas for these situations?
---     -- Is it a good idea that `simp` happily rewrites even though this increases the incongruence level?
---     -- Can we visualize the "incongruence level" by showing explicit casts for `reducible`, `instance` and `semireducible` transparency violations?
---     simp? [map, IterM.toList_map_eq_toList_mapM, - IterM.toList_map, Id.pure_run]
---     with_reducible congr -- This solves that problem that we don't rewrite inside instances
---     -- Observation: Types have already been acknowledged to be equal, and unfolding the very same expressions would make the terms equal, too.
---     --- Would it be possible to unfold the arguments when they are used in the type and need to be unfolded so that it type-checks?
---     -- At least, it's unintuitive that types are checked differently.
---     -- Another perspective on the problem:
---     --- It's weird that parameters that should be of the same type can syntactically differ, even though they
---     --- make problems with `simp`.
---     ---- Again, one could think about collecting all such "type correctness required unfolding equations" and allow simp to unfold them?
---     simp only [Id.pure_run]
---   · simp only [map, IterM.toList_map_eq_toList_mapM, - IterM.toList_map]
---   -- IDEA: Would it be an idea to include instances in the discr tree AFTER REDUCING THEM?
---   -- Should I just not rely so much on defeq? How would a non-defeq proof look like?
-
 set_option backward.isDefEq.respectTransparency false in
 public theorem Iter.toList_flatMapAfter {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
     [Finite α Id] [Finite α₂ Id]
diff --git a/src/Init/Data/Range/Polymorphic/SInt.lean b/src/Init/Data/Range/Polymorphic/SInt.lean
index 368f8b4b8e..37ba74ad27 100644
--- a/src/Init/Data/Range/Polymorphic/SInt.lean
+++ b/src/Init/Data/Range/Polymorphic/SInt.lean
@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
 module
+
 prelude
+
 public import Init.Data.Range.Polymorphic.Instances
 public import Init.Data.SInt
 import all Init.Data.SInt.Basic