can't view multiple goals

Stream: general

[Kevin Buzzard]

This came up in teaching:

import tactic

-- First we do the question using Prop (optimised for proving)

variables (P Q R S U : Prop)

theorem trick {Q : Prop} (hQ : Q) : Q ↔ true :=
iff_of_true hQ trivial
theorem trick2 {Q : Prop} (hQ : ¬ Q) : Q ↔ false :=
iff_false_intro hQ
example : ∀ P Q R S U : Prop,
  ¬ (
(Q ∨ P ∨ U) ∧ (U ∨ ¬Q ∨ S) ∧ (U ∨ Q ∨ ¬R) ∧ (P ∨ R ∨ ¬S) ∧
(P ∨ S ∨ R) ∧ (R ∨ ¬U ∨ Q) ∧ (R ∨ S ∨ ¬U) ∧ (¬S ∨ ¬R ∨ U) ∧
(U ∨ ¬Q ∨ ¬R) ∧ (¬Q ∨ U ∨ ¬S) ∧ (¬P ∨ ¬R ∨ Q) ∧ (S ∨ ¬U ∨ ¬P) ∧
(¬R ∨ ¬P ∨ U) ∧ (S ∨ ¬R ∨ ¬U) ∧ (¬R ∨ ¬Q ∨ ¬S) ∧ (Q ∨ R ∨ S) ∧
(¬U ∨ P ∨ ¬Q) ∧ (R ∨ ¬Q ∨ ¬P) ∧ (P ∨ R ∨ ¬Q) ∧ (S ∨ P ∨ Q) ∧
(R ∨ P ∨ U) ∧ (¬U ∨ Q ∨ R) ∧ (¬U ∨ R ∨ ¬Q) ∧ (¬S ∨ ¬U ∨ ¬Q) ∧
(¬U ∨ ¬S ∨ R) ∧ (¬S ∨ P ∨ U) ∧ (P ∨ Q ∨ ¬R) ∧ (¬S ∨ ¬R ∨ U) ∧
(¬Q ∨ ¬S ∨ U) ∧ (P ∨ R ∨ ¬Q) ∧ (P ∨ Q ∨ ¬S) ∧ (U ∨ ¬S ∨ ¬P) ∧
(¬U ∨ R ∨ ¬P) ∧ (¬U ∨ P ∨ ¬Q) ∧ (¬R ∨ ¬P ∨ S) ∧ (R ∨ S ∨ ¬U) ∧
(P ∨ ¬U ∨ Q) ∧ (¬S ∨ R ∨ P) ∧ (¬P ∨ ¬Q ∨ ¬R) ∧ (¬P ∨ R ∨ ¬S)) :=
begin
  intros,
  by_cases hP : P;rw trick hP; try {rw iff_false_intro hP}; clear hP; simp;
  by_cases hP : Q;rw trick hP; try {rw iff_false_intro hP}; clear hP; simp; -- <- should be 4 goals here
  by_cases hP : R;rw trick hP; try {rw iff_false_intro hP}; clear hP; simp;
  by_cases hP : S;rw trick hP; try {rw iff_false_intro hP}; clear hP; simp;
  by_cases hP : U;rw trick hP; try {rw iff_false_intro hP}; clear hP; simp,
end

I wanted to inspect the goals part way through the proof, but I was surprised to find that changing the semicolon at the end of the second cases line of the proof to a comma still only let me see one goal -- I'm sure I've used this trick in the past to temporarily view multiple goals just to check things aren't going arwy in one of these crazy semicolony proofs.

[Kevin Buzzard]

PS one can check that there are four goals after the highlighted semicolon, because you can put sorry four times even though the infoview says there's only one goal.

[Bryan Gin-ge Chen]

I think this is discussed at the re-opened lean#201