perf: reduce elaboration time and proof size of tree map internals (#7459)

There are several things done here:
1. Use the modified `simp_to_model` which already exists in hash maps.
This version of `simp_to_model` allows specifying the query operations
to use in addition to the modifying operations. This is mostly to
improve elaboration time and actually increases olean size.
2. Instead of proving `toListModel_balance` directly, we write
`toListModel_balanceₘ` and use that instead (this saves ~3 MB).
3. Use `fun_cases` and `dsimp` instead of `rw [x.eq_def]` more
frequently in `Balancing.olean` (this saves a bit over 2 MB).
4. Mark `updateCell` and other functions dependent on it as
`noncomputable`. The main problem with `updateCell` is how other
functions, in particular `glue`, get recursively inlined, which blows
the size of the IR (this saves ~1 MB).
5. Instead of using `simp_to_model` to prove results on `insert!`,
`erase!`, etc., `simpa`s are used now, e.g. `simpa only
[insert_eq_insert!] using isEmpty_insert h`. This mainly improves
elaboration time although the olean size also goes down by ~0.3 MB.

Author: Rob23oba

src/Std/Data/DHashMap/Internal/RawLemmas.lean

@@ -2702,7 +2702,7 @@ theorem getKey!_modify_self (h : m.1.WF) [Inhabited α] {k : α} {f : β k → 
 theorem getKey_modify (h : m.1.WF) [Inhabited α] {k k' : α} {f : β k → β k}
     (hc : (m.modify k f).contains k') :
     (m.modify k f).getKey k' hc =
-      if heq : k == k' then
+      if k == k' then
         k
       else
         haveI h' : m.contains k' := by rwa [contains_modify _ h] at hc
@@ -2827,7 +2827,7 @@ theorem getKey!_modify_self (h : m.1.WF) [Inhabited α] {k : α} {f : β → β}
 theorem getKey_modify (h : m.1.WF) [Inhabited α] {k k' : α} {f : β → β}
     (hc : (Const.modify m k f).contains k') :
     (Const.modify m k f).getKey k' hc =
-      if heq : k == k' then
+      if k == k' then
         k
       else
         haveI h' : m.contains k' := by rwa [contains_modify _ h] at hc

src/Std/Data/DHashMap/RawLemmas.lean

@@ -43,8 +43,7 @@ private def baseNames : Array Name :=
     ``getKey?_eq, ``getKey_eq, ``getKey!_eq, ``getKeyD_eq,
     ``insertMany_eq, ``Const.insertMany_eq, ``Const.insertManyIfNewUnit_eq,
     ``ofList_eq, ``Const.ofList_eq, ``Const.unitOfList_eq,
-    ``alter_eq, ``Const.alter_eq, ``modify_eq, ``Const.modify_eq,
-    ``Subtype.eta]
+    ``alter_eq, ``Const.alter_eq, ``modify_eq, ``Const.modify_eq]
 
 /-- Internal implementation detail of the hash map -/
 scoped syntax "simp_to_raw" ("using" term)? : tactic
@@ -55,7 +54,7 @@ macro_rules
 | `(tactic| simp_to_raw $[using $using?]?) => do
   `(tactic|
     (try simp (discharger := with_reducible wf_trivial) only [$[$(Array.map Lean.mkIdent baseNames):term],*]
-     $[apply $(using?.toArray):term];*)
+     $[with_reducible apply $(using?.toArray):term];*)
      <;> with_reducible try wf_trivial)
 
 end Internal.Raw
@@ -2857,15 +2856,14 @@ theorem getKey!_modify_self [LawfulBEq α] [Inhabited α] {k : α} {f : β k →
   simp_to_raw using Raw₀.getKey!_modify_self
 
 theorem getKey_modify [LawfulBEq α] [Inhabited α] {k k' : α} {f : β k → β k}
-    (h : m.WF) {hc : k' ∈ m.modify k f} :
+    (h : m.WF) : {hc : k' ∈ m.modify k f} →
     (m.modify k f).getKey k' hc =
       if k == k' then
         k
       else
         haveI h' : k' ∈ m := mem_modify h |>.mp hc
         m.getKey k' h' := by
-  simp only [mem_iff_contains] at hc
-  revert hc
+  simp only [mem_iff_contains]
   simp_to_raw using Raw₀.getKey_modify
 
 @[simp]
@@ -3003,15 +3001,14 @@ theorem getKey!_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k
   simp_to_raw using Raw₀.Const.getKey!_modify_self
 
 theorem getKey_modify [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β}
-    (h : m.WF) {hc : k' ∈ Const.modify m k f} :
+    (h : m.WF) : {hc : k' ∈ Const.modify m k f} →
     (Const.modify m k f).getKey k' hc =
       if k == k' then
         k
       else
         haveI h' : k' ∈ m := mem_modify h |>.mp hc
         m.getKey k' h' := by
-  simp only [mem_iff_contains] at hc
-  revert hc
+  simp only [mem_iff_contains]
   simp_to_raw using Raw₀.Const.getKey_modify
 
 @[simp]

src/Std/Data/DTreeMap/Internal/Balancing.lean

@@ -530,8 +530,7 @@ theorem balance!_eq_balanceₘ {k v} {l r : Impl α β} (hlb : l.Balanced) (hrb
     (hlr : BalanceLErasePrecond l.size r.size ∨ BalanceLErasePrecond r.size l.size) :
     balance! k v l r = balanceₘ k v l r := by
   cases k, v, l, r using balance!.fun_cases
-  all_goals
-    simp only [balance!, balanceₘ]
+  all_goals dsimp only [balance!, balanceₘ]
   · rfl
   · split <;> simp_all [Std.Internal.tree_tac]
   · split <;> simp_all only [Std.Internal.tree_tac]
@@ -655,7 +654,7 @@ theorem balanced_rotateL (k v l rs rk rv rl rr) (hl : l.Balanced)
     (hlr : BalanceLErasePrecond l.size rs ∨ BalanceLErasePrecond rs l.size)
     (hh : rs > delta * l.size) :
     (rotateL k v l rk rv rl rr : Impl α β).Balanced := by
-  cases k, v, l, rk, rv, rl, rr using rotateL.fun_cases <;> simp only [rotateL]
+  fun_cases rotateL k v l rk rv rl rr <;> dsimp only [rotateL]
   · split
     · next h =>
       exact balanced_singleL _ _ _ _ _ _ _ _ hl hr hlr hh h
@@ -669,7 +668,7 @@ theorem balanced_rotateR (k v ls lk lv ll lr r) (hl : (Impl.inner ls lk lv ll lr
     (hr : r.Balanced) (hlr : BalanceLErasePrecond ls r.size ∨ BalanceLErasePrecond r.size ls)
     (hh : ls > delta * r.size) :
     (rotateR k v lk lv ll lr r : Impl α β).Balanced := by
-  cases k, v, lk, lv, ll, lr, r using rotateR.fun_cases <;> simp only [rotateR]
+  fun_cases rotateR k v lk lv ll lr r <;> dsimp only [rotateR]
   · split
     · next h =>
       exact balanced_singleR k v _ _ _ _ _ _ hl hr hlr hh h
@@ -681,89 +680,79 @@ theorem balanced_rotateR (k v ls lk lv ll lr r) (hl : (Impl.inner ls lk lv ll lr
 
 theorem balanceL_eq_balanceLErase {k : α} {v : β k} {l r : Impl α β} {hlb hrb hlr} :
     balanceL k v l r hlb hrb hlr = balanceLErase k v l r hlb hrb hlr.erase := by
-  rw [balanceL.eq_def, balanceLErase.eq_def]
+  fun_cases balanceL k v l r hlb hrb hlr
+  all_goals dsimp only [balanceL, balanceLErase]
+  contradiction
   split
-  · dsimp only
-    split
-    all_goals dsimp only
-    contradiction
-  · dsimp only
-    split
-    all_goals dsimp only
-    split
-    · split
-      · dsimp only
-      · contradiction
-      · contradiction
-    · rfl
+  · split <;> contradiction
+  · rfl
 
 theorem balanceLErase_eq_balanceL! {k : α} {v : β k} {l r : Impl α β} {hlb hrb hlr} :
     balanceLErase k v l r hlb hrb hlr = balanceL! k v l r := by
-  rw [balanceLErase.eq_def, balanceL!.eq_def]
-  repeat' (split; dsimp)
-  all_goals try contradiction
-  all_goals simp_all [-Nat.not_lt]
+  fun_cases balanceL! k v l r
+  all_goals dsimp only [balanceLErase, balanceL!]
+  all_goals simp only [*]
+  all_goals dsimp only [dreduceDIte, dreduceIte]
+  all_goals contradiction
 
 theorem balanceL!_eq_balance! {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced)
     (hrb : r.Balanced) (hlr : BalanceLErasePrecond l.size r.size) :
     balanceL! k v l r = balance! k v l r := by
   cases k, v, l, r using balance!.fun_cases
-  all_goals
-    simp only [balanceL!, balance!, *, if_true, if_false, true_and, size_inner, size_leaf]
+  all_goals dsimp only [balanceL!, balance!]
+  all_goals try simp only [*]
+  all_goals try dsimp only [dreduceDIte, dreduceIte]
   all_goals try rfl
   all_goals try contradiction
   all_goals try (exfalso; tree_tac; done)
-  all_goals congr; tree_tac
+  congr; tree_tac
 
 theorem balanceR_eq_balanceRErase {k : α} {v : β k} {l r : Impl α β} {hlb hrb hlr} :
     balanceR k v l r hlb hrb hlr = balanceRErase k v l r hlb hrb hlr.erase := by
-  rw [balanceR.eq_def, balanceRErase.eq_def]
+  fun_cases balanceR k v l r hlb hrb hlr
+  all_goals dsimp only [balanceR, balanceRErase]
+  contradiction
   split
-  · dsimp only
-    split
-    all_goals dsimp only
-    contradiction
-  · dsimp only
-    split
-    all_goals dsimp only
-    split
-    · split
-      · dsimp only
-      · contradiction
-      · contradiction
-    · rfl
+  · split <;> contradiction
+  · rfl
 
 theorem balanceRErase_eq_balanceR! {k : α} {v : β k} {l r : Impl α β} {hlb hrb hlr} :
     balanceRErase k v l r hlb hrb hlr = balanceR! k v l r := by
-  rw [balanceRErase.eq_def, balanceR!.eq_def]
-  repeat' (split; dsimp)
-  all_goals try contradiction
-  all_goals simp_all [-Nat.not_lt]
+  fun_cases balanceR! k v l r
+  all_goals dsimp only [balanceRErase, balanceR!]
+  all_goals simp only [*]
+  all_goals dsimp only [dreduceDIte, dreduceIte]
+  all_goals contradiction
 
 theorem balanceR!_eq_balance! {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced)
     (hrb : r.Balanced) (hlr : BalanceLErasePrecond r.size l.size) :
     balanceR! k v l r = balance! k v l r := by
   cases k, v, l, r using balance!.fun_cases
-  all_goals
-    simp only [balanceR!, balance!, *, if_true, if_false, true_and, size_inner, size_leaf]
+  all_goals dsimp only [balanceR!, balance!]
+  all_goals try simp only [*]
+  all_goals try dsimp only [dreduceDIte, dreduceIte]
   all_goals try rfl
   all_goals try contradiction
   all_goals try (exfalso; tree_tac; done)
-  all_goals congr; tree_tac
+  congr; tree_tac
 
 theorem balance_eq_balance! {k : α} {v : β k} {l r : Impl α β} {hlb hrb hlr} :
     balance k v l r hlb hrb hlr = balance! k v l r := by
-  rw [balance.eq_def, balance!.eq_def]
-  repeat' (split; dsimp)
-  all_goals try contradiction
-  all_goals simp_all [-Nat.not_lt]
+  fun_cases balance! k v l r
+  all_goals dsimp only [balance, balance!]
+  all_goals simp only [*]
+  all_goals dsimp only [dreduceDIte]
+  all_goals contradiction
 
 theorem balance_eq_inner [Ord α] {sz k v} {l r : Impl α β}
     (hl : (inner sz k v l r).Balanced) {h} :
     balance k v l r hl.left hl.right h = inner sz k v l r := by
   rw [balance_eq_balance!, balance!_eq_balanceₘ hl.left hl.right h, balanceₘ]
   have hl' := balanced_inner_iff.mp hl
-  fun_cases balanceₘ k v l r <;> tree_tac
+  rw [hl'.2.2.2]
+  split; rfl
+  replace hl' := hl'.2.2.1.resolve_left ‹_›
+  simp only [Nat.not_lt_of_le, hl'.1, hl'.2, reduceDIte, bin]
 
 theorem balance!_desc {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced)
     (hlr : BalanceLErasePrecond l.size r.size ∨ BalanceLErasePrecond r.size l.size) :