awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LittleWedderburn
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
⊢ IsScalarTower (↥Z) (↥Zx) D

Tactic:
haveI : IsScalarTower Z Zx D := ⟨fun x y z ↦ mul_assoc _ _ _⟩
-- Module: Mathlib.RingTheory.LittleWedderburn
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
intro : eval (↑q : ℤ) Φₙ ∣ (↑((q ^ n - 1) / (q ^ d - 1)) : ℤ)
⊢ eval (↑q : ℤ) Φₙ ∣ (↑((q ^ n - 1) / card.{u_1} (↥Zx)ˣ) : ℤ)

Tactic:
rw [card_units, card_Zx]

Premises used: Fintype.card_units
-- Module: Mathlib.RingTheory.LittleWedderburn
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
intro : eval (↑q : ℤ) Φₙ ∣ (HPow.hPow (α := ℤ) (↑q : ℤ) n - 1) / (HPow.hPow (α := ℤ) (↑q : ℤ) d - 1)
⊢ eval (↑q : ℤ) Φₙ ∣ (↑((q ^ n - 1) / (q ^ d - 1)) : ℤ)

Tactic:
push_cast [h1qd, h1qn]
-- Module: Mathlib.RingTheory.LittleWedderburn
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
intro : (HPow.hPow (α := ℤ) (↑q : ℤ) d - 1) * eval (↑q : ℤ) Φₙ ∣ HPow.hPow (α := ℤ) (↑q : ℤ) n - 1
⊢ eval (↑q : ℤ) Φₙ ∣ (HPow.hPow (α := ℤ) (↑q : ℤ) n - 1) / (HPow.hPow (α := ℤ) (↑q : ℤ) d - 1)

Tactic:
apply Int.dvd_div_of_mul_dvd

Premises used: Int.dvd_div_of_mul_dvd
-- Module: Mathlib.RingTheory.LittleWedderburn
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
⊢ ∀ {k : ℕ}, eval (↑q : ℤ) (HPow.hPow (α := ℤ[X]) X k - 1) = HPow.hPow (α := ℤ) (↑q : ℤ) k - 1

Tactic:
simp only [eval_X, eval_one, eval_pow, eval_sub, forall_const]

Premises used: Polynomial.eval_X, Polynomial.eval_pow, Polynomial.eval_one, forall_const, Polynomial.eval_sub
-- Module: Mathlib.RingTheory.LittleWedderburn
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
⊢ ∀ {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]
-- Module: Mathlib.RingTheory.LittleWedderburn
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
intro : eval (↑q : ℤ) ((HPow.hPow (α := ℤ[X]) X d - 1) * Φₙ) ∣ eval (↑q : ℤ) (HPow.hPow (α := ℤ[X]) X n - 1)
⊢ (HPow.hPow (α := ℤ) (↑q : ℤ) d - 1) * eval (↑q : ℤ) Φₙ ∣ HPow.hPow (α := ℤ) (↑q : ℤ) n - 1

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

Premises used: Polynomial.eval_mul
-- Module: Mathlib.RingTheory.LittleWedderburn
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)

Tactic:
map_dvd (evalRingHom ↑q) (X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd ℤ ?_)
-- Module: Mathlib.RingTheory.LittleWedderburn
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
intro : d ∈ n.properDivisors
⊢ eval (↑q : ℤ) ((HPow.hPow (α := ℤ[X]) X d - 1) * Φₙ) ∣ eval (↑q : ℤ) (HPow.hPow (α := ℤ[X]) X n - 1)

Tactic:
refine map_dvd (evalRingHom ↑q) (X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd ℤ ?_)

Premises used: Int, map_dvd, Polynomial.evalRingHom, Polynomial.X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd
-- Module: Mathlib.RingTheory.LittleWedderburn
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

Tactic:
Nat.mem_properDivisors.mpr ⟨⟨_, (finrank_mul_finrank Z Zx D).symm⟩, ?_⟩

Premises used: Iff.mpr, Membership.mem, Subtype, Module.finrank_mul_finrank, And.intro, Exists.intro, Nat.mem_properDivisors, Eq.symm
-- Module: Mathlib.RingTheory.LittleWedderburn
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
intro : d < n
⊢ d ∈ n.properDivisors

Tactic:
refine Nat.mem_properDivisors.mpr ⟨⟨_, (finrank_mul_finrank Z Zx D).symm⟩, ?_⟩

Premises used: Iff.mpr, Membership.mem, Subtype, Module.finrank_mul_finrank, And.intro, Exists.intro, Nat.mem_properDivisors, Eq.symm
-- Module: Mathlib.RingTheory.LittleWedderburn
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
intro : card.{u_1} ↥Zx < card D
⊢ d < n

Tactic:
rw [← Nat.pow_lt_pow_iff_right hq, ← card_D, ← card_Zx]

Premises used: Nat.pow_lt_pow_iff_right
-- Module: Mathlib.RingTheory.LittleWedderburn
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
intro : ∀ (b : D) (hb : b ∉ Zx), card.{u_1} ↥Zx < card D
⊢ card.{u_1} ↥Zx < card D

Tactic:
obtain ⟨b, -, hb⟩ := SetLike.exists_of_lt hZx.lt_top

Premises used: SetLike.exists_of_lt, Ne.lt_top
-- Module: Mathlib.RingTheory.LittleWedderburn
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

Tactic:
card_lt_of_injective_of_notMem _ Subtype.val_injective (?_ : b ∉ _)

Premises used: Subtype.val_injective, Fintype.card_lt_of_injective_of_notMem
-- Module: Mathlib.RingTheory.LittleWedderburn
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
intro : b ∉ Set.range (ι := ↥Zx) (Subtype.val (p := fun (x : D) ↦ x ∈ Zx))
⊢ card.{u_1} ↥Zx < card D

Tactic:
refine card_lt_of_injective_of_notMem _ Subtype.val_injective (?_ : b ∉ _)

Premises used: Subtype.val_injective, Fintype.card_lt_of_injective_of_notMem
-- Module: Mathlib.RingTheory.LittleWedderburn
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 : ↥Zx
hb : (↑b : D) ∉ Zx
⊢ False

Tactic:
hb b.2

Premises used: Subtype.property
-- Module: Mathlib.RingTheory.LittleWedderburn
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 : ↥Zx
hb : (↑b : D) ∉ Zx
⊢ False

Tactic:
exact hb b.2

Premises used: Subtype.property
-- Module: Mathlib.RingTheory.LittleWedderburn
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) ⊤

Tactic:
cases nonempty_fintype D

Premises used: nonempty_fintype
-- Module: Mathlib.RingTheory.LittleWedderburn
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
val : Fintype 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) ⊤
⊢ Eq (α := Subring D) (Subring.center D) ⊤

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

Premises used: Fintype.card
-- Module: Mathlib.RingTheory.LittleWedderburn
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
intro : InductionHyp D
⊢ Eq (α := Subring D) (Subring.center D) ⊤

Tactic:
apply InductionHyp.center_eq_top

Premises used: _private.0.LittleWedderburn.InductionHyp.center_eq_top
-- Module: Mathlib.RingTheory.LittleWedderburn
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)
⊢ ∀ (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

Premises used: Subring.mem_center_iff
-- Module: Mathlib.RingTheory.LittleWedderburn
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 : ∀ (g : ↥R), g * Subtype.mk (p := fun (x : D) ↦ x ∈ R) y hy = Subtype.mk (p := fun (x : D) ↦ x ∈ R) y hy * g
⊢ x * y = y * x

Tactic:
simpa using this ⟨x, hx⟩

Premises used: Subtype.mk
-- Module: Mathlib.RingTheory.LittleWedderburn
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
intro : Membership.mem (γ := Subring ↥R) (Subring.center ↥R) (Subtype.mk (p := fun (x : D) ↦ x ∈ R) y hy)
⊢ 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⟩
-- Module: Mathlib.RingTheory.LittleWedderburn
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)
rw : card.{u_1} ↥R < n
⊢ Membership.mem (γ := Subring ↥R) (Subring.center ↥R) (Subtype.mk (p := fun (x : D) ↦ x ∈ R) y hy)

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

Premises used: Membership.mem, inferInstance, Fintype.card, Subtype, rfl