chore: update DTreeMap proofs with more unfolding induction (#8382)

This is a post-stage0 update following #8359.

Author: nomeata

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

@@ -529,9 +529,8 @@ attribute [Std.Internal.tree_tac] and_true true_and and_self heq_eq_eq inner.inj
 theorem balance!_eq_balanceₘ {k v} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced)
     (hlr : BalanceLErasePrecond l.size r.size ∨ BalanceLErasePrecond r.size l.size) :
     balance! k v l r = balanceₘ k v l r := by
-  set_option tactic.fun_induction.unfolding false in
   fun_cases balance!
-  all_goals dsimp only [balance!, balanceₘ]
+  all_goals dsimp only [balanceₘ]
   · rfl
   · split <;> simp_all [Std.Internal.tree_tac]
   · split <;> simp_all only [Std.Internal.tree_tac]
@@ -579,7 +578,7 @@ theorem balance!_eq_balanceₘ {k v} {l r : Impl α β} (hlb : l.Balanced) (hrb
       omega
   · rw [rotateL]
     repeat simp_all only [Std.Internal.tree_tac, dite_true, ite_false, ite_true, Nat.not_lt]
-    rw [if_neg (by omega), if_neg (by omega), if_neg (by omega)]
+    rw [if_neg (by omega), if_neg (by omega)]
     simp only [Std.Internal.tree_tac, Nat.add_right_cancel_iff] at *
     omega
   · exfalso
@@ -651,45 +650,30 @@ 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
-  set_option tactic.fun_induction.unfolding false in
-  fun_cases rotateL k v l rk rv rl rr <;> dsimp only [rotateL]
-  · split
-    · next h =>
-      exact balanced_singleL _ _ _ _ _ _ _ _ hl hr hlr hh h
-    · contradiction
-  · rw [if_neg ‹_›]
-    tree_tac
-  · rw [if_neg ‹_›]
-    exact balanced_doubleL k v _ _ _ _ _ _ _ _ _ _ hl hr hlr hh ‹_›
+  fun_cases rotateL
+  · exact balanced_singleL _ _ _ _ _ _ _ _ hl hr hlr hh ‹_›
+  · tree_tac
+  · exact balanced_doubleL k v _ _ _ _ _ _ _ _ _ _ hl hr hlr hh ‹_›
 
 theorem balanced_rotateR (k v ls lk lv ll lr r) (hl : (Impl.inner ls lk lv ll lr).Balanced)
     (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
-  set_option tactic.fun_induction.unfolding false in
-  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
-    · contradiction
-  · rw [if_neg ‹_›]
-    tree_tac
-  · rw [if_neg ‹_›]
-    exact balanced_doubleR k v _ _ _ _ _ _ _ _ _ _ hl hr hlr hh ‹_›
+  fun_cases rotateR
+  · exact balanced_singleR k v _ _ _ _ _ _ hl hr hlr hh ‹_›
+  · tree_tac
+  · exact balanced_doubleR k v _ _ _ _ _ _ _ _ _ _ hl hr hlr hh ‹_›
 
 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
-  set_option tactic.fun_induction.unfolding false in
-  fun_cases balanceL k v l r hlb hrb hlr
-  all_goals dsimp only [balanceL, balanceLErase]
-  split
-  · split <;> contradiction
-  · rfl
+  fun_cases balanceL
+  all_goals dsimp only [balanceLErase]
+  all_goals simp only [↓reduceDIte, ↓reduceIte, *]
 
 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
-  fun_cases balanceL! k v l r
-  all_goals dsimp only [balanceLErase, balanceL!]
+  fun_cases balanceL!
+  all_goals dsimp only [balanceLErase]
   all_goals simp only [*]
   all_goals dsimp only [dreduceDIte, dreduceIte]
   all_goals contradiction
@@ -698,26 +682,20 @@ theorem balanceL!_eq_balance! {k : α} {v : β k} {l r : Impl α β} (hlb : l.Ba
     (hrb : r.Balanced) (hlr : BalanceLErasePrecond l.size r.size) :
     balanceL! k v l r = balance! k v l r := by
   fun_cases balance!
-  all_goals dsimp only [balanceL!, balance!]
+  all_goals dsimp only [balanceL!]
   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)
   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
-  set_option tactic.fun_induction.unfolding false in
-  fun_cases balanceR k v l r hlb hrb hlr
-  all_goals dsimp only [balanceR, balanceRErase]
-  split
-  · split <;> contradiction
-  · rfl
+  fun_cases balanceR <;>
+    simp only [balanceRErase, ↓reduceDIte, ↓reduceIte, *]
 
 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
-  fun_cases balanceR! k v l r
+  fun_cases balanceR!
   all_goals dsimp only [balanceRErase, balanceR!]
   all_goals simp only [*]
   all_goals dsimp only [dreduceDIte, dreduceIte]
@@ -726,22 +704,16 @@ theorem balanceRErase_eq_balanceR! {k : α} {v : β k} {l r : Impl α β} {hlb h
 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
-  fun_cases balance! k v l r
-  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
+  fun_cases balance!
+  all_goals dsimp only [balanceR!]
   all_goals try (exfalso; tree_tac; done)
   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
-  set_option tactic.fun_induction.unfolding false in
-  fun_cases balance! k v l r
-  all_goals dsimp only [balance, balance!]
-  all_goals simp only [*]
-  all_goals dsimp only [dreduceDIte]
+  fun_cases balance!
+  all_goals dsimp only [balance]
+  all_goals simp only [↓reduceDIte, ↓reduceIte, *]
   all_goals contradiction
 
 theorem balance_eq_inner [Ord α] {sz k v} {l r : Impl α β}

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

@@ -686,29 +686,13 @@ theorem insertMax_eq_insertMax! [Ord α] {a b} {t : Impl α β} (htb) :
 
 theorem link_eq_link! [Ord α] {k v} {l r : Impl α β} (hlb hrb) :
     (link k v l r hlb hrb).impl = link! k v l r := by
-  set_option tactic.fun_induction.unfolding false in
-  fun_cases link! <;> rw [link, link!]
-  · rw [insertMin_eq_insertMin!]
-  · rw [insertMax_eq_insertMax!]
-  · split <;> simp only [balanceLErase_eq_balanceL!, link_eq_link! hlb hrb.left]
-  · split <;> simp only [balanceRErase_eq_balanceR!, balanceLErase_eq_balanceL!,
-      link_eq_link! hlb hrb.left, link_eq_link! hlb.right hrb]
-  · split
-    · simp only [balanceLErase_eq_balanceL!, link_eq_link! hlb hrb.left]
-    · simp only [Std.Internal.tree_tac]
-termination_by sizeOf l + sizeOf r
+  fun_induction link! <;>
+    simp [*, link, balanceLErase_eq_balanceL!, balanceRErase_eq_balanceR!, insertMin_eq_insertMin!, insertMax_eq_insertMax!, size]
 
 theorem link2_eq_link2! [Ord α] {l r : Impl α β} (hlb hrb) :
     (link2 l r hlb hrb).impl = link2! l r := by
-  set_option tactic.fun_induction.unfolding false in
-  fun_cases link2! <;> rw [link2!, link2]
-  · split <;> simp only [balanceLErase_eq_balanceL!, link2_eq_link2! hlb hrb.left]
-  · split <;> simp only [balanceRErase_eq_balanceR!, balanceLErase_eq_balanceL!,
-      link2_eq_link2! hlb.right hrb, link2_eq_link2! hlb hrb.left]
-  · split
-    · simp only [balanceLErase_eq_balanceL!, link2_eq_link2! hlb hrb.left]
-    · simp only [Std.Internal.tree_tac, glue_eq_glue!]
-termination_by sizeOf l + sizeOf r
+  fun_induction link2! <;>
+    simp [*, link2, balanceLErase_eq_balanceL!, balanceRErase_eq_balanceR!, glue_eq_glue!]
 
 namespace Const