Theorem: LoVe.any_goals_solve_repeat_first_example (LoVe/Lectures/LoVe08_Metaprogramming_Demo.lean)

State before:
⊢ Even 4 ∧ Even 7 ∧ Even 3 ∧ Even 0
Tactic:
repeat' apply And.intro
State after:
case left

⊢ Even 4

case right.left

⊢ Even 7

case right.right.left

⊢ Even 3

case right.right.right

⊢ Even 0

State before:
case left

⊢ Even 4

case right.left

⊢ Even 7

case right.right.left

⊢ Even 3

case right.right.right

⊢ Even 0
Tactic:
any_goals
  solve
  | repeat'
      first
      | apply Even.add_two
      | apply Even.zero
State after:
case right.left

⊢ Even 7

case right.right.left

⊢ Even 3

State before:
case right.left

⊢ Even 7

case right.right.left

⊢ Even 3
Tactic:
repeat' sorry
State after:
no goals

State before:
case right.right

⊢ Even 3 ∧ Even 0
Tactic:
apply And.intro
State after:
case right.right.left

⊢ Even 3

case right.right.right

⊢ Even 0

State before:
case right.right.right

⊢ Even 0
Tactic:
solve
| repeat'
    first
    | apply Even.add_two
    | apply Even.zero
State after:
no goals

State before:
case right.right.right

⊢ Even 0
Tactic:
repeat'
  first
  | apply Even.add_two
  | apply Even.zero
State after:
no goals

State before:
case right.right.right

⊢ Even 0
Tactic:
first
| apply Even.add_two
| apply Even.zero
State after:
no goals

State before:
case right.right.left

⊢ Even 3
Tactic:
apply Even.add_two
State after:
case right.right.left.a

⊢ Even 1

State before:
case right.right.right

⊢ Even 0
Tactic:
apply Even.zero
State after:
no goals

State before:
case right.right.left

⊢ Even 3
Tactic:
sorry
State after:
no goals