-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.elabHeadersAux.eq_def : ∀ (views : Array Lean.Elab.Command.InductiveView) (i : ℕ) (acc : Array Lean.Elab.Command.PreElabHeaderResult),
  Lean.Elab.Command.elabHeadersAux✝ views i acc =
    Lean.Elab.Term.withAutoBoundImplicitForbiddenPred (fun n => views.any fun x => x.shortDeclName == n)
      (if h : i < views.size then
        have view := views[i];
        do
        let acc ←
          Lean.withRef view.ref
              (Lean.Elab.Term.withDeprecationContextFromAttrs view.modifiers.attrs
                (Lean.Elab.Term.withAutoBoundImplicit
                  (Lean.Elab.Term.elabBinders view.binders.getArgs fun params => do
                    let __x ←
                      Lean.Elab.Term.withAutoBoundImplicit do
                          let typeStx ←
                            view.type?.getDM do
                                let info ← Lean.MonadRef.mkInfoFromRefPos
                                let _ ← Lean.getCurrMacroScope
                                let _ ← Lean.MonadQuotation.getContext
                                pure
                                    {
                                        raw :=
                                          Lean.Syntax.node2 info `Lean.Parser.Term.sort (Lean.Syntax.atom info "Sort")
                                            (Lean.Syntax.node1 info `null
                                              (Lean.Syntax.node1 info `Lean.Parser.Level.hole
                                                (Lean.Syntax.atom info "_"))) }.raw
                          let type ← Lean.Elab.Term.elabType typeStx
                          Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing
                          let type ← Lean.instantiateMVars type
                          have inlayHintPos? : Option String.Pos.Raw :=
                            view.binders.getTailPos? true <|> view.declId.getTailPos? true
                          let indices ← Lean.Elab.Term.addAutoBoundImplicits #[] inlayHintPos?
                          let type ← liftM (Lean.Meta.mkForallFVars indices type)
                          have __do_jp : Unit → Lean.Elab.TermElabM (Lean.Expr × ℕ) := fun __r =>
                            pure (type, indices.size)
                          if view.allowIndices = true then do
                              let __do_lift ← liftM (Lean.Meta.isTypeFormerType type)
                              if __do_lift = true then __do_jp ()
                                else do
                                  let __r ←
                                    Lean.throwErrorAt typeStx
                                        (Lean.toMessageData
                                            "Invalid resulting type: Expected a sort or an indexed family of sorts" ++
                                          (Lean.toMessageData
                                              "Examples of valid sorts include `Type _`, `Sort _`, and `Prop`").hint')
                                  __do_jp __r
                            else do
                              let __do_lift ← liftM (Lean.Meta.whnfD type)
                              if __do_lift.isSort = true then __do_jp ()
                                else do
                                  let __r ←
                                    Lean.throwErrorAt typeStx
                                        (Lean.toMessageData "Invalid resulting type: Expected a sort" ++
                                          (Lean.toMessageData
                                              "Examples of valid sorts include `Type _`, `Sort _`, and `Prop`").hint')
                                  __do_jp __r
                    match __x with
                      | (type, snd) => do
                        let params ← Lean.Elab.Term.addAutoBoundImplicits params (view.declId.getTailPos? true)
                        have cls : Lean.Name := `Elab.inductive
                        let __do_lift ← Lean.isTracingEnabledFor cls
                        have __do_jp : Unit → Lean.Elab.TermElabM (Array Lean.Elab.Command.PreElabHeaderResult) :=
                          fun __r => do
                          let levelNames ← Lean.Elab.Term.getLevelNames
                          let type ← liftM (Lean.Meta.mkForallFVars params type)
                          pure
                              (acc.push
                                { view := view, levelNames := levelNames, numParams := params.size, type := type,
                                  origParams := params })
                        if __do_lift = true then do
                            let __r ←
                              Lean.addTrace cls
                                  (Lean.toMessageData "header params: " ++ Lean.toMessageData params ++
                                      Lean.toMessageData ", type: " ++
                                    Lean.toMessageData type)
                            __do_jp __r
                          else __do_jp ())))
        Lean.Elab.Command.elabHeadersAux✝ views (i + 1) acc
      else pure acc)