leanprover-community · JOSHCLUNE · May 26, 2026 · Sep 27, 2025 · Sep 27, 2025 · Sep 30, 2025
diff --git a/Duper/Clause.lean b/Duper/Clause.lean
@@ -51,8 +51,8 @@ def toExpr (lit : Lit) : Expr :=
 def fromSingleExpr (e : Expr) (sign := true) : Lit :=
   Lit.mk
     (sign := true)
-    (lvl := levelOne)
-    (ty := mkSort levelZero)
+    (lvl := Level.one)
+    (ty := mkSort Level.zero)
     (lhs := Expr.consumeMData e)
     (rhs := if sign then mkConst ``True else mkConst ``False)
 

diff --git a/Duper/Interface.lean b/Duper/Interface.lean
@@ -481,12 +481,16 @@ def formulasWithStringsToAutoLemmas (formulas : List (Expr × Expr × Array Name
 
 /-- Determines whether `lem`'s deriv info indicates that `lem` is part of the goal and should be included in the set of support. Note that `derivInfo`
     only works on lemmas generated from `formulasToAutoLemmas` or `formulasWithStringsToAutoLemmas`. In cases where the lemma was not generated from
-    `formulasToAutoLemmas`, `derivInfo` defaults to indicating that both `isFromGoal` and `includeInSetOfSupport` are `true`. -/
+    `formulasToAutoLemmas`, `derivInfo` defaults to indicating that both `isFromGoal` and `includeInSetOfSupport` are `true`. The only exception to this
+    is if all leaves have exactly the form "termLikeDefEq", in which case `derivInfo` indicates that `isFromGoal` is `false`. -/
 def derivInfo (lem : Auto.Lemma) : Bool × Bool :=
   let derivLeaves := getLeavesFromDTr lem.deriv
   let matchesFormat := derivLeaves.any (fun l => "true, true".isPrefixOf l || "false, true".isPrefixOf l || "true, false".isPrefixOf l || "false, false".isPrefixOf l)
   if !matchesFormat then
-    (true, true)
+    if derivLeaves.all (fun l => l == "termLikeDefEq") then
+      (false, true)
+    else
+      (true, true)
   else
     let isFromGoal := derivLeaves.any (fun l => "true".isPrefixOf l)
     let includeInSetOfSupport := derivLeaves.any (fun l => "true, true".isPrefixOf l || "false, true".isPrefixOf l)

diff --git a/Duper/Rules/BoolHoist.lean b/Duper/Rules/BoolHoist.lean
@@ -28,7 +28,7 @@ def boolHoistAtExpr (e : Expr) (pos : ClausePos) (given : Clause) (c : MClause)
       return #[]
     let eType ← inferType e
     let loaded ← getLoadedClauses
-    let ug ← unifierGenerator #[(eType, .sort levelZero)]
+    let ug ← unifierGenerator #[(eType, .sort Level.zero)]
     let yC := do
       setLoadedClauses loaded
       let lit := c.lits[pos.lit]!

diff --git a/Duper/Rules/BoolSimp.lean b/Duper/Rules/BoolSimp.lean
@@ -320,7 +320,7 @@ partial def mkRule25Theorem (e : Expr) (counter : Nat) (i : Nat) (j : Nat) : Met
   | _ =>
     let iIdx := (counter - 1) - i
     let jIdx := (counter - 1) - j
-    return mkApp2 (mkConst ``False.elim [levelZero]) e (mkApp (Expr.bvar iIdx) (Expr.bvar jIdx))
+    return mkApp2 (mkConst ``False.elim [Level.zero]) e (mkApp (Expr.bvar iIdx) (Expr.bvar jIdx))
 
 /-- Assuming e has the form e1 ∨ e2 ∨ ... ∨ en, returns an array #[e1, e2, ... en].
     Note: If e has the form (e1a ∨ e1b) ∨ e2 ∨ ... en, then the disjunction (e1a ∨ e1b) will
@@ -870,7 +870,7 @@ partial def applyRule27 (e : Expr) : RuleM (Option (Nat × Nat)) := do
 /-- s1 ↔ s2 ↦ s1 = s2 -/
 def applyRule28 (e : Expr) : Option Expr :=
   match e with
-  | Expr.app (Expr.app (Expr.const ``Iff _) e1) e2 => some $ mkApp3 (mkConst ``Eq [levelOne]) (mkSort levelZero) e1 e2
+  | Expr.app (Expr.app (Expr.const ``Iff _) e1) e2 => some $ mkApp3 (mkConst ``Eq [Level.one]) (mkSort Level.zero) e1 e2
   | _ => none
 
 /-- Returns the rule theorem corresponding to boolSimpRule with the first argument applied.
@@ -1095,7 +1095,7 @@ def getBoolSimpRuleTheorem (boolSimpRule : BoolSimpRule) (originalExp : Expr) (i
   | rule23 => -- ∀ p : Prop, f(p) ↦ f(True) ∧ f(False)
     match originalExp.consumeMData with
     | Expr.forallE n _ b _ => do
-      let bFunction := Expr.lam n (mkSort levelZero) b BinderInfo.default
+      let bFunction := Expr.lam n (mkSort Level.zero) b BinderInfo.default
       return mkApp (mkConst ``rule23Theorem) bFunction
     | _ => throwError "Invalid originalExp {originalExp} for rule23"
   | rule23b => -- ∀ b : Bool, f(b) ↦ f true ∧ f false (assuming `f : Bool → Prop`)
@@ -1157,7 +1157,7 @@ def mkBoolSimpProof (substPos : ClausePos) (boolSimpRule : BoolSimpRule) (ijOpt
           let abstrExp := abstrLit.toExpr
           let abstrLam :=
             if boolSimpRuleOperatesOnBool boolSimpRule then mkLambda `x BinderInfo.default (mkConst ``Bool) abstrExp
-            else mkLambda `x BinderInfo.default (mkSort levelZero) abstrExp
+            else mkLambda `x BinderInfo.default (mkSort Level.zero) abstrExp
           let rwproof ← Meta.mkAppM ``Eq.mp #[← Meta.mkAppM ``congrArg #[abstrLam, boolSimpRuleThm], h]
           Meta.mkLambdaFVars #[h] $ ← orIntro (cLits.map Lit.toExpr) i $ rwproof
         else

diff --git a/Duper/Rules/ContextualLiteralCutting.lean b/Duper/Rules/ContextualLiteralCutting.lean
@@ -49,7 +49,7 @@ def mkContextualLiteralCuttingProof (negatedLitMainIdx : Nat) (assignment : List
                       let hSideFlipped ← Meta.mkAppM ``Eq.symm #[hSide]
                       Meta.mkAppM' hMain #[hSideFlipped]
                     else Meta.mkAppM' hMain #[hSide]
-                Meta.mkLambdaFVars #[hMain] $ mkApp2 (mkConst ``False.elim [levelZero]) body contraProof
+                Meta.mkLambdaFVars #[hMain] $ mkApp2 (mkConst ``False.elim [Level.zero]) body contraProof
               caseProofsMain := caseProofsMain.push pr
             else
               let pr ← Meta.withLocalDeclD `hMain curMainLit.toExpr fun hMain => do

diff --git a/Duper/Rules/DatatypeAcyclicity.lean b/Duper/Rules/DatatypeAcyclicity.lean
@@ -167,7 +167,7 @@ def mkDatatypeAcyclicityProof (removedLitNum : Nat) (litSide : LitSide) (premise
           let gtProof ← buildGtProof lit.lhs lit.rhs
           let neProof ← mkAppM ``Nat.ne_of_gt #[gtProof]
           sizeOfEqFalseMVarId.assign neProof
-          let proofCase := mkApp2 (mkConst ``False.elim [levelZero]) body $ mkApp sizeOfEqFalseMVar sizeOfEq -- Has the type `body`
+          let proofCase := mkApp2 (mkConst ``False.elim [Level.zero]) body $ mkApp sizeOfEqFalseMVar sizeOfEq -- Has the type `body`
           trace[duper.rule.datatypeAcyclicity] "lit: {lit}, lit.ty: {lit.ty}, sizeOfInst: {sizeOfInst}, abstrLam: {abstrLam}, sizeOfEq: {sizeOfEq}"
           trace[duper.rule.datatypeAcyclicity] "sizeOfEqFalseMVar: {sizeOfEqFalseMVar}, proofCase: {proofCase}"
           Meta.mkLambdaFVars #[h] proofCase

diff --git a/Duper/Rules/DatatypeDistinctness.lean b/Duper/Rules/DatatypeDistinctness.lean
@@ -74,7 +74,7 @@ def mkDatatypeDistinctnessProof (refs : List (Option Nat)) (premises : List Expr
               pure $ #[some (mkConst ``False)] ++ (Array.range (2 * numParams + 2)).map (fun _ => none) ++
                 (← (Array.range numParams).mapM (fun x => do pure $ some (← mkAppOptM ``rfl #[none, some (lit.ty.getAppArgs[x]!)]))) ++ #[some (← mkAppM ``heq_of_eq #[h])]
           let proofCase ← mkAppOptM' (mkConst (.str tyName "noConfusion") (0 :: lvls)) noConfusionArgs
-          let proofCase := mkApp2 (mkConst ``False.elim [levelZero]) body proofCase
+          let proofCase := mkApp2 (mkConst ``False.elim [Level.zero]) body proofCase
           Meta.mkLambdaFVars #[h] proofCase
         proofCases := proofCases.push proofCase
       | none => -- refs[i] should have the value (some j) where parentLits[i] == c[j]

diff --git a/Duper/Rules/DatatypeInjectivity.lean b/Duper/Rules/DatatypeInjectivity.lean
@@ -97,7 +97,7 @@ def mkDatatypeInjectivityNegProof (removedLitNum : Nat) (premises : List Expr) (
             match ← inferType injEq with
             | Expr.app (Expr.app (Expr.app (Expr.const ``Eq [_]) _) _) e2 => pure e2
             | _ => throwError "mkDatatypeInjectivityNegProof :: Type of {injEq} is not an equality as expected"
-          let propMVar ← mkFreshExprMVar (mkSort levelZero)
+          let propMVar ← mkFreshExprMVar (mkSort Level.zero)
           let abstrLam ← mkLambdaFVars #[propMVar] $ ← mkAppM ``Eq #[← mkAppM ``Not #[propMVar], ← mkAppM ``Not #[argEqualities]]
           let proofCase ← mkAppM ``Eq.mpr #[← mkAppM ``congrArg #[abstrLam, injEq], ← mkAppM ``Eq.refl #[← mkAppM ``Not #[argEqualities]]]
           let proofCase ← mkAppM ``Eq.mp #[proofCase, h]

diff --git a/Duper/Rules/DecElim.lean b/Duper/Rules/DecElim.lean
@@ -52,7 +52,7 @@ def mkDecElimProof (refs : List (Option Nat)) (premises : List Expr) (parents :
         trace[duper.rule.decElim] "Built {proofCase} proving {d} is false"
         let pr ← Meta.withLocalDeclD `h lit.toExpr fun h => do
           let proofCase := mkApp proofCase h
-          let proofCase := mkApp2 (mkConst ``False.elim [levelZero]) body proofCase
+          let proofCase := mkApp2 (mkConst ``False.elim [Level.zero]) body proofCase
           Meta.mkLambdaFVars #[h] proofCase
         caseProofs := caseProofs.push pr
       | some j =>

diff --git a/Duper/Rules/DestructiveEqualityResolution.lean b/Duper/Rules/DestructiveEqualityResolution.lean
@@ -32,7 +32,7 @@ def mkDestructiveEqualtiyResolutionProof (i : Nat) (premises : List Expr) (paren
         let pr ← Meta.withLocalDeclD `h lit.toExpr fun h => do
           let pr := mkApp2 (mkConst ``rfl [lit.lvl]) lit.ty lit.lhs
           let pr := mkApp h pr
-          let pr := mkApp2 (mkConst ``False.elim [levelZero]) body pr
+          let pr := mkApp2 (mkConst ``False.elim [Level.zero]) body pr
           Meta.mkLambdaFVars #[h] pr
         caseProofs := caseProofs.push pr
       else

diff --git a/Duper/Rules/ElimResolvedLit.lean b/Duper/Rules/ElimResolvedLit.lean
@@ -28,7 +28,7 @@ def mkElimResolvedLitProof (refs : List (Option Nat)) (premises : List Expr) (pa
         let proofCase ← Meta.withLocalDeclD `h lit.toExpr fun h => do
           let proofCase := mkApp2 (mkConst ``rfl [lit.lvl]) lit.ty lit.lhs
           let proofCase := mkApp h proofCase
-          let proofCase := mkApp2 (mkConst ``False.elim [levelZero]) body proofCase
+          let proofCase := mkApp2 (mkConst ``False.elim [Level.zero]) body proofCase
           Meta.mkLambdaFVars #[h] proofCase
         proofCases := proofCases.push proofCase
       else

diff --git a/Duper/Rules/EqHoist.lean b/Duper/Rules/EqHoist.lean
@@ -39,7 +39,7 @@ def mkEqHoistProof (pos : ClausePos) (premises : List Expr)
           let substLitPos : LitPos := ⟨pos.side, pos.pos⟩
           let abstrLit ← (lit.abstractAtPos! substLitPos)
           let abstrExp := abstrLit.toExpr
-          let abstrLam := mkLambda `x BinderInfo.default (mkSort levelZero) abstrExp
+          let abstrLam := mkLambda `x BinderInfo.default (mkSort Level.zero) abstrExp
           let lastTwoClausesProof ← Meta.mkAppM ``eq_hoist_proof #[freshVar1, freshVar2, abstrLam, h]
           Meta.mkLambdaFVars #[h] $ ← orSubclause (cLits.map Lit.toExpr) 2 lastTwoClausesProof
         else

diff --git a/Duper/Rules/EqualityResolution.lean b/Duper/Rules/EqualityResolution.lean
@@ -27,7 +27,7 @@ def mkEqualityResolutionProof (i : Nat) (premises : List Expr) (parents : List P
         let pr ← Meta.withLocalDeclD `h lit.toExpr fun h => do
           let pr := mkApp2 (mkConst ``rfl [lit.lvl]) lit.ty lit.lhs
           let pr := mkApp h pr
-          let pr := mkApp2 (mkConst ``False.elim [levelZero]) body pr
+          let pr := mkApp2 (mkConst ``False.elim [Level.zero]) body pr
           Meta.mkLambdaFVars #[h] pr
         caseProofs := caseProofs.push pr
       else

diff --git a/Duper/Rules/ExistsHoist.lean b/Duper/Rules/ExistsHoist.lean
@@ -38,7 +38,7 @@ def mkExistsHoistProof (pos : ClausePos) (premises : List Expr) (parents : List
           let substLitPos : LitPos := ⟨pos.side, pos.pos⟩
           let abstrLit ← (lit.abstractAtPos! substLitPos)
           let abstrExp := abstrLit.toExpr
-          let abstrLam := mkLambda `x BinderInfo.default (mkSort levelZero) abstrExp
+          let abstrLam := mkLambda `x BinderInfo.default (mkSort Level.zero) abstrExp
           let lastTwoLitsProof ← Meta.mkAppM ``exists_hoist_proof #[freshVar1, abstrLam, h]
           Meta.mkLambdaFVars #[h] $ ← orSubclause (cLits.map Lit.toExpr) 2 lastTwoLitsProof
         else
@@ -70,7 +70,7 @@ def existsHoistAtExpr (e : Expr) (pos : ClausePos) (given : Clause) (c : MClause
     -- Make freshVars, freshVarExistsExpr and newLitLhs
     let freshVar1 ← mkFreshExprMVar none
     let freshVar1Ty ← inferType freshVar1
-    let freshVar2Ty := Expr.forallE .anonymous freshVar1Ty (mkSort levelZero) BinderInfo.default -- freshVar1Ty → Prop
+    let freshVar2Ty := Expr.forallE .anonymous freshVar1Ty (mkSort Level.zero) BinderInfo.default -- freshVar1Ty → Prop
     let freshVar2 ← mkFreshExprMVar freshVar2Ty
     let freshVarExistsExpr ← mkAppM ``Exists #[freshVar2]
     let newLitLhs := .app freshVar2 freshVar1

diff --git a/Duper/Rules/FalseElim.lean b/Duper/Rules/FalseElim.lean
@@ -38,13 +38,13 @@ def mkFalseElimProof (i : Nat) (premises : List Expr) (parents : List ProofParen
         if lit.lhs == mkConst ``True then -- lit unified with `True = False`
           let pr ← Meta.withLocalDeclD `h lit.toExpr fun h => do
             let proofCase := mkApp (mkConst ``true_ne_false) h
-            let proofCase := mkApp2 (mkConst ``False.elim [levelZero]) body proofCase
+            let proofCase := mkApp2 (mkConst ``False.elim [Level.zero]) body proofCase
             Meta.mkLambdaFVars #[h] proofCase
           caseProofs := caseProofs.push pr
         else -- lit unified with `False = True`
           let pr ← Meta.withLocalDeclD `h lit.toExpr fun h => do
             let proofCase := mkApp (mkConst ``false_ne_true) h
-            let proofCase := mkApp2 (mkConst ``False.elim [levelZero]) body proofCase
+            let proofCase := mkApp2 (mkConst ``False.elim [Level.zero]) body proofCase
             Meta.mkLambdaFVars #[h] proofCase
           caseProofs := caseProofs.push pr
       else

diff --git a/Duper/Rules/FluidBoolHoist.lean b/Duper/Rules/FluidBoolHoist.lean
@@ -77,8 +77,8 @@ def fluidBoolHoistAtExpr (e : Expr) (pos : ClausePos) (given : Clause) (c : MCla
     if litEligibility == Eligibility.notEligible || sideComparison == Comparison.LessThan then return #[]
 
     let freshFunctionOutputType ← inferType e
-    let freshFunction ← mkFreshFunction (mkSort levelZero) freshFunctionOutputType -- mkFreshFunction defined in FluidSup.lean
-    let freshPropVar ← mkFreshExprMVar (mkSort levelZero)
+    let freshFunction ← mkFreshFunction (mkSort Level.zero) freshFunctionOutputType -- mkFreshFunction defined in FluidSup.lean
+    let freshPropVar ← mkFreshExprMVar (mkSort Level.zero)
     let freshFunctionApp ← Meta.whnf (.app freshFunction freshPropVar)
 
     let loaded ← getLoadedClauses

diff --git a/Duper/Rules/ForallHoist.lean b/Duper/Rules/ForallHoist.lean
@@ -38,7 +38,7 @@ def mkForallHoistProof (pos : ClausePos) (premises : List Expr)
           let substLitPos : LitPos := ⟨pos.side, pos.pos⟩
           let abstrLit ← (lit.abstractAtPos! substLitPos)
           let abstrExp := abstrLit.toExpr
-          let abstrLam := mkLambda `x BinderInfo.default (mkSort levelZero) abstrExp
+          let abstrLam := mkLambda `x BinderInfo.default (mkSort Level.zero) abstrExp
           let lastTwoLitsProof ← Meta.mkAppM ``forall_hoist_proof #[freshVar1, abstrLam, h]
           Meta.mkLambdaFVars #[h] $ ← orSubclause (cLits.map Lit.toExpr) 2 lastTwoLitsProof
         else
@@ -51,7 +51,7 @@ def mkForallHoistProof (pos : ClausePos) (premises : List Expr)
 /-- Returns the dependent forall and lambda expressions -/
 def mkForallAndLambda (freshVar1Ty : Expr) : MetaM (Expr × Expr) :=
   Meta.withLocalDeclD `_ freshVar1Ty fun fvar => do
-    let newMVar ← Meta.mkFreshExprMVar (mkSort levelZero)
+    let newMVar ← Meta.mkFreshExprMVar (mkSort Level.zero)
     let forallExpr ← Meta.mkForallFVars #[fvar] newMVar
     let lambdaExpr ← Meta.mkLambdaFVars #[fvar] newMVar
     return (forallExpr, lambdaExpr)

diff --git a/Duper/Rules/IdentBoolFalseElim.lean b/Duper/Rules/IdentBoolFalseElim.lean
@@ -36,11 +36,11 @@ def mkIdentBoolFalseElimProof (refs : List (Option Nat)) (premises : List Expr)
         let proofCase ← Meta.withLocalDeclD `h lit.toExpr fun h => do
           if (lit.lhs == mkConst ``false) then
             let proofCase := mkApp (mkConst ``bool_false_ne_true) h
-            let proofCase := mkApp2 (mkConst ``False.elim [levelZero]) body proofCase
+            let proofCase := mkApp2 (mkConst ``False.elim [Level.zero]) body proofCase
             Meta.mkLambdaFVars #[h] proofCase
           else if(lit.lhs == mkConst ``true) then
             let proofCase := mkApp (mkConst ``bool_true_ne_false) h
-            let proofCase := mkApp2 (mkConst ``False.elim [levelZero]) body proofCase
+            let proofCase := mkApp2 (mkConst ``False.elim [Level.zero]) body proofCase
             Meta.mkLambdaFVars #[h] proofCase
           else
             throwError "mkIdentBoolFalseElimProof failed to match {lit.lhs} to an expected expression"

diff --git a/Duper/Rules/IdentPropFalseElim.lean b/Duper/Rules/IdentPropFalseElim.lean
@@ -16,7 +16,7 @@ initialize Lean.registerTraceClass `duper.rule.identPropFalseElim
 def isFalsePropLiteral (lit : Lit) : MetaM Bool := do
   match lit.ty with
   | Expr.sort lvl =>
-    if Level.isEquiv (← Lean.instantiateLevelMVars lvl) levelZero then
+    if Level.isEquiv (← Lean.instantiateLevelMVars lvl) Level.zero then
       return lit.sign &&
         ((lit.lhs == mkConst ``True && lit.rhs == mkConst ``False) ||
         (lit.lhs == mkConst ``False && lit.rhs == mkConst ``True))
@@ -42,11 +42,11 @@ def mkIdentPropFalseElimProof (refs : List (Option Nat)) (premises : List Expr)
         let proofCase ← Meta.withLocalDeclD `h lit.toExpr fun h => do
           if (lit.lhs == mkConst ``False) then
             let proofCase := mkApp (mkConst ``prop_false_ne_true) h
-            let proofCase := mkApp2 (mkConst ``False.elim [levelZero]) body proofCase
+            let proofCase := mkApp2 (mkConst ``False.elim [Level.zero]) body proofCase
             Meta.mkLambdaFVars #[h] proofCase
           else if(lit.lhs == mkConst ``True) then
             let proofCase := mkApp (mkConst ``prop_true_ne_false) h
-            let proofCase := mkApp2 (mkConst ``False.elim [levelZero]) body proofCase
+            let proofCase := mkApp2 (mkConst ``False.elim [Level.zero]) body proofCase
             Meta.mkLambdaFVars #[h] proofCase
           else
             throwError "mkIdentPropFalseElimProof failed to match {lit.lhs} to an expected expression"

diff --git a/Duper/Rules/NeHoist.lean b/Duper/Rules/NeHoist.lean
@@ -39,7 +39,7 @@ def mkNeHoistProof (pos : ClausePos) (premises : List Expr)
           let substLitPos : LitPos := ⟨pos.side, pos.pos⟩
           let abstrLit ← (lit.abstractAtPos! substLitPos)
           let abstrExp := abstrLit.toExpr
-          let abstrLam := mkLambda `x BinderInfo.default (mkSort levelZero) abstrExp
+          let abstrLam := mkLambda `x BinderInfo.default (mkSort Level.zero) abstrExp
           let lastTwoClausesProof ← Meta.mkAppM ``ne_hoist_proof #[freshVar1, freshVar2, abstrLam, h]
           Meta.mkLambdaFVars #[h] $ ← orSubclause (cLits.map Lit.toExpr) 2 lastTwoClausesProof
         else