Theorem: problem3 (BrownCs22/Exercises/submission.lean)

State before:
⊢ ∃ n, 12 * n = 84
Tactic:
existsi 7
State after:
⊢ 12 * 7 = 84

State before:
⊢ 12 * 7 = 84
Tactic:
norm_num
State after:
no goals