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
M_1 : Type u_2
inst_3 : AddCommGroup M_1
inst_4 : Module R M_1
inst_5 : Subsingleton M_1
N : Type u_3
inst_6 : AddCommGroup N
inst_7 : Module R N
e : M_1 ≃ₗ[R] N
this : Subsingleton N
⊢ IsFiniteLength R N

Tactic:
exact .of_subsingleton
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M_1 : Type u_2
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
S : Submodule R M
inst_5 : IsSimpleModule.{u_1, u_2} R (M ⧸ S)
h : IsFiniteLength.{u_1, u_2} R ↥S
ih :
  ∀ {N : Type u_3} [inst_8 : AddCommGroup N] [inst_9 : Module R N]
    (e : LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥S) N), IsFiniteLength R N
N : Type u_3
inst_6 : AddCommGroup N
inst_7 : Module R N
e : M ≃ₗ[R] N
⊢ IsSimpleModule.{u_1, u_3} R (N ⧸ Submodule.map (↑e : M →ₗ[R] N) S)

Tactic:
have : IsSimpleModule R (N ⧸ Submodule.map (e : M →ₗ[R] N) S) :=
      IsSimpleModule.congr (Submodule.Quotient.equiv S _ e rfl).symm
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M_1 : Type u_2
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
S : Submodule R M
inst_5 : IsSimpleModule.{u_1, u_2} R (M ⧸ S)
h : IsFiniteLength.{u_1, u_2} R ↥S
ih :
  ∀ {N : Type u_3} [inst_8 : AddCommGroup N] [inst_9 : Module R N]
    (e : LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥S) N), IsFiniteLength R N
N : Type u_3
inst_6 : AddCommGroup N
inst_7 : Module R N
e : M ≃ₗ[R] N
this : IsSimpleModule.{u_1, u_3} R (N ⧸ Submodule.map (↑e : M →ₗ[R] N) S)
⊢ IsFiniteLength R N

Tactic:
.of_simple_quotient (ih <| e.submoduleMap S)

Premises used: IsFiniteLength.of_simple_quotient, LinearEquiv.submoduleMap
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M_1 : Type u_2
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
S : Submodule R M
inst_5 : IsSimpleModule.{u_1, u_2} R (M ⧸ S)
h : IsFiniteLength.{u_1, u_2} R ↥S
ih :
  ∀ {N : Type u_3} [inst_8 : AddCommGroup N] [inst_9 : Module R N]
    (e : LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥S) N), IsFiniteLength R N
N : Type u_3
inst_6 : AddCommGroup N
inst_7 : Module R N
e : M ≃ₗ[R] N
this : IsSimpleModule.{u_1, u_3} R (N ⧸ Submodule.map (↑e : M →ₗ[R] N) S)
⊢ IsFiniteLength R N

Tactic:
exact .of_simple_quotient (ih <| e.submoduleMap S)
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
e : M ≃ₗ[R] N
h : IsFiniteLength R M
of_subsingleton :
  ∀ {M : Type u_2} [inst_5 : AddCommGroup M] [inst_6 : Module R M] [Subsingleton M] {N : Type u_3}
    [inst_8 : AddCommGroup N] [inst_9 : Module R N] (e : M ≃ₗ[R] N), IsFiniteLength R N
of_simple_quotient :
  ∀ {M : Type u_2} [inst_5 : AddCommGroup M] [inst_6 : Module R M] {S : Submodule R M}
    [IsSimpleModule.{u_1, u_2} R (M ⧸ S)],
    IsFiniteLength.{u_1, u_2} R ↥S →
      ∀
        (ih :
          ∀ {N : Type u_3} [inst_8 : AddCommGroup N] [inst_9 : Module R N]
            (e : LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥S) N), IsFiniteLength R N)
        {N : Type u_3} [inst_8 : AddCommGroup N] [inst_9 : Module R N] (e : M ≃ₗ[R] N), IsFiniteLength R N
⊢ IsFiniteLength R N

Tactic:
induction h generalizing N with
  | of_subsingleton =>
    have := e.symm.toEquiv.subsingleton; exact .of_subsingleton
  | @of_simple_quotient M _ _ S _ _ ih =>
    have : IsSimpleModule R (N ⧸ Submodule.map (e : M →ₗ[R] N) S) :=
      IsSimpleModule.congr (Submodule.Quotient.equiv S _ e rfl).symm
    exact .of_simple_quotient (ih <| e.submoduleMap S)
-- 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 : IsNoetherian R M
inst_4 : IsArtinian R M
obtain :
  ∀ (f : ℕ → Submodule R M) (f0 : IsMin (f 0)) (n : ℕ) (hn : IsMax (f n) ∧ ∀ i < n, f i ⋖ f (i + 1)),
    ∃ (s : CompositionSeries (Submodule R M)),
      RelSeries.head (r :=
            {x : Submodule R M × Submodule R M |
              match (motive := Submodule R M × Submodule R M → Prop) x with
              | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
            s =
          ⊥ ∧
        RelSeries.last (r :=
            {x : Submodule R M × Submodule R M |
              match (motive := Submodule R M × Submodule R M → Prop) x with
              | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
            s =
          ⊤
⊢ ∃ (s : CompositionSeries (Submodule R M)),
    RelSeries.head (r :=
          {x : Submodule R M × Submodule R M |
            match (motive := Submodule R M × Submodule R M → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
          s =
        ⊥ ∧
      RelSeries.last (r :=
          {x : Submodule R M × Submodule R M |
            match (motive := Submodule R M × Submodule R M → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
          s =
        ⊤

Tactic:
obtain ⟨f, f0, n, hn⟩ := exists_covBy_seq_of_wellFoundedLT_wellFoundedGT (Submodule R M)

Premises used: Submodule, exists_covBy_seq_of_wellFoundedLT_wellFoundedGT
-- 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 : IsNoetherian R M
inst_4 : IsArtinian R M
f : ℕ → Submodule R M
f0 : IsMin (f 0)
n : ℕ
hn : IsMax (f n) ∧ ∀ i < n, f i ⋖ f (i + 1)
⊢ ∃ (s : CompositionSeries (Submodule R M)),
    RelSeries.head (r :=
          {x : Submodule R M × Submodule R M |
            match (motive := Submodule R M × Submodule R M → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
          s =
        ⊥ ∧
      RelSeries.last (r :=
          {x : Submodule R M × Submodule R M |
            match (motive := Submodule R M × Submodule R M → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
          s =
        ⊤

Tactic:
⟨⟨n, fun i ↦ f i, fun i ↦ hn.2 i i.2⟩, f0.eq_bot, hn.1.eq_top⟩

Premises used: Fin.isLt, IsMax.eq_top, Fin.val, IsMin.eq_bot, And.right, And.left, And.intro, Exists.intro, RelSeries.mk
-- 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 : IsNoetherian R M
inst_4 : IsArtinian R M
f : ℕ → Submodule R M
f0 : IsMin (f 0)
n : ℕ
hn : IsMax (f n) ∧ ∀ i < n, f i ⋖ f (i + 1)
⊢ ∃ (s : CompositionSeries (Submodule R M)),
    RelSeries.head (r :=
          {x : Submodule R M × Submodule R M |
            match (motive := Submodule R M × Submodule R M → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
          s =
        ⊥ ∧
      RelSeries.last (r :=
          {x : Submodule R M × Submodule R M |
            match (motive := Submodule R M × Submodule R M → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
          s =
        ⊤

Tactic:
exact ⟨⟨n, fun i ↦ f i, fun i ↦ hn.2 i i.2⟩, f0.eq_bot, hn.1.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
h :
  ∃ (s : CompositionSeries (Submodule R M)),
    RelSeries.head (r :=
          {x : Submodule R M × Submodule R M |
            match (motive := Submodule R M × Submodule R M → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
          s =
        ⊥ ∧
      RelSeries.last (r :=
          {x : Submodule R M × Submodule R M |
            match (motive := Submodule R M × Submodule R M → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
          s =
        ⊤
obtain :
  ∀ (s : CompositionSeries (Submodule R M))
    (s_head :
      RelSeries.head (r :=
          {x : Submodule R M × Submodule R M |
            match (motive := Submodule R M × Submodule R M → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
          s =
        ⊥)
    (s_last :
      RelSeries.last (r :=
          {x : Submodule R M × Submodule R M |
            match (motive := Submodule R M × Submodule R M → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
          s =
        ⊤),
    IsFiniteLength.{u_1, u_2} R ↥⊤
⊢ IsFiniteLength.{u_1, u_2} R ↥⊤

Tactic:
obtain ⟨s, s_head, s_last⟩ := h
-- 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
s : CompositionSeries (Submodule R M)
s_head :
  RelSeries.head (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊥
s_last :
  RelSeries.last (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊤
rw :
  IsFiniteLength.{u_1, u_2} R
    ↥(RelSeries.last (r :=
        {x : Submodule R M × Submodule R M |
          match (motive := Submodule R M × Submodule R M → Prop) x with
          | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
        s)
⊢ IsFiniteLength.{u_1, u_2} R ↥⊤

Tactic:
rw [← s_last]
-- 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
s : CompositionSeries (Submodule R M)
s_head :
  RelSeries.head (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊥
s_last :
  RelSeries.last (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊤
suffices :
  ∀
    (i :
      Fin
        (s.length (r :=
            {x : Submodule R M × Submodule R M |
              match (motive := Submodule R M × Submodule R M → Prop) x with
              | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y}) +
          1)),
    IsFiniteLength.{u_1, u_2} R
      ↥(s.toFun (r :=
          {x : Submodule R M × Submodule R M |
            match (motive := Submodule R M × Submodule R M → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
          i)
⊢ IsFiniteLength.{u_1, u_2} R
    ↥(RelSeries.last (r :=
        {x : Submodule R M × Submodule R M |
          match (motive := Submodule R M × Submodule R M → Prop) x with
          | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
        s)

Tactic:
suffices ∀ i, IsFiniteLength R (s i) from this (Fin.last _)
-- 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
s : CompositionSeries (Submodule R M)
s_head :
  RelSeries.head (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊥
s_last :
  RelSeries.last (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊤
zero :
  IsFiniteLength.{u_1, u_2} R
    ↥(RelSeries.head (r :=
        {x : Submodule R M × Submodule R M |
          match (motive := Submodule R M × Submodule R M → Prop) x with
          | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
        s)
⊢ IsFiniteLength.{u_1, u_2} R
    ↥(s.toFun (r :=
        {x : Submodule R M × Submodule R M |
          match (motive := Submodule R M × Submodule R M → Prop) x with
          | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
        0)

Tactic:
change IsFiniteLength R s.head

Premises used: Membership.mem, Subtype, RelSeries.head, IsFiniteLength
-- 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
s : CompositionSeries (Submodule R M)
s_head :
  RelSeries.head (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊥
s_last :
  RelSeries.last (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊤
zero : IsFiniteLength.{u_1, u_2} R ↥⊥
⊢ IsFiniteLength.{u_1, u_2} R
    ↥(RelSeries.head (r :=
        {x : Submodule R M × Submodule R M |
          match (motive := Submodule R M × Submodule R M → Prop) x with
          | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
        s)

Tactic:
rw [s_head]
-- 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
s : CompositionSeries (Submodule R M)
s_head :
  RelSeries.head (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊥
s_last :
  RelSeries.last (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊤
⊢ IsFiniteLength.{u_1, u_2} R ↥⊥

Tactic:
.of_subsingleton

Premises used: IsFiniteLength.of_subsingleton
-- 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
s : CompositionSeries (Submodule R M)
s_head :
  RelSeries.head (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊥
s_last :
  RelSeries.last (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊤
⊢ IsFiniteLength.{u_1, u_2} R ↥⊥

Tactic:
exact .of_subsingleton
-- 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
s : CompositionSeries (Submodule R M)
s_head :
  RelSeries.head (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊥
s_last :
  RelSeries.last (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊤
i :
  Fin
    (s.length (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y}))
ih :
  IsFiniteLength.{u_1, u_2} R
    ↥(s.toFun (r :=
        {x : Submodule R M × Submodule R M |
          match (motive := Submodule R M × Submodule R M → Prop) x with
          | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
        i.castSucc)
cov : Membership.mem (γ := SetRel (Submodule R M) (Submodule R M))
  {x : Submodule R M × Submodule R M |
    match (motive := Submodule R M × Submodule R M → Prop) x with
    | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y}
  (s.toFun (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      i.castSucc,
    s.toFun (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      i.succ) :=
  ⋯
⊢ IsSimpleModule.{u_1, u_2} R
    (↥(s.toFun (r :=
          {x : Submodule R M × Submodule R M |
            match (motive := Submodule R M × Submodule R M → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
          i.succ) ⧸
      Submodule.comap
        (s.toFun (r :=
            {x : Submodule R M × Submodule R M |
              match (motive := Submodule R M × Submodule R M → Prop) x with
              | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
            i.succ).subtype
        (s.toFun (r :=
          {x : Submodule R M × Submodule R M |
            match (motive := Submodule R M × Submodule R M → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
          i.castSucc))

Tactic:
have := (covBy_iff_quot_is_simple cov.le).mp cov
-- 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
s : CompositionSeries (Submodule R M)
s_head :
  RelSeries.head (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊥
s_last :
  RelSeries.last (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊤
i :
  Fin
    (s.length (r :=
        {x : Submodule R M × Submodule R M |
          match (motive := Submodule R M × Submodule R M → Prop) x with
          | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y}) +
      1)
zero :
  IsFiniteLength.{u_1, u_2} R
    ↥(s.toFun (r :=
        {x : Submodule R M × Submodule R M |
          match (motive := Submodule R M × Submodule R M → Prop) x with
          | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
        0)
succ :
  ∀
    (i :
      Fin
        (s.length (r :=
          {x : Submodule R M × Submodule R M |
            match (motive := Submodule R M × Submodule R M → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})))
    (ih :
      IsFiniteLength.{u_1, u_2} R
        ↥(s.toFun (r :=
            {x : Submodule R M × Submodule R M |
              match (motive := Submodule R M × Submodule R M → Prop) x with
              | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
            i.castSucc)),
    IsFiniteLength.{u_1, u_2} R
      ↥(s.toFun (r :=
          {x : Submodule R M × Submodule R M |
            match (motive := Submodule R M × Submodule R M → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
          i.succ)
⊢ IsFiniteLength.{u_1, u_2} R
    ↥(s.toFun (r :=
        {x : Submodule R M × Submodule R M |
          match (motive := Submodule R M × Submodule R M → Prop) x with
          | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
        i)

Tactic:
induction i using Fin.induction with
    | zero => change IsFiniteLength R s.head; rw [s_head]; exact .of_subsingleton
    | succ i ih =>
      let cov := s.step i
      have := (covBy_iff_quot_is_simple cov.le).mp cov
      have := ((s i.castSucc).comap (s i.succ).subtype).equivMapOfInjective
        _ (Submodule.injective_subtype _)
      rw [Submodule.map_comap_subtype, inf_of_le_right cov.le] at this
      exact .of_simple_quotient (this.symm.isFiniteLength ih)

Premises used: Membership.mem, Subtype, RelSeries.head, Submodule.map_comap_subtype, IsFiniteLength
-- 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
⊢ IsFiniteLength R M ↔ IsNoetherian R M ∧ IsArtinian R M

Tactic:
open scoped IsSimpleOrder in
  ⟨fun h ↦ h.rec (fun {M} _ _ _ ↦ ⟨inferInstance, inferInstance⟩) fun M _ _ {N} _ _ ⟨_, _⟩ ↦
    ⟨(isNoetherian_iff_submodule_quotient N).mpr ⟨‹_›, isNoetherian_iff'.mpr inferInstance⟩,
      (isArtinian_iff_submodule_quotient N).mpr ⟨‹_›, inferInstance⟩⟩,
    fun ⟨_, _⟩ ↦ isFiniteLength_of_exists_compositionSeries
      (exists_compositionSeries_of_isNoetherian_isArtinian R M)⟩

Premises used: IsFiniteLength.rec, isFiniteLength_of_exists_compositionSeries, exists_compositionSeries_of_isNoetherian_isArtinian, Iff.intro, _private.0.isFiniteLength_iff_isNoetherian_isArtinian.match_2, IsFiniteLength
-- 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
⊢ IsFiniteLength R M ↔
    ∃ (s : CompositionSeries (Submodule R M)),
      RelSeries.head (r :=
            {x : Submodule R M × Submodule R M |
              match (motive := Submodule R M × Submodule R M → Prop) x with
              | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
            s =
          ⊥ ∧
        RelSeries.last (r :=
            {x : Submodule R M × Submodule R M |
              match (motive := Submodule R M × Submodule R M → Prop) x with
              | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
            s =
          ⊤

Tactic:
⟨fun h ↦ have ⟨_, _⟩ := isFiniteLength_iff_isNoetherian_isArtinian.mp h
    exists_compositionSeries_of_isNoetherian_isArtinian R M,
    isFiniteLength_of_exists_compositionSeries⟩

Premises used: isFiniteLength_of_exists_compositionSeries, RelSeries.last, Exists, exists_compositionSeries_of_isNoetherian_isArtinian, Bot.bot, And, Iff.intro, Iff.mp, RelSeries.head, Top.top, _private.0.isFiniteLength_iff_isNoetherian_isArtinian.match_2, Eq, isFiniteLength_iff_isNoetherian_isArtinian
-- 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
rw :
  [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, IsFiniteLength R M,
      ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m].TFAE

Tactic:
rw [isFiniteLength_iff_isNoetherian_isArtinian]

Premises used: isFiniteLength_iff_isNoetherian_isArtinian