Theorem: test_and_then (lean/main/09_tactics.lean)

State before:
⊢ 1 = 1 ∧ 2 = 2
Tactic:
apply And.intro and_then rfl
State after:
no goals