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

⊢ Even 1

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