case intro
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
z : k
⊢ ∃ z_1, z ^ 2 = z_1 * z_1
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
⊢ ∃ z, x = z * z
rcases exists_pow_nat_eq x zero_lt_two with ⟨z, rfl⟩
no goals
case intro
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
z : k
⊢ ∃ z_1, z ^ 2 = z_1 * z_1
exact ⟨z, sq z⟩