Theorem: LoVe.any_goals_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 apply Even.add_two
State after:
case left.a

⊢ Even 2

case right.left.a

⊢ Even 5

case right.right.left.a

⊢ Even 1

case right.right.right

⊢ Even 0

State before:
case left.a

⊢ Even 2

case right.left.a

⊢ Even 5

case right.right.left.a

⊢ Even 1

case right.right.right

⊢ Even 0
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.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:
sorry
State after:
no goals