no goals
F : Type ?u.311
α : Type u_1
β : Type ?u.317
R : Type ?u.320
inst✝ : Mul α
a : α
x✝ : IsSquare (op a)
c : αᵐᵒᵖ
hc : op a = c * c
⊢ a = unop c * unop c
rw [← unop_mul, ← hc, unop_op]
no goals
F : Type ?u.311
α : Type u_1
β : Type ?u.317
R : Type ?u.320
inst✝ : Mul α
a : α
x✝ : IsSquare a
c : α
hc : a = c * c
⊢ IsSquare (op a)
simp [hc]