case intro
R✝ : Type ?u.925715
R : Type u_1
inst✝³ : Finite R
inst✝² : CommRing R
inst✝¹ : IsReduced R
inst✝ : CharP R 2
a : R
val✝ : Fintype R
⊢ IsSquare a
R✝ : Type ?u.925715
R : Type u_1
inst✝³ : Finite R
inst✝² : CommRing R
inst✝¹ : IsReduced R
inst✝ : CharP R 2
a : R
⊢ IsSquare a
cases nonempty_fintype R
no goals
case intro
R✝ : Type ?u.925715
R : Type u_1
inst✝³ : Finite R
inst✝² : CommRing R
inst✝¹ : IsReduced R
inst✝ : CharP R 2
a : R
val✝ : Fintype R
⊢ IsSquare a
exact
  Exists.imp (fun b h => pow_two b ▸ Eq.symm h)
    (((Fintype.bijective_iff_injective_and_card _).mpr ⟨frobenius_inj R 2, rfl⟩).surjective a)