Theorem: LoVe.proof_of_False (LoVe/Lectures/LoVe05_FunctionalProgramming_Demo.lean)

State before:
hi : immoral 0 = immoral 0 + 1
⊢ immoral 0 - immoral 0 = immoral 0 + 1 - immoral 0
Tactic:
rw [←hi]
State after:
no goals

State before:
hi : immoral 0 = immoral 0 + 1
him : immoral 0 - immoral 0 = immoral 0 + 1 - immoral 0
⊢ 0 = 1
Tactic:
simp at him
State after:
no goals

State before:
hi : immoral 0 = immoral 0 + 1
him : immoral 0 - immoral 0 = immoral 0 + 1 - immoral 0
h0eq1 : 0 = 1
⊢ False
Tactic:
simp at h0eq1
State after:
no goals