From 8aa375ba3e5c0e3eb4108d8f3e08be1122a2d189 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 3 Aug 2020 17:47:24 -0700
Subject: [PATCH] fix: bug at `FVarSubst` generation

---
 src/Lean/Meta/Tactic/Induction.lean | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/Tactic/Induction.lean b/src/Lean/Meta/Tactic/Induction.lean
index d43c4ef6ee..6c26af38ed 100644
--- a/src/Lean/Meta/Tactic/Induction.lean
+++ b/src/Lean/Meta/Tactic/Induction.lean
@@ -103,7 +103,7 @@ private partial def finalizeAux
           (extra,  mvarId') ← introN mvarId' nextra [] false;
           let subst := reverted.size.fold
             (fun i (subst : FVarSubst) =>
-              if i ≤ indices.size + 1 then subst
+              if i < indices.size + 1 then subst
               else
                 let revertedFVarId := reverted.get! i;
                 let newFVarId      := extra.get! (i - indices.size - 1);
@@ -173,6 +173,7 @@ withMVarContext mvarId $ do
     (majorFVarId', mvarId) ← intro1 mvarId false;
     -- Create FVarSubst with indices
     let baseSubst : FVarSubst := indices.iterate {} (fun i index subst => subst.insert index.fvarId! (indices'.get! i.val));
+    trace! `Meta.Tactic.induction ("after revert&intro" ++ Format.line ++ MessageData.ofGoal mvarId);
     -- Update indices and major
     let indices := indices'.map mkFVar;
     let majorFVarId := majorFVarId';
@@ -209,5 +210,8 @@ withMVarContext mvarId $ do
         | _ =>
          throwTacticEx `induction mvarId "major premise is not of the form (C ...)"
 
+@[init] private def regTraceClasses : IO Unit := do
+registerTraceClass `Meta.Tactic.induction
+
 end Meta
 end Lean