-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
intro : ∀ (val : Fintype D), Eq (α := Subring D) (Subring.center D) ⊤
intro₁ :
  ∀ (n : ℕ)
    (IH :
      ∀ m < n,
        ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D) (hn : card D = m),
          Eq (α := Subring D) (Subring.center D) ⊤)
    (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D) (hn : card D = n),
    Eq (α := Subring D) (Subring.center D) ⊤
intro₂ :
  ∀ (n : ℕ)
    (IH :
      ∀ m < n,
        ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D) (hn : card D = m),
          Eq (α := Subring D) (Subring.center D) ⊤)
    (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D) (hn : card D = n), InductionHyp D
intro₃ :
  ∀ (n : ℕ)
    (IH :
      ∀ m < n,
        ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D) (hn : card D = m),
          Eq (α := Subring D) (Subring.center D) ⊤)
    (D : Type u_1) [inst : DivisionRing D] [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
intro₄ :
  ∀ (n : ℕ)
    (IH :
      ∀ m < n,
        ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D) (hn : card D = m),
          Eq (α := Subring D) (Subring.center D) ⊤)
    (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D) (hn : card D = n) {R : Subring D} (hR : R < ⊤)
    ⦃x y : D⦄ (hx : x ∈ R) (hy : y ∈ R),
    Membership.mem (γ := Subring ↥R) (Subring.center ↥R) (Subtype.mk (p := fun (x : D) ↦ x ∈ R) y hy)
intro₅ :
  ∀ (n : ℕ)
    (IH :
      ∀ m < n,
        ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D) (hn : card D = m),
          Eq (α := Subring D) (Subring.center D) ⊤)
    (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D) (hn : card D = n) {R : Subring D} (hR : R < ⊤)
    ⦃x y : D⦄ (hx : x ∈ R) (hy : y ∈ R),
    Membership.mem (γ := Subring ↥R) (Subring.center ↥R) (Subtype.mk (p := fun (x : D) ↦ x ∈ R) y hy)
intro₆ :
  ∀ (n : ℕ)
    (IH :
      ∀ m < n,
        ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D) (hn : card D = m),
          Eq (α := Subring D) (Subring.center D) ⊤)
    (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D) (hn : card D = n) {R : Subring D} (hR : R < ⊤)
    ⦃x y : D⦄ (hx : x ∈ R) (hy : y ∈ R),
    let R_dr : DivisionRing ↥R := divisionRingOfIsDomain ↥R;
    Membership.mem (γ := Subring ↥R) ⊤ (Subtype.mk (p := fun (x : D) ↦ x ∈ R) y hy)
⊢ Eq (α := Subring D) (Subring.center D) ⊤
have cases : ∀ (n : ℕ)
  (IH :
    ∀ m < n,
      ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D) (hn : card D = m),
        Eq (α := Subring D) (Subring.center D) ⊤)
  (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D) (hn : card D = n) {R : Subring D} (hR : R < ⊤)
  ⦃x y : D⦄ (hx : x ∈ R) (hy : y ∈ R), card.{u_1} ↥R < n
Tactic: classical
  cases nonempty_fintype D
  induction hn : Fintype.card D using Nat.strong_induction_on generalizing D with | _ n IH
  apply InductionHyp.center_eq_top
  intro R hR x y hx hy
  suffices (⟨y, hy⟩ : R) ∈ Subring.center R by
    rw [Subring.mem_center_iff] at this
    simpa using this ⟨x, hx⟩
  let R_dr : DivisionRing R := Fintype.divisionRingOfIsDomain R
  rw [IH (Fintype.card R) _ R inferInstance rfl]
  · trivial
  rw [← hn, ← Subring.card_top D]
  convert! Set.card_lt_card hR
Cleared hypotheses: D, inst, inst_1