-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Length (goal)
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)))
⊢ 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)))
have 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)))
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
Cleared hypotheses: k