awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : IsSimpleRing R
tfae_1_to_2 : ∀ (a : IsSemisimpleRing R), IsArtinianRing R
tfae_2_to_3 : ∀ (a : IsArtinianRing R), ∃ (I : Ideal R), IsAtom I
h_1 : ∃ (I : Ideal R), IsAtom I
I : Ideal R
hI : IsAtom I
left : Nontrivial R
h : ∀ (I : Ideal R), Submodule.IsFullyInvariant I → I = ⊥ ∨ I = ⊤
this : IsSimpleModule R ↥I
⊢ IsSemisimpleRing R
have inl : ∀ (eq : Eq (α := Ideal R) (isotypicComponent R R ↥I : Submodule R R) (⊥ : Ideal R)), IsSemisimpleRing R
Tactic: obtain eq | eq := h _ (.isotypicComponent R R I)
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : IsSimpleRing R
tfae_1_to_2 : ∀ (a : IsSemisimpleRing R), IsArtinianRing R
tfae_2_to_3 : ∀ (a : IsArtinianRing R), ∃ (I : Ideal R), IsAtom I
h_1 : ∃ (I : Ideal R), IsAtom I
I : Ideal R
hI : IsAtom I
left : Nontrivial R
h : ∀ (I : Ideal R), Submodule.IsFullyInvariant I → I = ⊥ ∨ I = ⊤
this : IsSimpleModule R ↥I
inl : ∀ (eq : Eq (α := Ideal R) (isotypicComponent R R ↥I : Submodule R R) (⊥ : Ideal R)), IsSemisimpleRing R
⊢ IsSemisimpleRing R
have inr : ∀ (eq : Eq (α := Ideal R) (isotypicComponent R R ↥I : Submodule R R) (⊤ : Ideal R)), IsSemisimpleRing R
Tactic: obtain eq | eq := h _ (.isotypicComponent R R I)
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (hypothesis)
Goal:
R : Type u
inst : Ring R
inst_1 : IsSimpleRing R
tfae_1_to_2 : ∀ (a : IsSemisimpleRing R), IsArtinianRing R
tfae_2_to_3 : ∀ (a : IsArtinianRing R), ∃ (I : Ideal R), IsAtom I
⊢ [IsSemisimpleRing R, IsArtinianRing R, ∃ (I : Ideal R), IsAtom I].TFAE
have tfae_3_to_1 : ∀ (a : ∃ (I : Ideal R), IsAtom I), IsSemisimpleRing R
Tactic: tfae_have 3 → 1 := fun ⟨I, hI⟩ ↦ by
    have ⟨_, h⟩ := isSimpleRing_iff_isTwoSided_imp.mp ‹IsSimpleRing R›
    simp_rw [← isFullyInvariant_iff_isTwoSided] at h
    have := isSimpleModule_iff_isAtom.mpr hI
    obtain eq | eq := h _ (.isotypicComponent R R I)
    · exact (hI.bot_lt.not_ge <| (le_sSup <| by exact ⟨.refl ..⟩).trans_eq eq).elim
    exact .congr (.symm <| .trans (.ofEq _ _ eq) Submodule.topEquiv)
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (goal)
Goal:
R : Type u
inst : Ring R
⊢ IsSimpleRing R ∧ IsArtinianRing R ↔ IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R
have refine_1 : IsSimpleRing R ∧ IsArtinianRing R →
  IsSimpleRing R → IsArtinianRing R → IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R
Tactic: refine ⟨fun ⟨_, _⟩ ↦ ?_, fun ⟨_, _, _⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (goal)
Goal:
R : Type u
inst : Ring R
refine_1 :
  IsSimpleRing R ∧ IsArtinianRing R →
    IsSimpleRing R → IsArtinianRing R → IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R
⊢ IsSimpleRing R ∧ IsArtinianRing R ↔ IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R
have refine_2 : IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R →
  IsSemisimpleRing R → IsIsotypic R R → Nontrivial R → IsSimpleRing R ∧ IsArtinianRing R
Tactic: refine ⟨fun ⟨_, _⟩ ↦ ?_, fun ⟨_, _, _⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (hypothesis)
Goal:
R : Type u
inst : Ring R
h : IsSimpleRing R ∧ IsArtinianRing R
left : IsSimpleRing R
right : IsArtinianRing R
⊢ IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R
have this : IsSemisimpleRing R
Tactic: have := IsSimpleRing.isSemisimpleRing_iff_isArtinianRing.mpr ‹_›
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (hypothesis)
Goal:
R : Type u
inst : Ring R
h : IsSimpleRing R ∧ IsArtinianRing R
left : IsSimpleRing R
right : IsArtinianRing R
⊢ IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R
have this : IsSemisimpleRing R
Tactic: on_goal 1 => have := IsSimpleRing.isSemisimpleRing_iff_isArtinianRing.mpr ‹_›
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (goal)
Goal:
R : Type u
inst : Ring R
h : IsSimpleRing R ∧ IsArtinianRing R
left : IsSimpleRing R
right : IsArtinianRing R
this : IsSemisimpleRing R
⊢ IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R
have refine_1 : (Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤) ∧ IsArtinianRing R →
  (Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤) →
    IsSemisimpleRing R ∧ (∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤) ∧ Nontrivial R
Tactic: simp_rw [isIsotypic_iff_isFullyInvariant_imp_bot_or_top,
      isFullyInvariant_iff_isTwoSided, isSimpleRing_iff_isTwoSided_imp] at *
Cleared hypotheses: h, left
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (goal)
Goal:
R : Type u
inst : Ring R
h : IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R
left : IsSemisimpleRing R
left_1 : IsIsotypic R R
right : Nontrivial R
⊢ IsSimpleRing R ∧ IsArtinianRing R
have refine_2 : IsSemisimpleRing R ∧ (∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤) ∧ Nontrivial R →
  (∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤) →
    (Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤) ∧ IsArtinianRing R
Tactic: simp_rw [isIsotypic_iff_isFullyInvariant_imp_bot_or_top,
      isFullyInvariant_iff_isTwoSided, isSimpleRing_iff_isTwoSided_imp] at *
Cleared hypotheses: h, left_1
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (goal)
Goal:
R : Type u
inst : Ring R
right : IsArtinianRing R
this : IsSemisimpleRing R
h : (Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤) ∧ IsArtinianRing R
left : Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤
⊢ (∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤) ∧ Nontrivial R
have rwa : Nontrivial R ∧ ∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤
Tactic: rwa [and_comm]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : IsSimpleRing R
inst_2 : IsArtinianRing R
⊢ ∃ (n : ℕ) (_ : NeZero n) (I : Ideal R) (_ : IsSimpleModule R ↥I),
    Nonempty.{u + 1} (R ≃+* Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ)
have have : ∀ (n : ℕ) (hn : NeZero n) (S : Submodule R R) (hS : IsSimpleModule R ↥S) (e : R ≃ₗ[R] Fin n → ↥S),
  ∃ (n : ℕ) (_ : NeZero n) (I : Ideal R) (_ : IsSimpleModule R ↥I),
    Nonempty.{u + 1} (R ≃+* Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ)
Tactic: have ⟨n, hn, S, hS, ⟨e⟩⟩ := (isIsotypic R R).linearEquiv_fun
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : IsSimpleRing R
inst_2 : IsArtinianRing R
n : ℕ
hn : NeZero n
S : Submodule R R
hS : IsSimpleModule R ↥S
e : R ≃ₗ[R] Fin n → ↥S
⊢ ∃ (n : ℕ) (_ : NeZero n) (I : Ideal R) (_ : IsSimpleModule R ↥I),
    Nonempty.{u + 1} (R ≃+* Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ)
have refine : Rᵐᵒᵖ ≃+* Matrix (Fin n) (Fin n) (Module.End R ↥S)
Tactic: refine ⟨n, hn, S, hS, ⟨.trans (.opOp R) <| .trans (.op ?_) (.symm .mopMatrix)⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : IsSimpleRing R
inst_2 : IsArtinianRing R
⊢ ∃ (n : ℕ) (_ : NeZero n) (D : Type u) (x : DivisionRing D), Nonempty.{u + 1} (R ≃+* Matrix (Fin n) (Fin n) D)
have have : ∀ (n : ℕ) (hn : NeZero n) (I : Ideal R),
  IsSimpleModule R ↥I →
    ∀ (e : R ≃+* Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ),
      ∃ (n : ℕ) (_ : NeZero n) (D : Type u) (x : DivisionRing D), Nonempty.{u + 1} (R ≃+* Matrix (Fin n) (Fin n) D)
Tactic: have ⟨n, hn, I, _, ⟨e⟩⟩ := exists_ringEquiv_matrix_end_mulOpposite R
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (goal)
Goal:
R₀ : Type u_1
R : Type u
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Algebra R₀ R
inst_3 : IsSimpleRing R
inst_4 : IsArtinianRing R
⊢ ∃ (n : ℕ) (_ : NeZero n) (I : Ideal R) (_ : IsSimpleModule R ↥I),
    Nonempty.{u + 1} (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ)
have have : ∀ (n : ℕ) (hn : NeZero n) (S : Submodule R R) (hS : IsSimpleModule R ↥S) (e : R ≃ₗ[R] Fin n → ↥S),
  ∃ (n : ℕ) (_ : NeZero n) (I : Ideal R) (_ : IsSimpleModule R ↥I),
    Nonempty.{u + 1} (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ)
Tactic: have ⟨n, hn, S, hS, ⟨e⟩⟩ := (isIsotypic R R).linearEquiv_fun
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (goal)
Goal:
R₀ : Type u_1
R : Type u
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Algebra R₀ R
inst_3 : IsSimpleRing R
inst_4 : IsArtinianRing R
n : ℕ
hn : NeZero n
S : Submodule R R
hS : IsSimpleModule R ↥S
e : R ≃ₗ[R] Fin n → ↥S
⊢ ∃ (n : ℕ) (_ : NeZero n) (I : Ideal R) (_ : IsSimpleModule R ↥I),
    Nonempty.{u + 1} (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ)
have refine : Rᵐᵒᵖ ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥S)
Tactic: refine ⟨n, hn, S, hS, ⟨.trans (.opOp R₀ R) <| .trans (.op ?_) (.symm .mopMatrix)⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (goal)
Goal:
R₀ : Type u_1
R : Type u
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Algebra R₀ R
inst_3 : IsSimpleRing R
inst_4 : IsArtinianRing R
⊢ ∃ (n : ℕ) (_ : NeZero n) (D : Type u) (x : DivisionRing D) (x_1 : Algebra R₀ D),
    Nonempty.{u + 1} (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D)
have have : ∀ (n : ℕ) (hn : NeZero n) (I : Ideal R),
  IsSimpleModule R ↥I →
    ∀ (e : R ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ),
      ∃ (n : ℕ) (_ : NeZero n) (D : Type u) (x : DivisionRing D) (x_1 : Algebra R₀ D),
        Nonempty.{u + 1} (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D)
Tactic: have ⟨n, hn, I, _, ⟨e⟩⟩ := exists_algEquiv_matrix_end_mulOpposite R₀ R
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (goal)
Goal:
R₀ : Type u_1
R : Type u
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Algebra R₀ R
inst_3 : IsSimpleRing R
inst_4 : IsArtinianRing R
inst_5 : Module.Finite R₀ R
⊢ ∃ (n : ℕ) (_ : NeZero n) (D : Type u) (x : DivisionRing D) (x_1 : Algebra R₀ D) (_ : Module.Finite R₀ D),
    Nonempty.{u + 1} (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D)
have have : ∀ (n : ℕ) (hn : NeZero n) (I : Ideal R),
  IsSimpleModule R ↥I →
    ∀ (e : R ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ),
      ∃ (n : ℕ) (_ : NeZero n) (D : Type u) (x : DivisionRing D) (x_1 : Algebra R₀ D) (_ : Module.Finite R₀ D),
        Nonempty.{u + 1} (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D)
Tactic: have ⟨n, hn, I, _, ⟨e⟩⟩ := exists_algEquiv_matrix_end_mulOpposite R₀ R
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (hypothesis)
Goal:
R₀ : Type u_1
R : Type u
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Algebra R₀ R
inst_3 : IsSimpleRing R
inst_4 : IsArtinianRing R
inst_5 : Module.Finite R₀ R
n : ℕ
hn : NeZero n
I : Ideal R
w : IsSimpleModule R ↥I
e : R ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ
⊢ ∃ (n : ℕ) (_ : NeZero n) (D : Type u) (x : DivisionRing D) (x_1 : Algebra R₀ D) (_ : Module.Finite R₀ D),
    Nonempty.{u + 1} (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D)
have this : Module.Finite.{u_1, u} R₀ (Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ)
Tactic: have := Module.Finite.equiv e.toLinearEquiv
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (goal)
Goal:
R₀ : Type u_1
R : Type u
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Algebra R₀ R
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R₀ M
inst_5 : Module R M
inst_6 : IsScalarTower R₀ R M
inst_7 : IsSemisimpleModule R M
inst_8 : Module.Finite R M
⊢ ∃ (n : ℕ) (S : Fin n → Submodule R M) (d : Fin n → ℕ),
    (∀ (i : Fin n), IsSimpleModule.{u, v} R ↥(S i)) ∧
      (∀ (i : Fin n), NeZero (d i)) ∧
        Nonempty.{v + 1} (End R M ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (End R ↥(S i)))
have choose : ∀ (d : (c : (↑(isotypicComponents R M) : Type v)) → ℕ)
  (pos : ∀ (c : (↑(isotypicComponents R M) : Type v)), NeZero (d c))
  (S : (c : (↑(isotypicComponents R M) : Type v)) → Submodule R M),
  (∀ (c : (↑(isotypicComponents R M) : Type v)), S c ≤ (↑c : Submodule R M)) →
    ∀ (simple : ∀ (c : (↑(isotypicComponents R M) : Type v)), IsSimpleModule.{u, v} R ↥(S c))
      (e :
        ∀ (c : (↑(isotypicComponents R M) : Type v)),
          Nonempty.{v + 1} (↥(↑c : Submodule R M) ≃ₗ[R] Fin (d c) → ↥(S c))),
      ∃ (n : ℕ) (S : Fin n → Submodule R M) (d : Fin n → ℕ),
        (∀ (i : Fin n), IsSimpleModule.{u, v} R ↥(S i)) ∧
          (∀ (i : Fin n), NeZero (d i)) ∧
            Nonempty.{v + 1} (End R M ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (End R ↥(S i)))
Tactic: choose d pos S _ simple e using fun c : isotypicComponents R M ↦
    (IsIsotypic.isotypicComponents c.2).submodule_linearEquiv_fun
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (goal)
Goal:
R₀ : Type u_1
R : Type u
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Algebra R₀ R
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R₀ M
inst_5 : Module R M
inst_6 : IsScalarTower R₀ R M
inst_7 : IsSemisimpleModule R M
inst_8 : Module.Finite R M
⊢ ∃ (n : ℕ) (D : Fin n → Type v) (d : Fin n → ℕ) (x : (i : Fin n) → DivisionRing (D i)) (x_1 :
    (i : Fin n) → Algebra.{u_1, v} R₀ (D i)),
    (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty.{v + 1} (End R M ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))
have have : ∀ (n : ℕ) (S : Fin n → Submodule R M) (d : Fin n → ℕ),
  (∀ (i : Fin n), IsSimpleModule.{u, v} R ↥(S i)) →
    ∀ (hd : ∀ (i : Fin n), NeZero (d i))
      (e : End R M ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (End R ↥(S i))),
      ∃ (n : ℕ) (D : Fin n → Type v) (d : Fin n → ℕ) (x : (i : Fin n) → DivisionRing (D i)) (x_1 :
        (i : Fin n) → Algebra.{u_1, v} R₀ (D i)),
        (∀ (i : Fin n), NeZero (d i)) ∧
          Nonempty.{v + 1} (End R M ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))
Tactic: have ⟨n, S, d, _, hd, ⟨e⟩⟩ := exists_end_algEquiv_pi_matrix_end R₀ R M
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (goal)
Goal:
R₀ : Type u_1
R : Type u
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Algebra R₀ R
inst_3 : IsSemisimpleRing R
⊢ ∃ (n : ℕ) (D : Fin n → Type u) (d : Fin n → ℕ) (x : (i : Fin n) → DivisionRing (D i)) (x_1 :
    (i : Fin n) → Algebra.{u_1, u} R₀ (D i)),
    (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty.{u + 1} (R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))
have have : ∀ (n : ℕ) (S : Fin n → Ideal R) (d : Fin n → ℕ),
  (∀ (i : Fin n), IsSimpleModule R ↥(S i)) →
    ∀ (hd : ∀ (i : Fin n), NeZero (d i))
      (e : R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (Module.End R ↥(S i))ᵐᵒᵖ),
      ∃ (n : ℕ) (D : Fin n → Type u) (d : Fin n → ℕ) (x : (i : Fin n) → DivisionRing (D i)) (x_1 :
        (i : Fin n) → Algebra.{u_1, u} R₀ (D i)),
        (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty.{u + 1} (R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))
Tactic: have ⟨n, S, d, _, hd, ⟨e⟩⟩ := exists_algEquiv_pi_matrix_end_mulOpposite R₀ R
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (goal)
Goal:
R₀ : Type u_1
R : Type u
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Algebra R₀ R
inst_3 : IsSemisimpleRing R
inst_4 : Module.Finite R₀ R
⊢ ∃ (n : ℕ) (D : Fin n → Type u) (d : Fin n → ℕ) (x : (i : Fin n) → DivisionRing (D i)) (x_1 :
    (i : Fin n) → Algebra.{u_1, u} R₀ (D i)) (_ : ∀ (i : Fin n), Module.Finite.{u_1, u} R₀ (D i)),
    (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty.{u + 1} (R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))
have have : ∀ (n : ℕ) (D : Fin n → Type u) (d : Fin n → ℕ) (w : (i : Fin n) → DivisionRing (D i))
  (w_1 : (i : Fin n) → Algebra.{u_1, u} R₀ (D i)) (hd : ∀ (i : Fin n), NeZero (d i))
  (e : R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i)),
  ∃ (n : ℕ) (D : Fin n → Type u) (d : Fin n → ℕ) (x : (i : Fin n) → DivisionRing (D i)) (x_1 :
    (i : Fin n) → Algebra.{u_1, u} R₀ (D i)) (_ : ∀ (i : Fin n), Module.Finite.{u_1, u} R₀ (D i)),
    (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty.{u + 1} (R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))
Tactic: have ⟨n, D, d, _, _, hd, ⟨e⟩⟩ := exists_algEquiv_pi_matrix_divisionRing R₀ R
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (hypothesis)
Goal:
R₀ : Type u_1
R : Type u
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Algebra R₀ R
inst_3 : IsSemisimpleRing R
inst_4 : Module.Finite R₀ R
n : ℕ
D : Fin n → Type u
d : Fin n → ℕ
w : (i : Fin n) → DivisionRing (D i)
w_1 : (i : Fin n) → Algebra.{u_1, u} R₀ (D i)
hd : ∀ (i : Fin n), NeZero (d i)
e : R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i)
⊢ ∃ (n : ℕ) (D : Fin n → Type u) (d : Fin n → ℕ) (x : (i : Fin n) → DivisionRing (D i)) (x_1 :
    (i : Fin n) → Algebra.{u_1, u} R₀ (D i)) (_ : ∀ (i : Fin n), Module.Finite.{u_1, u} R₀ (D i)),
    (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty.{u + 1} (R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))
have this : Module.Finite.{u_1, u} R₀ ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))
Tactic: have := Module.Finite.equiv e.toLinearEquiv
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (goal)
Goal:
R₀ : Type u_1
R : Type u
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Algebra R₀ R
inst_3 : IsSemisimpleRing R
inst_4 : Module.Finite R₀ R
n : ℕ
D : Fin n → Type u
d : Fin n → ℕ
w : (i : Fin n) → DivisionRing (D i)
w_1 : (i : Fin n) → Algebra.{u_1, u} R₀ (D i)
hd : ∀ (i : Fin n), NeZero (d i)
e : R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i)
this : Module.Finite.{u_1, u} R₀ ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))
⊢ ∃ (n : ℕ) (D : Fin n → Type u) (d : Fin n → ℕ) (x : (i : Fin n) → DivisionRing (D i)) (x_1 :
    (i : Fin n) → Algebra.{u_1, u} R₀ (D i)) (_ : ∀ (i : Fin n), Module.Finite.{u_1, u} R₀ (D i)),
    (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty.{u + 1} (R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))
have refine : ∀ (i : Fin n), Module.Finite.{u_1, u} R₀ (D i)
Tactic: refine ⟨n, D, d, _, _, fun i ↦ ?_, hd, ⟨e⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.SimpleRing.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
inst_1 : IsSimpleRing R
⊢ Nontrivial R
have obtain : ∀ (x : R), Membership.mem (γ := TwoSidedIdeal R) ⊤ x → ∀ (hx : x ∉ ⊥), Nontrivial R
Tactic: obtain ⟨x, _, hx⟩ := SetLike.exists_of_lt (bot_lt_top : (⊥ : TwoSidedIdeal R) < ⊤)
-- Lean 4 proof step from Mathlib.RingTheory.SimpleRing.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
inst_1 : IsSimpleRing R
x : R
left : Membership.mem (γ := TwoSidedIdeal R) ⊤ x
hx : x ∉ ⊥
w w₁ : R
⊢ Nontrivial R
have h : x ≠ 0
Tactic: use x, 0, hx
-- Lean 4 proof step from Mathlib.RingTheory.SimpleRing.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
A : Type u_2
inst_1 : DivisionRing A
I : TwoSidedIdeal A
⊢ I = ⊥ ∨ I = ⊤
have rw : ¬I = ⊥ → 1 ∈ I
Tactic: rw [or_iff_not_imp_left, ← I.one_mem_iff]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleRing.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
A : Type u_2
inst_1 : DivisionRing A
I : TwoSidedIdeal A
H : ¬I = ⊥
⊢ 1 ∈ I
have obtain : ∀ (x : A) (hx1 : x ∈ I) (hx2 : x ≠ 0), 1 ∈ I
Tactic: obtain ⟨x, hx1, hx2 : x ≠ 0⟩ := SetLike.exists_of_lt (bot_lt_iff_ne_bot.mpr H : ⊥ < I)
-- Lean 4 proof step from Mathlib.RingTheory.SimpleRing.Basic (hypothesis)
Goal:
R : Type u_2
S : Type u_3
inst : NonAssocRing R
inst_1 : IsSimpleRing R
inst_2 : NonAssocSemiring S
f : R →+* S
h : Eq (α := TwoSidedIdeal R) (TwoSidedIdeal.ker f) ⊤
⊢ Eq.{u_3 + 1} (α := S) 0 1
have mem : Membership.mem (γ := TwoSidedIdeal R) (TwoSidedIdeal.ker f) 1
Tactic: have mem : 1 ∈ TwoSidedIdeal.ker f := h.symm ▸ TwoSidedIdeal.mem_top _
-- Lean 4 proof step from Mathlib.RingTheory.SimpleRing.Basic (goal)
Goal:
R : Type u_2
S : Type u_3
inst : NonAssocRing R
inst_1 : IsSimpleRing R
inst_2 : NonAssocSemiring S
f : R →+* S
h : Eq (α := TwoSidedIdeal R) (TwoSidedIdeal.ker f) ⊤
mem : Membership.mem (γ := TwoSidedIdeal R) (TwoSidedIdeal.ker f) 1
⊢ Eq.{u_3 + 1} (α := S) 0 1
have rwa : ∀ (mem : Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) 1 : S) (0 : S)), Eq.{u_3 + 1} (α := S) 0 1
Tactic: rwa [TwoSidedIdeal.mem_ker, map_one, eq_comm] at mem
Cleared hypotheses: mem
-- Lean 4 proof step from Mathlib.RingTheory.SimpleRing.Basic (goal)
Goal:
R : Type u_2
S : Type u_3
inst : NonAssocRing R
inst_1 : IsSimpleRing R
inst_2 : NonAssocSemiring S
f : R →+* S
h : Eq (α := TwoSidedIdeal R) (TwoSidedIdeal.ker f) ⊤
mem : Membership.mem (γ := TwoSidedIdeal R) (TwoSidedIdeal.ker f) 1
rwa : ∀ (mem : Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) 1 : S) (0 : S)), Eq.{u_3 + 1} (α := S) 0 1
⊢ Eq.{u_3 + 1} (α := S) 0 1
have rwa₁ : ∀ (mem : Eq.{u_3 + 1} (α := S) 1 0), Eq.{u_3 + 1} (α := S) 0 1
Tactic: rwa [TwoSidedIdeal.mem_ker, map_one, eq_comm] at mem
Cleared hypotheses: mem
-- Lean 4 proof step from Mathlib.RingTheory.SimpleRing.Basic (goal)
Goal:
R : Type u_2
S : Type u_3
inst : NonAssocRing R
inst_1 : IsSimpleRing R
inst_2 : NonAssocSemiring S
f : R →+* S
h : Eq (α := TwoSidedIdeal R) (TwoSidedIdeal.ker f) ⊤
mem : Membership.mem (γ := TwoSidedIdeal R) (TwoSidedIdeal.ker f) 1
rwa : ∀ (mem : Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) 1 : S) (0 : S)), Eq.{u_3 + 1} (α := S) 0 1
rwa₁ : ∀ (mem : Eq.{u_3 + 1} (α := S) 1 0), Eq.{u_3 + 1} (α := S) 0 1
⊢ Eq.{u_3 + 1} (α := S) 0 1
have rwa₂ : ∀ (mem : Eq.{u_3 + 1} (α := S) 0 1), Eq.{u_3 + 1} (α := S) 0 1
Tactic: rwa [TwoSidedIdeal.mem_ker, map_one, eq_comm] at mem
Cleared hypotheses: mem
-- Lean 4 proof step from Mathlib.RingTheory.SimpleRing.Congr (goal)
Goal:
R : Type u_1
inst : Ring R
e : TwoSidedIdeal R ≃o { I : Ideal R // I.IsTwoSided } := orderIsoIsTwoSided
⊢ IsSimpleRing R ↔ Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤
have simp_rw : (Nontrivial R ∧
    ∀ (a : Ideal R) (b : a.IsTwoSided),
      Eq (α := { I : Ideal R // I.IsTwoSided })
          ((e : (a : TwoSidedIdeal R) → { I : Ideal R // I.IsTwoSided })
              ((e.toEquiv (r := fun (x1 x2 : TwoSidedIdeal R) ↦ x1 ≤ x2) (s :=
                      fun (x1 x2 : { I : Ideal R // I.IsTwoSided }) ↦ x1 ≤ x2).symm :
                  (a : { I : Ideal R // I.IsTwoSided }) → TwoSidedIdeal R)
                (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsTwoSided) a b)) :
            { I : Ideal R // I.IsTwoSided })
          ((e : (a : TwoSidedIdeal R) → { I : Ideal R // I.IsTwoSided }) ⊥ : { I : Ideal R // I.IsTwoSided }) ∨
        Eq (α := { I : Ideal R // I.IsTwoSided })
          ((e : (a : TwoSidedIdeal R) → { I : Ideal R // I.IsTwoSided })
              ((e.toEquiv (r := fun (x1 x2 : TwoSidedIdeal R) ↦ x1 ≤ x2) (s :=
                      fun (x1 x2 : { I : Ideal R // I.IsTwoSided }) ↦ x1 ≤ x2).symm :
                  (a : { I : Ideal R // I.IsTwoSided }) → TwoSidedIdeal R)
                (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsTwoSided) a b)) :
            { I : Ideal R // I.IsTwoSided })
          ((e : (a : TwoSidedIdeal R) → { I : Ideal R // I.IsTwoSided }) ⊤ : { I : Ideal R // I.IsTwoSided })) ↔
  Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤
Tactic: simp_rw [isSimpleRing_iff, isSimpleOrder_iff, orderIsoRingCon.toEquiv.nontrivial_congr,
    RingCon.nontrivial_iff, e.forall_congr_left, Subtype.forall, ← e.injective.eq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleRing.Field (hypothesis)
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx2 : Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subring A) (Subring.center A) x) x hx1 ≠ 0
⊢ ∃ (b : ↥(Subring.center A)),
    Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subring A) (Subring.center A) x) x hx1 * b = 1
have hx1₁ : ∀ (g : A), g * x = x * g
Tactic: rw [Subring.mem_center_iff] at hx1
Cleared hypotheses: hx2
-- Lean 4 proof step from Mathlib.RingTheory.SimpleRing.Field (hypothesis)
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx1 : ∀ (g : A), g * x = x * g
hx2 : Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subring A) (Subring.center A) x) x hx1_1 ≠ 0
⊢ ∃ (b : ↥(Subring.center A)),
    Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subring A) (Subring.center A) x) x hx1_1 * b = 1
have hx2₁ : x ≠ 0
Tactic: replace hx2 : x ≠ 0 := by simpa [Subtype.ext_iff] using hx2
Cleared hypotheses: hx2