all_goals
all_goals
は、後に続くタクティクをすべてのゴールに対して適用します。
variable (P Q : Prop)
example (hP : P) (hQ : Q) : P ∧ Q := by
-- `P` と `Q` をそれぞれ示せばよい
constructor
-- どちらも仮定から従うので、
-- 両方に `assumption` を適用する
all_goals assumption
all_goals
には、タクティクブロックを渡すこともできます。
example {R : Prop} (hnP : ¬ P) : (P → R) ∧ (P → Q) := by
constructor
all_goals
intro h
contradiction
タクティク結合子 <;>
によってもほぼ同じことができます。
example (hP : P) (hQ : Q) : P ∧ Q := by
constructor <;> assumption