Theorem: one_eq_two (Lectures/NatRec.lean)

State before:
⊢ 1 = 2
Tactic:
let e := wrong 1
State after:
e : Empty := wrong 1
⊢ 1 = 2

State before:
e : Empty := wrong 1
⊢ 1 = 2
Tactic:
let h := vac_contra e 1
State after:
e : Empty := wrong 1
h : wrong 1 = e → 1 = 2 := vac_contra e 1
⊢ 1 = 2

State before:
e : Empty := wrong 1
h : wrong 1 = e → 1 = 2 := vac_contra e 1
⊢ 1 = 2
Tactic:
apply h
State after:
e : Empty := wrong 1
h : wrong 1 = e → 1 = 2 := vac_contra e 1
⊢ wrong 1 = e

State before:
e : Empty := wrong 1
h : wrong 1 = e → 1 = 2 := vac_contra e 1
⊢ wrong 1 = e
Tactic:
rfl
State after:
no goals