Theorem: example_1' (BrownCs22/Homework/Hw1.lean)

State before:
p : Prop
⊢ p → p → p
Tactic:
intro hp1
State after:
p : Prop
hp1 : p
⊢ p → p

State before:
p : Prop
hp1 : p
⊢ p → p
Tactic:
intro hp2
State after:
p : Prop
hp1 hp2 : p
⊢ p

State before:
p : Prop
hp1 hp2 : p
⊢ p
Tactic:
sorry
State after:
no goals