Add files using upload-large-folder tool

backend/core/leanprover--lean4---v4.22.0/src/lean/Lean/Elab/Tactic/Do/ProofMode/LeftRight.lean

@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König, Mario Carneiro, Sebastian Graf
+-/
+prelude
+import Std.Tactic.Do.Syntax
+import Lean.Elab.Tactic.Do.ProofMode.MGoal
+
+namespace Lean.Elab.Tactic.Do.ProofMode
+open Std.Do
+open Lean Elab Tactic Meta
+
+def mLeftRightCore (right : Bool) (mvar : MVarId) : MetaM MVarId := do
+  let g ← instantiateMVars <| ← mvar.getType
+  let some goal := parseMGoal? g | throwError "not in proof mode"
+
+  let mkApp3 (.const ``SPred.or []) σs L R := goal.target | throwError "target is not SPred.or"
+
+  let (thm, keep) := if right then (``SPred.or_intro_r', R) else (``SPred.or_intro_l', L)
+
+  let newGoal ← mkFreshExprSyntheticOpaqueMVar {goal with target := keep}.toExpr
+  mvar.assign (mkApp5 (mkConst thm) σs goal.hyps L R newGoal)
+  return newGoal.mvarId!
+
+@[builtin_tactic Lean.Parser.Tactic.mleft]
+def elabMLeft : Tactic | _ => do
+  let mvar ← getMainGoal
+  mvar.withContext do
+  let newGoal ← mLeftRightCore (right := false) mvar
+  replaceMainGoal [newGoal]
+
+@[builtin_tactic Lean.Parser.Tactic.mright]
+def elabMRight : Tactic | _ => do
+  let mvar ← getMainGoal
+  mvar.withContext do
+  let newGoal ← mLeftRightCore (right := true) mvar
+  replaceMainGoal [newGoal]

backend/core/leanprover--lean4---v4.22.0/src/lean/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean

@@ -0,0 +1,154 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König, Mario Carneiro, Sebastian Graf
+-/
+prelude
+import Std.Do.SPred.DerivedLaws
+import Std.Tactic.Do.ProofMode
+import Lean.Meta
+
+namespace Lean.Elab.Tactic.Do.ProofMode
+
+open Lean Elab Meta
+open Std.Do Std.Tactic.Do
+
+@[match_pattern] def nameAnnotation := `name
+@[match_pattern] def uniqAnnotation := `uniq
+
+structure Hyp where
+  name : Name
+  uniq : Name -- for display purposes only
+  p : Expr
+
+def parseHyp? : Expr → Option Hyp
+  | .mdata ⟨[(nameAnnotation, .ofName name), (uniqAnnotation, .ofName uniq)]⟩ p =>
+    some ⟨name, uniq, p⟩ -- NB: mdatas are transparent to SubExpr; hence no pos.push
+  | _ => none
+
+def Hyp.toExpr (hyp : Hyp) : Expr :=
+  .mdata ⟨[(nameAnnotation, .ofName hyp.name), (uniqAnnotation, .ofName hyp.uniq)]⟩ hyp.p
+
+-- set_option pp.all true in
+-- #check ⌜True⌝
+def emptyHyp (σs : Expr) : Expr := -- ⌜True⌝ standing in for an empty conjunction of hypotheses
+  mkApp3 (mkConst ``SVal.curry) (.sort .zero) σs <| mkLambda `escape .default (mkApp (mkConst ``SVal.StateTuple) σs) (mkConst ``True)
+def parseEmptyHyp? : Expr → Option Expr
+  | mkApp3 (.const ``SVal.curry _) (.sort .zero) σs (.lam _ _ (.const ``True _) _) => some σs
+  | _ => none
+
+def pushLeftConjunct (pos : SubExpr.Pos) : SubExpr.Pos :=
+  pos.pushNaryArg 3 1
+
+def pushRightConjunct (pos : SubExpr.Pos) : SubExpr.Pos :=
+  pos.pushNaryArg 3 2
+
+/-- Combine two hypotheses into a conjunction.
+Precondition: Neither `lhs` nor `rhs` is empty (`parseEmptyHyp?`). -/
+def mkAnd! (σs lhs rhs : Expr) : Expr :=
+  mkApp3 (mkConst ``SPred.and) σs lhs rhs
+
+/-- Smart constructor that cancels away empty hypotheses,
+along with a proof that `lhs ∧ rhs ⊣⊢ₛ result`. -/
+def mkAnd (σs lhs rhs : Expr) : Expr × Expr :=
+  if let some _ := parseEmptyHyp? lhs then
+    (rhs, mkApp2 (mkConst ``SPred.true_and) σs rhs)
+  else if let some _ := parseEmptyHyp? rhs then
+    (lhs, mkApp2 (mkConst ``SPred.and_true) σs lhs)
+  else
+    let result := mkAnd! σs lhs rhs
+    (result, mkApp2 (mkConst ``SPred.bientails.refl) σs result)
+
+def σs.mkType : Expr := mkApp (mkConst ``List [.succ .zero]) (mkSort (.succ .zero))
+def σs.mkNil : Expr := mkApp (mkConst ``List.nil [.succ .zero]) (mkSort (.succ .zero))
+
+def parseAnd? (e : Expr) : Option (Expr × Expr × Expr) :=
+  e.app3? ``SPred.and <|> (σs.mkNil, ·) <$> e.app2? ``And
+
+structure MGoal where
+  σs : Expr -- Q(List Type)
+  hyps : Expr -- A conjunction of hypotheses in `SPred σs`, each carrying a name and uniq as metadata (`parseHyp?`)
+  target : Expr -- Q(SPred $σs)
+  deriving Inhabited
+
+def parseMGoal? (expr : Expr) : Option MGoal := do
+  let some (σs, hyps, target) := expr.consumeMData.app3? ``MGoalEntails | none
+  some { σs, hyps, target }
+
+open Tactic in
+def ensureMGoal : TacticM (MVarId × MGoal) := do
+  let mvar ← getMainGoal
+  let goal ← instantiateMVars <| (← mvar.getType)
+  if let some goal := parseMGoal? goal then
+    return (mvar, goal)
+  else
+    throwError "Not in proof mode"
+
+def MGoal.strip (goal : MGoal) : Expr := -- omits the .mdata wrapper
+  mkApp3 (mkConst ``SPred.entails) goal.σs goal.hyps goal.target
+
+/-- Roundtrips with `parseMGoal?`. -/
+def MGoal.toExpr (goal : MGoal) : Expr :=
+  mkApp3 (mkConst ``MGoalEntails) goal.σs goal.hyps goal.target
+
+partial def MGoal.findHyp? (goal : MGoal) (name : Name) : Option (SubExpr.Pos × Hyp) := go goal.hyps SubExpr.Pos.root
+  where
+    go (e : Expr) (p : SubExpr.Pos) : Option (SubExpr.Pos × Hyp) := do
+      if let some hyp := parseHyp? e then
+        if hyp.name = name then
+          return (p, hyp)
+        else
+          none
+      else if let some (_, lhs, rhs) := parseAnd? e then
+        -- NB: Need to prefer rhs over lhs, like the goal view (Lean.Elab.Tactic.Do.ProofMode.Delab).
+        go rhs (pushLeftConjunct p) <|> go lhs (pushRightConjunct p)
+      else if let some _ := parseEmptyHyp? e then
+        none
+      else
+        panic! "MGoal.findHyp?: hypothesis without proper metadata: {e}"
+
+def MGoal.checkProof (goal : MGoal) (prf : Expr) (suppressWarning : Bool := false) : MetaM Unit := do
+  check prf
+  let prf_type ← inferType prf
+  unless ← isDefEq goal.toExpr prf_type do
+    throwError "MGoal.checkProof: the proof and its supposed type did not match.\ngoal:  {goal.toExpr}\nproof: {prf_type}"
+  unless suppressWarning do
+    logWarning m!"stray MGoal.checkProof {prf_type} {goal.toExpr}"
+
+def getFreshHypName : TSyntax ``binderIdent → CoreM (Name × Syntax)
+  | `(binderIdent| $name:ident) => pure (name.getId, name)
+  | stx => return (← mkFreshUserName `h, stx)
+
+partial def betaRevPreservingHypNames (σs' e : Expr) (args : Array Expr) : Expr :=
+  if let some _σs := parseEmptyHyp? e then
+    emptyHyp σs'
+  else if let some hyp := parseHyp? e then
+    { hyp with p := hyp.p.betaRev args }.toExpr
+  else if let some (_σs, lhs, rhs) := parseAnd? e then
+    -- _σs = σ :: σs'
+    mkAnd! σs' (betaRevPreservingHypNames σs' lhs args) (betaRevPreservingHypNames σs' rhs args)
+  else
+    e.betaRev args
+
+def betaPreservingHypNames (σs' e : Expr) (args : Array Expr) : Expr :=
+  betaRevPreservingHypNames σs' e args.reverse
+
+def dropStateList (σs : Expr) (n : Nat) : MetaM Expr := do
+  let mut σs := σs
+  for _ in [:n] do
+    let some (_type, _σ, σs') := (← whnfR σs).app3? ``List.cons | throwError "Ambient state list not a cons {σs}"
+    σs := σs'
+  return σs
+
+def addLocalVarInfo (stx : Syntax) (lctx : LocalContext)
+    (expr : Expr) (expectedType? : Option Expr) (isBinder := false) : MetaM Unit := do
+  Elab.withInfoContext' (pure ())
+    (fun _ =>
+      return .inl <| .ofTermInfo
+        { elaborator := .anonymous, lctx, expr, stx, expectedType?, isBinder })
+    (return .ofPartialTermInfo { elaborator := .anonymous, lctx, stx, expectedType? })
+
+def addHypInfo (stx : Syntax) (σs : Expr) (hyp : Hyp) (isBinder := false) : MetaM Unit := do
+  let lctx ← getLCtx
+  let ty := mkApp2 (mkConst ``MGoalHypMarker) σs hyp.p
+  addLocalVarInfo stx (lctx.mkLocalDecl ⟨hyp.uniq⟩ hyp.name ty) (.fvar ⟨hyp.uniq⟩) ty isBinder

backend/core/leanprover--lean4---v4.22.0/src/lean/Lean/Elab/Tactic/Do/ProofMode/Pure.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König, Mario Carneiro, Sebastian Graf
+-/
+prelude
+import Std.Tactic.Do.Syntax
+import Lean.Elab.Tactic.Do.ProofMode.MGoal
+import Lean.Elab.Tactic.Do.ProofMode.Focus
+
+namespace Lean.Elab.Tactic.Do.ProofMode
+open Std.Do SPred.Tactic
+open Lean Elab Tactic Meta
+
+-- NB: We do not use MVarId.intro because that would mean we require all callers to supply an MVarId.
+-- This function only knows about the hypothesis H=⌜φ⌝ to destruct.
+-- It will provide a proof for Q ∧ H ⊢ₛ T
+-- if `k` produces a proof for Q ⊢ₛ T that may range over a pure proof h : φ.
+-- It calls `k` with the φ in H = ⌜φ⌝ and a proof `h : φ` thereof.
+def mPureCore (σs : Expr) (hyp : Expr) (name : TSyntax ``binderIdent)
+  (k : Expr /-φ:Prop-/ → Expr /-h:φ-/ → MetaM (α × MGoal × Expr)) : MetaM (α × MGoal × Expr) := do
+  let φ ← mkFreshExprMVar (mkSort .zero)
+  let inst ← synthInstance (mkApp3 (mkConst ``IsPure) σs hyp φ)
+  let (name, ref) ← getFreshHypName name
+  withLocalDeclD name φ fun h => do
+    addLocalVarInfo ref (← getLCtx) h φ
+    let (a, goal, prf /- : goal.toExpr -/) ← k φ h
+    let prf ← mkLambdaFVars #[h] prf
+    let prf := mkApp7 (mkConst ``Pure.thm) σs goal.hyps hyp goal.target φ inst prf
+    let goal := { goal with hyps := mkAnd! σs goal.hyps hyp }
+    return (a, goal, prf)
+
+@[builtin_tactic Lean.Parser.Tactic.mpure]
+def elabMPure : Tactic
+  | `(tactic| mpure $hyp) => do
+    let mvar ← getMainGoal
+    mvar.withContext do
+    let g ← instantiateMVars <| ← mvar.getType
+    let some goal := parseMGoal? g | throwError "not in proof mode"
+    let res ← goal.focusHypWithInfo hyp
+    let (m, _new_goal, prf) ← mPureCore goal.σs res.focusHyp (← `(binderIdent| $hyp:ident)) fun _ _ => do
+      let goal := res.restGoal goal
+      let m ← mkFreshExprSyntheticOpaqueMVar goal.toExpr
+      return (m, goal, m)
+    let prf := res.rewriteHyps goal prf
+    mvar.assign prf
+    replaceMainGoal [m.mvarId!]
+  | _ => throwUnsupportedSyntax
+
+macro "mpure_intro" : tactic => `(tactic| apply Pure.intro)

backend/core/leanprover--lean4---v4.22.0/src/lean/Lean/Elab/Tactic/Do/ProofMode/Refine.lean

@@ -0,0 +1,80 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König, Mario Carneiro, Sebastian Graf
+-/
+prelude
+import Std.Tactic.Do.Syntax
+import Lean.Elab.Tactic.Do.ProofMode.Focus
+import Lean.Elab.Tactic.Do.ProofMode.Assumption
+import Lean.Elab.Tactic.Do.ProofMode.Exact
+
+namespace Lean.Elab.Tactic.Do.ProofMode
+open Std.Do SPred.Tactic Lean.Parser.Tactic
+open Lean Elab Tactic Meta
+
+def patAsTerm (pat : MRefinePat) (expected : Option Expr := none) : OptionT TacticM Expr := do
+  match pat with
+  | .pure t => elabTerm t expected
+  | .one name =>
+    if let `(binderIdent| $name:ident) := name then
+      elabTerm (← `($name)) expected
+    else failure
+  | _ => failure
+
+partial def mRefineCore (goal : MGoal) (pat : MRefinePat) (k : MGoal → TSyntax ``binderIdent → TacticM Expr) : TacticM Expr := do
+  match pat with
+  | .stateful name => liftMetaM do
+    match name with
+    | `(binderIdent| $name:ident) => do
+      let some prf ← goal.exact name | throwError "unknown hypothesis '{repr name}'"
+      return prf
+    | _ => do
+      let some prf ← goal.assumption | throwError "could not solve {goal.target} by assumption"
+      return prf
+  | .pure t => do
+    goal.exactPure t
+  | .one name =>
+      if let `(binderIdent| $_:ident) := name then
+        mRefineCore goal (.pure ⟨name.raw⟩) k <|> mRefineCore goal (.stateful name) k
+      else
+        mRefineCore goal (.stateful name) k
+  | .hole name => k goal name
+  | .tuple [] => throwUnsupportedSyntax
+  | .tuple [p] => mRefineCore goal p k
+  | .tuple (p::ps) => do
+    let T ← whnfR goal.target
+    if let some (σs, T₁, T₂) := parseAnd? T.consumeMData then
+      let prf₁ ← mRefineCore { goal with target := T₁ } p k
+      let prf₂ ← mRefineCore { goal with target := T₂ } (.tuple ps) k
+      return mkApp6 (mkConst ``SPred.and_intro) σs goal.hyps T₁ T₂ prf₁ prf₂
+    else if let some (α, σs, ψ) := T.app3? ``SPred.exists then
+      let some witness ← patAsTerm p (some α) | throwError "pattern does not elaborate to a term to instantiate ψ"
+      let prf ← mRefineCore { goal with target := ψ.betaRev #[witness] } (.tuple ps) k
+      let u ← getLevel α
+      return mkApp6 (mkConst ``SPred.exists_intro' [u]) α σs goal.hyps ψ witness prf
+    else throwError "Neither a conjunction nor an existential quantifier {goal.target}"
+
+@[builtin_tactic Lean.Parser.Tactic.mrefine]
+def elabMRefine : Tactic
+  | `(tactic| mrefine $pat:mrefinePat) => do
+    let pat ← liftMacroM <| MRefinePat.parse pat
+    let (mvar, goal) ← mStartMVar (← getMainGoal)
+    mvar.withContext do
+
+    let goals ← IO.mkRef #[]
+    let prf ← mRefineCore goal pat fun goal name => do
+      let m ← mkFreshExprSyntheticOpaqueMVar goal.toExpr name.raw.getId
+      goals.modify (·.push m.mvarId!)
+      return m
+    mvar.assign prf
+    replaceMainGoal (← goals.get).toList
+  | _ => throwUnsupportedSyntax
+
+@[builtin_tactic Lean.Parser.Tactic.mexists]
+def elabMExists : Tactic
+  | `(tactic| mexists $args,*) => do
+    let pats ← args.getElems.mapM fun t => `(mrefinePat| ⌜$t⌝)
+    let pat ← pats.foldrM (fun pat acc => `(mrefinePat| ⟨$pat, $acc⟩)) (← `(mrefinePat| ?_))
+    evalTactic (← `(tactic| (mrefine $pat; try massumption)))
+  | _ => throwUnsupportedSyntax

backend/core/leanprover--lean4---v4.22.0/src/lean/Lean/Elab/Tactic/Do/ProofMode/Revert.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König, Mario Carneiro, Sebastian Graf
+-/
+prelude
+import Std.Tactic.Do.Syntax
+import Lean.Elab.Tactic.Do.ProofMode.Focus
+import Lean.Elab.Tactic.Do.ProofMode.Basic
+
+namespace Lean.Elab.Tactic.Do.ProofMode
+open Std.Do SPred.Tactic
+open Lean Elab Tactic Meta
+
+partial def mRevertStep (goal : MGoal) (ref : TSyntax `ident) (k : MGoal → MetaM Expr) : MetaM Expr := do
+  let res ← goal.focusHypWithInfo ref
+  let P := goal.hyps
+  let Q := res.restHyps
+  let H := res.focusHyp
+  let T := goal.target
+  let prf ← k { goal with hyps := Q, target := mkApp3 (mkConst ``SPred.imp) goal.σs H T }
+  let prf := mkApp7 (mkConst ``Revert.revert) goal.σs P Q H T res.proof prf
+  return prf
+
+@[builtin_tactic Lean.Parser.Tactic.mrevert]
+def elabMRevert : Tactic
+  | `(tactic| mrevert $h) => do
+  let (mvar, goal) ← mStartMVar (← getMainGoal)
+  mvar.withContext do
+
+  let goals ← IO.mkRef []
+  mvar.assign (← mRevertStep goal h fun newGoal => do
+    let m ← mkFreshExprSyntheticOpaqueMVar newGoal.toExpr
+    goals.modify (m.mvarId! :: ·)
+    return m)
+  replaceMainGoal (← goals.get)
+  | _ => throwUnsupportedSyntax

backend/core/leanprover--lean4---v4.22.0/src/lean/Lean/Elab/Tactic/Do/ProofMode/Specialize.lean

@@ -0,0 +1,176 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König, Mario Carneiro, Sebastian Graf
+-/
+prelude
+import Std.Tactic.Do.Syntax
+import Lean.Elab.Tactic.Do.ProofMode.MGoal
+import Lean.Elab.Tactic.Do.ProofMode.Focus
+import Lean.Elab.Tactic.Do.ProofMode.Basic
+import Lean.Elab.Tactic.Do.ProofMode.Pure
+
+namespace Lean.Elab.Tactic.Do.ProofMode
+open Std.Do SPred.Tactic
+open Lean Elab Tactic Meta
+
+initialize registerTraceClass `Meta.Tactic.Do.specialize
+
+def mSpecializeImpStateful (σs : Expr) (P : Expr) (QR : Expr) (arg : TSyntax `term) : OptionT TacticM (Expr × Expr) := do
+  guard (arg.raw.isIdent)
+  let some argRes := focusHyp σs (mkAnd! σs P QR) arg.raw.getId | failure
+  let some hyp := parseHyp? argRes.focusHyp | failure
+  addHypInfo arg σs hyp
+  OptionT.mk do -- no OptionT failure after this point
+  -- The goal is P ∧ (Q → R)
+  -- argRes.proof : P ∧ (Q → R) ⊣⊢ₛ P' ∧ Q
+  -- we want to return (R, (proof : P ∧ (Q → R) ⊢ₛ P ∧ R))
+  let some specHyp := parseHyp? QR | panic! "Precondition of specializeImpStateful violated"
+  let P' := argRes.restHyps
+  let Q := argRes.focusHyp
+  let hrefocus := argRes.proof -- P ∧ (Q → R) ⊣⊢ₛ P' ∧ Q
+  let mkApp3 (.const ``SPred.imp []) σs Q' R := specHyp.p | throwError "Expected implication {QR}"
+  let proof := mkApp6 (mkConst ``Specialize.imp_stateful) σs P P' Q R hrefocus
+  -- check proof
+  trace[Meta.Tactic.Do.specialize] "Statefully specialize {specHyp.p} with {Q}. New Goal: {mkAnd! σs P R}"
+  unless ← isDefEq Q Q' do
+    throwError "failed to specialize {specHyp.p} with {Q}"
+
+  return ({ specHyp with p := R }.toExpr, proof)
+
+def mSpecializeImpPure (_σs : Expr) (P : Expr) (QR : Expr) (arg : TSyntax `term) : OptionT TacticM (Expr × Expr) := do
+  let some specHyp := parseHyp? QR | panic! "Precondition of specializeImpPure violated"
+  let mkApp3 (.const ``SPred.imp []) σs Q R := specHyp.p | failure
+  let mut φ ← mkFreshExprMVar (mkSort .zero)
+  let mut (hφ, mvarIds) ← try
+    elabTermWithHoles arg.raw φ `specialize (allowNaturalHoles := true)
+    catch _ => failure
+  -- We might have hφ : φ and Q = ⌜φ⌝. In this case, convert hφ to a proof of ⊢ₛ ⌜φ⌝,
+  -- so that we can infer an instance of `PropAsSPredTautology`.
+  -- NB: PropAsSPredTautology φ ⌜φ⌝ is unfortunately impossible because ⊢ₛ ⌜φ⌝ does not imply φ.
+  -- Hence this additional (lossy) conversion.
+  if let some inst ← synthInstance? (mkApp3 (mkConst ``IsPure) σs Q φ) then
+    hφ := mkApp5 (mkConst ``Specialize.pure_taut) σs φ Q inst hφ
+    φ := mkApp2 (mkConst ``tautological) σs Q
+
+  let some inst ← synthInstance? (mkApp3 (mkConst ``PropAsSPredTautology) φ σs Q)
+    | failure
+
+  OptionT.mk do -- no OptionT failure after this point
+  -- The goal is P ∧ (Q → R)
+  -- we want to return (R, (proof : P ∧ (Q → R) ⊢ₛ P ∧ R))
+  pushGoals mvarIds
+  let proof := mkApp7 (mkConst ``Specialize.imp_pure) σs φ P Q R inst hφ
+  -- check proof
+  trace[Meta.Tactic.Do.specialize] "Purely specialize {specHyp.p} with {Q}. New Goal: {mkAnd! σs P R}"
+  -- logInfo m!"proof: {← inferType proof}"
+  return ({ specHyp with p := R }.toExpr, proof)
+
+def mSpecializeForall (_σs : Expr) (P : Expr) (Ψ : Expr) (arg : TSyntax `term) : OptionT TacticM (Expr × Expr) := do
+  let some specHyp := parseHyp? Ψ | panic! "Precondition of specializeForall violated"
+  let mkApp3 (.const ``SPred.forall [u]) α σs αR := specHyp.p | failure
+  let (a, mvarIds) ← try
+    elabTermWithHoles arg.raw α `specialize (allowNaturalHoles := true)
+    catch _ => failure
+  OptionT.mk do -- no OptionT failure after this point
+  pushGoals mvarIds
+  let proof := mkApp5 (mkConst ``Specialize.forall [u]) σs α P αR a
+  let R := αR.beta #[a]
+  -- check proof
+  trace[Meta.Tactic.Do.specialize] "Instantiate {specHyp.p} with {a}. New Goal: {mkAnd! σs P R}"
+  return ({ specHyp with p := R }.toExpr, proof)
+
+@[builtin_tactic Lean.Parser.Tactic.mspecialize]
+def elabMSpecialize : Tactic
+  | `(tactic| mspecialize $hyp $args*) => do
+  let (mvar, goal) ← mStartMVar (← getMainGoal)
+  mvar.withContext do
+
+  -- Want to prove goal P ⊢ T, where hyp occurs in P.
+  -- So we
+  -- 1. focus on hyp (referred to as H):  P ⊣⊢ₛ P' ∧ H. Prove P' ∧ H ⊢ₛ T
+  -- 2. Produce a (transitive chain of) proofs
+  --      P' ∧ H ⊢ P' ∧ H₁ ⊢ₛ P' ∧ H₂ ⊢ₛ ...
+  --    One for each arg; end up with goal P' ∧ H' ⊢ₛ T
+  -- 3. Recombine with mkAnd (NB: P' might be empty), compose with P' ∧ H' ⊣⊢ₛ mkAnd P' H'.
+  -- 4. Make a new MVar for goal `mkAnd P' H' ⊢ T` and assign the transitive chain.
+  let some specFocus := goal.focusHyp hyp.getId | throwError "unknown identifier '{hyp}'"
+  let σs := goal.σs
+  let P := specFocus.restHyps
+  let mut H := specFocus.focusHyp
+  let some hyp' := parseHyp? H | panic! "Invariant of specialize violated"
+  addHypInfo hyp σs hyp'
+  -- invariant: proof (_ : { goal with hyps := mkAnd! σs P H }.toExpr) fills the mvar
+  let mut proof : Expr → Expr :=
+    mkApp7 (mkConst ``Specialize.focus) σs goal.hyps P H goal.target specFocus.proof
+
+  for arg in args do
+    let res? ← OptionT.run
+      (mSpecializeImpStateful σs P H arg
+        <|> mSpecializeImpPure σs P H arg
+        <|> mSpecializeForall σs P H arg)
+    match res? with
+    | some (H', H2H') =>
+      -- logInfo m!"H: {H}, proof: {← inferType H2H'}"
+      proof := fun hgoal => proof (mkApp6 (mkConst ``SPred.entails.trans) σs (mkAnd! σs P H) (mkAnd! σs P H') goal.target H2H' hgoal)
+      H := H'
+    | none =>
+      throwError "Could not specialize {H} with {arg}"
+
+  let newMVar ← mkFreshExprSyntheticOpaqueMVar { goal with hyps := mkAnd! σs P H }.toExpr
+  mvar.assign (proof newMVar)
+  replaceMainGoal [newMVar.mvarId!]
+
+  | _ => throwUnsupportedSyntax
+
+@[builtin_tactic Lean.Parser.Tactic.mspecializePure]
+def elabMspecializePure : Tactic
+  | `(tactic| mspecialize_pure $head $args* => $hyp) => do
+  -- "mspecialize_pure" >> term >> many (ppSpace >> checkColGt "irrelevant" >> termParser (eval_prec max)) >> "as" >> ident
+  let (mvar, goal) ← mStartMVar (← getMainGoal)
+  mvar.withContext do
+
+  -- Want to prove goal P ⊢ₛ T. `head` is a pure proof of type `φ` that turns into `⊢ₛ H` via `start_entails`.
+  -- So we
+  -- 1. Introduce `head` via `PropAsEntails` as stateful hypothesis named `hyp`, P ∧ (hyp : H) ⊢ₛ T
+  -- 2. (from here on it's the same as `mspecialize`.)
+  --    Produce a (transitive chain of) proofs
+  --      P ∧ H ⊢ P ∧ H₁ ⊢ₛ P ∧ H₂ ⊢ₛ ...
+  --    One for each arg; end up with goal P ∧ H' ⊢ₛ T
+  -- 3. Recombine with mkAnd (NB: P' might be empty), compose with P' ∧ H' ⊣⊢ₛ mkAnd P' H'.
+  -- 4. Make a new MVar for goal `mkAnd P' H' ⊢ T` and assign the transitive chain.
+  let σs := goal.σs
+  let P := goal.hyps
+  let T := goal.target
+  let hφ ← elabTerm head none
+  let φ ← inferType hφ
+  let H ← mkFreshExprMVar (mkApp (mkConst ``SPred) σs)
+  let inst ← synthInstance (mkApp3 (mkConst ``PropAsSPredTautology) φ σs H)
+  let uniq ← mkFreshId
+  let mut H := (Hyp.mk hyp.getId uniq (← instantiateMVars H)).toExpr
+
+  let goal : MGoal := { goal with hyps := mkAnd! σs P H }
+  -- invariant: proof (_ : { goal with hyps := mkAnd! σs P H }.toExpr) fills the mvar
+  let mut proof : Expr → Expr :=
+    mkApp8 (mkConst ``Specialize.pure_start) σs φ H P T inst hφ
+
+  for arg in args do
+    let res? ← OptionT.run
+      (mSpecializeImpStateful σs P H ⟨arg⟩
+        <|> mSpecializeImpPure σs P H ⟨arg⟩
+        <|> mSpecializeForall σs P H ⟨arg⟩)
+    match res? with
+    | some (H', H2H') =>
+      -- logInfo m!"H: {H}, proof: {← inferType H2H'}"
+      proof := fun hgoal => proof (mkApp6 (mkConst ``SPred.entails.trans) σs (mkAnd! σs P H) (mkAnd! σs P H') goal.target H2H' hgoal)
+      H := H'
+    | none =>
+      throwError "Could not specialize {H} with {arg}"
+
+  let some hyp' := parseHyp? H | panic! "Invariant of specialize_pure violated"
+  addHypInfo hyp σs hyp'
+
+  let newMVar ← mkFreshExprSyntheticOpaqueMVar { goal with hyps := mkAnd! σs P H }.toExpr
+  mvar.assign (proof newMVar)
+  replaceMainGoal [newMVar.mvarId!]
+  | _ => throwUnsupportedSyntax

backend/core/leanprover--lean4---v4.22.0/src/lean/Lean/Elab/Tactic/Omega/Core.lean

@@ -0,0 +1,575 @@
+/-
+Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Omega.Constraint
+import Lean.Elab.Tactic.Omega.OmegaM
+import Lean.Elab.Tactic.Omega.MinNatAbs
+
+namespace Lean.Elab.Tactic.Omega
+
+initialize Lean.registerTraceClass `omega
+
+open Lean (Expr)
+open Lean Meta Omega
+
+open Lean in
+instance : ToExpr LinearCombo where
+  toExpr lc :=
+    (Expr.const ``LinearCombo.mk []).app (toExpr lc.const) |>.app (toExpr lc.coeffs)
+  toTypeExpr := .const ``LinearCombo []
+
+open Lean in
+instance : ToExpr Constraint where
+  toExpr s :=
+    (Expr.const ``Constraint.mk []).app (toExpr s.lowerBound) |>.app (toExpr s.upperBound)
+  toTypeExpr := .const ``Constraint []
+
+/--
+A delayed proof that a constraint is satisfied at the atoms.
+-/
+abbrev Proof : Type := OmegaM Expr
+
+/--
+Our internal representation of an argument "justifying" that a constraint holds on some coefficients.
+We'll use this to construct the proof term once a contradiction is found.
+-/
+inductive Justification : Constraint → Coeffs → Type
+  /--
+  `Problem.assumptions[i]` generates a proof that `s.sat' coeffs atoms`
+  -/
+  | assumption (s : Constraint) (x : Coeffs) (i : Nat) : Justification s x
+  /-- The result of `tidy` on another `Justification`. -/
+  | tidy (j : Justification s c) : Justification (tidyConstraint s c) (tidyCoeffs s c)
+  /-- The result of `combine` on two `Justifications`. -/
+  | combine {s t c} (j : Justification s c) (k : Justification t c) : Justification (s.combine t) c
+  /-- A linear `combo` of two `Justifications`. -/
+  | combo {s t x y} (a : Int) (j : Justification s x) (b : Int) (k : Justification t y) :
+    Justification (Constraint.combo a s b t) (Coeffs.combo a x b y)
+  /--
+  The justification for the constraint constructed using "balanced mod" while
+  eliminating an equality.
+  -/
+  | bmod (m : Nat) (r : Int) (i : Nat) {x} (j : Justification (.exact r) x) :
+      Justification (.exact (Int.bmod r m)) (bmod_coeffs m i x)
+
+/-- Wrapping for `Justification.tidy` when `tidy?` is nonempty. -/
+nonrec def Justification.tidy? (j : Justification s c) : Option (Σ s' c', Justification s' c') :=
+  match tidy? (s, c) with
+  | some _ => some ⟨_, _, tidy j⟩
+  | none => none
+
+namespace Justification
+
+private def bullet (s : String) := "• " ++ s.replace "\n" "\n  "
+
+/-- Print a `Justification` as an indented tree structure. -/
+def toString : Justification s x → String
+  | assumption _ _ i => s!"{x} ∈ {s}: assumption {i}"
+  | @tidy s' x' j =>
+    if s == s' && x == x' then j.toString else s!"{x} ∈ {s}: tidying up:\n" ++ bullet j.toString
+  | combine j k =>
+    s!"{x} ∈ {s}: combination of:\n" ++ bullet j.toString ++ "\n" ++ bullet k.toString
+  | combo a j b k =>
+    s!"{x} ∈ {s}: {a} * x + {b} * y combo of:\n" ++ bullet j.toString ++ "\n" ++ bullet k.toString
+  | bmod m _ i j =>
+    s!"{x} ∈ {s}: bmod with m={m} and i={i} of:\n" ++ bullet j.toString
+
+instance : ToString (Justification s x) where toString := toString
+
+open Lean
+
+/-- Construct the proof term associated to a `tidy` step. -/
+def tidyProof (s : Constraint) (x : Coeffs) (v : Expr) (prf : Expr) : Expr :=
+  mkApp4 (.const ``tidy_sat []) (toExpr s) (toExpr x) v prf
+
+/-- Construct the proof term associated to a `combine` step. -/
+def combineProof (s t : Constraint) (x : Coeffs) (v : Expr) (ps pt : Expr) : Expr :=
+  mkApp6 (.const ``Constraint.combine_sat' []) (toExpr s) (toExpr t) (toExpr x) v ps pt
+
+/-- Construct the proof term associated to a `combo` step. -/
+def comboProof (s t : Constraint) (a : Int) (x : Coeffs) (b : Int) (y : Coeffs)
+    (v : Expr) (px py : Expr) : Expr :=
+  mkApp9 (.const ``combo_sat' []) (toExpr s) (toExpr t) (toExpr a) (toExpr x) (toExpr b) (toExpr y)
+    v px py
+
+/-- Construct the proof term associated to a `bmod` step. -/
+def bmodProof (m : Nat) (r : Int) (i : Nat) (x : Coeffs) (v : Expr) (w : Expr) : MetaM Expr := do
+  let m := toExpr m
+  let r := toExpr r
+  let i := toExpr i
+  let x := toExpr x
+  let h ← mkDecideProof (mkApp4 (.const ``LE.le [.zero]) (.const ``Nat []) (.const ``instLENat [])
+    (.app (.const ``Coeffs.length []) x) i)
+  let lhs := mkApp2 (.const ``Coeffs.get []) v i
+  let rhs := mkApp3 (.const ``bmod_div_term []) m x v
+  let p ← mkEqReflWithExpectedType lhs rhs
+  return mkApp8 (.const ``bmod_sat []) m r i x v h p w
+
+-- TODO could we increase sharing in the proof term here?
+
+/-- Constructs a proof that `s.sat' c v = true` -/
+def proof (v : Expr) (assumptions : Array Proof) : Justification s c → Proof
+  | assumption s c i => assumptions[i]!
+  | @tidy s c j => return tidyProof s c v (← proof v assumptions j)
+  | @combine s t c j k =>
+    return combineProof s t c v (← proof v assumptions j) (← proof v assumptions k)
+  | @combo s t x y a j b k =>
+    return comboProof s t a x b y v (← proof v assumptions j) (← proof v assumptions k)
+  | @bmod m r i x j => do bmodProof m r i x v (← proof v assumptions j)
+
+end Justification
+
+/-- A `Justification` bundled together with its parameters. -/
+structure Fact where
+  /-- The coefficients of a constraint. -/
+  coeffs : Coeffs
+  /-- The constraint. -/
+  constraint : Constraint
+  /-- The justification of a derived fact. -/
+  justification : Justification constraint coeffs
+
+namespace Fact
+
+instance : ToString Fact where
+  toString f := toString f.justification
+
+/-- `tidy`, implemented on `Fact`. -/
+def tidy (f : Fact) : Fact :=
+  match f.justification.tidy? with
+  | some ⟨constraint, coeffs, justification⟩ => { coeffs, constraint, justification }
+  | none => f
+
+/-- `combo`, implemented on `Fact`. -/
+def combo (a : Int) (f : Fact) (b : Int) (g : Fact) : Fact :=
+  { coeffs := .combo a f.coeffs b g.coeffs
+    constraint := .combo a f.constraint b g.constraint
+    justification := .combo a f.justification b g.justification }
+
+end Fact
+
+/--
+A `omega` problem.
+
+This is a hybrid structure:
+it contains both `Expr` objects giving proofs of the "ground" assumptions
+(or rather continuations which will produce the proofs when needed)
+and internal representations of the linear constraints that we manipulate in the algorithm.
+
+While the algorithm is running we do not synthesize any new `Expr` proofs: proof extraction happens
+only once we've found a contradiction.
+-/
+structure Problem where
+  /-- The ground assumptions that the algorithm starts from. -/
+  assumptions : Array Proof := ∅
+  /-- The number of variables in the problem. -/
+  numVars : Nat := 0
+  /-- The current constraints, indexed by their coefficients. -/
+  constraints : Std.HashMap Coeffs Fact := ∅
+  /--
+  The coefficients for which `constraints` contains an exact constraint (i.e. an equality).
+  -/
+  equalities : Std.HashSet Coeffs := ∅
+  /--
+  Equations that have already been used to eliminate variables,
+  along with the variable which was removed, and its coefficient (either `1` or `-1`).
+  The earlier elements are more recent,
+  so if these are being reapplied it is essential to use `List.foldr`.
+  -/
+  eliminations : List (Fact × Nat × Int) := []
+  /-- Whether the problem is possible. -/
+  possible : Bool := true
+  /-- If the problem is impossible, then `proveFalse?` will contain a proof of `False`. -/
+  proveFalse? : Option Proof := none
+  /-- Invariant between `possible` and `proveFalse?`. -/
+  proveFalse?_spec : possible || proveFalse?.isSome := by rfl
+  /--
+  If we have found a contradiction,
+  `explanation?` will contain a human readable account of the deriviation.
+  -/
+  explanation? : Thunk String := ""
+
+namespace Problem
+
+/-- Check if a problem has no constraints. -/
+def isEmpty (p : Problem) : Bool := p.constraints.isEmpty
+
+instance : ToString Problem where
+  toString p :=
+    if p.possible then
+      if p.isEmpty then
+        "trivial"
+      else
+        "\n".intercalate <|
+          (p.constraints.toList.map fun ⟨coeffs, ⟨_, cst, _⟩⟩ => s!"{coeffs} ∈ {cst}")
+    else
+      "impossible"
+
+open Lean in
+/--
+Takes a proof that `s.sat' x v` for some `s` such that `s.isImpossible`,
+and constructs a proof of `False`.
+-/
+def proveFalse {s x} (j : Justification s x) (assumptions : Array Proof) : Proof := do
+  let v := ← atomsCoeffs
+  let prf ← j.proof v assumptions
+  let x := toExpr x
+  let s := toExpr s
+  let impossible ←
+    mkDecideProof (← mkEq (mkApp (.const ``Constraint.isImpossible []) s) (.const ``true []))
+  return mkApp5 (.const ``Constraint.not_sat'_of_isImpossible []) s impossible x v prf
+
+/--
+Insert a constraint into the problem,
+without checking if there is already a constraint for these coefficients.
+-/
+def insertConstraint (p : Problem) : Fact → Problem
+  | f@⟨x, s, j⟩ =>
+    if s.isImpossible then
+      { p with
+        possible := false
+        proveFalse? := some (proveFalse j p.assumptions)
+        explanation? := Thunk.mk fun _ => j.toString
+        proveFalse?_spec := rfl }
+    else
+      { p with
+        numVars := max p.numVars x.length
+        constraints := p.constraints.insert x f
+        proveFalse?_spec := p.proveFalse?_spec
+        equalities :=
+        if f.constraint.isExact then
+          p.equalities.insert x
+        else
+          p.equalities }
+
+/--
+Add a constraint into the problem,
+combining it with any existing constraints for the same coefficients.
+-/
+def addConstraint (p : Problem) : Fact → Problem
+  | f@⟨x, s, j⟩ =>
+    if p.possible then
+      match p.constraints[x]? with
+      | none =>
+        match s with
+        | .trivial => p
+        | _ => p.insertConstraint f
+      | some ⟨x', t, k⟩ =>
+        if h : x = x' then
+          let r := s.combine t
+          if r = t then
+            -- No need to overwrite the existing fact
+            -- with the same fact with a more complicated justification
+            p
+          else
+            if r = s then
+              -- The new constraint is strictly stronger, no need to combine with the old one:
+              p.insertConstraint ⟨x, s, j⟩
+            else
+              p.insertConstraint ⟨x, s.combine t, j.combine (h ▸ k)⟩
+        else
+          p -- unreachable
+    else
+      p
+
+/--
+Walk through the equalities, finding either the first equality with minimal coefficient `±1`,
+or otherwise the equality with minimal `(r.minNatAbs, r.maxNatAbs)` (ordered lexicographically).
+
+Returns the coefficients of the equality, along with the value of `minNatAbs`.
+
+Although we don't need to run a termination proof here, it's nevertheless important that we use this
+ordering so the algorithm terminates in practice!
+-/
+def selectEquality (p : Problem) : Option (Coeffs × Nat) :=
+  p.equalities.fold (init := none) fun
+  | none, c => (c, c.minNatAbs)
+  | some (r, m), c =>
+    if 2 ≤ m then
+      let m' := c.minNatAbs
+      if (m' < m || m' = m && c.maxNatAbs < r.maxNatAbs) then
+        (c, m')
+      else
+        (r, m)
+    else
+      (r, m)
+
+/--
+If we have already solved some equalities, apply those to some new `Fact`.
+-/
+def replayEliminations (p : Problem) (f : Fact) : Fact :=
+  p.eliminations.foldr (init := f) fun (f, i, s) g =>
+    match Coeffs.get g.coeffs i with
+    | 0 => g
+    | y => Fact.combo (-1 * s * y) f 1 g
+
+/--
+Solve an "easy" equality, i.e. one with a coefficient that is `±1`.
+
+After solving, the variable will have been eliminated from all constraints.
+-/
+def solveEasyEquality (p : Problem) (c : Coeffs) : Problem :=
+  let i := c.findIdx? (·.natAbs = 1) |>.getD 0 -- findIdx? is always some
+  let sign := c.get i |> Int.sign
+  match p.constraints[c]? with
+  | some f =>
+    let init :=
+    { assumptions := p.assumptions
+      eliminations := (f, i, sign) :: p.eliminations }
+    p.constraints.fold (init := init) fun p' coeffs g =>
+      match Coeffs.get coeffs i with
+      | 0 =>
+        p'.addConstraint g
+      | ci =>
+        let k := -1 * sign * ci
+        p'.addConstraint (Fact.combo k f 1 g).tidy
+  | _ => p -- unreachable
+
+open Lean in
+/--
+We deal with a hard equality by introducing a new easy equality.
+
+After solving the easy equality,
+the minimum lexicographic value of `(c.minNatAbs, c.maxNatAbs)` will have been reduced.
+-/
+def dealWithHardEquality (p : Problem) (c : Coeffs) : OmegaM Problem :=
+  match p.constraints[c]? with
+  | some ⟨_, ⟨some r, some r'⟩, j⟩ => do
+    let m := c.minNatAbs + 1
+    -- We have to store the valid value of the newly introduced variable in the atoms.
+    let x := mkApp3 (.const ``bmod_div_term []) (toExpr m) (toExpr c) (← atomsCoeffs)
+    let (i, facts?) ← lookup x
+    if hr : r' = r then
+      match facts? with
+      | none => throwError "When solving hard equality, new atom had been seen before!"
+      | some facts => if ! facts.isEmpty then
+        throwError "When solving hard equality, there were unexpected new facts!"
+      return p.addConstraint { coeffs := _, constraint := _, justification := (hr ▸ j).bmod m r i }
+    else
+      throwError "Invalid constraint, expected an equation." -- unreachable
+  | _ =>
+    return p -- unreachable
+
+/--
+Solve an equality, by deciding whether it is easy (has a `±1` coefficient) or hard,
+and delegating to the appropriate function.
+-/
+def solveEquality (p : Problem) (c : Coeffs) (m : Nat) : OmegaM Problem :=
+  if m = 1 then
+    return p.solveEasyEquality c
+  else
+    p.dealWithHardEquality c
+
+/-- Recursively solve all equalities. -/
+partial def solveEqualities (p : Problem) : OmegaM Problem :=
+  if p.possible then
+    match p.selectEquality with
+    | some (c, m) => do (← p.solveEquality c m).solveEqualities
+    | none => return p
+  else return p
+
+open Constraint
+
+open Lean in
+/-- Constructing the proof term for `addInequality`. -/
+def addInequality_proof (c : Int) (x : Coeffs) (p : Proof) : Proof := do
+  return mkApp4 (.const ``addInequality_sat []) (toExpr c) (toExpr x) (← atomsCoeffs) (← p)
+
+open Lean in
+/-- Constructing the proof term for `addEquality`. -/
+def addEquality_proof (c : Int) (x : Coeffs) (p : Proof) : Proof := do
+  return mkApp4 (.const ``addEquality_sat []) (toExpr c) (toExpr x) (← atomsCoeffs) (← p)
+
+/--
+Helper function for adding an inequality of the form `const + Coeffs.dot coeffs atoms ≥ 0`
+to a `Problem`.
+
+(This is only used while initializing a `Problem`. During elimination we use `addConstraint`.)
+-/
+-- We are given `prf? : const + Coeffs.dot coeffs atoms ≥ 0`,
+-- and need to transform this to `Coeffs.dot coeffs atoms ≥ -const`.
+def addInequality (p : Problem) (const : Int) (coeffs : Coeffs) (prf? : Option Proof) : Problem :=
+  let prf := prf?.getD (do mkSorry (← mkFreshExprMVar none) false)
+  let i := p.assumptions.size
+  let p' := { p with assumptions := p.assumptions.push (addInequality_proof const coeffs prf) }
+  let f : Fact :=
+  { coeffs
+    constraint := { lowerBound := some (-const), upperBound := none }
+    justification := .assumption _ _ i }
+  let f := p.replayEliminations f
+  let f := f.tidy
+  p'.addConstraint f
+
+/--
+Helper function for adding an equality of the form `const + Coeffs.dot coeffs atoms = 0`
+to a `Problem`.
+
+(This is only used while initializing a `Problem`. During elimination we use `addConstraint`.)
+-/
+def addEquality (p : Problem) (const : Int) (coeffs : Coeffs) (prf? : Option Proof) : Problem :=
+  let prf := prf?.getD (do mkSorry (← mkFreshExprMVar none) false)
+  let i := p.assumptions.size
+  let p' := { p with assumptions := p.assumptions.push (addEquality_proof const coeffs prf) }
+  let f : Fact :=
+  { coeffs
+    constraint := { lowerBound := some (-const), upperBound := some (-const) }
+    justification := .assumption _ _ i }
+  let f := p.replayEliminations f
+  let f := f.tidy
+  p'.addConstraint f
+
+/-- Folding `addInequality` over a list. -/
+def addInequalities (p : Problem) (ineqs : List (Int × Coeffs × Option Proof)) : Problem :=
+  ineqs.foldl (init := p) fun p ⟨const, coeffs, prf?⟩ => p.addInequality const coeffs prf?
+
+/-- Folding `addEquality` over a list. -/
+def addEqualities (p : Problem) (eqs : List (Int × Coeffs × Option Proof)) : Problem :=
+  eqs.foldl (init := p) fun p ⟨const, coeffs, prf?⟩ => p.addEquality const coeffs prf?
+
+/-- Representation of the data required to run Fourier-Motzkin elimination on a variable. -/
+structure FourierMotzkinData where
+  /-- Which variable is being eliminated. -/
+  var : Nat
+  /-- The "irrelevant" facts which do not involve the target variable. -/
+  irrelevant : List Fact := []
+  /--
+  The facts which give a lower bound on the target variable,
+  and the coefficient of the target variable in each.
+  -/
+  lowerBounds : List (Fact × Int) := []
+  /--
+  The facts which give an upper bound on the target variable,
+  and the coefficient of the target variable in each.
+  -/
+  upperBounds : List (Fact × Int) := []
+  /--
+  Whether the elimination would be exact, because all of the lower bound coefficients are `±1`.
+  -/
+  lowerExact : Bool := true
+  /--
+  Whether the elimination would be exact, because all of the upper bound coefficients are `±1`.
+  -/
+  upperExact : Bool := true
+deriving Inhabited
+
+instance : ToString FourierMotzkinData where
+  toString d :=
+    let irrelevant := d.irrelevant.map fun ⟨x, s, _⟩ => s!"{x} ∈ {s}"
+    let lowerBounds := d.lowerBounds.map fun ⟨⟨x, s, _⟩, _⟩ => s!"{x} ∈ {s}"
+    let upperBounds := d.upperBounds.map fun ⟨⟨x, s, _⟩, _⟩ => s!"{x} ∈ {s}"
+    s!"Fourier-Motzkin elimination data for variable {d.var}\n"
+      ++ s!"• irrelevant: {irrelevant}\n"
+      ++ s!"• lowerBounds: {lowerBounds}\n"
+      ++ s!"• upperBounds: {upperBounds}"
+
+/-- Is a Fourier-Motzkin elimination empty (i.e. there are no relevant constraints). -/
+def FourierMotzkinData.isEmpty (d : FourierMotzkinData) : Bool :=
+  d.lowerBounds.isEmpty && d.upperBounds.isEmpty
+/-- The number of new constraints that would be introduced by Fourier-Motzkin elimination. -/
+def FourierMotzkinData.size (d : FourierMotzkinData) : Nat :=
+  d.lowerBounds.length * d.upperBounds.length
+/-- Is the Fourier-Motzkin elimination known to be exact? -/
+def FourierMotzkinData.exact (d : FourierMotzkinData) : Bool := d.lowerExact || d.upperExact
+
+/-- Prepare the Fourier-Motzkin elimination data for each variable. -/
+-- TODO we could short-circuit here, if we find one with `size = 0`.
+def fourierMotzkinData (p : Problem) : Array FourierMotzkinData := Id.run do
+  let n := p.numVars
+  let mut data : Array FourierMotzkinData :=
+    (List.range p.numVars).foldl (fun a i => a.push { var := i}) #[]
+  for (_, f@⟨xs, s, _⟩) in p.constraints do
+    for i in [0:n] do
+      let x := Coeffs.get xs i
+      data := data.modify i fun d =>
+        if x = 0 then
+          { d with irrelevant := f :: d.irrelevant }
+        else Id.run do
+          let s' := s.scale x
+          let mut d' := d
+          if s'.lowerBound.isSome then
+            d' := { d' with
+              lowerBounds := (f, x) :: d'.lowerBounds
+              lowerExact := d'.lowerExact && x.natAbs = 1 }
+          if s'.upperBound.isSome then
+            d' := { d' with
+              upperBounds := (f, x) :: d'.upperBounds
+              upperExact := d'.upperExact && x.natAbs = 1 }
+          return d'
+  return data
+
+/--
+Decides which variable to run Fourier-Motzkin elimination on, and returns the associated data.
+
+We prefer eliminations which introduce no new inequalities, or otherwise exact eliminations,
+and break ties by the number of new inequalities introduced.
+-/
+def fourierMotzkinSelect (data : Array FourierMotzkinData) : MetaM FourierMotzkinData := do
+  let data := data.filter fun d => ¬ d.isEmpty
+  trace[omega] "Selecting variable to eliminate from (idx, size, exact) triples:\n\
+    {data.map fun d => (d.var, d.size, d.exact)}"
+  let mut bestIdx := 0
+  let mut bestSize := data[0]!.size
+  let mut bestExact := data[0]!.exact
+  if bestSize = 0 then
+    trace[omega] "Selected variable {data[0]!.var}."
+    return data[0]!
+  for h : i in [1:data.size] do
+    let exact := data[i].exact
+    let size := data[i].size
+    if size = 0 || !bestExact && exact || (bestExact == exact) && size < bestSize then
+      if size = 0 then
+        trace[omega] "Selected variable {data[i].var}"
+        return data[i]
+      bestIdx := i
+      bestExact := exact
+      bestSize := size
+  trace[omega] "Selected variable {data[bestIdx]!.var}."
+  return data[bestIdx]!
+
+/--
+Run Fourier-Motzkin elimination on one variable.
+-/
+-- This is only in MetaM to enable tracing.
+def fourierMotzkin (p : Problem) : MetaM Problem := do
+  let data := p.fourierMotzkinData
+  -- Now perform the elimination.
+  let ⟨_, irrelevant, lower, upper, _, _⟩ ← fourierMotzkinSelect data
+  let mut r : Problem := { assumptions := p.assumptions, eliminations := p.eliminations }
+  for f in irrelevant do
+    r := r.insertConstraint f
+  for ⟨f, b⟩ in lower do
+    for ⟨g, a⟩ in upper do
+      r := r.addConstraint (Fact.combo a f (-b) g).tidy
+  return r
+
+mutual
+
+/--
+Run the `omega` algorithm (for now without dark and grey shadows!) on a problem.
+-/
+partial def runOmega (p : Problem) : OmegaM Problem := do
+  trace[omega] "Running omega on:\n{p}"
+  if p.possible then
+    let p' ← p.solveEqualities
+    elimination p'
+  else
+    return p
+
+/-- As for `runOmega`, but assuming the first round of solving equalities has already happened. -/
+partial def elimination (p : Problem) : OmegaM Problem :=
+  if p.possible then
+    if p.isEmpty then
+      return p
+    else do
+      trace[omega] "Running Fourier-Motzkin elimination on:\n{p}"
+      runOmega (← p.fourierMotzkin)
+  else
+    return p
+
+end
+
+end Problem
+
+end Lean.Elab.Tactic.Omega

backend/core/leanprover--lean4---v4.22.0/src/lean/Lean/Elab/Tactic/Omega/Frontend.lean

@@ -0,0 +1,712 @@
+/-
+Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Lean.Elab.Tactic.Omega.Core
+import Lean.Elab.Tactic.FalseOrByContra
+import Lean.Elab.Tactic.Config
+import Lean.Elab.MutualDef
+import Lean.Meta.Closure
+
+/-!
+# Frontend to the `omega` tactic.
+
+See `Lean.Elab.Tactic.Omega` for an overview of the tactic.
+-/
+
+open Lean Meta Omega
+
+namespace Lean.Elab.Tactic.Omega
+
+/--
+Allow elaboration of `OmegaConfig` arguments to tactics.
+-/
+declare_config_elab elabOmegaConfig Lean.Meta.Omega.OmegaConfig
+
+/-- Match on the two defeq expressions for successor: `n+1`, `n.succ`. -/
+def succ? (e : Expr) : Option Expr :=
+  match e.getAppFnArgs with
+  | (``Nat.succ, #[n]) => some n
+  | (``HAdd.hAdd, #[_, _, _, _, a, b]) => do
+     if b == toExpr (1 : Nat) then some a else none
+  | _ => none
+
+/--
+A partially processed `omega` context.
+
+We have:
+* a `Problem` representing the integer linear constraints extracted so far, and their proofs
+* the unprocessed `facts : List Expr` taken from the local context,
+* the unprocessed `disjunctions : List Expr`,
+  which will only be split one at a time if we can't otherwise find a contradiction.
+
+We begin with `facts := ← getLocalHyps` and `problem := .trivial`,
+and progressively process the facts.
+
+As we process the facts, we may generate additional facts
+(e.g. about coercions and integer divisions).
+To avoid duplicates, we maintain a `HashSet` of previously processed facts.
+-/
+structure MetaProblem where
+  /-- An integer linear arithmetic problem. -/
+  problem : Problem := {}
+  /-- Pending facts which have not been processed yet. -/
+  facts : List Expr := []
+  /--
+  Pending disjunctions, which we will case split one at a time if we can't get a contradiction.
+  -/
+  disjunctions : List Expr := []
+  /-- Facts which have already been processed; we keep these to avoid duplicates. -/
+  processedFacts : Std.HashSet Expr := ∅
+
+/-- Construct the `rfl` proof that `lc.eval atoms = e`. -/
+def mkEvalRflProof (e : Expr) (lc : LinearCombo) : OmegaM Expr := do
+  mkEqReflWithExpectedType e (mkApp2 (.const ``LinearCombo.eval []) (toExpr lc) (← atomsCoeffs))
+
+/-- If `e : Expr` is the `n`-th atom, construct the proof that
+`e = (coordinate n).eval atoms`. -/
+def mkCoordinateEvalAtomsEq (e : Expr) (n : Nat) : OmegaM Expr := do
+  if n < 10 then
+    let atoms ← atoms
+    let tail ← mkListLit (.const ``Int []) atoms[n<...*].toArray.toList
+    let lem := .str ``LinearCombo s!"coordinate_eval_{n}"
+    mkEqSymm (mkAppN (.const lem []) (atoms[*...=n].toArray.push tail))
+  else
+    let atoms ← atomsCoeffs
+    let n := toExpr n
+    -- Construct the `rfl` proof that `e = (atoms.get? n).getD 0`
+    let eq ← mkEqReflWithExpectedType e (mkApp2 (.const ``Coeffs.get []) atoms n)
+    mkEqTrans eq (← mkEqSymm (mkApp2 (.const ``LinearCombo.coordinate_eval []) n atoms))
+
+/-- Construct the linear combination (and its associated proof and new facts) for an atom. -/
+def mkAtomLinearCombo (e : Expr) : OmegaM (LinearCombo × OmegaM Expr × Std.HashSet Expr) := do
+  let (n, facts) ← lookup e
+  return ⟨LinearCombo.coordinate n, mkCoordinateEvalAtomsEq e n, facts.getD ∅⟩
+
+mutual
+
+/--
+Wrapper for `asLinearComboImpl`,
+using a cache for previously visited expressions.
+
+Gives a small (10%) speedup in testing.
+I tried using a pointer based cache,
+but there was never enough subexpression sharing to make it effective.
+-/
+partial def asLinearCombo (e : Expr) : OmegaM (LinearCombo × OmegaM Expr × Std.HashSet Expr) := do
+  let cache ← get
+  match cache.get? e with
+  | some (lc, prf) =>
+    trace[omega] "Found in cache: {e}"
+    return (lc, prf, ∅)
+  | none =>
+    let (lc, proof, r) ← asLinearComboImpl e
+    modifyThe Cache fun cache => (cache.insert e (lc, proof.run' cache))
+    pure (lc, proof, r)
+
+/--
+Translates an expression into a `LinearCombo`.
+Also returns:
+* a proof that this linear combo evaluated at the atoms is equal to the original expression
+* a list of new facts which should be recorded:
+  * for each new atom `a` of the form `((x : Nat) : Int)`, the fact that `0 ≤ a`
+  * for each new atom `a` of the form `x / k`, for `k` a positive numeral, the facts that
+    `k * a ≤ x < (k + 1) * a`
+  * for each new atom of the form `((a - b : Nat) : Int)`, the fact:
+    `b ≤ a ∧ ((a - b : Nat) : Int) = a - b ∨ a < b ∧ ((a - b : Nat) : Int) = 0`
+
+We also transform the expression as we descend into it:
+* pushing coercions: `↑(x + y)`, `↑(x * y)`, `↑(x / k)`, `↑(x % k)`, `↑k`
+* unfolding `emod`: `x % k` → `x - x / k`
+-/
+partial def asLinearComboImpl (e : Expr) : OmegaM (LinearCombo × OmegaM Expr × Std.HashSet Expr) := do
+  trace[omega] "processing {e}"
+  match groundInt? e with
+  | some i =>
+    let lc := {const := i}
+    return ⟨lc, mkEvalRflProof e lc, ∅⟩
+  | none =>
+    if e.isFVar then
+      if let some v ← e.fvarId!.getValue? then
+        rewrite e (← mkEqReflWithExpectedType e v)
+      else
+        mkAtomLinearCombo e
+    else match e.getAppFnArgs with
+  | (``HAdd.hAdd, #[_, _, _, _, e₁, e₂]) => do
+    let (l₁, prf₁, facts₁) ← asLinearCombo e₁
+    let (l₂, prf₂, facts₂) ← asLinearCombo e₂
+    let prf : OmegaM Expr := do
+      let add_eval :=
+        mkApp3 (.const ``LinearCombo.add_eval []) (toExpr l₁) (toExpr l₂) (← atomsCoeffs)
+      mkEqTrans
+        (← mkAppM ``Int.add_congr #[← prf₁, ← prf₂])
+        (← mkEqSymm add_eval)
+    pure (l₁ + l₂, prf, facts₁.union facts₂)
+  | (``HSub.hSub, #[_, _, _, _, e₁, e₂]) => do
+    let (l₁, prf₁, facts₁) ← asLinearCombo e₁
+    let (l₂, prf₂, facts₂) ← asLinearCombo e₂
+    let prf : OmegaM Expr := do
+      let sub_eval :=
+        mkApp3 (.const ``LinearCombo.sub_eval []) (toExpr l₁) (toExpr l₂) (← atomsCoeffs)
+      mkEqTrans
+        (← mkAppM ``Int.sub_congr #[← prf₁, ← prf₂])
+        (← mkEqSymm sub_eval)
+    pure (l₁ - l₂, prf, facts₁.union facts₂)
+  | (``Neg.neg, #[_, _, e']) => do
+    let (l, prf, facts) ← asLinearCombo e'
+    let prf' : OmegaM Expr := do
+      let neg_eval := mkApp2 (.const ``LinearCombo.neg_eval []) (toExpr l) (← atomsCoeffs)
+      mkEqTrans
+        (← mkAppM ``Int.neg_congr #[← prf])
+        (← mkEqSymm neg_eval)
+    pure (-l, prf', facts)
+  | (``HMul.hMul, #[_, _, _, _, x, y]) =>
+    -- If we decide not to expand out the multiplication,
+    -- we have to revert the `OmegaM` state so that any new facts about the factors
+    -- can still be reported when they are visited elsewhere.
+    let r? ← commitWhen do
+      let (xl, xprf, xfacts) ← asLinearCombo x
+      let (yl, yprf, yfacts) ← asLinearCombo y
+      if xl.coeffs.isZero ∨ yl.coeffs.isZero then
+        let prf : OmegaM Expr := do
+          let h ← mkDecideProof (mkApp2 (.const ``Or [])
+            (.app (.const ``Coeffs.isZero []) (toExpr xl.coeffs))
+            (.app (.const ``Coeffs.isZero []) (toExpr yl.coeffs)))
+          let mul_eval :=
+            mkApp4 (.const ``LinearCombo.mul_eval []) (toExpr xl) (toExpr yl) (← atomsCoeffs) h
+          mkEqTrans
+            (← mkAppM ``Int.mul_congr #[← xprf, ← yprf])
+            (← mkEqSymm mul_eval)
+        pure (some (LinearCombo.mul xl yl, prf, xfacts.union yfacts), true)
+      else
+        pure (none, false)
+    match r? with
+    | some r => pure r
+    | none => mkAtomLinearCombo e
+  | (``HMod.hMod, #[_, _, _, _, n, k]) =>
+    match groundNat? k with
+    | some k' => do
+      let k' := toExpr (k' : Int)
+      rewrite (← mkAppM ``HMod.hMod #[n, k']) (mkApp2 (.const ``Int.emod_def []) n k')
+    | none => mkAtomLinearCombo e
+  | (``HDiv.hDiv, #[_, _, _, _, x, z]) =>
+    match groundInt? z with
+    | some 0 => rewrite e (mkApp (.const ``Int.ediv_zero []) x)
+    | some i => do
+      let e' ← mkAppM ``HDiv.hDiv #[x, toExpr i]
+      if i < 0 then
+        rewrite e' (mkApp2 (.const ``Int.ediv_neg []) x (toExpr (-i)))
+      else
+        mkAtomLinearCombo e'
+    | _ => mkAtomLinearCombo e
+  | (``Min.min, #[_, _, a, b]) =>
+    if (← cfg).splitMinMax then
+      rewrite e (mkApp2 (.const ``Int.min_def []) a b)
+    else
+      mkAtomLinearCombo e
+  | (``Max.max, #[_, _, a, b]) =>
+    if (← cfg).splitMinMax then
+      rewrite e (mkApp2 (.const ``Int.max_def []) a b)
+    else
+      mkAtomLinearCombo e
+  | (``HPow.hPow, #[_, _, _, _, b, k]) =>
+    match succ? k with /- match for `e+1` and `e.succ` -/
+    | none => mkAtomLinearCombo e
+    | some k' =>
+        match groundInt? b with
+        | some _ => rewrite e (mkApp2 (.const ``Int.pow_succ []) b k')
+        | none => mkAtomLinearCombo e
+  | (``Nat.cast, #[α, i, n]) =>
+      match_expr α with
+      | Int => handleNatCast e i n
+      | _ => mkAtomLinearCombo e
+  | (``Prod.fst, #[α, β, p]) => match p with
+    | .app (.app (.app (.app (.const ``Prod.mk [u, v]) _) _) x) y =>
+      rewrite e (mkApp4 (.const ``Prod.fst_mk [u, v]) α x β y)
+    | _ => mkAtomLinearCombo e
+  | (``Prod.snd, #[α, β, p]) => match p with
+    | .app (.app (.app (.app (.const ``Prod.mk [u, v]) _) _) x) y =>
+      rewrite e (mkApp4 (.const ``Prod.snd_mk [u, v]) α x β y)
+    | _ => mkAtomLinearCombo e
+  | (``Int.negSucc, #[n]) => rewrite e (mkApp (.const ``Int.negSucc_eq []) n)
+  | _ => mkAtomLinearCombo e
+where
+  /--
+  Apply a rewrite rule to an expression, and interpret the result as a `LinearCombo`.
+  (We're not rewriting any subexpressions here, just the top level, for efficiency.)
+  -/
+  rewrite (lhs rw : Expr) : OmegaM (LinearCombo × OmegaM Expr × Std.HashSet Expr) := do
+    trace[omega] "rewriting {lhs} via {rw} : {← inferType rw}"
+    match (← inferType rw).eq? with
+    | some (_, _lhs', rhs) =>
+      let (lc, prf, facts) ← asLinearCombo rhs
+      let prf' : OmegaM Expr := do mkEqTrans rw (← prf)
+      pure (lc, prf', facts)
+    | none => panic! "Invalid rewrite rule in 'asLinearCombo'"
+  handleNatCast (e i n : Expr) : OmegaM (LinearCombo × OmegaM Expr × Std.HashSet Expr) := do
+    match n with
+    | .fvar h =>
+      if let some v ← h.getValue? then
+        rewrite e (← mkEqReflWithExpectedType e
+          (mkApp3 (.const ``Nat.cast [0]) (.const ``Int []) i v))
+      else
+        mkAtomLinearCombo e
+    | _ => match n.getAppFnArgs with
+    | (``Nat.succ, #[n]) => rewrite e (.app (.const ``Int.ofNat_succ []) n)
+    | (``HAdd.hAdd, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.natCast_add []) a b)
+    | (``HMul.hMul, #[_, _, _, _, a, b]) =>
+      let (lc, prf, r) ← rewrite e (mkApp2 (.const ``Int.ofNat_mul []) a b)
+      -- Add the fact that the multiplication is non-negative.
+      pure (lc, prf, r.insert (mkApp2 (.const ``Int.ofNat_mul_nonneg []) a b))
+    | (``HDiv.hDiv, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.natCast_ediv []) a b)
+    | (``OfNat.ofNat, #[_, n, _]) => rewrite e (.app (.const ``Int.natCast_ofNat []) n)
+    | (``HMod.hMod, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.natCast_emod []) a b)
+    | (``HSub.hSub, #[_, _, _, _, mkApp6 (.const ``HSub.hSub _) _ _ _ _ a b, c]) =>
+      rewrite e (mkApp3 (.const ``Int.ofNat_sub_sub []) a b c)
+    | (``HPow.hPow, #[_, _, _, _, a, b]) =>
+      match groundNat? a with
+      | some _ => rewrite e (mkApp2 (.const ``Int.ofNat_pow []) a b)
+      | none => mkAtomLinearCombo e
+    | (``Prod.fst, #[_, β, p]) => match p with
+      | .app (.app (.app (.app (.const ``Prod.mk [0, v]) _) _) x) y =>
+        rewrite e (mkApp3 (.const ``Int.ofNat_fst_mk [v]) β x y)
+      | _ => mkAtomLinearCombo e
+    | (``Prod.snd, #[α, _, p]) => match p with
+      | .app (.app (.app (.app (.const ``Prod.mk [u, 0]) _) _) x) y =>
+        rewrite e (mkApp3 (.const ``Int.ofNat_snd_mk [u]) α x y)
+      | _ => mkAtomLinearCombo e
+    | (``Min.min, #[_, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_min []) a b)
+    | (``Max.max, #[_, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_max []) a b)
+    | (``Int.toNat, #[n]) => rewrite e (mkApp (.const ``Int.toNat_eq_max []) n)
+    | (``HShiftLeft.hShiftLeft, #[_, _, _, _, a, b]) =>
+      rewrite e (mkApp2 (.const ``Int.ofNat_shiftLeft_eq []) a b)
+    | (``HShiftRight.hShiftRight, #[_, _, _, _, a, b]) =>
+      rewrite e (mkApp2 (.const ``Int.ofNat_shiftRight_eq_div_pow []) a b)
+    | (``Int.natAbs, #[n]) =>
+      if (← cfg).splitNatAbs then
+        rewrite e (mkApp (.const ``Int.ofNat_natAbs []) n)
+      else
+        mkAtomLinearCombo e
+    | (``Fin.val, #[n, x]) =>
+      handleFinVal e i n x
+    | _ => mkAtomLinearCombo e
+  handleFinVal (e i n x : Expr) : OmegaM (LinearCombo × OmegaM Expr × Std.HashSet Expr) := do
+    match x with
+    | .fvar h =>
+      if let some v ← h.getValue? then
+        rewrite e (← mkEqReflWithExpectedType e
+          (mkApp3 (.const ``Nat.cast [0]) (.const ``Int []) i (mkApp2 (.const ``Fin.val []) n v)))
+      else
+        mkAtomLinearCombo e
+    | _ => match x.getAppFnArgs, n.nat? with
+      | (``HAdd.hAdd, #[_, _, _, _, a, b]), _ =>
+        rewrite e (mkApp3 (.const ``Fin.ofNat_val_add []) n a b)
+      | (``HMul.hMul, #[_, _, _, _, a, b]), _ =>
+        rewrite e (mkApp3 (.const ``Fin.ofNat_val_mul []) n a b)
+      | (``HSub.hSub, #[_, _, _, _, a, b]), some _ =>
+        -- Only do this rewrite if `n` is a numeral.
+        rewrite e (mkApp3 (.const ``Fin.ofNat_val_sub []) n a b)
+      | (``OfNat.ofNat, #[_, y, _]), some m =>
+        -- Only do this rewrite if `n` is a nonzero numeral.
+        if m = 0 then
+          mkAtomLinearCombo e
+        else
+          match y with
+          | .lit (.natVal y) =>
+            rewrite e (mkApp4 (.const ``Fin.ofNat_val_natCast [])
+              (toExpr (m - 1)) (toExpr y) (.lit (.natVal (y % m))) (← mkEqRefl (toExpr (y % m))))
+          | _ =>
+            -- This shouldn't happen, we obtained `y` from `OfNat.ofNat`
+            mkAtomLinearCombo e
+      | _, _ => mkAtomLinearCombo e
+
+end
+namespace MetaProblem
+
+/-- The trivial `MetaProblem`, with no facts to process and a trivial `Problem`. -/
+def trivial : MetaProblem where
+  problem := {}
+
+instance : Inhabited MetaProblem := ⟨trivial⟩
+
+/--
+Add an integer equality to the `Problem`.
+
+We solve equalities as they are discovered, as this often results in an earlier contradiction.
+-/
+def addIntEquality (p : MetaProblem) (h x : Expr) : OmegaM MetaProblem := do
+  let (lc, prf, facts) ← asLinearCombo x
+  let newFacts : Std.HashSet Expr := facts.fold (init := ∅) fun s e =>
+    if p.processedFacts.contains e then s else s.insert e
+  trace[omega] "Adding proof of {lc} = 0"
+  pure <|
+  { p with
+    facts := newFacts.toList ++ p.facts
+    problem := ← (p.problem.addEquality lc.const lc.coeffs
+      (some do mkEqTrans (← mkEqSymm (← prf)) h)) |>.solveEqualities }
+
+/--
+Add an integer inequality to the `Problem`.
+
+We solve equalities as they are discovered, as this often results in an earlier contradiction.
+-/
+def addIntInequality (p : MetaProblem) (h y : Expr) : OmegaM MetaProblem := do
+  let (lc, prf, facts) ← asLinearCombo y
+  let newFacts : Std.HashSet Expr := facts.fold (init := ∅) fun s e =>
+    if p.processedFacts.contains e then s else s.insert e
+  trace[omega] "Adding proof of {lc} ≥ 0"
+  pure <|
+  { p with
+    facts := newFacts.toList ++ p.facts
+    problem := ← (p.problem.addInequality lc.const lc.coeffs
+      (some do mkAppM ``le_of_le_of_eq #[h, (← prf)])) |>.solveEqualities }
+
+/-- Given a fact `h` with type `¬ P`, return a more useful fact obtained by pushing the negation. -/
+def pushNot (h P : Expr) : MetaM (Option Expr) := do
+  let P ← whnfR P
+  trace[omega] "pushing negation: {P}"
+  match P with
+  | .forallE _ t b _ =>
+    if (← isProp t) && (← isProp b) then
+     return some (mkApp4 (.const ``Decidable.and_not_of_not_imp []) t b
+      (.app (.const ``Classical.propDecidable []) t) h)
+    else
+      return none
+  | .app _ _ =>
+    match_expr P with
+    | LT.lt α _ x y => match_expr α with
+      | Nat => return some (mkApp3 (.const ``Nat.le_of_not_lt []) x y h)
+      | Int => return some (mkApp3 (.const ``Int.le_of_not_lt []) x y h)
+      | Fin n => return some (mkApp4 (.const ``Fin.le_of_not_lt []) n x y h)
+      | _ => return none
+    | LE.le α _ x y => match_expr α with
+      | Nat => return some (mkApp3 (.const ``Nat.lt_of_not_le []) x y h)
+      | Int => return some (mkApp3 (.const ``Int.lt_of_not_le []) x y h)
+      | Fin n => return some (mkApp4 (.const ``Fin.lt_of_not_le []) n x y h)
+      | _ => return none
+    | Eq α x y => match_expr α with
+      | Nat => return some (mkApp3 (.const ``Nat.lt_or_gt_of_ne []) x y h)
+      | Int => return some (mkApp3 (.const ``Int.lt_or_gt_of_ne []) x y h)
+      | Fin n => return some (mkApp4 (.const ``Fin.lt_or_gt_of_ne []) n x y h)
+      | _ => return none
+    | Dvd.dvd α _ k x => match_expr α with
+      | Nat => return some (mkApp3 (.const ``Nat.emod_pos_of_not_dvd []) k x h)
+      | Int =>
+        -- This introduces a disjunction that could be avoided by checking `k ≠ 0`.
+        return some (mkApp3 (.const ``Int.emod_pos_of_not_dvd []) k x h)
+      | _ => return none
+    | Prod.Lex _ _ _ _ _ _ => return some (← mkAppM ``Prod.of_not_lex #[h])
+    | Not P =>
+      return some (mkApp3 (.const ``Decidable.of_not_not []) P
+        (.app (.const ``Classical.propDecidable []) P) h)
+    | And P Q =>
+      return some (mkApp5 (.const ``Decidable.or_not_not_of_not_and []) P Q
+        (.app (.const ``Classical.propDecidable []) P)
+        (.app (.const ``Classical.propDecidable []) Q) h)
+    | Or P Q =>
+      return some (mkApp3 (.const ``and_not_not_of_not_or []) P Q h)
+    | Iff P Q =>
+      return some (mkApp5 (.const ``Decidable.and_not_or_not_and_of_not_iff []) P Q
+        (.app (.const ``Classical.propDecidable []) P)
+        (.app (.const ``Classical.propDecidable []) Q) h)
+    | _ => return none
+  | _ => return none
+
+/--
+Parse an `Expr` and extract facts, also returning the number of new facts found.
+-/
+partial def addFact (p : MetaProblem) (h : Expr) : OmegaM (MetaProblem × Nat) := do
+  if ! p.problem.possible then
+    return (p, 0)
+  else
+    let t ← instantiateMVars (← whnfR (← inferType h))
+    trace[omega] "adding fact: {t}"
+    match t with
+    | .forallE _ x y _ =>
+      if ← pure t.isArrow <&&> isProp x <&&> isProp y then
+        p.addFact (mkApp4 (.const ``Decidable.not_or_of_imp []) x y
+          (.app (.const ``Classical.propDecidable []) x) h)
+      else
+        trace[omega] "rejecting forall: it's not an arrow, or not propositional"
+        return (p, 0)
+    | .app _ _ =>
+      match_expr t with
+      | Eq α x y =>
+        match_expr α with
+        | Int =>
+          match y.int? with
+          | some 0 => pure (← p.addIntEquality h x, 1)
+          | _ => p.addFact (mkApp3 (.const ``Int.sub_eq_zero_of_eq []) x y h)
+        | Nat => p.addFact (mkApp3 (.const ``Int.ofNat_congr []) x y h)
+        | Fin n => p.addFact (mkApp4 (.const ``Fin.val_congr []) n x y h)
+        | _ => pure (p, 0)
+      | LE.le α _ x y =>
+        match_expr α with
+        | Int =>
+          match x.int? with
+          | some 0 => pure (← p.addIntInequality h y, 1)
+          | _ => p.addFact (mkApp3 (.const ``Int.sub_nonneg_of_le []) y x h)
+        | Nat => p.addFact (mkApp3 (.const ``Int.ofNat_le_of_le []) x y h)
+        | Fin n => p.addFact (mkApp4 (.const ``Fin.val_le_of_le []) n x y h)
+        | _ => pure (p, 0)
+      | LT.lt α _ x y =>
+        match_expr α with
+        | Int => p.addFact (mkApp3 (.const ``Int.add_one_le_of_lt []) x y h)
+        | Nat => p.addFact (mkApp3 (.const ``Int.ofNat_lt_of_lt []) x y h)
+        | Fin n => p.addFact (mkApp4 (.const ``Fin.val_add_one_le_of_lt []) n x y h)
+        | _ => pure (p, 0)
+      | GT.gt α _ x y =>
+        match_expr α with
+        | Int => p.addFact (mkApp3 (.const ``Int.lt_of_gt []) x y h)
+        | Nat => p.addFact (mkApp3 (.const ``Nat.lt_of_gt []) x y h)
+        | Fin n => p.addFact (mkApp4 (.const ``Fin.val_add_one_le_of_gt []) n x y h)
+        | _ => pure (p, 0)
+      | GE.ge α _ x y =>
+        match_expr α with
+        | Int => p.addFact (mkApp3 (.const ``Int.le_of_ge []) x y h)
+        | Nat => p.addFact (mkApp3 (.const ``Nat.le_of_ge []) x y h)
+        | Fin n => p.addFact (mkApp4 (.const ``Fin.val_le_of_ge []) n x y h)
+        | _ => pure (p, 0)
+      | Ne α x y =>
+        match_expr α with
+        | Int => p.addFact (mkApp3 (.const ``Int.lt_or_gt_of_ne []) x y h)
+        | Nat => p.addFact (mkApp3 (.const ``Nat.lt_or_gt_of_ne []) x y h)
+        | _ => pure (p, 0)
+      | Dvd.dvd α _ k x =>
+        match_expr α with
+        | Int => p.addFact (mkApp3 (.const ``Int.emod_eq_zero_of_dvd []) k x h)
+        | Nat => p.addFact (mkApp3 (.const ``Nat.mod_eq_zero_of_dvd []) k x h)
+        | _ => pure (p, 0)
+      | Not P => match ← pushNot h P with
+        | none => return (p, 0)
+        | some h' => p.addFact h'
+      | Prod.Lex _ _ _ _ _ _ => p.addFact (← mkAppM ``Prod.of_lex #[h])
+      | And t₁ t₂ => do
+          let (p₁, n₁) ← p.addFact (mkApp3 (.const ``And.left []) t₁ t₂ h)
+          let (p₂, n₂) ← p₁.addFact (mkApp3 (.const ``And.right []) t₁ t₂ h)
+          return (p₂, n₁ + n₂)
+      | Exists α P =>
+        p.addFact (mkApp3 (.const ``Exists.choose_spec [← getLevel α]) α P h)
+      | Subtype α P =>
+        p.addFact (mkApp3 (.const ``Subtype.property [← getLevel α]) α P h)
+      | Iff P₁ P₂ =>
+        p.addFact (mkApp4 (.const ``Decidable.and_or_not_and_not_of_iff [])
+          P₁ P₂ (.app (.const ``Classical.propDecidable []) P₂) h)
+      | Or _ _ =>
+        if (← cfg).splitDisjunctions then
+          return ({ p with disjunctions := p.disjunctions.insert h }, 1)
+        else
+          return (p, 0)
+      | _ => pure (p, 0)
+    | _ => pure (p, 0)
+
+/--
+Process all the facts in a `MetaProblem`, returning the new problem, and the number of new facts.
+
+This is partial because new facts may be generated along the way.
+-/
+partial def processFacts (p : MetaProblem) : OmegaM (MetaProblem × Nat) := do
+  match p.facts with
+  | [] => pure (p, 0)
+  | h :: t =>
+    if p.processedFacts.contains h then
+      processFacts { p with facts := t }
+    else
+      let (p₁, n₁) ← MetaProblem.addFact { p with
+        facts := t
+        processedFacts := p.processedFacts.insert h } h
+      let (p₂, n₂) ← p₁.processFacts
+      return (p₂, n₁ + n₂)
+
+end MetaProblem
+
+/--
+Helpful error message when omega cannot find a solution
+-/
+def formatErrorMessage (p : Problem) : OmegaM MessageData := do
+  if p.possible then
+    if p.isEmpty then
+      return m!"No usable constraints found. You may need to unfold definitions so `omega` can see \
+      linear arithmetic facts about `Nat` and `Int`, which may also involve multiplication, \
+      division, and modular remainder by constants."
+    else
+      let as ← atoms
+      return .ofLazyM (es := as) do
+        let mask ← mentioned as p.constraints
+        let names ← varNames mask
+        return m!"a possible counterexample may satisfy the constraints\n" ++
+          m!"{prettyConstraints names p.constraints}\nwhere\n{prettyAtoms names as mask}"
+  else
+    -- formatErrorMessage should not be used in this case
+    return "it is trivially solvable"
+where
+  varNameOf (i : Nat) : String :=
+    let c : Char := .ofNat ('a'.toNat + (i % 26))
+    let suffix := if i < 26 then "" else s!"_{i / 26}"
+    s!"{c}{suffix}"
+
+  inScope (s : String) : MetaM Bool := do
+    let n := .mkSimple s
+    if (← resolveGlobalName n).isEmpty then
+      if ((← getLCtx).findFromUserName? n).isNone then
+        return false
+    return true
+
+  -- Assign ascending names a, b, c, …, z, a1 … to all atoms mentioned according to the mask
+  -- but avoid names in the local or global scope
+  varNames (mask : Array Bool) : MetaM (Array String) := do
+    let mut names := #[]
+    let mut next := 0
+    for h : i in [:mask.size] do
+      if mask[i] then
+        while ← inScope (varNameOf next) do next := next + 1
+        names := names.push (varNameOf next)
+        next := next + 1
+      else
+        names := names.push "(masked)"
+    return names
+
+  -- We sort the constraints; otherwise the order is dependent on details of the hashing
+  -- and this can cause test suite output churn
+  prettyConstraints (names : Array String) (constraints : Std.HashMap Coeffs Fact) : String :=
+    constraints.toList
+      |>.toArray
+      |>.qsort (·.1 < ·.1)
+      |>.map (fun ⟨coeffs, ⟨_, cst, _⟩⟩ => "  " ++ prettyConstraint (prettyCoeffs names coeffs) cst)
+      |>.toList
+      |> "\n".intercalate
+
+  prettyConstraint (e : String) : Constraint → String
+    | ⟨none, none⟩ => s!"{e} is unconstrained" -- should not happen in error messages
+    | ⟨none, some y⟩ => s!"{e} ≤ {y}"
+    | ⟨some x, none⟩ => s!"{e} ≥ {x}"
+    | ⟨some x, some y⟩ =>
+      if y < x then "∅" else -- should not happen in error messages
+      s!"{x} ≤ {e} ≤ {y}"
+
+  prettyCoeffs (names : Array String) (coeffs : Coeffs) : String :=
+    coeffs.toList.zipIdx
+      |>.filter (fun (c,_) => c ≠ 0)
+      |>.mapIdx (fun j (c,i) =>
+        (if j > 0 then if c > 0 then " + " else " - " else if c > 0 then "" else "- ") ++
+        (if Int.natAbs c = 1 then names[i]! else s!"{c.natAbs}*{names[i]!}"))
+      |> String.join
+
+  mentioned (atoms : Array Expr) (constraints : Std.HashMap Coeffs Fact) : MetaM (Array Bool) := do
+    let initMask := .replicate atoms.size false
+    return constraints.fold (init := initMask) fun mask coeffs _ =>
+      coeffs.zipIdx.foldl (init := mask) fun mask (c, i) =>
+        if c = 0 then mask else mask.set! i true
+
+  prettyAtoms (names : Array String) (atoms : Array Expr) (mask : Array Bool) : MessageData :=
+    (Array.zip names atoms).toList.zipIdx
+      |>.filter (fun (_, i) => mask.getD i false)
+      |>.map (fun ((n, a),_) => m!" {n} := {a}")
+      |> m!"\n".joinSep
+
+mutual
+
+/--
+Split a disjunction in a `MetaProblem`, and if we find a new usable fact
+call `omegaImpl` in both branches.
+-/
+partial def splitDisjunction (m : MetaProblem) : OmegaM Expr := do
+  match m.disjunctions with
+    | [] => throwError "omega could not prove the goal:\n{← formatErrorMessage m.problem}"
+    | h :: t => do
+      let hType ← whnfD (← inferType h)
+      trace[omega] "Case splitting on {hType}"
+      let_expr Or hType₁ hType₂ := hType | throwError "Unexpected disjunction {hType}"
+      let p?₁ ← withoutModifyingState do withLocalDeclD `h₁ hType₁ fun h₁ => do
+        withTraceNode `omega (msg := fun _ => do pure m!"Assuming fact:{indentExpr hType₁}") do
+        let m₁ := { m with facts := [h₁], disjunctions := t }
+        let (m₁, n) ← m₁.processFacts
+        if 0 < n then
+          let p₁ ← omegaImpl m₁
+          let p₁ ← mkLambdaFVars #[h₁] p₁
+          return some p₁
+        else
+          return none
+      if let some p₁ := p?₁ then
+         withLocalDeclD `h₂ hType₂ fun h₂ => do
+          withTraceNode `omega (msg := fun _ => do pure m!"Assuming fact:{indentExpr hType₂}") do
+          let m₂ := { m with facts := [h₂], disjunctions := t }
+          let p₂ ← omegaImpl m₂
+          let p₂ ← mkLambdaFVars #[h₂] p₂
+          return mkApp6 (mkConst ``Or.elim) hType₁ hType₂ (mkConst ``False) h p₁ p₂
+      else
+        trace[omega] "No new facts found."
+        splitDisjunction { m with disjunctions := t }
+
+/-- Implementation of the `omega` algorithm, and handling disjunctions. -/
+partial def omegaImpl (m : MetaProblem) : OmegaM Expr := do
+  let (m, _) ← m.processFacts
+  guard m.facts.isEmpty
+  let p := m.problem
+  trace[omega] "Extracted linear arithmetic problem:\nAtoms: {← atomsList}\n{p}"
+  let p' ← if p.possible then p.elimination else pure p
+  trace[omega] "After elimination:\nAtoms: {← atomsList}\n{p'}"
+  match p'.possible, p'.proveFalse?, p'.proveFalse?_spec with
+  | true, _, _ =>
+    splitDisjunction m
+  | false, .some prf, _ =>
+    trace[omega] "Justification:\n{p'.explanation?.get}"
+    let prf ← instantiateMVars (← prf)
+    trace[omega] "omega found a contradiction, proving {← inferType prf}"
+    return prf
+
+end
+
+/--
+Given a collection of facts, try prove `False` using the omega algorithm,
+and close the goal using that.
+-/
+def omega (facts : List Expr) (g : MVarId) (cfg : OmegaConfig := {}) : MetaM Unit :=
+  g.withContext do
+    let prf ← OmegaM.run (omegaImpl { facts }) cfg
+    g.assign prf
+
+open Lean Elab Tactic Parser.Tactic
+
+/-- The `omega` tactic, for resolving integer and natural linear arithmetic problems. -/
+def omegaTactic (cfg : OmegaConfig) : TacticM Unit := do
+  liftMetaFinishingTactic fun g => do
+    if debug.terminalTacticsAsSorry.get (← getOptions) then
+      g.admit
+    else
+      let some g ← g.falseOrByContra | return ()
+      g.withContext do
+        let type ← g.getType
+        let g' ← mkFreshExprSyntheticOpaqueMVar type
+        let hyps := (← getLocalHyps).toList
+        trace[omega] "analyzing {hyps.length} hypotheses:\n{← hyps.mapM inferType}"
+        omega hyps g'.mvarId! cfg
+        -- Omega proofs are typically rather large, so hide them in a separate definition
+        let e ← mkAuxTheorem type (← instantiateMVarsProfiling g') (zetaDelta := true)
+        g.assign e
+
+
+/-- The `omega` tactic, for resolving integer and natural linear arithmetic problems. This
+`TacticM Unit` frontend with default configuration can be used as an Aesop rule, for example via
+the tactic call `aesop (add 50% tactic Lean.Elab.Tactic.Omega.omegaDefault)`. -/
+def omegaDefault : TacticM Unit := omegaTactic {}
+
+@[builtin_tactic Lean.Parser.Tactic.omega]
+def evalOmega : Tactic
+  | `(tactic| omega%$tk $cfg:optConfig) => do
+    -- Call `assumption` first, to avoid constructing unnecessary proofs.
+    withReducibleAndInstances (evalAssumption tk) <|> do
+    let cfg ← elabOmegaConfig cfg
+    omegaTactic cfg
+  | _ => throwUnsupportedSyntax
+
+builtin_initialize bitvec_to_nat : SimpExtension ←
+  registerSimpAttr `bitvec_to_nat
+    "simp lemmas converting `BitVec` goals to `Nat` goals"
+
+@[deprecated bitvec_to_nat (since := "2025-02-10")]
+builtin_initialize bvOmegaSimpExtension : SimpExtension ←
+  registerSimpAttr `bv_toNat
+    "simp lemmas converting `BitVec` goals to `Nat` goals, for the `bv_omega` preprocessor"

backend/core/leanprover--lean4---v4.22.0/src/lean/Std/Data/ExtTreeSet/Basic.lean

@@ -0,0 +1,523 @@
+/-
+Copyright (c) 2025 Robin Arnez. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robin Arnez, Markus Himmel, Paul Reichert
+-/
+prelude
+import Std.Data.ExtTreeMap.Basic
+
+/-!
+# Extensional tree sets
+
+This file develops the type `Std.ExtTreeSet` of tree sets.
+
+Lemmas about the operations on `Std.Data.ExtTreeSet` will be available in the
+module `Std.Data.ExtTreeSet.Lemmas`.
+
+See the module `Std.Data.TreeSet.Raw.Basic` for a variant of this type which is safe to use in
+nested inductive types.
+-/
+
+set_option autoImplicit false
+set_option linter.missingDocs true
+
+universe u v w w₂
+
+variable {α : Type u} {cmp : α → α → Ordering}
+
+namespace Std
+
+/--
+Extensional tree sets.
+
+A tree set stores elements of a certain type in a certain order. It depends on a comparator function
+that defines an ordering on the keys and provides efficient order-dependent queries, such as
+retrieval of the minimum or maximum.
+
+To ensure that the operations behave as expected, the comparator function `cmp` should satisfy
+certain laws that ensure a consistent ordering:
+
+* If `a` is less than (or equal) to `b`, then `b` is greater than (or equal) to `a`
+and vice versa (see the `OrientedCmp` typeclass).
+* If `a` is less than or equal to `b` and `b` is, in turn, less than or equal to `c`, then `a`
+is less than or equal to `c` (see the `TransCmp` typeclass).
+
+Keys for which `cmp a b = Ordering.eq` are considered the same, i.e., there can be only one of them
+be contained in a single tree set at the same time.
+
+To avoid expensive copies, users should make sure that the tree set is used linearly.
+
+Internally, the tree sets are represented as size-bounded trees, a type of self-balancing binary
+search tree with efficient order statistic lookups.
+
+In contrast to regular dependent tree maps, `Std.ExtTreeSet` offers several extensionality lemmas
+and therefore has more lemmas about equality of tree sets. This doesn't affect the amount of
+supported functions though: `Std.ExtTreeSet` supports all operations from `Std.TreeMap`.
+
+In order to use most functions, a `TransCmp` instance is required. This is necessary to make sure
+that the functions are congruent, i.e. equivalent tree sets as parameters produce equivalent return
+values.
+
+These tree sets contain a bundled well-formedness invariant, which means that they cannot
+be used in nested inductive types. For these use cases, `Std.TreeSet.Raw` and
+`Std.TreeSet.Raw.WF` unbundle the invariant from the tree set. When in doubt, prefer
+`ExtTreeSet` over `TreeSet.Raw`.
+-/
+structure ExtTreeSet (α : Type u) (cmp : α → α → Ordering := by exact compare) where
+  /-- Internal implementation detail of the tree map. -/
+  inner : ExtTreeMap α Unit cmp
+
+namespace ExtTreeSet
+
+/--
+Creates a new empty tree set. It is also possible and recommended to
+use the empty collection notations `∅` and `{}` to create an empty tree set. `simp` replaces
+`empty` with `∅`.
+-/
+@[inline]
+def empty : ExtTreeSet α cmp :=
+  ⟨ExtTreeMap.empty⟩
+
+instance : EmptyCollection (ExtTreeSet α cmp) where
+  emptyCollection := empty
+
+instance : Inhabited (ExtTreeSet α cmp) where
+  default := ∅
+
+@[simp, grind =]
+theorem empty_eq_emptyc : (empty : ExtTreeSet α cmp) = ∅ :=
+  rfl
+
+/--
+Inserts the given element into the set. If the tree set already contains an element that is
+equal (with regard to `cmp`) to the given element, then the tree set is returned unchanged.
+
+Note: this non-replacement behavior is true for `ExtTreeSet` and `ExtTreeSet.Raw`.
+The `insert` function on `ExtTreeMap`, `ExtDTreeMap`, `ExtTreeMap.Raw` and `ExtDTreeMap.Raw` behaves
+differently: it will overwrite an existing mapping.
+-/
+@[inline]
+def insert [TransCmp cmp] (l : ExtTreeSet α cmp) (a : α) : ExtTreeSet α cmp :=
+  ⟨l.inner.insertIfNew a ()⟩
+
+instance [TransCmp cmp] : Singleton α (ExtTreeSet α cmp) where
+  singleton e := (∅ : ExtTreeSet α cmp).insert e
+
+instance [TransCmp cmp] : Insert α (ExtTreeSet α cmp) where
+  insert e s := s.insert e
+
+instance [TransCmp cmp] : LawfulSingleton α (ExtTreeSet α cmp) where
+  insert_empty_eq _ := rfl
+
+/--
+Checks whether an element is present in a set and inserts the element if it was not found.
+If the tree set already contains an element that is equal (with regard to `cmp` to the given
+element, then the tree set is returned unchanged.
+
+Equivalent to (but potentially faster than) calling `contains` followed by `insert`.
+-/
+@[inline]
+def containsThenInsert [TransCmp cmp] (t : ExtTreeSet α cmp) (a : α) : Bool × ExtTreeSet α cmp :=
+  let p := t.inner.containsThenInsertIfNew a ()
+  (p.1, ⟨p.2⟩)
+
+/--
+Returns `true` if `a`, or an element equal to `a` according to the comparator `cmp`, is contained
+in the set. There is also a `Prop`-valued version of this: `a ∈ t` is equivalent to
+`t.contains a = true`.
+
+Observe that this is different behavior than for lists: for lists, `∈` uses `=` and `contains` uses
+`==` for equality checks, while for tree sets, both use the given comparator `cmp`.
+-/
+@[inline]
+def contains [TransCmp cmp] (l : ExtTreeSet α cmp) (a : α) : Bool :=
+  l.inner.contains a
+
+instance [TransCmp cmp] : Membership α (ExtTreeSet α cmp) where
+  mem m a := m.contains a
+
+instance [TransCmp cmp] {m : ExtTreeSet α cmp} {a : α} : Decidable (a ∈ m) :=
+  inferInstanceAs <| Decidable (m.contains a)
+
+/-- Returns the number of mappings present in the map. -/
+@[inline]
+def size (t : ExtTreeSet α cmp) : Nat :=
+  t.inner.size
+
+/-- Returns `true` if the tree set contains no mappings. -/
+@[inline]
+def isEmpty (t : ExtTreeSet α cmp) : Bool :=
+  t.inner.isEmpty
+
+/-- Removes the given key if it exists. -/
+@[inline]
+def erase [TransCmp cmp] (t : ExtTreeSet α cmp) (a : α) : ExtTreeSet α cmp :=
+  ⟨t.inner.erase a⟩
+
+/--
+Checks if given key is contained and returns the key if it is, otherwise `none`.
+The result in the `some` case is guaranteed to be pointer equal to the key in the map.
+-/
+@[inline]
+def get? [TransCmp cmp] (t : ExtTreeSet α cmp) (a : α) : Option α :=
+  t.inner.getKey? a
+
+/--
+Retrieves the key from the set that matches `a`. Ensures that such a key exists by requiring a proof
+of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the set.
+-/
+@[inline]
+def get [TransCmp cmp] (t : ExtTreeSet α cmp) (a : α) (h : a ∈ t) : α :=
+  t.inner.getKey a h
+
+/--
+Checks if given key is contained and returns the key if it is, otherwise panics.
+If no panic occurs the result is guaranteed to be pointer equal to the key in the set.
+-/
+@[inline]
+def get! [TransCmp cmp] [Inhabited α] (t : ExtTreeSet α cmp) (a : α) : α :=
+  t.inner.getKey! a
+
+/--
+Checks if given key is contained and returns the key if it is, otherwise `fallback`.
+If they key is contained the result is guaranteed to be pointer equal to the key in the set.
+-/
+@[inline]
+def getD [TransCmp cmp] (t : ExtTreeSet α cmp) (a : α) (fallback : α) : α :=
+  t.inner.getKeyD a fallback
+
+/--
+Tries to retrieve the smallest element of the tree set, returning `none` if the set is empty.
+-/
+@[inline]
+def min? [TransCmp cmp] (t : ExtTreeSet α cmp) : Option α :=
+  ExtTreeMap.minKey? t.inner
+
+/--
+Given a proof that the tree set is not empty, retrieves the smallest element.
+-/
+@[inline]
+def min [TransCmp cmp] (t : ExtTreeSet α cmp) (h : t ≠ ∅) : α :=
+  ExtTreeMap.minKey t.inner (fun _ => nomatch t)
+
+/--
+Tries to retrieve the smallest element of the tree set, panicking if the set is empty.
+-/
+@[inline]
+def min! [TransCmp cmp] [Inhabited α] (t : ExtTreeSet α cmp) : α :=
+  ExtTreeMap.minKey! t.inner
+
+/--
+Tries to retrieve the smallest element of the tree set, returning `fallback` if the tree set is empty.
+-/
+@[inline]
+def minD [TransCmp cmp] (t : ExtTreeSet α cmp) (fallback : α) : α :=
+  ExtTreeMap.minKeyD t.inner fallback
+
+/--
+Tries to retrieve the largest element of the tree set, returning `none` if the set is empty.
+-/
+@[inline]
+def max? [TransCmp cmp] (t : ExtTreeSet α cmp) : Option α :=
+  ExtTreeMap.maxKey? t.inner
+
+/--
+Given a proof that the tree set is not empty, retrieves the largest element.
+-/
+@[inline]
+def max [TransCmp cmp] (t : ExtTreeSet α cmp) (h : t ≠ ∅) : α :=
+  ExtTreeMap.maxKey t.inner (fun _ => nomatch t)
+
+/--
+Tries to retrieve the largest element of the tree set, panicking if the set is empty.
+-/
+@[inline]
+def max! [TransCmp cmp] [Inhabited α] (t : ExtTreeSet α cmp) : α :=
+  ExtTreeMap.maxKey! t.inner
+
+/--
+Tries to retrieve the largest element of the tree set, returning `fallback` if the tree set is empty.
+-/
+@[inline]
+def maxD [TransCmp cmp] (t : ExtTreeSet α cmp) (fallback : α) : α :=
+  ExtTreeMap.maxKeyD t.inner fallback
+
+/-- Returns the `n`-th smallest element, or `none` if `n` is at least `t.size`. -/
+@[inline]
+def atIdx? [TransCmp cmp] (t : ExtTreeSet α cmp) (n : Nat) : Option α :=
+  ExtTreeMap.keyAtIdx? t.inner n
+
+/-- Returns the `n`-th smallest element. -/
+@[inline]
+def atIdx [TransCmp cmp] (t : ExtTreeSet α cmp) (n : Nat) (h : n < t.size) : α :=
+  ExtTreeMap.keyAtIdx t.inner n h
+
+/-- Returns the `n`-th smallest element, or panics if `n` is at least `t.size`. -/
+@[inline]
+def atIdx! [TransCmp cmp] [Inhabited α] (t : ExtTreeSet α cmp) (n : Nat) : α :=
+  ExtTreeMap.keyAtIdx! t.inner n
+
+/-- Returns the `n`-th smallest element, or `fallback` if `n` is at least `t.size`. -/
+@[inline]
+def atIdxD [TransCmp cmp] (t : ExtTreeSet α cmp) (n : Nat) (fallback : α) : α :=
+  ExtTreeMap.keyAtIdxD t.inner n fallback
+
+/--
+Tries to retrieve the smallest element that is greater than or equal to the
+given element, returning `none` if no such element exists.
+-/
+@[inline]
+def getGE? [TransCmp cmp] (t : ExtTreeSet α cmp) (k : α) : Option α :=
+  ExtTreeMap.getKeyGE? t.inner k
+
+/--
+Tries to retrieve the smallest element that is greater than the given element,
+returning `none` if no such element exists.
+-/
+@[inline]
+def getGT? [TransCmp cmp] (t : ExtTreeSet α cmp) (k : α) : Option α :=
+  ExtTreeMap.getKeyGT? t.inner k
+
+/--
+Tries to retrieve the largest element that is less than or equal to the
+given element, returning `none` if no such element exists.
+-/
+@[inline]
+def getLE? [TransCmp cmp] (t : ExtTreeSet α cmp) (k : α) : Option α :=
+  ExtTreeMap.getKeyLE? t.inner k
+
+/--
+Tries to retrieve the smallest element that is less than the given element,
+returning `none` if no such element exists.
+-/
+@[inline]
+def getLT? [TransCmp cmp] (t : ExtTreeSet α cmp) (k : α) : Option α :=
+  ExtTreeMap.getKeyLT? t.inner k
+
+/--
+Given a proof that such an element exists, retrieves the smallest element that is
+greater than or equal to the given element.
+-/
+@[inline]
+def getGE [TransCmp cmp] (t : ExtTreeSet α cmp) (k : α) (h : ∃ a ∈ t, (cmp a k).isGE) : α :=
+  ExtTreeMap.getKeyGE t.inner k h
+
+/--
+Given a proof that such an element exists, retrieves the smallest element that is
+greater than the given element.
+-/
+@[inline]
+def getGT [TransCmp cmp] (t : ExtTreeSet α cmp) (k : α) (h : ∃ a ∈ t, cmp a k = .gt) : α :=
+  ExtTreeMap.getKeyGT t.inner k h
+
+/--
+Given a proof that such an element exists, retrieves the largest element that is
+less than or equal to the given element.
+-/
+@[inline]
+def getLE [TransCmp cmp] (t : ExtTreeSet α cmp) (k : α) (h : ∃ a ∈ t, (cmp a k).isLE) : α :=
+  ExtTreeMap.getKeyLE t.inner k h
+
+/--
+Given a proof that such an element exists, retrieves the smallest element that is
+less than the given element.
+-/
+@[inline]
+def getLT [TransCmp cmp] (t : ExtTreeSet α cmp) (k : α) (h : ∃ a ∈ t, cmp a k = .lt) : α :=
+  ExtTreeMap.getKeyLT t.inner k h
+
+/--
+Tries to retrieve the smallest element that is greater than or equal to the
+given element, panicking if no such element exists.
+-/
+@[inline]
+def getGE! [TransCmp cmp] [Inhabited α] (t : ExtTreeSet α cmp) (k : α) : α :=
+  ExtTreeMap.getKeyGE! t.inner k
+
+/--
+Tries to retrieve the smallest element that is greater than the given element,
+panicking if no such element exists.
+-/
+@[inline]
+def getGT! [TransCmp cmp] [Inhabited α] (t : ExtTreeSet α cmp) (k : α) : α :=
+  ExtTreeMap.getKeyGT! t.inner k
+
+/--
+Tries to retrieve the largest element that is less than or equal to the
+given element, panicking if no such element exists.
+-/
+@[inline]
+def getLE! [TransCmp cmp] [Inhabited α] (t : ExtTreeSet α cmp) (k : α) : α :=
+  ExtTreeMap.getKeyLE! t.inner k
+
+/--
+Tries to retrieve the smallest element that is less than the given element,
+panicking if no such element exists.
+-/
+@[inline]
+def getLT! [TransCmp cmp] [Inhabited α] (t : ExtTreeSet α cmp) (k : α) : α :=
+  ExtTreeMap.getKeyLT! t.inner k
+
+/--
+Tries to retrieve the smallest element that is greater than or equal to the
+given element, returning `fallback` if no such element exists.
+-/
+@[inline]
+def getGED [TransCmp cmp] (t : ExtTreeSet α cmp) (k : α) (fallback : α) : α :=
+  ExtTreeMap.getKeyGED t.inner k fallback
+
+/--
+Tries to retrieve the smallest element that is greater than the given element,
+returning `fallback` if no such element exists.
+-/
+@[inline]
+def getGTD [TransCmp cmp] (t : ExtTreeSet α cmp) (k : α) (fallback : α) : α :=
+  ExtTreeMap.getKeyGTD t.inner k fallback
+
+/--
+Tries to retrieve the largest element that is less than or equal to the
+given element, returning `fallback` if no such element exists.
+-/
+@[inline]
+def getLED [TransCmp cmp] (t : ExtTreeSet α cmp) (k : α) (fallback : α) : α :=
+  ExtTreeMap.getKeyLED t.inner k fallback
+
+/--
+Tries to retrieve the smallest element that is less than the given element,
+returning `fallback` if no such element exists.
+-/
+@[inline]
+def getLTD [TransCmp cmp] (t : ExtTreeSet α cmp) (k : α) (fallback : α) : α :=
+  ExtTreeMap.getKeyLTD t.inner k fallback
+
+variable {γ δ : Type w} {m : Type w → Type w₂} [Monad m] [LawfulMonad m]
+
+/-- Removes all elements from the tree set for which the given function returns `false`. -/
+@[inline]
+def filter (f : α → Bool) (m : ExtTreeSet α cmp) : ExtTreeSet α cmp :=
+  ⟨m.inner.filter fun a _ => f a⟩
+
+/--
+Monadically computes a value by folding the given function over the elements in the tree set in
+ascending order.
+-/
+@[inline]
+def foldlM [TransCmp cmp] (f : δ → (a : α) → m δ) (init : δ) (t : ExtTreeSet α cmp) : m δ :=
+  t.inner.foldlM (fun c a _ => f c a) init
+
+/-- Folds the given function over the elements of the tree set in ascending order. -/
+@[inline]
+def foldl [TransCmp cmp] (f : δ → (a : α) → δ) (init : δ) (t : ExtTreeSet α cmp) : δ :=
+  t.inner.foldl (fun c a _ => f c a) init
+
+/--
+Monadically computes a value by folding the given function over the elements in the tree set in
+descending order.
+-/
+@[inline]
+def foldrM [TransCmp cmp] (f : (a : α) → δ → m δ) (init : δ) (t : ExtTreeSet α cmp) : m δ :=
+  t.inner.foldrM (fun a _ acc => f a acc) init
+
+/-- Folds the given function over the elements of the tree set in descending order. -/
+@[inline]
+def foldr [TransCmp cmp] (f : (a : α) → δ → δ) (init : δ) (t : ExtTreeSet α cmp) : δ :=
+  t.inner.foldr (fun a _ acc => f a acc) init
+
+/-- Partitions a tree set into two tree sets based on a predicate. -/
+@[inline]
+def partition [TransCmp cmp] (f : (a : α) → Bool) (t : ExtTreeSet α cmp) :
+    ExtTreeSet α cmp × ExtTreeSet α cmp :=
+  let p := t.inner.partition fun a _ => f a; (⟨p.1⟩, ⟨p.2⟩)
+
+/-- Carries out a monadic action on each element in the tree set in ascending order. -/
+@[inline]
+def forM [TransCmp cmp] (f : α → m PUnit) (t : ExtTreeSet α cmp) : m PUnit :=
+  t.inner.forM (fun a _ => f a)
+
+/--
+Support for the `for` loop construct in `do` blocks. The iteration happens in ascending
+order.
+-/
+@[inline]
+def forIn [TransCmp cmp] (f : α → δ → m (ForInStep δ)) (init : δ) (t : ExtTreeSet α cmp) : m δ :=
+  t.inner.forIn (fun a _ c => f a c) init
+
+/-
+Note: We ignore the monad instance provided by `forM` / `forIn` and instead use the one from the
+instance in order to get the `LawfulMonad m` assumption
+-/
+
+instance [TransCmp cmp] [inst : Monad m] [LawfulMonad m] : ForM m (ExtTreeSet α cmp) α where
+  forM t f := @forM _ _ _ inst _ _ f t
+
+instance [TransCmp cmp] [inst : Monad m] [LawfulMonad m] : ForIn m (ExtTreeSet α cmp) α where
+  forIn m init f := @forIn _ _ _ _ inst _ _ f init m
+
+/-- Check if all elements satisfy the predicate, short-circuiting if a predicate fails. -/
+@[inline]
+def any [TransCmp cmp] (t : ExtTreeSet α cmp) (p : α → Bool) : Bool :=
+  t.inner.any (fun a _ => p a)
+
+/-- Check if any element satisfies the predicate, short-circuiting if a predicate succeeds. -/
+@[inline]
+def all [TransCmp cmp] (t : ExtTreeSet α cmp) (p : α → Bool) : Bool :=
+  t.inner.all (fun a _ => p a)
+
+/-- Transforms the tree set into a list of elements in ascending order. -/
+@[inline]
+def toList [TransCmp cmp] (t : ExtTreeSet α cmp) : List α :=
+  t.inner.keys
+
+/-- Transforms a list into a tree set. -/
+def ofList (l : List α) (cmp : α → α → Ordering := by exact compare) : ExtTreeSet α cmp :=
+  ⟨ExtTreeMap.unitOfList l cmp⟩
+
+/-- Transforms the tree set into an array of elements in ascending order. -/
+@[inline]
+def toArray [TransCmp cmp] (t : ExtTreeSet α cmp) : Array α :=
+  t.inner.keysArray
+
+/-- Transforms an array into a tree set. -/
+def ofArray (a : Array α) (cmp : α → α → Ordering := by exact compare) : ExtTreeSet α cmp :=
+  ⟨ExtTreeMap.unitOfArray a cmp⟩
+
+/--
+Returns a set that contains all mappings of `t₁` and `t₂.
+
+This function ensures that `t₁` is used linearly.
+Hence, as long as `t₁` is unshared, the performance characteristics follow the following imperative
+description: Iterate over all mappings in `t₂`, inserting them into `t₁`.
+
+Hence, the runtime of this method scales logarithmically in the size of `t₁` and linearly in the
+size of `t₂` as long as `t₁` is unshared.
+-/
+@[inline]
+def merge [TransCmp cmp] (t₁ t₂ : ExtTreeSet α cmp) : ExtTreeSet α cmp :=
+  ⟨ExtTreeMap.mergeWith (fun _ _ _ => ()) t₁.inner t₂.inner⟩
+
+/--
+Inserts multiple elements into the tree set by iterating over the given collection and calling
+`insert`. If the same element (with respect to `cmp`) appears multiple times, the first occurrence
+takes precedence.
+
+Note: this precedence behavior is true for `ExtTreeSet` and `ExtTreeSet.Raw`. The `insertMany` function on
+`ExtTreeMap`, `ExtDTreeMap`, `ExtTreeMap.Raw` and `ExtDTreeMap.Raw` behaves differently: it will prefer the last
+appearance.
+-/
+@[inline]
+def insertMany [TransCmp cmp] {ρ} [ForIn Id ρ α] (t : ExtTreeSet α cmp) (l : ρ) : ExtTreeSet α cmp :=
+  ⟨ExtTreeMap.insertManyIfNewUnit t.inner l⟩
+
+/--
+Erases multiple items from the tree set by iterating over the given collection and calling erase.
+-/
+@[inline]
+def eraseMany [TransCmp cmp] {ρ} [ForIn Id ρ α] (t : ExtTreeSet α cmp) (l : ρ) : ExtTreeSet α cmp :=
+  ⟨t.inner.eraseMany l⟩
+
+instance [TransCmp cmp] [Repr α] : Repr (ExtTreeSet α cmp) where
+  reprPrec m prec := Repr.addAppParen ("Std.ExtTreeSet.ofList " ++ repr m.toList) prec
+
+end ExtTreeSet
+
+end Std

backend/core/leanprover--lean4---v4.22.0/src/lean/Std/Data/ExtTreeSet/Lemmas.lean

@@ -0,0 +1,1539 @@
+/-
+Copyright (c) 2025 Robin Arnez. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robin Arnez, Markus Himmel, Paul Reichert
+-/
+prelude
+import Std.Data.ExtTreeMap.Lemmas
+import Std.Data.ExtTreeSet.Basic
+
+/-!
+# Tree set lemmas
+
+This file contains lemmas about `Std.ExtTreeSet`.
+-/
+
+set_option linter.missingDocs true
+set_option autoImplicit false
+
+universe u v w w'
+
+namespace Std.ExtTreeSet
+
+variable {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp}
+
+private theorem ext {t t' : ExtTreeSet α cmp} : t.inner = t'.inner → t = t' := by
+  cases t; cases t'; rintro rfl; rfl
+
+private theorem ext_iff {t t' : ExtTreeSet α cmp} : t = t' ↔ t.inner = t'.inner :=
+  ⟨fun h => h ▸ rfl, ext⟩
+
+@[simp]
+theorem isEmpty_iff {t : ExtTreeSet α cmp} [TransCmp cmp] : t.isEmpty ↔ t = ∅ :=
+  ExtTreeMap.isEmpty_iff.trans ext_iff.symm
+
+@[simp]
+theorem isEmpty_eq_false_iff {t : ExtTreeSet α cmp} [TransCmp cmp] : t.isEmpty = false ↔ ¬t = ∅ :=
+  (Bool.not_eq_true _).symm.to_iff.trans (not_congr isEmpty_iff)
+
+@[simp, grind =]
+theorem isEmpty_empty : (∅ : ExtTreeSet α cmp).isEmpty :=
+  ExtTreeMap.isEmpty_empty
+
+@[simp]
+theorem empty_eq : ∅ = t ↔ t = ∅ := eq_comm
+
+@[simp]
+theorem insert_ne_empty [TransCmp cmp] {k : α} :
+    t.insert k ≠ ∅ :=
+  mt ext_iff.mp ExtTreeMap.insertIfNew_ne_empty
+
+@[grind =]
+theorem mem_iff_contains [TransCmp cmp] {k : α} : k ∈ t ↔ t.contains k :=
+  ExtTreeMap.mem_iff_contains
+
+@[simp, grind _=_]
+theorem contains_iff_mem [TransCmp cmp] {k : α} : t.contains k ↔ k ∈ t :=
+  ExtTreeMap.contains_iff_mem
+
+theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) :
+    t.contains k = t.contains k' :=
+  ExtTreeMap.contains_congr hab
+
+theorem mem_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) : k ∈ t ↔ k' ∈ t :=
+  ExtTreeMap.mem_congr hab
+
+@[simp, grind =]
+theorem contains_empty [TransCmp cmp] {k : α} : (∅ : ExtTreeSet α cmp).contains k = false :=
+  rfl
+
+@[simp]
+theorem not_mem_empty [TransCmp cmp] {k : α} : k ∉ (∅ : ExtTreeSet α cmp) :=
+  Bool.false_ne_true
+
+theorem eq_empty_iff_forall_contains [TransCmp cmp] : t = ∅ ↔ ∀ a, t.contains a = false :=
+  ext_iff.trans ExtTreeMap.eq_empty_iff_forall_contains
+
+theorem eq_empty_iff_forall_not_mem [TransCmp cmp] : t = ∅ ↔ ∀ a, ¬a ∈ t :=
+  ext_iff.trans ExtTreeMap.eq_empty_iff_forall_not_mem
+
+theorem ne_empty_of_mem [TransCmp cmp] {a : α} (h : a ∈ t) : t ≠ ∅ :=
+  (not_congr eq_empty_iff_forall_not_mem).mpr fun h' => h' a h
+
+@[simp]
+theorem insert_eq_insert [TransCmp cmp] {p : α} : Insert.insert p t = t.insert p :=
+  rfl
+
+@[simp]
+theorem singleton_eq_insert [TransCmp cmp] {p : α} :
+    Singleton.singleton p = (∅ : ExtTreeSet α cmp).insert p :=
+  rfl
+
+@[simp, grind =]
+theorem contains_insert [TransCmp cmp] {k a : α} :
+    (t.insert k).contains a = (cmp k a == .eq || t.contains a) :=
+  ExtTreeMap.contains_insertIfNew
+
+@[simp, grind =]
+theorem mem_insert [TransCmp cmp] {k a : α} :
+    a ∈ t.insert k ↔ cmp k a = .eq ∨ a ∈ t :=
+  ExtTreeMap.mem_insertIfNew
+
+theorem contains_insert_self [TransCmp cmp] {k : α} :
+    (t.insert k).contains k :=
+  ExtTreeMap.contains_insertIfNew_self
+
+theorem mem_insert_self [TransCmp cmp] {k : α} :
+    k ∈ t.insert k :=
+  ExtTreeMap.mem_insertIfNew_self
+
+theorem contains_of_contains_insert [TransCmp cmp] {k a : α} :
+    (t.insert k).contains a → cmp k a ≠ .eq → t.contains a :=
+  ExtTreeMap.contains_of_contains_insertIfNew
+
+theorem mem_of_mem_insert [TransCmp cmp] {k a : α} :
+    a ∈ t.insert k → cmp k a ≠ .eq → a ∈ t :=
+  ExtTreeMap.mem_of_mem_insertIfNew
+
+/-- This is a restatement of `mem_of_mem_insert` that is written to exactly match the
+proof obligation in the statement of `get_insert`. -/
+theorem mem_of_mem_insert' [TransCmp cmp] {k a : α} :
+    a ∈ t.insert k → ¬ (cmp k a = .eq ∧ ¬ k ∈ t) → a ∈ t :=
+  ExtTreeMap.mem_of_mem_insertIfNew'
+
+@[simp, grind =]
+theorem size_empty : (∅ : ExtTreeSet α cmp).size = 0 :=
+  ExtTreeMap.size_empty
+
+theorem isEmpty_eq_size_beq_zero : t.isEmpty = (t.size == 0) :=
+  ExtTreeMap.isEmpty_eq_size_beq_zero
+
+theorem eq_empty_iff_size_eq_zero [TransCmp cmp] : t = ∅ ↔ t.size = 0 :=
+  ext_iff.trans ExtTreeMap.eq_empty_iff_size_eq_zero
+
+@[grind =]
+theorem size_insert [TransCmp cmp] {k : α} :
+    (t.insert k).size = if t.contains k then t.size else t.size + 1 :=
+  ExtTreeMap.size_insertIfNew
+
+theorem size_le_size_insert [TransCmp cmp] {k : α} :
+    t.size ≤ (t.insert k).size :=
+  ExtTreeMap.size_le_size_insertIfNew
+
+theorem size_insert_le [TransCmp cmp] {k : α} :
+    (t.insert k).size ≤ t.size + 1 :=
+  ExtTreeMap.size_insertIfNew_le
+
+@[simp, grind =]
+theorem erase_empty [TransCmp cmp] {k : α} : (∅ : ExtTreeSet α cmp).erase k = ∅ :=
+  ext ExtTreeMap.erase_empty
+
+@[simp, grind =]
+theorem erase_eq_empty_iff [TransCmp cmp] {k : α} :
+    t.erase k = ∅ ↔ t = ∅ ∨ (t.size = 1 ∧ k ∈ t) := by
+  simpa only [ext_iff] using ExtTreeMap.erase_eq_empty_iff
+
+theorem eq_empty_iff_erase_eq_empty_and_not_mem [TransCmp cmp] (k : α) :
+    t = ∅ ↔ t.erase k = ∅ ∧ ¬k ∈ t := by
+  simpa only [ext_iff] using ExtTreeMap.eq_empty_iff_erase_eq_empty_and_not_mem k
+
+theorem ne_empty_of_erase_ne_empty [TransCmp cmp] {k : α} (h : t.erase k ≠ ∅) : t ≠ ∅ := by
+  simp_all
+
+@[simp, grind =]
+theorem contains_erase [TransCmp cmp] {k a : α} :
+    (t.erase k).contains a = (cmp k a != .eq && t.contains a) :=
+  ExtTreeMap.contains_erase
+
+@[simp, grind =]
+theorem mem_erase [TransCmp cmp] {k a : α} :
+    a ∈ t.erase k ↔ cmp k a ≠ .eq ∧ a ∈ t :=
+  ExtTreeMap.mem_erase
+
+theorem contains_of_contains_erase [TransCmp cmp] {k a : α} :
+    (t.erase k).contains a → t.contains a :=
+  ExtTreeMap.contains_of_contains_erase
+
+theorem mem_of_mem_erase [TransCmp cmp] {k a : α} :
+    (t.erase k).contains a → t.contains a :=
+  ExtTreeMap.mem_of_mem_erase
+
+@[grind =]
+theorem size_erase [TransCmp cmp] {k : α} :
+    (t.erase k).size = if t.contains k then t.size - 1 else t.size :=
+  ExtTreeMap.size_erase
+
+theorem size_erase_le [TransCmp cmp] {k : α} :
+    (t.erase k).size ≤ t.size :=
+  ExtTreeMap.size_erase_le
+
+theorem size_le_size_erase [TransCmp cmp] {k : α} :
+    t.size ≤ (t.erase k).size + 1 :=
+  ExtTreeMap.size_le_size_erase
+
+@[simp, grind =]
+theorem get?_empty [TransCmp cmp] {a : α} : (∅ : ExtTreeSet α cmp).get? a = none :=
+  ExtTreeMap.getKey?_empty
+
+@[grind =] theorem get?_insert [TransCmp cmp] {k a : α} :
+    (t.insert k).get? a = if cmp k a = .eq ∧ ¬k ∈ t then some k else t.get? a :=
+  ExtTreeMap.getKey?_insertIfNew
+
+theorem contains_eq_isSome_get? [TransCmp cmp] {a : α} :
+    t.contains a = (t.get? a).isSome :=
+  ExtTreeMap.contains_eq_isSome_getKey?
+
+@[simp, grind =]
+theorem isSome_get?_eq_contains [TransCmp cmp] {a : α} :
+    (t.get? a).isSome = t.contains a :=
+  contains_eq_isSome_get?.symm
+
+theorem mem_iff_isSome_get? [TransCmp cmp] {a : α} :
+    a ∈ t ↔ (t.get? a).isSome :=
+  ExtTreeMap.mem_iff_isSome_getKey?
+
+@[simp]
+theorem isSome_get?_iff_mem [TransCmp cmp] {a : α} :
+    (t.get? a).isSome ↔ a ∈ t :=
+  mem_iff_isSome_get?.symm
+
+theorem get?_eq_none_of_contains_eq_false [TransCmp cmp] {a : α} :
+    t.contains a = false → t.get? a = none :=
+  ExtTreeMap.getKey?_eq_none_of_contains_eq_false
+
+theorem get?_eq_none [TransCmp cmp] {a : α} :
+    ¬ a ∈ t → t.get? a = none :=
+  ExtTreeMap.getKey?_eq_none
+
+@[grind =] theorem get?_erase [TransCmp cmp] {k a : α} :
+    (t.erase k).get? a = if cmp k a = .eq then none else t.get? a :=
+  ExtTreeMap.getKey?_erase
+
+@[simp]
+theorem get?_erase_self [TransCmp cmp] {k : α} :
+    (t.erase k).get? k = none :=
+  ExtTreeMap.getKey?_erase_self
+
+theorem compare_get?_self [TransCmp cmp] {k : α} :
+    (t.get? k).all (cmp · k = .eq) :=
+  ExtTreeMap.compare_getKey?_self
+
+theorem get?_congr [TransCmp cmp] {k k' : α} (h' : cmp k k' = .eq) :
+    t.get? k = t.get? k' :=
+  ExtTreeMap.getKey?_congr h'
+
+theorem get?_eq_some_of_contains [TransCmp cmp] [LawfulEqCmp cmp] {k : α} (h' : t.contains k) :
+    t.get? k = some k :=
+  ExtTreeMap.getKey?_eq_some_of_contains h'
+
+theorem get?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] {k : α} (h' : k ∈ t) :
+    t.get? k = some k :=
+  ExtTreeMap.getKey?_eq_some_of_contains h'
+
+@[grind =] theorem get_insert [TransCmp cmp] {k a : α} {h₁} :
+    (t.insert k).get a h₁ =
+      if h₂ : cmp k a = .eq ∧ ¬ k ∈ t then k
+      else t.get a (mem_of_mem_insert' h₁ h₂) :=
+  ExtTreeMap.getKey_insertIfNew
+
+@[simp, grind =] theorem get_erase [TransCmp cmp] {k a : α} {h'} :
+    (t.erase k).get a h' = t.get a (mem_of_mem_erase h') :=
+  ExtTreeMap.getKey_erase
+
+theorem get?_eq_some_get [TransCmp cmp] {a : α} (h') :
+    t.get? a = some (t.get a h') :=
+  ExtTreeMap.getKey?_eq_some_getKey h'
+
+theorem compare_get_self [TransCmp cmp] {k : α} (h' : k ∈ t) :
+    cmp (t.get k h') k = .eq :=
+  ExtTreeMap.compare_getKey_self h'
+
+theorem get_congr [TransCmp cmp] {k₁ k₂ : α} (h' : cmp k₁ k₂ = .eq)
+    (h₁ : k₁ ∈ t) : t.get k₁ h₁ = t.get k₂ ((mem_congr h').mp h₁) :=
+  ExtTreeMap.getKey_congr h' h₁
+
+@[simp, grind =]
+theorem get_eq [TransCmp cmp] [LawfulEqCmp cmp] {k : α} (h' : k ∈ t) :
+    t.get k h' = k :=
+  ExtTreeMap.getKey_eq h'
+
+@[simp, grind =]
+theorem get!_empty [TransCmp cmp] [Inhabited α] {a : α} :
+    (∅ : ExtTreeSet α cmp).get! a = default :=
+  ExtTreeMap.getKey!_empty
+
+@[grind =] theorem get!_insert [TransCmp cmp] [Inhabited α] {k a : α} :
+    (t.insert k).get! a = if cmp k a = .eq ∧ ¬ k ∈ t then k else t.get! a :=
+  ExtTreeMap.getKey!_insertIfNew
+
+theorem get!_eq_default_of_contains_eq_false [TransCmp cmp] [Inhabited α] {a : α} :
+    t.contains a = false → t.get! a = default :=
+  ExtTreeMap.getKey!_eq_default_of_contains_eq_false
+
+theorem get!_eq_default [TransCmp cmp] [Inhabited α] {a : α} :
+    ¬ a ∈ t → t.get! a = default :=
+  ExtTreeMap.getKey!_eq_default
+
+@[grind =] theorem get!_erase [TransCmp cmp] [Inhabited α] {k a : α} :
+    (t.erase k).get! a = if cmp k a = .eq then default else t.get! a :=
+  ExtTreeMap.getKey!_erase
+
+@[simp]
+theorem get!_erase_self [TransCmp cmp] [Inhabited α] {k : α} :
+    (t.erase k).get! k = default :=
+  ExtTreeMap.getKey!_erase_self
+
+theorem get?_eq_some_get!_of_contains [TransCmp cmp] [Inhabited α] {a : α} :
+    t.contains a = true → t.get? a = some (t.get! a) :=
+  ExtTreeMap.getKey?_eq_some_getKey!_of_contains
+
+theorem get?_eq_some_get! [TransCmp cmp] [Inhabited α] {a : α} :
+    a ∈ t → t.get? a = some (t.get! a) :=
+  ExtTreeMap.getKey?_eq_some_getKey!
+
+theorem get!_eq_get!_get? [TransCmp cmp] [Inhabited α] {a : α} :
+    t.get! a = (t.get? a).get! :=
+  ExtTreeMap.getKey!_eq_get!_getKey?
+
+theorem get_eq_get! [TransCmp cmp] [Inhabited α] {a : α} {h} :
+    t.get a h = t.get! a :=
+  ExtTreeMap.getKey_eq_getKey!
+
+theorem get!_congr [TransCmp cmp] [Inhabited α] {k k' : α} (h' : cmp k k' = .eq) :
+    t.get! k = t.get! k' :=
+  ExtTreeMap.getKey!_congr h'
+
+theorem get!_eq_of_contains [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k : α}
+    (h' : t.contains k) :
+    t.get! k = k :=
+  ExtTreeMap.getKey!_eq_of_contains h'
+
+theorem get!_eq_of_mem [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k : α} (h' : k ∈ t) :
+    t.get! k = k :=
+  ExtTreeMap.getKey!_eq_of_mem h'
+
+@[simp, grind =]
+theorem getD_empty [TransCmp cmp] {a : α} {fallback : α} :
+    (∅ : ExtTreeSet α cmp).getD a fallback = fallback :=
+  ExtTreeMap.getKeyD_empty
+
+@[grind =] theorem getD_insert [TransCmp cmp] {k a fallback : α} :
+    (t.insert k).getD a fallback =
+      if cmp k a = .eq ∧ ¬ k ∈ t then k else t.getD a fallback :=
+  ExtTreeMap.getKeyD_insertIfNew
+
+theorem getD_eq_fallback_of_contains_eq_false [TransCmp cmp] {a fallback : α} :
+    t.contains a = false → t.getD a fallback = fallback :=
+  ExtTreeMap.getKeyD_eq_fallback_of_contains_eq_false
+
+theorem getD_eq_fallback [TransCmp cmp] {a fallback : α} :
+    ¬ a ∈ t → t.getD a fallback = fallback :=
+  ExtTreeMap.getKeyD_eq_fallback
+
+@[grind =] theorem getD_erase [TransCmp cmp] {k a fallback : α} :
+    (t.erase k).getD a fallback =
+      if cmp k a = .eq then fallback else t.getD a fallback :=
+  ExtTreeMap.getKeyD_erase
+
+@[simp]
+theorem getD_erase_self [TransCmp cmp] {k fallback : α} :
+    (t.erase k).getD k fallback = fallback :=
+  ExtTreeMap.getKeyD_erase_self
+
+theorem get?_eq_some_getD_of_contains [TransCmp cmp] {a fallback : α} :
+    t.contains a = true → t.get? a = some (t.getD a fallback) :=
+  ExtTreeMap.getKey?_eq_some_getKeyD_of_contains
+
+theorem get?_eq_some_getD [TransCmp cmp] {a fallback : α} :
+    a ∈ t → t.get? a = some (t.getD a fallback) :=
+  ExtTreeMap.getKey?_eq_some_getKeyD
+
+theorem getD_eq_getD_get? [TransCmp cmp] {a fallback : α} :
+    t.getD a fallback = (t.get? a).getD fallback :=
+  ExtTreeMap.getKeyD_eq_getD_getKey?
+
+theorem get_eq_getD [TransCmp cmp] {a fallback : α} {h} :
+    t.get a h = t.getD a fallback :=
+  ExtTreeMap.getKey_eq_getKeyD
+
+theorem get!_eq_getD_default [TransCmp cmp] [Inhabited α] {a : α} :
+    t.get! a = t.getD a default :=
+  ExtTreeMap.getKey!_eq_getKeyD_default
+
+theorem getD_congr [TransCmp cmp] {k k' fallback : α} (h' : cmp k k' = .eq) :
+    t.getD k fallback = t.getD k' fallback :=
+  ExtTreeMap.getKeyD_congr h'
+
+theorem getD_eq_of_contains [TransCmp cmp] [LawfulEqCmp cmp] {k fallback : α} (h' : t.contains k) :
+    t.getD k fallback = k :=
+  ExtTreeMap.getKeyD_eq_of_contains h'
+
+theorem getD_eq_of_mem [TransCmp cmp] [LawfulEqCmp cmp] {k fallback : α} (h' : k ∈ t) :
+    t.getD k fallback = k :=
+  ExtTreeMap.getKeyD_eq_of_contains h'
+
+@[simp, grind =]
+theorem containsThenInsert_fst [TransCmp cmp] {k : α} :
+    (t.containsThenInsert k).1 = t.contains k :=
+  ExtTreeMap.containsThenInsertIfNew_fst
+
+@[simp, grind =]
+theorem containsThenInsert_snd [TransCmp cmp] {k : α} :
+    (t.containsThenInsert k).2 = t.insert k :=
+  ext <| ExtTreeMap.containsThenInsertIfNew_snd
+
+@[simp, grind =]
+theorem length_toList [TransCmp cmp] :
+    t.toList.length = t.size :=
+  ExtTreeMap.length_keys
+
+@[simp, grind =]
+theorem isEmpty_toList [TransCmp cmp] :
+    t.toList.isEmpty = t.isEmpty :=
+  ExtTreeMap.isEmpty_keys
+
+@[simp]
+theorem toList_eq_nil_iff [TransCmp cmp] :
+    t.toList = [] ↔ t = ∅ :=
+  ExtTreeMap.keys_eq_nil_iff.trans ext_iff.symm
+
+@[simp, grind =]
+theorem contains_toList [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] {k : α} :
+    t.toList.contains k = t.contains k :=
+  ExtTreeMap.contains_keys
+
+@[simp]
+theorem mem_toList [LawfulEqCmp cmp] [TransCmp cmp] {k : α} :
+    k ∈ t.toList ↔ k ∈ t :=
+  ExtTreeMap.mem_keys
+
+theorem distinct_toList [TransCmp cmp] :
+    t.toList.Pairwise (fun a b => ¬ cmp a b = .eq) :=
+  ExtTreeMap.distinct_keys
+
+theorem ordered_toList [TransCmp cmp] :
+    t.toList.Pairwise (fun a b => cmp a b = .lt) :=
+  ExtTreeMap.ordered_keys
+
+section monadic
+
+variable {δ : Type w} {m : Type w → Type w'}
+
+theorem foldlM_eq_foldlM_toList [TransCmp cmp] [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} :
+    t.foldlM f init = t.toList.foldlM f init :=
+  ExtTreeMap.foldlM_eq_foldlM_keys
+
+theorem foldl_eq_foldl_toList [TransCmp cmp] {f : δ → α → δ} {init : δ} :
+    t.foldl f init = t.toList.foldl f init :=
+  ExtTreeMap.foldl_eq_foldl_keys
+
+theorem foldrM_eq_foldrM_toList [TransCmp cmp] [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} :
+    t.foldrM f init = t.toList.foldrM f init :=
+  ExtTreeMap.foldrM_eq_foldrM_keys
+
+theorem foldr_eq_foldr_toList [TransCmp cmp] {f : α → δ → δ} {init : δ} :
+    t.foldr f init = t.toList.foldr f init :=
+  ExtTreeMap.foldr_eq_foldr_keys
+
+@[simp, grind =]
+theorem forM_eq_forM [TransCmp cmp] [Monad m] [LawfulMonad m] {f : α → m PUnit} :
+    t.forM f = ForM.forM t f := rfl
+
+theorem forM_eq_forM_toList [TransCmp cmp] [Monad m] [LawfulMonad m] {f : α → m PUnit} :
+    ForM.forM t f = t.toList.forM f :=
+  ExtTreeMap.forM_eq_forM_keys
+
+@[simp, grind =]
+theorem forIn_eq_forIn [TransCmp cmp] [Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ} :
+    t.forIn f init = ForIn.forIn t init f := rfl
+
+theorem forIn_eq_forIn_toList [TransCmp cmp] [Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ} :
+    ForIn.forIn t init f = ForIn.forIn t.toList init f :=
+  ExtTreeMap.forIn_eq_forIn_keys
+
+end monadic
+
+@[simp, grind =]
+theorem insertMany_nil [TransCmp cmp] : t.insertMany [] = t :=
+  rfl
+
+@[simp, grind =]
+theorem insertMany_list_singleton [TransCmp cmp] {k : α} :
+    t.insertMany [k] = t.insert k :=
+  rfl
+
+@[grind _=_]
+theorem insertMany_cons [TransCmp cmp] {l : List α} {k : α} :
+    t.insertMany (k :: l) = (t.insert k).insertMany l :=
+  ext ExtTreeMap.insertManyIfNewUnit_cons
+
+@[grind _=_]
+theorem insertMany_append [TransCmp cmp] {l₁ l₂ : List α} :
+    insertMany t (l₁ ++ l₂) = insertMany (insertMany t l₁) l₂ := by
+  induction l₁ generalizing t with
+  | nil => simp
+  | cons hd tl ih =>
+    rw [List.cons_append, insertMany_cons, insertMany_cons, ih]
+
+@[simp, grind =]
+theorem contains_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
+    {l : List α} {k : α} :
+    (t.insertMany l).contains k = (t.contains k || l.contains k) :=
+  ExtTreeMap.contains_insertManyIfNewUnit_list
+
+@[simp, grind =]
+theorem mem_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
+    {l : List α} {k : α} :
+    k ∈ insertMany t l ↔ k ∈ t ∨ l.contains k :=
+  ExtTreeMap.mem_insertManyIfNewUnit_list
+
+theorem mem_of_mem_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
+    {l : List α} {k : α} (contains_eq_false : l.contains k = false) :
+    k ∈ insertMany t l → k ∈ t :=
+  ExtTreeMap.mem_of_mem_insertManyIfNewUnit_list contains_eq_false
+
+theorem get?_insertMany_list_of_not_mem_of_contains_eq_false
+    [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α}
+    (not_mem : ¬ k ∈ t) (contains_eq_false : l.contains k = false) :
+    get? (insertMany t l) k = none :=
+  ExtTreeMap.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
+    not_mem contains_eq_false
+
+theorem get?_insertMany_list_of_not_mem_of_mem [TransCmp cmp]
+    {l : List α} {k k' : α} (k_eq : cmp k k' = .eq)
+    (not_mem : ¬ k ∈ t) (distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) (mem : k ∈ l) :
+    get? (insertMany t l) k' = some k :=
+  ExtTreeMap.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem k_eq not_mem distinct mem
+
+theorem get?_insertMany_list_of_mem [TransCmp cmp]
+    {l : List α} {k : α} (mem : k ∈ t) :
+    get? (insertMany t l) k = get? t k :=
+  ExtTreeMap.getKey?_insertManyIfNewUnit_list_of_mem mem
+
+theorem get_insertMany_list_of_mem [TransCmp cmp]
+    {l : List α} {k : α} {h'} (contains : k ∈ t) :
+    get (insertMany t l) k h' = get t k contains :=
+  ExtTreeMap.getKey_insertManyIfNewUnit_list_of_mem contains
+
+theorem get_insertMany_list_of_not_mem_of_mem [TransCmp cmp]
+    {l : List α}
+    {k k' : α} (k_eq : cmp k k' = .eq) {h'} (not_mem : ¬ k ∈ t)
+    (distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) (mem : k ∈ l) :
+    get (insertMany t l) k' h' = k :=
+  ExtTreeMap.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem k_eq not_mem distinct mem
+
+theorem get!_insertMany_list_of_not_mem_of_contains_eq_false
+    [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited α] {l : List α} {k : α}
+    (not_mem : ¬ k ∈ t) (contains_eq_false : l.contains k = false) :
+    get! (insertMany t l) k = default :=
+  ExtTreeMap.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
+    not_mem contains_eq_false
+
+theorem get!_insertMany_list_of_not_mem_of_mem [TransCmp cmp]
+    [Inhabited α] {l : List α} {k k' : α} (k_eq : cmp k k' = .eq)
+    (not_mem : ¬ k ∈ t) (distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) (mem : k ∈ l) :
+    get! (insertMany t l) k' = k :=
+  ExtTreeMap.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem k_eq not_mem distinct mem
+
+theorem get!_insertMany_list_of_mem [TransCmp cmp]
+    [Inhabited α] {l : List α} {k : α} (mem : k ∈ t):
+    get! (insertMany t l) k = get! t k :=
+  ExtTreeMap.getKey!_insertManyIfNewUnit_list_of_mem mem
+
+theorem getD_insertMany_list_of_not_mem_of_contains_eq_false
+    [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k fallback : α}
+    (not_mem : ¬ k ∈ t) (contains_eq_false : l.contains k = false) :
+    getD (insertMany t l) k fallback = fallback :=
+  ExtTreeMap.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
+    not_mem contains_eq_false
+
+theorem getD_insertMany_list_of_not_mem_of_mem [TransCmp cmp]
+    {l : List α} {k k' fallback : α} (k_eq : cmp k k' = .eq)
+    (not_mem : ¬ k ∈ t) (distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) (mem : k ∈ l) :
+    getD (insertMany t l) k' fallback = k :=
+  ExtTreeMap.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem k_eq not_mem distinct mem
+
+theorem getD_insertMany_list_of_mem [TransCmp cmp]
+    {l : List α} {k fallback : α} (mem : k ∈ t) :
+    getD (insertMany t l) k fallback = getD t k fallback :=
+  ExtTreeMap.getKeyD_insertManyIfNewUnit_list_of_mem mem
+
+theorem size_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
+    {l : List α}
+    (distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) :
+    (∀ (a : α), a ∈ t → l.contains a = false) →
+    (insertMany t l).size = t.size + l.length :=
+  ExtTreeMap.size_insertManyIfNewUnit_list distinct
+
+theorem size_le_size_insertMany_list [TransCmp cmp]
+    {l : List α} :
+    t.size ≤ (insertMany t l).size :=
+  ExtTreeMap.size_le_size_insertManyIfNewUnit_list
+
+grind_pattern size_le_size_insertMany_list => (insertMany t l).size
+
+theorem size_insertMany_list_le [TransCmp cmp]
+    {l : List α} :
+    (insertMany t l).size ≤ t.size + l.length :=
+  ExtTreeMap.size_insertManyIfNewUnit_list_le
+
+grind_pattern size_insertMany_list_le => (insertMany t l).size
+
+@[simp, grind =]
+theorem isEmpty_insertMany_list [TransCmp cmp] {l : List α} :
+    (t.insertMany l).isEmpty = (t.isEmpty && l.isEmpty) :=
+  ExtTreeMap.isEmpty_insertManyIfNewUnit_list
+
+@[simp]
+theorem insertMany_list_eq_empty_iff [TransCmp cmp] {l : List α} :
+    t.insertMany l = ∅ ↔ t = ∅ ∧ l = [] := by
+  simpa only [ext_iff] using ExtTreeMap.insertManyIfNewUnit_list_eq_empty_iff
+
+@[simp, grind =]
+theorem ofList_nil :
+    ofList ([] : List α) cmp =
+      (∅ : ExtTreeSet α cmp) :=
+  rfl
+
+@[simp]
+theorem ofList_singleton [TransCmp cmp] {k : α} :
+    ofList [k] cmp = (∅ : ExtTreeSet α cmp).insert k :=
+  rfl
+
+@[grind _=_]
+theorem ofList_cons [TransCmp cmp] {hd : α} {tl : List α} :
+    ofList (hd :: tl) cmp =
+      insertMany ((∅ : ExtTreeSet α cmp).insert hd) tl :=
+  ext ExtTreeMap.unitOfList_cons
+
+theorem ofList_eq_insertMany_empty [TransCmp cmp] {l : List α} :
+    ofList l cmp = insertMany (∅ : ExtTreeSet α cmp) l :=
+  match l with
+  | [] => by simp
+  | hd :: tl => by simp [ofList_cons, insertMany_cons]
+
+@[simp, grind =]
+theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
+    (ofList l cmp).contains k = l.contains k :=
+  ExtTreeMap.contains_unitOfList
+
+@[simp, grind =]
+theorem mem_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
+    k ∈ ofList l cmp ↔ l.contains k := by
+  simp [mem_iff_contains]
+
+theorem get?_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
+    {l : List α} {k : α}
+    (contains_eq_false : l.contains k = false) :
+    get? (ofList l cmp) k = none :=
+  ExtTreeMap.getKey?_unitOfList_of_contains_eq_false contains_eq_false
+
+theorem get?_ofList_of_mem [TransCmp cmp]
+    {l : List α} {k k' : α} (k_eq : cmp k k' = .eq)
+    (distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) (mem : k ∈ l) :
+    get? (ofList l cmp) k' = some k :=
+  ExtTreeMap.getKey?_unitOfList_of_mem k_eq distinct mem
+
+theorem get_ofList_of_mem [TransCmp cmp]
+    {l : List α}
+    {k k' : α} (k_eq : cmp k k' = .eq)
+    (distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq))
+    (mem : k ∈ l) {h'} :
+    get (ofList l cmp) k' h' = k :=
+  ExtTreeMap.getKey_unitOfList_of_mem k_eq distinct mem
+
+theorem get!_ofList_of_contains_eq_false [TransCmp cmp] [BEq α]
+    [LawfulBEqCmp cmp] [Inhabited α] {l : List α} {k : α}
+    (contains_eq_false : l.contains k = false) :
+    get! (ofList l cmp) k = default :=
+  ExtTreeMap.getKey!_unitOfList_of_contains_eq_false contains_eq_false
+
+theorem get!_ofList_of_mem [TransCmp cmp]
+    [Inhabited α] {l : List α} {k k' : α} (k_eq : cmp k k' = .eq)
+    (distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq))
+    (mem : k ∈ l) :
+    get! (ofList l cmp) k' = k :=
+  ExtTreeMap.getKey!_unitOfList_of_mem k_eq distinct mem
+
+theorem getD_ofList_of_contains_eq_false [TransCmp cmp] [BEq α]
+    [LawfulBEqCmp cmp] {l : List α} {k fallback : α}
+    (contains_eq_false : l.contains k = false) :
+    getD (ofList l cmp) k fallback = fallback :=
+  ExtTreeMap.getKeyD_unitOfList_of_contains_eq_false contains_eq_false
+
+theorem getD_ofList_of_mem [TransCmp cmp]
+    {l : List α} {k k' fallback : α} (k_eq : cmp k k' = .eq)
+    (distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq))
+    (mem : k ∈ l) :
+    getD (ofList l cmp) k' fallback = k :=
+  ExtTreeMap.getKeyD_unitOfList_of_mem k_eq distinct mem
+
+theorem size_ofList [TransCmp cmp] {l : List α}
+    (distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) :
+    (ofList l cmp).size = l.length :=
+  ExtTreeMap.size_unitOfList distinct
+
+theorem size_ofList_le [TransCmp cmp] {l : List α} :
+    (ofList l cmp).size ≤ l.length :=
+  ExtTreeMap.size_unitOfList_le
+
+grind_pattern size_ofList_le => (ofList l cmp).size
+
+@[simp]
+theorem ofList_eq_empty_iff [TransCmp cmp] {l : List α} :
+    ofList l cmp = ∅ ↔ l = [] :=
+  ext_iff.trans ExtTreeMap.unitOfList_eq_empty_iff
+
+section Min
+
+@[simp, grind =]
+theorem min?_empty [TransCmp cmp] :
+    (∅ : ExtTreeSet α cmp).min? = none :=
+  ExtTreeMap.minKey?_empty
+
+@[simp, grind =]
+theorem min?_eq_none_iff [TransCmp cmp] :
+    t.min? = none ↔ t = ∅ :=
+  ExtTreeMap.minKey?_eq_none_iff.trans ext_iff.symm
+
+theorem min?_eq_some_iff_get?_eq_self_and_forall [TransCmp cmp] {km} :
+    t.min? = some km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE :=
+  ExtTreeMap.minKey?_eq_some_iff_getKey?_eq_self_and_forall
+
+theorem min?_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] {km} :
+    t.min? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE :=
+  ExtTreeMap.minKey?_eq_some_iff_mem_and_forall
+
+@[simp, grind =]
+theorem isNone_min?_eq_isEmpty [TransCmp cmp] :
+    t.min?.isNone = t.isEmpty :=
+  ExtTreeMap.isNone_minKey?_eq_isEmpty
+
+@[simp, grind =]
+theorem isSome_min?_eq_not_isEmpty [TransCmp cmp] :
+    t.min?.isSome = !t.isEmpty :=
+  ExtTreeMap.isSome_minKey?_eq_not_isEmpty
+
+theorem isSome_min?_iff_ne_empty [TransCmp cmp] :
+    t.min?.isSome ↔ t ≠ ∅ :=
+  ExtTreeMap.isSome_minKey?_iff_ne_empty.trans (not_congr ext_iff).symm
+
+@[grind =] theorem min?_insert [TransCmp cmp] {k} :
+    (t.insert k).min? =
+      some (t.min?.elim k fun k' => if cmp k k' = .lt then k else k') :=
+  ExtTreeMap.minKey?_insertIfNew
+
+theorem isSome_min?_insert [TransCmp cmp] {k} :
+    (t.insert k).min?.isSome :=
+  ExtTreeMap.isSome_minKey?_insertIfNew
+
+theorem min?_insert_le_min? [TransCmp cmp] {k km kmi} :
+    (hkm : t.min? = some km) →
+    (hkmi : (t.insert k |>.min? |>.get isSome_min?_insert) = kmi) →
+    cmp kmi km |>.isLE :=
+  ExtTreeMap.minKey?_insertIfNew_le_minKey?
+
+theorem min?_insert_le_self [TransCmp cmp] {k kmi} :
+    (hkmi : (t.insert k |>.min?.get isSome_min?_insert) = kmi) →
+    cmp kmi k |>.isLE :=
+  ExtTreeMap.minKey?_insertIfNew_le_self
+
+theorem contains_min? [TransCmp cmp] {km} :
+    (hkm : t.min? = some km) → t.contains km :=
+  ExtTreeMap.contains_minKey?
+
+theorem min?_mem [TransCmp cmp] {km} :
+    (hkm : t.min? = some km) → km ∈ t :=
+  ExtTreeMap.minKey?_mem
+
+theorem isSome_min?_of_contains [TransCmp cmp] {k} :
+    (hc : t.contains k) → t.min?.isSome :=
+  ExtTreeMap.isSome_minKey?_of_contains
+
+theorem isSome_min?_of_mem [TransCmp cmp] {k} :
+    k ∈ t → t.min?.isSome :=
+  ExtTreeMap.isSome_minKey?_of_mem
+
+theorem min?_le_of_contains [TransCmp cmp] {k km} :
+    (hc : t.contains k) → (hkm : (t.min?.get <| isSome_min?_of_contains hc) = km) →
+    cmp km k |>.isLE :=
+  ExtTreeMap.minKey?_le_of_contains
+
+theorem min?_le_of_mem [TransCmp cmp] {k km} :
+    (hc : k ∈ t) → (hkm : (t.min?.get <| isSome_min?_of_mem hc) = km) →
+    cmp km k |>.isLE :=
+  ExtTreeMap.minKey?_le_of_mem
+
+theorem le_min? [TransCmp cmp] {k} :
+    (∀ k', t.min? = some k' → (cmp k k').isLE) ↔ (∀ k', k' ∈ t → (cmp k k').isLE) :=
+  ExtTreeMap.le_minKey?
+
+theorem get?_min? [TransCmp cmp] {km} :
+    (hkm : t.min? = some km) → t.get? km = some km :=
+  ExtTreeMap.getKey?_minKey?
+
+theorem get_min? [TransCmp cmp] {km hc} :
+    (hkm : t.min?.get (isSome_min?_of_contains hc) = km) → t.get km hc = km :=
+  ExtTreeMap.getKey_minKey?
+
+theorem get!_min? [TransCmp cmp] [Inhabited α] {km} :
+    (hkm : t.min? = some km) → t.get! km = km :=
+  ExtTreeMap.getKey!_minKey?
+
+theorem getD_min? [TransCmp cmp] {km fallback} :
+    (hkm : t.min? = some km) → t.getD km fallback = km :=
+  ExtTreeMap.getKeyD_minKey?
+
+@[simp]
+theorem min?_bind_get? [TransCmp cmp] :
+    t.min?.bind t.get? = t.min? :=
+  ExtTreeMap.minKey?_bind_getKey?
+
+theorem min?_erase_eq_iff_not_compare_eq_min? [TransCmp cmp] {k} :
+    (t.erase k |>.min?) = t.min? ↔
+      ∀ {km}, t.min? = some km → ¬ cmp k km = .eq :=
+  ExtTreeMap.minKey?_erase_eq_iff_not_compare_eq_minKey?
+
+theorem min?_erase_eq_of_not_compare_eq_min? [TransCmp cmp] {k} :
+    (hc : ∀ {km}, t.min? = some km → ¬ cmp k km = .eq) →
+    (t.erase k |>.min?) = t.min? :=
+  ExtTreeMap.minKey?_erase_eq_of_not_compare_eq_minKey?
+
+theorem isSome_min?_of_isSome_min?_erase [TransCmp cmp] {k} :
+    (hs : t.erase k |>.min?.isSome) →
+    t.min?.isSome :=
+  ExtTreeMap.isSome_minKey?_of_isSome_minKey?_erase
+
+theorem min?_le_min?_erase [TransCmp cmp] {k km kme} :
+    (hkme : (t.erase k |>.min?) = some kme) →
+    (hkm : (t.min?.get <|
+      isSome_min?_of_isSome_min?_erase <| hkme ▸ Option.isSome_some) = km) →
+    cmp km kme |>.isLE :=
+  ExtTreeMap.minKey?_le_minKey?_erase
+
+@[grind =_] theorem min?_eq_head?_toList [TransCmp cmp] :
+    t.min? = t.toList.head? :=
+  ExtTreeMap.minKey?_eq_head?_keys
+
+theorem min_eq_get_min? [TransCmp cmp] {he} :
+    t.min he = t.min?.get (isSome_min?_iff_ne_empty.mpr he) :=
+  ExtTreeMap.minKey_eq_get_minKey?
+
+theorem min?_eq_some_min [TransCmp cmp] (he) :
+    t.min? = some (t.min he) :=
+  ExtTreeMap.minKey?_eq_some_minKey (mt ext he)
+
+theorem min_eq_iff_get?_eq_self_and_forall [TransCmp cmp] {he km} :
+    t.min he = km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE :=
+  ExtTreeMap.minKey_eq_iff_getKey?_eq_self_and_forall
+
+theorem min_eq_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] {he km} :
+    t.min he = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE :=
+  ExtTreeMap.minKey_eq_iff_mem_and_forall
+
+@[grind =] theorem min_insert [TransCmp cmp] {k} :
+    (t.insert k).min insert_ne_empty =
+      t.min?.elim k fun k' => if cmp k k' = .lt then k else k' :=
+  ExtTreeMap.minKey_insertIfNew
+
+theorem min_insert_le_min [TransCmp cmp] {k he} :
+    cmp (t.insert k |>.min insert_ne_empty)
+      (t.min he) |>.isLE :=
+  ExtTreeMap.minKey_insertIfNew_le_minKey
+
+theorem min_insert_le_self [TransCmp cmp] {k} :
+    cmp (t.insert k |>.min <| insert_ne_empty) k |>.isLE :=
+  ExtTreeMap.minKey_insertIfNew_le_self
+
+@[grind =] theorem contains_min [TransCmp cmp] {he} :
+    t.contains (t.min he) :=
+  ExtTreeMap.contains_minKey
+
+@[grind] theorem min_mem [TransCmp cmp] {he} :
+    t.min he ∈ t :=
+  ExtTreeMap.minKey_mem
+
+theorem min_le_of_contains [TransCmp cmp] {k} (hc : t.contains k) :
+    cmp (t.min (ne_empty_of_mem hc)) k |>.isLE :=
+  ExtTreeMap.minKey_le_of_contains hc
+
+theorem min_le_of_mem [TransCmp cmp] {k} (hc : k ∈ t) :
+    cmp (t.min (ne_empty_of_mem hc)) k |>.isLE :=
+  ExtTreeMap.minKey_le_of_mem hc
+
+theorem le_min [TransCmp cmp] {k he} :
+    (cmp k (t.min he)).isLE ↔ (∀ k', k' ∈ t → (cmp k k').isLE) :=
+  ExtTreeMap.le_minKey
+
+@[simp, grind =]
+theorem get?_min [TransCmp cmp] {he} :
+    t.get? (t.min he) = some (t.min he) :=
+  ExtTreeMap.getKey?_minKey
+
+@[simp, grind =]
+theorem get_min [TransCmp cmp] {he hc} :
+    t.get (t.min he) hc = t.min he :=
+  ExtTreeMap.getKey_minKey
+
+@[simp, grind =]
+theorem get!_min [TransCmp cmp] [Inhabited α] {he} :
+    t.get! (t.min he) = t.min he :=
+  ExtTreeMap.getKey!_minKey
+
+@[simp, grind =]
+theorem getD_min [TransCmp cmp] {he fallback} :
+    t.getD (t.min he) fallback = t.min he :=
+  ExtTreeMap.getKeyD_minKey
+
+@[simp]
+theorem min_erase_eq_iff_not_compare_eq_min [TransCmp cmp] {k he} :
+    (t.erase k |>.min he) =
+        t.min (ne_empty_of_erase_ne_empty he) ↔
+      ¬ cmp k (t.min <| ne_empty_of_erase_ne_empty he) = .eq :=
+  ExtTreeMap.minKey_erase_eq_iff_not_compare_eq_minKey
+
+theorem min_erase_eq_of_not_compare_eq_min [TransCmp cmp] {k he} :
+    (hc : ¬ cmp k (t.min (ne_empty_of_erase_ne_empty he)) = .eq) →
+    (t.erase k |>.min he) =
+      t.min (ne_empty_of_erase_ne_empty he) :=
+  ExtTreeMap.minKey_erase_eq_of_not_compare_eq_minKey
+
+theorem min_le_min_erase [TransCmp cmp] {k he} :
+    cmp (t.min <| ne_empty_of_erase_ne_empty he)
+      (t.erase k |>.min he) |>.isLE :=
+  ExtTreeMap.minKey_le_minKey_erase
+
+theorem min_eq_head_toList [TransCmp cmp] {he} :
+    t.min he = t.toList.head (mt toList_eq_nil_iff.mp he) :=
+  ExtTreeMap.minKey_eq_head_keys
+
+theorem min?_eq_some_min! [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) :
+    t.min? = some t.min! :=
+  ExtTreeMap.minKey?_eq_some_minKey! (mt ext he)
+
+theorem min_eq_min! [TransCmp cmp] [Inhabited α] {he : t ≠ ∅} :
+    t.min he = t.min! :=
+  ExtTreeMap.minKey_eq_minKey!
+
+theorem min!_empty [TransCmp cmp] [Inhabited α] :
+    (∅ : ExtTreeSet α cmp).min! = default :=
+  ExtTreeMap.minKey!_empty
+
+theorem min!_eq_iff_get?_eq_self_and_forall [TransCmp cmp] [Inhabited α]
+    (he : t ≠ ∅) {km} :
+    t.min! = km ↔ t.get? km = some km ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
+  ExtTreeMap.minKey!_eq_iff_getKey?_eq_self_and_forall (mt ext he)
+
+theorem min!_eq_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α]
+    (he : t ≠ ∅) {km} :
+    t.min! = km ↔ km ∈ t ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
+  ExtTreeMap.minKey!_eq_iff_mem_and_forall (mt ext he)
+
+@[grind =] theorem min!_insert [TransCmp cmp] [Inhabited α] {k} :
+    (t.insert k |>.min!) =
+      t.min?.elim k fun k' => if cmp k k' = .lt then k else k' :=
+  ExtTreeMap.minKey!_insertIfNew
+
+theorem min!_insert_le_min! [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {k} :
+    cmp (t.insert k |>.min!) t.min! |>.isLE :=
+  ExtTreeMap.minKey!_insertIfNew_le_minKey! (mt ext he)
+
+theorem min!_insert_le_self [TransCmp cmp] [Inhabited α] {k} :
+    cmp (t.insert k |>.min!) k |>.isLE :=
+  ExtTreeMap.minKey!_insertIfNew_le_self
+
+@[grind =] theorem contains_min! [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) :
+    t.contains t.min! :=
+  ExtTreeMap.contains_minKey! (mt ext he)
+
+@[grind] theorem min!_mem [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) :
+    t.min! ∈ t :=
+  ExtTreeMap.minKey!_mem (mt ext he)
+
+theorem min!_le_of_contains [TransCmp cmp] [Inhabited α] {k} (hc : t.contains k) :
+    cmp t.min! k |>.isLE :=
+  ExtTreeMap.minKey!_le_of_contains hc
+
+theorem min!_le_of_mem [TransCmp cmp] [Inhabited α] {k} (hc : k ∈ t) :
+    cmp t.min! k |>.isLE :=
+  ExtTreeMap.minKey!_le_of_mem hc
+
+theorem le_min! [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {k} :
+    (cmp k t.min!).isLE ↔ (∀ k', k' ∈ t → (cmp k k').isLE) :=
+  ExtTreeMap.le_minKey! (mt ext he)
+
+theorem get?_min! [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) :
+    t.get? t.min! = some t.min! :=
+  ExtTreeMap.getKey?_minKey! (mt ext he)
+
+@[grind =] theorem get_min! [TransCmp cmp] [Inhabited α] {hc} :
+    t.get t.min! hc = t.min! :=
+  ExtTreeMap.getKey_minKey!
+
+@[simp, grind =]
+theorem get_min!_eq_min [TransCmp cmp] [Inhabited α] {hc} :
+    t.get t.min! hc = t.min (ne_empty_of_mem hc) :=
+  ExtTreeMap.getKey_minKey!_eq_minKey
+
+theorem get!_min! [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) :
+    t.get! t.min! = t.min! :=
+  ExtTreeMap.getKey!_minKey! (mt ext he)
+
+theorem getD_min! [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {fallback} :
+    t.getD t.min! fallback = t.min! :=
+  ExtTreeMap.getKeyD_minKey! (mt ext he)
+
+theorem min!_erase_eq_of_not_compare_min!_eq [TransCmp cmp] [Inhabited α] {k}
+    (he : t.erase k ≠ ∅) (heq : ¬ cmp k t.min! = .eq) :
+    (t.erase k |>.min!) = t.min! :=
+  ExtTreeMap.minKey!_erase_eq_of_not_compare_minKey!_eq (mt ext he) heq
+
+theorem min!_le_min!_erase [TransCmp cmp] [Inhabited α] {k}
+    (he : t.erase k ≠ ∅) :
+    cmp t.min! (t.erase k |>.min!) |>.isLE :=
+  ExtTreeMap.minKey!_le_minKey!_erase (mt ext he)
+
+theorem min!_eq_head!_toList [TransCmp cmp] [Inhabited α] :
+    t.min! = t.toList.head! :=
+  ExtTreeMap.minKey!_eq_head!_keys
+
+theorem min?_eq_some_minD [TransCmp cmp] (he : t ≠ ∅) {fallback} :
+    t.min? = some (t.minD fallback) :=
+  ExtTreeMap.minKey?_eq_some_minKeyD (mt ext he)
+
+theorem minD_empty [TransCmp cmp] {fallback} :
+    (∅ : ExtTreeSet α cmp).minD fallback = fallback :=
+  ExtTreeMap.minKeyD_empty
+
+theorem min!_eq_minD_default [TransCmp cmp] [Inhabited α] :
+    t.min! = t.minD default :=
+  ExtTreeMap.minKey!_eq_minKeyD_default
+
+theorem minD_eq_iff_get?_eq_self_and_forall [TransCmp cmp]
+    (he : t ≠ ∅) {km fallback} :
+    t.minD fallback = km ↔ t.get? km = some km ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
+  ExtTreeMap.minKeyD_eq_iff_getKey?_eq_self_and_forall (mt ext he)
+
+theorem minD_eq_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp]
+    (he : t ≠ ∅) {km fallback} :
+    t.minD fallback = km ↔ km ∈ t ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
+  ExtTreeMap.minKeyD_eq_iff_mem_and_forall (mt ext he)
+
+@[grind =] theorem minD_insert [TransCmp cmp] {k fallback} :
+    (t.insert k |>.minD fallback) =
+      t.min?.elim k fun k' => if cmp k k' = .lt then k else k' :=
+  ExtTreeMap.minKeyD_insertIfNew
+
+theorem minD_insert_le_minD [TransCmp cmp]
+    (he : t ≠ ∅) {k fallback} :
+    cmp (t.insert k |>.minD fallback) (t.minD fallback) |>.isLE :=
+  ExtTreeMap.minKeyD_insertIfNew_le_minKeyD (mt ext he)
+
+theorem minD_insert_le_self [TransCmp cmp] {k fallback} :
+    cmp (t.insert k |>.minD fallback) k |>.isLE :=
+  ExtTreeMap.minKeyD_insertIfNew_le_self
+
+@[grind =] theorem contains_minD [TransCmp cmp] (he : t ≠ ∅) {fallback} :
+    t.contains (t.minD fallback) :=
+  ExtTreeMap.contains_minKeyD (mt ext he)
+
+@[grind] theorem minD_mem [TransCmp cmp] (he : t ≠ ∅) {fallback} :
+    t.minD fallback ∈ t :=
+  ExtTreeMap.minKeyD_mem (mt ext he)
+
+theorem minD_le_of_contains [TransCmp cmp] {k} (hc : t.contains k) {fallback} :
+    cmp (t.minD fallback) k |>.isLE :=
+  ExtTreeMap.minKeyD_le_of_contains hc
+
+theorem minD_le_of_mem [TransCmp cmp] {k} (hc : k ∈ t) {fallback} :
+    cmp (t.minD fallback) k |>.isLE :=
+  ExtTreeMap.minKeyD_le_of_mem hc
+
+theorem le_minD [TransCmp cmp] (he : t ≠ ∅) {k fallback} :
+    (cmp k (t.minD fallback)).isLE ↔ (∀ k', k' ∈ t → (cmp k k').isLE) :=
+  ExtTreeMap.le_minKeyD (mt ext he)
+
+theorem get?_minD [TransCmp cmp] (he : t ≠ ∅) {fallback} :
+    t.get? (t.minD fallback) = some (t.minD fallback) :=
+  ExtTreeMap.getKey?_minKeyD (mt ext he)
+
+@[grind =] theorem get_minD [TransCmp cmp] {fallback hc} :
+    t.get (t.minD fallback) hc = t.minD fallback :=
+  ExtTreeMap.getKey_minKeyD
+
+theorem get!_minD [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {fallback} :
+    t.get! (t.minD fallback) = t.minD fallback :=
+  ExtTreeMap.getKey!_minKeyD (mt ext he)
+
+theorem getD_minD [TransCmp cmp] (he : t ≠ ∅) {fallback fallback'} :
+    t.getD (t.minD fallback) fallback' = t.minD fallback :=
+  ExtTreeMap.getKeyD_minKeyD (mt ext he)
+
+theorem minD_erase_eq_of_not_compare_minD_eq [TransCmp cmp] {k fallback}
+    (he : t.erase k ≠ ∅) (heq : ¬ cmp k (t.minD fallback) = .eq) :
+    (t.erase k |>.minD fallback) = t.minD fallback :=
+  ExtTreeMap.minKeyD_erase_eq_of_not_compare_minKeyD_eq (mt ext he) heq
+
+theorem minD_le_minD_erase [TransCmp cmp] {k}
+    (he : t.erase k ≠ ∅) {fallback} :
+    cmp (t.minD fallback) (t.erase k |>.minD fallback) |>.isLE :=
+  ExtTreeMap.minKeyD_le_minKeyD_erase (mt ext he)
+
+theorem minD_eq_headD_toList [TransCmp cmp] {fallback} :
+    t.minD fallback = t.toList.headD fallback :=
+  ExtTreeMap.minKeyD_eq_headD_keys
+
+end Min
+
+section Max
+
+@[simp, grind =]
+theorem max?_empty [TransCmp cmp] :
+    (∅ : ExtTreeSet α cmp).max? = none :=
+  ExtTreeMap.maxKey?_empty
+
+@[simp, grind =]
+theorem max?_eq_none_iff [TransCmp cmp] :
+    t.max? = none ↔ t = ∅ :=
+  ExtTreeMap.maxKey?_eq_none_iff.trans ext_iff.symm
+
+theorem max?_eq_some_iff_get?_eq_self_and_forall [TransCmp cmp] {km} :
+    t.max? = some km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE :=
+  ExtTreeMap.maxKey?_eq_some_iff_getKey?_eq_self_and_forall
+
+theorem max?_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] {km} :
+    t.max? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE :=
+  ExtTreeMap.maxKey?_eq_some_iff_mem_and_forall
+
+@[simp, grind =]
+theorem isNone_max?_eq_isEmpty [TransCmp cmp] :
+    t.max?.isNone = t.isEmpty :=
+  ExtTreeMap.isNone_maxKey?_eq_isEmpty
+
+@[simp, grind =]
+theorem isSome_max?_eq_not_isEmpty [TransCmp cmp] :
+    t.max?.isSome = !t.isEmpty :=
+  ExtTreeMap.isSome_maxKey?_eq_not_isEmpty
+
+theorem isSome_max?_iff_ne_empty [TransCmp cmp] :
+    t.max?.isSome ↔ t ≠ ∅ :=
+  ExtTreeMap.isSome_maxKey?_iff_ne_empty.trans (not_congr ext_iff).symm
+
+@[grind =] theorem max?_insert [TransCmp cmp] {k} :
+    (t.insert k).max? =
+      some (t.max?.elim k fun k' => if cmp k' k = .lt then k else k') :=
+  ExtTreeMap.maxKey?_insertIfNew
+
+theorem isSome_max?_insert [TransCmp cmp] {k} :
+    (t.insert k).max?.isSome :=
+  ExtTreeMap.isSome_maxKey?_insertIfNew
+
+theorem max?_le_max?_insert [TransCmp cmp] {k km kmi} :
+    (hkm : t.max? = some km) →
+    (hkmi : (t.insert k |>.max? |>.get isSome_max?_insert) = kmi) →
+    cmp km kmi |>.isLE :=
+  ExtTreeMap.maxKey?_le_maxKey?_insertIfNew
+
+theorem self_le_max?_insert [TransCmp cmp] {k kmi} :
+    (hkmi : (t.insert k |>.max?.get isSome_max?_insert) = kmi) →
+    cmp k kmi |>.isLE :=
+  ExtTreeMap.self_le_maxKey?_insertIfNew
+
+theorem contains_max? [TransCmp cmp] {km} :
+    (hkm : t.max? = some km) → t.contains km :=
+  ExtTreeMap.contains_maxKey?
+
+theorem max?_mem [TransCmp cmp] {km} :
+    (hkm : t.max? = some km) → km ∈ t :=
+  ExtTreeMap.maxKey?_mem
+
+theorem isSome_max?_of_contains [TransCmp cmp] {k} :
+    (hc : t.contains k) → t.max?.isSome :=
+  ExtTreeMap.isSome_maxKey?_of_contains
+
+theorem isSome_max?_of_mem [TransCmp cmp] {k} :
+    k ∈ t → t.max?.isSome :=
+  ExtTreeMap.isSome_maxKey?_of_mem
+
+theorem le_max?_of_contains [TransCmp cmp] {k km} :
+    (hc : t.contains k) → (hkm : (t.max?.get <| isSome_max?_of_contains hc) = km) →
+    cmp k km |>.isLE :=
+  ExtTreeMap.le_maxKey?_of_contains
+
+theorem le_max?_of_mem [TransCmp cmp] {k km} :
+    (hc : k ∈ t) → (hkm : (t.max?.get <| isSome_max?_of_mem hc) = km) →
+    cmp k km |>.isLE :=
+  ExtTreeMap.le_maxKey?_of_mem
+
+theorem max?_le [TransCmp cmp] {k} :
+    (∀ k', t.max? = some k' → (cmp k' k).isLE) ↔ (∀ k', k' ∈ t → (cmp k' k).isLE) :=
+  ExtTreeMap.maxKey?_le
+
+theorem get?_max? [TransCmp cmp] {km} :
+    (hkm : t.max? = some km) → t.get? km = some km :=
+  ExtTreeMap.getKey?_maxKey?
+
+theorem get_max? [TransCmp cmp] {km hc} :
+    (hkm : t.max?.get (isSome_max?_of_contains hc) = km) → t.get km hc = km :=
+  ExtTreeMap.getKey_maxKey?
+
+theorem get!_max? [TransCmp cmp] [Inhabited α] {km} :
+    (hkm : t.max? = some km) → t.get! km = km :=
+  ExtTreeMap.getKey!_maxKey?
+
+theorem getD_max? [TransCmp cmp] {km fallback} :
+    (hkm : t.max? = some km) → t.getD km fallback = km :=
+  ExtTreeMap.getKeyD_maxKey?
+
+@[simp]
+theorem max?_bind_get? [TransCmp cmp] :
+    t.max?.bind t.get? = t.max? :=
+  ExtTreeMap.maxKey?_bind_getKey?
+
+theorem max?_erase_eq_iff_not_compare_eq_max? [TransCmp cmp] {k} :
+    (t.erase k |>.max?) = t.max? ↔
+      ∀ {km}, t.max? = some km → ¬ cmp k km = .eq :=
+  ExtTreeMap.maxKey?_erase_eq_iff_not_compare_eq_maxKey?
+
+theorem max?_erase_eq_of_not_compare_eq_max? [TransCmp cmp] {k} :
+    (hc : ∀ {km}, t.max? = some km → ¬ cmp k km = .eq) →
+    (t.erase k |>.max?) = t.max? :=
+  ExtTreeMap.maxKey?_erase_eq_of_not_compare_eq_maxKey?
+
+theorem isSome_max?_of_isSome_max?_erase [TransCmp cmp] {k} :
+    (hs : t.erase k |>.max?.isSome) →
+    t.max?.isSome :=
+  ExtTreeMap.isSome_maxKey?_of_isSome_maxKey?_erase
+
+theorem max?_erase_le_max? [TransCmp cmp] {k km kme} :
+    (hkme : (t.erase k |>.max?) = some kme) →
+    (hkm : (t.max?.get <|
+      isSome_max?_of_isSome_max?_erase <| hkme ▸ Option.isSome_some) = km) →
+    cmp kme km |>.isLE :=
+  ExtTreeMap.maxKey?_erase_le_maxKey?
+
+theorem max?_eq_getLast?_toList [TransCmp cmp] :
+    t.max? = t.toList.getLast? :=
+  ExtTreeMap.maxKey?_eq_getLast?_keys
+
+theorem max_eq_get_max? [TransCmp cmp] {he} :
+    t.max he = t.max?.get (isSome_max?_iff_ne_empty.mpr he) :=
+  ExtTreeMap.maxKey_eq_get_maxKey?
+
+theorem max?_eq_some_max [TransCmp cmp] (he) :
+    t.max? = some (t.max he) :=
+  ExtTreeMap.maxKey?_eq_some_maxKey (mt ext he)
+
+theorem max_eq_iff_get?_eq_self_and_forall [TransCmp cmp] {he km} :
+    t.max he = km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE :=
+  ExtTreeMap.maxKey_eq_iff_getKey?_eq_self_and_forall
+
+theorem max_eq_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] {he km} :
+    t.max he = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE :=
+  ExtTreeMap.maxKey_eq_iff_mem_and_forall
+
+@[grind =] theorem max_insert [TransCmp cmp] {k} :
+    (t.insert k).max insert_ne_empty =
+      t.max?.elim k fun k' => if cmp k' k = .lt then k else k' :=
+  ExtTreeMap.maxKey_insertIfNew
+
+theorem max_le_max_insert [TransCmp cmp] {k he} :
+    cmp (t.max he)
+      (t.insert k |>.max insert_ne_empty) |>.isLE :=
+  ExtTreeMap.maxKey_le_maxKey_insertIfNew
+
+theorem self_le_max_insert [TransCmp cmp] {k} :
+    cmp k (t.insert k |>.max <| insert_ne_empty) |>.isLE :=
+  ExtTreeMap.self_le_maxKey_insertIfNew
+
+@[grind =] theorem contains_max [TransCmp cmp] {he} :
+    t.contains (t.max he) :=
+  ExtTreeMap.contains_maxKey
+
+@[grind] theorem max_mem [TransCmp cmp] {he} :
+    t.max he ∈ t :=
+  ExtTreeMap.maxKey_mem
+
+theorem le_max_of_contains [TransCmp cmp] {k} (hc : t.contains k) :
+    cmp k (t.max (ne_empty_of_mem hc)) |>.isLE :=
+  ExtTreeMap.le_maxKey_of_contains hc
+
+theorem le_max_of_mem [TransCmp cmp] {k} (hc : k ∈ t) :
+    cmp k (t.max (ne_empty_of_mem hc)) |>.isLE :=
+  ExtTreeMap.le_maxKey_of_mem hc
+
+theorem max_le [TransCmp cmp] {k he} :
+    (cmp (t.max he) k).isLE ↔ (∀ k', k' ∈ t → (cmp k' k).isLE) :=
+  ExtTreeMap.maxKey_le
+
+@[simp, grind =]
+theorem get?_max [TransCmp cmp] {he} :
+    t.get? (t.max he) = some (t.max he) :=
+  ExtTreeMap.getKey?_maxKey
+
+@[simp, grind =]
+theorem get_max [TransCmp cmp] {he hc} :
+    t.get (t.max he) hc = t.max he :=
+  ExtTreeMap.getKey_maxKey
+
+@[simp, grind =]
+theorem get!_max [TransCmp cmp] [Inhabited α] {he} :
+    t.get! (t.max he) = t.max he :=
+  ExtTreeMap.getKey!_maxKey
+
+@[simp, grind =]
+theorem getD_max [TransCmp cmp] {he fallback} :
+    t.getD (t.max he) fallback = t.max he :=
+  ExtTreeMap.getKeyD_maxKey
+
+@[simp]
+theorem max_erase_eq_iff_not_compare_eq_max [TransCmp cmp] {k he} :
+    (t.erase k |>.max he) =
+        t.max (ne_empty_of_erase_ne_empty he) ↔
+      ¬ cmp k (t.max <| ne_empty_of_erase_ne_empty he) = .eq :=
+  ExtTreeMap.maxKey_erase_eq_iff_not_compare_eq_maxKey
+
+theorem max_erase_eq_of_not_compare_eq_max [TransCmp cmp] {k he} :
+    (hc : ¬ cmp k (t.max (ne_empty_of_erase_ne_empty he)) = .eq) →
+    (t.erase k |>.max he) =
+      t.max (ne_empty_of_erase_ne_empty he) :=
+  ExtTreeMap.maxKey_erase_eq_of_not_compare_eq_maxKey
+
+theorem max_erase_le_max [TransCmp cmp] {k he} :
+    cmp (t.erase k |>.max he)
+      (t.max <| ne_empty_of_erase_ne_empty he) |>.isLE :=
+  ExtTreeMap.maxKey_erase_le_maxKey
+
+@[grind =_]
+theorem max_eq_getLast_toList [TransCmp cmp] {he} :
+    t.max he = t.toList.getLast (mt toList_eq_nil_iff.mp he) :=
+  ExtTreeMap.maxKey_eq_getLast_keys
+
+theorem max?_eq_some_max! [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) :
+    t.max? = some t.max! :=
+  ExtTreeMap.maxKey?_eq_some_maxKey! (mt ext he)
+
+theorem max_eq_max! [TransCmp cmp] [Inhabited α] {he : t ≠ ∅} :
+    t.max he = t.max! :=
+  ExtTreeMap.maxKey_eq_maxKey!
+
+theorem max!_empty [TransCmp cmp] [Inhabited α] :
+    (∅ : ExtTreeSet α cmp).max! = default :=
+  ExtTreeMap.maxKey!_empty
+
+theorem max!_eq_iff_get?_eq_self_and_forall [TransCmp cmp] [Inhabited α]
+    (he : t ≠ ∅) {km} :
+    t.max! = km ↔ t.get? km = some km ∧ ∀ k, k ∈ t → (cmp k km).isLE :=
+  ExtTreeMap.maxKey!_eq_iff_getKey?_eq_self_and_forall (mt ext he)
+
+theorem max!_eq_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α]
+    (he : t ≠ ∅) {km} :
+    t.max! = km ↔ km ∈ t ∧ ∀ k, k ∈ t → (cmp k km).isLE :=
+  ExtTreeMap.maxKey!_eq_iff_mem_and_forall (mt ext he)
+
+@[grind =] theorem max!_insert [TransCmp cmp] [Inhabited α] {k} :
+    (t.insert k |>.max!) =
+      t.max?.elim k fun k' => if cmp k' k = .lt then k else k' :=
+  ExtTreeMap.maxKey!_insertIfNew
+
+theorem max!_le_max!_insert [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {k} :
+    cmp t.max! (t.insert k |>.max!) |>.isLE :=
+  ExtTreeMap.maxKey!_le_maxKey!_insertIfNew (mt ext he)
+
+theorem self_le_max!_insert [TransCmp cmp] [Inhabited α] {k} :
+    cmp k (t.insert k |>.max!) |>.isLE :=
+  ExtTreeMap.self_le_maxKey!_insertIfNew
+
+@[grind =] theorem contains_max! [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) :
+    t.contains t.max! :=
+  ExtTreeMap.contains_maxKey! (mt ext he)
+
+@[grind] theorem max!_mem [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) :
+    t.max! ∈ t :=
+  ExtTreeMap.maxKey!_mem (mt ext he)
+
+theorem le_max!_of_contains [TransCmp cmp] [Inhabited α] {k} (hc : t.contains k) :
+    cmp k t.max! |>.isLE :=
+  ExtTreeMap.le_maxKey!_of_contains hc
+
+theorem le_max!_of_mem [TransCmp cmp] [Inhabited α] {k} (hc : k ∈ t) :
+    cmp k t.max! |>.isLE :=
+  ExtTreeMap.le_maxKey!_of_mem hc
+
+theorem max!_le [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {k} :
+    (cmp t.max! k).isLE ↔ (∀ k', k' ∈ t → (cmp k' k).isLE) :=
+  ExtTreeMap.maxKey!_le (mt ext he)
+
+theorem get?_max! [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) :
+    t.get? t.max! = some t.max! :=
+  ExtTreeMap.getKey?_maxKey! (mt ext he)
+
+@[grind =] theorem get_max! [TransCmp cmp] [Inhabited α] {hc} :
+    t.get t.max! hc = t.max! :=
+  ExtTreeMap.getKey_maxKey!
+
+@[simp, grind =]
+theorem get_max!_eq_max [TransCmp cmp] [Inhabited α] {hc} :
+    t.get t.max! hc = t.max (ne_empty_of_mem hc) :=
+  ExtTreeMap.getKey_maxKey!_eq_maxKey
+
+theorem get!_max! [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) :
+    t.get! t.max! = t.max! :=
+  ExtTreeMap.getKey!_maxKey! (mt ext he)
+
+theorem getD_max! [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {fallback} :
+    t.getD t.max! fallback = t.max! :=
+  ExtTreeMap.getKeyD_maxKey! (mt ext he)
+
+theorem max!_erase_eq_of_not_compare_max!_eq [TransCmp cmp] [Inhabited α] {k}
+    (he : t.erase k ≠ ∅) (heq : ¬ cmp k t.max! = .eq) :
+    (t.erase k |>.max!) = t.max! :=
+  ExtTreeMap.maxKey!_erase_eq_of_not_compare_maxKey!_eq (mt ext he) heq
+
+theorem max!_erase_le_max! [TransCmp cmp] [Inhabited α] {k}
+    (he : t.erase k ≠ ∅) :
+    cmp (t.erase k |>.max!) t.max! |>.isLE :=
+  ExtTreeMap.maxKey!_erase_le_maxKey! (mt ext he)
+
+@[grind =_]
+theorem max!_eq_getLast!_toList [TransCmp cmp] [Inhabited α] :
+    t.max! = t.toList.getLast! :=
+  ExtTreeMap.maxKey!_eq_getLast!_keys
+
+theorem max?_eq_some_maxD [TransCmp cmp] (he : t ≠ ∅) {fallback} :
+    t.max? = some (t.maxD fallback) :=
+  ExtTreeMap.maxKey?_eq_some_maxKeyD (mt ext he)
+
+theorem maxD_empty [TransCmp cmp] {fallback} :
+    (∅ : ExtTreeSet α cmp).maxD fallback = fallback :=
+  ExtTreeMap.maxKeyD_empty
+
+theorem max!_eq_maxD_default [TransCmp cmp] [Inhabited α] :
+    t.max! = t.maxD default :=
+  ExtTreeMap.maxKey!_eq_maxKeyD_default
+
+theorem maxD_eq_iff_get?_eq_self_and_forall [TransCmp cmp]
+    (he : t ≠ ∅) {km fallback} :
+    t.maxD fallback = km ↔ t.get? km = some km ∧ ∀ k, k ∈ t → (cmp k km).isLE :=
+  ExtTreeMap.maxKeyD_eq_iff_getKey?_eq_self_and_forall (mt ext he)
+
+theorem maxD_eq_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp]
+    (he : t ≠ ∅) {km fallback} :
+    t.maxD fallback = km ↔ km ∈ t ∧ ∀ k, k ∈ t → (cmp k km).isLE :=
+  ExtTreeMap.maxKeyD_eq_iff_mem_and_forall (mt ext he)
+
+@[grind =] theorem maxD_insert [TransCmp cmp] {k fallback} :
+    (t.insert k |>.maxD fallback) =
+      t.max?.elim k fun k' => if cmp k' k = .lt then k else k' :=
+  ExtTreeMap.maxKeyD_insertIfNew
+
+theorem maxD_le_maxD_insert [TransCmp cmp]
+    (he : t ≠ ∅) {k fallback} :
+    cmp (t.maxD fallback) (t.insert k |>.maxD fallback) |>.isLE :=
+  ExtTreeMap.maxKeyD_le_maxKeyD_insertIfNew (mt ext he)
+
+theorem self_le_maxD_insert [TransCmp cmp] {k fallback} :
+    cmp k (t.insert k |>.maxD fallback) |>.isLE :=
+  ExtTreeMap.self_le_maxKeyD_insertIfNew
+
+@[grind =] theorem contains_maxD [TransCmp cmp] (he : t ≠ ∅) {fallback} :
+    t.contains (t.maxD fallback) :=
+  ExtTreeMap.contains_maxKeyD (mt ext he)
+
+@[grind] theorem maxD_mem [TransCmp cmp] (he : t ≠ ∅) {fallback} :
+    t.maxD fallback ∈ t :=
+  ExtTreeMap.maxKeyD_mem (mt ext he)
+
+theorem le_maxD_of_contains [TransCmp cmp] {k} (hc : t.contains k) {fallback} :
+    cmp k (t.maxD fallback) |>.isLE :=
+  ExtTreeMap.le_maxKeyD_of_contains hc
+
+theorem le_maxD_of_mem [TransCmp cmp] {k} (hc : k ∈ t) {fallback} :
+    cmp k (t.maxD fallback) |>.isLE :=
+  ExtTreeMap.le_maxKeyD_of_mem hc
+
+theorem maxD_le [TransCmp cmp] (he : t ≠ ∅) {k fallback} :
+    (cmp (t.maxD fallback) k).isLE ↔ (∀ k', k' ∈ t → (cmp k' k).isLE) :=
+  ExtTreeMap.maxKeyD_le (mt ext he)
+
+theorem get?_maxD [TransCmp cmp] (he : t ≠ ∅) {fallback} :
+    t.get? (t.maxD fallback) = some (t.maxD fallback) :=
+  ExtTreeMap.getKey?_maxKeyD (mt ext he)
+
+@[grind =] theorem get_maxD [TransCmp cmp] {fallback hc} :
+    t.get (t.maxD fallback) hc = t.maxD fallback :=
+  ExtTreeMap.getKey_maxKeyD
+
+theorem get!_maxD [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {fallback} :
+    t.get! (t.maxD fallback) = t.maxD fallback :=
+  ExtTreeMap.getKey!_maxKeyD (mt ext he)
+
+theorem getD_maxD [TransCmp cmp] (he : t ≠ ∅) {fallback fallback'} :
+    t.getD (t.maxD fallback) fallback' = t.maxD fallback :=
+  ExtTreeMap.getKeyD_maxKeyD (mt ext he)
+
+theorem maxD_erase_eq_of_not_compare_maxD_eq [TransCmp cmp] {k fallback}
+    (he : t.erase k ≠ ∅) (heq : ¬ cmp k (t.maxD fallback) = .eq) :
+    (t.erase k |>.maxD fallback) = t.maxD fallback :=
+  ExtTreeMap.maxKeyD_erase_eq_of_not_compare_maxKeyD_eq (mt ext he) heq
+
+theorem maxD_erase_le_maxD [TransCmp cmp] {k}
+    (he : t.erase k ≠ ∅) {fallback} :
+    cmp (t.erase k |>.maxD fallback) (t.maxD fallback) |>.isLE :=
+  ExtTreeMap.maxKeyD_erase_le_maxKeyD (mt ext he)
+
+theorem maxD_eq_getLastD_toList [TransCmp cmp] {fallback} :
+    t.maxD fallback = t.toList.getLastD fallback :=
+  ExtTreeMap.maxKeyD_eq_getLastD_keys
+
+end Max
+
+section Ext
+
+variable {t₁ t₂ : ExtTreeSet α cmp}
+
+@[ext 900]
+theorem ext_get? [TransCmp cmp] {t₁ t₂ : ExtTreeSet α cmp}
+    (h : ∀ k, t₁.get? k = t₂.get? k) : t₁ = t₂ :=
+  ext (ExtTreeMap.ext_getKey?_unit h)
+
+theorem ext_contains [TransCmp cmp] [LawfulEqCmp cmp]
+    {t₁ t₂ : ExtTreeSet α cmp}
+    (h : ∀ k, t₁.contains k = t₂.contains k) : t₁ = t₂ :=
+  ext (ExtTreeMap.ext_contains_unit h)
+
+@[ext]
+theorem ext_mem [TransCmp cmp] [LawfulEqCmp cmp]
+    {t₁ t₂ : ExtTreeSet α cmp}
+    (h : ∀ k, k ∈ t₁ ↔ k ∈ t₂) : t₁ = t₂ :=
+  ext (ExtTreeMap.ext_mem_unit h)
+
+theorem ext_toList [TransCmp cmp] (h : t₁.toList.Perm t₂.toList) : t₁ = t₂ :=
+  ext (ExtTreeMap.ext_keys_unit h)
+
+theorem toList_inj [TransCmp cmp] : t₁.toList = t₂.toList ↔ t₁ = t₂ :=
+  ⟨ext_toList ∘ .of_eq, fun h => h ▸ rfl⟩
+
+end Ext
+
+end Std.ExtTreeSet

backend/core/leanprover--lean4---v4.22.0/src/lean/Std/Data/HashMap/AdditionalOperations.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+prelude
+import Std.Data.DHashMap.AdditionalOperations
+import Std.Data.HashMap.Basic
+import Std.Data.HashMap.Raw
+
+/-!
+# Additional hash map operations
+
+This module defines the operations `map` and `filterMap` on `Std.HashMap`.
+Lemmas about these operations are found in `Std.Data.HashMap.Lemmas`.
+-/
+
+set_option linter.missingDocs true
+set_option autoImplicit false
+
+universe u v w
+
+variable {α : Type u} {β : Type v} {γ : Type w}
+
+namespace Std
+
+namespace HashMap
+
+namespace Raw
+
+theorem WF.filterMap [BEq α] [Hashable α] {m : Raw α β} {f : α → β → Option γ} (h : m.WF) :
+    (m.filterMap f).WF :=
+  ⟨DHashMap.Raw.WF.filterMap h.out⟩
+
+theorem WF.map [BEq α] [Hashable α] {m : Raw α β} {f : α → β → γ} (h : m.WF) : (m.map f).WF :=
+  ⟨DHashMap.Raw.WF.map h.out⟩
+
+end Raw
+
+@[inline, inherit_doc DHashMap.filterMap] def filterMap [BEq α] [Hashable α] (f : α → β → Option γ)
+    (m : HashMap α β) : HashMap α γ :=
+  ⟨m.inner.filterMap f⟩
+
+@[inline, inherit_doc DHashMap.map] def map [BEq α] [Hashable α] (f : α → β → γ) (m : HashMap α β) :
+    HashMap α γ :=
+  ⟨m.inner.map f⟩
+
+end HashMap
+
+end Std

backend/core/leanprover--lean4---v4.22.0/src/lean/Std/Data/HashMap/Basic.lean

@@ -0,0 +1,325 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+prelude
+import Std.Data.DHashMap.Basic
+
+set_option linter.missingDocs true
+set_option autoImplicit false
+
+/-!
+# Hash maps
+
+This module develops the type `Std.HashMap` of hash maps. Dependent hash maps are defined in
+`Std.Data.DHashMap`.
+
+The operations `map` and `filterMap` on `Std.HashMap` are defined in the module
+`Std.Data.HashMap.AdditionalOperations`.
+
+Lemmas about the operations on `Std.HashMap` are available in the
+module `Std.Data.HashMap.Lemmas`.
+
+See the module `Std.Data.HashMap.Raw` for a variant of this type which is safe to use in
+nested inductive types.
+-/
+
+universe u v w
+
+variable {α : Type u} {β : Type v} {_ : BEq α} {_ : Hashable α}
+
+namespace Std
+
+/--
+Hash maps.
+
+This is a simple separate-chaining hash table. The data of the hash map consists of a cached size
+and an array of buckets, where each bucket is a linked list of key-value pais. The number of buckets
+is always a power of two. The hash map doubles its size upon inserting an element such that the
+number of elements is more than 75% of the number of buckets.
+
+The hash table is backed by an `Array`. Users should make sure that the hash map is used linearly to
+avoid expensive copies.
+
+The hash map uses `==` (provided by the `BEq` typeclass) to compare keys and `hash` (provided by
+the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
+should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the
+`EquivBEq` and `LawfulHashable` typeclasses). Both of these conditions are automatic if the BEq
+instance is lawful, i.e., if `a == b` implies `a = b`.
+
+These hash maps contain a bundled well-formedness invariant, which means that they cannot
+be used in nested inductive types. For these use cases, `Std.Data.HashMap.Raw` and
+`Std.Data.HashMap.Raw.WF` unbundle the invariant from the hash map. When in doubt, prefer
+`HashMap` over `HashMap.Raw`.
+
+Dependent hash maps, in which keys may occur in their values' types, are available as
+`Std.Data.DHashMap`.
+-/
+structure HashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where
+  /-- Internal implementation detail of the hash map -/
+  inner : DHashMap α (fun _ => β)
+
+namespace HashMap
+
+@[inline, inherit_doc DHashMap.empty] def emptyWithCapacity [BEq α] [Hashable α] (capacity := 8) :
+    HashMap α β :=
+  ⟨DHashMap.emptyWithCapacity capacity⟩
+
+@[deprecated emptyWithCapacity (since := "2025-03-12"), inherit_doc emptyWithCapacity]
+abbrev empty := @emptyWithCapacity
+
+instance [BEq α] [Hashable α] : EmptyCollection (HashMap α β) where
+  emptyCollection := emptyWithCapacity
+
+instance [BEq α] [Hashable α] : Inhabited (HashMap α β) where
+  default := ∅
+
+@[inherit_doc DHashMap.Equiv]
+structure Equiv (m₁ m₂ : HashMap α β) where
+  /-- Internal implementation detail of the hash map -/
+  inner : m₁.1.Equiv m₂.1
+
+@[inherit_doc] scoped infixl:50 " ~m " => Equiv
+
+@[inline, inherit_doc DHashMap.insert] def insert (m : HashMap α β) (a : α)
+    (b : β) : HashMap α β :=
+  ⟨m.inner.insert a b⟩
+
+instance : Singleton (α × β) (HashMap α β) := ⟨fun ⟨a, b⟩ => (∅ : HashMap α β).insert a b⟩
+
+instance : Insert (α × β) (HashMap α β) := ⟨fun ⟨a, b⟩ s => s.insert a b⟩
+
+instance : LawfulSingleton (α × β) (HashMap α β) := ⟨fun _ => rfl⟩
+
+@[inline, inherit_doc DHashMap.insertIfNew] def insertIfNew (m : HashMap α β)
+    (a : α) (b : β) : HashMap α β :=
+  ⟨m.inner.insertIfNew a b⟩
+
+@[inline, inherit_doc DHashMap.containsThenInsert] def containsThenInsert
+    (m : HashMap α β) (a : α) (b : β) : Bool × HashMap α β :=
+  let ⟨replaced, r⟩ := m.inner.containsThenInsert a b
+  ⟨replaced, ⟨r⟩⟩
+
+@[inline, inherit_doc DHashMap.containsThenInsertIfNew] def containsThenInsertIfNew
+    (m : HashMap α β) (a : α) (b : β) : Bool × HashMap α β :=
+  let ⟨replaced, r⟩ := m.inner.containsThenInsertIfNew a b
+  ⟨replaced, ⟨r⟩⟩
+
+/--
+Checks whether a key is present in a map, returning the associate value, and inserts a value for
+the key if it was not found.
+
+If the returned value is `some v`, then the returned map is unaltered. If it is `none`, then the
+returned map has a new value inserted.
+
+Equivalent to (but potentially faster than) calling `get?` followed by `insertIfNew`.
+-/
+@[inline] def getThenInsertIfNew? (m : HashMap α β) (a : α) (b : β) :
+    Option β × HashMap α β :=
+  let ⟨previous, r⟩ := DHashMap.Const.getThenInsertIfNew? m.inner a b
+  ⟨previous, ⟨r⟩⟩
+
+/--
+The notation `m[a]?` is preferred over calling this function directly.
+
+Tries to retrieve the mapping for the given key, returning `none` if no such mapping is present.
+-/
+@[inline] def get? (m : HashMap α β) (a : α) : Option β :=
+  DHashMap.Const.get? m.inner a
+
+@[inline, inherit_doc DHashMap.contains] def contains (m : HashMap α β)
+    (a : α) : Bool :=
+  m.inner.contains a
+
+instance [BEq α] [Hashable α] : Membership α (HashMap α β) where
+  mem m a := a ∈ m.inner
+
+instance [BEq α] [Hashable α] {m : HashMap α β} {a : α} : Decidable (a ∈ m) :=
+  inferInstanceAs (Decidable (a ∈ m.inner))
+
+/--
+The notation `m[a]` or `m[a]'h` is preferred over calling this function directly.
+
+Retrieves the mapping for the given key. Ensures that such a mapping exists by requiring a proof of
+`a ∈ m`.
+-/
+@[inline] def get (m : HashMap α β) (a : α) (h : a ∈ m) : β :=
+  DHashMap.Const.get m.inner a h
+
+@[inline, inherit_doc DHashMap.Const.getD] def getD (m : HashMap α β) (a : α)
+    (fallback : β) : β :=
+  DHashMap.Const.getD m.inner a fallback
+
+/--
+The notation `m[a]!` is preferred over calling this function directly.
+
+Tries to retrieve the mapping for the given key, panicking if no such mapping is present.
+-/
+@[inline] def get! [Inhabited β] (m : HashMap α β) (a : α) : β :=
+  DHashMap.Const.get! m.inner a
+
+instance [BEq α] [Hashable α] : GetElem? (HashMap α β) α β (fun m a => a ∈ m) where
+  getElem m a h := m.get a h
+  getElem? m a := m.get? a
+  getElem! m a := m.get! a
+
+@[inline, inherit_doc DHashMap.getKey?] def getKey? (m : HashMap α β) (a : α) : Option α :=
+  DHashMap.getKey? m.inner a
+
+@[inline, inherit_doc DHashMap.getKey] def getKey (m : HashMap α β) (a : α) (h : a ∈ m) : α :=
+  DHashMap.getKey m.inner a h
+
+@[inline, inherit_doc DHashMap.getKeyD] def getKeyD (m : HashMap α β) (a : α) (fallback : α) : α :=
+  DHashMap.getKeyD m.inner a fallback
+
+@[inline, inherit_doc DHashMap.getKey!] def getKey! [Inhabited α] (m : HashMap α β) (a : α) : α :=
+  DHashMap.getKey! m.inner a
+
+@[inline, inherit_doc DHashMap.erase] def erase (m : HashMap α β) (a : α) :
+    HashMap α β :=
+  ⟨m.inner.erase a⟩
+
+@[inline, inherit_doc DHashMap.size] def size (m : HashMap α β) : Nat :=
+  m.inner.size
+
+@[inline, inherit_doc DHashMap.isEmpty] def isEmpty (m : HashMap α β) : Bool :=
+  m.inner.isEmpty
+
+@[inline, inherit_doc DHashMap.keys] def keys (m : HashMap α β) : List α :=
+  m.inner.keys
+
+@[inline, inherit_doc DHashMap.Const.ofList] def ofList [BEq α] [Hashable α] (l : List (α × β)) :
+    HashMap α β :=
+  ⟨DHashMap.Const.ofList l⟩
+
+@[inline, inherit_doc DHashMap.Const.unitOfList] def unitOfList [BEq α] [Hashable α] (l : List α) :
+    HashMap α Unit :=
+  ⟨DHashMap.Const.unitOfList l⟩
+
+@[inline, inherit_doc DHashMap.Const.toList] def toList (m : HashMap α β) :
+    List (α × β) :=
+  DHashMap.Const.toList m.inner
+
+@[inline, inherit_doc DHashMap.foldM] def foldM {m : Type w → Type w}
+    [Monad m] {γ : Type w} (f : γ → α → β → m γ) (init : γ) (b : HashMap α β) : m γ :=
+  b.inner.foldM f init
+
+@[inline, inherit_doc DHashMap.fold] def fold {γ : Type w}
+    (f : γ → α → β → γ) (init : γ) (b : HashMap α β) : γ :=
+  b.inner.fold f init
+
+@[inline, inherit_doc DHashMap.forM] def forM {m : Type w → Type w} [Monad m]
+    (f : (a : α) → β → m PUnit) (b : HashMap α β) : m PUnit :=
+  b.inner.forM f
+
+@[inline, inherit_doc DHashMap.forIn] def forIn {m : Type w → Type w} [Monad m]
+    {γ : Type w} (f : (a : α) → β → γ → m (ForInStep γ)) (init : γ) (b : HashMap α β) : m γ :=
+  b.inner.forIn f init
+
+instance [BEq α] [Hashable α] {m : Type w → Type w} : ForM m (HashMap α β) (α × β) where
+  forM m f := m.forM (fun a b => f (a, b))
+
+instance [BEq α] [Hashable α] {m : Type w → Type w} : ForIn m (HashMap α β) (α × β) where
+  forIn m init f := m.forIn (fun a b acc => f (a, b) acc) init
+
+@[inline, inherit_doc DHashMap.filter] def filter (f : α → β → Bool)
+    (m : HashMap α β) : HashMap α β :=
+  ⟨m.inner.filter f⟩
+
+@[inline, inherit_doc DHashMap.modify] def modify (m : HashMap α β) (a : α) (f : β → β) :
+    HashMap α β :=
+  ⟨DHashMap.Const.modify m.inner a f⟩
+
+@[inline, inherit_doc DHashMap.alter] def alter (m : HashMap α β) (a : α)
+    (f : Option β → Option β) : HashMap α β :=
+  ⟨DHashMap.Const.alter m.inner a f⟩
+
+@[inline, inherit_doc DHashMap.Const.insertMany] def insertMany {ρ : Type w}
+    [ForIn Id ρ (α × β)] (m : HashMap α β) (l : ρ) : HashMap α β :=
+  ⟨DHashMap.Const.insertMany m.inner l⟩
+
+@[inline, inherit_doc DHashMap.Const.insertManyIfNewUnit] def insertManyIfNewUnit
+    {ρ : Type w} [ForIn Id ρ α] (m : HashMap α Unit) (l : ρ) : HashMap α Unit :=
+  ⟨DHashMap.Const.insertManyIfNewUnit m.inner l⟩
+
+
+section Unverified
+
+/-! We currently do not provide lemmas for the functions below. -/
+
+@[inline, inherit_doc DHashMap.partition] def partition (f : α → β → Bool)
+    (m : HashMap α β) : HashMap α β × HashMap α β :=
+  let ⟨l, r⟩ := m.inner.partition f
+  ⟨⟨l⟩, ⟨r⟩⟩
+
+@[inline, inherit_doc DHashMap.Const.toArray] def toArray (m : HashMap α β) :
+    Array (α × β) :=
+  DHashMap.Const.toArray m.inner
+
+@[inline, inherit_doc DHashMap.keysArray] def keysArray (m : HashMap α β) :
+    Array α :=
+  m.inner.keysArray
+
+@[inline, inherit_doc DHashMap.values] def values (m : HashMap α β) : List β :=
+  m.inner.values
+
+@[inline, inherit_doc DHashMap.valuesArray] def valuesArray (m : HashMap α β) :
+    Array β :=
+  m.inner.valuesArray
+
+/-- Computes the union of the given hash maps, by traversing `m₂` and inserting its elements into `m₁`. -/
+@[inline] def union [BEq α] [Hashable α] (m₁ m₂ : HashMap α β) : HashMap α β :=
+  m₂.fold (init := m₁) fun acc x => acc.insert x
+
+instance [BEq α] [Hashable α] : Union (HashMap α β) := ⟨union⟩
+
+@[inline, inherit_doc DHashMap.Const.unitOfArray] def unitOfArray [BEq α] [Hashable α] (l : Array α) :
+    HashMap α Unit :=
+  ⟨DHashMap.Const.unitOfArray l⟩
+
+@[inline, inherit_doc DHashMap.Internal.numBuckets] def Internal.numBuckets
+    (m : HashMap α β) : Nat :=
+  DHashMap.Internal.numBuckets m.inner
+
+instance [BEq α] [Hashable α] [Repr α] [Repr β] : Repr (HashMap α β) where
+  reprPrec m prec := Repr.addAppParen ("Std.HashMap.ofList " ++ reprArg m.toList) prec
+
+end Unverified
+
+end Std.HashMap
+
+/--
+Groups the elements of an array `xs` according to the function `key`, returning a hash map in which
+each group is associated with its key. Groups preserve the relative order of elements in `xs`.
+
+Example:
+```lean example
+#eval #[0, 1, 2, 3, 4, 5, 6].groupByKey (· % 2)
+```
+```output
+Std.HashMap.ofList [(0, #[0, 2, 4, 6]), (1, #[1, 3, 5])]
+```
+-/
+def Array.groupByKey [BEq α] [Hashable α] (key : β → α) (xs : Array β)
+    : Std.HashMap α (Array β) := Id.run do
+  let mut groups := ∅
+  for x in xs do
+    groups := groups.alter (key x) (some <| ·.getD #[] |>.push x)
+  return groups
+
+/--
+Groups the elements of a list `xs` according to the function `key`, returning a hash map in which
+each group is associated with its key. Groups preserve the relative order of elements in `xs`.
+
+Example:
+```lean example
+#eval [0, 1, 2, 3, 4, 5, 6].groupByKey (· % 2)
+```
+```output
+Std.HashMap.ofList [(0, [0, 2, 4, 6]), (1, [1, 3, 5])]
+```
+-/
+def List.groupByKey [BEq α] [Hashable α] (key : β → α) (xs : List β) :
+    Std.HashMap α (List β) :=
+  xs.foldr (init := ∅) fun x acc => acc.alter (key x) (fun v => some <| x :: v.getD [])

backend/core/leanprover--lean4---v4.22.0/src/lean/lake/Lake/Util/Store.lean

@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Init.Notation
+
+namespace Lake
+
+/-- A monad equipped with a dependently typed key-value store for a particular key. -/
+class MonadStore1Of {κ : Type u} (k : κ) (α : semiOutParam $ Type v) (m : Type v → Type w) where
+  fetch? : m (Option α)
+  store : α → m PUnit
+
+export MonadStore1Of (store)
+
+/-- Similar to `MonadStore1Of`, but `α` is an `outParam` for convenience. -/
+class MonadStore1 {κ : Type u} (k : κ) (α : outParam $ Type v) (m : Type v → Type w) where
+  fetch? : m (Option α)
+  store : α → m PUnit
+
+export MonadStore1 (fetch?)
+
+instance [MonadStore1Of k α m] : MonadStore1 k α m where
+  fetch? := MonadStore1Of.fetch? k
+  store := MonadStore1Of.store k
+
+/-- A monad equipped with a dependently typed key-object store. -/
+class MonadDStore (κ : Type u) (β : semiOutParam $ κ → Type v) (m : Type v → Type w) where
+  fetch? : (key : κ) → m (Option (β key))
+  store : (key : κ) → β key → m PUnit
+
+instance [MonadDStore κ β m] : MonadStore1Of k (β k) m where
+  fetch? := MonadDStore.fetch? k
+  store o := MonadDStore.store k o
+
+/-- A monad equipped with a key-object store. -/
+abbrev MonadStore κ α m := MonadDStore κ (fun _ => α) m
+
+instance [MonadLift m n] [MonadDStore κ β m] : MonadDStore κ β n where
+  fetch? k := liftM (m := m) <| fetch? k
+  store k a := liftM (m := m) <| store k a
+
+@[inline] def fetchOrCreate [Monad m]
+(key : κ) [MonadStore1Of key α m] (create : m α) : m α := do
+  if let some val ← fetch? key then
+    return val
+  else
+    let val ← create
+    store key val
+    return val

backend/core/leanprover--lean4---v4.22.0/src/lean/lake/Lake/Util/StoreInsts.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Lake.Util.DRBMap
+import Lake.Util.RBArray
+import Lake.Util.Family
+import Lake.Util.Store
+
+open Lean
+namespace Lake
+
+instance [Monad m] [EqOfCmpWrt κ β cmp] : MonadDStore κ β (StateT (DRBMap κ β cmp) m) where
+  fetch? k := return (← get).find? k
+  store k a := modify (·.insert k a)
+
+instance [MonadLiftT (ST ω) m] [Monad m] [EqOfCmpWrt κ β cmp] : MonadDStore κ β (StateRefT' ω (DRBMap κ β cmp) m) where
+  fetch? k := return (← get).find? k
+  store k a := modify (·.insert k a)
+
+instance [Monad m] : MonadStore κ α (StateT (RBMap κ α cmp) m) where
+  fetch? k := return (← get).find? k
+  store k a := modify (·.insert k a)
+
+instance [MonadLiftT (ST ω) m] [Monad m] : MonadStore κ α (StateRefT' ω (RBMap κ α cmp) m) where
+  fetch? k := return (← get).find? k
+  store k a := modify (·.insert k a)
+
+instance [Monad m] : MonadStore κ α (StateT (RBArray κ α cmp) m) where
+  fetch? k := return (← get).find? k
+  store k a := modify (·.insert k a)
+
+instance [MonadLiftT (ST ω) m] [Monad m] : MonadStore κ α (StateRefT' ω (RBArray κ α cmp) m) where
+  fetch? k := return (← get).find? k
+  store k a := modify (·.insert k a)
+
+-- uses the eagerly specialized `RBMap` functions in `NameMap`
+instance [Monad m] : MonadStore Name α (StateT (NameMap α) m) where
+  fetch? k := return (← get).find? k
+  store k a := modify (·.insert k a)
+
+instance [MonadLiftT (ST ω) m] [Monad m] : MonadStore Name α (StateRefT' ω (NameMap α) m) where
+  fetch? k := return (← get).find? k
+  store k a := modify (·.insert k a)
+
+@[inline] instance [MonadDStore κ β m] [t : FamilyOut β k α] : MonadStore1Of k α m where
+  fetch? := cast (by rw [t.fam_eq]) <| fetch? (m := m) k
+  store a := store k <| cast t.fam_eq.symm a

backend/core/leanprover--lean4---v4.22.0/src/lean/lake/Lake/Util/Sugar.lean

@@ -0,0 +1,15 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Init.Notation
+
+namespace Lake
+
+macro "try " x:term " else " y:term : term =>
+  ``($x <|> $y)
+
+macro "try " x:doSeq " else " y:doSeq : doElem =>
+  `(doElem| (do $x) <|> (do $y))

backend/core/leanprover--lean4---v4.22.0/src/lean/lake/Lake/Util/Task.lean

@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Init.Control.Option
+
+namespace Lake
+
+instance : Monad Task where
+  map := Task.map
+  pure := Task.pure
+  bind := Task.bind
+
+abbrev ETask ε := ExceptT ε Task
+abbrev OptionTask := OptionT Task
+
+def BaseIOTask := Task
+instance : Monad BaseIOTask := inferInstanceAs <| Monad Task
+instance [Inhabited α] : Inhabited (BaseIOTask α) := inferInstance
+
+abbrev EIOTask ε := ExceptT ε BaseIOTask
+abbrev OptionIOTask := OptionT BaseIOTask
+
+instance : Inhabited (OptionIOTask α) := ⟨failure⟩

backend/core/leanprover--lean4---v4.22.0/src/lean/lake/Lake/Util/Version.lean

@@ -0,0 +1,226 @@
+/-
+Copyright (c) 2024 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Lean.Data.Json
+import Lake.Util.Date
+
+/-! # Version
+
+This module contains useful definitions for manipulating versions.
+It also defines a `v!"<ver>"` syntax for version literals.
+-/
+
+open System Lean
+
+namespace Lake
+
+/-- The major-minor-patch triple of a [SemVer](https://semver.org/). -/
+structure SemVerCore where
+  major : Nat := 0
+  minor : Nat := 0
+  patch : Nat := 0
+  deriving Inhabited, Repr, DecidableEq, Ord
+
+instance : LT SemVerCore := ltOfOrd
+instance : LE SemVerCore := leOfOrd
+instance : Min SemVerCore := minOfLe
+instance : Max SemVerCore := maxOfLe
+
+def SemVerCore.parse (ver : String) : Except String SemVerCore := do
+  try
+    match ver.split (· == '.') with
+    | [major, minor, patch] =>
+        let parseNat (v : String) (what : String) := do
+          let some v := v.toNat?
+            | throw s!"expect numeral {what} version, got '{v}'"
+          return v
+        return {
+          major := ← parseNat major "major"
+          minor := ← parseNat minor "minor"
+          patch := ← parseNat patch "patch"
+        }
+    | ps => throw s!"incorrect number of components: got {ps.length}, expected 3"
+  catch e =>
+    throw s!"invalid version core: {e}"
+
+protected def SemVerCore.toString (ver : SemVerCore) : String :=
+  s!"{ver.major}.{ver.minor}.{ver.patch}"
+
+instance : ToString SemVerCore := ⟨SemVerCore.toString⟩
+instance : ToJson SemVerCore := ⟨(·.toString)⟩
+instance : FromJson SemVerCore := ⟨(do SemVerCore.parse <| ← fromJson? ·)⟩
+
+/--
+A Lean-style semantic version.
+A major-minor-patch triple with an optional arbitrary `-` suffix.
+-/
+structure StdVer extends SemVerCore where
+  specialDescr : String := ""
+  deriving Inhabited, Repr, DecidableEq
+
+/-- A Lean version. -/
+abbrev LeanVer := StdVer
+
+instance : Coe StdVer SemVerCore := ⟨StdVer.toSemVerCore⟩
+
+@[inline] protected def StdVer.ofSemVerCore (ver : SemVerCore) : StdVer :=
+  {toSemVerCore := ver, specialDescr := ""}
+
+instance : Coe SemVerCore StdVer := ⟨StdVer.ofSemVerCore⟩
+
+protected def StdVer.compare (a b : StdVer) : Ordering :=
+  match compare a.toSemVerCore b.toSemVerCore with
+  | .eq =>
+    match a.specialDescr, b.specialDescr with
+    | "", "" => .eq
+    |  _, "" => .lt
+    | "",  _ => .gt
+    | a, b => compare a b
+  | ord => ord
+
+instance : Ord StdVer := ⟨StdVer.compare⟩
+
+instance : LT StdVer := ltOfOrd
+instance : LE StdVer := leOfOrd
+instance : Min StdVer := minOfLe
+instance : Max StdVer := maxOfLe
+
+def StdVer.parse (ver : String) : Except String StdVer := do
+  let sepPos := ver.find (· == '-')
+  if h : ver.atEnd sepPos then
+    SemVerCore.parse ver
+  else
+    let core ← SemVerCore.parse <| ver.extract 0 sepPos
+    let specialDescr := ver.extract (ver.next' sepPos h) ver.endPos
+    if specialDescr.isEmpty then
+      throw "invalid version: '-' suffix cannot be empty"
+    return {toSemVerCore := core, specialDescr}
+
+protected def StdVer.toString (ver : StdVer) : String :=
+  if ver.specialDescr.isEmpty then
+    ver.toSemVerCore.toString
+  else
+    s!"{ver.toSemVerCore}-{ver.specialDescr}"
+
+instance : ToString StdVer := ⟨StdVer.toString⟩
+instance : ToJson StdVer := ⟨(·.toString)⟩
+instance : FromJson StdVer := ⟨(do StdVer.parse <| ← fromJson? ·)⟩
+
+/-- A Lean toolchain version. -/
+inductive ToolchainVer
+| release (ver : LeanVer)
+| nightly (date : Date)
+| pr (no : Nat)
+| other (name : String)
+deriving Repr, DecidableEq
+
+instance : Coe LeanVer ToolchainVer := ⟨ToolchainVer.release⟩
+
+def ToolchainVer.defaultOrigin := "leanprover/lean4"
+def ToolchainVer.prOrigin := "leanprover/lean4-pr-releases"
+
+def ToolchainVer.ofString (ver : String) : ToolchainVer := Id.run do
+  let colonPos := ver.posOf ':'
+  let (origin, tag) :=
+    if h : colonPos < ver.endPos then
+      let pos := ver.next' colonPos (by simp_all [String.endPos, String.atEnd])
+      (ver.extract 0 colonPos, ver.extract pos ver.endPos)
+    else
+      ("", ver)
+  if tag.startsWith "v" then
+    if let .ok ver := StdVer.parse (tag.drop 1) then
+      if origin.isEmpty || origin == defaultOrigin then
+        return .release ver
+    return .other ver
+  else if tag.startsWith "nightly-" then
+    if let some date := Date.ofString? (tag.drop "nightly-".length) then
+      if origin.isEmpty || origin == defaultOrigin then
+        return .nightly date
+  else if tag.startsWith "pr-release-" then
+    if let some n := (tag.drop "pr-release-".length).toNat? then
+      if origin.isEmpty || origin == prOrigin then
+        return .pr n
+  else
+    if let .ok ver := StdVer.parse ver then
+      if origin.isEmpty || origin == defaultOrigin then
+        return .release ver
+  return .other ver
+
+/-- Parse a toolchain from a `lean-toolchain` file. -/
+def ToolchainVer.ofFile? (toolchainFile : FilePath) : IO (Option ToolchainVer) := do
+  try
+    let toolchainString ← IO.FS.readFile toolchainFile
+    return some <| ToolchainVer.ofString toolchainString.trim
+  catch
+    | .noFileOrDirectory .. =>
+      return none
+    | e => throw e
+
+/-- The `elan` toolchain file name (i.e., `lean-toolchain`). -/
+def toolchainFileName : FilePath := "lean-toolchain"
+
+/-- Parse a toolchain from the `lean-toolchain` file of the directory `dir`. -/
+@[inline] def ToolchainVer.ofDir? (dir : FilePath) : IO (Option ToolchainVer) :=
+  ToolchainVer.ofFile? (dir / toolchainFileName)
+
+protected def ToolchainVer.toString (ver : ToolchainVer) : String :=
+  match ver with
+  | .release ver => s!"{defaultOrigin}:v{ver}"
+  | .nightly date => s!"{defaultOrigin}:nightly-{date}"
+  | .pr n => s!"{prOrigin}:pr-release-{n}"
+  | .other s => s
+
+instance : ToString ToolchainVer := ⟨ToolchainVer.toString⟩
+instance : ToJson ToolchainVer := ⟨(·.toString)⟩
+instance : FromJson ToolchainVer := ⟨(ToolchainVer.ofString <$> fromJson? ·)⟩
+
+protected def ToolchainVer.lt (a b : ToolchainVer) : Prop :=
+  match a, b with
+  | .release v1, .release v2 => v1 < v2
+  | .nightly d1, .nightly d2 => d1 < d2
+  | _, _ => False
+
+instance : LT ToolchainVer := ⟨ToolchainVer.lt⟩
+
+instance ToolchainVer.decLt (a b : ToolchainVer) : Decidable (a < b) :=
+  match a, b with
+  | .release v1, .release v2 => inferInstanceAs (Decidable (v1 < v2))
+  | .nightly d1, .nightly d2 => inferInstanceAs (Decidable (d1 < d2))
+  | .release _, .pr _ | .release _, .nightly _ | .release _, .other _
+  | .nightly _, .release _ | .nightly _, .pr _ | .nightly _, .other _
+  | .pr _, _ | .other _, _ => .isFalse (by simp [LT.lt, ToolchainVer.lt])
+
+protected def ToolchainVer.le (a b : ToolchainVer) : Prop :=
+  match a, b with
+  | .release v1, .release v2 => v1 ≤ v2
+  | .nightly d1, .nightly d2 => d1 ≤ d2
+  | .pr n1, .pr n2 => n1 = n2
+  | .other v1, .other v2 => v1 = v2
+  | _, _ => False
+
+instance : LE ToolchainVer := ⟨ToolchainVer.le⟩
+
+instance ToolchainVer.decLe (a b : ToolchainVer) : Decidable (a ≤ b) :=
+  match a, b with
+  | .release v1, .release v2 => inferInstanceAs (Decidable (v1 ≤ v2))
+  | .nightly d1, .nightly d2 => inferInstanceAs (Decidable (d1 ≤ d2))
+  | .pr n1, .pr n2 => inferInstanceAs (Decidable (n1 = n2))
+  | .other v1, .other v2 => inferInstanceAs (Decidable (v1 = v2))
+  | .release _, .pr _ | .release _, .nightly _ | .release _, .other _
+  | .nightly _, .release _ | .nightly _, .pr _ | .nightly _, other _
+  | .pr _, .release _ | .pr _, .nightly _ |  .pr _, .other _
+  | .other _, .release _ | .other _, .nightly _ | .other _, .pr _ =>
+    .isFalse (by simp [LE.le, ToolchainVer.le])
+
+/-- Parses a version from a string. -/
+class DecodeVersion (α : Type u) where
+  decodeVersion : String → Except String α
+
+export DecodeVersion (decodeVersion)
+
+instance : DecodeVersion SemVerCore := ⟨SemVerCore.parse⟩
+@[default_instance] instance : DecodeVersion StdVer := ⟨StdVer.parse⟩
+instance : DecodeVersion ToolchainVer := ⟨(pure <| ToolchainVer.ofString ·)⟩

backend/core/leanprover--lean4---v4.22.0/src/lean/lake/tests/8448/A.lean

@@ -0,0 +1,2 @@
+@[extern "increment8"]
+opaque A.increment8 : Int8 → Int8

backend/core/leanprover--lean4---v4.22.0/src/lean/lake/tests/8448/B.lean

@@ -0,0 +1,5 @@
+import A
+
+def B.increment8 := A.increment8
+
+#eval B.increment8 1