_aux_Mathlib_Order_Filter_Defs___elabRules_Mathlib_Tactic_filterUpwards_1

Lean4
@[tactic Mathlib.Tactic.filterUpwards]
public meta def _aux_Mathlib_Order_Filter_Defs___elabRules_Mathlib_Tactic_filterUpwards_1 : Lean.Elab.Tactic.Tactic✝ :=
  fun
  | `(tactic| filter_upwards$[ [$[$args],*]]?$[ with $wth*]?$[ using $usingArg]?) => do
    focus do
        let config : ApplyConfig := { newGoals := ApplyNewGoals.nonDependentOnly }
        for e in args.getD #[] |>.reverse do
          let goal ← getMainGoal
          replaceMainGoal <|
              ←
                goal.withContext <|
                  runTermElab
                    (do
                      let m ← mkFreshExprMVar none
                      let lem ←
                        Term.elabTermEnsuringType (← ``(Filter.mp_mem $e $(← Term.exprToSyntax m))) (← goal.getType)
                      goal.assign lem
                      return [m.mvarId!])
        liftMetaTactic fun goal => do
            goal.apply (← mkConstWithFreshMVarLevels ``Filter.univ_mem') config
        evalTactic <| ← `(tactic| dsimp -zeta only [Set.mem_setOf_eq])
        if let some l := wth then
          evalTactic <| ← `(tactic| intro$[ $l]*)
        if let some e := usingArg then
          evalTactic <| ← `(tactic| exact $e)
  | _ => no_error_if_unused% throwUnsupportedSyntax✝
Похожие утверждения