linter.style.multiGoal を紹介する

[Seasawher]

/--
warning: There are 2 unclosed goals before 'exact hP' and at least one remaining goal afterwards.
Please focus on the current goal, for instance using `·` (typed as "\.").
note: this linter can be disabled with `set_option linter.style.multiGoal false`
-/
#guard_msgs in
  set_option linter.style.multiGoal true in

  example {P Q : Prop} (hP : P) (hQ : Q) : P ∧ Q := by
    constructor
    exact hP
    exact hQ