awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : (↑(length R M) : WithBot ℕ∞) = (↑0 : WithBot ℕ∞) ↔ Subsingleton M
⊢ length R M = 0 ↔ Subsingleton M
have rw₁ : Order.krullDim.{u_2} (Submodule R M) = (↑0 : WithBot ℕ∞) ↔ Subsingleton M
Tactic: rw [← WithBot.coe_inj, Module.coe_length, WithBot.coe_zero,
    Order.krullDim_eq_zero_iff_of_orderTop, Submodule.subsingleton_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : (↑(length R M) : WithBot ℕ∞) = (↑0 : WithBot ℕ∞) ↔ Subsingleton M
rw₁ : Order.krullDim.{u_2} (Submodule R M) = (↑0 : WithBot ℕ∞) ↔ Subsingleton M
⊢ length R M = 0 ↔ Subsingleton M
have rw₂ : Order.krullDim.{u_2} (Submodule R M) = 0 ↔ Subsingleton M
Tactic: rw [← WithBot.coe_inj, Module.coe_length, WithBot.coe_zero,
    Order.krullDim_eq_zero_iff_of_orderTop, Submodule.subsingleton_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : (↑(length R M) : WithBot ℕ∞) = (↑0 : WithBot ℕ∞) ↔ Subsingleton M
rw₁ : Order.krullDim.{u_2} (Submodule R M) = (↑0 : WithBot ℕ∞) ↔ Subsingleton M
rw₂ : Order.krullDim.{u_2} (Submodule R M) = 0 ↔ Subsingleton M
⊢ length R M = 0 ↔ Subsingleton M
have rw₃ : Subsingleton.{u_2 + 1} (Submodule R M) ↔ Subsingleton M
Tactic: rw [← WithBot.coe_inj, Module.coe_length, WithBot.coe_zero,
    Order.krullDim_eq_zero_iff_of_orderTop, Submodule.subsingleton_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : (↑(length R M) : WithBot ℕ∞) = (↑0 : WithBot ℕ∞) ↔ Subsingleton M
rw₁ : Order.krullDim.{u_2} (Submodule R M) = (↑0 : WithBot ℕ∞) ↔ Subsingleton M
rw₂ : Order.krullDim.{u_2} (Submodule R M) = 0 ↔ Subsingleton M
rw₃ : Subsingleton.{u_2 + 1} (Submodule R M) ↔ Subsingleton M
⊢ length R M = 0 ↔ Subsingleton M
have rw₄ : Subsingleton M ↔ Subsingleton M
Tactic: rw [← WithBot.coe_inj, Module.coe_length, WithBot.coe_zero,
    Order.krullDim_eq_zero_iff_of_orderTop, Submodule.subsingleton_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ 0 < length R M ↔ Nontrivial M
have rw : length R M ≠ 0 ↔ Nontrivial M
Tactic: rw [pos_iff_ne_zero, ne_eq, Module.length_eq_zero_iff, not_subsingleton_iff_nontrivial]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : length R M ≠ 0 ↔ Nontrivial M
⊢ 0 < length R M ↔ Nontrivial M
have rw₁ : ¬length R M = 0 ↔ Nontrivial M
Tactic: rw [pos_iff_ne_zero, ne_eq, Module.length_eq_zero_iff, not_subsingleton_iff_nontrivial]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : length R M ≠ 0 ↔ Nontrivial M
rw₁ : ¬length R M = 0 ↔ Nontrivial M
⊢ 0 < length R M ↔ Nontrivial M
have rw₂ : ¬Subsingleton M ↔ Nontrivial M
Tactic: rw [pos_iff_ne_zero, ne_eq, Module.length_eq_zero_iff, not_subsingleton_iff_nontrivial]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : length R M ≠ 0 ↔ Nontrivial M
rw₁ : ¬length R M = 0 ↔ Nontrivial M
rw₂ : ¬Subsingleton M ↔ Nontrivial M
⊢ 0 < length R M ↔ Nontrivial M
have rw₃ : Nontrivial M ↔ Nontrivial M
Tactic: rw [pos_iff_ne_zero, ne_eq, Module.length_eq_zero_iff, not_subsingleton_iff_nontrivial]
-- Lean 4 proof step from Mathlib.RingTheory.Length (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : CompositionSeries (Submodule R M)
h₁ :
  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 =
    ⊥
h₂ :
  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.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})) :
      ℕ∞) =
    length R M
have H : IsFiniteLength R M
Tactic: have H := isFiniteLength_of_exists_compositionSeries ⟨s, h₁, h₂⟩
-- Lean 4 proof step from Mathlib.RingTheory.Length (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : CompositionSeries (Submodule R M)
h₁ :
  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 =
    ⊥
h₂ :
  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 =
    ⊤
H : IsFiniteLength R M
⊢ (↑(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})) :
      ℕ∞) =
    length R M
have this : IsNoetherian R M
Tactic: have := (isFiniteLength_iff_isNoetherian_isArtinian.mp H).1
-- Lean 4 proof step from Mathlib.RingTheory.Length (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : CompositionSeries (Submodule R M)
h₁ :
  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 =
    ⊥
h₂ :
  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 =
    ⊤
H : IsFiniteLength R M
this : IsNoetherian R M
⊢ (↑(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})) :
      ℕ∞) =
    length R M
have this₁ : IsArtinian R M
Tactic: have := (isFiniteLength_iff_isNoetherian_isArtinian.mp H).2
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : CompositionSeries (Submodule R M)
h₁ :
  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 =
    ⊥
h₂ :
  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 =
    ⊤
H : IsFiniteLength R M
this_1 : IsNoetherian R M
this : IsArtinian R M
⊢ (↑(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})) :
      ℕ∞) =
    length R M
have rw : (↑(↑(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})) :
        ℕ∞) :
    WithBot ℕ∞) =
  Order.krullDim.{u_2} (Submodule R M)
Tactic: rw [← WithBot.coe_inj, Module.coe_length]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : CompositionSeries (Submodule R M)
h₁ :
  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 =
    ⊥
h₂ :
  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 =
    ⊤
H : IsFiniteLength R M
this_1 : IsNoetherian R M
this : IsArtinian R M
⊢ (↑(↑(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})) :
          ℕ∞) :
      WithBot ℕ∞) =
    Order.krullDim.{u_2} (Submodule R M)
have a : (↑(↑(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})) :
        ℕ∞) :
    WithBot ℕ∞) ≤
  Order.krullDim.{u_2} (Submodule R M)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : CompositionSeries (Submodule R M)
h₁ :
  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 =
    ⊥
h₂ :
  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 =
    ⊤
H : IsFiniteLength R M
this_1 : IsNoetherian R M
this : IsArtinian R M
a :
  (↑(↑(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})) :
          ℕ∞) :
      WithBot ℕ∞) ≤
    Order.krullDim.{u_2} (Submodule R M)
⊢ (↑(↑(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})) :
          ℕ∞) :
      WithBot ℕ∞) =
    Order.krullDim.{u_2} (Submodule R M)
have a₁ : Order.krullDim.{u_2} (Submodule R M) ≤
  (↑(↑(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})) :
        ℕ∞) :
    WithBot ℕ∞)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : CompositionSeries (Submodule R M)
h₁ :
  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 =
    ⊥
h₂ :
  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 =
    ⊤
H : IsFiniteLength R M
this_1 : IsNoetherian R M
this : IsArtinian R M
⊢ Order.krullDim.{u_2} (Submodule R M) ≤
    (↑(↑(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})) :
          ℕ∞) :
      WithBot ℕ∞)
have a : ∀ (i : LTSeries (Submodule R M)),
  LE.le (α := WithBot ℕ∞)
    (↑(i.length (r :=
          {x : Submodule R M × Submodule R M |
            match (motive := Submodule R M × Submodule R M → Prop) x with
            | (a, b) => a < b})) :
      WithBot ℕ∞)
    (↑(↑(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})) :
          ℕ∞) :
      WithBot ℕ∞)
Tactic: rw [Order.krullDim, iSup_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : CompositionSeries (Submodule R M)
h₁ :
  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 =
    ⊥
h₂ :
  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 =
    ⊤
H : IsFiniteLength R M
this_1 : IsNoetherian R M
this : IsArtinian R M
t : LTSeries (Submodule R M)
⊢ LE.le (α := WithBot ℕ∞)
    (↑(t.length (r :=
          {x : Submodule R M × Submodule R M |
            match (motive := Submodule R M × Submodule R M → Prop) x with
            | (a, b) => a < b})) :
      WithBot ℕ∞)
    (↑(↑(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})) :
          ℕ∞) :
      WithBot ℕ∞)
have a : LE.le (α := ℕ∞)
  (↑(t.length (r :=
        {x : Submodule R M × Submodule R M |
          match (motive := Submodule R M × Submodule R M → Prop) x with
          | (a, b) => a < b})) :
    ℕ∞)
  (↑(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})) :
    ℕ∞)
Tactic: refine WithBot.coe_le_coe.mpr ?_
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ length R M = ⊤ ↔ InfiniteDimensionalOrder.{u_2} (Submodule R M)
have rw : (↑(length R M) : WithBot ℕ∞) = (↑⊤ : WithBot ℕ∞) ↔ InfiniteDimensionalOrder.{u_2} (Submodule R M)
Tactic: rw [← WithBot.coe_inj, WithBot.coe_top, coe_length, Order.krullDim_eq_top_iff,
      ← not_finiteDimensionalOrder_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : (↑(length R M) : WithBot ℕ∞) = (↑⊤ : WithBot ℕ∞) ↔ InfiniteDimensionalOrder.{u_2} (Submodule R M)
⊢ length R M = ⊤ ↔ InfiniteDimensionalOrder.{u_2} (Submodule R M)
have rw₁ : (↑(length R M) : WithBot ℕ∞) = ⊤ ↔ InfiniteDimensionalOrder.{u_2} (Submodule R M)
Tactic: rw [← WithBot.coe_inj, WithBot.coe_top, coe_length, Order.krullDim_eq_top_iff,
      ← not_finiteDimensionalOrder_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : (↑(length R M) : WithBot ℕ∞) = (↑⊤ : WithBot ℕ∞) ↔ InfiniteDimensionalOrder.{u_2} (Submodule R M)
rw₁ : (↑(length R M) : WithBot ℕ∞) = ⊤ ↔ InfiniteDimensionalOrder.{u_2} (Submodule R M)
⊢ length R M = ⊤ ↔ InfiniteDimensionalOrder.{u_2} (Submodule R M)
have rw₂ : Order.krullDim.{u_2} (Submodule R M) = ⊤ ↔ InfiniteDimensionalOrder.{u_2} (Submodule R M)
Tactic: rw [← WithBot.coe_inj, WithBot.coe_top, coe_length, Order.krullDim_eq_top_iff,
      ← not_finiteDimensionalOrder_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : (↑(length R M) : WithBot ℕ∞) = (↑⊤ : WithBot ℕ∞) ↔ InfiniteDimensionalOrder.{u_2} (Submodule R M)
rw₁ : (↑(length R M) : WithBot ℕ∞) = ⊤ ↔ InfiniteDimensionalOrder.{u_2} (Submodule R M)
rw₂ : Order.krullDim.{u_2} (Submodule R M) = ⊤ ↔ InfiniteDimensionalOrder.{u_2} (Submodule R M)
⊢ length R M = ⊤ ↔ InfiniteDimensionalOrder.{u_2} (Submodule R M)
have rw₃ : InfiniteDimensionalOrder.{u_2} (Submodule R M) ↔ InfiniteDimensionalOrder.{u_2} (Submodule R M)
Tactic: rw [← WithBot.coe_inj, WithBot.coe_top, coe_length, Order.krullDim_eq_top_iff,
      ← not_finiteDimensionalOrder_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : (↑(length R M) : WithBot ℕ∞) = (↑⊤ : WithBot ℕ∞) ↔ InfiniteDimensionalOrder.{u_2} (Submodule R M)
rw₁ : (↑(length R M) : WithBot ℕ∞) = ⊤ ↔ InfiniteDimensionalOrder.{u_2} (Submodule R M)
rw₂ : Order.krullDim.{u_2} (Submodule R M) = ⊤ ↔ InfiniteDimensionalOrder.{u_2} (Submodule R M)
rw₃ : InfiniteDimensionalOrder.{u_2} (Submodule R M) ↔ InfiniteDimensionalOrder.{u_2} (Submodule R M)
⊢ length R M = ⊤ ↔ InfiniteDimensionalOrder.{u_2} (Submodule R M)
have rw₄ : ¬FiniteDimensionalOrder.{u_2} (Submodule R M) ↔ ¬FiniteDimensionalOrder.{u_2} (Submodule R M)
Tactic: rw [← WithBot.coe_inj, WithBot.coe_top, coe_length, Order.krullDim_eq_top_iff,
      ← not_finiteDimensionalOrder_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ length R M ≠ ⊤ ↔ FiniteDimensionalOrder.{u_2} (Submodule R M)
have rw : ¬length R M = ⊤ ↔ FiniteDimensionalOrder.{u_2} (Submodule R M)
Tactic: rw [Ne, length_eq_top_iff_infiniteDimensionalOrder, ← not_finiteDimensionalOrder_iff, not_not]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : ¬length R M = ⊤ ↔ FiniteDimensionalOrder.{u_2} (Submodule R M)
⊢ length R M ≠ ⊤ ↔ FiniteDimensionalOrder.{u_2} (Submodule R M)
have rw₁ : ¬InfiniteDimensionalOrder.{u_2} (Submodule R M) ↔ FiniteDimensionalOrder.{u_2} (Submodule R M)
Tactic: rw [Ne, length_eq_top_iff_infiniteDimensionalOrder, ← not_finiteDimensionalOrder_iff, not_not]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : ¬length R M = ⊤ ↔ FiniteDimensionalOrder.{u_2} (Submodule R M)
rw₁ : ¬InfiniteDimensionalOrder.{u_2} (Submodule R M) ↔ FiniteDimensionalOrder.{u_2} (Submodule R M)
⊢ length R M ≠ ⊤ ↔ FiniteDimensionalOrder.{u_2} (Submodule R M)
have rw₂ : ¬¬FiniteDimensionalOrder.{u_2} (Submodule R M) ↔ FiniteDimensionalOrder.{u_2} (Submodule R M)
Tactic: rw [Ne, length_eq_top_iff_infiniteDimensionalOrder, ← not_finiteDimensionalOrder_iff, not_not]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : ¬length R M = ⊤ ↔ FiniteDimensionalOrder.{u_2} (Submodule R M)
rw₁ : ¬InfiniteDimensionalOrder.{u_2} (Submodule R M) ↔ FiniteDimensionalOrder.{u_2} (Submodule R M)
rw₂ : ¬¬FiniteDimensionalOrder.{u_2} (Submodule R M) ↔ FiniteDimensionalOrder.{u_2} (Submodule R M)
⊢ length R M ≠ ⊤ ↔ FiniteDimensionalOrder.{u_2} (Submodule R M)
have rw₃ : FiniteDimensionalOrder.{u_2} (Submodule R M) ↔ FiniteDimensionalOrder.{u_2} (Submodule R M)
Tactic: rw [Ne, length_eq_top_iff_infiniteDimensionalOrder, ← not_finiteDimensionalOrder_iff, not_not]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ length R M ≠ ⊤ ↔ IsFiniteLength R M
have refine_1 : ∀ (h : length R M ≠ ⊤), IsFiniteLength R M
Tactic: refine ⟨fun h ↦ ?_, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
refine_1 : ∀ (h : length R M ≠ ⊤), IsFiniteLength R M
⊢ length R M ≠ ⊤ ↔ IsFiniteLength R M
have refine_2 : ∀ (H : IsFiniteLength R M), length R M ≠ ⊤
Tactic: refine ⟨fun h ↦ ?_, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Length (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h : length R M ≠ ⊤
⊢ IsFiniteLength R M
have h₁ : FiniteDimensionalOrder.{u_2} (Submodule R M)
Tactic: rw [length_ne_top_iff_finiteDimensionalOrder] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h : FiniteDimensionalOrder.{u_2} (Submodule R M)
⊢ IsFiniteLength R M
have refine_1 : (WellFounded fun (x1 x2 : Submodule R M) ↦ x1 > x2) ∧ WellFounded fun (x1 x2 : Submodule R M) ↦ x1 < x2
Tactic: rw [isFiniteLength_iff_isNoetherian_isArtinian, isNoetherian_iff, isArtinian_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R_1 : Type u_1
M : Type u_2
inst : Ring R_1
inst_1 : AddCommGroup M
inst_2 : Module R_1 M
h : FiniteDimensionalOrder.{u_2} (Submodule R_1 M)
R : SetRel (Submodule R_1 M) (Submodule R_1 M) :=
  {x : Submodule R_1 M × Submodule R_1 M |
    match (motive := Submodule R_1 M × Submodule R_1 M → Prop) x with
    | (N₁, N₂) => N₁ < N₂}
⊢ (WellFounded fun (x1 x2 : Submodule R_1 M) ↦ x1 > x2) ∧ WellFounded fun (x1 x2 : Submodule R_1 M) ↦ x1 < x2
have refine_1 : R.inv.IsWellFounded ∧ R.IsWellFounded
Tactic: change R.inv.IsWellFounded ∧ R.IsWellFounded
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
H : IsFiniteLength R M
⊢ length R M ≠ ⊤
have refine_2 : ∀ (s : CompositionSeries (Submodule R M))
  (hs₁ :
    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 =
      ⊥)
  (hs₂ :
    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 =
      ⊤),
  length R M ≠ ⊤
Tactic: obtain ⟨s, hs₁, hs₂⟩ := isFiniteLength_iff_exists_compositionSeries.mp H