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

State before:
⊢ Even 4 ∧ Even 7 ∧ Even 3 ∧ Even 0
Tactic:
intro_and_even
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.left

⊢ Even 3
Tactic:
sorry
State after:
no goals