Theorem: tst3 (reading/tactic.lean)

State before:
p q : Prop
⊢ p → q → p
Tactic:
intros h1 h2
State after:
p q : Prop
h1 : p
h2 : q
⊢ p

State before:
p q : Prop
h1 : p
h2 : q
⊢ p
Tactic:
assumption
State after:
no goals