-- 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 =
    ⊤
this :
  ∀
    (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)),
    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)))
rw :
  length B (B ⊗[A] M) =
    (↑(↑(Fin.last
                (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}))) :
            ℕ) :
        ℕ∞) *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
rw₁ :
  length B (B ⊗[A] M) =
    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})
            (Fin.last
              (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})))))
rw₂ :
  length B (B ⊗[A] M) =
    length B
      ↥(Submodule.baseChange B
          (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))
rw₃ : length B (B ⊗[A] M) = length B ↥(Submodule.baseChange B ⊤)
rw₄ : length B (B ⊗[A] M) = length B ↥⊤
rw₅ rw₆ : length B (B ⊗[A] M) = length B (B ⊗[A] M)
⊢ length B (B ⊗[A] M) =
    (↑(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})) :
        ℕ∞) *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))

Tactic:
rw [← Fin.val_last s.length, ← this, ← RelSeries.last, hs_top, baseChange_top, length_top]

Premises used: RelSeries.last, Module.length_top, RelSeries.length, Submodule.baseChange_top, Fin.val_last