awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (hypothesis)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
hD : InductionHyp D
val : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this : Field ↥Z := hD.field ⋯
q : ℕ := card.{u_1} ↥Z
card_Z : q = card.{u_1} ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key :
  HSub.hSub (α := ℤ) (↑q : ℤ) 1 + (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ) =
    HPow.hPow (α := ℤ) (↑q : ℤ) n - 1
i : ConjClasses Dˣ
x : Dˣ
hx : Membership.mem (γ := Set (ConjClasses Dˣ)) (ConjClasses.noncenter Dˣ) (ConjClasses.mk x)
Zx : Subring D := Subring.centralizer {(↑x : D)}
⊢ eval (↑q : ℤ) Φₙ ∣ (↑((q ^ n - 1) / card.{u_1} (↥Zx)ˣ) : ℤ)
have hZx : Zx ≠ ⊤
Tactic: have hZx : Zx ≠ ⊤ := by
    by_contra! hZx
    refine (ConjClasses.mk_bijOn (Dˣ)).mapsTo (Set.subset_center_units ?_) hx
    exact Subring.centralizer_eq_top_iff_subset.mp hZx <| Set.mem_singleton _
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (hypothesis)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
hD : InductionHyp D
val : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this_1 : Field ↥Z := hD.field ⋯
q : ℕ := card.{u_1} ↥Z
card_Z : q = card.{u_1} ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key :
  HSub.hSub (α := ℤ) (↑q : ℤ) 1 + (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ) =
    HPow.hPow (α := ℤ) (↑q : ℤ) n - 1
i : ConjClasses Dˣ
x : Dˣ
hx : Membership.mem (γ := Set (ConjClasses Dˣ)) (ConjClasses.noncenter Dˣ) (ConjClasses.mk x)
Zx : Subring D := Subring.centralizer {(↑x : D)}
hZx : Zx ≠ ⊤
this_2 : Field ↥Zx := hD.field ⋯
this : Algebra ↥Z ↥Zx := RingHom.toAlgebra (Subring.inclusion ⋯)
d : ℕ := finrank.{u_1, u_1} ↥Z ↥Zx
⊢ eval (↑q : ℤ) Φₙ ∣ (↑((q ^ n - 1) / card.{u_1} (↥Zx)ˣ) : ℤ)
have card_Zx : card.{u_1} ↥Zx = q ^ d
Tactic: have card_Zx : card Zx = q ^ d := Module.card_eq_pow_finrank
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
hD : InductionHyp D
val : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this_1 : Field ↥Z := hD.field ⋯
q : ℕ := card.{u_1} ↥Z
card_Z : q = card.{u_1} ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key :
  HSub.hSub (α := ℤ) (↑q : ℤ) 1 + (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ) =
    HPow.hPow (α := ℤ) (↑q : ℤ) n - 1
i : ConjClasses Dˣ
x : Dˣ
hx : Membership.mem (γ := Set (ConjClasses Dˣ)) (ConjClasses.noncenter Dˣ) (ConjClasses.mk x)
Zx : Subring D := Subring.centralizer {(↑x : D)}
hZx : Zx ≠ ⊤
this_2 : Field ↥Zx := hD.field ⋯
this : Algebra ↥Z ↥Zx := RingHom.toAlgebra (Subring.inclusion ⋯)
d : ℕ := finrank.{u_1, u_1} ↥Z ↥Zx
card_Zx : card.{u_1} ↥Zx = q ^ d
⊢ 1 ≤ q ^ d
have rw : 1 ≤ card.{u_1} ↥Zx
Tactic: rw [← card_Zx]
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (hypothesis)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
hD : InductionHyp D
val : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this_1 : Field ↥Z := hD.field ⋯
q : ℕ := card.{u_1} ↥Z
card_Z : q = card.{u_1} ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key :
  HSub.hSub (α := ℤ) (↑q : ℤ) 1 + (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ) =
    HPow.hPow (α := ℤ) (↑q : ℤ) n - 1
i : ConjClasses Dˣ
x : Dˣ
hx : Membership.mem (γ := Set (ConjClasses Dˣ)) (ConjClasses.noncenter Dˣ) (ConjClasses.mk x)
Zx : Subring D := Subring.centralizer {(↑x : D)}
hZx : Zx ≠ ⊤
this_2 : Field ↥Zx := hD.field ⋯
this : Algebra ↥Z ↥Zx := RingHom.toAlgebra (Subring.inclusion ⋯)
d : ℕ := finrank.{u_1, u_1} ↥Z ↥Zx
card_Zx : card.{u_1} ↥Zx = q ^ d
⊢ eval (↑q : ℤ) Φₙ ∣ (↑((q ^ n - 1) / card.{u_1} (↥Zx)ˣ) : ℤ)
have h1qd : 1 ≤ q ^ d
Tactic: have h1qd : 1 ≤ q ^ d := by rw [← card_Zx]; exact card_pos
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (hypothesis)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
hD : InductionHyp D
val : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this_1 : Field ↥Z := hD.field ⋯
q : ℕ := card.{u_1} ↥Z
card_Z : q = card.{u_1} ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key :
  HSub.hSub (α := ℤ) (↑q : ℤ) 1 + (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ) =
    HPow.hPow (α := ℤ) (↑q : ℤ) n - 1
i : ConjClasses Dˣ
x : Dˣ
hx : Membership.mem (γ := Set (ConjClasses Dˣ)) (ConjClasses.noncenter Dˣ) (ConjClasses.mk x)
Zx : Subring D := Subring.centralizer {(↑x : D)}
hZx : Zx ≠ ⊤
this_2 : Field ↥Zx := hD.field ⋯
this : Algebra ↥Z ↥Zx := RingHom.toAlgebra (Subring.inclusion ⋯)
d : ℕ := finrank.{u_1, u_1} ↥Z ↥Zx
card_Zx : card.{u_1} ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
⊢ eval (↑q : ℤ) Φₙ ∣ (↑((q ^ n - 1) / card.{u_1} (↥Zx)ˣ) : ℤ)
have this₁ : IsScalarTower (↥Z) (↥Zx) D
Tactic: haveI : IsScalarTower Z Zx D := ⟨fun x y z ↦ mul_assoc _ _ _⟩
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
hD : InductionHyp D
val : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this_1 : Field ↥Z := hD.field ⋯
q : ℕ := card.{u_1} ↥Z
card_Z : q = card.{u_1} ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key :
  HSub.hSub (α := ℤ) (↑q : ℤ) 1 + (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ) =
    HPow.hPow (α := ℤ) (↑q : ℤ) n - 1
i : ConjClasses Dˣ
x : Dˣ
hx : Membership.mem (γ := Set (ConjClasses Dˣ)) (ConjClasses.noncenter Dˣ) (ConjClasses.mk x)
Zx : Subring D := Subring.centralizer {(↑x : D)}
hZx : Zx ≠ ⊤
this_2 : Field ↥Zx := hD.field ⋯
this_3 : Algebra ↥Z ↥Zx := RingHom.toAlgebra (Subring.inclusion ⋯)
d : ℕ := finrank.{u_1, u_1} ↥Z ↥Zx
card_Zx : card.{u_1} ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
this : IsScalarTower (↥Z) (↥Zx) D
⊢ eval (↑q : ℤ) Φₙ ∣ (↑((q ^ n - 1) / card.{u_1} (↥Zx)ˣ) : ℤ)
have intro : eval (↑q : ℤ) Φₙ ∣ (↑((q ^ n - 1) / (q ^ d - 1)) : ℤ)
Tactic: rw [card_units, card_Zx]
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
hD : InductionHyp D
val : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this_1 : Field ↥Z := hD.field ⋯
q : ℕ := card.{u_1} ↥Z
card_Z : q = card.{u_1} ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key :
  HSub.hSub (α := ℤ) (↑q : ℤ) 1 + (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ) =
    HPow.hPow (α := ℤ) (↑q : ℤ) n - 1
i : ConjClasses Dˣ
x : Dˣ
hx : Membership.mem (γ := Set (ConjClasses Dˣ)) (ConjClasses.noncenter Dˣ) (ConjClasses.mk x)
Zx : Subring D := Subring.centralizer {(↑x : D)}
hZx : Zx ≠ ⊤
this_2 : Field ↥Zx := hD.field ⋯
this_3 : Algebra ↥Z ↥Zx := RingHom.toAlgebra (Subring.inclusion ⋯)
d : ℕ := finrank.{u_1, u_1} ↥Z ↥Zx
card_Zx : card.{u_1} ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
this : IsScalarTower (↥Z) (↥Zx) D
⊢ eval (↑q : ℤ) Φₙ ∣ (↑((q ^ n - 1) / (q ^ d - 1)) : ℤ)
have intro : eval (↑q : ℤ) Φₙ ∣ (HPow.hPow (α := ℤ) (↑q : ℤ) n - 1) / (HPow.hPow (α := ℤ) (↑q : ℤ) d - 1)
Tactic: push_cast [h1qd, h1qn]
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
hD : InductionHyp D
val : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this_1 : Field ↥Z := hD.field ⋯
q : ℕ := card.{u_1} ↥Z
card_Z : q = card.{u_1} ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key :
  HSub.hSub (α := ℤ) (↑q : ℤ) 1 + (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ) =
    HPow.hPow (α := ℤ) (↑q : ℤ) n - 1
i : ConjClasses Dˣ
x : Dˣ
hx : Membership.mem (γ := Set (ConjClasses Dˣ)) (ConjClasses.noncenter Dˣ) (ConjClasses.mk x)
Zx : Subring D := Subring.centralizer {(↑x : D)}
hZx : Zx ≠ ⊤
this_2 : Field ↥Zx := hD.field ⋯
this_3 : Algebra ↥Z ↥Zx := RingHom.toAlgebra (Subring.inclusion ⋯)
d : ℕ := finrank.{u_1, u_1} ↥Z ↥Zx
card_Zx : card.{u_1} ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
this : IsScalarTower (↥Z) (↥Zx) D
⊢ eval (↑q : ℤ) Φₙ ∣ (HPow.hPow (α := ℤ) (↑q : ℤ) n - 1) / (HPow.hPow (α := ℤ) (↑q : ℤ) d - 1)
have intro : (HPow.hPow (α := ℤ) (↑q : ℤ) d - 1) * eval (↑q : ℤ) Φₙ ∣ HPow.hPow (α := ℤ) (↑q : ℤ) n - 1
Tactic: apply Int.dvd_div_of_mul_dvd
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (hypothesis)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
hD : InductionHyp D
val : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this_1 : Field ↥Z := hD.field ⋯
q : ℕ := card.{u_1} ↥Z
card_Z : q = card.{u_1} ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key :
  HSub.hSub (α := ℤ) (↑q : ℤ) 1 + (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ) =
    HPow.hPow (α := ℤ) (↑q : ℤ) n - 1
i : ConjClasses Dˣ
x : Dˣ
hx : Membership.mem (γ := Set (ConjClasses Dˣ)) (ConjClasses.noncenter Dˣ) (ConjClasses.mk x)
Zx : Subring D := Subring.centralizer {(↑x : D)}
hZx : Zx ≠ ⊤
this_2 : Field ↥Zx := hD.field ⋯
this_3 : Algebra ↥Z ↥Zx := RingHom.toAlgebra (Subring.inclusion ⋯)
d : ℕ := finrank.{u_1, u_1} ↥Z ↥Zx
card_Zx : card.{u_1} ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
this : IsScalarTower (↥Z) (↥Zx) D
⊢ (HPow.hPow (α := ℤ) (↑q : ℤ) d - 1) * eval (↑q : ℤ) Φₙ ∣ HPow.hPow (α := ℤ) (↑q : ℤ) n - 1
have aux : ∀ {k : ℕ}, eval (↑q : ℤ) (HPow.hPow (α := ℤ[X]) X k - 1) = HPow.hPow (α := ℤ) (↑q : ℤ) k - 1
Tactic: have aux : ∀ {k : ℕ}, ((X : ℤ[X]) ^ k - 1).eval ↑q = (q : ℤ) ^ k - 1 := by
    simp only [eval_X, eval_one, eval_pow, eval_sub, forall_const]
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
hD : InductionHyp D
val : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this_1 : Field ↥Z := hD.field ⋯
q : ℕ := card.{u_1} ↥Z
card_Z : q = card.{u_1} ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key :
  HSub.hSub (α := ℤ) (↑q : ℤ) 1 + (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ) =
    HPow.hPow (α := ℤ) (↑q : ℤ) n - 1
i : ConjClasses Dˣ
x : Dˣ
hx : Membership.mem (γ := Set (ConjClasses Dˣ)) (ConjClasses.noncenter Dˣ) (ConjClasses.mk x)
Zx : Subring D := Subring.centralizer {(↑x : D)}
hZx : Zx ≠ ⊤
this_2 : Field ↥Zx := hD.field ⋯
this_3 : Algebra ↥Z ↥Zx := RingHom.toAlgebra (Subring.inclusion ⋯)
d : ℕ := finrank.{u_1, u_1} ↥Z ↥Zx
card_Zx : card.{u_1} ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
this : IsScalarTower (↥Z) (↥Zx) D
aux : ∀ {k : ℕ}, eval (↑q : ℤ) (HPow.hPow (α := ℤ[X]) X k - 1) = HPow.hPow (α := ℤ) (↑q : ℤ) k - 1
⊢ (HPow.hPow (α := ℤ) (↑q : ℤ) d - 1) * eval (↑q : ℤ) Φₙ ∣ HPow.hPow (α := ℤ) (↑q : ℤ) n - 1
have intro : eval (↑q : ℤ) ((HPow.hPow (α := ℤ[X]) X d - 1) * Φₙ) ∣ eval (↑q : ℤ) (HPow.hPow (α := ℤ[X]) X n - 1)
Tactic: rw [← aux, ← aux, ← eval_mul]
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
hD : InductionHyp D
val : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this_1 : Field ↥Z := hD.field ⋯
q : ℕ := card.{u_1} ↥Z
card_Z : q = card.{u_1} ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key :
  HSub.hSub (α := ℤ) (↑q : ℤ) 1 + (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ) =
    HPow.hPow (α := ℤ) (↑q : ℤ) n - 1
i : ConjClasses Dˣ
x : Dˣ
hx : Membership.mem (γ := Set (ConjClasses Dˣ)) (ConjClasses.noncenter Dˣ) (ConjClasses.mk x)
Zx : Subring D := Subring.centralizer {(↑x : D)}
hZx : Zx ≠ ⊤
this_2 : Field ↥Zx := hD.field ⋯
this_3 : Algebra ↥Z ↥Zx := RingHom.toAlgebra (Subring.inclusion ⋯)
d : ℕ := finrank.{u_1, u_1} ↥Z ↥Zx
card_Zx : card.{u_1} ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
this : IsScalarTower (↥Z) (↥Zx) D
aux : ∀ {k : ℕ}, eval (↑q : ℤ) (HPow.hPow (α := ℤ[X]) X k - 1) = HPow.hPow (α := ℤ) (↑q : ℤ) k - 1
⊢ eval (↑q : ℤ) ((HPow.hPow (α := ℤ[X]) X d - 1) * Φₙ) ∣ eval (↑q : ℤ) (HPow.hPow (α := ℤ[X]) X n - 1)
have intro : d ∈ n.properDivisors
Tactic: refine map_dvd (evalRingHom ↑q) (X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd ℤ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
hD : InductionHyp D
val : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this_1 : Field ↥Z := hD.field ⋯
q : ℕ := card.{u_1} ↥Z
card_Z : q = card.{u_1} ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key :
  HSub.hSub (α := ℤ) (↑q : ℤ) 1 + (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ) =
    HPow.hPow (α := ℤ) (↑q : ℤ) n - 1
i : ConjClasses Dˣ
x : Dˣ
hx : Membership.mem (γ := Set (ConjClasses Dˣ)) (ConjClasses.noncenter Dˣ) (ConjClasses.mk x)
Zx : Subring D := Subring.centralizer {(↑x : D)}
hZx : Zx ≠ ⊤
this_2 : Field ↥Zx := hD.field ⋯
this_3 : Algebra ↥Z ↥Zx := RingHom.toAlgebra (Subring.inclusion ⋯)
d : ℕ := finrank.{u_1, u_1} ↥Z ↥Zx
card_Zx : card.{u_1} ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
this : IsScalarTower (↥Z) (↥Zx) D
aux : ∀ {k : ℕ}, eval (↑q : ℤ) (HPow.hPow (α := ℤ[X]) X k - 1) = HPow.hPow (α := ℤ) (↑q : ℤ) k - 1
⊢ d ∈ n.properDivisors
have intro : d < n
Tactic: refine Nat.mem_properDivisors.mpr ⟨⟨_, (finrank_mul_finrank Z Zx D).symm⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
hD : InductionHyp D
val : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this_1 : Field ↥Z := hD.field ⋯
q : ℕ := card.{u_1} ↥Z
card_Z : q = card.{u_1} ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key :
  HSub.hSub (α := ℤ) (↑q : ℤ) 1 + (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ) =
    HPow.hPow (α := ℤ) (↑q : ℤ) n - 1
i : ConjClasses Dˣ
x : Dˣ
hx : Membership.mem (γ := Set (ConjClasses Dˣ)) (ConjClasses.noncenter Dˣ) (ConjClasses.mk x)
Zx : Subring D := Subring.centralizer {(↑x : D)}
hZx : Zx ≠ ⊤
this_2 : Field ↥Zx := hD.field ⋯
this_3 : Algebra ↥Z ↥Zx := RingHom.toAlgebra (Subring.inclusion ⋯)
d : ℕ := finrank.{u_1, u_1} ↥Z ↥Zx
card_Zx : card.{u_1} ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
this : IsScalarTower (↥Z) (↥Zx) D
aux : ∀ {k : ℕ}, eval (↑q : ℤ) (HPow.hPow (α := ℤ[X]) X k - 1) = HPow.hPow (α := ℤ) (↑q : ℤ) k - 1
⊢ d < n
have intro : card.{u_1} ↥Zx < card D
Tactic: rw [← Nat.pow_lt_pow_iff_right hq, ← card_D, ← card_Zx]
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
hD : InductionHyp D
val : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this_1 : Field ↥Z := hD.field ⋯
q : ℕ := card.{u_1} ↥Z
card_Z : q = card.{u_1} ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key :
  HSub.hSub (α := ℤ) (↑q : ℤ) 1 + (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ) =
    HPow.hPow (α := ℤ) (↑q : ℤ) n - 1
i : ConjClasses Dˣ
x : Dˣ
hx : Membership.mem (γ := Set (ConjClasses Dˣ)) (ConjClasses.noncenter Dˣ) (ConjClasses.mk x)
Zx : Subring D := Subring.centralizer {(↑x : D)}
hZx : Zx ≠ ⊤
this_2 : Field ↥Zx := hD.field ⋯
this_3 : Algebra ↥Z ↥Zx := RingHom.toAlgebra (Subring.inclusion ⋯)
d : ℕ := finrank.{u_1, u_1} ↥Z ↥Zx
card_Zx : card.{u_1} ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
this : IsScalarTower (↥Z) (↥Zx) D
aux : ∀ {k : ℕ}, eval (↑q : ℤ) (HPow.hPow (α := ℤ[X]) X k - 1) = HPow.hPow (α := ℤ) (↑q : ℤ) k - 1
⊢ card.{u_1} ↥Zx < card D
have intro : ∀ (b : D) (hb : b ∉ Zx), card.{u_1} ↥Zx < card D
Tactic: obtain ⟨b, -, hb⟩ := SetLike.exists_of_lt hZx.lt_top
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
hD : InductionHyp D
val : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this_1 : Field ↥Z := hD.field ⋯
q : ℕ := card.{u_1} ↥Z
card_Z : q = card.{u_1} ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key :
  HSub.hSub (α := ℤ) (↑q : ℤ) 1 + (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ) =
    HPow.hPow (α := ℤ) (↑q : ℤ) n - 1
i : ConjClasses Dˣ
x : Dˣ
hx : Membership.mem (γ := Set (ConjClasses Dˣ)) (ConjClasses.noncenter Dˣ) (ConjClasses.mk x)
Zx : Subring D := Subring.centralizer {(↑x : D)}
hZx : Zx ≠ ⊤
this_2 : Field ↥Zx := hD.field ⋯
this_3 : Algebra ↥Z ↥Zx := RingHom.toAlgebra (Subring.inclusion ⋯)
d : ℕ := finrank.{u_1, u_1} ↥Z ↥Zx
card_Zx : card.{u_1} ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
this : IsScalarTower (↥Z) (↥Zx) D
aux : ∀ {k : ℕ}, eval (↑q : ℤ) (HPow.hPow (α := ℤ[X]) X k - 1) = HPow.hPow (α := ℤ) (↑q : ℤ) k - 1
b : D
hb : b ∉ Zx
⊢ card.{u_1} ↥Zx < card D
have intro : b ∉ Set.range (ι := ↥Zx) (Subtype.val (p := fun (x : D) ↦ x ∈ Zx))
Tactic: refine card_lt_of_injective_of_notMem _ Subtype.val_injective (?_ : b ∉ _)
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
⊢ Eq (α := Subring D) (Subring.center D) ⊤
have intro : ∀ (val : Fintype D), Eq (α := Subring D) (Subring.center D) ⊤
Tactic: cases nonempty_fintype D
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
val : Fintype D
⊢ Eq (α := Subring D) (Subring.center D) ⊤
have 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) ⊤
Tactic: induction hn : Fintype.card D using Nat.strong_induction_on generalizing D with | _ n IH
Cleared hypotheses: D, inst, inst_1, val
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (goal)
Goal:
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
inst_1 : Finite D
val : Fintype D
hn : card D = n
⊢ Eq (α := Subring D) (Subring.center D) ⊤
have intro : InductionHyp D
Tactic: apply InductionHyp.center_eq_top
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (hypothesis)
Goal:
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
inst_1 : Finite D
val : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
this : Membership.mem (γ := Subring ↥R) (Subring.center ↥R) (Subtype.mk (p := fun (x : D) ↦ x ∈ R) y hy)
⊢ x * y = y * x
have this₁ : ∀ (g : ↥R), g * Subtype.mk (p := fun (x : D) ↦ x ∈ R) y hy = Subtype.mk (p := fun (x : D) ↦ x ∈ R) y hy * g
Tactic: rw [Subring.mem_center_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (goal)
Goal:
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
inst_1 : 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
have intro : Membership.mem (γ := Subring ↥R) (Subring.center ↥R) (Subtype.mk (p := fun (x : D) ↦ x ∈ R) y hy)
Tactic: suffices (⟨y, hy⟩ : R) ∈ Subring.center R by
    rw [Subring.mem_center_iff] at this
    simpa using this ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (goal)
Goal:
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
inst_1 : 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
⊢ Membership.mem (γ := Subring ↥R) (Subring.center ↥R) (Subtype.mk (p := fun (x : D) ↦ x ∈ R) y hy)
have intro : Membership.mem (γ := Subring ↥R) ⊤ (Subtype.mk (p := fun (x : D) ↦ x ∈ R) y hy)
Tactic: rw [IH (Fintype.card R) _ R inferInstance rfl]
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (goal)
Goal:
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
inst_1 : 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
intro : Membership.mem (γ := Subring ↥R) ⊤ (Subtype.mk (p := fun (x : D) ↦ x ∈ R) y hy)
⊢ Membership.mem (γ := Subring ↥R) (Subring.center ↥R) (Subtype.mk (p := fun (x : D) ↦ x ∈ R) y hy)
have rw : card.{u_1} ↥R < n
Tactic: rw [IH (Fintype.card R) _ R inferInstance rfl]
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (goal)
Goal:
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
inst_1 : 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.{u_1} ↥R < n
have rw : card.{u_1} ↥R < card.{u_1} ↥⊤
Tactic: rw [← hn, ← Subring.card_top D]
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
⊢ Eq (α := Subring D) (Subring.center D) ⊤
have intro : ∀ (val : Fintype D), Eq (α := Subring D) (Subring.center D) ⊤
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
-- 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) ⊤
⊢ Eq (α := Subring D) (Subring.center D) ⊤
have 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) ⊤
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