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

State before:
a : ℚ
h : ∃ b, a = b ^ 2
⊢ a ≥ 0
Tactic:
cases' h with b hb
State after:
case intro
a b : ℚ
hb : a = b ^ 2
⊢ a ≥ 0

State before:
case intro
a b : ℚ
hb : a = b ^ 2
⊢ a ≥ 0
Tactic:
calc a = b ^ 2 := hb
_ ≥ 0 := by apply sq_nonneg
State after:
no goals

State before:
a b : ℚ
hb : a = b ^ 2
⊢ b ^ 2 ≥ 0
Tactic:
apply sq_nonneg
State after:
no goals