letI : Fintype { x // x ∈ MulAction.stabilizer (ConjAct Rˣ)
      (ConjClasses.exists_rep A|>.choose) } := Fintype.ofFinite _
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
this : Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) := Set.fintypeRange fun m => m • ⋯.choose
⊢ 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
this✝ : Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) := Set.fintypeRange fun m => m • ⋯.choose
this : Fintype ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose) :=
  Fintype.ofFinite ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↑{⋯.choose}.centralizer