awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
inst_1 : IsSimpleRing R
tfae_1_to_2 : ∀ (a : IsSemisimpleRing R), IsArtinianRing R
⊢ ∃ (I : Ideal R), IsAtom I

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
inst_1 : IsSimpleRing R
tfae_1_to_2 : ∀ (a : IsSemisimpleRing R), IsArtinianRing R
⊢ ∀ (a : IsArtinianRing R), ∃ (I : Ideal R), IsAtom I

Tactic:
2 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
inst_1 : IsSimpleRing R
tfae_1_to_2 : ∀ (a : IsSemisimpleRing R), IsArtinianRing R
⊢ ∀ (a : IsArtinianRing R), ∃ (I : Ideal R), IsAtom I

Tactic:
tfae_have 2 → 3 := fun _ ↦ IsAtomic.exists_atom _

Premises used: IsAtomic.exists_atom
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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
⊢ ∃ (I : Ideal R), IsAtom I

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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
⊢ ∀ (a : ∃ (I : Ideal R), IsAtom I), IsSemisimpleRing R

Tactic:
3 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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 : ∃ (I : Ideal R), IsAtom I
I : Ideal R
hI : IsAtom I
⊢ Nontrivial R

Tactic:
have ⟨_, h⟩ := isSimpleRing_iff_isTwoSided_imp.mp ‹IsSimpleRing R›
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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 : ∃ (I : Ideal R), IsAtom I
I : Ideal R
hI : IsAtom I
left : Nontrivial R
⊢ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤

Tactic:
have ⟨_, h⟩ := isSimpleRing_iff_isTwoSided_imp.mp ‹IsSimpleRing R›
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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), I.IsTwoSided → I = ⊥ ∨ I = ⊤
⊢ ∀ (I : Ideal R), Submodule.IsFullyInvariant I → I = ⊥ ∨ I = ⊤

Tactic:
simp_rw [← isFullyInvariant_iff_isTwoSided] at h

Premises used: isFullyInvariant_iff_isTwoSided
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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 = ⊤
⊢ IsSimpleModule R ↥I

Tactic:
have := isSimpleModule_iff_isAtom.mpr hI
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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
inr : ∀ (eq : Eq (α := Ideal R) (isotypicComponent R R ↥I : Submodule R R) (⊤ : Ideal R)), IsSemisimpleRing R
⊢ IsSemisimpleRing R

Tactic:
obtain eq | eq := h _ (.isotypicComponent R R I)

Premises used: Submodule.IsFullyInvariant.isotypicComponent, Membership.mem, Subtype
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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
eq : Eq (α := Ideal R) (isotypicComponent R R ↥I : Submodule R R) (⊥ : Ideal R)
⊢ Membership.mem (γ := Set (Ideal R)) {m : Submodule R R | Nonempty.{u + 1} (↥m ≃ₗ[R] ↥I)} I

Tactic:
⟨.refl ..⟩

Premises used: Set.Mem, setOf, Nonempty.intro, LinearEquiv.refl
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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
eq : Eq (α := Ideal R) (isotypicComponent R R ↥I : Submodule R R) (⊥ : Ideal R)
⊢ Membership.mem (γ := Set (Ideal R)) {m : Submodule R R | Nonempty.{u + 1} (↥m ≃ₗ[R] ↥I)} I

Tactic:
exact ⟨.refl ..⟩
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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
eq : Eq (α := Ideal R) (isotypicComponent R R ↥I : Submodule R R) (⊥ : Ideal R)
⊢ IsSemisimpleRing R

Tactic:
exact (hI.bot_lt.not_ge <| (le_sSup <| by exact ⟨.refl ..⟩).trans_eq eq).elim

Premises used: LE.le.trans_eq, False.elim, IsAtom.bot_lt, le_sSup, LT.lt.not_ge
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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
eq : Eq (α := Ideal R) (isotypicComponent R R ↥I : Submodule R R) (⊤ : Ideal R)
⊢ IsSemisimpleRing R

Tactic:
.congr (.symm <| .trans (.ofEq _ _ eq) Submodule.topEquiv)

Premises used: LinearEquiv.symm, Submodule.topEquiv, LinearEquiv.ofEq, IsSemisimpleModule.congr, LinearEquiv.trans
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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
eq : Eq (α := Ideal R) (isotypicComponent R R ↥I : Submodule R R) (⊤ : Ideal R)
⊢ IsSemisimpleRing R

Tactic:
exact .congr (.symm <| .trans (.ofEq _ _ eq) Submodule.topEquiv)
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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
⊢ ∀ (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)
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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
tfae_3_to_1 : ∀ (a : ∃ (I : Ideal R), IsAtom I), IsSemisimpleRing R
⊢ [IsSemisimpleRing R, IsArtinianRing R, ∃ (I : Ideal R), IsAtom I].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
inst_1 : IsSimpleRing R
⊢ IsSemisimpleRing R ↔ IsArtinianRing R

Tactic:
tfae.out 0 1

Premises used: IsSimpleRing.tfae, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
⊢ IsSimpleRing R ∧ IsArtinianRing R ↔ IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R

Tactic:
⟨fun ⟨_, _⟩ ↦ ?_, fun ⟨_, _, _⟩ ↦ ?_⟩

Premises used: Nontrivial, IsArtinianRing, IsSimpleRing, _private.0.isSimpleRing_isArtinianRing_iff.match_1, And, Iff.intro, _private.0.isSimpleRing_isArtinianRing_iff.match_2, IsSemisimpleRing, IsIsotypic
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
refine_1 :
  IsSimpleRing R ∧ IsArtinianRing R →
    IsSimpleRing R → IsArtinianRing R → IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R
refine_2 :
  IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R →
    IsSemisimpleRing R → IsIsotypic R R → Nontrivial R → IsSimpleRing R ∧ IsArtinianRing R
⊢ IsSimpleRing R ∧ IsArtinianRing R ↔ IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R

Tactic:
refine ⟨fun ⟨_, _⟩ ↦ ?_, fun ⟨_, _, _⟩ ↦ ?_⟩
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
h : IsSimpleRing R ∧ IsArtinianRing R
left : IsSimpleRing R
right : IsArtinianRing R
⊢ IsSemisimpleRing R

Tactic:
have := IsSimpleRing.isSemisimpleRing_iff_isArtinianRing.mpr ‹_›
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
h : IsSimpleRing R ∧ IsArtinianRing R
left : IsSimpleRing R
right : IsArtinianRing R
⊢ IsSemisimpleRing R

Tactic:
on_goal 1 => have := IsSimpleRing.isSemisimpleRing_iff_isArtinianRing.mpr ‹_›
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
h : IsSimpleRing R ∧ IsArtinianRing R
left : IsSimpleRing R
right : IsArtinianRing R
this : IsSemisimpleRing R
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
⊢ IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R

Tactic:
simp_rw [isIsotypic_iff_isFullyInvariant_imp_bot_or_top,
      isFullyInvariant_iff_isTwoSided, isSimpleRing_iff_isTwoSided_imp] at *

Premises used: isSimpleRing_iff_isTwoSided_imp, isFullyInvariant_iff_isTwoSided, isIsotypic_iff_isFullyInvariant_imp_bot_or_top
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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
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
⊢ IsSimpleRing R ∧ IsArtinianRing R

Tactic:
simp_rw [isIsotypic_iff_isFullyInvariant_imp_bot_or_top,
      isFullyInvariant_iff_isTwoSided, isSimpleRing_iff_isTwoSided_imp] at *

Premises used: isSimpleRing_iff_isTwoSided_imp, isFullyInvariant_iff_isTwoSided, isIsotypic_iff_isFullyInvariant_imp_bot_or_top
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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 = ⊤
rwa rwa₁ rwa₂ rwa₃ : Nontrivial R ∧ ∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤
⊢ (∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤) ∧ Nontrivial R

Tactic:
rwa [and_comm]

Premises used: and_comm
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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 = ⊤
⊢ IsSemisimpleRing R ∧ (∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤) ∧ Nontrivial R

Tactic:
exact ⟨this, by rwa [and_comm]⟩
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
left : IsSemisimpleRing R
right : Nontrivial R
h : IsSemisimpleRing R ∧ (∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤) ∧ Nontrivial R
left_1 : ∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤
⊢ (Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤) ∧ IsArtinianRing R

Tactic:
⟨⟨‹_›, ‹_›⟩, inferInstance⟩

Premises used: inferInstance, And.intro
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
left : IsSemisimpleRing R
right : Nontrivial R
h : IsSemisimpleRing R ∧ (∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤) ∧ Nontrivial R
left_1 : ∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤
⊢ (Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤) ∧ IsArtinianRing R

Tactic:
exact ⟨⟨‹_›, ‹_›⟩, inferInstance⟩
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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
⊢ IsSemisimpleRing R

Tactic:
(isSimpleRing_isArtinianRing_iff.mp ⟨‹_›, ‹_›⟩).1

Premises used: And.left, And.intro, Iff.mp, isSimpleRing_isArtinianRing_iff
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
inst_1 : IsSimpleRing R
inst_2 : IsArtinianRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
⊢ IsIsotypic R M

Tactic:
(isSimpleRing_isArtinianRing_iff.mp ⟨‹_›, ‹_›⟩).2.1.of_self M

Premises used: IsIsotypic.of_self, And.right, And.left, And.intro, Iff.mp, isSimpleRing_isArtinianRing_iff
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
inst_1 : IsSimpleRing R
inst_2 : IsArtinianRing R
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)ᵐᵒᵖ)
⊢ ∃ (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
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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)ᵐᵒᵖ)

Tactic:
⟨n, hn, S, hS, ⟨.trans (.opOp R) <| .trans (.op ?_) (.symm .mopMatrix)⟩⟩

Premises used: RingEquiv.op, RingEquiv.opOp, RingEquiv.mopMatrix, Nonempty.intro, Exists.intro, RingEquiv.trans, DFunLike.coe, RingEquiv.symm
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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
refine : Rᵐᵒᵖ ≃+* Matrix (Fin n) (Fin n) (Module.End R ↥S)
⊢ ∃ (n : ℕ) (_ : NeZero n) (I : Ideal R) (_ : IsSimpleModule R ↥I),
    Nonempty.{u + 1} (R ≃+* Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ)

Tactic:
refine ⟨n, hn, S, hS, ⟨.trans (.opOp R) <| .trans (.op ?_) (.symm .mopMatrix)⟩⟩
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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
⊢ Rᵐᵒᵖ ≃+* Matrix (Fin n) (Fin n) (Module.End R ↥S)

Tactic:
exact .trans (.moduleEndSelf R) <| .trans e.conjRingEquiv (endVecRingEquivMatrixEnd ..)
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
inst_1 : IsSimpleRing R
inst_2 : IsArtinianRing R
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)
⊢ ∃ (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
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
inst_1 : IsSimpleRing R
inst_2 : IsArtinianRing R
n : ℕ
hn : NeZero n
I : Ideal R
w : 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:
⟨n, hn, _, _, ⟨e⟩⟩

Premises used: Nonempty.intro, Exists.intro
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
inst_1 : IsSimpleRing R
inst_2 : IsArtinianRing R
n : ℕ
hn : NeZero n
I : Ideal R
w : 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:
exact ⟨n, hn, _, _, ⟨e⟩⟩
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
inst_1 : IsSimpleRing R
inst_2 : IsArtinianRing R
n : ℕ
hn : NeZero n
I : Ideal R
w : 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:
classical exact ⟨n, hn, _, _, ⟨e⟩⟩
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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
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)ᵐᵒᵖ)
⊢ ∃ (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
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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)ᵐᵒᵖ)

Tactic:
⟨n, hn, S, hS, ⟨.trans (.opOp R₀ R) <| .trans (.op ?_) (.symm .mopMatrix)⟩⟩

Premises used: AlgEquiv.symm, AlgEquiv.opOp, AlgEquiv.op, Nonempty.intro, AlgEquiv.trans, Exists.intro, AlgEquiv.mopMatrix, DFunLike.coe
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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
refine : Rᵐᵒᵖ ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥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:
refine ⟨n, hn, S, hS, ⟨.trans (.opOp R₀ R) <| .trans (.op ?_) (.symm .mopMatrix)⟩⟩
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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
⊢ Rᵐᵒᵖ ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥S)

Tactic:
exact .trans (.moduleEndSelf R₀) <| .trans (e.conjAlgEquiv R₀) (endVecAlgEquivMatrixEnd ..)
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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
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)
⊢ ∃ (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
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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
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),
    Nonempty.{u + 1} (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D)

Tactic:
⟨n, hn, _, _, _, ⟨e⟩⟩

Premises used: Nonempty.intro, Exists.intro
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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
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),
    Nonempty.{u + 1} (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D)

Tactic:
exact ⟨n, hn, _, _, _, ⟨e⟩⟩
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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
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),
    Nonempty.{u + 1} (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D)

Tactic:
classical exact ⟨n, hn, _, _, _, ⟨e⟩⟩
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
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
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)
⊢ ∃ (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