internlm/Lean-Github huggingface dataset:
Theorem: div_of_qpoly_div
Proof state before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
hkeqm : ¬k = m
hkm : k ≤ m
this : q ^ m - 1 = q ^ (m - k) * (q ^ k - 1) + (q ^ (m - k) - 1)
h1 : q ^ k - 1 ∣ q ^ (m - k) - 1
hmk : m - k < m
⊢ 0 < m - k
Tactic:
exact Nat.sub_pos_of_lt <| Nat.lt_of_le_of_ne hkm hkeqm
Proof state after:
no goals
Theorem: orbit_stabilizer
Proof state before:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↑{⋯.choose}.centralizer
Tactic:
letI := Fintype.ofFinite (Set.centralizer {ConjClasses.exists_rep A|>.choose})
Proof state after:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↑{⋯.choose}.centralizer
Theorem: orbit_stabilizer
Proof state before:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↑{⋯.choose}.centralizer
Tactic:
letI : Fintype ↑(MulAction.orbit (ConjAct Rˣ) (ConjClasses.exists_rep A|>.choose))
    := by refine Set.fintypeRange fun m => m • Exists.choose ?_
Proof state after:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this✝ : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
this : Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) := Set.fintypeRange fun m => m • ⋯.choose
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↑{⋯.choose}.centralizer
Theorem: orbit_stabilizer
Proof state before:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this✝ : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
this : Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) := Set.fintypeRange fun m => m • ⋯.choose
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↑{⋯.choose}.centralizer
Tactic:
letI : Fintype { x // x ∈ MulAction.stabilizer (ConjAct Rˣ)
      (ConjClasses.exists_rep A|>.choose) } := Fintype.ofFinite _
Proof state after:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this✝¹ : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
this✝ : Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) := Set.fintypeRange fun m => m • ⋯.choose
this : Fintype ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose) :=
  Fintype.ofFinite ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↑{⋯.choose}.centralizer
Theorem: orbit_stabilizer
Proof state before:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this✝¹ : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
this✝ : Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) := Set.fintypeRange fun m => m • ⋯.choose
this : Fintype ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose) :=
  Fintype.ofFinite ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↑{⋯.choose}.centralizer
Tactic:
have := MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct Rˣ)
    (ConjClasses.exists_rep A|>.choose)
Proof state after:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this✝² : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
this✝¹ : Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) := Set.fintypeRange fun m => m • ⋯.choose
this✝ : Fintype ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose) :=
  Fintype.ofFinite ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
this :
  Fintype.card ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) * Fintype.card ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose) =
    Fintype.card (ConjAct Rˣ)
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↑{⋯.choose}.centralizer
Theorem: orbit_stabilizer
Proof state before:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this✝² : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
this✝¹ : Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) := Set.fintypeRange fun m => m • ⋯.choose
this✝ : Fintype ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose) :=
  Fintype.ofFinite ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
this :
  Fintype.card ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) * Fintype.card ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose) =
    Fintype.card (ConjAct Rˣ)
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↑{⋯.choose}.centralizer
Tactic:
replace this := this.symm
Proof state after:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this✝² : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
this✝¹ : Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) := Set.fintypeRange fun m => m • ⋯.choose
this✝ : Fintype ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose) :=
  Fintype.ofFinite ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
this :
  Fintype.card (ConjAct Rˣ) =
    Fintype.card ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) * Fintype.card ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↑{⋯.choose}.centralizer
Theorem: orbit_stabilizer
Proof state before:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this✝² : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
this✝¹ : Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) := Set.fintypeRange fun m => m • ⋯.choose
this✝ : Fintype ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose) :=
  Fintype.ofFinite ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
this :
  Fintype.card (ConjAct Rˣ) =
    Fintype.card ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) * Fintype.card ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↑{⋯.choose}.centralizer
Tactic:
rw [Fintype.card_congr <| ConjAct_stabilizer_centralizer_eq (ConjClasses.exists_rep A|>.choose)]
Proof state after:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this✝² : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
this✝¹ : Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) := Set.fintypeRange fun m => m • ⋯.choose
this✝ : Fintype ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose) :=
  Fintype.ofFinite ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
this :
  Fintype.card (ConjAct Rˣ) =
    Fintype.card ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) * Fintype.card ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
Theorem: orbit_stabilizer
Proof state before:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this✝² : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
this✝¹ : Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) := Set.fintypeRange fun m => m • ⋯.choose
this✝ : Fintype ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose) :=
  Fintype.ofFinite ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
this :
  Fintype.card (ConjAct Rˣ) =
    Fintype.card ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) * Fintype.card ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
Tactic:
convert this
Proof state after:
case h.e'_3.h.e'_5.h.h.e'_2
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this✝² : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
this✝¹ : Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) := Set.fintypeRange fun m => m • ⋯.choose
this✝ : Fintype ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose) :=
  Fintype.ofFinite ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
this :
  Fintype.card (ConjAct Rˣ) =
    Fintype.card ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) * Fintype.card ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
⊢ A.carrier = MulAction.orbit (ConjAct Rˣ) ⋯.choose
Theorem: orbit_stabilizer
Proof state before:
case h.e'_3.h.e'_5.h.h.e'_2
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this✝² : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
this✝¹ : Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) := Set.fintypeRange fun m => m • ⋯.choose
this✝ : Fintype ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose) :=
  Fintype.ofFinite ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
this :
  Fintype.card (ConjAct Rˣ) =
    Fintype.card ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) * Fintype.card ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
⊢ A.carrier = MulAction.orbit (ConjAct Rˣ) ⋯.choose
Tactic:
rw [ConjAct.orbit_eq_carrier_conjClasses, (ConjClasses.exists_rep A|>.choose_spec)]
Proof state after:
no goals
Theorem: orbit_stabilizer
Proof state before:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
⊢ Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose)
Tactic:
refine Set.fintypeRange fun m => m • Exists.choose ?_
Proof state after:
no goals
Theorem: wedderburn
Proof state before:
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
⊢ IsField R
Tactic:
let Z := center R
Proof state after:
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
⊢ IsField R
Theorem: wedderburn
Proof state before:
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
⊢ IsField R
Tactic:
obtain ⟨n, h_card⟩ := VectorSpace.card_fintype Z R
Proof state after:
case intro
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
n : ℕ
h_card : Fintype.card R = Fintype.card ↥Z ^ n
⊢ IsField R
Theorem: wedderburn
Proof state before:
case intro
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
n : ℕ
h_card : Fintype.card R = Fintype.card ↥Z ^ n
⊢ IsField R
Tactic:
have H : (∃ x y : R, x ≠ y) := by exact exists_pair_ne R
Proof state after:
case intro
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
n : ℕ
h_card : Fintype.card R = Fintype.card ↥Z ^ n
H : ∃ x y, x ≠ y
⊢ IsField R
Theorem: wedderburn
Proof state before:
case intro
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
n : ℕ
h_card : Fintype.card R = Fintype.card ↥Z ^ n
H : ∃ x y, x ≠ y
⊢ IsField R
Tactic:
have h_n : n ≠ 0 := by
  by_contra h
  subst h
  simp only [_root_.pow_zero] at h_card
  rcases H with ⟨x, y, H⟩
  absurd H
  exact Fintype.card_le_one_iff.mp (Nat.le_of_eq h_card) x y
Proof state after:
case intro
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
n : ℕ
h_card : Fintype.card R = Fintype.card ↥Z ^ n
H : ∃ x y, x ≠ y
h_n : n ≠ 0
⊢ IsField R
Theorem: wedderburn
Proof state before:
case intro
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
n : ℕ
h_card : Fintype.card R = Fintype.card ↥Z ^ n
H : ∃ x y, x ≠ y
h_n : n ≠ 0
⊢ IsField R
Tactic:
set q := Fintype.card Z
Proof state after:
case intro
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
n : ℕ
H : ∃ x y, x ≠ y
h_n : n ≠ 0
q : ℕ := Fintype.card ↥Z
h_card : Fintype.card R = q ^ n
⊢ IsField R
Theorem: wedderburn
Proof state before:
case intro
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
n : ℕ
H : ∃ x y, x ≠ y
h_n : n ≠ 0
q : ℕ := Fintype.card ↥Z
h_card : Fintype.card R = q ^ n
⊢ IsField R
Tactic:
have finclassa: ∀ (A : ConjClasses Rˣ), Fintype ↑(ConjClasses.carrier A) := by
  intro A
  exact ConjClasses.instFintypeElemCarrier
Proof state after:
case intro
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
n : ℕ
H : ∃ x y, x ≠ y
h_n : n ≠ 0
q : ℕ := Fintype.card ↥Z
h_card : Fintype.card R = q ^ n
finclassa : (A : ConjClasses Rˣ) → Fintype ↑A.carrier
⊢ IsField R
Theorem: wedderburn
Proof state before:
case intro
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
n : ℕ
H : ∃ x y, x ≠ y
h_n : n ≠ 0
q : ℕ := Fintype.card ↥Z
h_card : Fintype.card R = q ^ n
finclassa : (A : ConjClasses Rˣ) → Fintype ↑A.carrier
⊢ IsField R
Tactic:
have : ∀ (A :  ConjClasses Rˣ), Fintype ↑(Set.centralizer {Quotient.out' A}) := by
  intro A
  exact setFintype (Set.centralizer {Quotient.out' A})
Proof state after:
case intro
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
n : ℕ
H : ∃ x y, x ≠ y
h_n : n ≠ 0
q : ℕ := Fintype.card ↥Z
h_card : Fintype.card R = q ^ n
finclassa : (A : ConjClasses Rˣ) → Fintype ↑A.carrier
this : (A : ConjClasses Rˣ) → Fintype ↑{Quotient.out' A}.centralizer
⊢ IsField R
Theorem: wedderburn
Proof state before:
case intro
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
n : ℕ
H : ∃ x y, x ≠ y
h_n : n ≠ 0
q : ℕ := Fintype.card ↥Z
h_card : Fintype.card R = q ^ n
finclassa : (A : ConjClasses Rˣ) → Fintype ↑A.carrier
this : (A : ConjClasses Rˣ) → Fintype ↑{Quotient.out' A}.centralizer
⊢ IsField R
Tactic:
letI fintypea : ∀ (A :  ConjClasses Rˣ), Fintype ↑{A |
    have := finclassa A; Fintype.card ↑(ConjClasses.carrier A) > 1} := by
  intro A
  exact
    setFintype
      {A |
        let_fun this := finclassa A;
        Fintype.card ↑(ConjClasses.carrier A) > 1}
Proof state after:
case intro
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
n : ℕ
H : ∃ x y, x ≠ y
h_n : n ≠ 0
q : ℕ := Fintype.card ↥Z
h_card : Fintype.card R = q ^ n
finclassa : (A : ConjClasses Rˣ) → Fintype ↑A.carrier
this : (A : ConjClasses Rˣ) → Fintype ↑{Quotient.out' A}.centralizer
fintypea : ConjClasses Rˣ →
  Fintype
    ↑{A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1} :=
  fun A =>
    setFintype
      {A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1}
⊢ IsField R
Theorem: wedderburn
Proof state before:
case intro
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
n : ℕ
H : ∃ x y, x ≠ y
h_n : n ≠ 0
q : ℕ := Fintype.card ↥Z
h_card : Fintype.card R = q ^ n
finclassa : (A : ConjClasses Rˣ) → Fintype ↑A.carrier
this : (A : ConjClasses Rˣ) → Fintype ↑{Quotient.out' A}.centralizer
fintypea : ConjClasses Rˣ →
  Fintype
    ↑{A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1} :=
  fun A =>
    setFintype
      {A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1}
⊢ IsField R
Tactic:
have : Fintype ↑{A |
    have := finclassa A;  Fintype.card ↑(ConjClasses.carrier A) > 1} :=
  setFintype {A |
                let_fun this := finclassa A;
                Fintype.card ↑(ConjClasses.carrier A) > 1}
Proof state after:
case intro
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
n : ℕ
H : ∃ x y, x ≠ y
h_n : n ≠ 0
q : ℕ := Fintype.card ↥Z
h_card : Fintype.card R = q ^ n
finclassa : (A : ConjClasses Rˣ) → Fintype ↑A.carrier
this✝ : (A : ConjClasses Rˣ) → Fintype ↑{Quotient.out' A}.centralizer
fintypea : ConjClasses Rˣ →
  Fintype
    ↑{A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1} :=
  fun A =>
    setFintype
      {A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1}
this :
  Fintype
    ↑{A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1}
⊢ IsField R
Theorem: wedderburn
Proof state before:
case intro
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
n : ℕ
H : ∃ x y, x ≠ y
h_n : n ≠ 0
q : ℕ := Fintype.card ↥Z
h_card : Fintype.card R = q ^ n
finclassa : (A : ConjClasses Rˣ) → Fintype ↑A.carrier
this✝ : (A : ConjClasses Rˣ) → Fintype ↑{Quotient.out' A}.centralizer
fintypea : ConjClasses Rˣ →
  Fintype
    ↑{A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1} :=
  fun A =>
    setFintype
      {A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1}
this :
  Fintype
    ↑{A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1}
⊢ IsField R
Tactic:
let S' := ConjClasses.noncenter Rˣ
Proof state after:
case intro
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
n : ℕ
H : ∃ x y, x ≠ y
h_n : n ≠ 0
q : ℕ := Fintype.card ↥Z
h_card : Fintype.card R = q ^ n
finclassa : (A : ConjClasses Rˣ) → Fintype ↑A.carrier
this✝ : (A : ConjClasses Rˣ) → Fintype ↑{Quotient.out' A}.centralizer
fintypea : ConjClasses Rˣ →
  Fintype
    ↑{A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1} :=
  fun A =>
    setFintype
      {A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1}
this :
  Fintype
    ↑{A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1}
S' : Set (ConjClasses Rˣ) := ConjClasses.noncenter Rˣ
⊢ IsField R
Theorem: wedderburn
Proof state before:
case intro
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
n : ℕ
H : ∃ x y, x ≠ y
h_n : n ≠ 0
q : ℕ := Fintype.card ↥Z
h_card : Fintype.card R = q ^ n
finclassa : (A : ConjClasses Rˣ) → Fintype ↑A.carrier
this✝ : (A : ConjClasses Rˣ) → Fintype ↑{Quotient.out' A}.centralizer
fintypea : ConjClasses Rˣ →
  Fintype
    ↑{A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1} :=
  fun A =>
    setFintype
      {A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1}
this :
  Fintype
    ↑{A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1}
S' : Set (ConjClasses Rˣ) := ConjClasses.noncenter Rˣ
⊢ IsField R
Tactic:
haveI : Fintype S' := Fintype.ofFinite ↑S'
Proof state after:
case intro
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
n : ℕ
H : ∃ x y, x ≠ y
h_n : n ≠ 0
q : ℕ := Fintype.card ↥Z
h_card : Fintype.card R = q ^ n
finclassa : (A : ConjClasses Rˣ) → Fintype ↑A.carrier
this✝¹ : (A : ConjClasses Rˣ) → Fintype ↑{Quotient.out' A}.centralizer
fintypea : ConjClasses Rˣ →
  Fintype
    ↑{A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1} :=
  fun A =>
    setFintype
      {A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1}
this✝ :
  Fintype
    ↑{A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1}
S' : Set (ConjClasses Rˣ) := ConjClasses.noncenter Rˣ
this : Fintype ↑S'
⊢ IsField R
Theorem: wedderburn
Proof state before:
case intro
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
n : ℕ
H : ∃ x y, x ≠ y
h_n : n ≠ 0
q : ℕ := Fintype.card ↥Z
h_card : Fintype.card R = q ^ n
finclassa : (A : ConjClasses Rˣ) → Fintype ↑A.carrier
this✝¹ : (A : ConjClasses Rˣ) → Fintype ↑{Quotient.out' A}.centralizer
fintypea : ConjClasses Rˣ →
  Fintype
    ↑{A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1} :=
  fun A =>
    setFintype
      {A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1}
this✝ :
  Fintype
    ↑{A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1}
S' : Set (ConjClasses Rˣ) := ConjClasses.noncenter Rˣ
this : Fintype ↑S'
⊢ IsField R
Tactic:
let S := S'.toFinset
Proof state after:
case intro
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
n : ℕ
H : ∃ x y, x ≠ y
h_n : n ≠ 0
q : ℕ := Fintype.card ↥Z
h_card : Fintype.card R = q ^ n
finclassa : (A : ConjClasses Rˣ) → Fintype ↑A.carrier
this✝¹ : (A : ConjClasses Rˣ) → Fintype ↑{Quotient.out' A}.centralizer
fintypea : ConjClasses Rˣ →
  Fintype
    ↑{A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1} :=
  fun A =>
    setFintype
      {A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1}
this✝ :
  Fintype
    ↑{A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1}
S' : Set (ConjClasses Rˣ) := ConjClasses.noncenter Rˣ
this : Fintype ↑S'
S : Finset (ConjClasses Rˣ) := S'.toFinset
⊢ IsField R
Theorem: wedderburn
Proof state before:
case intro
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
n : ℕ
H : ∃ x y, x ≠ y
h_n : n ≠ 0
q : ℕ := Fintype.card ↥Z
h_card : Fintype.card R = q ^ n
finclassa : (A : ConjClasses Rˣ) → Fintype ↑A.carrier
this✝¹ : (A : ConjClasses Rˣ) → Fintype ↑{Quotient.out' A}.centralizer
fintypea : ConjClasses Rˣ →
  Fintype
    ↑{A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1} :=
  fun A =>
    setFintype
      {A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1}
this✝ :
  Fintype
    ↑{A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1}
S' : Set (ConjClasses Rˣ) := ConjClasses.noncenter Rˣ
this : Fintype ↑S'
S : Finset (ConjClasses Rˣ) := S'.toFinset
⊢ IsField R
Tactic:
let n_k : S' → ℕ := sorry
Proof state after:
case intro
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
n : ℕ
H : ∃ x y, x ≠ y
h_n : n ≠ 0
q : ℕ := Fintype.card ↥Z
h_card : Fintype.card R = q ^ n
finclassa : (A : ConjClasses Rˣ) → Fintype ↑A.carrier
this✝¹ : (A : ConjClasses Rˣ) → Fintype ↑{Quotient.out' A}.centralizer
fintypea : ConjClasses Rˣ →
  Fintype
    ↑{A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1} :=
  fun A =>
    setFintype
      {A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1}
this✝ :
  Fintype
    ↑{A |
        let_fun this := finclassa A;
        Fintype.card ↑A.carrier > 1}
S' : Set (ConjClasses Rˣ) := ConjClasses.noncenter Rˣ
this : Fintype ↑S'
S : Finset (ConjClasses Rˣ) := S'.toFinset
n_k : ↑S' → ℕ := sorryAx (↑S' → ℕ)
⊢ IsField R