From edcad9a14b98e6af134dc2afb276cb42e8a2417c Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 6 May 2025 19:10:45 +0200
Subject: [PATCH] chore: post-stage0 fixes for #8171 (#8250)

---
 src/Lean/Meta/Tactic/FunInd.lean              | 40 ++++++++-----------
 src/Std/Data/DTreeMap/Internal/Balancing.lean | 10 -----
 stage0/src/stdlib_flags.h                     |  2 +
 3 files changed, 19 insertions(+), 33 deletions(-)

diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean
index 1371e1b088..d90ee7f0f4 100644
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@@ -203,11 +203,6 @@ something goes wrong, one still gets a useful induction principle, just maybe wi
 not fully simplified.
 -/
 
-register_builtin_option backward.funind.contradiction : Bool := {
-  defValue := true
-  descr    := "omit cases by contradiction (temporary bootstrap option)"
-}
-
 set_option autoImplicit false
 
 namespace Lean.Tactic.FunInd
@@ -727,24 +722,23 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
 
   -- Check for unreachable cases. We look for the kind of expressions that `by contradiction`
   -- produces
-  if backward.funind.contradiction.get (← getOptions) then
-    match_expr e with
-    | False.elim _ h => do
-      return ← mkFalseElim goal h
-    | absurd _ _ h₁ h₂ => do
-      return ← mkAbsurd goal h₁ h₂
-    | _ => pure ()
-    if e.isApp && e.getAppFn.isConst && isNoConfusion (← getEnv) e.getAppFn.constName! then
-      let arity := (← inferType e.getAppFn).getNumHeadForalls -- crucially not reducing the noConfusionType in the type
-      let h := e.getArg! (arity - 1)
-      let hType ← inferType h
-      -- The following duplicates a bit of code from the contradiction tactic, maybe worth extracting
-      -- into a common helper at some point
-      if let some (_, lhs, rhs) ← matchEq? hType then
-        if let some lhsCtor ← matchConstructorApp? lhs then
-        if let some rhsCtor ← matchConstructorApp? rhs then
-        if lhsCtor.name != rhsCtor.name then
-          return (← mkNoConfusion goal h)
+  match_expr e with
+  | False.elim _ h => do
+    return ← mkFalseElim goal h
+  | absurd _ _ h₁ h₂ => do
+    return ← mkAbsurd goal h₁ h₂
+  | _ => pure ()
+  if e.isApp && e.getAppFn.isConst && isNoConfusion (← getEnv) e.getAppFn.constName! then
+    let arity := (← inferType e.getAppFn).getNumHeadForalls -- crucially not reducing the noConfusionType in the type
+    let h := e.getArg! (arity - 1)
+    let hType ← inferType h
+    -- The following duplicates a bit of code from the contradiction tactic, maybe worth extracting
+    -- into a common helper at some point
+    if let some (_, lhs, rhs) ← matchEq? hType then
+      if let some lhsCtor ← matchConstructorApp? lhs then
+      if let some rhsCtor ← matchConstructorApp? rhs then
+      if lhsCtor.name != rhsCtor.name then
+        return (← mkNoConfusion goal h)
 
   -- we look in to `PProd.mk`, as it occurs in the mutual structural recursion construction
   match_expr goal with
diff --git a/src/Std/Data/DTreeMap/Internal/Balancing.lean b/src/Std/Data/DTreeMap/Internal/Balancing.lean
index 364adddc4f..d79e7ba716 100644
--- a/src/Std/Data/DTreeMap/Internal/Balancing.lean
+++ b/src/Std/Data/DTreeMap/Internal/Balancing.lean
@@ -7,10 +7,6 @@ prelude
 import Init.Data.AC
 import Std.Data.DTreeMap.Internal.Balanced
 
--- Temporary bootstrapping fix
-#guard_msgs(drop error) in
-set_option backward.funind.contradiction false
-
 /-!
 # Balancing operations
 
@@ -686,7 +682,6 @@ theorem balanceL_eq_balanceLErase {k : α} {v : β k} {l r : Impl α β} {hlb hr
     balanceL k v l r hlb hrb hlr = balanceLErase k v l r hlb hrb hlr.erase := by
   fun_cases balanceL k v l r hlb hrb hlr
   all_goals dsimp only [balanceL, balanceLErase]
-  contradiction
   split
   · split <;> contradiction
   · rfl
@@ -715,7 +710,6 @@ theorem balanceR_eq_balanceRErase {k : α} {v : β k} {l r : Impl α β} {hlb hr
     balanceR k v l r hlb hrb hlr = balanceRErase k v l r hlb hrb hlr.erase := by
   fun_cases balanceR k v l r hlb hrb hlr
   all_goals dsimp only [balanceR, balanceRErase]
-  contradiction
   split
   · split <;> contradiction
   · rfl
@@ -765,15 +759,11 @@ theorem balance!_desc {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced)
   fun_cases balanceₘ k v l r
   · rw [if_pos ‹_›, bin, balanced_inner_iff]
     exact ⟨rfl, hlb, hrb, Or.inl ‹_›, rfl⟩
-  · rw [if_neg ‹_›, dif_pos ‹_›]
-    contradiction
   · rw [if_neg ‹_›, dif_pos ‹_›]
     simp only [size_rotateL (.left ‹_›), size_bin, size_inner]
     rw [← Balanced.eq ‹_›]
     refine ⟨rfl, ?_⟩
     apply balanced_rotateL <;> assumption
-  · simp only [delta, size_leaf] at *
-    omega
   · rw [if_neg ‹_›, dif_neg ‹_›, dif_pos ‹_›]
     simp only [size_rotateR (.right ‹_›), size_bin, size_inner]
     rw [← Balanced.eq ‹_›]
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index b64fc2dae6..6d6bf38615 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// please update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;