letI := Fintype.ofFinite (Set.centralizer {ConjClasses.exists_rep A|>.choose})
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↑{⋯.choose}.centralizer
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↑{⋯.choose}.centralizer