cleanups

Author: datokrat

src/Init/Data/Range/Polymorphic/PRange.lean

@@ -304,11 +304,19 @@ This is encoded in `LawfulClosedOpenIntersection`.
 class ClosedOpenIntersection (shape : RangeShape) (α : Type w) where
   intersection : PRange shape α → PRange ⟨.closed, .open⟩ α → PRange ⟨.closed, .open⟩ α
 
+/--
+This typeclass ensures that the intersection according to `ClosedOpenIntersection shape α`
+of two ranges contains exactly those elements that are contained in both ranges.
+-/
 class LawfulClosedOpenIntersection (shape : RangeShape) (α : Type w)
     [ClosedOpenIntersection shape α]
     [SupportsLowerBound shape.lower α] [SupportsUpperBound shape.upper α]
     [SupportsLowerBound .closed α]
     [SupportsUpperBound .open α] where
+  /--
+  The intersection according to `ClosedOpenIntersection shapee α` of two ranges contains exactly
+  those elements that are contained in both ranges.
+  -/
   mem_intersection_iff {a : α} {r : PRange ⟨shape.lower, shape.upper⟩ α}
       {s : PRange ⟨.closed, .open⟩ α} :
     a ∈ ClosedOpenIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s

src/Init/Data/Slice/Array.lean

@@ -30,10 +30,12 @@ instance {shape} {α : Type u} [ClosedOpenIntersection shape Nat] :
 instance {s : Subarray α} : ToIterator s Id α :=
   .of _
     (PRange.Internal.iter (s.internalRepresentation.start...<s.internalRepresentation.stop)
-      |>.attachWith (· < s.internalRepresentation.array.size) (by
-        simp only [Internal.isPlausibleIndirectOutput_iter_iff, Membership.mem,
-          SupportsUpperBound.IsSatisfied, and_imp]
-        intro out _ h
-        have := s.internalRepresentation.stop_le_array_size
-        omega)
+      |>.attachWith (· < s.internalRepresentation.array.size) ?h
       |>.map fun i => s.internalRepresentation.array[i.1])
+where finally
+  case h =>
+    simp only [Internal.isPlausibleIndirectOutput_iter_iff, Membership.mem,
+      SupportsUpperBound.IsSatisfied, and_imp]
+    intro out _ h
+    have := s.internalRepresentation.stop_le_array_size
+    omega

src/Init/Data/Slice/Operations.lean

@@ -27,23 +27,28 @@ def Internal.iter (s : Slice γ) [ToIterator s Id β] :=
   ToIterator.iter s
 
 /--
-Returns the number of elements -- not necessarily distinct -- in the given slice.
+Returns the number of elements with distinct indices in the given slice.
+
+Example: `#[1, 1, 1][0...2] = 2`.
 -/
 @[always_inline, inline]
 def size (s : Slice g) [ToIterator s Id β] [Iterator (ToIterator.State s Id) Id β]
     [IteratorSize (ToIterator.State s Id) Id] :=
   Internal.iter s |>.size
 
+/-- Allocates a new array that contains the elements of the slice. -/
 @[always_inline, inline]
 def toArray (s : Slice g) [ToIterator s Id β] [Iterator (ToIterator.State s Id) Id β]
     [IteratorCollect (ToIterator.State s Id) Id Id] [Finite (ToIterator.State s Id) Id] : Array β :=
   Internal.iter s |>.toArray
 
+/-- Allocates a new list that contains the elements of the slice. -/
 @[always_inline, inline]
 def toList (s : Slice g) [ToIterator s Id β] [Iterator (ToIterator.State s Id) Id β]
     [IteratorCollect (ToIterator.State s Id) Id Id] [Finite (ToIterator.State s Id) Id] : List β :=
   Internal.iter s |>.toList
 
+/-- Allocates a new list that contains the elements of the slice in reverse order. -/
 @[always_inline, inline]
 def toListRev (s : Slice g) [ToIterator s Id β] [Iterator (ToIterator.State s Id) Id β]
     [IteratorCollect (ToIterator.State s Id) Id Id] [Finite (ToIterator.State s Id) Id] : List β :=