awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : Etale R S
β : S
hadj : Eq (α := Subalgebra R S) R[β] ⊤
h : Monic (minpoly R β)
this : Module.Free R S
hβ₀ :
  Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S))
    (ResidueField R)[((residue S : (a : S) → ResidueField S) β : ResidueField S)] ⊤
refine_2 :
  natDegree (minpoly R β) ≤
    natDegree.{u_1} (R := ResidueField R)
      (minpoly (ResidueField R) (B := ResidueField S) ((residue S : (a : S) → ResidueField S) β : ResidueField S))
⊢ natDegree (R := ResidueField R) (map (residue R) (minpoly R β)) ≤
    natDegree.{u_1} (R := ResidueField R)
      (minpoly (ResidueField R) (B := ResidueField S) ((residue S : (a : S) → ResidueField S) β : ResidueField S))
have refine_2₁ : Module.finrank R S ≤
  natDegree.{u_1} (R := ResidueField R)
    (minpoly (ResidueField R) (B := ResidueField S) ((residue S : (a : S) → ResidueField S) β : ResidueField S))
Tactic: rw [h.natDegree_map _,
      ← (IsAdjoinRootMonic.mkOfAdjoinEqTop' hadj).finrank,
      finrank_eq_finrank_residueField,
      (IsAdjoinRootMonic.mkOfAdjoinEqTop' hβ₀).finrank]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : Etale R S
β : S
hadj : Eq (α := Subalgebra R S) R[β] ⊤
h : Monic (minpoly R β)
this : Module.Free R S
hβ₀ :
  Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S))
    (ResidueField R)[((residue S : (a : S) → ResidueField S) β : ResidueField S)] ⊤
refine_2 :
  natDegree (minpoly R β) ≤
    natDegree.{u_1} (R := ResidueField R)
      (minpoly (ResidueField R) (B := ResidueField S) ((residue S : (a : S) → ResidueField S) β : ResidueField S))
refine_2₁ :
  Module.finrank R S ≤
    natDegree.{u_1} (R := ResidueField R)
      (minpoly (ResidueField R) (B := ResidueField S) ((residue S : (a : S) → ResidueField S) β : ResidueField S))
⊢ natDegree (R := ResidueField R) (map (residue R) (minpoly R β)) ≤
    natDegree.{u_1} (R := ResidueField R)
      (minpoly (ResidueField R) (B := ResidueField S) ((residue S : (a : S) → ResidueField S) β : ResidueField S))
have refine_2₂ : Module.finrank.{u_1, u_2} (ResidueField R) (ResidueField S) ≤
  natDegree.{u_1} (R := ResidueField R)
    (minpoly (ResidueField R) (B := ResidueField S) ((residue S : (a : S) → ResidueField S) β : ResidueField S))
Tactic: rw [h.natDegree_map _,
      ← (IsAdjoinRootMonic.mkOfAdjoinEqTop' hadj).finrank,
      finrank_eq_finrank_residueField,
      (IsAdjoinRootMonic.mkOfAdjoinEqTop' hβ₀).finrank]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : Etale R S
β : S
hadj : Eq (α := Subalgebra R S) R[β] ⊤
h : Monic (minpoly R β)
this : Module.Free R S
hβ₀ :
  Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S))
    (ResidueField R)[((residue S : (a : S) → ResidueField S) β : ResidueField S)] ⊤
refine_2 :
  natDegree (minpoly R β) ≤
    natDegree.{u_1} (R := ResidueField R)
      (minpoly (ResidueField R) (B := ResidueField S) ((residue S : (a : S) → ResidueField S) β : ResidueField S))
refine_2₁ :
  Module.finrank R S ≤
    natDegree.{u_1} (R := ResidueField R)
      (minpoly (ResidueField R) (B := ResidueField S) ((residue S : (a : S) → ResidueField S) β : ResidueField S))
refine_2₂ :
  Module.finrank.{u_1, u_2} (ResidueField R) (ResidueField S) ≤
    natDegree.{u_1} (R := ResidueField R)
      (minpoly (ResidueField R) (B := ResidueField S) ((residue S : (a : S) → ResidueField S) β : ResidueField S))
⊢ natDegree (R := ResidueField R) (map (residue R) (minpoly R β)) ≤
    natDegree.{u_1} (R := ResidueField R)
      (minpoly (ResidueField R) (B := ResidueField S) ((residue S : (a : S) → ResidueField S) β : ResidueField S))
have refine_2₃ : natDegree.{u_1} (R := ResidueField R)
    (minpoly (ResidueField R) (B := ResidueField S) ((residue S : (a : S) → ResidueField S) β : ResidueField S)) ≤
  natDegree.{u_1} (R := ResidueField R)
    (minpoly (ResidueField R) (B := ResidueField S) ((residue S : (a : S) → ResidueField S) β : ResidueField S))
Tactic: rw [h.natDegree_map _,
      ← (IsAdjoinRootMonic.mkOfAdjoinEqTop' hadj).finrank,
      finrank_eq_finrank_residueField,
      (IsAdjoinRootMonic.mkOfAdjoinEqTop' hβ₀).finrank]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : Etale R S
β : S
hadj : Eq (α := Subalgebra R S) R[β] ⊤
⊢ IsUnit.{u_2} (M := S) ((aeval β : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) (minpoly R β) : R[X]) : S)
have a : Ne (α := ResidueField S)
  ((residue S : (a : S) → ResidueField S)
      ((aeval β : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) (minpoly R β) : R[X])) :
    ResidueField S)
  (0 : ResidueField S)
Tactic: apply fun s ↦ (residue_ne_zero_iff_isUnit s).mp
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : Etale R S
β : S
hadj : Eq (α := Subalgebra R S) R[β] ⊤
⊢ Ne (α := ResidueField S)
    ((residue S : (a : S) → ResidueField S)
        ((aeval β : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) (minpoly R β) : R[X])) :
      ResidueField S)
    (0 : ResidueField S)
have a : Ne.{u_2 + 1} (α := ResidueField S)
  (((aeval ((residue S : (a : S) → ResidueField S) β) :
          AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
        (a : (ResidueField R)[X]) → ResidueField S)
      ((derivative : (a : (ResidueField R)[X]) → (ResidueField R)[X])
        (minpoly (ResidueField R) (B := ResidueField S) ((residue S : (a : S) → ResidueField S) β : ResidueField S))) :
    ResidueField S)
  (0 : ResidueField S)
Tactic: rw [map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl,
    ← derivative_map, minpoly_map_residue hadj]
-- 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
p q : Submodule B M
h : p ⋖ q
f : ↥p →ₗ[B] ↥q := inclusion ⋯
⊢ IsSimpleModule.{u_2, u_3} B (↥q ⧸ f.range)
have rwa : IsSimpleModule.{u_2, u_3} B (↥q ⧸ comap q.subtype p)
Tactic: rwa [range_inclusion, ← covBy_iff_quot_is_simple h.le]
-- 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
p q : Submodule B M
h : p ⋖ q
f : ↥p →ₗ[B] ↥q := inclusion ⋯
⊢ length.{u_1, u_3} A ↥q = length.{u_1, u_3} A ↥p + length.{u_1, u_2} (ResidueField A) (ResidueField B)
have key : IsSimpleModule.{u_2, u_3} B (↥q ⧸ f.range)
Tactic: have key : IsSimpleModule B (q ⧸ f.range) := by
    rwa [range_inclusion, ← covBy_iff_quot_is_simple h.le]
-- 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
p q : Submodule B M
h : p ⋖ q
f : ↥p →ₗ[B] ↥q := inclusion ⋯
key : IsSimpleModule.{u_2, u_3} B (↥q ⧸ f.range)
⊢ length.{u_1, u_3} A ↥q = length.{u_1, u_3} A ↥p + length.{u_1, u_2} (ResidueField A) (ResidueField B)
have obtain : ∀ (m : Ideal B) (hm : m.IsMaximal) (e : LinearEquiv.{u_2, u_2, u_3, u_2} (RingHom.id B) (↥q ⧸ f.range) (B ⧸ m)),
  length.{u_1, u_3} A ↥q = length.{u_1, u_3} A ↥p + length.{u_1, u_2} (ResidueField A) (ResidueField B)
Tactic: obtain ⟨m, hm, ⟨e⟩⟩ := isSimpleModule_iff_quot_maximal.mp key
-- 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
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) (B ⧸ m)
⊢ length.{u_1, u_3} A ↥q = length.{u_1, u_3} A ↥p + length.{u_1, u_2} (ResidueField A) (ResidueField B)
have rw : ∀
  (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))),
  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 [eq_maximalIdeal hm] at e
Cleared hypotheses: e
-- 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
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
⊢ length.{u_1, u_3} A ↥q = length.{u_1, u_3} A ↥p + length.{u_1, u_2} (ResidueField A) (ResidueField B)
have this : Function.Injective (α := ↥p) (β := ↥q) (⇑f : (a : ↥p) → ↥q)
Tactic: have : Function.Injective f := inclusion_injective _
-- 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
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 : Function.Injective (α := ↥p) (β := ↥q) (⇑f : (a : ↥p) → ↥q)
⊢ length.{u_1, u_3} A ↥q = length.{u_1, u_3} A ↥p + length.{u_1, u_2} (ResidueField A) (ResidueField B)
have this₁ : Function.Surjective.{u_3 + 1, u_2 + 1} (α := ↥q) (β := ResidueField B) (⇑g : (a : ↥q) → ResidueField B)
Tactic: have : Function.Surjective g := e.surjective.comp f.range.mkQ_surjective
-- 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
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 : Function.Surjective.{u_3 + 1, u_2 + 1} (α := ↥q) (β := ResidueField B) (⇑g : (a : ↥q) → 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)
have 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)
Tactic: have : Function.Exact f g := exact_iff.mpr ((e.ker_comp f.range.mkQ).trans f.range.ker_mkQ)
-- 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
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)
⊢ length.{u_1, u_3} A ↥q = length.{u_1, u_3} A ↥p + length.{u_1, u_2} (ResidueField A) (ResidueField B)
have 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)
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]
-- 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
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)
⊢ length.{u_1, u_3} A ↥q = length.{u_1, u_3} A ↥p + length.{u_1, u_2} (ResidueField A) (ResidueField B)
have 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)
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]
-- 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
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)
⊢ length.{u_1, u_3} A ↥q = length.{u_1, u_3} A ↥p + length.{u_1, u_2} (ResidueField A) (ResidueField B)
have 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)) : ℕ∞)
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]
-- 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
⊢ length A M = length B M * length.{u_1, u_2} (ResidueField A) (ResidueField B)
have pos : ∀ (h : IsFiniteLength B M), length A M = length B M * length.{u_1, u_2} (ResidueField A) (ResidueField B)
Tactic: by_cases h : IsFiniteLength B 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 : 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)
⊢ length A M = length B M * length.{u_1, u_2} (ResidueField A) (ResidueField B)
have neg : ∀ (h : ¬IsFiniteLength B M), length A M = length B M * length.{u_1, u_2} (ResidueField A) (ResidueField B)
Tactic: by_cases h : IsFiniteLength B 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 : 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 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)
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 : 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 = length B M * length.{u_1, u_2} (ResidueField A) (ResidueField B)
have 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)
Tactic: rw [← length_compositionSeries s hs_bot hs_top]