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

State before:
a b : ℚ
h1 : a - b = 4
h2 : a * b = 1
⊢ (a + b) ^ 2 = (a - b) ^ 2 + 4 * (a * b)
Tactic:
ring
State after:
no goals

State before:
a b : ℚ
h1 : a - b = 4
h2 : a * b = 1
⊢ (a - b) ^ 2 + 4 * (a * b) = 4 ^ 2 + 4 * 1
Tactic:
rw [h1, h2]
State after:
no goals

State before:
a b : ℚ
h1 : a - b = 4
h2 : a * b = 1
⊢ 4 ^ 2 + 4 * 1 = 20
Tactic:
ring
State after:
no goals