-- 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 : Flat A B
h : IsFiniteLength A M
s : CompositionSeries (Submodule A M)
hs_bot :
  RelSeries.head (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊥
hs_top :
  RelSeries.last (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊤
k :
  Fin
    (s.length (r :=
        {x : Submodule A M × Submodule A M |
          match (motive := Submodule A M × Submodule A M → Prop) x with
          | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y}) +
      1)
pos :
  length B
      ↥(Submodule.baseChange B
          (s.toFun (r :=
            {x : Submodule A M × Submodule A M |
              match (motive := Submodule A M × Submodule A M → Prop) x with
              | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
            0)) =
    (↑(↑0 : ℕ) : ℕ∞) *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
pos₁ :
  ∀
    (i :
      Fin
        (s.length (r :=
          {x : Submodule A M × Submodule A M |
            match (motive := Submodule A M × Submodule A M → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})))
    (hi :
      length B
          ↥(Submodule.baseChange B
              (s.toFun (r :=
                {x : Submodule A M × Submodule A M |
                  match (motive := Submodule A M × Submodule A M → Prop) x with
                  | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
                i.castSucc)) =
        (↑(↑i.castSucc : ℕ) : ℕ∞) *
          length B
            (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))),
    length B
        ↥(Submodule.baseChange B
            (s.toFun (r :=
              {x : Submodule A M × Submodule A M |
                match (motive := Submodule A M × Submodule A M → Prop) x with
                | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
              i.succ)) =
      (↑(↑i.succ : ℕ) : ℕ∞) *
        length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
⊢ length B
      ↥(Submodule.baseChange B
          (s.toFun (r :=
            {x : Submodule A M × Submodule A M |
              match (motive := Submodule A M × Submodule A M → Prop) x with
              | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
            k)) =
    (↑(↑k : ℕ) : ℕ∞) *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))

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

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