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
⊢ False
have key : card.{u_1} ↥(Subgroup.center Dˣ) + ∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card =
  card.{u_1} Dˣ
Tactic: have key := Group.card_center_add_sum_card_noncenter_eq_card (Dˣ)
-- 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
key :
  card.{u_1} ↥(Subgroup.center Dˣ) + ∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card =
    card.{u_1} Dˣ
⊢ False
have key₁ : q - 1 + ∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card = q ^ n - 1
Tactic: rw [card_congr (show _ ≃* Zˣ from Subgroup.centerUnitsEquivUnitsCenter D).toEquiv,
      card_units, ← card_Z, card_units, card_D] at key
Cleared hypotheses: key
-- 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
key : q - 1 + ∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card = q ^ n - 1
Φₙ : ℤ[X] := cyclotomic n ℤ
⊢ False
have key₁ : Eq (α := ℤ) (↑(q - 1 + ∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ) (↑(q ^ n - 1) : ℤ)
Tactic: apply_fun (Nat.cast : ℕ → ℤ) at key
Cleared hypotheses: key
-- 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 :
  Eq (α := ℤ) (↑(q - 1 + ∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ) (↑(q ^ n - 1) : ℤ)
⊢ False
have key₁ : HSub.hSub (α := ℤ) (↑q : ℤ) 1 + (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ) =
  HPow.hPow (α := ℤ) (↑q : ℤ) n - 1
Tactic: rw [Nat.cast_add, Nat.cast_sub h1qn, Nat.cast_sub hq.le, Nat.cast_one, Nat.cast_pow] at key
Cleared hypotheses: key
-- 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
this : eval (↑q : ℤ) Φₙ ∣ (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ)
⊢ False
have contra : eval (↑q : ℤ) Φₙ ∣ eval (↑q : ℤ) (HPow.hPow (α := ℤ[X]) X n - 1)
Tactic: have contra : Φₙ.eval _ ∣ _ := eval_dvd (cyclotomic.dvd_X_pow_sub_one n ℤ) (x := (q : ℤ))
-- 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
this : eval (↑q : ℤ) Φₙ ∣ (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ)
contra : eval (↑q : ℤ) Φₙ ∣ eval (↑q : ℤ) (HPow.hPow (α := ℤ[X]) X n - 1)
⊢ False
have contra₁ : eval (↑q : ℤ) Φₙ ∣ HSub.hSub (α := ℤ) (↑q : ℤ) 1
Tactic: rw [eval_sub, eval_X_pow, eval_one, ← key, Int.dvd_add_left this] at contra
Cleared hypotheses: contra
-- 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
this : eval (↑q : ℤ) Φₙ ∣ (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ)
contra : eval (↑q : ℤ) Φₙ ∣ HSub.hSub (α := ℤ) (↑q : ℤ) 1
⊢ False
have refine_1 : 0 < q - 1
Tactic: refine (Nat.le_of_dvd ?_ ?_).not_gt (sub_one_lt_natAbs_cyclotomic_eval (n := n) ?_ hq.ne')
-- 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
this : eval (↑q : ℤ) Φₙ ∣ (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ)
contra : eval (↑q : ℤ) Φₙ ∣ HSub.hSub (α := ℤ) (↑q : ℤ) 1
refine_1 : 0 < q - 1
⊢ False
have refine_2 : (eval (↑q : ℤ) (cyclotomic n ℤ)).natAbs ∣ q - 1
Tactic: refine (Nat.le_of_dvd ?_ ?_).not_gt (sub_one_lt_natAbs_cyclotomic_eval (n := n) ?_ hq.ne')
-- 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
this : eval (↑q : ℤ) Φₙ ∣ (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ)
contra : eval (↑q : ℤ) Φₙ ∣ HSub.hSub (α := ℤ) (↑q : ℤ) 1
refine_1 : 0 < q - 1
refine_2 : (eval (↑q : ℤ) (cyclotomic n ℤ)).natAbs ∣ q - 1
⊢ False
have refine_3 : 1 < n
Tactic: refine (Nat.le_of_dvd ?_ ?_).not_gt (sub_one_lt_natAbs_cyclotomic_eval (n := n) ?_ hq.ne')
-- 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
this : eval (↑q : ℤ) Φₙ ∣ (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ)
contra : eval (↑q : ℤ) Φₙ ∣ HSub.hSub (α := ℤ) (↑q : ℤ) 1
⊢ (eval (↑q : ℤ) (cyclotomic n ℤ)).natAbs ∣ q - 1
have h : q - 1 = (HSub.hSub (α := ℤ) (↑q : ℤ) 1).natAbs
Tactic: convert! Int.natAbs_dvd_natAbs.mpr contra
-- 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
this : eval (↑q : ℤ) Φₙ ∣ (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ)
contra : eval (↑q : ℤ) Φₙ ∣ HSub.hSub (α := ℤ) (↑q : ℤ) 1
⊢ q - 1 = (HSub.hSub (α := ℤ) (↑q : ℤ) 1).natAbs
have h : ∀ (q : ℕ) (card_Z : q = card.{u_1} ↥Z) (hq : 1 < q),
  let n := finrank (↥Z) D;
  ∀ (card_D : card D = q ^ n) (h1qn : 1 ≤ q ^ n),
    let Φₙ : ℤ[X] := cyclotomic n ℤ;
    ∀
      (key :
        HSub.hSub (α := ℤ) (↑q : ℤ) 1 +
            (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ) =
          HPow.hPow (α := ℤ) (↑q : ℤ) n - 1)
      (this : eval (↑q : ℤ) Φₙ ∣ (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ))
      (contra : eval (↑q : ℤ) Φₙ ∣ HSub.hSub (α := ℤ) (↑q : ℤ) 1), q - 1 = (HSub.hSub (α := ℤ) (↑q : ℤ) 1).natAbs
Tactic: clear_value q
Cleared hypotheses: q, card_Z, hq, n, card_D, h1qn, Φₙ, key, this, contra
-- 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
this : eval (↑q : ℤ) Φₙ ∣ (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ)
contra : eval (↑q : ℤ) Φₙ ∣ HSub.hSub (α := ℤ) (↑q : ℤ) 1
⊢ 1 < n
have refine_3 : ∀ (h : n ≤ 1), False
Tactic: by_contra! h
-- 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
this : eval (↑q : ℤ) Φₙ ∣ (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ)
contra : eval (↑q : ℤ) Φₙ ∣ HSub.hSub (α := ℤ) (↑q : ℤ) 1
h : n ≤ 1
⊢ False
have refine_3 : ∀ (x : D) (hx : ∀ (w : D), ∃ (c : ↥Z), c • x = w), False
Tactic: obtain ⟨x, hx⟩ := finrank_le_one_iff.mp h
-- 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
this : eval (↑q : ℤ) Φₙ ∣ (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ)
contra : eval (↑q : ℤ) Φₙ ∣ HSub.hSub (α := ℤ) (↑q : ℤ) 1
h : n ≤ 1
x : D
hx : ∀ (w : D), ∃ (c : ↥Z), c • x = w
⊢ False
have refine_3 : ∀ (y : D), Membership.mem (γ := Subring D) ⊤ y → ∀ (z : D), z * y = y * z
Tactic: refine not_le_of_gt hZ.lt_top (fun y _ ↦ Subring.mem_center_iff.mpr fun z ↦ ?_)
-- 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
this : eval (↑q : ℤ) Φₙ ∣ (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ)
contra : eval (↑q : ℤ) Φₙ ∣ HSub.hSub (α := ℤ) (↑q : ℤ) 1
h : n ≤ 1
x : D
hx : ∀ (w : D), ∃ (c : ↥Z), c • x = w
y : D
h_1 : Membership.mem (γ := Subring D) ⊤ y
z : D
⊢ z * y = y * z
have refine_3 : ∀ (r : ↥Z), Membership.mem (γ := Subring D) ⊤ (r • x) → z * r • x = r • x * z
Tactic: obtain ⟨r, rfl⟩ := hx y
Cleared hypotheses: y, h_1
-- 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
this : eval (↑q : ℤ) Φₙ ∣ (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ)
contra : eval (↑q : ℤ) Φₙ ∣ HSub.hSub (α := ℤ) (↑q : ℤ) 1
h : n ≤ 1
x : D
hx : ∀ (w : D), ∃ (c : ↥Z), c • x = w
z : D
r : ↥Z
h_1 : Membership.mem (γ := Subring D) ⊤ (r • x)
⊢ z * r • x = r • x * z
have refine_3 : ∀ (s : ↥Z), s • x * r • x = r • x * s • x
Tactic: obtain ⟨s, rfl⟩ := hx z
Cleared hypotheses: z
-- 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
this : eval (↑q : ℤ) Φₙ ∣ (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ)
contra : eval (↑q : ℤ) Φₙ ∣ HSub.hSub (α := ℤ) (↑q : ℤ) 1
h : n ≤ 1
x : D
hx : ∀ (w : D), ∃ (c : ↥Z), c • x = w
r : ↥Z
h_1 : Membership.mem (γ := Subring D) ⊤ (r • x)
s : ↥Z
⊢ s • x * r • x = r • x * s • x
have refine_3 : (s * r) • (x * x) = r • x * s • x
Tactic: rw [smul_mul_smul_comm, smul_mul_smul_comm, mul_comm]
-- 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
this : eval (↑q : ℤ) Φₙ ∣ (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ)
contra : eval (↑q : ℤ) Φₙ ∣ HSub.hSub (α := ℤ) (↑q : ℤ) 1
h : n ≤ 1
x : D
hx : ∀ (w : D), ∃ (c : ↥Z), c • x = w
r : ↥Z
h_1 : Membership.mem (γ := Subring D) ⊤ (r • x)
s : ↥Z
refine_3 : (s * r) • (x * x) = r • x * s • x
⊢ s • x * r • x = r • x * s • x
have refine_3₁ : (s * r) • (x * x) = (r * s) • (x * x)
Tactic: rw [smul_mul_smul_comm, smul_mul_smul_comm, mul_comm]
-- 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
this : eval (↑q : ℤ) Φₙ ∣ (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ)
contra : eval (↑q : ℤ) Φₙ ∣ HSub.hSub (α := ℤ) (↑q : ℤ) 1
h : n ≤ 1
x : D
hx : ∀ (w : D), ∃ (c : ↥Z), c • x = w
r : ↥Z
h_1 : Membership.mem (γ := Subring D) ⊤ (r • x)
s : ↥Z
refine_3 : (s * r) • (x * x) = r • x * s • x
refine_3₁ : (s * r) • (x * x) = (r * s) • (x * x)
⊢ s • x * r • x = r • x * s • x
have refine_3₂ : (r * s) • (x * x) = (r * s) • (x * x)
Tactic: rw [smul_mul_smul_comm, smul_mul_smul_comm, mul_comm]
-- 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 : 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
⊢ False
have intro : eval (↑q : ℤ) Φₙ ∣ (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ)
Tactic: suffices Φₙ.eval ↑q ∣ ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) by
    have contra : Φₙ.eval _ ∣ _ := eval_dvd (cyclotomic.dvd_X_pow_sub_one n ℤ) (x := (q : ℤ))
    rw [eval_sub, eval_X_pow, eval_one, ← key, Int.dvd_add_left this] at contra
    refine (Nat.le_of_dvd ?_ ?_).not_gt (sub_one_lt_natAbs_cyclotomic_eval (n := n) ?_ hq.ne')
    · exact tsub_pos_of_lt hq
    · convert! Int.natAbs_dvd_natAbs.mpr contra
      clear_value q
      simp only [eq_comm, Int.natAbs_eq_iff, Nat.cast_sub hq.le, Nat.cast_one, neg_sub, true_or]
    · by_contra! h
      obtain ⟨x, hx⟩ := finrank_le_one_iff.mp h
      refine not_le_of_gt hZ.lt_top (fun y _ ↦ Subring.mem_center_iff.mpr fun z ↦ ?_)
      obtain ⟨r, rfl⟩ := hx y
      obtain ⟨s, rfl⟩ := hx z
      rw [smul_mul_smul_comm, smul_mul_smul_comm, mul_comm]
-- 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 : 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
⊢ eval (↑q : ℤ) Φₙ ∣ (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ)
have intro : eval (↑q : ℤ) Φₙ ∣ ∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), (↑x.carrier.toFinset.card : ℤ)
Tactic: rw [Nat.cast_sum]
-- 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 : 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
⊢ eval (↑q : ℤ) Φₙ ∣ ∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), (↑x.carrier.toFinset.card : ℤ)
have intro : ∀ (i : ConjClasses Dˣ),
  Membership.mem (γ := Finset (ConjClasses Dˣ)) (Set.toFinset (ConjClasses.noncenter Dˣ)) i →
    eval (↑q : ℤ) Φₙ ∣ (↑i.carrier.toFinset.card : ℤ)
Tactic: apply Finset.dvd_sum
-- 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 (γ := Finset (ConjClasses Dˣ)) (Set.toFinset (ConjClasses.noncenter Dˣ))
    (Quot.mk (⇑(IsConj.setoid Dˣ) : Dˣ → Dˣ → Prop) x)
⊢ eval (↑q : ℤ) Φₙ ∣ (↑(ConjClasses.carrier (Quot.mk (⇑(IsConj.setoid Dˣ) : Dˣ → Dˣ → Prop) x)).toFinset.card : ℤ)
have hx₁ : Membership.mem (γ := Set (ConjClasses Dˣ)) (ConjClasses.noncenter Dˣ) (ConjClasses.mk x)
Tactic: simp -zeta only [ConjClasses.quot_mk_eq_mk, Set.mem_toFinset] at hx ⊢
Cleared hypotheses: hx
-- 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 : 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 : ℤ) Φₙ ∣ (↑(ConjClasses.carrier (ConjClasses.mk x)).toFinset.card : ℤ)
have intro : eval (↑q : ℤ) Φₙ ∣ (↑((q ^ n - 1) / card.{u_1} (↥Zx)ˣ) : ℤ)
Tactic: rw [Set.toFinset_card, ConjClasses.card_carrier, ← card_congr
        (show Zxˣ ≃* _ from unitsCentralizerEquiv _ x).toEquiv, card_units, card_D]
-- 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 : 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 = ⊤
⊢ False
have refine : Membership.mem (γ := Set Dˣ) (Units.val ⁻¹' Set.center D) x
Tactic: refine (ConjClasses.mk_bijOn (Dˣ)).mapsTo (Set.subset_center_units ?_) hx