-- Module: Mathlib.RingTheory.LocalRing.Length
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Module B M
inst_9 : IsScalarTower A B M
h : IsFiniteLength B M
s : CompositionSeries (Submodule B M)
hs_bot :
  RelSeries.head (r :=
      {x : Submodule B M × Submodule B M |
        match (motive := Submodule B M × Submodule B M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊥
hs_top :
  RelSeries.last (r :=
      {x : Submodule B M × Submodule B M |
        match (motive := Submodule B M × Submodule B M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊤
k :
  Fin
    (s.length (r :=
        {x : Submodule B M × Submodule B M |
          match (motive := Submodule B M × Submodule B M → Prop) x with
          | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y}) +
      1)
pos :
  length.{u_1, u_3} A
      ↥(s.toFun (r :=
          {x : Submodule B M × Submodule B M |
            match (motive := Submodule B M × Submodule B M → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
          0) =
    (↑(↑0 : ℕ) : ℕ∞) * length.{u_1, u_2} (ResidueField A) (ResidueField B)
pos₁ :
  ∀
    (i :
      Fin
        (s.length (r :=
          {x : Submodule B M × Submodule B M |
            match (motive := Submodule B M × Submodule B M → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})))
    (hi :
      length.{u_1, u_3} A
          ↥(s.toFun (r :=
              {x : Submodule B M × Submodule B M |
                match (motive := Submodule B M × Submodule B M → Prop) x with
                | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
              i.castSucc) =
        (↑(↑i.castSucc : ℕ) : ℕ∞) * length.{u_1, u_2} (ResidueField A) (ResidueField B)),
    length.{u_1, u_3} A
        ↥(s.toFun (r :=
            {x : Submodule B M × Submodule B M |
              match (motive := Submodule B M × Submodule B M → Prop) x with
              | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
            i.succ) =
      (↑(↑i.succ : ℕ) : ℕ∞) * length.{u_1, u_2} (ResidueField A) (ResidueField B)
⊢ length.{u_1, u_3} A
      ↥(s.toFun (r :=
          {x : Submodule B M × Submodule B M |
            match (motive := Submodule B M × Submodule B M → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
          k) =
    (↑(↑k : ℕ) : ℕ∞) * length.{u_1, u_2} (ResidueField A) (ResidueField B)

Tactic:
induction k using Fin.induction with
    | zero => rw [← RelSeries.head, hs_bot]; simp
    | succ i hi => simpa [hi, add_one_mul] using (s.step i).length_restrictScalars A

Premises used: add_one_mul, Submodule.zero, RelSeries.head