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

Proof state:
case intro.h.hD
n : ℕ
IH :
  ∀ m < n,
    ∀ (D : Type u_1) [inst : DivisionRing D] [inst_1 : Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
⊢ ⟨y, hy⟩ ∈ Subring.center ↥R

Tactic:
let R_dr : DivisionRing R := Fintype.divisionRingOfIsDomain R

Result:
case intro.h.hD
n : ℕ
IH :
  ∀ m < n,
    ∀ (D : Type u_1) [inst : DivisionRing D] [inst_1 : Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
R_dr : DivisionRing ↥R := divisionRingOfIsDomain ↥R
⊢ ⟨y, hy⟩ ∈ Subring.center ↥R

Proof state:
n : ℕ
IH :
  ∀ m < n,
    ∀ (D : Type u_1) [inst : DivisionRing D] [inst_1 : Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
R_dr : DivisionRing ↥R := divisionRingOfIsDomain ↥R
⊢ card ↥R < card ↥⊤

Tactic:
convert Set.card_lt_card hR

Result:
no goals

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

Tactic:
induction' hn : Fintype.card D using Nat.strong_induction_on with n IH generalizing D

Result:
case intro.h
n : ℕ
IH :
  ∀ m < n,
    ∀ (D : Type u_1) [inst : DivisionRing D] [inst_1 : Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
⊢ Subring.center D = ⊤

Proof state:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
⊢ Subring.center D = ⊤

Tactic:
cases nonempty_fintype D

Result:
case intro
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
⊢ Subring.center D = ⊤

Proof state:
case intro.h
n : ℕ
IH :
  ∀ m < n,
    ∀ (D : Type u_1) [inst : DivisionRing D] [inst_1 : Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
⊢ Subring.center D = ⊤

Tactic:
apply InductionHyp.center_eq_top

Result:
case intro.h.hD
n : ℕ
IH :
  ∀ m < n,
    ∀ (D : Type u_1) [inst : DivisionRing D] [inst_1 : Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
⊢ LittleWedderburn.InductionHyp D

Proof state:
n : ℕ
IH :
  ∀ m < n,
    ∀ (D : Type u_1) [inst : DivisionRing D] [inst_1 : Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
this : ⟨y, hy⟩ ∈ Subring.center ↥R
⊢ x * y = y * x

Tactic:
rw [Subring.mem_center_iff] at this

Result:
n : ℕ
IH :
  ∀ m < n,
    ∀ (D : Type u_1) [inst : DivisionRing D] [inst_1 : Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
this : ∀ (g : ↥R), g * ⟨y, hy⟩ = ⟨y, hy⟩ * g
⊢ x * y = y * x

Proof state:
n : ℕ
IH :
  ∀ m < n,
    ∀ (D : Type u_1) [inst : DivisionRing D] [inst_1 : Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
R_dr : DivisionRing ↥R := divisionRingOfIsDomain ↥R
⊢ card ↥R < n

Tactic:
rw [← hn, ← Subring.card_top D]

Result:
n : ℕ
IH :
  ∀ m < n,
    ∀ (D : Type u_1) [inst : DivisionRing D] [inst_1 : Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
R_dr : DivisionRing ↥R := divisionRingOfIsDomain ↥R
⊢ card ↥R < card ↥⊤

Proof state:
case intro.h.hD
n : ℕ
IH :
  ∀ m < n,
    ∀ (D : Type u_1) [inst : DivisionRing D] [inst_1 : Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
R_dr : DivisionRing ↥R := divisionRingOfIsDomain ↥R
⊢ ⟨y, hy⟩ ∈ ⊤

Tactic:
trivial

Result:
no goals

Proof state:
case intro.h.hD
n : ℕ
IH :
  ∀ m < n,
    ∀ (D : Type u_1) [inst : DivisionRing D] [inst_1 : Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
⊢ LittleWedderburn.InductionHyp D

Tactic:
intro R hR x y hx hy

Result:
case intro.h.hD
n : ℕ
IH :
  ∀ m < n,
    ∀ (D : Type u_1) [inst : DivisionRing D] [inst_1 : Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
⊢ x * y = y * x

Proof state:
case intro.h.hD
n : ℕ
IH :
  ∀ m < n,
    ∀ (D : Type u_1) [inst : DivisionRing D] [inst_1 : Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
⊢ x * y = y * x

Tactic:
suffices (⟨y, hy⟩ : R) ∈ Subring.center R by
  rw [Subring.mem_center_iff] at this
  simpa using this ⟨x, hx⟩

Result:
case intro.h.hD
n : ℕ
IH :
  ∀ m < n,
    ∀ (D : Type u_1) [inst : DivisionRing D] [inst_1 : Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
⊢ ⟨y, hy⟩ ∈ Subring.center ↥R

Proof state:
n : ℕ
IH :
  ∀ m < n,
    ∀ (D : Type u_1) [inst : DivisionRing D] [inst_1 : Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
this : ∀ (g : ↥R), g * ⟨y, hy⟩ = ⟨y, hy⟩ * g
⊢ x * y = y * x

Tactic:
simpa using this ⟨x, hx⟩

Result:
no goals

Proof state:
case intro.h.hD
n : ℕ
IH :
  ∀ m < n,
    ∀ (D : Type u_1) [inst : DivisionRing D] [inst_1 : Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
R_dr : DivisionRing ↥R := divisionRingOfIsDomain ↥R
⊢ ⟨y, hy⟩ ∈ Subring.center ↥R

Tactic:
rw [IH (Fintype.card R) _ R inferInstance rfl]

Result:
case intro.h.hD
n : ℕ
IH :
  ∀ m < n,
    ∀ (D : Type u_1) [inst : DivisionRing D] [inst_1 : Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
R_dr : DivisionRing ↥R := divisionRingOfIsDomain ↥R
⊢ ⟨y, hy⟩ ∈ ⊤

n : ℕ
IH :
  ∀ m < n,
    ∀ (D : Type u_1) [inst : DivisionRing D] [inst_1 : Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
R_dr : DivisionRing ↥R := divisionRingOfIsDomain ↥R
⊢ card ↥R < n