Theorem: LoVe.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:
repeat'
  first
  | apply Even.add_two
  | apply Even.zero
State after:
case right.left.a.a.a

⊢ Even 1

case right.right.left.a

⊢ Even 1

State before:
case right.left.a.a.a

⊢ Even 1

case right.right.left.a

⊢ Even 1
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:
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.a

⊢ Even 1
Tactic:
sorry
State after:
no goals