awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Subsingleton R
⊢ length R M = 0

Tactic:
have := Module.subsingleton R M
  Module.length_eq_zero

Premises used: Module.length_eq_zero, Module.subsingleton
-- Module: Mathlib.RingTheory.Length
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
rw₃ rw₄ : Nontrivial M ↔ Nontrivial M
⊢ 0 < length R M ↔ Nontrivial M

Tactic:
rw [pos_iff_ne_zero, ne_eq, Module.length_eq_zero_iff, not_subsingleton_iff_nontrivial]

Premises used: ne_eq, Module.length_eq_zero_iff, not_subsingleton_iff_nontrivial, pos_iff_ne_zero
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial M
⊢ 0 < length R M

Tactic:
Module.length_pos_iff.mpr ‹_›

Premises used: Iff.mpr, Module.length_pos_iff
-- Module: Mathlib.RingTheory.Length
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 =
    ⊤
⊢ IsFiniteLength R M

Tactic:
have H := isFiniteLength_of_exists_compositionSeries ⟨s, h₁, h₂⟩
-- Module: Mathlib.RingTheory.Length
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
⊢ IsNoetherian R M

Tactic:
have := (isFiniteLength_iff_isNoetherian_isArtinian.mp H).1
-- Module: Mathlib.RingTheory.Length
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
⊢ IsArtinian R M

Tactic:
have := (isFiniteLength_iff_isNoetherian_isArtinian.mp H).2
-- Module: Mathlib.RingTheory.Length
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
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)
⊢ (↑(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

Tactic:
rw [← WithBot.coe_inj, Module.coe_length]

Premises used: Module.coe_length, WithBot.coe_inj
-- Module: Mathlib.RingTheory.Length
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)
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 ℕ∞)
⊢ (↑(↑(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

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Length
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)

Tactic:
(Order.LTSeries.length_le_krullDim <| s.map ⟨id, fun h ↦ h.1⟩)

Premises used: Order.LTSeries.length_le_krullDim, RelSeries.map, CovBy, setOf, id, Set.Subset, And.left, RelHom.mk
-- Module: Mathlib.RingTheory.Length
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)

Tactic:
exact (Order.LTSeries.length_le_krullDim <| s.map ⟨id, fun h ↦ h.1⟩)

Premises used: Order.LTSeries.length_le_krullDim, RelSeries.map, id, And.left, RelHom.mk
-- Module: Mathlib.RingTheory.Length
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 :
  ∀ (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 ℕ∞)
⊢ 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:
rw [Order.krullDim, iSup_le_iff]

Premises used: Order.krullDim, iSup_le_iff
-- Module: Mathlib.RingTheory.Length
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 ℕ∞)

Tactic:
WithBot.coe_le_coe.mpr ?_

Premises used: Iff.mpr, WithBot.coe_le_coe
-- Module: Mathlib.RingTheory.Length
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)
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})) :
      ℕ∞)
⊢ 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 ℕ∞)

Tactic:
refine WithBot.coe_le_coe.mpr ?_

Premises used: Iff.mpr, WithBot.coe_le_coe
-- Module: Mathlib.RingTheory.Length
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_2 : IsArtinian R M
t : LTSeries (Submodule R M)
t' :
  RelSeries (α := Submodule R M)
    {x : Submodule R M × Submodule R M |
      match (motive := Submodule R M × Submodule R M → Prop) x with
      | (a, b) => a ⋖ b}
i :
  Fin
      (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}) +
        1) ↪
    Fin
      (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}) +
        1)
hi :
  t'.toFun (r :=
        {x : Submodule R M × Submodule R M |
          match (motive := Submodule R M × Submodule R M → Prop) x with
          | (a, b) => a ⋖ b}) ∘
      (⇑i : (a : Fin (t.length + 1)) → Fin (t'.length + 1)) =
    t.toFun (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (a, b) => a < b})
ht₁ :
  t'.head (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (a, b) => a ⋖ b}) =
    ⊥
ht₂ :
  t'.last (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (a, b) => a ⋖ b}) =
    ⊤
this :
  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})) ≃
    Fin
      (t'.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}))
⊢ 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}) ≤
    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})

Tactic:
simpa using Fintype.card_le_of_embedding i

Premises used: Fintype.card_le_of_embedding
-- Module: Mathlib.RingTheory.Length
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_2 : IsArtinian R M
t : LTSeries (Submodule R M)
t' :
  RelSeries (α := Submodule R M)
    {x : Submodule R M × Submodule R M |
      match (motive := Submodule R M × Submodule R M → Prop) x with
      | (a, b) => a ⋖ b}
i :
  Fin
      (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}) +
        1) ↪
    Fin
      (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}) +
        1)
hi :
  t'.toFun (r :=
        {x : Submodule R M × Submodule R M |
          match (motive := Submodule R M × Submodule R M → Prop) x with
          | (a, b) => a ⋖ b}) ∘
      (⇑i : (a : Fin (t.length + 1)) → Fin (t'.length + 1)) =
    t.toFun (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (a, b) => a < b})
ht₁ :
  t'.head (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (a, b) => a ⋖ b}) =
    ⊥
ht₂ :
  t'.last (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (a, b) => a ⋖ b}) =
    ⊤
this :
  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})) ≃
    Fin
      (t'.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}))
⊢ 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}) ≤
    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})

Tactic:
have h : t.length ≤ t'.length := by simpa using Fintype.card_le_of_embedding i
-- Module: Mathlib.RingTheory.Length
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)
rw₄ rw₅ : ¬FiniteDimensionalOrder.{u_2} (Submodule R M) ↔ ¬FiniteDimensionalOrder.{u_2} (Submodule R M)
⊢ length 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]

Premises used: Module.coe_length, WithBot.coe_top, WithBot.coe_inj, not_finiteDimensionalOrder_iff, Order.krullDim_eq_top_iff
-- Module: Mathlib.RingTheory.Length
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)
rw₃ rw₄ : FiniteDimensionalOrder.{u_2} (Submodule R M) ↔ FiniteDimensionalOrder.{u_2} (Submodule R M)
⊢ length R M ≠ ⊤ ↔ FiniteDimensionalOrder.{u_2} (Submodule R M)

Tactic:
rw [Ne, length_eq_top_iff_infiniteDimensionalOrder, ← not_finiteDimensionalOrder_iff, not_not]

Premises used: Classical.not_not, Module.length_eq_top_iff_infiniteDimensionalOrder, Ne, not_finiteDimensionalOrder_iff
-- Module: Mathlib.RingTheory.Length
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

Tactic:
⟨fun h ↦ ?_, fun H ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.Length
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
refine_2 : ∀ (H : IsFiniteLength R M), length R M ≠ ⊤
⊢ length R M ≠ ⊤ ↔ IsFiniteLength R M

Tactic:
refine ⟨fun h ↦ ?_, fun H ↦ ?_⟩
-- Module: Mathlib.RingTheory.Length
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 ≠ ⊤
⊢ FiniteDimensionalOrder.{u_2} (Submodule R M)

Tactic:
rw [length_ne_top_iff_finiteDimensionalOrder] at h

Premises used: Module.length_ne_top_iff_finiteDimensionalOrder
-- Module: Mathlib.RingTheory.Length
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)
refine_1 : (WellFounded fun (x1 x2 : Submodule R M) ↦ x1 > x2) ∧ WellFounded fun (x1 x2 : Submodule R M) ↦ x1 < x2
⊢ IsFiniteLength R M

Tactic:
rw [isFiniteLength_iff_isNoetherian_isArtinian, isNoetherian_iff, isArtinian_iff]

Premises used: isArtinian_iff, isFiniteLength_iff_isNoetherian_isArtinian, isNoetherian_iff
-- Module: Mathlib.RingTheory.Length
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₂}
refine_1 : R.inv.IsWellFounded ∧ R.IsWellFounded
⊢ (WellFounded fun (x1 x2 : Submodule R_1 M) ↦ x1 > x2) ∧ WellFounded fun (x1 x2 : Submodule R_1 M) ↦ x1 < x2

Tactic:
change R.inv.IsWellFounded ∧ R.IsWellFounded

Premises used: SetRel.inv, SetRel.IsWellFounded