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

State before:
m n : ℕ
⊢ 2 * m + n = m + m + n
Tactic:
rw [Nat.two_mul]
State after:
no goals

State before:
m n : ℕ
hmul : 2 * m + n = m + m + n
⊢ m + m + n = m + n + m
Tactic:
ac_rfl
State after:
no goals