mathlib3

a8629a59 - refactor(tactic/interactive): use 1-indexing in work_on_goal (#11813)

refactor(tactic/interactive): use 1-indexing in work_on_goal (#11813) Backporting the change in https://github.com/leanprover-community/mathlib4/pull/178 to make `work_on_goal` 1-indexed. See also: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60work_on_goal.60.20vs.20.60swap.60 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>