-- 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 =
    ⊤
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 =
    ⊤
s' : CompositionSeries (Submodule R M) :=
  RelSeries.map (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 :=
    {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
    (RelHom.mk (r := fun (x1 x2 : Submodule R P) ↦
      Membership.mem (γ := SetRel (Submodule R P) (Submodule R P))
        {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}
        (x1, x2))
      (s := fun (x1 x2 : Submodule R M) ↦
      Membership.mem (γ := SetRel (Submodule R M) (Submodule R M))
        {x : Submodule R M × Submodule R M |
          match (motive := Submodule R M × Submodule R M → Prop) x with
          | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y}
        (x1, x2))
      (Submodule.comap g) ⋯)
t' : CompositionSeries (Submodule R M) :=
  RelSeries.map (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})
    (s :=
    {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
    (RelHom.mk (r := fun (x1 x2 : Submodule R N) ↦
      Membership.mem (γ := SetRel (Submodule R N) (Submodule R N))
        {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}
        (x1, x2))
      (s := fun (x1 x2 : Submodule R M) ↦
      Membership.mem (γ := SetRel (Submodule R M) (Submodule R M))
        {x : Submodule R M × Submodule R M |
          match (motive := Submodule R M × Submodule R M → Prop) x with
          | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y}
        (x1, x2))
      (Submodule.map f) ⋯)
hfg : Submodule.map f ⊤ = Submodule.comap g ⊥
r : RelSeries (α := Submodule R M)
  {x : Submodule R M × Submodule R M |
    match (motive := Submodule R M × Submodule R M → Prop) x with
    | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y} :=
  RelSeries.smash (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' s' ⋯
pos :
  (↑(r.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})) :
      ℕ∞) =
    HAdd.hAdd (α := ℕ∞)
      (↑(t.length (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})) :
        ℕ∞)
      (↑(s.length (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})) :
        ℕ∞)
⊢ length R M = length R N + length R P

Tactic:
rw [← Module.length_compositionSeries s hs₁ hs₂,
        ← Module.length_compositionSeries t ht₁ ht₂,
        ← Module.length_compositionSeries r
          (by simpa [r, t', ht₁, -Submodule.map_bot] using Submodule.map_bot f)
          (by simpa [r, s', hs₂, -Submodule.comap_top] using Submodule.comap_top g)]

Premises used: Module.length_compositionSeries