awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (goal)
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
    ↥(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)
have 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)
Tactic: change IsFiniteLength R s.head
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (goal)
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
    ↥(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)
have zero : IsFiniteLength.{u_1, u_2} R ↥⊥
Tactic: rw [s_head]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (goal)
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)
⊢ 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)
have 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)
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)
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (goal)
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)
⊢ 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)
have 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)
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)
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (goal)
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
⊢ [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
have 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
Tactic: rw [isFiniteLength_iff_isNoetherian_isArtinian]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (goal)
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
⊢ [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
have 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
Tactic: obtain ⟨s, hs⟩ := IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top R M
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (hypothesis)
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, 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
have tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
Tactic: tfae_have 1 ↔ 2 := ⟨fun _ ↦ inferInstance, fun _ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (hypothesis)
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
⊢ [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
have 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
Tactic: tfae_have 2 → 5 := fun _ ↦ ⟨s, WellFoundedGT.finite_of_sSupIndep hs.1, hs⟩
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (hypothesis)
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
⊢ [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
have 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
Tactic: tfae_have 3 → 5 := fun _ ↦ ⟨s, WellFoundedLT.finite_of_sSupIndep hs.1, hs⟩
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (goal)
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
⊢ IsNoetherian R M ∧ IsArtinian R M
have 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))
Tactic: rw [← isNoetherian_top_iff, ← Submodule.topEquiv.isArtinian_iff,
      ← sSup_eq_top, sSup_eq_iSup, ← iSup_subtype'']
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (hypothesis)
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
⊢ 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))
have simple₁ : ∀ (x : (↑s : Type u_2)), IsSimpleModule.{u_1, u_2} R ↥(↑x : Submodule R M)
Tactic: rw [SetCoe.forall'] at simple
Cleared hypotheses: simple
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (hypothesis)
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)
⊢ 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))
have this : Finite.{u_2 + 1} (↑s : Type u_2)
Tactic: have := fin.to_subtype
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (hypothesis)
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
⊢ [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
have 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
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⟩
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (hypothesis)
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
⊢ [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
have tfae_4_to_2 : ∀ (a : IsNoetherian R M ∧ IsArtinian R M), IsNoetherian R M
Tactic: tfae_have 4 → 2 := And.left
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (hypothesis)
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
⊢ [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
have tfae_4_to_3 : ∀ (a : IsNoetherian R M ∧ IsArtinian R M), IsArtinian R M
Tactic: tfae_have 4 → 3 := And.right
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (goal)
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
f : M →ₗ[R] N
H : IsFiniteLength R N
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ IsFiniteLength R M
have rw : ∀ (H : IsNoetherian R N ∧ IsArtinian R N)
  (hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)), IsNoetherian R M ∧ IsArtinian R M
Tactic: rw [isFiniteLength_iff_isNoetherian_isArtinian] at H ⊢
Cleared hypotheses: H, hf
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (hypothesis)
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
f : M →ₗ[R] N
H : IsNoetherian R N ∧ IsArtinian R N
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ IsNoetherian R M ∧ IsArtinian R M
have left : IsNoetherian R N
Tactic: cases H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (hypothesis)
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
f : M →ₗ[R] N
H : IsNoetherian R N ∧ IsArtinian R N
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
left : IsNoetherian R N
⊢ IsNoetherian R M ∧ IsArtinian R M
have right : IsArtinian R N
Tactic: cases H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (goal)
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
f : M →ₗ[R] N
H : IsFiniteLength R M
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ IsFiniteLength R N
have rw : ∀ (H : IsNoetherian R M ∧ IsArtinian R M)
  (hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)), IsNoetherian R N ∧ IsArtinian R N
Tactic: rw [isFiniteLength_iff_isNoetherian_isArtinian] at H ⊢
Cleared hypotheses: H, hf
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (hypothesis)
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
f : M →ₗ[R] N
H : IsNoetherian R M ∧ IsArtinian R M
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ IsNoetherian R N ∧ IsArtinian R N
have left : IsNoetherian R M
Tactic: cases H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (hypothesis)
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
f : M →ₗ[R] N
H : IsNoetherian R M ∧ IsArtinian R M
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
left : IsNoetherian R M
⊢ IsNoetherian R N ∧ IsArtinian R N
have right : IsArtinian R M
Tactic: cases H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
⊢ FiniteType R A
have obtain : ∀ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] A)
  (hf :
    Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
      Ideal.FG (RingHom.ker f.toRingHom)),
  FiniteType R A
Tactic: obtain ⟨n, f, hf⟩ := FinitePresentation.out (R := R) (A := A)
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
⊢ FiniteType R A
have apply : ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] A),
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
Tactic: apply FiniteType.iff_quotient_mvPolynomial''.2
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsNoetherianRing R
⊢ FiniteType R A ↔ FinitePresentation R A
have refine : ∀ (h : FiniteType R A), FinitePresentation R A
Tactic: refine ⟨fun h => ?_, fun hfp => Algebra.FiniteType.of_finitePresentation⟩
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsNoetherianRing R
h : FiniteType R A
⊢ FinitePresentation R A
have obtain : ∀ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] A)
  (hf : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)),
  FinitePresentation R A
Tactic: obtain ⟨n, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.1 h
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
⊢ FinitePresentation R A
have refine : Ideal.FG (RingHom.ker f.toRingHom)
Tactic: refine ⟨n, f, hf, ?_⟩