case intro
F : Type ?u.14072
α : Type u_1
β : Type ?u.14078
R : Type ?u.14081
inst✝ : Monoid α
a✝ : α
n : ℕ
a : α
⊢ IsSquare (a ^ (n + n))
F : Type ?u.14072
α : Type u_1
β : Type ?u.14078
R : Type ?u.14081
inst✝ : Monoid α
n : ℕ
a : α
⊢ Even n → ∀ (a : α), IsSquare (a ^ n)
rintro ⟨n, rfl⟩ a
no goals
case intro
F : Type ?u.14072
α : Type u_1
β : Type ?u.14078
R : Type ?u.14081
inst✝ : Monoid α
a✝ : α
n : ℕ
a : α
⊢ IsSquare (a ^ (n + n))
exact ⟨a ^ n, pow_add _ _ _⟩