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
this : eval (↑q : ℤ) Φₙ ∣ (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ)
contra : eval (↑q : ℤ) Φₙ ∣ HSub.hSub (α := ℤ) (↑q : ℤ) 1
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
⊢ q - 1 = (HSub.hSub (α := ℤ) (↑q : ℤ) 1).natAbs

Tactic:
clear_value q
-- 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_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

Tactic:
simp only [eq_comm, Int.natAbs_eq_iff, Nat.cast_sub hq.le, Nat.cast_one, neg_sub, true_or]

Premises used: neg_sub, Nat.cast_sub, true_or, LT.lt.le, eq_comm, Int.natAbs_eq_iff, Nat.cast_one
-- 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
this : eval (↑q : ℤ) Φₙ ∣ (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ)
contra : eval (↑q : ℤ) Φₙ ∣ HSub.hSub (α := ℤ) (↑q : ℤ) 1
refine_3 : ∀ (h : n ≤ 1), False
⊢ 1 < n

Tactic:
by_contra! h
-- 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
this : eval (↑q : ℤ) Φₙ ∣ (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ)
contra : eval (↑q : ℤ) Φₙ ∣ HSub.hSub (α := ℤ) (↑q : ℤ) 1
h : n ≤ 1
refine_3 : ∀ (x : D) (hx : ∀ (w : D), ∃ (c : ↥Z), c • x = w), False
⊢ False

Tactic:
obtain ⟨x, hx⟩ := finrank_le_one_iff.mp h

Premises used: Iff.mp, finrank_le_one_iff
-- 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
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

Tactic:
not_le_of_gt hZ.lt_top (fun y _ ↦ Subring.mem_center_iff.mpr fun z ↦ ?_)

Premises used: Subring.mem_center_iff, Iff.mpr, Ne.lt_top, not_le_of_gt
-- 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
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
refine_3 : ∀ (y : D), Membership.mem (γ := Subring D) ⊤ y → ∀ (z : D), z * y = y * z
⊢ False

Tactic:
refine not_le_of_gt hZ.lt_top (fun y _ ↦ Subring.mem_center_iff.mpr fun z ↦ ?_)

Premises used: Subring.mem_center_iff, Iff.mpr, Ne.lt_top, not_le_of_gt
-- 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
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
refine_3 : ∀ (r : ↥Z), Membership.mem (γ := Subring D) ⊤ (r • x) → z * r • x = r • x * z
⊢ z * y = y * z

Tactic:
obtain ⟨r, rfl⟩ := hx y

Premises used: rfl
-- 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
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)
refine_3 : ∀ (s : ↥Z), s • x * r • x = r • x * s • x
⊢ z * r • x = r • x * z

Tactic:
obtain ⟨s, rfl⟩ := hx z

Premises used: rfl
-- 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
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)
refine_3₂ refine_3₃ : (r * s) • (x * x) = (r * s) • (x * x)
⊢ s • x * r • x = r • x * s • x

Tactic:
rw [smul_mul_smul_comm, smul_mul_smul_comm, mul_comm]

Premises used: smul_mul_smul_comm, mul_comm
-- 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 : 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
intro : eval (↑q : ℤ) Φₙ ∣ (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ)
⊢ False

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]
-- 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 : 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
intro : eval (↑q : ℤ) Φₙ ∣ ∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), (↑x.carrier.toFinset.card : ℤ)
⊢ eval (↑q : ℤ) Φₙ ∣ (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ)

Tactic:
rw [Nat.cast_sum]

Premises used: Nat.cast_sum
-- 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 : 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
intro :
  ∀ (i : ConjClasses Dˣ),
    Membership.mem (γ := Finset (ConjClasses Dˣ)) (Set.toFinset (ConjClasses.noncenter Dˣ)) i →
      eval (↑q : ℤ) Φₙ ∣ (↑i.carrier.toFinset.card : ℤ)
⊢ eval (↑q : ℤ) Φₙ ∣ ∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), (↑x.carrier.toFinset.card : ℤ)

Tactic:
apply Finset.dvd_sum

Premises used: Finset.dvd_sum
-- 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 : 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)
⊢ 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 ⊢

Premises used: Set.mem_toFinset, ConjClasses.quot_mk_eq_mk
-- 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 : 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)}
intro : eval (↑q : ℤ) Φₙ ∣ (↑((q ^ n - 1) / card.{u_1} (↥Zx)ˣ) : ℤ)
⊢ eval (↑q : ℤ) Φₙ ∣ (↑(ConjClasses.carrier (ConjClasses.mk x)).toFinset.card : ℤ)

Tactic:
rw [Set.toFinset_card, ConjClasses.card_carrier, ← card_congr
        (show Zxˣ ≃* _ from unitsCentralizerEquiv _ x).toEquiv, card_units, card_D]

Premises used: Fintype.card_congr, Fintype.card_units, MulEquiv.toEquiv, Set.toFinset_card, unitsCentralizerEquiv, ConjClasses.card_carrier
-- 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 : 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)}
by_contra! : ∀ (hZx : Zx = ⊤), False
⊢ Zx ≠ ⊤

Tactic:
by_contra! hZx
-- 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 : 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

Tactic:
(ConjClasses.mk_bijOn (Dˣ)).mapsTo (Set.subset_center_units ?_) hx

Premises used: Units, ConjClasses.mk_bijOn, Set.BijOn.mapsTo, Set.subset_center_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 : 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 = ⊤
refine : Membership.mem (γ := Set Dˣ) (Units.val ⁻¹' Set.center D) x
⊢ False

Tactic:
refine (ConjClasses.mk_bijOn (Dˣ)).mapsTo (Set.subset_center_units ?_) hx

Premises used: Units, ConjClasses.mk_bijOn, Set.BijOn.mapsTo, Set.subset_center_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 : 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 = ⊤
⊢ Membership.mem (γ := Set Dˣ) (Units.val ⁻¹' Set.center D) x

Tactic:
Subring.centralizer_eq_top_iff_subset.mp hZx <| Set.mem_singleton _

Premises used: Set.mem_singleton, Subring.centralizer_eq_top_iff_subset, Set.Mem, setOf, Set.center, Set.preimage, Iff.mp
-- 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 : 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 = ⊤
⊢ Membership.mem (γ := Set Dˣ) (Units.val ⁻¹' Set.center D) x

Tactic:
exact Subring.centralizer_eq_top_iff_subset.mp hZx <| Set.mem_singleton _

Premises used: Set.mem_singleton, Subring.centralizer_eq_top_iff_subset, Iff.mp
-- 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 : 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)}
⊢ 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 _
-- 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.{u_1} ↥Zx = q ^ d

Tactic:
have card_Zx : card Zx = q ^ d := Module.card_eq_pow_finrank
-- 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
rw : 1 ≤ card.{u_1} ↥Zx
⊢ 1 ≤ q ^ d

Tactic:
rw [← card_Zx]
-- 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
⊢ 1 ≤ card.{u_1} ↥Zx

Tactic:
card_pos

Premises used: Fintype.card_pos, Nat.lt
-- 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
⊢ 1 ≤ card.{u_1} ↥Zx

Tactic:
exact card_pos

Premises used: Fintype.card_pos
-- 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
⊢ 1 ≤ q ^ d

Tactic:
have h1qd : 1 ≤ q ^ d := by rw [← card_Zx]; exact card_pos