And を分解できる `and_constructor` と withMainContext

elab "step_3" : tactic => do
  let mvarId ← getMainGoal
  let goalType : Q(Prop) ← getMainTarget

  -- ゴールの状態が a ∧ b という形になっている(And _ _ の形)ことを確認して、
  -- a と b に相当するものを取り出す
  let ~q($a ∧ $b) := goalType
    | throwError "Goal type is not of the form `a ∧ b`"

  let mvarId1 ← mkFreshExprMVarQ q($a) (userName := `left)
  let mvarId2 ← mkFreshExprMVarQ q($b) (userName := `right)

  mvarId.assign q(And.intro $mvarId1 $mvarId2)
  modify fun _ => { goals := [mvarId1.mvarId!, mvarId2.mvarId!] }

The issue provides a Lean tactic snippet that manually decomposes an And goal and mentions and_constructor and withMainContext. Start by locating the corresponding Lean example or documentation entry; clarify the intended change and consider the work done only when the requested explanation or example is specified and added.