cleanups

Author: datokrat

src/Init/Core.lean

@@ -1360,13 +1360,6 @@ theorem Relation.TransGen.trans {α : Sort u} {r : α → α → Prop} {a b c} :
   | single h => exact TransGen.tail hab h
   | tail _ h ih => exact TransGen.tail ih h
 
-theorem Relation.TransGen.mono {α : Sort u} {r s : α → α → Prop} (h : ∀ a b, r a b → s a b) {a b} :
-    TransGen r a b → TransGen s a b := by
-  intro hab
-  induction hab
-  case single rab => exact .single (h _ _ rab)
-  case tail rbc ih => exact .tail ih (h _ _ rbc)
-
 /-! # Subtype -/
 
 namespace Subtype

src/Init/Data/Iterators/Combinators/Monadic/Take.lean

@@ -34,6 +34,10 @@ structure Take (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α
   countdown : Nat
   /-- Internal implementation detail of the iterator library -/
   inner : IterM (α := α) m β
+  /--
+  Internal implementation detail of the iterator library.
+  This proof term ensures that a `take` always produces a finite iterator from a productive one.
+  -/
   finite : countdown > 0 ∨ Finite α m
 
 /--