Theorem: LoVe.ForwardProofs.add_comm_zero_left_by_exact (LoVe/Lectures/LoVe04_ForwardProofs_Demo.lean)

State before:
n : ℕ
⊢ add 0 n = add n 0
Tactic:
exact add_comm 0 n
State after:
no goals