case refine'_1
F : Type ?u.32005
α : Type u_1
β : Type ?u.32011
R : Type ?u.32014
inst✝ : DivisionMonoid α
a : α
h : IsSquare a⁻¹
⊢ IsSquare a

case refine'_2
F : Type ?u.32005
α : Type u_1
β : Type ?u.32011
R : Type ?u.32014
inst✝ : DivisionMonoid α
a : α
h : IsSquare a
⊢ IsSquare a⁻¹
F : Type ?u.32005
α : Type u_1
β : Type ?u.32011
R : Type ?u.32014
inst✝ : DivisionMonoid α
a : α
⊢ IsSquare a⁻¹ ↔ IsSquare a
refine' ⟨fun h => _, fun h => _⟩
case refine'_1
F : Type ?u.32005
α : Type u_1
β : Type ?u.32011
R : Type ?u.32014
inst✝ : DivisionMonoid α
a : α
h : IsSquare a⁻¹
⊢ IsSquare (op a⁻¹⁻¹)
case refine'_1
F : Type ?u.32005
α : Type u_1
β : Type ?u.32011
R : Type ?u.32014
inst✝ : DivisionMonoid α
a : α
h : IsSquare a⁻¹
⊢ IsSquare a
rw [← isSquare_op_iff, ← inv_inv a]
no goals
case refine'_1
F : Type ?u.32005
α : Type u_1
β : Type ?u.32011
R : Type ?u.32014
inst✝ : DivisionMonoid α
a : α
h : IsSquare a⁻¹
⊢ IsSquare (op a⁻¹⁻¹)
exact h.map (MulEquiv.inv' α)
no goals
case refine'_2
F : Type ?u.32005
α : Type u_1
β : Type ?u.32011
R : Type ?u.32014
inst✝ : DivisionMonoid α
a : α
h : IsSquare a
⊢ IsSquare a⁻¹
exact ((isSquare_op_iff a).mpr h).map (MulEquiv.inv' α).symm