chore: remove unnecessary explicit indexing proofs (#185)

Aesop/Builder/Forward.lean

@@ -60,7 +60,7 @@ def getImmediatePremises  (type : Expr) (pat? : Option RulePattern)
       for h : i in [:args.size] do
         if isPatternInstantiated i then
           continue
-        let fvarId := (args[i]'h.2).fvarId!
+        let fvarId := args[i].fvarId!
         let ldecl ← fvarId.getDecl
         let isNondep : MetaM Bool :=
           args.allM (start := i + 1) λ arg => do

Aesop/RulePattern.lean

@@ -144,7 +144,7 @@ def openRuleType (pat : RulePattern) (inst : RulePatternInstantiation)
   let mut assigned := ∅
   for h : i in [:mvars.size] do
     if let some inst ← pat.getInstantiation inst i then
-      let mvarId := mvars[i]'h.2 |>.mvarId!
+      let mvarId := mvars[i] |>.mvarId!
       -- We use `isDefEq` to make sure that universe metavariables occurring in
       -- the type of `mvarId` are assigned.
       if ← isDefEq (.mvar mvarId) inst then
@@ -163,7 +163,7 @@ def specializeRule (pat : RulePattern) (inst : RulePatternInstantiation)
         if let some inst ← pat.getInstantiation inst i then
           args := args.push $ some inst
         else
-          let fvarId := fvarIds[i]'h.2
+          let fvarId := fvarIds[i]
           args := args.push $ some fvarId
           remainingFVarIds := remainingFVarIds.push fvarId
       let result ← mkLambdaFVars remainingFVarIds (← mkAppOptM' rule args)
@@ -207,7 +207,7 @@ where
     let e := s.lctx.mkLambda s.fvars e
     let mut mvarIdToPos := ∅
     for h : i in [:s.fvars.size] do
-      let name := s.lctx.get! (s.fvars[i]'h.2).fvarId! |>.userName
+      let name := s.lctx.get! (s.fvars[i]).fvarId! |>.userName
       mvarIdToPos := mvarIdToPos.insert ⟨name⟩ i
     let result :=
       { paramNames := s.paramNames, numMVars := s.fvars.size, expr := e }

Aesop/RuleTac/Forward.lean

@@ -33,7 +33,7 @@ partial def makeForwardHyps (e : Expr) (pat? : Option RulePattern)
     let mut instMVars := Array.mkEmpty argMVars.size
     let mut immediateMVars := Array.mkEmpty argMVars.size
     for h : i in [:argMVars.size] do
-      let mvarId := argMVars[i]'h.2 |>.mvarId!
+      let mvarId := argMVars[i].mvarId!
       if patInstantiatedMVars.contains mvarId then
         continue
       if immediate.contains i then

Aesop/Script/StructureDynamic.lean

@@ -60,7 +60,7 @@ def DynStructureM.run (x : DynStructureM α) (script : UScript) :
     MetaM (α × Bool) := do
   let mut steps : PHashMap MVarId (Nat × Step) := {}
   for h : i in [:script.size] do
-    let step := script[i]'h.2
+    let step := script[i]
     steps := steps.insert step.preGoal (i, step)
   let (a, s) ← ReaderT.run x { steps } |>.run {}
   return (a, s.perfect)

Aesop/Script/StructureStatic.lean

@@ -22,7 +22,7 @@ protected def StaticStructureM.run (script : UScript) (x : StaticStructureM α)
     CoreM (α × Bool) := do
   let mut steps : Std.HashMap MVarId (Nat × Step) := Std.HashMap.empty script.size
   for h : i in [:script.size] do
-    let step := script[i]'h.2
+    let step := script[i]
     if h : step.postGoals.size = 1 then
       if step.postGoals[0].goal == step.preGoal then
         continue

Aesop/Script/Util.lean

@@ -18,7 +18,7 @@ def findFirstStep? {α β : Type} (goals : Array α) (step? : α → Option β)
      (stepOrder : β → Nat) : Option (Nat × α × β) := Id.run do
   let mut firstStep? := none
   for h : pos in [:goals.size] do
-    let g := goals[pos]'h.2
+    let g := goals[pos]
     if let some step := step? g then
       if let some (_, _, currentFirstStep) := firstStep? then
         if stepOrder step < stepOrder currentFirstStep then

Aesop/Search/Expansion.lean

@@ -69,7 +69,7 @@ def addRapps (parentRef : GoalRef) (rule : RegularRule)
   let mut rrefs := Array.mkEmpty rapps.size
   let mut subgoals := Array.mkEmpty $ rapps.size * 3
   for h : i in [:rapps.size] do
-    let rapp := rapps[i]'h.2
+    let rapp := rapps[i]
     let successProbability :=
       parent.successProbability *
       (rapp.successProbability?.getD rule.successProbability)