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

Proof state:
case h.e'_4
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
⊢ q - 1 = (↑q - 1).natAbs

Tactic:
clear_value q

Result:
case h.e'_4
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 ⋯
n : ℕ := finrank (↥Z) D
Φₙ : ℤ[X] := cyclotomic n ℤ
q : ℕ
card_Z : q = card ↥Z
hq : 1 < q
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ 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
⊢ q - 1 = (↑q - 1).natAbs

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}
hZx : Zx ≠ ⊤
this✝ : Field ↥Zx := hD.field ⋯
this : Algebra ↥Z ↥Zx := (Subring.inclusion ⋯).toAlgebra
d : ℕ := finrank ↥Z ↥Zx
card_Zx : card ↥Zx = q ^ d
⊢ 1 ≤ card ↥Zx

Tactic:
exact card_pos

Result:
no goals

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 : Quot.mk (⇑(IsConj.setoid Dˣ)) x ∈ (ConjClasses.noncenter Dˣ).toFinset
⊢ eval (↑q) Φₙ ∣ ↑(ConjClasses.carrier (Quot.mk (⇑(IsConj.setoid Dˣ)) x)).toFinset.card

Tactic:
simp (config := {zeta := false}) only [ConjClasses.quot_mk_eq_mk, Set.mem_toFinset] at hx ⊢

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ˣ
⊢ eval (↑q) Φₙ ∣ ↑(ConjClasses.mk x).carrier.toFinset.card

Proof state:
case intro
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : LittleWedderburn.InductionHyp D
val✝ : Fintype D
⊢ Subring.center D = ⊤

Tactic:
set Z := Subring.center D

Result:
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
⊢ Z = ⊤

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 ≠ ⊤
⊢ False

Tactic:
letI : Field Z := hD.field hZ.lt_top

Result:
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 ⋯
⊢ False

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
key : q - 1 + ∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card = q ^ n - 1
Φₙ : ℤ[X] := cyclotomic n ℤ
⊢ False

Tactic:
apply_fun (Nat.cast : ℕ → ℤ) at key

Result:
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)
⊢ False

Proof state:
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

Tactic:
by_contra! h

Result:
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
h : n ≤ 1
⊢ False

Proof state:
case refine_3.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
this : eval (↑q) Φₙ ∣ ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card)
contra : eval (↑q) Φₙ ∣ ↑q - 1
h : n ≤ 1
x : D
hx : ∀ (w : D), ∃ c, c • x = w
y : D
x✝ : y ∈ ⊤
z : D
⊢ z * y = y * z

Tactic:
obtain ⟨r, rfl⟩ := hx y

Result:
case refine_3.intro.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
this : eval (↑q) Φₙ ∣ ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card)
contra : eval (↑q) Φₙ ∣ ↑q - 1
h : n ≤ 1
x : D
hx : ∀ (w : D), ∃ c, c • x = w
z : D
r : ↥Z
x✝ : r • x ∈ ⊤
⊢ z * r • x = r • x * z