Theorem: test_reverse_goals (lean/main/09_tactics.lean)

State before:
⊢ (1 = 2 ∧ 3 = 4) ∧ 5 = 6
Tactic:
constructor
State after:
case left

⊢ 1 = 2 ∧ 3 = 4

case right

⊢ 5 = 6

State before:
case left

⊢ 1 = 2 ∧ 3 = 4

case right

⊢ 5 = 6
Tactic:
constructor
State after:
case left.left

⊢ 1 = 2

case left.right

⊢ 3 = 4

case right

⊢ 5 = 6

State before:
case left.left

⊢ 1 = 2

case left.right

⊢ 3 = 4

case right

⊢ 5 = 6
Tactic:
reverse_goals
State after:
case right

⊢ 5 = 6

case left.right

⊢ 3 = 4

case left.left

⊢ 1 = 2

State before:
case right

⊢ 5 = 6

case left.right

⊢ 3 = 4

case left.left

⊢ 1 = 2
Tactic:
all_goals sorry
State after:
no goals

State before:
case left.left

⊢ 1 = 2
Tactic:
sorry
State after:
no goals