awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalRing.Etale
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
this : Module.Free R S
r : R
x : S
⊢ ((↑(Ideal.quotEquivOfEq ⋯) : S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R) ≃+ S ⧸ maximalIdeal S) :
        (a : S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) → S ⧸ maximalIdeal S)
      (HSMul.hSMul (α := HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R)) (β :=
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
        ((Ideal.Quotient.mk (maximalIdeal R) : (a : R) → R ⧸ maximalIdeal R) r :
          HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) :
              (a : S) → S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))
            x :
          HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))) =
    HSMul.hSMul (α := HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R)) (β :=
      HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))
      ((Ideal.Quotient.mk (maximalIdeal R) : (a : R) → R ⧸ maximalIdeal R) r :
        HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
      (((↑(Ideal.quotEquivOfEq ⋯) : S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R) ≃+ S ⧸ maximalIdeal S) :
            (a : S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) → S ⧸ maximalIdeal S)
          ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) :
              (a : S) → S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))
            x) :
        HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))

Tactic:
rfl
-- Module: Mathlib.RingTheory.LocalRing.Etale
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[β] ⊤
⊢ Monic (minpoly R β)

Tactic:
have h := minpoly.monic <| Algebra.IsIntegral.isIntegral (R:=R) β
-- Module: Mathlib.RingTheory.LocalRing.Etale
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 β)
⊢ Eq (α := (ResidueField R)[X]) (map (residue R) (minpoly R β))
    (minpoly (ResidueField R) (B := ResidueField S) ((residue S : (a : S) → ResidueField S) β : ResidueField S))

Tactic:
eq_of_monic_of_dvd_of_natDegree_le
    (minpoly.monic <| Algebra.IsIntegral.isIntegral <| residue S β)
    (h.map _) (minpoly.dvd (ResidueField R) (residue S β) ?_) ?_

Premises used: Algebra.IsIntegral.isIntegral, minpoly.monic, IsLocalRing.residue, Polynomial.eq_of_monic_of_dvd_of_natDegree_le, IsLocalRing.ResidueField, minpoly.dvd, Polynomial.Monic.map, DFunLike.coe
-- Module: Mathlib.RingTheory.LocalRing.Etale
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 β)
refine_1 :
  Eq.{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)
        (map (residue R) (minpoly R β)) :
      ResidueField S)
    (0 : ResidueField S)
refine_2 :
  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))
⊢ Eq (α := (ResidueField R)[X]) (map (residue R) (minpoly R β))
    (minpoly (ResidueField R) (B := ResidueField S) ((residue S : (a : S) → ResidueField S) β : ResidueField S))

Tactic:
refine eq_of_monic_of_dvd_of_natDegree_le
    (minpoly.monic <| Algebra.IsIntegral.isIntegral <| residue S β)
    (h.map _) (minpoly.dvd (ResidueField R) (residue S β) ?_) ?_

Premises used: Algebra.IsIntegral.isIntegral, minpoly.monic, IsLocalRing.residue, Polynomial.eq_of_monic_of_dvd_of_natDegree_le, IsLocalRing.ResidueField, minpoly.dvd, Polynomial.Monic.map, DFunLike.coe
-- Module: Mathlib.RingTheory.LocalRing.Etale
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 β)
refine_1 :
  Eq (α := ResidueField S)
    ((residue S : (a : S) → ResidueField S) ((aeval β : (a : R[X]) → S) (minpoly R β)) : ResidueField S)
    (0 : ResidueField S)
⊢ Eq.{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)
        (map (residue R) (minpoly R β)) :
      ResidueField S)
    (0 : ResidueField S)

Tactic:
rw [← map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl]

Premises used: Polynomial.map_aeval_eq_aeval_map, rfl
-- Module: Mathlib.RingTheory.LocalRing.Etale
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 β)
⊢ Eq (α := ResidueField S)
    ((residue S : (a : S) → ResidueField S) ((aeval β : (a : R[X]) → S) (minpoly R β)) : ResidueField S)
    (0 : ResidueField S)

Tactic:
simp
-- Module: Mathlib.RingTheory.LocalRing.Etale
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 β)
⊢ Module.Free R S

Tactic:
have : Module.Free R S := Module.free_of_flat_of_isLocalRing
-- Module: Mathlib.RingTheory.LocalRing.Etale
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
⊢ Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S))
    (ResidueField R)[((residue S : (a : S) → ResidueField S) β : ResidueField S)] ⊤

Tactic:
have hβ₀ := (adjoin_residue_eq_top_iff_adjoin_eq_top β).mpr hadj
-- Module: Mathlib.RingTheory.LocalRing.Etale
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))
refine_2₃ 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))
⊢ 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))

Tactic:
rw [h.natDegree_map _,
      ← (IsAdjoinRootMonic.mkOfAdjoinEqTop' hadj).finrank,
      finrank_eq_finrank_residueField,
      (IsAdjoinRootMonic.mkOfAdjoinEqTop' hβ₀).finrank]

Premises used: IsAdjoinRootMonic.finrank, Polynomial.Monic.natDegree_map, IsLocalRing.finrank_eq_finrank_residueField, IsAdjoinRootMonic.mkOfAdjoinEqTop'
-- Module: Mathlib.RingTheory.LocalRing.Etale
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[β] ⊤
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)
⊢ IsUnit.{u_2} (M := S) ((aeval β : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) (minpoly R β) : R[X]) : S)

Tactic:
apply fun s ↦ (residue_ne_zero_iff_isUnit s).mp

Premises used: IsLocalRing.residue_ne_zero_iff_isUnit, Iff.mp
-- Module: Mathlib.RingTheory.LocalRing.Etale
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[β] ⊤
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)
⊢ 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:
rw [map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl,
    ← derivative_map, minpoly_map_residue hadj]

Premises used: IsLocalRing.minpoly_map_residue, Polynomial.derivative_map, Polynomial.map_aeval_eq_aeval_map, rfl
-- Module: Mathlib.RingTheory.LocalRing.Etale
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.{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:
(Algebra.IsSeparable.isSeparable _ _).aeval_derivative_ne_zero (minpoly.aeval _ _)

Premises used: Algebra.IsSeparable.isSeparable, minpoly.aeval, Polynomial.Separable.aeval_derivative_ne_zero
-- Module: Mathlib.RingTheory.LocalRing.Etale
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.{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:
exact (Algebra.IsSeparable.isSeparable _ _).aeval_derivative_ne_zero (minpoly.aeval _ _)

Premises used: Algebra.IsSeparable.isSeparable, Polynomial.Separable.aeval_derivative_ne_zero
-- 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 ⋯
rwa : IsSimpleModule.{u_2, u_3} B (↥q ⧸ comap q.subtype p)
rwa₁ rwa₂ rwa₃ rwa₄ : p ⋖ q
⊢ IsSimpleModule.{u_2, u_3} B (↥q ⧸ f.range)

Tactic:
rwa [range_inclusion, ← covBy_iff_quot_is_simple h.le]

Premises used: covBy_iff_quot_is_simple, Submodule.range_inclusion, CovBy.le
-- 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 ⋯
⊢ 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]
-- 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)
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)
⊢ 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

Premises used: isSimpleModule_iff_quot_maximal, 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
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)
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)
⊢ 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

Premises used: IsLocalRing.eq_maximalIdeal
-- 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
⊢ Function.Injective (α := ↥p) (β := ↥q) (⇑f : (a : ↥p) → ↥q)

Tactic:
have : Function.Injective f := inclusion_injective _
-- 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 : Function.Injective (α := ↥p) (β := ↥q) (⇑f : (a : ↥p) → ↥q)
⊢ 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
-- 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 : Function.Surjective.{u_3 + 1, u_2 + 1} (α := ↥q) (β := ResidueField B) (⇑g : (a : ↥q) → ResidueField B)
⊢ 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)
-- 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.Injective (α := ↥p) (β := ↥q)
    (⇑((↑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)

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)
⊢ Function.Surjective.{u_3 + 1, u_2 + 1} (α := ↥q) (β := ResidueField B)
    (⇑((↑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