awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
c : Submodule R M
hc : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) c
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this_1 : IsSemisimpleModule.{u_2, u} R ↥c
this_2 : IsSemisimpleModule.{u_2, u} R ↥(c ⊓ sSup s)
this_3 : ∀ (c : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑c : Submodule R M)
S : Submodule R M
le : S ≤ c ⊓ sSup s
right : IsSimpleModule.{u_2, u} R ↥S
c' : Submodule R M
hc' : c' ∈ s
S' : Submodule R M
le' : S' ≤ c'
e : ↥S ≃ₗ[R] ↥S'
this : IsSimpleModule.{u_2, u} R ↥S'
rw : Membership.mem (γ := Set (Submodule R M)) {isotypicComponent R M ↥S} (isotypicComponent R M ↥S')
⊢ Membership.mem (γ := Set (Submodule R M)) {c} c'

Tactic:
rw [eq_isotypicComponent_of_le hc (le.trans inf_le_left), eq_isotypicComponent_of_le hc'.1 le']

Premises used: eq_isotypicComponent_of_le, And.left, inf_le_left, LE.le.trans
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
c : Submodule R M
hc : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) c
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this_1 : IsSemisimpleModule.{u_2, u} R ↥c
this_2 : IsSemisimpleModule.{u_2, u} R ↥(c ⊓ sSup s)
this_3 : ∀ (c : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑c : Submodule R M)
S : Submodule R M
le : S ≤ c ⊓ sSup s
right : IsSimpleModule.{u_2, u} R ↥S
c' : Submodule R M
hc' : c' ∈ s
S' : Submodule R M
le' : S' ≤ c'
e : ↥S ≃ₗ[R] ↥S'
this : IsSimpleModule.{u_2, u} R ↥S'
⊢ Membership.mem (γ := Set (Submodule R M)) {isotypicComponent R M ↥S} (isotypicComponent R M ↥S')

Tactic:
e.symm.isotypicComponent_eq

Premises used: LinearEquiv.symm, Set.Mem, setOf, Set.singleton, LinearEquiv.isotypicComponent_eq
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
c : Submodule R M
hc : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) c
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this_1 : IsSemisimpleModule.{u_2, u} R ↥c
this_2 : IsSemisimpleModule.{u_2, u} R ↥(c ⊓ sSup s)
this_3 : ∀ (c : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑c : Submodule R M)
S : Submodule R M
le : S ≤ c ⊓ sSup s
right : IsSimpleModule.{u_2, u} R ↥S
c' : Submodule R M
hc' : c' ∈ s
S' : Submodule R M
le' : S' ≤ c'
e : ↥S ≃ₗ[R] ↥S'
this : IsSimpleModule.{u_2, u} R ↥S'
⊢ Membership.mem (γ := Set (Submodule R M)) {isotypicComponent R M ↥S} (isotypicComponent R M ↥S')

Tactic:
exact e.symm.isotypicComponent_eq

Premises used: LinearEquiv.symm, LinearEquiv.isotypicComponent_eq
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R₀ : Type u_1
R : Type u_2
M : Type u
N : Type u_3
S : Type u_4
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Algebra R₀ R
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : AddCommGroup S
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R S
inst_9 : IsSimpleModule R S
inst_10 : IsNoetherian R M
⊢ Finite.{u + 1} (↑(isotypicComponents R M) : Type u)

Tactic:
Set.finite_coe_iff.mpr <| WellFoundedGT.finite_of_sSupIndep (sSupIndep_isotypicComponents R M)

Premises used: Iff.mpr, WellFoundedGT.finite_of_sSupIndep, sSupIndep_isotypicComponents, Set.finite_coe_iff
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
S : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup S
inst_3 : Module R M
inst_4 : Module R S
inst_5 : IsSimpleModule R S
h : Eq (α := Submodule R M) (isotypicComponent R M S) ⊤
⊢ IsIsotypicOfType R M S

Tactic:
fun m _ ↦ have ⟨_, ⟨e⟩, ⟨e'⟩⟩ := m.linearEquiv_of_sSup_eq_top _ h; ⟨e'.trans e⟩

Premises used: _private.0.IsIsotypicOfType.isotypicComponent.match_1, setOf, Membership.mem, Subtype, Nonempty.intro, Submodule.linearEquiv_of_sSup_eq_top, LinearEquiv, IsIsotypicOfType, Nonempty, RingHom.id, LinearEquiv.trans
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
S : Submodule R M
inst_5 : IsSimpleModule.{u_2, u} R ↥S
f : M →ₗ[R] N
rw : (f ∘ₗ S.subtype).range
| map f S

Tactic:
rw [← S.range_subtype, ← LinearMap.range_comp]

Premises used: LinearMap.range_comp, Submodule.range_subtype
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
S : Submodule R M
inst_5 : IsSimpleModule.{u_2, u} R ↥S
f : M →ₗ[R] N
conv_lhs : (f ∘ₗ S.subtype).range ≤ isotypicComponent.{u_3, u_2, u} R N ↥S
⊢ map f S ≤ isotypicComponent.{u_3, u_2, u} R N ↥S

Tactic:
conv_lhs => rw [← S.range_subtype, ← LinearMap.range_comp]

Premises used: LinearMap.range_comp, Submodule.range_subtype
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
S : Submodule R M
inst_5 : IsSimpleModule.{u_2, u} R ↥S
f : M →ₗ[R] N
inl :
  ∀ (inj : Function.Injective.{u + 1, u_3 + 1} (α := ↥S) (β := N) (⇑(f ∘ₗ S.subtype) : (a : ↥S) → N)),
    (f ∘ₗ S.subtype).range ≤ isotypicComponent.{u_3, u_2, u} R N ↥S
inr : ∀ (eq : f ∘ₗ S.subtype = 0), (f ∘ₗ S.subtype).range ≤ isotypicComponent.{u_3, u_2, u} R N ↥S
⊢ (f ∘ₗ S.subtype).range ≤ isotypicComponent.{u_3, u_2, u} R N ↥S

Tactic:
obtain inj | eq := (f ∘ₗ S.subtype).injective_or_eq_zero

Premises used: LinearMap.comp, Submodule.subtype, LinearMap.injective_or_eq_zero
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
S : Submodule R M
inst_5 : IsSimpleModule.{u_2, u} R ↥S
f : M →ₗ[R] N
inj : Function.Injective.{u + 1, u_3 + 1} (α := ↥S) (β := N) (⇑(f ∘ₗ S.subtype) : (a : ↥S) → N)
⊢ (f ∘ₗ S.subtype).range ≤ isotypicComponent.{u_3, u_2, u} R N ↥S

Tactic:
le_sSup ⟨.symm <| .ofInjective _ inj⟩

Premises used: LinearEquiv.symm, Set.Mem, Nonempty.intro, LinearEquiv.ofInjective, le_sSup
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
S : Submodule R M
inst_5 : IsSimpleModule.{u_2, u} R ↥S
f : M →ₗ[R] N
inj : Function.Injective.{u + 1, u_3 + 1} (α := ↥S) (β := N) (⇑(f ∘ₗ S.subtype) : (a : ↥S) → N)
⊢ (f ∘ₗ S.subtype).range ≤ isotypicComponent.{u_3, u_2, u} R N ↥S

Tactic:
exact le_sSup ⟨.symm <| .ofInjective _ inj⟩
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
S : Submodule R M
inst_5 : IsSimpleModule.{u_2, u} R ↥S
f : M →ₗ[R] N
eq : f ∘ₗ S.subtype = 0
inr :
  LE.le (α := Submodule R N) (LinearMap.range.{u_2, u_2, u, u_3} (R := R) (M := ↥S) (τ₁₂ := RingHom.id R) 0)
    (isotypicComponent.{u_3, u_2, u} R N ↥S)
inr₁ : LE.le (α := Submodule R N) ⊥ (isotypicComponent.{u_3, u_2, u} R N ↥S)
⊢ (f ∘ₗ S.subtype).range ≤ isotypicComponent.{u_3, u_2, u} R N ↥S

Tactic:
simp_rw [eq, LinearMap.range_zero, bot_le]

Premises used: LinearMap.range_zero, bot_le
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
N : Type u_3
S : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup S
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R S
inst_7 : IsSimpleModule R S
f : M →ₗ[R] N
⊢ isotypicComponent R M S ≤ Submodule.comap f (isotypicComponent R N S)

Tactic:
sSup_le fun m ⟨e⟩ ↦ Submodule.map_le_iff_le_comap.mp <|
    have := IsSimpleModule.congr e
    (m.map_le_isotypicComponent f).trans_eq e.isotypicComponent_eq

Premises used: LE.le.trans_eq, Set.Mem, LE.le, isotypicComponent, Submodule.map_le_isotypicComponent, Submodule.comap, Iff.mp, Submodule.map_le_iff_le_comap, sSup_le, _private.0.instIsSemisimpleModuleSubtypeMemSubmoduleIsotypicComponent.match_2, LinearEquiv.isotypicComponent_eq, IsSimpleModule.congr
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_5
inst : Semiring R
I : Ideal R
⊢ Submodule.IsFullyInvariant I ↔ I.IsTwoSided

Tactic:
simpa only [Submodule.IsFullyInvariant, ← MulOpposite.opEquiv.trans (RingEquiv.moduleEndSelf R
    |>.toEquiv) |>.forall_congr_right, SetLike.le_def, I.isTwoSided_iff] using forall_comm

Premises used: RingEquiv.toEquiv, RingEquiv.moduleEndSelf, MulOpposite.opEquiv, Equiv.trans, SetLike.le_def, forall_comm, Ideal.isTwoSided_iff, Equiv.forall_congr_right, Submodule.IsFullyInvariant
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_5
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : Submodule R M
⊢ Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) m ↔ m.IsFullyInvariant

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Submodule.IsFullyInvariant
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R₀ : Type u_1
R : Type u_2
M : Type u
N_1 : Type u_3
S : Type u_4
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Algebra R₀ R
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N_1
inst_5 : AddCommGroup S
inst_6 : Module R M
inst_7 : Module R N_1
inst_8 : Module R S
inst_9 : IsSimpleModule R S
ι : Type u_5
inst_10 : DecidableEq ι
N : ι → Submodule R M
ind : iSupIndep N
iSup_top : Eq.{u + 1} (α := Submodule R M) (⨆ (i : ι), N i) ⊤
invar : ∀ (i : ι), (N i).IsFullyInvariant
f : Module.End R M
x_1 : M
i : ι
x : M
h : x ∈ N i
⊢ (fun (x : M) ↦
      Eq (α := M)
        (((fun (f : (i : ι) → Module.End R ↥(N i)) ↦
                  (↑(ind.linearEquiv iSup_top) : (Π₀ (i : ι), ↥(N i)) →ₗ[R] M) ∘ₗ
                    DFinsupp.mapRange.linearMap (β₁ := fun (i : ι) ↦ ↥(N i)) (β₂ := fun (i : ι) ↦ ↥(N i)) f ∘ₗ
                      (↑(ind.linearEquiv iSup_top).symm : M →ₗ[R] Π₀ (i : ι), ↥(N i)))
                ((fun (f : Module.End R M) (i : ι) ↦ LinearMap.restrict f ⋯) f) :
              (a : M) → M)
            x :
          M)
        ((f : (a : M) → M) x : M))
    x

Tactic:
simp [ind.linearEquiv_symm_apply _ h]

Premises used: iSupIndep.linearEquiv_symm_apply
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R₀ : Type u_1
R : Type u_2
M : Type u
N_1 : Type u_3
S : Type u_4
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Algebra R₀ R
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N_1
inst_5 : AddCommGroup S
inst_6 : Module R M
inst_7 : Module R N_1
inst_8 : Module R S
inst_9 : IsSimpleModule R S
ι : Type u_5
inst_10 : DecidableEq ι
N : ι → Submodule R M
ind : iSupIndep N
iSup_top : Eq.{u + 1} (α := Submodule R M) (⨆ (i : ι), N i) ⊤
invar : ∀ (i : ι), (N i).IsFullyInvariant
f : Module.End R M
x : M
⊢ (fun (x : M) ↦
      Eq (α := M)
        (((fun (f : (i : ι) → Module.End R ↥(N i)) ↦
                  (↑(ind.linearEquiv iSup_top) : (Π₀ (i : ι), ↥(N i)) →ₗ[R] M) ∘ₗ
                    DFinsupp.mapRange.linearMap (β₁ := fun (i : ι) ↦ ↥(N i)) (β₂ := fun (i : ι) ↦ ↥(N i)) f ∘ₗ
                      (↑(ind.linearEquiv iSup_top).symm : M →ₗ[R] Π₀ (i : ι), ↥(N i)))
                ((fun (f : Module.End R M) (i : ι) ↦ LinearMap.restrict f ⋯) f) :
              (a : M) → M)
            x :
          M)
        ((f : (a : M) → M) x : M))
    0

Tactic:
simp
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R₀ : Type u_1
R : Type u_2
M : Type u
N_1 : Type u_3
S : Type u_4
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Algebra R₀ R
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N_1
inst_5 : AddCommGroup S
inst_6 : Module R M
inst_7 : Module R N_1
inst_8 : Module R S
inst_9 : IsSimpleModule R S
ι : Type u_5
inst_10 : DecidableEq ι
N : ι → Submodule R M
ind : iSupIndep N
iSup_top : Eq.{u + 1} (α := Submodule R M) (⨆ (i : ι), N i) ⊤
invar : ∀ (i : ι), (N i).IsFullyInvariant
f : Module.End R M
x x_1 x_2 : M
h₁ :
  (fun (x : M) ↦
      Eq (α := M)
        (((fun (f : (i : ι) → Module.End R ↥(N i)) ↦
                  (↑(ind.linearEquiv iSup_top) : (Π₀ (i : ι), ↥(N i)) →ₗ[R] M) ∘ₗ
                    DFinsupp.mapRange.linearMap (β₁ := fun (i : ι) ↦ ↥(N i)) (β₂ := fun (i : ι) ↦ ↥(N i)) f ∘ₗ
                      (↑(ind.linearEquiv iSup_top).symm : M →ₗ[R] Π₀ (i : ι), ↥(N i)))
                ((fun (f : Module.End R M) (i : ι) ↦ LinearMap.restrict f ⋯) f) :
              (a : M) → M)
            x :
          M)
        ((f : (a : M) → M) x : M))
    x_1
h₂ :
  (fun (x : M) ↦
      Eq (α := M)
        (((fun (f : (i : ι) → Module.End R ↥(N i)) ↦
                  (↑(ind.linearEquiv iSup_top) : (Π₀ (i : ι), ↥(N i)) →ₗ[R] M) ∘ₗ
                    DFinsupp.mapRange.linearMap (β₁ := fun (i : ι) ↦ ↥(N i)) (β₂ := fun (i : ι) ↦ ↥(N i)) f ∘ₗ
                      (↑(ind.linearEquiv iSup_top).symm : M →ₗ[R] Π₀ (i : ι), ↥(N i)))
                ((fun (f : Module.End R M) (i : ι) ↦ LinearMap.restrict f ⋯) f) :
              (a : M) → M)
            x :
          M)
        ((f : (a : M) → M) x : M))
    x_2
⊢ (fun (x : M) ↦
      Eq (α := M)
        (((fun (f : (i : ι) → Module.End R ↥(N i)) ↦
                  (↑(ind.linearEquiv iSup_top) : (Π₀ (i : ι), ↥(N i)) →ₗ[R] M) ∘ₗ
                    DFinsupp.mapRange.linearMap (β₁ := fun (i : ι) ↦ ↥(N i)) (β₂ := fun (i : ι) ↦ ↥(N i)) f ∘ₗ
                      (↑(ind.linearEquiv iSup_top).symm : M →ₗ[R] Π₀ (i : ι), ↥(N i)))
                ((fun (f : Module.End R M) (i : ι) ↦ LinearMap.restrict f ⋯) f) :
              (a : M) → M)
            x :
          M)
        ((f : (a : M) → M) x : M))
    (x_1 + x_2)

Tactic:
simpa only [map_add] using congr($h₁ + $h₂)

Premises used: map_add
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R₀ : Type u_1
R : Type u_2
M : Type u
N_1 : Type u_3
S : Type u_4
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Algebra R₀ R
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N_1
inst_5 : AddCommGroup S
inst_6 : Module R M
inst_7 : Module R N_1
inst_8 : Module R S
inst_9 : IsSimpleModule R S
ι : Type u_5
inst_10 : DecidableEq ι
N : ι → Submodule R M
ind : iSupIndep N
iSup_top : Eq.{u + 1} (α := Submodule R M) (⨆ (i : ι), N i) ⊤
invar : ∀ (i : ι), (N i).IsFullyInvariant
f : Module.End R M
x : M
⊢ Eq (α := M)
    (((fun (f : (i : ι) → Module.End R ↥(N i)) ↦
              (↑(ind.linearEquiv iSup_top) : (Π₀ (i : ι), ↥(N i)) →ₗ[R] M) ∘ₗ
                DFinsupp.mapRange.linearMap (β₁ := fun (i : ι) ↦ ↥(N i)) (β₂ := fun (i : ι) ↦ ↥(N i)) f ∘ₗ
                  (↑(ind.linearEquiv iSup_top).symm : M →ₗ[R] Π₀ (i : ι), ↥(N i)))
            ((fun (f : Module.End R M) (i : ι) ↦ LinearMap.restrict f ⋯) f) :
          (a : M) → M)
        x :
      M)
    ((f : (a : M) → M) x : M)

Tactic:
exact Submodule.iSup_induction _ (motive := (_ = f ·)) (iSup_top ▸ Submodule.mem_top (x := x))
      (fun i x h ↦ by simp [ind.linearEquiv_symm_apply _ h]) (by simp)
      fun _ _ h₁ h₂ ↦ by simpa only [map_add] using congr($h₁ + $h₂)

Premises used: Submodule.iSup_induction
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R₀ : Type u_1
R : Type u_2
M : Type u
N_1 : Type u_3
S : Type u_4
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Algebra R₀ R
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N_1
inst_5 : AddCommGroup S
inst_6 : Module R M
inst_7 : Module R N_1
inst_8 : Module R S
inst_9 : IsSimpleModule R S
ι : Type u_5
inst_10 : DecidableEq ι
N : ι → Submodule R M
ind : iSupIndep N
iSup_top : Eq.{u + 1} (α := Submodule R M) (⨆ (i : ι), N i) ⊤
invar : ∀ (i : ι), (N i).IsFullyInvariant
f : (i : ι) → Module.End R ↥(N i)
h :
  ∀ (i : ι) (x : ↥(N i)),
    Eq.{u + 1} (α := M)
      (↑(((fun (f : Module.End R M) (i : ι) ↦ LinearMap.restrict f ⋯)
                ((fun (f : (i : ι) → Module.End R ↥(N i)) ↦
                    (↑(ind.linearEquiv iSup_top) : (Π₀ (i : ι), ↥(N i)) →ₗ[R] M) ∘ₗ
                      DFinsupp.mapRange.linearMap (β₁ := fun (i : ι) ↦ ↥(N i)) (β₂ := fun (i : ι) ↦ ↥(N i)) f ∘ₗ
                        (↑(ind.linearEquiv iSup_top).symm : M →ₗ[R] Π₀ (i : ι), ↥(N i)))
                  f)
                i :
              (a : ↥(N i)) → ↥(N i))
            x) :
        M)
      (↑((f i : (a : ↥(N i)) → ↥(N i)) x) : M)
⊢ (fun (f : Module.End R M) (i : ι) ↦ LinearMap.restrict f ⋯)
      ((fun (f : (i : ι) → Module.End R ↥(N i)) ↦
          (↑(ind.linearEquiv iSup_top) : (Π₀ (i : ι), ↥(N i)) →ₗ[R] M) ∘ₗ
            DFinsupp.mapRange.linearMap (β₁ := fun (i : ι) ↦ ↥(N i)) (β₂ := fun (i : ι) ↦ ↥(N i)) f ∘ₗ
              (↑(ind.linearEquiv iSup_top).symm : M →ₗ[R] Π₀ (i : ι), ↥(N i)))
        f) =
    f

Tactic:
ext i x
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R₀ : Type u_1
R : Type u_2
M : Type u
N_1 : Type u_3
S : Type u_4
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Algebra R₀ R
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N_1
inst_5 : AddCommGroup S
inst_6 : Module R M
inst_7 : Module R N_1
inst_8 : Module R S
inst_9 : IsSimpleModule R S
ι : Type u_5
inst_10 : DecidableEq ι
N : ι → Submodule R M
ind : iSupIndep N
iSup_top : Eq.{u + 1} (α := Submodule R M) (⨆ (i : ι), N i) ⊤
invar : ∀ (i : ι), (N i).IsFullyInvariant
f : (i : ι) → Module.End R ↥(N i)
i : ι
x : ↥(N i)
⊢ Eq.{u + 1} (α := M)
    (↑(((fun (f : Module.End R M) (i : ι) ↦ LinearMap.restrict f ⋯)
              ((fun (f : (i : ι) → Module.End R ↥(N i)) ↦
                  (↑(ind.linearEquiv iSup_top) : (Π₀ (i : ι), ↥(N i)) →ₗ[R] M) ∘ₗ
                    DFinsupp.mapRange.linearMap (β₁ := fun (i : ι) ↦ ↥(N i)) (β₂ := fun (i : ι) ↦ ↥(N i)) f ∘ₗ
                      (↑(ind.linearEquiv iSup_top).symm : M →ₗ[R] Π₀ (i : ι), ↥(N i)))
                f)
              i :
            (a : ↥(N i)) → ↥(N i))
          x) :
      M)
    (↑((f i : (a : ↥(N i)) → ↥(N i)) x) : M)

Tactic:
simp [ind.linearEquiv_symm_apply _ x.2]

Premises used: iSupIndep.linearEquiv_symm_apply, Subtype.property
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
S : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup S
inst_3 : Module R M
inst_4 : Module R S
inst_5 : IsSimpleModule R S
⊢ IsFullyInvariant (isotypicComponent R M S)

Tactic:
LinearMap.le_comap_isotypicComponent S

Premises used: LinearMap.le_comap_isotypicComponent, Submodule.IsFullyInvariant
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : Submodule R M
h : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) m
obtain : ∀ (w : Submodule R M), IsSimpleModule.{u_2, u} R ↥w → IsFullyInvariant (isotypicComponent R M ↥w)
⊢ m.IsFullyInvariant

Tactic:
obtain ⟨_, _, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
w : Submodule R M
left : IsSimpleModule.{u_2, u} R ↥w
⊢ IsFullyInvariant (isotypicComponent R M ↥w)

Tactic:
.isotypicComponent R M _

Premises used: Submodule.IsFullyInvariant.isotypicComponent
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
w : Submodule R M
left : IsSimpleModule.{u_2, u} R ↥w
⊢ IsFullyInvariant (isotypicComponent R M ↥w)

Tactic:
exact .isotypicComponent R M _
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R₀ : Type u_1
R : Type u_2
M : Type u
N : Type u_3
S : Type u_4
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Algebra R₀ R
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : AddCommGroup S
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R S
inst_9 : IsSimpleModule R S
s : Set (↑(isotypicComponents R M) : Type u)
c : (↑(isotypicComponents R M) : Type u)
hc :
  Membership.mem (γ := Set (↑(isotypicComponents R M) : Type u))
    {c : (↑(isotypicComponents R M) : Type u) |
      (↑c : Submodule R M) ≤
        (↑(⨆ c ∈ s,
              Subtype.mk (p := fun (x : Submodule R M) ↦
                Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x)
                (↑c : Submodule R M) ⋯) :
          Submodule R M)}
    c
hcs : c ∉ s
simp_rw :
  ∀ (i : (↑(isotypicComponents R M) : Type u)) (j : i ∈ s),
    (↑i : Submodule R M) ≤ sSup (isotypicComponents R M \ {(↑c : Submodule R M)})
⊢ LE.le (α := Submodule R M)
    (↑(⨆ c ∈ s,
          Subtype.mk (p := fun (x : Submodule R M) ↦
            Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x)
            (↑c : Submodule R M) ⋯) :
      Submodule R M)
    (sSup (isotypicComponents R M \ {(↑c : Submodule R M)}))

Tactic:
simp_rw [CompleteSublattice.coe_iSup, iSup₂_le_iff]

Premises used: CompleteSublattice.coe_iSup, iSup₂_le_iff
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R₀ : Type u_1
R : Type u_2
M : Type u
N : Type u_3
S : Type u_4
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Algebra R₀ R
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : AddCommGroup S
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R S
inst_9 : IsSimpleModule R S
s : Set (↑(isotypicComponents R M) : Type u)
c : (↑(isotypicComponents R M) : Type u)
hc :
  Membership.mem (γ := Set (↑(isotypicComponents R M) : Type u))
    {c : (↑(isotypicComponents R M) : Type u) |
      (↑c : Submodule R M) ≤
        (↑(⨆ c ∈ s,
              Subtype.mk (p := fun (x : Submodule R M) ↦
                Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x)
                (↑c : Submodule R M) ⋯) :
          Submodule R M)}
    c
hcs : c ∉ s
⊢ ∀ (i : (↑(isotypicComponents R M) : Type u)) (j : i ∈ s),
    (↑i : Submodule R M) ≤ sSup (isotypicComponents R M \ {(↑c : Submodule R M)})

Tactic:
fun c hc ↦ le_sSup ⟨c.2, Subtype.coe_ne_coe.mpr (ne_of_mem_of_not_mem hc hcs)⟩

Premises used: Iff.mpr, Set.Mem, ne_of_mem_of_not_mem, And.intro, le_sSup, Subtype.coe_ne_coe, Subtype.property
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R₀ : Type u_1
R : Type u_2
M : Type u
N : Type u_3
S : Type u_4
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Algebra R₀ R
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : AddCommGroup S
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R S
inst_9 : IsSimpleModule R S
s : Set (↑(isotypicComponents R M) : Type u)
c : (↑(isotypicComponents R M) : Type u)
hc :
  Membership.mem (γ := Set (↑(isotypicComponents R M) : Type u))
    {c : (↑(isotypicComponents R M) : Type u) |
      (↑c : Submodule R M) ≤
        (↑(⨆ c ∈ s,
              Subtype.mk (p := fun (x : Submodule R M) ↦
                Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x)
                (↑c : Submodule R M) ⋯) :
          Submodule R M)}
    c
hcs : c ∉ s
⊢ ∀ (i : (↑(isotypicComponents R M) : Type u)) (j : i ∈ s),
    (↑i : Submodule R M) ≤ sSup (isotypicComponents R M \ {(↑c : Submodule R M)})

Tactic:
exact fun c hc ↦ le_sSup ⟨c.2, Subtype.coe_ne_coe.mpr (ne_of_mem_of_not_mem hc hcs)⟩
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
S : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup S
inst_3 : Module R M
inst_4 : Module R S
inst_5 : IsSimpleModule R S
inst_6 : IsSemisimpleModule R M
rw : LE.le (α := Submodule R M) ⊤ (isotypicComponent R M S) ↔ IsIsotypicOfType R M S
rw₁ : IsIsotypicOfType.{u, u_2, u_4} R (↥⊤) S ↔ IsIsotypicOfType R M S
rw₂ rw₃ : IsIsotypicOfType R M S ↔ IsIsotypicOfType R M S
⊢ Eq (α := Submodule R M) (isotypicComponent R M S) ⊤ ↔ IsIsotypicOfType R M S

Tactic:
rw [← top_le_iff, le_isotypicComponent_iff, Submodule.topEquiv.isIsotypicOfType_iff]

Premises used: Submodule.topEquiv, LinearEquiv.isIsotypicOfType_iff, top_le_iff, le_isotypicComponent_iff