-- Mathlib/RingTheory/LittleWedderburn.lean
theorem center_eq_top [Finite D] (hD : InductionHyp D) : Subring.center D = ⊤

Proof state:
case intro.h.mk.h
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : LittleWedderburn.InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝² : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
hZx : Zx ≠ ⊤
this✝¹ : Field ↥Zx := hD.field ⋯
this✝ : Algebra ↥Z ↥Zx := (Subring.inclusion ⋯).toAlgebra
d : ℕ := finrank ↥Z ↥Zx
card_Zx : card ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
this : IsScalarTower (↥Z) (↥Zx) D
aux : ∀ {k : ℕ}, eval (↑q) (X ^ k - 1) = ↑q ^ k - 1
⊢ (↑q ^ d - 1) * eval (↑q) Φₙ ∣ ↑q ^ n - 1

Tactic:
rw [← aux, ← aux, ← eval_mul]

Result:
case intro.h.mk.h
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : LittleWedderburn.InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝² : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
hZx : Zx ≠ ⊤
this✝¹ : Field ↥Zx := hD.field ⋯
this✝ : Algebra ↥Z ↥Zx := (Subring.inclusion ⋯).toAlgebra
d : ℕ := finrank ↥Z ↥Zx
card_Zx : card ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
this : IsScalarTower (↥Z) (↥Zx) D
aux : ∀ {k : ℕ}, eval (↑q) (X ^ k - 1) = ↑q ^ k - 1
⊢ eval (↑q) ((X ^ d - 1) * Φₙ) ∣ eval (↑q) (X ^ n - 1)

Proof state:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : LittleWedderburn.InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
⊢ Zx ≠ ⊤

Tactic:
by_contra! hZx

Result:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : LittleWedderburn.InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
hZx : Zx = ⊤
⊢ False

Proof state:
case intro.h.mk
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : LittleWedderburn.InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
hZx : Zx ≠ ⊤
⊢ eval (↑q) Φₙ ∣ ↑((q ^ n - 1) / card (↥Zx)ˣ)

Tactic:
letI : Field Zx := hD.field hZx.lt_top

Result:
case intro.h.mk
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : LittleWedderburn.InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝ : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
hZx : Zx ≠ ⊤
this : Field ↥Zx := hD.field ⋯
⊢ eval (↑q) Φₙ ∣ ↑((q ^ n - 1) / card (↥Zx)ˣ)

Proof state:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : LittleWedderburn.InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝ : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
this : eval (↑q) Φₙ ∣ ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card)
contra : eval (↑q) Φₙ ∣ ↑q - 1
⊢ False

Tactic:
refine (Nat.le_of_dvd ?_ ?_).not_lt (sub_one_lt_natAbs_cyclotomic_eval (n := n) ?_ hq.ne')

Result:
case refine_1
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : LittleWedderburn.InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝ : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
this : eval (↑q) Φₙ ∣ ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card)
contra : eval (↑q) Φₙ ∣ ↑q - 1
⊢ 0 < q - 1

case refine_2
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : LittleWedderburn.InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝ : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
this : eval (↑q) Φₙ ∣ ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card)
contra : eval (↑q) Φₙ ∣ ↑q - 1
⊢ (eval (↑q) (cyclotomic n ℤ)).natAbs ∣ q - 1

case refine_3
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : LittleWedderburn.InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝ : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
this : eval (↑q) Φₙ ∣ ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card)
contra : eval (↑q) Φₙ ∣ ↑q - 1
⊢ 1 < n

Proof state:
case intro
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : LittleWedderburn.InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
⊢ eval (↑q) Φₙ ∣ ∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, ↑x.carrier.toFinset.card

Tactic:
apply Finset.dvd_sum

Result:
case intro.h
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : LittleWedderburn.InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
⊢ ∀ i ∈ (ConjClasses.noncenter Dˣ).toFinset, eval (↑q) Φₙ ∣ ↑i.carrier.toFinset.card