A variant of `t1 <;> t2` that fails if `<…>` isn't needed?

Stream: new members

[Louis Cabarion]

1. Is there a variant of t₁ <;> t₂ that fails if t₁ by itself would close the goal?
2. Is there a variant of t₁ <;> t₂ that fails if t₁; t₂ by itself would close the goal?

#mwe which shows four examples where in the last three variants have "extra tactics" that are silently ignored:

example : (1 + 2 = 3 ∧ 2 + 3 = 5) ∧ (3 + 4 = 7 ∧ 4 + 5 = 9) := by
  constructor <;> constructor <;> rfl
example : (1 + 2 = 3 ∧ 2 + 3 = 5) ∧ (3 + 4 = 7 ∧ 4 + 5 = 9) := by
  constructor <;> constructor <;> rfl <;> rfl
example : (1 + 2 = 3 ∧ 2 + 3 = 5) ∧ (3 + 4 = 7 ∧ 4 + 5 = 9) := by
  constructor <;> constructor <;> rfl <;> skip
example : (1 + 2 = 3 ∧ 2 + 3 = 5) ∧ (3 + 4 = 7 ∧ 4 + 5 = 9) := by
  constructor <;> constructor <;> rfl <;> fail

[Damiano Testa]

I think that mathlib has a linter that tells you about these things.

[Damiano Testa]

With import Mathlib, the last three emit a warning.

[Louis Cabarion]

Thanks @Damiano Testa.

The other case is covered by the linter.unnecessarySeqFocus linter:

import Mathlib
example (x y : Nat) (h₁ : x = 1) (h₂ : y = 2): x + y = 3 := by
  rw [h₁] <;> rw [h₂]
-- Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice
-- Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`