case intro
R✝ : Type ?u.39609
G : Type ?u.39612
inst✝⁵ : Ring R✝
inst✝⁴ : IsDomain R✝
inst✝³ : Fintype R✝
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Finite R
val✝ : Fintype R
⊢ IsField R
R✝ : Type ?u.39609
G : Type ?u.39612
inst✝⁵ : Ring R✝
inst✝⁴ : IsDomain R✝
inst✝³ : Fintype R✝
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Finite R
⊢ IsField R
cases nonempty_fintype R
no goals
case intro
R✝ : Type ?u.39609
G : Type ?u.39612
inst✝⁵ : Ring R✝
inst✝⁴ : IsDomain R✝
inst✝³ : Fintype R✝
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Finite R
val✝ : Fintype R
⊢ IsField R
exact @Field.toIsField R (@Fintype.fieldOfDomain R _ _ (Classical.decEq R) _)