max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update code after #7110

Browse source
This commit is contained in:
Joachim Breitner 2025-02-17 17:18:32 +01:00 • committed by Sebastian Ullrich
parent 1a374ceab2
commit 2cdf4b14e1
2 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Init/Internal/Order/Lemmas.lean
View file

@ -351,7 +351,7 @@ theorem monotone_forIn'_loop {α : Type uu}
monotone (fun x => Array.forIn'.loop as (f x) i h b) := by
induction i, h, b using Array.forIn'.loop.induct with
| case1 => apply monotone_const
| case2 _ _ _ _ _ _ _ ih =>
| case2 _ _ _ _ _ _ ih =>
apply monotone_bind
· apply monotone_apply
apply monotone_apply
@ -424,7 +424,7 @@ theorem monotone_foldrM_fold
unfold Array.foldrM.fold
simp only [↓reduceIte, *]
apply monotone_const
| case3 _ _ _ _ _ _ ih =>
| case3 _ _ _ _ _ ih =>
unfold Array.foldrM.fold
simp only [reduceCtorEq, ↓reduceIte, *]
apply monotone_bind
@ -601,7 +601,7 @@ theorem monotone_findSomeRevM?
| case1 =>
unfold Array.findSomeRevM?.find
apply monotone_const
| case2 _ _ _ _ ih =>
| case2 _ _ _ ih =>
unfold Array.findSomeRevM?.find
apply monotone_bind
· apply monotone_apply

8
src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
View file

@ -245,25 +245,25 @@ theorem toListModel_updateCell [Ord α] [TransOrd α] {k : α}
induction l, hlb using updateCell.induct k f
· simp_all [updateCell]
· simp_all [updateCell]
· rename_i sz k' v' l r hb hcmp l' hl'₁ hl'₂ hl'₃ hup hb' ih
· rename_i sz k' v' l r hb hcmp l' hl'₁ hl'₂ hl'₃ hup ih
simp only [updateCell, hcmp]
split <;> rename_i hcmp' <;> try (simp [hcmp] at hcmp'; done)
rw [toListModel_balance, toListModel_filter_gt_of_lt hcmp hlo,
toListModel_filter_lt_of_lt hcmp hlo, findCell_of_lt hcmp hlo, ih hlo.left]
simp
· rename_i sz k' v' l r hl hcmp hf hl'
· rename_i sz k' v' l r hl hcmp hf
simp only [updateCell, hcmp, hf]
split <;> rename_i hcmp' <;> try (simp [hcmp] at hcmp'; done)
rw [toListModel_glue, toListModel_filter_gt_of_eq hcmp hlo, findCell_of_eq hcmp hlo,
hf, toListModel_filter_lt_of_eq hcmp hlo]
simp
· rename_i sz k' v' l r hl hcmp k'' v'' hf hl'
· rename_i sz k' v' l r hl hcmp k'' v'' hf
simp only [updateCell, hcmp, hf]
split <;> rename_i hcmp' <;> try (simp [hcmp] at hcmp'; done)
rw [toListModel_inner, toListModel_filter_gt_of_eq hcmp hlo, findCell_of_eq hcmp hlo,
toListModel_filter_lt_of_eq hcmp hlo, hf]
simp
· rename_i sz k' v' l r hb hcmp l' hl'₁ hl'₂ hl'₃ hup hb' ih
· rename_i sz k' v' l r hb hcmp l' hl'₁ hl'₂ hl'₃ hup ih
simp only [updateCell, hcmp]
split <;> rename_i hcmp' <;> try (simp [hcmp] at hcmp'; done)
rw [toListModel_filter_gt_of_gt hcmp hlo, findCell_of_gt hcmp hlo,