awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
n : ℕ
hn : NeZero n
I : Ideal R
w : IsSimpleModule R ↥I
e : R ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ
⊢ Module.Finite.{u_1, u} R₀ (Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ)

Tactic:
have := Module.Finite.equiv e.toLinearEquiv
-- 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
n : ℕ
hn : NeZero n
I : Ideal R
w : IsSimpleModule R ↥I
e : R ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ
this : Module.Finite.{u_1, u} 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:
⟨n, hn, _, _, _, .of_surjective
    (Matrix.entryLinearMap R₀ _ (0 : Fin n) (0 : Fin n)) fun f ↦ ⟨fun _ _ ↦ f, rfl⟩, ⟨e⟩⟩

Premises used: Module.Finite.of_surjective, Nonempty.intro, Matrix.entryLinearMap, Exists.intro, OfNat.ofNat, rfl
-- 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
n : ℕ
hn : NeZero n
I : Ideal R
w : IsSimpleModule R ↥I
e : R ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ
this : Module.Finite.{u_1, u} 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:
exact ⟨n, hn, _, _, _, .of_surjective
    (Matrix.entryLinearMap R₀ _ (0 : Fin n) (0 : Fin n)) fun f ↦ ⟨fun _ _ ↦ f, rfl⟩, ⟨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
n : ℕ
hn : NeZero n
I : Ideal R
w : IsSimpleModule R ↥I
e : R ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ
this : Module.Finite.{u_1, u} 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:
classical exact ⟨n, hn, _, _, _, .of_surjective
    (Matrix.entryLinearMap R₀ _ (0 : Fin n) (0 : Fin n)) fun f ↦ ⟨fun _ _ ↦ f, rfl⟩, ⟨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
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
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)))
⊢ ∃ (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

Premises used: IsIsotypic.isotypicComponents, IsIsotypic.submodule_linearEquiv_fun, Subtype.property
-- 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
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
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
h : ∀ (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:
⟨_, _, _, fun _ ↦ simple _, fun _ ↦ pos _, ⟨.trans (endAlgEquiv R₀ R M) <| .trans
    (.piCongrRight fun c ↦ ((e c).some.conjAlgEquiv R₀).trans (endVecAlgEquivMatrixEnd ..)) <|
    (.piCongrLeft' R₀ _ (Finite.equivFin _))⟩⟩

Premises used: endVecAlgEquivMatrixEnd, LinearEquiv.conjAlgEquiv, Membership.mem, Subtype, Nonempty.some, AlgEquiv.piCongrRight, Nonempty.intro, AlgEquiv.trans, Finite.equivFin, And.intro, Exists.intro, Fin, IsSemisimpleModule.endAlgEquiv, AlgEquiv.piCongrLeft'
-- 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
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
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
h : ∀ (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:
exact ⟨_, _, _, fun _ ↦ simple _, fun _ ↦ pos _, ⟨.trans (endAlgEquiv R₀ R M) <| .trans
    (.piCongrRight fun c ↦ ((e c).some.conjAlgEquiv R₀).trans (endVecAlgEquivMatrixEnd ..)) <|
    (.piCongrLeft' R₀ _ (Finite.equivFin _))⟩⟩
-- 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
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
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
h : ∀ (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:
classical exact ⟨_, _, _, fun _ ↦ simple _, fun _ ↦ pos _, ⟨.trans (endAlgEquiv R₀ R M) <| .trans
    (.piCongrRight fun c ↦ ((e c).some.conjAlgEquiv R₀).trans (endVecAlgEquivMatrixEnd ..)) <|
    (.piCongrLeft' R₀ _ (Finite.equivFin _))⟩⟩
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
inst_4 : 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 ≃+* ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (End R ↥(S i))))

Tactic:
have ⟨n, S, d, hS, hd, ⟨e⟩⟩ := exists_end_algEquiv_pi_matrix_end ℕ R M; ⟨n, S, d, hS, hd, ⟨e⟩⟩

Premises used: Exists, Nonempty.intro, _private.0.IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_end.match_1, And, Nat, And.intro, AlgEquiv.toRingEquiv, Exists.intro, IsSemisimpleModule.exists_end_algEquiv_pi_matrix_end, Nonempty, Module.End, RingEquiv
-- 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
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
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))
⊢ ∃ (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
-- 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
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 → ℕ
left : ∀ (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:
⟨n, _, d, inferInstance, inferInstance, hd, ⟨e⟩⟩

Premises used: inferInstance, Nonempty.intro, And.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
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 → ℕ
left : ∀ (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:
exact ⟨n, _, d, inferInstance, inferInstance, hd, ⟨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
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 → ℕ
left : ∀ (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:
classical exact ⟨n, _, d, inferInstance, inferInstance, hd, ⟨e⟩⟩
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
inst_4 : Module.Finite R M
⊢ ∃ (n : ℕ) (D : Fin n → Type v) (d : Fin n → ℕ) (x : (i : Fin n) → DivisionRing (D i)),
    (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty.{v + 1} (End R M ≃+* ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i)))

Tactic:
have ⟨n, D, d, _, _, hd, ⟨e⟩⟩ := exists_end_algEquiv_pi_matrix_divisionRing ℕ R M
  ⟨n, D, d, _, hd, ⟨e⟩⟩

Premises used: Exists, _private.0.IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_divisionRing.match_1, Nonempty.intro, And, Nat, And.intro, AlgEquiv.toRingEquiv, Exists.intro, Nonempty, IsSemisimpleModule.exists_end_algEquiv_pi_matrix_divisionRing, Module.End, RingEquiv
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
inst_4 : Module.Finite R M
⊢ IsSemisimpleRing.{v} (End R M)

Tactic:
have ⟨_, _, _, _, _, ⟨e⟩⟩ := exists_end_ringEquiv_pi_matrix_divisionRing R M
  e.symm.isSemisimpleRing

Premises used: IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_divisionRing, IsSemisimpleRing, RingEquiv.isSemisimpleRing, Module.End, _private.0.IsSemisimpleRing.moduleEnd.match_1, RingEquiv.symm
-- 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 : IsSemisimpleRing R
⊢ ∃ (n : ℕ) (S : Fin n → Ideal R) (d : Fin n → ℕ),
    (∀ (i : Fin n), IsSimpleModule R ↥(S i)) ∧
      (∀ (i : Fin n), NeZero (d i)) ∧
        Nonempty.{u + 1} (R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (Module.End R ↥(S i))ᵐᵒᵖ)

Tactic:
have ⟨n, S, d, hS, hd, ⟨e⟩⟩ := IsSemisimpleModule.exists_end_algEquiv_pi_matrix_end R₀ R R
  ⟨n, S, d, hS, hd, ⟨.trans (.opOp R₀ R) <| .trans (.op <| .trans (.moduleEndSelf R₀) e) <|
    .trans (.piMulOpposite _ _) (.piCongrRight fun _ ↦ .symm .mopMatrix)⟩⟩

Premises used: AlgEquiv.symm, Matrix, AlgEquiv.opOp, Membership.mem, Exists, AlgEquiv.op, Subtype, AlgEquiv.piCongrRight, Nonempty.intro, And, AlgEquiv.trans, AlgEquiv, _private.0.IsSemisimpleRing.exists_algEquiv_pi_matrix_end_mulOpposite.match_1, And.intro, Exists.intro, AlgEquiv.moduleEndSelf, IsSemisimpleModule.exists_end_algEquiv_pi_matrix_end, Nonempty, Module.End, AlgEquiv.mopMatrix, Fin, DFunLike.coe, AlgEquiv.piMulOpposite
-- 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 : IsSemisimpleRing R
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))
⊢ ∃ (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
-- 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 : IsSemisimpleRing R
n : ℕ
S : Fin n → Ideal R
d : Fin n → ℕ
left : ∀ (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:
⟨n, _, d, inferInstance, inferInstance, hd, ⟨e⟩⟩

Premises used: inferInstance, Nonempty.intro, And.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 : IsSemisimpleRing R
n : ℕ
S : Fin n → Ideal R
d : Fin n → ℕ
left : ∀ (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:
exact ⟨n, _, d, inferInstance, inferInstance, hd, ⟨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 : IsSemisimpleRing R
n : ℕ
S : Fin n → Ideal R
d : Fin n → ℕ
left : ∀ (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:
classical exact ⟨n, _, d, inferInstance, inferInstance, hd, ⟨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 : IsSemisimpleRing R
inst_4 : Module.Finite R₀ R
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))
⊢ ∃ (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
-- 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 : 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)
⊢ 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
-- 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 : 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))

Tactic:
⟨n, D, d, _, _, fun i ↦ ?_, hd, ⟨e⟩⟩

Premises used: Nonempty.intro, And.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 : 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))
refine : ∀ (i : Fin n), Module.Finite.{u_1, u} R₀ (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:
refine ⟨n, D, d, _, _, fun i ↦ ?_, hd, ⟨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 : 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))
i : Fin n
l : ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i)) →ₗ[R₀] D i :=
  Matrix.entryLinearMap R₀ (D i) 0 0 ∘ₗ LinearMap.proj (φ := fun (i : Fin n) ↦ Matrix (Fin (d i)) (Fin (d i)) (D i)) i
x : D i
⊢ ((l : (a : (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i)) → D i) fun (j : Fin n) (x_1 x_2 : Fin (d j)) ↦
      Function.update (β := D) (fun (x : Fin n) ↦ 0) i x j) =
    x

Tactic:
simp [l]
-- 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 : 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))
i : Fin n
l : ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i)) →ₗ[R₀] D i :=
  Matrix.entryLinearMap R₀ (D i) 0 0 ∘ₗ LinearMap.proj (φ := fun (i : Fin n) ↦ Matrix (Fin (d i)) (Fin (d i)) (D i)) i
⊢ Module.Finite.{u_1, u} R₀ (D i)

Tactic:
exact .of_surjective l fun x ↦ ⟨fun j _ _ ↦ Function.update (fun _ ↦ 0) i x j, by simp [l]⟩