Theorem: HW2.problem_2 (BrownCs22/Homework/Hw2sols.lean)

State before:
⊢ 5 ∣ 15
Tactic:
existsi 3
State after:
⊢ 15 = 5 * 3

State before:
⊢ 15 = 5 * 3
Tactic:
numbers
State after:
no goals