Theorem: false_context (BrownCs22/Demos/01-intro.lean)

State before:
p q r : Prop
⊢ 1 = 2 → 1 = 2
Tactic:
intro h12
State after:
p q r : Prop
h12 : 1 = 2
⊢ 1 = 2

State before:
p q r : Prop
h12 : 1 = 2
⊢ 1 = 2
Tactic:
exact h12
State after:
no goals