awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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 =
    ⊤
this :
  ∀
    (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)),
    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)
⊢ length A M =
    (↑(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})) :
        ℕ∞) *
      length.{u_1, u_2} (ResidueField A) (ResidueField B)
have rw : length A M = length.{u_1, u_3} A ↥⊤
Tactic: rw [← Fin.val_last s.length, ← this, ← RelSeries.last, hs_top]
-- 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 : 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 =
    ⊤
⊢ length A M =
    (↑(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})) :
        ℕ∞) *
      length.{u_1, u_2} (ResidueField A) (ResidueField B)
have pos : ∀
  (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)),
  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: suffices ∀ k, length A (s k) = k * Module.length (ResidueField A) (ResidueField B) by
      rw [← Fin.val_last s.length, ← this, ← RelSeries.last, hs_top]
      exact length_top.symm
-- 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 : 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 =
    ⊤
⊢ 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)
have pos : length.{u_1, u_3} A ↥⊥ = (↑(↑0 : ℕ) : ℕ∞) * length.{u_1, u_2} (ResidueField A) (ResidueField B)
Tactic: rw [← RelSeries.head, hs_bot]
-- 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 : 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)
⊢ 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)
have 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)
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
Cleared hypotheses: k
-- 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 : 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)
⊢ 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)
have 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)
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
Cleared hypotheses: k
-- 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 : Module B M
inst_9 : IsScalarTower A B M
h : ¬IsFiniteLength B M
⊢ ¬IsFiniteLength A M
have contrapose! : ∀ (h : IsFiniteLength A M), IsFiniteLength B M
Tactic: contrapose! h
Cleared hypotheses: h
-- 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 : Module B M
inst_9 : IsScalarTower A B M
h : IsFiniteLength A M
⊢ IsFiniteLength B M
have rw : ∀ (h : IsNoetherian A M ∧ IsArtinian A M), IsNoetherian B M ∧ IsArtinian B M
Tactic: rw [isFiniteLength_iff_isNoetherian_isArtinian] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Length (hypothesis)
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
⊢ length A M = length B M * length.{u_1, u_2} (ResidueField A) (ResidueField B)
have this : ¬IsFiniteLength A M
Tactic: have : ¬ IsFiniteLength A M := by
      contrapose! h
      rw [isFiniteLength_iff_isNoetherian_isArtinian] at h ⊢
      exact h.imp (isNoetherian_of_tower A) (isArtinian_of_tower A)
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Length (hypothesis)
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
this : ¬IsFiniteLength A M
⊢ length A M = length B M * length.{u_1, u_2} (ResidueField A) (ResidueField B)
have h₁ : length B M = ⊤
Tactic: rw [← length_ne_top_iff, not_ne_iff] at h this
Cleared hypotheses: h, this
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Length (hypothesis)
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
this : ¬IsFiniteLength A M
h₁ : length B M = ⊤
⊢ length A M = length B M * length.{u_1, u_2} (ResidueField A) (ResidueField B)
have this₁ : length A M = ⊤
Tactic: rw [← length_ne_top_iff, not_ne_iff] at h this
Cleared hypotheses: h, this
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Length (hypothesis)
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 : length B M = ⊤
this : length A M = ⊤
⊢ length A M = length B M * length.{u_1, u_2} (ResidueField A) (ResidueField B)
have ne : length.{u_1, u_2} (ResidueField A) (ResidueField B) ≠ 0
Tactic: have ne : length (ResidueField A) (ResidueField B) ≠ 0 := by
      simpa [pos_iff_ne_zero] using Module.length_pos
-- 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 : Module B M
inst_9 : IsScalarTower A B M
h : length B M = ⊤
this : length A M = ⊤
ne : length.{u_1, u_2} (ResidueField A) (ResidueField B) ≠ 0
⊢ length A M = length B M * length.{u_1, u_2} (ResidueField A) (ResidueField B)
have neg : length A M = ⊤ * length.{u_1, u_2} (ResidueField A) (ResidueField B)
Tactic: rw [h, this, ENat.top_mul ne]
-- 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 : Module B M
inst_9 : IsScalarTower A B M
h : length B M = ⊤
this : length A M = ⊤
ne : length.{u_1, u_2} (ResidueField A) (ResidueField B) ≠ 0
neg : length A M = ⊤ * length.{u_1, u_2} (ResidueField A) (ResidueField B)
⊢ length A M = length B M * length.{u_1, u_2} (ResidueField A) (ResidueField B)
have neg₁ : ⊤ = ⊤ * length.{u_1, u_2} (ResidueField A) (ResidueField B)
Tactic: rw [h, this, ENat.top_mul ne]
-- 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 : Module B M
inst_9 : IsScalarTower A B M
h : length B M = ⊤
this : length A M = ⊤
ne : length.{u_1, u_2} (ResidueField A) (ResidueField B) ≠ 0
neg : length A M = ⊤ * length.{u_1, u_2} (ResidueField A) (ResidueField B)
neg₁ : ⊤ = ⊤ * length.{u_1, u_2} (ResidueField A) (ResidueField B)
⊢ length A M = length B M * length.{u_1, u_2} (ResidueField A) (ResidueField B)
have neg₂ : Eq (α := ℕ∞) ⊤ ⊤
Tactic: rw [h, this, ENat.top_mul ne]
-- 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
⊢ length B (B ⊗[A] M) =
    length A M *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
have pos : ∀ (h : IsFiniteLength A M),
  length B (B ⊗[A] M) =
    length A M *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
Tactic: by_cases h : IsFiniteLength A M
-- 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
pos :
  ∀ (h : IsFiniteLength A M),
    length B (B ⊗[A] M) =
      length A M *
        length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
⊢ length B (B ⊗[A] M) =
    length A M *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
have neg : ∀ (h : ¬IsFiniteLength A M),
  length B (B ⊗[A] M) =
    length A M *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
Tactic: by_cases h : IsFiniteLength A M
-- 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
⊢ length B (B ⊗[A] M) =
    length A M *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
have pos : ∀ (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 =
      ⊤),
  length B (B ⊗[A] M) =
    length A M *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
Tactic: obtain ⟨s, hs_bot, hs_top⟩ := isFiniteLength_iff_exists_compositionSeries.mp h
-- 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 =
    ⊤
⊢ length B (B ⊗[A] M) =
    length A M *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
have pos : 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 [← length_compositionSeries s hs_bot hs_top]
-- 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 =
    ⊤
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)))
⊢ 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)))
have 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)))
Tactic: rw [← Fin.val_last s.length, ← this, ← RelSeries.last, hs_top, baseChange_top, length_top]