awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Algebra.IsIntegral.{u, v} R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite.{u, v} R ↥A'], A'.LinearDisjoint B
x y :
  ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R]
    ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S)
hxy :
  Eq (α := S)
    ((Submodule.mulMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
            ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B) :
          (a :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) →
            S)
        x :
      S)
    ((Submodule.mulMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
            ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B) :
          (a :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) →
            S)
        y :
      S)
M' : Submodule R S
hM : M' ≤ (toSubmodule : (a : Subalgebra R S) → Submodule R S) A
hf : Module.Finite.{u, v} R ↥M'
s : Finset S
hs : Submodule.span R (↑s : Set S) = M'
hs' : (↑s : Set S) ⊆ (↑A : Set S)
A' : Subalgebra R S := Algebra.adjoin R (↑s : Set S)
hf' : Module.Finite.{u, v} R ↥A'
hA :
  LE.le (α := Submodule R S) ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A' : Submodule R S)
    ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)
h :
  {x, y} ⊆
    (↑(LinearMap.range
          (LinearMap.rTensor (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S))
            (Submodule.inclusion hA))) :
      Set
        (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)))
obtain :
  ∀
    (x' :
      ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A' : Submodule R S) ⊗[R]
        ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S))
    (hx' :
      (LinearMap.rTensor (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S))
              (Submodule.inclusion hA) :
            (a :
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A') ⊗[R]
                  ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) →
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B))
          x' =
        x),
    x = y
⊢ x = y

Tactic:
obtain ⟨x', hx'⟩ := h (show x ∈ {x, y} by simp)
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Algebra.IsIntegral.{u, v} R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite.{u, v} R ↥A'], A'.LinearDisjoint B
x y :
  ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R]
    ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S)
hxy :
  Eq (α := S)
    ((Submodule.mulMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
            ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B) :
          (a :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) →
            S)
        x :
      S)
    ((Submodule.mulMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
            ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B) :
          (a :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) →
            S)
        y :
      S)
M' : Submodule R S
hM : M' ≤ (toSubmodule : (a : Subalgebra R S) → Submodule R S) A
hf : Module.Finite.{u, v} R ↥M'
s : Finset S
hs : Submodule.span R (↑s : Set S) = M'
hs' : (↑s : Set S) ⊆ (↑A : Set S)
A' : Subalgebra R S := Algebra.adjoin R (↑s : Set S)
hf' : Module.Finite.{u, v} R ↥A'
hA :
  LE.le (α := Submodule R S) ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A' : Submodule R S)
    ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)
h :
  {x, y} ⊆
    (↑(LinearMap.range
          (LinearMap.rTensor (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S))
            (Submodule.inclusion hA))) :
      Set
        (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)))
x' :
  ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A' : Submodule R S) ⊗[R]
    ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S)
hx' :
  (LinearMap.rTensor (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S))
          (Submodule.inclusion hA) :
        (a :
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A') ⊗[R]
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) →
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B))
      x' =
    x
⊢ Membership.mem (γ :=
    Set
      (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R]
        ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S)))
    {x, y} y

Tactic:
simp
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Algebra.IsIntegral.{u, v} R ↥B
H : ∀ B' ≤ B, ∀ [Module.Finite.{u, v} R ↥B'], A.LinearDisjoint B'
⊢ A.LinearDisjoint B

Tactic:
(of_linearDisjoint_finite_left B A fun B' hB' _ ↦ (H B' hB').symm).symm

Premises used: Subalgebra.LinearDisjoint.symm, Subalgebra.LinearDisjoint.of_linearDisjoint_finite_left
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Algebra.IsIntegral.{u, v} R ↥A
inst_4 : Algebra.IsIntegral.{u, v} R ↥B
H :
  ∀ (A' B' : Subalgebra R S),
    A' ≤ A → B' ≤ B → ∀ [Module.Finite.{u, v} R ↥A'] [Module.Finite.{u, v} R ↥B'], A'.LinearDisjoint B'
⊢ A.LinearDisjoint B

Tactic:
of_linearDisjoint_finite_left A B fun _ hA' _ ↦
    of_linearDisjoint_finite_right _ B fun _ hB' _ ↦ H _ _ hA' hB'

Premises used: Subalgebra.LinearDisjoint.of_linearDisjoint_finite_right, Subalgebra.LinearDisjoint.of_linearDisjoint_finite_left
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
hc : ∀ (a b : ↥(A ⊓ B)), Commute (↑a : S) (↑b : S)
⊢ A ⊓ B = ⊥

Tactic:
eq_bot_of_rank_le_one (Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat_left H hc)

Premises used: Subalgebra.eq_bot_of_rank_le_one, Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat_left
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : Ring S
inst_2 : Algebra R S
A : Subalgebra R S
H : A.LinearDisjoint A
hc : ∀ (a b : ↥A), Commute (↑a : S) (↑b : S)
rw : ∀ (hc : ∀ (a b : ↥(A ⊓ A)), Commute (↑a : S) (↑b : S)), A ⊓ A = ⊥
⊢ A = ⊥

Tactic:
rw [← inf_of_le_left (le_refl A)] at hc ⊢

Premises used: le_refl, inf_of_le_left
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : Ring S
inst_2 : Algebra R S
A : Subalgebra R S
H : A.LinearDisjoint A
hc : ∀ (a b : ↥(A ⊓ A)), Commute (↑a : S) (↑b : S)
⊢ A ⊓ A = ⊥

Tactic:
H.inf_eq_bot_of_commute hc

Premises used: Subalgebra.LinearDisjoint.inf_eq_bot_of_commute
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : Ring S
inst_2 : Algebra R S
A : Subalgebra R S
H : A.LinearDisjoint A
hc : ∀ (a b : ↥(A ⊓ A)), Commute (↑a : S) (↑b : S)
⊢ A ⊓ A = ⊥

Tactic:
exact H.inf_eq_bot_of_commute hc

Premises used: Subalgebra.LinearDisjoint.inf_eq_bot_of_commute
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
⊢ A ⊓ B = ⊥

Tactic:
H.inf_eq_bot_of_commute fun _ _ ↦ mul_comm _ _

Premises used: Subalgebra.LinearDisjoint.inf_eq_bot_of_commute, mul_comm, Subtype.val
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Subalgebra R S
H : A.LinearDisjoint A
⊢ A = ⊥

Tactic:
H.eq_bot_of_commute_of_self fun _ _ ↦ mul_comm _ _

Premises used: mul_comm, Subtype.val, Subalgebra.LinearDisjoint.eq_bot_of_commute_of_self
-- Module: Mathlib.RingTheory.LittleWedderburn
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
hD : InductionHyp 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
hD : InductionHyp D
val : Fintype D
intro :
  let Z : Subring D := Subring.center D;
  Z = ⊤
⊢ Eq (α := Subring D) (Subring.center D) ⊤

Tactic:
set Z := Subring.center D

Premises used: Subring.center
-- 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
intro : ∀ (hZ : Z ≠ ⊤), False
⊢ Z = ⊤

Tactic:
by_contra! hZ
-- 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 ⋯
⊢ let q := card.{u_1} ↥Z;
  q = card.{u_1} ↥Z

Tactic:
set q := card Z with card_Z

Premises used: Membership.mem, Fintype.card, Subtype
-- 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
rw : 1 < card.{u_1} ↥Z
⊢ 1 < q

Tactic:
rw [card_Z]
-- 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
⊢ 1 < card.{u_1} ↥Z

Tactic:
one_lt_card

Premises used: Fintype.one_lt_card
-- 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
⊢ 1 < card.{u_1} ↥Z

Tactic:
exact one_lt_card

Premises used: Fintype.one_lt_card
-- 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
⊢ 1 < q

Tactic:
have hq : 1 < q := by rw [card_Z]; exact one_lt_card
-- 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 = q ^ n

Tactic:
have card_D : card D = q ^ n := 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 : 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
rw : 1 ≤ card D
⊢ 1 ≤ q ^ n

Tactic:
rw [← card_D]
-- 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
⊢ 1 ≤ card D

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 : 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
⊢ 1 ≤ card D

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 : 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
⊢ 1 ≤ q ^ n

Tactic:
have h1qn : 1 ≤ q ^ n := by rw [← card_D]; exact 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 : 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
⊢ 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ˣ)
-- 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
key :
  card.{u_1} ↥(Subgroup.center Dˣ) + ∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card =
    card.{u_1} Dˣ
⊢ 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

Premises used: Fintype.card_congr, Fintype.card_units, Subgroup.centerUnitsEquivUnitsCenter, MulEquiv.toEquiv
-- 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
key : q - 1 + ∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card = q ^ n - 1
Φₙ : ℤ[X] := cyclotomic n ℤ
⊢ Eq (α := ℤ) (↑(q - 1 + ∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ) (↑(q ^ n - 1) : ℤ)

Tactic:
apply_fun (Nat.cast : ℕ → ℤ) at key

Premises used: Nat.cast
-- 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 :
  Eq (α := ℤ) (↑(q - 1 + ∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ) (↑(q ^ n - 1) : ℤ)
⊢ 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

Premises used: Nat.cast_sub, LT.lt.le, Nat.cast_add, Nat.cast_pow, 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) : ℤ)
⊢ 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 : ℤ))
-- 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 : ℤ) Φₙ ∣ eval (↑q : ℤ) (HPow.hPow (α := ℤ[X]) X n - 1)
⊢ eval (↑q : ℤ) Φₙ ∣ HSub.hSub (α := ℤ) (↑q : ℤ) 1

Tactic:
rw [eval_sub, eval_X_pow, eval_one, ← key, Int.dvd_add_left this] at contra

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

Tactic:
(Nat.le_of_dvd ?_ ?_).not_gt (sub_one_lt_natAbs_cyclotomic_eval (n := n) ?_ hq.ne')

Premises used: Polynomial.sub_one_lt_natAbs_cyclotomic_eval, LT.lt.ne', LE.le.not_gt, Nat.le_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
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
refine_3 : 1 < n
⊢ False

Tactic:
refine (Nat.le_of_dvd ?_ ?_).not_gt (sub_one_lt_natAbs_cyclotomic_eval (n := n) ?_ hq.ne')

Premises used: Polynomial.sub_one_lt_natAbs_cyclotomic_eval, LT.lt.ne', LE.le.not_gt, Nat.le_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
this : eval (↑q : ℤ) Φₙ ∣ (↑(∑ x ∈ Set.toFinset (ConjClasses.noncenter Dˣ), x.carrier.toFinset.card) : ℤ)
contra : eval (↑q : ℤ) Φₙ ∣ HSub.hSub (α := ℤ) (↑q : ℤ) 1
⊢ 0 < q - 1

Tactic:
tsub_pos_of_lt hq

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

Tactic:
exact tsub_pos_of_lt hq

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

Tactic:
Int.natAbs_dvd_natAbs.mpr contra

Premises used: Iff.mpr, Int.natAbs_dvd_natAbs
-- 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 - 1 = (HSub.hSub (α := ℤ) (↑q : ℤ) 1).natAbs
⊢ (eval (↑q : ℤ) (cyclotomic n ℤ)).natAbs ∣ q - 1

Tactic:
convert! Int.natAbs_dvd_natAbs.mpr contra

Premises used: Iff.mpr, Int.natAbs_dvd_natAbs