awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
ind : sSupIndep s
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule.{u_2, u_4} R ↥m
⊢ iSupIndep.{u_4 + 1, u_4} (ι := { x : Submodule R M // x ∈ s }) (Subtype.val (p := fun (x : Submodule R M) ↦ x ∈ s))

Tactic:
rw [sSupIndep_iff] at ind

Premises used: sSupIndep_iff
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
ind : sSupIndep s
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule.{u_2, u_4} R ↥m
ind₁ :
  iSupIndep.{u_4 + 1, u_4} (ι := { x : Submodule R M // x ∈ s }) (Subtype.val (p := fun (x : Submodule R M) ↦ x ∈ s))
⊢ SupSet.sSup s = ⊤

Tactic:
rw [sSupIndep_iff] at ind

Premises used: sSupIndep_iff
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
ind : sSupIndep s
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule.{u_2, u_4} R ↥m
ind₁ :
  iSupIndep.{u_4 + 1, u_4} (ι := { x : Submodule R M // x ∈ s }) (Subtype.val (p := fun (x : Submodule R M) ↦ x ∈ s))
sSup₁ : SupSet.sSup s = ⊤
⊢ ∀ m ∈ s, IsSimpleModule.{u_2, u_4} R ↥m

Tactic:
rw [sSupIndep_iff] at ind

Premises used: sSupIndep_iff
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
ind :
  iSupIndep.{u_4 + 1, u_4} (ι := { x : Submodule R M // x ∈ s }) (Subtype.val (p := fun (x : Submodule R M) ↦ x ∈ s))
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule.{u_2, u_4} R ↥m
rw :
  Eq.{u_4 + 1} (α := Submodule R M)
    (iSup (ι := { x : Submodule R M // x ∈ s }) (Subtype.val (p := fun (x : Submodule R M) ↦ x ∈ s))) ⊤
rw₁ : iSup (ι := { x : Submodule R M // x ∈ s }) (Subtype.val (p := fun (x : Submodule R M) ↦ x ∈ s)) = SupSet.sSup s
rw₂ rw₃ :
  Eq.{u_4 + 1} (α := Submodule R M)
    (iSup (ι := { x : Submodule R M // x ∈ s }) (Subtype.val (p := fun (x : Submodule R M) ↦ x ∈ s)))
    (⨆ (a : (↑s : Type u_4)), (↑a : Submodule R M))
⊢ Eq.{u_4 + 1} (α := Submodule R M)
    (LinearMap.range (R := R) (M := Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M)) (τ₁₂ := RingHom.id R)
      ((DFinsupp.lsum ℕ (M := fun (i : { x : Submodule R M // x ∈ s }) ↦ ↥(↑i : Submodule R M)) :
          (a : (i : { x : Submodule R M // x ∈ s }) → ↥(↑i : Submodule R M) →ₗ[R] M) →
            (Π₀ (i : { x : Submodule R M // x ∈ s }), ↥(↑i : Submodule R M)) →ₗ[R] M)
        fun (i : { x : Submodule R M // x ∈ s }) ↦ (↑i : Submodule R M).subtype))
    ⊤

Tactic:
rw [← Submodule.iSup_eq_range_dfinsupp_lsum, ← sSup, sSup_eq_iSup']

Premises used: Submodule.iSup_eq_range_dfinsupp_lsum, sSup_eq_iSup'
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
ind :
  iSupIndep.{u_4 + 1, u_4} (ι := { x : Submodule R M // x ∈ s }) (Subtype.val (p := fun (x : Submodule R M) ↦ x ∈ s))
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule.{u_2, u_4} R ↥m
⊢ M ≃ₗ[R] Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M)

Tactic:
exact .symm <| .trans (.ofInjective _ ind.dfinsupp_lsum_injective) <| .trans (.ofEq _ ⊤ <|
    by rw [← Submodule.iSup_eq_range_dfinsupp_lsum, ← sSup, sSup_eq_iSup']) Submodule.topEquiv
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
ind :
  iSupIndep.{u_4 + 1, u_4} (ι := { x : Submodule R M // x ∈ s }) (Subtype.val (p := fun (x : Submodule R M) ↦ x ∈ s))
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule.{u_2, u_4} R ↥m
⊢ M ≃ₗ[R] Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M)

Tactic:
classical
  exact .symm <| .trans (.ofInjective _ ind.dfinsupp_lsum_injective) <| .trans (.ofEq _ ⊤ <|
    by rw [← Submodule.iSup_eq_range_dfinsupp_lsum, ← sSup, sSup_eq_iSup']) Submodule.topEquiv
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ IsSemisimpleModule R M ↔
    ∃ (s : Set (Submodule R M)) (x : M ≃ₗ[R] Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M)),
      ∀ (m : (↑s : Type u_4)), IsSimpleModule.{u_2, u_4} R ↥(↑m : Submodule R M)

Tactic:
⟨fun _ ↦ ?_, fun ⟨s, e, h⟩ ↦ .congr e⟩

Premises used: _private.0.isSemisimpleModule_iff_exists_linearEquiv_dfinsupp.match_1, IsSemisimpleModule, Iff.intro, IsSemisimpleModule.congr
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
refine :
  IsSemisimpleModule R M →
    ∃ (s : Set (Submodule R M)) (x : M ≃ₗ[R] Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M)),
      ∀ (m : (↑s : Type u_4)), IsSimpleModule.{u_2, u_4} R ↥(↑m : Submodule R M)
⊢ IsSemisimpleModule R M ↔
    ∃ (s : Set (Submodule R M)) (x : M ≃ₗ[R] Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M)),
      ∀ (m : (↑s : Type u_4)), IsSimpleModule.{u_2, u_4} R ↥(↑m : Submodule R M)

Tactic:
refine ⟨fun _ ↦ ?_, fun ⟨s, e, h⟩ ↦ .congr e⟩
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : IsSemisimpleModule R M
have :
  ∀ (s : Set (Submodule R M)) (e : M ≃ₗ[R] Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M))
    (h : sSupIndep s ∧ ∀ (m : (↑s : Type u_4)), IsSimpleModule.{u_2, u_4} R ↥(↑m : Submodule R M)),
    ∃ (s : Set (Submodule R M)) (x : M ≃ₗ[R] Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M)),
      ∀ (m : (↑s : Type u_4)), IsSimpleModule.{u_2, u_4} R ↥(↑m : Submodule R M)
⊢ ∃ (s : Set (Submodule R M)) (x : M ≃ₗ[R] Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M)),
    ∀ (m : (↑s : Type u_4)), IsSimpleModule.{u_2, u_4} R ↥(↑m : Submodule R M)

Tactic:
have ⟨s, e, h⟩ := IsSemisimpleModule.exists_linearEquiv_dfinsupp R M
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h_1 : IsSemisimpleModule R M
s : Set (Submodule R M)
e : M ≃ₗ[R] Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M)
h : sSupIndep s ∧ ∀ (m : (↑s : Type u_4)), IsSimpleModule.{u_2, u_4} R ↥(↑m : Submodule R M)
⊢ ∃ (s : Set (Submodule R M)) (x : M ≃ₗ[R] Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M)),
    ∀ (m : (↑s : Type u_4)), IsSimpleModule.{u_2, u_4} R ↥(↑m : Submodule R M)

Tactic:
⟨s, e, h.2⟩

Premises used: And.right, Exists.intro
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h_1 : IsSemisimpleModule R M
s : Set (Submodule R M)
e : M ≃ₗ[R] Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M)
h : sSupIndep s ∧ ∀ (m : (↑s : Type u_4)), IsSimpleModule.{u_2, u_4} R ↥(↑m : Submodule R M)
⊢ ∃ (s : Set (Submodule R M)) (x : M ≃ₗ[R] Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M)),
    ∀ (m : (↑s : Type u_4)), IsSimpleModule.{u_2, u_4} R ↥(↑m : Submodule R M)

Tactic:
exact ⟨s, e, h.2⟩
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
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) (x : M ≃ₗ[R] Π₀ (i : Fin n), ↥(S i)),
    ∀ (i : Fin n), IsSimpleModule.{u_2, u_4} R ↥(S i)

Tactic:
have ⟨s, e, h, simple⟩ := IsSemisimpleModule.exists_linearEquiv_dfinsupp R M
  have := WellFoundedGT.finite_of_iSupIndep ((sSupIndep_iff _).mp h)
    fun S ↦ (S.1.nontrivial_iff_ne_bot).mp <| IsSimpleModule.nontrivial R S
  ⟨_, _, e.trans <| DirectSum.lequivCongrLeft R (Finite.equivFin s), fun _ ↦ simple _⟩

Premises used: DirectSum.lequivCongrLeft, IsSimpleModule.nontrivial, WellFoundedGT.finite_of_iSupIndep, Membership.mem, Exists, Set.Elem, _private.0.IsSemisimpleModule.exists_linearEquiv_fin_dfinsupp.match_1, sSupIndep_iff, Subtype, Nat.card, Finite.equivFin, Submodule.nontrivial_iff_ne_bot, Exists.intro, Iff.mp, Equiv.symm, IsSemisimpleModule.exists_linearEquiv_dfinsupp, Subtype.val, LinearEquiv.trans, DFunLike.coe
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι_1 : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M_1 : Type u_4
inst_2 : AddCommGroup M_1
inst_3 : Module R M_1
m : Submodule R M_1
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
ι : Type u_7
inst_6 : Finite ι
M : ι → Type u_6
inst_7 : (i : ι) → AddCommGroup (M i)
inst_8 : (i : ι) → Module.{u_2, u_6} R (M i)
inst_9 : ∀ (i : ι), IsSemisimpleModule.{u_2, u_6} R (M i)
simp_rw simp_rw₁ :
  Eq (α := Submodule R ((i : ι) → M i)) (⨆ (i : ι), range (R := R) (M := M i) (τ₁₂ := RingHom.id R) (single R M i)) ⊤
simp_rw₂ :
  Eq (α := Submodule R ((i : ι) → M i))
    (⨆ (i : ι), Submodule.map (R := R) (M := M i) (σ₁₂ := RingHom.id R) (single R M i) ⊤) ⊤
simp_rw₃ :
  Eq (α := Submodule R ((i : ι) → M i)) (Submodule.pi (φ := M) Set.univ fun (i : ι) ↦ ⊤ : Submodule R ((i : ι) → M i)) ⊤
⊢ Eq (α := Submodule R ((i : ι) → M i))
    (⨆ (i : ι),
      (fun (x : ι) ↦ (range (R := R) (M := M x) (τ₁₂ := RingHom.id R) (single R M x) : Submodule R ((i : ι) → M i))) i)
    ⊤

Tactic:
simp_rw [range_eq_map, Submodule.iSup_map_single, Submodule.pi_top]

Premises used: Submodule.pi_top, Submodule.iSup_map_single, LinearMap.range_eq_map
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι_1 : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M_1 : Type u_4
inst_2 : AddCommGroup M_1
inst_3 : Module R M_1
m : Submodule R M_1
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
ι : Type u_7
inst_6 : Finite ι
M : ι → Type u_6
inst_7 : (i : ι) → AddCommGroup (M i)
inst_8 : (i : ι) → Module.{u_2, u_6} R (M i)
inst_9 : ∀ (i : ι), IsSemisimpleModule.{u_2, u_6} R (M i)
⊢ IsSemisimpleModule R ((i : ι) → M i)

Tactic:
exact isSemisimpleModule_of_isSemisimpleModule_submodule' (p := (range <| single _ _ ·))
    (fun i ↦ .range _) (by simp_rw [range_eq_map, Submodule.iSup_map_single, Submodule.pi_top])

Premises used: isSemisimpleModule_of_isSemisimpleModule_submodule', IsSemisimpleModule.range
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι_1 : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M_1 : Type u_4
inst_2 : AddCommGroup M_1
inst_3 : Module R M_1
m : Submodule R M_1
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
ι : Type u_7
inst_6 : Finite ι
M : ι → Type u_6
inst_7 : (i : ι) → AddCommGroup (M i)
inst_8 : (i : ι) → Module.{u_2, u_6} R (M i)
inst_9 : ∀ (i : ι), IsSemisimpleModule.{u_2, u_6} R (M i)
⊢ IsSemisimpleModule R ((i : ι) → M i)

Tactic:
classical
  exact isSemisimpleModule_of_isSemisimpleModule_submodule' (p := (range <| single _ _ ·))
    (fun i ↦ .range _) (by simp_rw [range_eq_map, Submodule.iSup_map_single, Submodule.pi_top])

Premises used: isSemisimpleModule_of_isSemisimpleModule_submodule', IsSemisimpleModule.range
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
p q : Submodule R M
h : IsSemisimpleModule.{u_2, u_4} R ↥p
h_1 : IsSemisimpleModule.{u_2, u_4} R ↥q
f : Bool → Submodule R M := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ Submodule R M) q p t
rw : p ⊔ q = ⨆ (x : Bool), f x
rw₁ rw₂ : p ⊔ q = f true ⊔ f false
⊢ p ⊔ q = ⨆ (i : Bool), ⨆ (_ : Membership.mem (γ := Set Bool) Set.univ i), f i

Tactic:
rw [iSup_univ, iSup_bool_eq]

Premises used: iSup_bool_eq, iSup_univ
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
p q : Submodule R M
h : IsSemisimpleModule.{u_2, u_4} R ↥p
h_1 : IsSemisimpleModule.{u_2, u_4} R ↥q
f : Bool → Submodule R M := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ Submodule R M) q p t
rw : IsSemisimpleModule.{u_2, u_4} R ↥(⨆ (i : Bool), ⨆ (_ : Membership.mem (γ := Set Bool) Set.univ i), f i)
⊢ IsSemisimpleModule.{u_2, u_4} R ↥(p ⊔ q)

Tactic:
rw [show p ⊔ q = ⨆ i ∈ Set.univ, f i by rw [iSup_univ, iSup_bool_eq]]
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
p q : Submodule R M
h : IsSemisimpleModule.{u_2, u_4} R ↥p
h_1 : IsSemisimpleModule.{u_2, u_4} R ↥q
f : Bool → Submodule R M := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ Submodule R M) q p t
h_2 : Membership.mem (γ := Set Bool) Set.univ false
⊢ IsSemisimpleModule.{u_2, u_4} R ↥(f false)

Tactic:
assumption
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
p q : Submodule R M
h : IsSemisimpleModule.{u_2, u_4} R ↥p
h_1 : IsSemisimpleModule.{u_2, u_4} R ↥q
f : Bool → Submodule R M := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ Submodule R M) q p t
h_2 : Membership.mem (γ := Set Bool) Set.univ true
⊢ IsSemisimpleModule.{u_2, u_4} R ↥(f true)

Tactic:
assumption
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
p q : Submodule R M
h : IsSemisimpleModule.{u_2, u_4} R ↥p
h_1 : IsSemisimpleModule.{u_2, u_4} R ↥q
f : Bool → Submodule R M := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ Submodule R M) q p t
⊢ IsSemisimpleModule.{u_2, u_4} R ↥(⨆ (i : Bool), ⨆ (_ : Membership.mem (γ := Set Bool) Set.univ i), f i)

Tactic:
exact isSemisimpleModule_biSup_of_isSemisimpleModule_submodule
    (by rintro (_ | _) _ <;> assumption)

Premises used: isSemisimpleModule_biSup_of_isSemisimpleModule_submodule
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleRing R
h : IsSimpleModule R M
⊢ ∃ (I : Ideal R), Nonempty (M ≃ₗ[R] ↥I)

Tactic:
have ⟨J, _, ⟨e⟩⟩ := isSimpleModule_iff_quot_maximal.mp h
  have ⟨I, ⟨e'⟩⟩ := IsSemisimpleModule.exists_submodule_linearEquiv_quotient J
  ⟨I, ⟨e.trans e'.symm⟩⟩

Premises used: IsSemisimpleModule.exists_submodule_linearEquiv_quotient, LinearEquiv.symm, _private.0.IsSemisimpleRing.exists_linearEquiv_ideal_of_isSimpleModule.match_2, Membership.mem, Exists, Subtype, Nonempty.intro, isSimpleModule_iff_quot_maximal, _private.0.IsSemisimpleRing.exists_linearEquiv_ideal_of_isSimpleModule.match_1, LinearEquiv, Exists.intro, Iff.mp, Nonempty, RingHom.id, LinearEquiv.trans
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι_1 : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
ι : Type u_6
inst_6 : IsSemisimpleModule R M
⊢ IsSemisimpleModule R (ι →₀ M)

Tactic:
isSemisimpleModule_of_isSemisimpleModule_submodule'
    (fun _ ↦ .congr (LinearMap.quotKerEquivRange _).symm) Finsupp.iSup_lsingle_range

Premises used: LinearEquiv.symm, isSemisimpleModule_of_isSemisimpleModule_submodule', LinearMap.quotKerEquivRange, IsSemisimpleModule.congr, Finsupp.iSup_lsingle_range
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : IsSemisimpleRing R
⊢ IsSemisimpleModule R M

Tactic:
.congr (LinearMap.quotKerEquivOfSurjective _ <| Finsupp.linearCombination_id_surjective R M).symm

Premises used: Finsupp.linearCombination_id_surjective, LinearEquiv.symm, LinearMap.quotKerEquivOfSurjective, IsSemisimpleModule.congr
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : IsSemisimpleModule R M
⊢ IsCoatomic.{u_4} (Submodule R M)

Tactic:
isCoatomic_of_isAtomic_of_complementedLattice_of_isModular

Premises used: isCoatomic_of_isAtomic_of_complementedLattice_of_isModular
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι_1 : Type u_1
R_1 : Type u_2
S : Type u_3
inst : Ring R_1
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R_1 M
m : Submodule R_1 M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R_1 N
ι : Type u_7
inst_6 : Finite ι
R : ι → Type u_6
inst_7 : (i : ι) → Ring (R i)
inst_8 : ∀ (i : ι), IsSemisimpleRing.{u_6} (R i)
x : (i : ι) → Module ((i : ι) → R i) (R i) := fun (i : ι) ↦ Module.compHom (R := R i) (R i) (Pi.evalRingHom R i)
e : (i : ι) → LinearMap (R := (i : ι) → R i) (S := R i) (Pi.evalRingHom R i) (R i) (R i) :=
  fun (i : ι) ↦
    let __src : R i →+ R i := AddMonoidHom.id (R i);
    { toFun := (↑__src : ZeroHom (R i) (R i)).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ ∀ (i : ι), IsSemisimpleModule ((i : ι) → R i) (R i)

Tactic:
have (i : _) : IsSemisimpleModule (Π i, R i) (R i) :=
    ((e i).isSemisimpleModule_iff_of_bijective Function.bijective_id).mpr inferInstance
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι_1 : Type u_1
R_1 : Type u_2
S : Type u_3
inst : Ring R_1
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R_1 M
m : Submodule R_1 M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R_1 N
ι : Type u_7
inst_6 : Finite ι
R : ι → Type u_6
inst_7 : (i : ι) → Ring (R i)
inst_8 : ∀ (i : ι), IsSemisimpleRing.{u_6} (R i)
x : (i : ι) → Module ((i : ι) → R i) (R i) := fun (i : ι) ↦ Module.compHom (R := R i) (R i) (Pi.evalRingHom R i)
e : (i : ι) → LinearMap (R := (i : ι) → R i) (S := R i) (Pi.evalRingHom R i) (R i) (R i) :=
  fun (i : ι) ↦
    let __src : R i →+ R i := AddMonoidHom.id (R i);
    { toFun := (↑__src : ZeroHom (R i) (R i)).toFun, map_add' := ⋯, map_smul' := ⋯ }
this : ∀ (i : ι), IsSemisimpleModule ((i : ι) → R i) (R i)
⊢ IsSemisimpleRing ((i : ι) → R i)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
hR : IsSemisimpleRing R
hS : IsSemisimpleRing S
this_1 : Module (R × S) R := Module.compHom (R := R) R (RingHom.fst R S)
this : Module (R × S) S := Module.compHom (R := S) S (RingHom.snd R S)
_e₁ : LinearMap (R := R × S) (S := R) (RingHom.fst R S) R R :=
  let __src : R →+ R := AddMonoidHom.id R;
  { toFun := (↑__src : ZeroHom R R).toFun, map_add' := ⋯, map_smul' := ⋯ }
_e₂ : LinearMap (R := R × S) (S := S) (RingHom.snd R S) S S :=
  let __src : S →+ S := AddMonoidHom.id S;
  { toFun := (↑__src : ZeroHom S S).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ IsSemisimpleRing S

Tactic:
rw [IsSemisimpleRing, ← _e₁.isSemisimpleModule_iff_of_bijective Function.bijective_id] at hR

Premises used: Function.bijective_id, LinearMap.isSemisimpleModule_iff_of_bijective, IsSemisimpleRing
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
hR : IsSemisimpleRing R
hS : IsSemisimpleRing S
this_1 : Module (R × S) R := Module.compHom (R := R) R (RingHom.fst R S)
this : Module (R × S) S := Module.compHom (R := S) S (RingHom.snd R S)
_e₁ : LinearMap (R := R × S) (S := R) (RingHom.fst R S) R R :=
  let __src : R →+ R := AddMonoidHom.id R;
  { toFun := (↑__src : ZeroHom R R).toFun, map_add' := ⋯, map_smul' := ⋯ }
_e₂ : LinearMap (R := R × S) (S := S) (RingHom.snd R S) S S :=
  let __src : S →+ S := AddMonoidHom.id S;
  { toFun := (↑__src : ZeroHom S S).toFun, map_add' := ⋯, map_smul' := ⋯ }
hS₁ : IsSemisimpleRing S
⊢ let this : Module (R × S) R := Module.compHom (R := R) R (RingHom.fst R S);
  IsSemisimpleModule (R × S) R

Tactic:
rw [IsSemisimpleRing, ← _e₁.isSemisimpleModule_iff_of_bijective Function.bijective_id] at hR

Premises used: Function.bijective_id, LinearMap.isSemisimpleModule_iff_of_bijective, IsSemisimpleRing
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
hS : IsSemisimpleRing S
this_1 : Module (R × S) R := Module.compHom (R := R) R (RingHom.fst R S)
hR : IsSemisimpleModule (R × S) R
this : Module (R × S) S := Module.compHom (R := S) S (RingHom.snd R S)
_e₁ : LinearMap (R := R × S) (S := R) (RingHom.fst R S) R R :=
  let __src : R →+ R := AddMonoidHom.id R;
  { toFun := (↑__src : ZeroHom R R).toFun, map_add' := ⋯, map_smul' := ⋯ }
_e₂ : LinearMap (R := R × S) (S := S) (RingHom.snd R S) S S :=
  let __src : S →+ S := AddMonoidHom.id S;
  { toFun := (↑__src : ZeroHom S S).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ let this : Module (R × S) R := Module.compHom (R := R) R (RingHom.fst R S);
  IsSemisimpleModule (R × S) R

Tactic:
rw [IsSemisimpleRing, ← _e₂.isSemisimpleModule_iff_of_bijective Function.bijective_id] at hS

Premises used: Function.bijective_id, LinearMap.isSemisimpleModule_iff_of_bijective, IsSemisimpleRing
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
hS : IsSemisimpleRing S
this_1 : Module (R × S) R := Module.compHom (R := R) R (RingHom.fst R S)
hR : IsSemisimpleModule (R × S) R
this : Module (R × S) S := Module.compHom (R := S) S (RingHom.snd R S)
_e₁ : LinearMap (R := R × S) (S := R) (RingHom.fst R S) R R :=
  let __src : R →+ R := AddMonoidHom.id R;
  { toFun := (↑__src : ZeroHom R R).toFun, map_add' := ⋯, map_smul' := ⋯ }
_e₂ : LinearMap (R := R × S) (S := S) (RingHom.snd R S) S S :=
  let __src : S →+ S := AddMonoidHom.id S;
  { toFun := (↑__src : ZeroHom S S).toFun, map_add' := ⋯, map_smul' := ⋯ }
hR₁ :
  let this : Module (R × S) R := Module.compHom (R := R) R (RingHom.fst R S);
  IsSemisimpleModule (R × S) R
⊢ let this : Module (R × S) S := Module.compHom (R := S) S (RingHom.snd R S);
  IsSemisimpleModule (R × S) S

Tactic:
rw [IsSemisimpleRing, ← _e₂.isSemisimpleModule_iff_of_bijective Function.bijective_id] at hS

Premises used: Function.bijective_id, LinearMap.isSemisimpleModule_iff_of_bijective, IsSemisimpleRing
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
this_1 : Module (R × S) R := Module.compHom (R := R) R (RingHom.fst R S)
hR : IsSemisimpleModule (R × S) R
this : Module (R × S) S := Module.compHom (R := S) S (RingHom.snd R S)
hS : IsSemisimpleModule (R × S) S
_e₁ : LinearMap (R := R × S) (S := R) (RingHom.fst R S) R R :=
  let __src : R →+ R := AddMonoidHom.id R;
  { toFun := (↑__src : ZeroHom R R).toFun, map_add' := ⋯, map_smul' := ⋯ }
_e₂ : LinearMap (R := R × S) (S := S) (RingHom.snd R S) S S :=
  let __src : S →+ S := AddMonoidHom.id S;
  { toFun := (↑__src : ZeroHom S S).toFun, map_add' := ⋯, map_smul' := ⋯ }
rw :
  IsSemisimpleModule (R × S)
    ↥(LinearMap.range (LinearMap.inl (R × S) R S) ⊔ LinearMap.range (LinearMap.inr (R × S) R S) :
        Submodule (R × S) (R × S))
⊢ IsSemisimpleRing (R × S)

Tactic:
rw [IsSemisimpleRing, ← Submodule.topEquiv.isSemisimpleModule_iff_of_bijective
    (LinearEquiv.bijective _), ← LinearMap.sup_range_inl_inr]

Premises used: LinearEquiv.bijective, Submodule.topEquiv, LinearMap.sup_range_inl_inr, LinearEquiv.toLinearMap, LinearMap.isSemisimpleModule_iff_of_bijective, IsSemisimpleRing