Theorem: Cpdt.Chapter3.true_neq_false (Cpdt/Chapter3/ManualConstructors.lean)

State before:
⊢ true ≠ false
Tactic:
intro h
State after:
h : true = false
⊢ False

State before:
h : true = false
⊢ False
Tactic:
rw [←Bool.toProp_false]
State after:
h : true = false
⊢ Bool.toProp false

State before:
h : true = false
⊢ Bool.toProp false
Tactic:
rw [←h]
State after:
h : true = false
⊢ Bool.toProp true

State before:
h : true = false
⊢ Bool.toProp true
Tactic:
rw [Bool.toProp_true]
State after:
h : true = false
⊢ True

State before:
h : true = false
⊢ True
Tactic:
exact True.intro
State after:
no goals