sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 10:24:07 +00:00
Code Issues Packages Projects Releases Wiki Activity

remove +instances

Browse Source
This commit is contained in:
Paul Reichert
2026-03-15 13:26:27 +01:00
parent 6790d3807f
commit 3896dfbf01
9 changed files with 71 additions and 57 deletions
Download Patch File Download Diff File Expand all files Collapse all files

43
src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
View File

@@ -435,8 +435,9 @@ theorem Iter.forIn_filterMapWithPostcondition
match ← (f out).run with
| some c => g c acc
| none => return .yield acc) := by
simp +instances [Iter.forIn_eq_forIn_toIterM, filterMapWithPostcondition, IterM.forIn_filterMapWithPostcondition,
instMonadLiftTOfMonadLift_instMonadLiftTOfPure]; rfl
simp only [filterMapWithPostcondition, IterM.forIn_filterMapWithPostcondition, forIn_eq_forIn_toIterM]
rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
rfl -- expressions are equal up to different matchers
theorem Iter.forIn_filterMapM
[Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
@@ -448,8 +449,9 @@ theorem Iter.forIn_filterMapM
match ← f out with
| some c => g c acc
| none => return .yield acc) := by
simp +instances [filterMapM, forIn_eq_forIn_toIterM, IterM.forIn_filterMapM,
instMonadLiftTOfMonadLift_instMonadLiftTOfPure]; rfl
simp [filterMapM, forIn_eq_forIn_toIterM, IterM.forIn_filterMapM]
rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
rfl
theorem Iter.forIn_filterMap
[Monad n] [LawfulMonad n] [Finite α Id]
@@ -469,8 +471,8 @@ theorem Iter.forIn_mapWithPostcondition
{g : β₂ → γ → o (ForInStep γ)} :
forIn (it.mapWithPostcondition f) init g =
forIn it init (fun out acc => do g (← (f out).run) acc) := by
simp +instances [mapWithPostcondition, forIn_eq_forIn_toIterM, IterM.forIn_mapWithPostcondition,
instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
simp only [mapWithPostcondition, forIn_eq_forIn_toIterM, IterM.forIn_mapWithPostcondition]
rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
theorem Iter.forIn_mapM
[Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
@@ -498,8 +500,8 @@ theorem Iter.forIn_filterWithPostcondition
haveI : MonadLift n o := ⟨monadLift⟩
forIn (it.filterWithPostcondition f) init g =
forIn it init (fun out acc => do if (← (f out).run).down then g out acc else return .yield acc) := by
simp +instances [filterWithPostcondition, forIn_eq_forIn_toIterM, IterM.forIn_filterWithPostcondition,
instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
simp only [filterWithPostcondition, forIn_eq_forIn_toIterM, IterM.forIn_filterWithPostcondition]
rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
theorem Iter.forIn_filterM
[Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
@@ -508,8 +510,8 @@ theorem Iter.forIn_filterM
[IteratorLoop α Id o] [LawfulIteratorLoop α Id o]
{it : Iter (α := α) β} {f : β → n (ULift Bool)} {init : γ} {g : β → γ → o (ForInStep γ)} :
forIn (it.filterM f) init g = forIn it init (fun out acc => do if (← f out).down then g out acc else return .yield acc) := by
simp +instances [filterM, forIn_eq_forIn_toIterM, IterM.forIn_filterM,
instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
simp only [filterM, forIn_eq_forIn_toIterM, IterM.forIn_filterM]
rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
theorem Iter.forIn_filter
[Monad n] [LawfulMonad n]
@@ -550,8 +552,9 @@ theorem Iter.foldM_filterMapM {α β γ δ : Type w}
it.foldM (init := init) (fun d b => do
let some c ← f b | pure d
g d c) := by
simp +instances [filterMapM, IterM.foldM_filterMapM, foldM_eq_foldM_toIterM,
instMonadLiftTOfMonadLift_instMonadLiftTOfPure]; rfl
simp only [filterMapM, IterM.foldM_filterMapM, foldM_eq_foldM_toIterM]
rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
rfl
theorem Iter.foldM_mapWithPostcondition {α β γ δ : Type w}
{n : Type w → Type w''} {o : Type w → Type w'''}
@@ -563,8 +566,8 @@ theorem Iter.foldM_mapWithPostcondition {α β γ δ : Type w}
{f : β → PostconditionT n γ} {g : δ → γ → o δ} {init : δ} {it : Iter (α := α) β} :
(it.mapWithPostcondition f).foldM (init := init) g =
it.foldM (init := init) (fun d b => do let c ← (f b).run; g d c) := by
simp +instances [mapWithPostcondition, IterM.foldM_mapWithPostcondition, foldM_eq_foldM_toIterM,
instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
simp only [mapWithPostcondition, IterM.foldM_mapWithPostcondition, foldM_eq_foldM_toIterM]
rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
theorem Iter.foldM_mapM {α β γ δ : Type w}
{n : Type w → Type w''} {o : Type w → Type w'''}
@@ -578,8 +581,8 @@ theorem Iter.foldM_mapM {α β γ δ : Type w}
haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
(it.mapM f).foldM (init := init) g =
it.foldM (init := init) (fun d b => do let c ← f b; g d c) := by
simp +instances [mapM, IterM.foldM_mapM, foldM_eq_foldM_toIterM,
instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
simp only [mapM, IterM.foldM_mapM, foldM_eq_foldM_toIterM]
rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
theorem Iter.foldM_filterWithPostcondition {α β δ : Type w}
{n : Type w → Type w''} {o : Type w → Type w'''}
@@ -591,8 +594,8 @@ theorem Iter.foldM_filterWithPostcondition {α β δ : Type w}
{f : β → PostconditionT n (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : Iter (α := α) β} :
(it.filterWithPostcondition f).foldM (init := init) g =
it.foldM (init := init) (fun d b => do if (← (f b).run).down then g d b else pure d) := by
simp +instances [filterWithPostcondition, IterM.foldM_filterWithPostcondition, foldM_eq_foldM_toIterM,
instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
simp only [filterWithPostcondition, IterM.foldM_filterWithPostcondition, foldM_eq_foldM_toIterM]
rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
theorem Iter.foldM_filterM {α β δ : Type w}
{n : Type w → Type w''} {o : Type w → Type w'''}
@@ -605,8 +608,8 @@ theorem Iter.foldM_filterM {α β δ : Type w}
{f : β → n (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : Iter (α := α) β} :
(it.filterM f).foldM (init := init) g =
it.foldM (init := init) (fun d b => do if (← f b).down then g d b else pure d) := by
simp +instances [filterM, IterM.foldM_filterM, foldM_eq_foldM_toIterM,
instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
simp only [filterM, IterM.foldM_filterM, foldM_eq_foldM_toIterM]
rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
theorem Iter.foldM_filterMap {α β γ δ : Type w} {n : Type w → Type w''}
[Iterator α Id β] [Finite α Id] [Monad n] [LawfulMonad n]

2
src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
View File

@@ -394,7 +394,7 @@ private theorem IterM.toList_filterMapWithPostcondition_filterMapWithPostconditi
(it.filterMapWithPostcondition (n := o) fg).toList := by
induction it using IterM.inductSteps with | step it ihy ihs
letI : MonadLift n o := ⟨monadLift⟩
haveI : LawfulMonadLift n o := ⟨by simp +instances [this], by simp +instances [this]⟩
haveI : LawfulMonadLift n o := ⟨LawfulMonadLiftT.monadLift_pure, LawfulMonadLiftT.monadLift_bind⟩
rw [toList_eq_match_step, toList_eq_match_step, step_filterMapWithPostcondition,
bind_assoc, step_filterMapWithPostcondition, step_filterMapWithPostcondition]
simp only [bind_assoc, liftM_bind]

7
src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
View File

@@ -32,11 +32,12 @@ theorem Iter.forIn'_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
IterM.DefaultConsumers.forIn' (n := m) (fun _ _ f x => f x.run) γ (fun _ _ _ => True)
it.toIterM init _ (fun _ => id)
(fun out h acc => return ⟨← f out (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc, trivial⟩) := by
simp +instances only [ForIn'.forIn']
simp only [ForIn'.forIn']
have : ∀ a b c, f a b c = (Subtype.val <$> (⟨·, trivial⟩) <$> f a b c) := by simp
simp +singlePass only [this]
rw [hl.lawful (fun _ _ f x => f x.run) (wf := IteratorLoop.wellFounded_of_finite)]
simp +instances [IteratorLoop.defaultImplementation]
simp only [IteratorLoop.forIn, Functor.map_map, id_map',
bind_pure_comp]
theorem Iter.forIn_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
{m : Type x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m]
@@ -81,7 +82,7 @@ theorem Iter.forIn'_eq_forIn'_toIterM {α β : Type w} [Iterator α Id β]
letI : ForIn' m (IterM (α := α) Id β) β _ := IterM.instForIn'
ForIn'.forIn' it.toIterM init
(fun out h acc => f out (isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc) := by
simp +instances [ForIn'.forIn', monadLift]
simp [ForIn'.forIn', monadLift]
theorem Iter.forIn_eq_forIn_toIterM {α β : Type w} [Iterator α Id β]
[Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]

4
src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
View File

@@ -109,10 +109,10 @@ theorem IterM.forIn'_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m
letI : ForIn' n (IterM (α := α) m β) β _ := IterM.instForIn'
ForIn'.forIn' (α := β) (m := n) it init f = IterM.DefaultConsumers.forIn' (n := n)
(fun _ _ f x => monadLift x >>= f) γ (fun _ _ _ => True) it init _ (fun _ => id) (return ⟨← f · · ·, trivial⟩) := by
simp +instances only [ForIn'.forIn']
simp only [ForIn'.forIn']
have : f = (Subtype.val <$> (⟨·, trivial⟩) <$> f · · ·) := by simp
rw [this, hl.lawful (fun _ _ f x => monadLift x >>= f) (wf := IteratorLoop.wellFounded_of_finite)]
simp +instances [IteratorLoop.defaultImplementation]
simp [IteratorLoop.forIn]
try rfl
theorem IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]

8
src/Init/Data/Order/Factories.lean
View File

@@ -208,7 +208,7 @@ public instance LawfulOrderLT.of_lt {α : Type u} [LT α] [i : Asymm (α := α)
haveI := LE.ofLT α
LawfulOrderLT α :=
letI := LE.ofLT α
{ lt_iff a b := by simp +instances [LE.le]; apply Asymm.asymm }
{ lt_iff a b := by simp [LE.le]; apply Asymm.asymm }
/--
If an `LT α` instance is asymmetric and its negation is transitive, then `LE.ofLT α` represents a
@@ -253,8 +253,7 @@ public theorem LawfulOrderInf.of_lt {α : Type u} [Min α] [LT α]
letI := LE.ofLT α
{ le_min_iff a b c := by
open Classical in
simp +instances only [LE.le]
simp [← not_or, Decidable.not_iff_not]
simp only [LE.le, ← not_or, Decidable.not_iff_not]
simpa [Decidable.imp_iff_not_or] using min_lt_iff a b c }
/--
@@ -283,8 +282,7 @@ public theorem LawfulOrderSup.of_lt {α : Type u} [Max α] [LT α]
letI := LE.ofLT α
{ max_le_iff a b c := by
open Classical in
simp +instances only [LE.le]
simp [← not_or, Decidable.not_iff_not]
simp only [LE.le, ← not_or, Decidable.not_iff_not]
simpa [Decidable.imp_iff_not_or] using lt_max_iff a b c }
/--

24
src/Init/Data/Order/Opposite.lean
View File

@@ -287,7 +287,7 @@ scoped instance (priority := low) instLawfulOrderLTOpposite {il : LE α} {it : L
letI := il.opposite
letI := it.opposite
{ lt_iff a b := by
simp +instances only [LE.opposite, LT.opposite]
simp only [LE.le, LT.lt]
letI := il; letI := it
exact LawfulOrderLT.lt_iff b a }
@@ -297,7 +297,7 @@ scoped instance (priority := low) instLawfulOrderBEqOpposite {il : LE α} {ib :
LawfulOrderBEq α :=
letI := il.opposite
{ beq_iff_le_and_ge a b := by
simp +instances only [LE.opposite]
simp only [LE.le]
letI := il; letI := ib
rw [LawfulOrderBEq.beq_iff_le_and_ge]
exact and_comm }
@@ -310,7 +310,7 @@ scoped instance (priority := low) instLawfulOrderInfOpposite {il : LE α} {im :
letI := il.opposite
letI := im.oppositeMax
{ max_le_iff a b c := by
simp +instances only [LE.opposite, Min.oppositeMax]
simp only [LE.le, Max.max]
letI := il; letI := im
exact LawfulOrderInf.le_min_iff c a b }
@@ -322,11 +322,11 @@ scoped instance (priority := low) instLawfulOrderMinOpposite {il : LE α} {im :
letI := il.opposite
letI := im.oppositeMax
{ max_eq_or a b := by
simp +instances only [Min.oppositeMax]
simp only [Max.max]
letI := il; letI := im
exact MinEqOr.min_eq_or a b
max_le_iff a b c := by
simp +instances only [LE.opposite, Min.oppositeMax]
simp only [LE.le, Max.max]
letI := il; letI := im
exact LawfulOrderInf.le_min_iff c a b }
@@ -338,7 +338,7 @@ scoped instance (priority := low) instLawfulOrderSupOpposite {il : LE α} {im :
letI := il.opposite
letI := im.oppositeMin
{ le_min_iff a b c := by
simp +instances only [LE.opposite, Max.oppositeMin]
simp only [LE.le, Min.min]
letI := il; letI := im
exact LawfulOrderSup.max_le_iff b c a }
@@ -350,11 +350,11 @@ scoped instance (priority := low) instLawfulOrderMaxOpposite {il : LE α} {im :
letI := il.opposite
letI := im.oppositeMin
{ min_eq_or a b := by
simp +instances only [Max.oppositeMin]
simp only [Min.min]
letI := il; letI := im
exact MaxEqOr.max_eq_or a b
le_min_iff a b c := by
simp +instances only [LE.opposite, Max.oppositeMin]
simp only [LE.le, Min.min]
letI := il; letI := im
exact LawfulOrderSup.max_le_iff b c a }
@@ -366,11 +366,11 @@ scoped instance (priority := low) instLawfulOrderLeftLeaningMinOpposite {il : LE
letI := il.opposite
letI := im.oppositeMax
{ max_eq_left a b hab := by
simp +instances only [Min.oppositeMax]
simp only [Max.max]
letI := il; letI := im
exact LawfulOrderLeftLeaningMin.min_eq_left a b hab
max_eq_right a b hab := by
simp +instances only [Min.oppositeMax]
simp only [Max.max]
letI := il; letI := im
exact LawfulOrderLeftLeaningMin.min_eq_right a b hab }
@@ -382,11 +382,11 @@ scoped instance (priority := low) instLawfulOrderLeftLeaningMaxOpposite {il : LE
letI := il.opposite
letI := im.oppositeMin
{ min_eq_left a b hab := by
simp +instances only [Max.oppositeMin]
simp only [Min.min]
letI := il; letI := im
exact LawfulOrderLeftLeaningMax.max_eq_left a b hab
min_eq_right a b hab := by
simp +instances only [Max.oppositeMin]
simp only [Min.min]
letI := il; letI := im
exact LawfulOrderLeftLeaningMax.max_eq_right a b hab }

6
src/Init/Data/Range/Polymorphic/RangeIterator.lean
View File

@@ -597,7 +597,7 @@ instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α] [LE α] [Decidabl
LawfulIteratorLoop (Rxc.Iterator α) Id n where
lawful := by
intro lift instLawfulMonadLiftFunction γ it init Pl wf f
simp +instances only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
simp only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
rw [IterM.DefaultConsumers.forIn'.wf]
split; rotate_left
· simp only [IterM.step_eq,
@@ -1170,7 +1170,7 @@ instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α] [LT α] [Decidabl
LawfulIteratorLoop (Rxo.Iterator α) Id n where
lawful := by
intro lift instLawfulMonadLiftFunction γ it init Pl wf f
simp +instances only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
simp only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
rw [IterM.DefaultConsumers.forIn'.wf]
split; rotate_left
· simp [IterM.step_eq, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure (liftBind := lift)]
@@ -1635,7 +1635,7 @@ instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α]
LawfulIteratorLoop (Rxi.Iterator α) Id n where
lawful := by
intro lift instLawfulMonadLiftFunction γ it init Pl wf f
simp +instances only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
simp only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
rw [IterM.DefaultConsumers.forIn'.wf]
split; rotate_left
· simp [Monadic.step_eq_step, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure]

20
src/Init/Data/Range/Polymorphic/SInt.lean
View File

@@ -248,6 +248,16 @@ instance : HasModel Int8 (BitVec 8) where
le_iff_encode_le := by simp [LE.le, Int8.le]
lt_iff_encode_lt := by simp [LT.lt, Int8.lt]
private theorem succ?_eq_minValueSealed {x : Int8} :
UpwardEnumerable.succ? x = if x + 1 = minValueSealed then none else some (x + 1) :=
(rfl)
private theorem succMany?_eq_maxValueSealed {i : Int8} :
UpwardEnumerable.succMany? n i =
have := i.minValue_le_toInt
if h : i.toInt + n ≤ maxValueSealed.toInt then some (.ofIntLE _ (by omega) (maxValueSealed_def ▸ h)) else none :=
(rfl)
theorem instUpwardEnumerable_eq :
instUpwardEnumerable = HasModel.instUpwardEnumerable := by
apply UpwardEnumerable.ext
@@ -255,16 +265,16 @@ theorem instUpwardEnumerable_eq :
apply HasModel.succ?_eq_of_technicalCondition
simp [HasModel.encode, succ?, ← Int8.toBitVec_inj, toBitVec_minValueSealed_eq_intMinSealed]
· ext
simp +instances [HasModel.succMany?_eq, instUpwardEnumerable, HasModel.encode, HasModel.decode,
simp [HasModel.succMany?_eq, succMany?_eq_maxValueSealed, HasModel.encode, HasModel.decode,
← toInt_toBitVec, toBitVec_maxValueSealed_eq_intMaxSealed, ofIntLE_eq_ofInt]
instance : LawfulUpwardEnumerable Int8 := by
simp +instances only [instUpwardEnumerable_eq]
rw [instUpwardEnumerable_eq]
infer_instance
instance : LawfulUpwardEnumerableLE Int8 := by
simp +instances only [instUpwardEnumerable_eq]
rw [instUpwardEnumerable_eq]
infer_instance
public instance instRxcHasSize : Rxc.HasSize Int8 where
@@ -276,7 +286,7 @@ theorem instRxcHasSize_eq :
← toInt_toBitVec, HasModel.toNat_toInt_add_one_sub_toInt (Nat.zero_lt_succ _)]
public instance instRxcLawfulHasSize : Rxc.LawfulHasSize Int8 := by
simp +instances only [instUpwardEnumerable_eq, instRxcHasSize_eq]
rw [instUpwardEnumerable_eq, instRxcHasSize_eq]
infer_instance
public instance : Rxc.IsAlwaysFinite Int8 := by exact inferInstance
@@ -293,7 +303,7 @@ theorem instRxiHasSize_eq :
HasModel.encode, HasModel.toNat_two_pow_sub_one_sub_toInt (show 8 > 0 by omega)]
public instance instRxiLawfulHasSize : Rxi.LawfulHasSize Int8 := by
simp +instances only [instUpwardEnumerable_eq, instRxiHasSize_eq]
rw [instUpwardEnumerable_eq, instRxiHasSize_eq]
infer_instance
public instance instRxiIsAlwaysFinite : Rxi.IsAlwaysFinite Int8 := by exact inferInstance

14
src/Init/Data/Slice/List/Lemmas.lean
View File

@@ -77,9 +77,9 @@ public theorem toList_mkSlice_rco {xs : List α} {lo hi : Nat} :
simp only [Std.Rco.Sliceable.mkSlice, toSlice, ListSlice.toList_eq]
by_cases h : lo < hi
· have : lo ≤ hi := by omega
simp +instances [h, List.take_drop, Nat.add_sub_cancel' ‹_›, ← List.take_eq_take_min]
simp [h, List.take_drop, Nat.add_sub_cancel' ‹_›, ← List.take_eq_take_min]
· have : min hi xs.length ≤ lo := by omega
simp +instances [h, Nat.min_eq_right this]
simp [h, Nat.min_eq_right this]
@[simp, grind =]
public theorem toArray_mkSlice_rco {xs : List α} {lo hi : Nat} :
@@ -114,7 +114,7 @@ public theorem size_mkSlice_rcc {xs : List α} {lo hi : Nat} :
public theorem toList_mkSlice_rci {xs : List α} {lo : Nat} :
xs[lo...*].toList = xs.drop lo := by
rw [List.drop_eq_drop_min]
simp +instances [ListSlice.toList_eq, Std.Rci.Sliceable.mkSlice, List.toUnboundedSlice]
simp [ListSlice.toList_eq, Std.Rci.Sliceable.mkSlice, List.toUnboundedSlice]
@[simp, grind =]
public theorem toArray_mkSlice_rci {xs : List α} {lo : Nat} :
@@ -291,7 +291,8 @@ namespace ListSlice
@[simp, grind =]
public theorem toList_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
xs[lo...hi].toList = (xs.toList.take hi).drop lo := by
simp +instances only [instSliceableListSliceNat_1, List.toList_mkSlice_rco, ListSlice.toList_eq (xs := xs)]
rw [instSliceableListSliceNat_1]
simp only [List.toList_mkSlice_rco, ListSlice.toList_eq (xs := xs)]
obtain ⟨⟨xs, stop⟩⟩ := xs
cases stop
· simp
@@ -329,9 +330,10 @@ public theorem size_mkSlice_rcc {xs : ListSlice α} {lo hi : Nat} :
@[simp, grind =]
public theorem toList_mkSlice_rci {xs : ListSlice α} {lo : Nat} :
xs[lo...*].toList = xs.toList.drop lo := by
simp +instances only [instSliceableListSliceNat_2, ListSlice.toList_eq (xs := xs)]
rw [instSliceableListSliceNat_2]
simp only [ListSlice.toList_eq (xs := xs)]
obtain ⟨⟨xs, stop⟩⟩ := xs
simp +instances only
simp only
split <;> simp
@[simp, grind =]