exact
  setFintype
    {A |
      let_fun this := finclassa A;
      Fintype.card ↑(ConjClasses.carrier A) > 1}
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
n : ℕ
H : ∃ x y, x ≠ y
h_n : n ≠ 0
q : ℕ := Fintype.card ↥Z
h_card : Fintype.card R = q ^ n
finclassa : (A : ConjClasses Rˣ) → Fintype ↑A.carrier
this : (A : ConjClasses Rˣ) → Fintype ↑{Quotient.out' A}.centralizer
A : ConjClasses Rˣ
⊢ Fintype
    ↑{A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1}
no goals