Bump toolchain to v4.8.0

Auto/Embedding/LCtx.lean

@@ -916,8 +916,10 @@ section add_nat
 
   def addAt_succ_l (lvl pos : Nat) (n : Nat) :
     addAt (.succ lvl) pos n = succAt pos (addAt lvl pos n) := by
-    dsimp [addAt, Nat.add_succ]
-    rw [mapAt_comp pos Nat.succ (fun x => x + lvl) n]
+    dsimp [addAt]
+    have heq: (fun x => x + (lvl + 1)) = (fun x => (x + lvl).succ) := by
+      apply funext; omega
+    rw [heq] ; apply mapAt_comp
 
   def addAt_succ_r (lvl pos : Nat) (n : Nat) :
     addAt (.succ lvl) pos n = addAt lvl pos (succAt pos n) := by
@@ -1015,8 +1017,9 @@ section genericInst
       case cons x xs =>
         simp at heq
         rw [← IH xs heq lctx n]
-        dsimp [pushLCtxs, Nat.blt, Nat.ble, Nat.add_succ]
-        rw [Nat.succ_sub_succ]
+        dsimp [pushLCtxs, Nat.blt, Nat.ble]
+        rw [Nat.add_succ, Nat.succ_sub_succ]
+        dsimp
 
   theorem contraPair.ofPushsPops (lvl : Nat) (xs : List α) (heq : xs.length = lvl) :
     contraPair (fun n => n + lvl) (fun lctx => List.ofFun lctx lvl = xs) (pushLCtxs xs) := by
@@ -1039,8 +1042,8 @@ section genericInst
         case cons ty tys x xs =>
           simp at heq
           apply HEq.trans _ (IH xs heq lctx n)
-          dsimp [Nat.blt, Nat.ble, Nat.add_succ]
-          rw [Nat.succ_sub_succ]; rfl)
+          dsimp [Nat.blt, Nat.ble]
+          rw [Nat.add_succ, Nat.succ_sub_succ]; rfl)
 
   theorem contraPairDep.ofPushsDepPopsDep
     {lctxty : α → Sort u} (lvl : Nat) {tys : List α}

Auto/Embedding/LamBVarOp.lean

@@ -252,7 +252,7 @@ theorem LamTerm.bvarLifts_add :
   rw [Nat.add_comm]; induction lvl₁
   case zero => rw [bvarLiftsIdx_zero]; rfl
   case succ lvl₁ IH =>
-    rw [Nat.add_succ]; rw [bvarLiftsIdx_succ_r, bvarLiftsIdx_succ_r, IH]    
+    rw [Nat.add_succ]; rw [bvarLiftsIdx_succ_r, bvarLiftsIdx_succ_r, IH]
 
 def LamWF.bvarLiftsIdx
   {lamVarTy lctx} {idx lvl : Nat}
@@ -266,7 +266,7 @@ def LamWF.fromBVarLiftsIdx
   {xs : List LamSort} (heq : xs.length = lvl)
   (rterm : LamTerm) (HWF : LamWF lamVarTy ⟨pushLCtxsAt xs idx lctx, rterm.bvarLiftsIdx idx lvl, rTy⟩) :
   LamWF lamVarTy ⟨lctx, rterm, rTy⟩ :=
-  LamWF.fromMapBVarAt (coPair.ofPushsPops _ _ heq) idx rterm HWF  
+  LamWF.fromMapBVarAt (coPair.ofPushsPops _ _ heq) idx rterm HWF
 
 theorem LamWF.interp_bvarLiftsIdx
   (lval : LamValuation.{u}) {idx lvl : Nat}
@@ -290,7 +290,7 @@ def LamWF.fromBVarLifts
   {xs : List LamSort} (heq : xs.length = lvl)
   (rterm : LamTerm) (HWF : LamWF lamVarTy ⟨pushLCtxs xs lctx, rterm.bvarLifts lvl, rTy⟩) :
   LamWF lamVarTy ⟨lctx, rterm, rTy⟩ :=
-  LamWF.fromBVarLiftsIdx (idx:=0) heq rterm (Eq.mp (by rw [pushLCtxsAt_zero]) HWF) 
+  LamWF.fromBVarLiftsIdx (idx:=0) heq rterm (Eq.mp (by rw [pushLCtxsAt_zero]) HWF)
 
 theorem LamWF.interp_bvarLifts
   (lval : LamValuation.{u}) {lvl : Nat}
@@ -392,9 +392,9 @@ theorem LamTerm.bvarLowersIdx?_bvar_eq_some :
     cases h₂ : (idx + lvl).ble n <;> simp
     case false =>
       have h₂' := Nat.lt_of_ble_eq_false h₂; clear h₂
-      apply not_or.mpr (And.intro ?nlt ?nge)
-      case nlt => intro h; have h' := Nat.not_le_of_lt h.left; apply h' h₁'
-      case nge => intro h; have h' := Nat.not_le_of_lt h₂'; apply h' h.left
+      apply (And.intro ?nlt ?nge)
+      case nlt => intro h; have h' := Nat.not_le_of_lt h; contradiction
+      case nge => intro h; have h' := Nat.not_le_of_lt h₂'; contradiction
     case true =>
       have h₂' := Nat.le_of_ble_eq_true h₂; clear h₂
       apply Iff.intro <;> intro h
@@ -535,4 +535,4 @@ def LamTerm.toString := LamTerm.toStringLCtx 0
 instance : ToString LamTerm where
   toString := LamTerm.toString
 
-end Auto.Embedding.Lam
+end Auto.Embedding.Lam

Auto/Embedding/LamBase.lean

@@ -2564,12 +2564,7 @@ theorem LamTerm.maxLooseBVarSucc.spec (m : Nat) :
   case mp =>
     let IH' := Nat.pred_le_pred (IH.mp h)
     rw [Nat.pred_succ] at IH'; exact IH'
-  case mpr =>
-    let h' := Nat.succ_le_succ h
-    apply IH.mpr; rw [Nat.succ_pred] at h'; exact h'
-    revert h; cases (maxLooseBVarSucc t)
-    case zero => intro h; cases h
-    case succ _ => intro _; simp
+  case mpr => apply IH.mpr; omega
 | .app _ t₁ t₂ => by
   dsimp [hasLooseBVarGe, maxLooseBVarSucc];
   rw [Bool.or_eq_true]; rw [spec m t₁]; rw [spec m t₂];
@@ -2954,7 +2949,7 @@ theorem LamTerm.getLamBodyN_mkLamFN_length_eq
     cases l <;> cases h
     case refl s' l =>
       dsimp [mkLamFN, getLamBodyN]
-      dsimp [Nat.add] at IH; apply IH; rfl
+      apply IH; rfl
 
 def LamTerm.getLamTysN (n : Nat) (t : LamTerm) : Option (List LamSort) :=
   match n with
@@ -3047,7 +3042,7 @@ theorem LamTerm.getAppArgsAux_eq : getAppArgsAux args t = getAppArgsAux [] t ++
     dsimp [getAppArgsAux]; rw [IHFn (args:=(s, arg) :: args), IHFn (args:=[(s, arg)])]
     rw [List.append_assoc]; rfl
 
-theorem LamTerm.maxEVarSucc_getAppArgsAux
+noncomputable def LamTerm.maxEVarSucc_getAppArgsAux
   (hs : HList (fun (_, arg) => arg.maxEVarSucc ≤ n) args) (ht : t.maxEVarSucc ≤ n) :
   HList (fun (_, arg) => arg.maxEVarSucc ≤ n) (LamTerm.getAppArgsAux args t) := by
   induction t generalizing args <;> try exact hs
@@ -3060,7 +3055,7 @@ def LamTerm.getAppArgs := getAppArgsAux []
 theorem LamTerm.getAppArgs_app : getAppArgs (.app s fn arg) = getAppArgs fn ++ [(s, arg)] := by
   dsimp [getAppArgs, getAppArgsAux]; rw [getAppArgsAux_eq]
 
-theorem LamTerm.maxEVarSucc_getAppArgs :
+noncomputable def LamTerm.maxEVarSucc_getAppArgs :
   HList (fun (_, arg) => arg.maxEVarSucc ≤ t.maxEVarSucc) (LamTerm.getAppArgs t) :=
   LamTerm.maxEVarSucc_getAppArgsAux .nil (Nat.le_refl _)
 
@@ -3117,7 +3112,7 @@ theorem LamTerm.getAppArgsNAux_eq : getAppArgsNAux n args t = (getAppArgsNAux n
       cases getAppArgsNAux n [] fn <;> dsimp
       rw [List.append_assoc]; rfl
 
-theorem LamTerm.maxEVarSucc_getAppArgsNAux
+def LamTerm.maxEVarSucc_getAppArgsNAux
   (hs : HList (fun (_, arg) => arg.maxEVarSucc ≤ m) args) (ht : t.maxEVarSucc ≤ m)
   (heq : LamTerm.getAppArgsNAux n args t = .some args') :
   HList (fun (_, arg) => arg.maxEVarSucc ≤ m) args' := by
@@ -3131,7 +3126,7 @@ theorem LamTerm.maxEVarSucc_getAppArgsNAux
 
 def LamTerm.getAppArgsN n := getAppArgsNAux n []
 
-theorem LamTerm.maxEVarSucc_getAppArgsN
+def LamTerm.maxEVarSucc_getAppArgsN
   (heq : LamTerm.getAppArgsN n t = .some l) :
   HList (fun (_, arg) => arg.maxEVarSucc ≤ t.maxEVarSucc) l :=
   LamTerm.maxEVarSucc_getAppArgsNAux .nil (Nat.le_refl _) heq
@@ -3193,7 +3188,7 @@ theorem LamTerm.getAppFnN_bvarAppsRev_length_eq
     cases l <;> cases heq
     case refl s' l =>
       rw [getAppFnN_succ']; dsimp [bvarAppsRev]
-      dsimp [Nat.add] at IH; rw [IH rfl]; rfl
+      rw [IH rfl]; rfl
 
 def LamTerm.getForallEFBody (t : LamTerm) : LamTerm :=
   match t with
@@ -3919,7 +3914,7 @@ def LamWF.ofLamCheck? {ltv : LamTyVal} :
   | .some (LamSort.base _), _ => intro contra; cases contra
   | .none, _ => intro contra; cases contra
 
-theorem LamWF.ofNonemptyLamWF (H : Nonempty (LamWF ltv ⟨lctx, t, s⟩)) :
+def LamWF.ofNonemptyLamWF (H : Nonempty (LamWF ltv ⟨lctx, t, s⟩)) :
   LamWF ltv ⟨lctx, t, s⟩ := by
   cases h₁ : LamTerm.lamCheck? ltv lctx t
   case none =>
@@ -4124,7 +4119,7 @@ theorem LamWF.interp_eqForallEFN'
   case nil =>
     dsimp [mkForallEFN, interp]
     conv =>
-      enter [2]; rw [IsomType.eqForall HList.nil_IsomType.{u + 1, u + 1, 0}]
+      enter [2]; rw [IsomType.eqForall HList.nil_IsomType.{0, u + 1, u + 1}]
       rw [PUnit.eqForall]; unfold HList.nil_IsomType; dsimp
       dsimp [pushLCtxs, pushLCtxsDep, Nat.blt, Nat.ble]
     apply congrArg; apply interp_substWF

Auto/Embedding/LamBitVec.lean

@@ -125,12 +125,13 @@ namespace BVLems
     case true =>
       rw [← Int.subNatNat_eq_coe, Int.subNatNat_of_lt (toNat_le _)]
       simp [BitVec.toInt, BitVec.ofInt]
-      have hzero : Nat.pred (2 ^ n - BitVec.toNat a) >>> i = 0 := by
+      have hzero : (2 ^ n - BitVec.toNat a - 1) >>> i = 0 := by
         rw [Nat.shiftRight_eq_div_pow]; apply (Nat.le_iff_div_eq_zero (Nat.two_pow_pos _)).mpr
-        rw [Nat.pred_lt_iff_le (Nat.two_pow_pos _)]
+        rw [Nat.sub_one, Nat.pred_lt_iff_le (Nat.two_pow_pos _)]
         apply Nat.le_trans (Nat.sub_le _ _) (Nat.pow_le_pow_of_le_right (.step .refl) h)
       apply eq_of_val_eq; rw [toNat_ofNatLt, hzero]
-      rw [toNat_neg, Int.mod_def', Int.emod]; dsimp; rw [Nat.zero_mod]
+      rw [toNat_neg, Int.mod_def', Int.emod]; dsimp only; rw [Nat.zero_mod]
+      dsimp only [Int.natAbs_ofNat, Nat.succ_eq_add_one, Nat.reduceAdd]
       rw [Int.subNatNat_of_sub_eq_zero ((Nat.sub_eq_zero_iff_le).mpr (Nat.two_pow_pos _))]
       rw [Int.toNat_ofNat, BitVec.toNat_ofNat]
       cases n <;> try rfl

Auto/Embedding/LamChecker.lean

@@ -362,7 +362,7 @@ def RTable.getValidsEnsureLCtx (r : RTable) (lctx : List LamSort) (vs : List Nat
     | .some (.nonempty _) => .none
     | .none => .none
 
-theorem RTable.getValidsEnsureLCtx_correct
+noncomputable def RTable.getValidsEnsureLCtx_correct
   (inv : RTable.inv r cv) (heq : getValidsEnsureLCtx r lctx vs = .some ts) :
   HList (fun t => LamThmValid cv.toLamValuation lctx t ∧ t.maxEVarSucc ≤ r.maxEVarSucc) ts := by
   induction vs generalizing ts

Auto/Embedding/LamConv.lean

@@ -152,7 +152,7 @@ theorem LamTerm.maxEVarSucc_etaExpandN? (heq : etaExpandN? n s t = .some t') :
   dsimp [etaExpandN?] at heq; cases h : s.getArgTysN n <;> rw [h] at heq <;> cases heq
   case refl l => rw [maxEVarSucc_etaExpandWith]
 
-theorem LamWF.etaExpandN?
+def LamWF.etaExpandN?
   (heq : LamTerm.etaExpandN? n s t = .some t') (wft : LamWF ltv ⟨lctx, t, s⟩) :
   LamWF ltv ⟨lctx, t', s⟩ := by
   dsimp [LamTerm.etaExpandN?] at heq; cases h₁ : s.getArgTysN n <;> rw [h₁] at heq <;> cases heq
@@ -164,7 +164,7 @@ theorem LamWF.etaExpandN?
     conv => arg 2; rw [seq]
     apply LamWF.etaExpandWith; rw [← seq]; exact wft
 
-theorem LamWF.fromEtaExpandN?
+def LamWF.fromEtaExpandN?
   (heq : LamTerm.etaExpandN? n s t = .some t') (wfEx : LamWF ltv ⟨lctx, t', s⟩) :
   LamWF ltv ⟨lctx, t, s⟩ := by
   dsimp [LamTerm.etaExpandN?] at heq; cases h₁ : s.getArgTysN n <;> rw [h₁] at heq <;> cases heq

Auto/Embedding/LamSystem.lean

@@ -266,11 +266,11 @@ theorem LamValid_substLCtxRecWF
     GLift.down (LamWF.interp (t:=t) (rty:=.base .prop) lval lctx' lctxTerm' ((@id (lctx' = lctx) (funext heq)) ▸ wf))) := by
   cases (@id (lctx' = lctx) (funext heq)); exact Iff.intro id id
 
-theorem LamWF.ofExistsLamWF (H : ∃ (_ : LamWF ltv ⟨lctx, t, s⟩), p) :
+def LamWF.ofExistsLamWF (H : ∃ (_ : LamWF ltv ⟨lctx, t, s⟩), p) :
   LamWF ltv ⟨lctx, t, s⟩ := by
   apply LamWF.ofNonemptyLamWF; cases H; apply Nonempty.intro; assumption
 
-theorem LamThmWF.ofLamThmWFP (H : LamThmWFP lval lctx s t) :
+def LamThmWF.ofLamThmWFP (H : LamThmWFP lval lctx s t) :
   LamThmWF lval lctx s t := by
   intro lctx'; apply LamWF.ofNonemptyLamWF (H lctx')
 
@@ -298,7 +298,7 @@ theorem LamTerm.lamThmWFCheck?_spec
     | false => intro H; cases H
   | .none => intro H; cases H
 
-theorem LamThmWF.ofLamThmWFCheck?
+def LamThmWF.ofLamThmWFCheck?
   {lctx : List LamSort} {rty : LamSort} {t : LamTerm}
   (h : LamTerm.lamThmWFCheck? lval.toLamTyVal lctx t = .some rty) : LamThmWF lval lctx rty t := by
   revert h; dsimp [LamTerm.lamThmWFCheck?]
@@ -317,7 +317,7 @@ theorem LamThmWF.ofLamThmWFCheck?
     | false => intro h; cases h
   | .none => intro h; cases h
 
-theorem LamThmWF.ofLamThmValid (H : LamThmValid lval lctx t) :
+def LamThmWF.ofLamThmValid (H : LamThmValid lval lctx t) :
   LamThmWF lval lctx (.base .prop) t :=
   LamThmWF.ofLamThmWFP (fun lctx => let ⟨wf, _⟩ := H lctx; Nonempty.intro wf)
 
@@ -359,7 +359,7 @@ theorem LamThmValid.maxLooseBVarSucc (H : LamThmValid lval lctx t) :
 theorem LamThmWFD.ofLamThmWF (H : LamThmWF lval lctx rty t) : LamThmWFD lval lctx rty t := by
   exists (H dfLCtxTy); apply LamThmWF.maxLooseBVarSucc H
 
-theorem LamThmWF.ofLamThmWFD (H : LamThmWFD lval lctx rty t) : LamThmWF lval lctx rty t := by
+def LamThmWF.ofLamThmWFD (H : LamThmWFD lval lctx rty t) : LamThmWF lval lctx rty t := by
   apply LamThmWF.ofLamThmWFP; have ⟨H, hSucc⟩ := H; apply LamThmWFP.ofLamThmWF
   intro lctx'; apply LamWF.lctxIrrelevance _ H; intros n hlt
   dsimp [pushLCtxs];
@@ -439,11 +439,11 @@ theorem LamThmValid.eVarIrrelevance
     hLamVarTy hLamILTy hTyVal hVarVal hILVal
     (by rw [hLCtxTy]) hirr (h lctx')
 
-theorem LamThmWF.ofLamThmEquiv_l (teq : LamThmEquiv lval lctx rty t₁ t₂) :
+def LamThmWF.ofLamThmEquiv_l (teq : LamThmEquiv lval lctx rty t₁ t₂) :
   LamThmWF lval lctx rty t₁ := LamThmWF.ofLamThmWFP (fun lctx' =>
     (let ⟨wf, _⟩ := teq lctx'; ⟨wf⟩))
 
-theorem LamThmWF.ofLamThmEquiv_r (teq : LamThmEquiv lval lctx rty t₁ t₂) :
+def LamThmWF.ofLamThmEquiv_r (teq : LamThmEquiv lval lctx rty t₁ t₂) :
   LamThmWF lval lctx rty t₂ := LamThmWF.ofLamThmWFP (fun lctx' =>
     (let ⟨_, ⟨wf, _⟩⟩ := teq lctx'; ⟨wf⟩))
 

Auto/LemDB.lean

@@ -47,8 +47,8 @@ partial def LemDB.toHashSet : LemDB → AttrM (HashSet Name)
       ret := ret.insertMany hset
     return ret
 
-private def throwUndeclaredLemDB (dbname action : Name) : AttrM α := do
-  let cmdstr := "#declare_lemdb " ++ dbname
+private def throwUndeclaredLemDB (dbname : Name) (action : String) : AttrM α := do
+  let cmdstr := "#declare_lemdb " ++ dbname.toString
   throwError ("Please declare lemma database using " ++
     s!"command {repr cmdstr} before {action}")
 

Auto/Lib/AbstractMVars.lean

@@ -98,7 +98,7 @@ partial def abstractExprMVars (e : Expr) : M Expr := do
             let type   ← abstractExprMVars decl.type
             let fvarId ← mkFreshFVarId
             let fvar := mkFVar fvarId;
-            let userName := if decl.userName.isAnonymous then (`x).appendIndexAfter (← get).fvars.size else decl.userName
+            let userName ← if decl.userName.isAnonymous then pure <| (`x).appendIndexAfter (← get).fvars.size else pure decl.userName
             modify fun s => {
               s with
               emap  := s.emap.insert mvarId fvar,
@@ -180,4 +180,4 @@ def abstractMVarsLambda (e : Expr) : MetaM AbstractMVarsResult := do
   setNGen s.ngen
   setMCtx s.mctx
   let e := s.lctx.mkLambda s.fvars e
-  pure { paramNames := s.paramNames, numMVars := s.fvars.size, expr := e }
+  pure { paramNames := s.paramNames, numMVars := s.fvars.size, expr := e }

Auto/Lib/BinTree.lean

@@ -26,7 +26,7 @@ private theorem wfAux (n n' : Nat) : n = n' + 2 → n / 2 < n := by
     apply Nat.succ_le_succ; apply Nat.zero_le
   case hLtK => apply Nat.le_refl
 
-theorem inductionOn.{u}
+def inductionOn.{u}
   {motive : Nat → Sort u} (x : Nat)
   (ind : ∀ x, motive ((x + 2) / 2) → motive (x + 2))
   (base₀ : motive 0) (base₁ : motive 1) : motive x :=
@@ -36,7 +36,7 @@ theorem inductionOn.{u}
   | x' + 2 => ind x' (inductionOn ((x' + 2) / 2) ind base₀ base₁)
 decreasing_by apply wfAux; rfl
 
-theorem induction.{u}
+def induction.{u}
   {motive : Nat → Sort u}
   (ind : ∀ x, motive ((x + 2) / 2) → motive (x + 2))
   (base₀ : motive 0) (base₁ : motive 1) : ∀ x, motive x :=

Auto/Lib/HList.lean

@@ -7,16 +7,16 @@ inductive HList (β : α → Sort _) : List α → Sort _
   | nil  : HList β .nil
   | cons : (x : β ty) → HList β tys → HList β (ty :: tys)
 
-theorem HList.nil_IsomType : IsomType (HList β .nil) PUnit :=
+def HList.nil_IsomType : IsomType (HList β .nil) PUnit :=
   ⟨fun _ => .unit, fun _ => .nil,
    fun x => match x with | .nil => rfl, fun _ => rfl⟩
 
-theorem HList.cons_IsomType : IsomType (HList β (a :: as)) (β a × HList β as) :=
+def HList.cons_IsomType : IsomType (HList β (a :: as)) (β a × HList β as) :=
   ⟨fun xs => match xs with | .cons x xs => (x, xs), fun (x, xs) => .cons x xs,
    fun xs => match xs with | .cons _ _ => rfl,
    fun (_, _) => rfl⟩
 
-theorem HList.singleton_IsomType : IsomType (HList β [a]) (β a) :=
+def HList.singleton_IsomType : IsomType (HList β [a]) (β a) :=
   ⟨fun xs => match xs with | .cons x .nil => x,
    fun x => .cons x .nil,
    fun xs => match xs with | .cons _ .nil => rfl,
@@ -129,14 +129,14 @@ theorem HList.append_get_append_eq (xs : HList β (as ++ bs)) :
     cases xs; case cons x xs =>
       dsimp [append_get_left, append_get_right, append]; rw [IH]
 
-theorem HList.append_IsomType {α : Type u} {β : α → Sort v} {xs ys : List α} :
+def HList.append_IsomType {α : Type u} {β : α → Sort v} {xs ys : List α} :
   IsomType (HList β (xs ++ ys)) (PProd (HList β xs) (HList β ys)) :=
   ⟨fun l => ⟨l.append_get_left, l.append_get_right⟩,
    fun ⟨l₁, l₂⟩ => HList.append l₁ l₂,
    HList.append_get_append_eq,
    fun ⟨l₁, l₂⟩ => by dsimp; congr; rw [append_get_left_eq]; rw [append_get_right_eq]⟩
 
-theorem HList.append_singleton_IsomType {α : Type u} {β : α → Sort v} {xs : List α} {x : α} :
+def HList.append_singleton_IsomType {α : Type u} {β : α → Sort v} {xs : List α} {x : α} :
   IsomType (HList β (xs ++ [x])) (PProd (HList β xs) (β x)) :=
   ⟨fun l => ⟨l.append_get_left, match l.append_get_right with | .cons x .nil => x⟩,
    fun ⟨l, e⟩ => HList.append l (.cons e .nil),

Auto/Lib/Pos.lean

@@ -49,7 +49,7 @@ def ofNat'WF (n : Nat) :=
     | _ => .xI (ofNat'WF (n / 2))
 decreasing_by rw [← h]; apply ofNat'WFAux; assumption
 
-theorem ofNat'WF.inductionOn.{u}
+def ofNat'WF.inductionOn.{u}
   {motive : Nat → Sort u} (x : Nat)
   (ind : ∀ x, motive ((x + 2) / 2) → motive (x + 2))
   (base₀ : motive 0) (base₁ : motive 1) : motive x :=
@@ -59,7 +59,7 @@ theorem ofNat'WF.inductionOn.{u}
   | x' + 2 => ind x' (inductionOn ((x' + 2) / 2) ind base₀ base₁)
 decreasing_by apply ofNat'WFAux; rfl
 
-theorem ofNat'WF.induction
+def ofNat'WF.induction
   {motive : Nat → Sort u}
   (ind : ∀ x, motive ((x + 2) / 2) → motive (x + 2))
   (base₀ : motive 0) (base₁ : motive 1) : ∀ x, motive x :=
@@ -100,6 +100,7 @@ theorem ofNat'WF.doubleSucc_xI (n : Nat) :
     have heq' : Nat.succ ((2 * n' + 3) / 2) = n' + 2 := by
       apply congrArg; rw [Nat.add_comm];
       rw [Nat.add_mul_div_left _ _ (by simp)]; rw [Nat.add_comm]
+    simp only [Nat.succ_eq_add_one] at heq'
     rw [heq']
 
 theorem ofNat'WF_toNat' (p : Pos) : ofNat'WF (toNat' p) = p := by

Auto/Solver/Native.lean

@@ -38,7 +38,7 @@ def emulateNative (lemmas : Array Lemma) : MetaM Expr := do
   let _ ← lemmas.mapM (fun lem => do
     if lem.params.size != 0 then
       throwError "Solver.emulateNative :: Universe levels parameters are not supported")
-  let descrs := lemmas.zipWithIndex.map (fun (lem, i) => (s!"lem{i}", lem.type, .default))
+  let descrs := lemmas.zipWithIndex.map (fun (lem, i) => (Name.mkSimple s!"lem{i}", lem.type, .default))
   let sty := Expr.mkForallFromBinderDescrs descrs (.const ``False [])
   let sorryExpr := Lean.mkApp2 (.const ``sorryAx [.zero]) sty (.const ``Bool.false [])
   return Lean.mkAppN sorryExpr (lemmas.map (fun lem => lem.proof))

Auto/Tactic.lean

@@ -133,7 +133,7 @@ def parseUOrDs (stxs : Array (TSyntax ``uord)) : TacticM (Array Prep.ConstUnfold
 
 def collectLctxLemmas (lctxhyps : Bool) (ngoalAndBinders : Array FVarId) : TacticM (Array Lemma) :=
   Meta.withNewMCtxDepth do
-    let fVarIds := (if lctxhyps then (← getLCtx).getFVarIds else ngoalAndBinders)
+    let fVarIds ← if lctxhyps then pure <| (← getLCtx).getFVarIds else pure ngoalAndBinders
     let mut lemmas := #[]
     for fVarId in fVarIds do
       let decl ← FVarId.getDecl fVarId