awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
p q : Submodule B M
h : p ⋖ q
f : ↥p →ₗ[B] ↥q := inclusion ⋯
key : IsSimpleModule.{u_2, u_3} B (↥q ⧸ f.range)
m : Ideal B
hm : m.IsMaximal
e :
  LinearEquiv.{u_2, u_2, u_3, u_2} (RingHom.id B) (↥q ⧸ f.range)
    (HasQuotient.Quotient B (B := Ideal B) (maximalIdeal B : Ideal B))
g : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id B) (↥q) (ResidueField B) :=
  (↑e : ↥q ⧸ f.range →ₗ[B] B ⧸ maximalIdeal B) ∘ₗ f.range.mkQ
this_1 : Function.Injective (α := ↥p) (β := ↥q) (⇑f : (a : ↥p) → ↥q)
this_2 : Function.Surjective.{u_3 + 1, u_2 + 1} (α := ↥q) (β := ResidueField B) (⇑g : (a : ↥q) → ResidueField B)
this :
  Function.Exact.{u_3, u_3, u_2} (M := ↥p) (N := ↥q) (P := ResidueField B) (⇑f : (a : ↥p) → ↥q)
    (⇑g : (a : ↥q) → ResidueField B)
⊢ Function.Exact.{u_3, u_3, u_2} (M := ↥p) (N := ↥q) (P := ResidueField B)
    (⇑((↑A :
            {S : Type u_2} →
              {M M₂ : Type u_3} →
                [inst : Semiring A] →
                  [inst_10 : Semiring S] →
                    [inst_11 : AddCommMonoid M] →
                      [inst_12 : AddCommMonoid M₂] →
                        [inst_13 : Module A M] →
                          [inst_14 : Module A M₂] →
                            [inst_15 : Module S M] →
                              [inst_16 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
          f) :
      (a : ↥p) → ↥q)
    (⇑((↑A :
            {S : Type u_2} →
              {M : Type u_3} →
                {M₂ : Type u_2} →
                  [inst : Semiring A] →
                    [inst_10 : Semiring S] →
                      [inst_11 : AddCommMonoid M] →
                        [inst_12 : AddCommMonoid M₂] →
                          [inst_13 : Module A M] →
                            [inst_14 : Module A M₂] →
                              [inst_15 : Module S M] →
                                [inst_16 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
          g) :
      (a : ↥q) → ResidueField B)

Tactic:
simpa
-- 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
p q : Submodule B M
h : p ⋖ q
f : ↥p →ₗ[B] ↥q := inclusion ⋯
key : IsSimpleModule.{u_2, u_3} B (↥q ⧸ f.range)
m : Ideal B
hm : m.IsMaximal
e :
  LinearEquiv.{u_2, u_2, u_3, u_2} (RingHom.id B) (↥q ⧸ f.range)
    (HasQuotient.Quotient B (B := Ideal B) (maximalIdeal B : Ideal B))
g : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id B) (↥q) (ResidueField B) :=
  (↑e : ↥q ⧸ f.range →ₗ[B] B ⧸ maximalIdeal B) ∘ₗ f.range.mkQ
this_1 : Function.Injective (α := ↥p) (β := ↥q) (⇑f : (a : ↥p) → ↥q)
this_2 : Function.Surjective.{u_3 + 1, u_2 + 1} (α := ↥q) (β := ResidueField B) (⇑g : (a : ↥q) → ResidueField B)
this :
  Function.Exact.{u_3, u_3, u_2} (M := ↥p) (N := ↥q) (P := ResidueField B) (⇑f : (a : ↥p) → ↥q)
    (⇑g : (a : ↥q) → ResidueField B)
rw :
  length.{u_1, u_3} A ↥p + length.{u_1, u_2} A (ResidueField B) =
    length.{u_1, u_3} A ↥p + length.{u_1, u_2} (ResidueField A) (ResidueField B)
rw₁ :
  length.{u_1, u_3} A ↥p + length.{u_1, u_2} (ResidueField A) (ResidueField B) =
    length.{u_1, u_3} A ↥p + length.{u_1, u_2} (ResidueField A) (ResidueField B)
rw₂ rw₃ :
  HAdd.hAdd (β := ℕ∞) (length.{u_1, u_3} A ↥p)
      ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank.{u_1, u_2} (ResidueField A) (ResidueField B)) : ℕ∞) =
    HAdd.hAdd (β := ℕ∞) (length.{u_1, u_3} A ↥p)
      ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank.{u_1, u_2} (ResidueField A) (ResidueField B)) : ℕ∞)
⊢ length.{u_1, u_3} A ↥q = length.{u_1, u_3} A ↥p + length.{u_1, u_2} (ResidueField A) (ResidueField B)

Tactic:
rw [length_eq_add_of_exact (f.restrictScalars A) (g.restrictScalars A)
    (by simpa) (by simpa) (by simpa), Module.length_eq_of_surjective (M := ResidueField B)
      (residue_surjective (R := A)), Module.length_eq_rank]

Premises used: Module.length_eq_of_surjective, LinearMap.restrictScalars, Module.length_eq_add_of_exact, Module.length_eq_rank, IsLocalRing.residue_surjective
-- 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
pos : ∀ (h : IsFiniteLength B M), length A M = length B M * length.{u_1, u_2} (ResidueField A) (ResidueField B)
neg : ∀ (h : ¬IsFiniteLength B M), length A M = length B 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)

Tactic:
by_cases h : IsFiniteLength B M

Premises used: IsFiniteLength
-- 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
pos :
  ∀ (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 = length B 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)

Tactic:
obtain ⟨s, hs_bot, hs_top⟩ := isFiniteLength_iff_exists_compositionSeries.mp h

Premises used: isFiniteLength_iff_exists_compositionSeries, Iff.mp
-- 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 =
    ⊤
pos :
  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)
⊢ length A M = length B M * length.{u_1, u_2} (ResidueField A) (ResidueField B)

Tactic:
rw [← length_compositionSeries s hs_bot hs_top]

Premises used: Module.length_compositionSeries
-- 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 =
    ⊤
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)
rw : length A M = length.{u_1, u_3} A ↥⊤
⊢ 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)

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

Premises used: RelSeries.last, RelSeries.length, Fin.val_last
-- 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 =
    ⊤
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 = length.{u_1, u_3} A ↥⊤

Tactic:
length_top.symm

Premises used: Set.Mem, Module.length_top, Eq.symm
-- 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 =
    ⊤
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 = length.{u_1, u_3} A ↥⊤

Tactic:
exact length_top.symm

Premises used: Module.length_top, Eq.symm
-- 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 =
    ⊤
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)
⊢ 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)

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
-- 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 =
    ⊤
pos : length.{u_1, u_3} A ↥⊥ = (↑(↑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})
          0) =
    (↑(↑0 : ℕ) : ℕ∞) * length.{u_1, u_2} (ResidueField A) (ResidueField B)

Tactic:
rw [← RelSeries.head, hs_bot]

Premises used: RelSeries.head
-- 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 =
    ⊤
⊢ length.{u_1, u_3} A ↥⊥ = (↑(↑0 : ℕ) : ℕ∞) * length.{u_1, u_2} (ResidueField A) (ResidueField B)

Tactic:
simp
-- 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 =
    ⊤
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:
simpa [hi, add_one_mul] using (s.step i).length_restrictScalars A

Premises used: add_one_mul, RelSeries.step, CovBy.length_restrictScalars
-- 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
contrapose! : ∀ (h : IsFiniteLength A M), IsFiniteLength B M
⊢ ¬IsFiniteLength A M

Tactic:
contrapose! h
-- 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 A M
rw : ∀ (h : IsNoetherian A M ∧ IsArtinian A M), IsNoetherian B M ∧ IsArtinian B M
⊢ IsFiniteLength B M

Tactic:
rw [isFiniteLength_iff_isNoetherian_isArtinian] at h ⊢

Premises used: isFiniteLength_iff_isNoetherian_isArtinian
-- 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 : IsNoetherian A M ∧ IsArtinian A M
⊢ IsNoetherian B M ∧ IsArtinian B M

Tactic:
h.imp (isNoetherian_of_tower A) (isArtinian_of_tower A)

Premises used: And.imp, isArtinian_of_tower, isNoetherian_of_tower
-- 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 : IsNoetherian A M ∧ IsArtinian A M
⊢ IsNoetherian B M ∧ IsArtinian B M

Tactic:
exact h.imp (isNoetherian_of_tower A) (isArtinian_of_tower A)

Premises used: And.imp, isArtinian_of_tower, isNoetherian_of_tower
-- 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
⊢ ¬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)
-- 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
this : ¬IsFiniteLength A M
⊢ length B M = ⊤

Tactic:
rw [← length_ne_top_iff, not_ne_iff] at h this

Premises used: not_ne_iff, Module.length_ne_top_iff