awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂}
⊢ R.inv.IsWellFounded ∧ R.IsWellFounded

Tactic:
⟨.of_finiteDimensional R.inv, .of_finiteDimensional R⟩

Premises used: SetRel.inv, SetRel.IsWellFounded.of_finiteDimensional, And.intro
-- 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₂}
⊢ R.inv.IsWellFounded ∧ R.IsWellFounded

Tactic:
exact ⟨.of_finiteDimensional R.inv, .of_finiteDimensional R⟩
-- 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 : IsFiniteLength R M
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 ≠ ⊤
⊢ length R M ≠ ⊤

Tactic:
obtain ⟨s, hs₁, hs₂⟩ := isFiniteLength_iff_exists_compositionSeries.mp H

Premises used: isFiniteLength_iff_exists_compositionSeries, Iff.mp
-- 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 : IsFiniteLength R M
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 =
    ⊤
refine_2 :
  Ne (α := ℕ∞)
    (↑(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 [← length_compositionSeries s hs₁ hs₂]

Premises used: Module.length_compositionSeries
-- 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 : IsFiniteLength R M
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 =
    ⊤
⊢ Ne (α := ℕ∞)
    (↑(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:
simp
-- 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 : IsArtinian R M
inst_4 : IsNoetherian R M
rw : IsNoetherian R M ∧ IsArtinian R M
⊢ length R M ≠ ⊤

Tactic:
rw [length_ne_top_iff, isFiniteLength_iff_isNoetherian_isArtinian]

Premises used: Module.length_ne_top_iff, isFiniteLength_iff_isNoetherian_isArtinian
-- 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 : IsArtinian R M
inst_4 : IsNoetherian R M
⊢ IsNoetherian R M ∧ IsArtinian R M

Tactic:
⟨‹_›, ‹_›⟩

Premises used: And.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
inst_3 : IsArtinian R M
inst_4 : IsNoetherian R M
⊢ IsNoetherian R M ∧ IsArtinian R M

Tactic:
exact ⟨‹_›, ‹_›⟩
-- 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 ≠ ⊤ ↔ IsFiniteLength R M
rw₁ rw₂ : IsFiniteLength R M ↔ IsFiniteLength R M
⊢ FiniteDimensionalOrder.{u_2} (Submodule R M) ↔ IsFiniteLength R M

Tactic:
rw [← Module.length_ne_top_iff_finiteDimensionalOrder, Module.length_ne_top_iff]

Premises used: Module.length_ne_top_iff, 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
inst_3 : IsArtinian R M
inst_4 : IsNoetherian R M
rw : IsNoetherian R M ∧ IsArtinian R M
⊢ FiniteDimensionalOrder.{u_2} (Submodule R M)

Tactic:
rw [Module.finiteDimensionalOrder_submodule_iff, isFiniteLength_iff_isNoetherian_isArtinian]

Premises used: Module.finiteDimensionalOrder_submodule_iff, isFiniteLength_iff_isNoetherian_isArtinian
-- 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 : IsArtinian R M
inst_4 left : IsNoetherian R M
right : IsArtinian R M
⊢ IsNoetherian R M ∧ IsArtinian R M

Tactic:
tauto
-- 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
N : Submodule R M
a : (↑(length.{u_1, u_2} R ↥N) : WithBot ℕ∞) = (↑(Order.height N) : WithBot ℕ∞)
⊢ length.{u_1, u_2} R ↥N = Order.height N

Tactic:
apply WithBot.coe_injective

Premises used: WithBot.coe_injective
-- 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
N : Submodule R M
a : (↑(length.{u_1, u_2} R ↥N) : WithBot ℕ∞) = Order.krullDim.{u_2} (↑(Set.Iic N) : Type u_2)
a₁ : Order.krullDim.{u_2} (Submodule R ↥N) = Order.krullDim.{u_2} (↑(Set.Iic N) : Type u_2)
a₂ a₃ : Order.krullDim.{u_2} (↑(Set.Iic N) : Type u_2) = Order.krullDim.{u_2} (↑(Set.Iic N) : Type u_2)
⊢ (↑(length.{u_1, u_2} R ↥N) : WithBot ℕ∞) = (↑(Order.height N) : WithBot ℕ∞)

Tactic:
rw [Order.height_eq_krullDim_Iic, coe_length, Order.krullDim_eq_of_orderIso (Submodule.mapIic _)]

Premises used: Submodule.mapIic, Module.coe_length, Order.krullDim_eq_of_orderIso, Order.height_eq_krullDim_Iic
-- 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
N : Submodule R M
a : (↑(length.{u_1, u_2} R (M ⧸ N)) : WithBot ℕ∞) = (↑(Order.coheight N) : WithBot ℕ∞)
⊢ length.{u_1, u_2} R (M ⧸ N) = Order.coheight N

Tactic:
apply WithBot.coe_injective

Premises used: WithBot.coe_injective
-- 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
N : Submodule R M
a : (↑(length.{u_1, u_2} R (M ⧸ N)) : WithBot ℕ∞) = Order.krullDim.{u_2} (↑(Set.Ici N) : Type u_2)
a₁ : Order.krullDim.{u_2} (Submodule R (M ⧸ N)) = Order.krullDim.{u_2} (↑(Set.Ici N) : Type u_2)
a₂ a₃ : Order.krullDim.{u_2} (↑(Set.Ici N) : Type u_2) = Order.krullDim.{u_2} (↑(Set.Ici N) : Type u_2)
⊢ (↑(length.{u_1, u_2} R (M ⧸ N)) : WithBot ℕ∞) = (↑(Order.coheight N) : WithBot ℕ∞)

Tactic:
rw [Order.coheight_eq_krullDim_Ici, coe_length,
    Order.krullDim_eq_of_orderIso (Submodule.comapMkQRelIso N)]

Premises used: Module.coe_length, Order.krullDim_eq_of_orderIso, Order.coheight_eq_krullDim_Ici, Submodule.comapMkQRelIso
-- 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
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
e : M ≃ₗ[R] N
a : (↑(Module.length R M) : WithBot ℕ∞) = (↑(Module.length R N) : WithBot ℕ∞)
⊢ Module.length R M = Module.length R N

Tactic:
apply WithBot.coe_injective

Premises used: WithBot.coe_injective
-- 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
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
e : M ≃ₗ[R] N
a : Order.krullDim.{u_2} (Submodule R M) = (↑(Module.length R N) : WithBot ℕ∞)
a₁ : Order.krullDim.{u_2} (Submodule R M) = Order.krullDim.{u_3} (Submodule R N)
a₂ a₃ : Order.krullDim.{u_3} (Submodule R N) = Order.krullDim.{u_3} (Submodule R N)
⊢ (↑(Module.length R M) : WithBot ℕ∞) = (↑(Module.length R N) : WithBot ℕ∞)

Tactic:
rw [Module.coe_length, Module.coe_length,
    Order.krullDim_eq_of_orderIso (Submodule.orderIsoMapComap e)]

Premises used: Module.coe_length, Order.krullDim_eq_of_orderIso, Submodule.orderIsoMapComap
-- 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 : Type u_3
inst_3 : CommRing S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
h : Function.Surjective.{u_3 + 1, u_1 + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
⊢ RingHomSurjective (algebraMap S R)

Tactic:
have : RingHomSurjective (algebraMap S R) := ⟨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 : Type u_3
inst_3 : CommRing S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
h : Function.Surjective.{u_3 + 1, u_1 + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
this : RingHomSurjective (algebraMap S R)
⊢ ∀ (m : S) (x : M),
    AddHom.toFun (AddHom.id M) (m • x) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((algebraMap S R : (a : S) → R) m : R) (AddHom.toFun (AddHom.id M) x)

Tactic:
simp
-- 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 : Type u_3
inst_3 : CommRing S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
h : Function.Surjective.{u_3 + 1, u_1 + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
this : RingHomSurjective (algebraMap S R)
f : M →ₛₗ[algebraMap S R] M := { toAddHom := AddHom.id M, map_smul' := ⋯ }
rw : (Order.krullDim.{u_2} (Submodule S M)).unbot ⋯ = length R M
rw₁ : (Order.krullDim.{u_2} (Submodule S M)).unbot ⋯ = (Order.krullDim.{u_2} (Submodule R M)).unbot ⋯
rw₂ : Order.krullDim.{u_2} (Submodule S M) = Order.krullDim.{u_2} (Submodule R M)
rw₃ rw₄ : Order.krullDim.{u_2} (Submodule R M) = Order.krullDim.{u_2} (Submodule R M)
⊢ length S M = length R M

Tactic:
rw [Module.length, Module.length, WithBot.unbot_inj,
    Order.krullDim_eq_of_orderIso (Submodule.orderIsoMapComapOfBijective f Function.bijective_id)]

Premises used: Function.bijective_id, WithBot.unbot_inj, Order.krullDim_eq_of_orderIso, Module.length, Submodule.orderIsoMapComapOfBijective
-- 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.{u_1, u_2} R ↥⊥ = 0

Tactic:
Module.length_eq_zero

Premises used: Module.length_eq_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
rw : Order.height.{u_2} (α := Submodule R M) ⊤ = length R M
rw₁ rw₂ : Order.height.{u_2} (α := Submodule R M) ⊤ = Order.height.{u_2} (α := Submodule R M) ⊤
⊢ length.{u_1, u_2} R ↥⊤ = length R M

Tactic:
rw [Module.length_submodule, Module.length_eq_height]

Premises used: Module.length_submodule, Module.length_eq_height
-- 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 : IsArtinian R M
inst_4 : IsNoetherian R M
N : Submodule R M
⊢ Order.height N < ⊤

Tactic:
simpa only [← Module.length_submodule] using Module.length_ne_top.lt_top

Premises used: Module.length_submodule, Ne.lt_top, Module.length_ne_top
-- 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 : IsArtinian R M
inst_4 : IsNoetherian R M
⊢ StrictMono.{u_2, 0} (α := Submodule R M) Order.height

Tactic:
fun N _ h ↦ Order.height_strictMono h N.height_lt_top

Premises used: StrictMono, Order.height_strictMono, Submodule.height_lt_top
-- 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 : IsArtinian R M
inst_4 : IsNoetherian R M
N : Submodule R M
h : N ≠ ⊤
⊢ Module.length.{u_1, u_2} R ↥N < Module.length R M

Tactic:
simpa [← Module.length_top (M := M), Module.length_submodule] using height_strictMono h.lt_top

Premises used: Submodule.height_strictMono, Module.length_top, Module.length_submodule, Ne.lt_top
-- 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
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R N
inst_6 : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
H : Function.Exact.{u_3, u_2, u_4} (M := N) (N := M) (P := P) (⇑f : (a : N) → M) (⇑g : (a : M) → P)
pos : ∀ (hP : IsFiniteLength R P), length R M = length R N + length R P
neg : ∀ (hP : ¬IsFiniteLength R P), length R M = length R N + length R P
⊢ length R M = length R N + length R P

Tactic:
by_cases hP : IsFiniteLength R P

Premises used: IsFiniteLength
-- 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
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R N
inst_6 : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
H : Function.Exact.{u_3, u_2, u_4} (M := N) (N := M) (P := P) (⇑f : (a : N) → M) (⇑g : (a : M) → P)
hP : IsFiniteLength R P
pos : ∀ (hN : IsFiniteLength R N), length R M = length R N + length R P
neg : ∀ (hN : ¬IsFiniteLength R N), length R M = length R N + length R P
⊢ length R M = length R N + length R P

Tactic:
by_cases hN : IsFiniteLength R N

Premises used: IsFiniteLength
-- 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
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R N
inst_6 : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
H : Function.Exact.{u_3, u_2, u_4} (M := N) (N := M) (P := P) (⇑f : (a : N) → M) (⇑g : (a : M) → P)
hP : IsFiniteLength R P
hN : IsFiniteLength R N
pos :
  ∀ (s : CompositionSeries (Submodule R P))
    (hs₁ :
      RelSeries.head (r :=
          {x : Submodule R P × Submodule R P |
            match (motive := Submodule R P × Submodule R P → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
          s =
        ⊥)
    (hs₂ :
      RelSeries.last (r :=
          {x : Submodule R P × Submodule R P |
            match (motive := Submodule R P × Submodule R P → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
          s =
        ⊤),
    length R M = length R N + length R P
⊢ length R M = length R N + length R P

Tactic:
obtain ⟨s, hs₁, hs₂⟩ := isFiniteLength_iff_exists_compositionSeries.mp hP

Premises used: isFiniteLength_iff_exists_compositionSeries, Iff.mp
-- 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
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R N
inst_6 : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
H : Function.Exact.{u_3, u_2, u_4} (M := N) (N := M) (P := P) (⇑f : (a : N) → M) (⇑g : (a : M) → P)
hP : IsFiniteLength R P
hN : IsFiniteLength R N
s : CompositionSeries (Submodule R P)
hs₁ :
  RelSeries.head (r :=
      {x : Submodule R P × Submodule R P |
        match (motive := Submodule R P × Submodule R P → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊥
hs₂ :
  RelSeries.last (r :=
      {x : Submodule R P × Submodule R P |
        match (motive := Submodule R P × Submodule R P → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊤
pos :
  ∀ (t : CompositionSeries (Submodule R N))
    (ht₁ :
      RelSeries.head (r :=
          {x : Submodule R N × Submodule R N |
            match (motive := Submodule R N × Submodule R N → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
          t =
        ⊥)
    (ht₂ :
      RelSeries.last (r :=
          {x : Submodule R N × Submodule R N |
            match (motive := Submodule R N × Submodule R N → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
          t =
        ⊤),
    length R M = length R N + length R P
⊢ length R M = length R N + length R P

Tactic:
obtain ⟨t, ht₁, ht₂⟩ := isFiniteLength_iff_exists_compositionSeries.mp hN

Premises used: isFiniteLength_iff_exists_compositionSeries, Iff.mp
-- 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
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R N
inst_6 : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
H : Function.Exact.{u_3, u_2, u_4} (M := N) (N := M) (P := P) (⇑f : (a : N) → M) (⇑g : (a : M) → P)
hP : IsFiniteLength R P
hN : ¬IsFiniteLength R N
⊢ ¬IsFiniteLength R M

Tactic:
have := mt (IsFiniteLength.of_injective · hf) hN
-- 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
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R N
inst_6 : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
H : Function.Exact.{u_3, u_2, u_4} (M := N) (N := M) (P := P) (⇑f : (a : N) → M) (⇑g : (a : M) → P)
hP : IsFiniteLength R P
hN : ¬IsFiniteLength R N
this : ¬IsFiniteLength R M
⊢ length R N = ⊤

Tactic:
rw [← Module.length_ne_top_iff, ne_eq, not_not] at hN this

Premises used: Classical.not_not, Module.length_ne_top_iff, ne_eq
-- 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
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R N
inst_6 : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
H : Function.Exact.{u_3, u_2, u_4} (M := N) (N := M) (P := P) (⇑f : (a : N) → M) (⇑g : (a : M) → P)
hP : IsFiniteLength R P
hN : ¬IsFiniteLength R N
this : ¬IsFiniteLength R M
hN₁ : length R N = ⊤
⊢ length R M = ⊤

Tactic:
rw [← Module.length_ne_top_iff, ne_eq, not_not] at hN this

Premises used: Classical.not_not, Module.length_ne_top_iff, ne_eq
-- 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
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R N
inst_6 : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
H : Function.Exact.{u_3, u_2, u_4} (M := N) (N := M) (P := P) (⇑f : (a : N) → M) (⇑g : (a : M) → P)
hP : IsFiniteLength R P
hN : length R N = ⊤
this : length R M = ⊤
neg : length R M = ⊤ + length R P
neg₁ : ⊤ = ⊤ + length R P
neg₂ neg₃ : Eq (α := ℕ∞) ⊤ ⊤
⊢ length R M = length R N + length R P

Tactic:
rw [hN, this, top_add]

Premises used: top_add
-- 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
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R N
inst_6 : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
H : Function.Exact.{u_3, u_2, u_4} (M := N) (N := M) (P := P) (⇑f : (a : N) → M) (⇑g : (a : M) → P)
hP : ¬IsFiniteLength R P
⊢ ¬IsFiniteLength R M

Tactic:
have := mt (IsFiniteLength.of_surjective · hg) hP
-- 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
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R N
inst_6 : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
H : Function.Exact.{u_3, u_2, u_4} (M := N) (N := M) (P := P) (⇑f : (a : N) → M) (⇑g : (a : M) → P)
hP : ¬IsFiniteLength R P
this : ¬IsFiniteLength R M
⊢ length R P = ⊤

Tactic:
rw [← Module.length_ne_top_iff, ne_eq, not_not] at hP this

Premises used: Classical.not_not, Module.length_ne_top_iff, ne_eq
-- 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
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R N
inst_6 : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
H : Function.Exact.{u_3, u_2, u_4} (M := N) (N := M) (P := P) (⇑f : (a : N) → M) (⇑g : (a : M) → P)
hP : ¬IsFiniteLength R P
this : ¬IsFiniteLength R M
hP₁ : length R P = ⊤
⊢ length R M = ⊤

Tactic:
rw [← Module.length_ne_top_iff, ne_eq, not_not] at hP this

Premises used: Classical.not_not, Module.length_ne_top_iff, ne_eq
-- 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
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R N
inst_6 : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
H : Function.Exact.{u_3, u_2, u_4} (M := N) (N := M) (P := P) (⇑f : (a : N) → M) (⇑g : (a : M) → P)
hP : length R P = ⊤
this : length R M = ⊤
neg : length R M = length R N + ⊤
neg₁ : ⊤ = length R N + ⊤
neg₂ neg₃ : Eq (α := ℕ∞) ⊤ ⊤
⊢ length R M = length R N + length R P

Tactic:
rw [hP, this, add_top]

Premises used: add_top