awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
obtain :
  ∀ (s : Set (Submodule R M)) (hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m),
    [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsNoetherian R M ∧ IsArtinian R M,
        ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m].TFAE
⊢ [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsNoetherian R M ∧ IsArtinian R M,
      ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m].TFAE

Tactic:
obtain ⟨s, hs⟩ := IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top R M

Premises used: IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
⊢ Module.Finite R M

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
⊢ IsNoetherian R M

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
⊢ Module.Finite R M ↔ IsNoetherian R M

Tactic:
1 ↔ 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
⊢ Module.Finite R M ↔ IsNoetherian R M

Tactic:
tfae_have 1 ↔ 2 := ⟨fun _ ↦ inferInstance, fun _ ↦ inferInstance⟩
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
⊢ IsNoetherian R M

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
⊢ ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
⊢ ∀ (a : IsNoetherian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m

Tactic:
2 → 5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
⊢ ∀ (a : IsNoetherian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m

Tactic:
tfae_have 2 → 5 := fun _ ↦ ⟨s, WellFoundedGT.finite_of_sSupIndep hs.1, hs⟩
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 :
  ∀ (a : IsNoetherian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
⊢ IsArtinian R M

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 :
  ∀ (a : IsNoetherian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
⊢ ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 :
  ∀ (a : IsNoetherian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
⊢ ∀ (a : IsArtinian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m

Tactic:
3 → 5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 :
  ∀ (a : IsNoetherian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
⊢ ∀ (a : IsArtinian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m

Tactic:
tfae_have 3 → 5 := fun _ ↦ ⟨s, WellFoundedLT.finite_of_sSupIndep hs.1, hs⟩
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 :
  ∀ (a : IsNoetherian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_3_to_5 :
  ∀ (a : IsArtinian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
⊢ ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 :
  ∀ (a : IsNoetherian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_3_to_5 :
  ∀ (a : IsArtinian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
⊢ IsNoetherian R M ∧ IsArtinian R M

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 :
  ∀ (a : IsNoetherian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_3_to_5 :
  ∀ (a : IsArtinian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
⊢ ∀ (a : ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m),
    IsNoetherian R M ∧ IsArtinian R M

Tactic:
5 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s_1 : Set (Submodule R M)
hs : sSupIndep s_1 ∧ sSup s_1 = ⊤ ∧ ∀ m ∈ s_1, IsSimpleModule.{u_1, u_2} R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 :
  ∀ (a : IsNoetherian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_3_to_5 :
  ∀ (a : IsArtinian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
h : ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
s : Set (Submodule R M)
fin : s.Finite
left : sSupIndep s
sSup_eq_top : sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
rw :
  IsNoetherian.{u_1, u_2} R ↥(⨆ (i : (↑s : Type u_2)), (↑i : Submodule R M)) ∧
    IsArtinian.{u_1, u_2} R ↥(⨆ (i : (↑s : Type u_2)), (↑i : Submodule R M))
⊢ IsNoetherian R M ∧ IsArtinian R M

Tactic:
rw [← isNoetherian_top_iff, ← Submodule.topEquiv.isArtinian_iff,
      ← sSup_eq_top, sSup_eq_iSup, ← iSup_subtype'']

Premises used: Submodule.topEquiv, iSup_subtype'', sSup_eq_iSup, isNoetherian_top_iff, LinearEquiv.isArtinian_iff
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s_1 : Set (Submodule R M)
hs : sSupIndep s_1 ∧ sSup s_1 = ⊤ ∧ ∀ m ∈ s_1, IsSimpleModule.{u_1, u_2} R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 :
  ∀ (a : IsNoetherian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_3_to_5 :
  ∀ (a : IsArtinian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
h : ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
s : Set (Submodule R M)
fin : s.Finite
left : sSupIndep s
sSup_eq_top : sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
⊢ ∀ (x : (↑s : Type u_2)), IsSimpleModule.{u_1, u_2} R ↥(↑x : Submodule R M)

Tactic:
rw [SetCoe.forall'] at simple

Premises used: SetCoe.forall'
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s_1 : Set (Submodule R M)
hs : sSupIndep s_1 ∧ sSup s_1 = ⊤ ∧ ∀ m ∈ s_1, IsSimpleModule.{u_1, u_2} R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 :
  ∀ (a : IsNoetherian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_3_to_5 :
  ∀ (a : IsArtinian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
h : ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
s : Set (Submodule R M)
fin : s.Finite
left : sSupIndep s
sSup_eq_top : sSup s = ⊤
simple : ∀ (x : (↑s : Type u_2)), IsSimpleModule.{u_1, u_2} R ↥(↑x : Submodule R M)
⊢ Finite.{u_2 + 1} (↑s : Type u_2)

Tactic:
have := fin.to_subtype
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s_1 : Set (Submodule R M)
hs : sSupIndep s_1 ∧ sSup s_1 = ⊤ ∧ ∀ m ∈ s_1, IsSimpleModule.{u_1, u_2} R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 :
  ∀ (a : IsNoetherian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_3_to_5 :
  ∀ (a : IsArtinian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
h : ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
s : Set (Submodule R M)
fin : s.Finite
left : sSupIndep s
sSup_eq_top : sSup s = ⊤
simple : ∀ (x : (↑s : Type u_2)), IsSimpleModule.{u_1, u_2} R ↥(↑x : Submodule R M)
this : Finite.{u_2 + 1} (↑s : Type u_2)
⊢ IsNoetherian.{u_1, u_2} R ↥(⨆ (i : (↑s : Type u_2)), (↑i : Submodule R M)) ∧
    IsArtinian.{u_1, u_2} R ↥(⨆ (i : (↑s : Type u_2)), (↑i : Submodule R M))

Tactic:
⟨isNoetherian_iSup, isArtinian_iSup⟩

Premises used: isNoetherian_iSup, And.intro, isArtinian_iSup
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s_1 : Set (Submodule R M)
hs : sSupIndep s_1 ∧ sSup s_1 = ⊤ ∧ ∀ m ∈ s_1, IsSimpleModule.{u_1, u_2} R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 :
  ∀ (a : IsNoetherian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_3_to_5 :
  ∀ (a : IsArtinian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
h : ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
s : Set (Submodule R M)
fin : s.Finite
left : sSupIndep s
sSup_eq_top : sSup s = ⊤
simple : ∀ (x : (↑s : Type u_2)), IsSimpleModule.{u_1, u_2} R ↥(↑x : Submodule R M)
this : Finite.{u_2 + 1} (↑s : Type u_2)
⊢ IsNoetherian.{u_1, u_2} R ↥(⨆ (i : (↑s : Type u_2)), (↑i : Submodule R M)) ∧
    IsArtinian.{u_1, u_2} R ↥(⨆ (i : (↑s : Type u_2)), (↑i : Submodule R M))

Tactic:
exact ⟨isNoetherian_iSup, isArtinian_iSup⟩
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 :
  ∀ (a : IsNoetherian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_3_to_5 :
  ∀ (a : IsArtinian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
⊢ ∀ (a : ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m),
    IsNoetherian R M ∧ IsArtinian R M

Tactic:
tfae_have 5 → 4 := fun ⟨s, fin, _, sSup_eq_top, simple⟩ ↦ by
    rw [← isNoetherian_top_iff, ← Submodule.topEquiv.isArtinian_iff,
      ← sSup_eq_top, sSup_eq_iSup, ← iSup_subtype'']
    rw [SetCoe.forall'] at simple
    have := fin.to_subtype
    exact ⟨isNoetherian_iSup, isArtinian_iSup⟩
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 :
  ∀ (a : IsNoetherian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_3_to_5 :
  ∀ (a : IsArtinian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_5_to_4 :
  ∀ (a : ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m),
    IsNoetherian R M ∧ IsArtinian R M
⊢ IsNoetherian R M ∧ IsArtinian R M

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 :
  ∀ (a : IsNoetherian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_3_to_5 :
  ∀ (a : IsArtinian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_5_to_4 :
  ∀ (a : ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m),
    IsNoetherian R M ∧ IsArtinian R M
⊢ IsNoetherian R M

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 :
  ∀ (a : IsNoetherian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_3_to_5 :
  ∀ (a : IsArtinian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_5_to_4 :
  ∀ (a : ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m),
    IsNoetherian R M ∧ IsArtinian R M
⊢ ∀ (a : IsNoetherian R M ∧ IsArtinian R M), IsNoetherian R M

Tactic:
4 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 :
  ∀ (a : IsNoetherian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_3_to_5 :
  ∀ (a : IsArtinian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_5_to_4 :
  ∀ (a : ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m),
    IsNoetherian R M ∧ IsArtinian R M
⊢ ∀ (a : IsNoetherian R M ∧ IsArtinian R M), IsNoetherian R M

Tactic:
tfae_have 4 → 2 := And.left

Premises used: And.left
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 :
  ∀ (a : IsNoetherian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_3_to_5 :
  ∀ (a : IsArtinian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_5_to_4 :
  ∀ (a : ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m),
    IsNoetherian R M ∧ IsArtinian R M
tfae_4_to_2 : ∀ (a : IsNoetherian R M ∧ IsArtinian R M), IsNoetherian R M
⊢ IsNoetherian R M ∧ IsArtinian R M

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 :
  ∀ (a : IsNoetherian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_3_to_5 :
  ∀ (a : IsArtinian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_5_to_4 :
  ∀ (a : ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m),
    IsNoetherian R M ∧ IsArtinian R M
tfae_4_to_2 : ∀ (a : IsNoetherian R M ∧ IsArtinian R M), IsNoetherian R M
⊢ IsArtinian R M

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 :
  ∀ (a : IsNoetherian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_3_to_5 :
  ∀ (a : IsArtinian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_5_to_4 :
  ∀ (a : ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m),
    IsNoetherian R M ∧ IsArtinian R M
tfae_4_to_2 : ∀ (a : IsNoetherian R M ∧ IsArtinian R M), IsNoetherian R M
⊢ ∀ (a : IsNoetherian R M ∧ IsArtinian R M), IsArtinian R M

Tactic:
4 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 :
  ∀ (a : IsNoetherian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_3_to_5 :
  ∀ (a : IsArtinian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_5_to_4 :
  ∀ (a : ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m),
    IsNoetherian R M ∧ IsArtinian R M
tfae_4_to_2 : ∀ (a : IsNoetherian R M ∧ IsArtinian R M), IsNoetherian R M
⊢ ∀ (a : IsNoetherian R M ∧ IsArtinian R M), IsArtinian R M

Tactic:
tfae_have 4 → 3 := And.right

Premises used: And.right