## Stream: general

### Topic: can't view multiple goals

#### Kevin Buzzard (Oct 10 2020 at 21:47):

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 (Oct 10 2020 at 21:50):

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 (Oct 10 2020 at 22:15):

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

Last updated: May 12 2021 at 04:19 UTC