awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FormallyUnramified R S
inst_8 : EssFiniteType R S
x : M
r s : S
⊢ (_root_.TensorProduct.lift
          ((↑R :
              {S M : Type u_2} →
                {M₂ : Type u_3} →
                  [inst : Semiring R] →
                    [inst_9 : Semiring S] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module R M] →
                            [inst_13 : Module R M₂] →
                              [inst_14 : Module S M] →
                                [inst_15 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (LinearMap.flip
                ((↑R :
                    {S : Type u_2} →
                      {M : Type u_3} →
                        {M₂ : Type (max u_3 u_2)} →
                          [inst : Semiring R] →
                            [inst_9 : Semiring S] →
                              [inst_10 : AddCommMonoid M] →
                                [inst_11 : AddCommMonoid M₂] →
                                  [inst_12 : Module R M] →
                                    [inst_13 : Module R M₂] →
                                      [inst_14 : Module S M] →
                                        [inst_15 : Module S M₂] →
                                          [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                  (LinearMap.flip
                      (AlgHom.toLinearMap (lsmul S S M) : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) S (End S M)) :
                    M →ₗ[S] S →ₗ[S] M)) :
              LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) S (M →ₗ[R] M))) :
        (a : S ⊗[R] M) → M)
      (((TensorProduct.AlgebraTensorModule.map LinearMap.id
                (((LinearMap.flip
                        (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                      M →ₗ[R] S →ₗ[R] M) :
                    (a : M) → S →ₗ[R] M)
                  x) :
              S ⊗[R] S →ₗ[S] S ⊗[R] M) :
            (a : S ⊗[R] S) → S ⊗[R] M)
          (r ⊗ₜ[R] s) :
        S ⊗[R] M) =
    HSMul.hSMul (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (r ⊗ₜ[R] s) : S) x

Tactic:
simp [mul_smul, smul_comm r s]

Premises used: SMulCommClass.smul_comm, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FormallyUnramified R S
inst_8 : EssFiniteType R S
x : M
rw : HSMul.hSMul.{u_2, u_3, u_3} (α := S) 1 x = x
rw₁ rw₂ : x = x
⊢ HSMul.hSMul (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (elem R S) : S) x = x

Tactic:
rw [lmul_elem, one_smul]

Premises used: Algebra.FormallyUnramified.lmul_elem, one_smul
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FormallyUnramified R S
inst_8 : EssFiniteType R S
inst_9 : Flat R M
⊢ Flat S M

Tactic:
Module.Flat.of_retract _ _ (comp_sec R S M)

Premises used: Module.Flat.of_retract, Algebra.FormallyUnramified.comp_sec
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FormallyUnramified R S
inst_8 : EssFiniteType R S
inst_9 : Projective R M
⊢ Projective S M

Tactic:
Module.Projective.of_split _ _ (comp_sec R S M)

Premises used: Module.Projective.of_split, Algebra.FormallyUnramified.comp_sec
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
⊢ FormallyUnramified S (ResidueField S)

Tactic:
.quotient _

Premises used: IsLocalRing.ResidueField, Algebra.FormallyUnramified.quotient
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : FormallyUnramified R S
⊢ FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)

Tactic:
have : FormallyUnramified R (ResidueField S) := .comp _ S _
  .of_restrictScalars R _ _

Premises used: Algebra.FormallyUnramified.comp, IsLocalRing.ResidueField, Algebra.FormallyUnramified.of_restrictScalars
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : FormallyUnramified R S
⊢ Module.Finite.{u_1, u_2} (ResidueField R) (ResidueField S)

Tactic:
have : EssFiniteType R (ResidueField S) := .comp _ S _
  have : EssFiniteType (ResidueField R) (ResidueField S) := .of_comp R _ _
  FormallyUnramified.finite_of_free _ _

Premises used: Algebra.EssFiniteType.of_comp, Algebra.EssFiniteType.comp, IsLocalRing.ResidueField, Algebra.FormallyUnramified.finite_of_free
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : FormallyUnramified R S
⊢ Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)

Tactic:
FormallyUnramified.isSeparable _ _

Premises used: Algebra.FormallyUnramified.isSeparable
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : FormallyUnramified R S
mR : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)
⊢ mR ≤ maximalIdeal S

Tactic:
have hmR : mR ≤ maximalIdeal S := ((local_hom_TFAE (algebraMap R S)).out 0 2 rfl rfl).mp ‹_›
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : FormallyUnramified R S
mR : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this : Algebra.{u_1, u_2} (ResidueField R) (S ⧸ mR) :=
  { smul := Quotient.lift₂ (fun (x1 : R) (x2 : S) ↦ ⟦x1 • x2⟧) ⋯,
    algebraMap := Ideal.quotientMap (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (algebraMap R S) ⋯,
    commutes' := ⋯, smul_def' := ⋯ }
⊢ IsScalarTower.{u_1, u_1, u_2} R (ResidueField R) (S ⧸ mR)

Tactic:
have : IsScalarTower R (ResidueField R) (S ⧸ mR) := inferInstanceAs (IsScalarTower R (R ⧸ _) _)
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : FormallyUnramified R S
mR : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this_1 : Algebra.{u_1, u_2} (ResidueField R) (S ⧸ mR) :=
  { smul := Quotient.lift₂ (fun (x1 : R) (x2 : S) ↦ ⟦x1 • x2⟧) ⋯,
    algebraMap := Ideal.quotientMap (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (algebraMap R S) ⋯,
    commutes' := ⋯, smul_def' := ⋯ }
this : IsScalarTower.{u_1, u_1, u_2} R (ResidueField R) (S ⧸ mR)
⊢ FormallyUnramified.{u_2, u_1} (ResidueField R) (S ⧸ mR)

Tactic:
have : FormallyUnramified (ResidueField R) (S ⧸ mR) := .of_restrictScalars R _ _
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : FormallyUnramified R S
mR : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this_1 : Algebra.{u_1, u_2} (ResidueField R) (S ⧸ mR) :=
  { smul := Quotient.lift₂ (fun (x1 : R) (x2 : S) ↦ ⟦x1 • x2⟧) ⋯,
    algebraMap := Ideal.quotientMap (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (algebraMap R S) ⋯,
    commutes' := ⋯, smul_def' := ⋯ }
this_2 : IsScalarTower.{u_1, u_1, u_2} R (ResidueField R) (S ⧸ mR)
this : FormallyUnramified.{u_2, u_1} (ResidueField R) (S ⧸ mR)
⊢ EssFiniteType.{u_1, u_2} (ResidueField R) (S ⧸ mR)

Tactic:
have : EssFiniteType (ResidueField R) (S ⧸ mR) := .of_comp R _ _
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : FormallyUnramified R S
mR : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this_1 : Algebra.{u_1, u_2} (ResidueField R) (S ⧸ mR) :=
  { smul := Quotient.lift₂ (fun (x1 : R) (x2 : S) ↦ ⟦x1 • x2⟧) ⋯,
    algebraMap := Ideal.quotientMap (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (algebraMap R S) ⋯,
    commutes' := ⋯, smul_def' := ⋯ }
this_2 : IsScalarTower.{u_1, u_1, u_2} R (ResidueField R) (S ⧸ mR)
this_3 : FormallyUnramified.{u_2, u_1} (ResidueField R) (S ⧸ mR)
this : EssFiniteType.{u_1, u_2} (ResidueField R) (S ⧸ mR)
⊢ Module.Finite.{u_1, u_2} (ResidueField R) (S ⧸ mR)

Tactic:
have : Module.Finite (ResidueField R) (S ⧸ mR) := FormallyUnramified.finite_of_free _ _
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : FormallyUnramified R S
mR : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this_1 : Algebra.{u_1, u_2} (ResidueField R) (S ⧸ mR) :=
  { smul := Quotient.lift₂ (fun (x1 : R) (x2 : S) ↦ ⟦x1 • x2⟧) ⋯,
    algebraMap := Ideal.quotientMap (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (algebraMap R S) ⋯,
    commutes' := ⋯, smul_def' := ⋯ }
this_2 : IsScalarTower.{u_1, u_1, u_2} R (ResidueField R) (S ⧸ mR)
this_3 : FormallyUnramified.{u_2, u_1} (ResidueField R) (S ⧸ mR)
this_4 : EssFiniteType.{u_1, u_2} (ResidueField R) (S ⧸ mR)
this : Module.Finite.{u_1, u_2} (ResidueField R) (S ⧸ mR)
⊢ IsReduced.{u_2} (S ⧸ mR)

Tactic:
have : IsReduced (S ⧸ mR) := FormallyUnramified.isReduced_of_field (ResidueField R) (S ⧸ mR)
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : FormallyUnramified R S
mR : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this_1 : Algebra.{u_1, u_2} (ResidueField R) (S ⧸ mR) :=
  { smul := Quotient.lift₂ (fun (x1 : R) (x2 : S) ↦ ⟦x1 • x2⟧) ⋯,
    algebraMap := Ideal.quotientMap (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (algebraMap R S) ⋯,
    commutes' := ⋯, smul_def' := ⋯ }
this_2 : IsScalarTower.{u_1, u_1, u_2} R (ResidueField R) (S ⧸ mR)
this_3 : FormallyUnramified.{u_2, u_1} (ResidueField R) (S ⧸ mR)
this_4 : EssFiniteType.{u_1, u_2} (ResidueField R) (S ⧸ mR)
this_5 : Module.Finite.{u_1, u_2} (ResidueField R) (S ⧸ mR)
this : IsReduced.{u_2} (S ⧸ mR)
⊢ IsArtinianRing.{u_2} (S ⧸ mR)

Tactic:
have : IsArtinianRing (S ⧸ mR) := isArtinian_of_tower (ResidueField R) inferInstance
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : FormallyUnramified R S
mR : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this_1 : Algebra.{u_1, u_2} (ResidueField R) (S ⧸ mR) :=
  { smul := Quotient.lift₂ (fun (x1 : R) (x2 : S) ↦ ⟦x1 • x2⟧) ⋯,
    algebraMap := Ideal.quotientMap (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (algebraMap R S) ⋯,
    commutes' := ⋯, smul_def' := ⋯ }
this_2 : IsScalarTower.{u_1, u_1, u_2} R (ResidueField R) (S ⧸ mR)
this_3 : FormallyUnramified.{u_2, u_1} (ResidueField R) (S ⧸ mR)
this_4 : EssFiniteType.{u_1, u_2} (ResidueField R) (S ⧸ mR)
this_5 : Module.Finite.{u_1, u_2} (ResidueField R) (S ⧸ mR)
this_6 : IsReduced.{u_2} (S ⧸ mR)
this : IsArtinianRing.{u_2} (S ⧸ mR)
⊢ Nontrivial.{u_2} (S ⧸ mR)

Tactic:
have : Nontrivial (S ⧸ mR) :=
    Ideal.Quotient.nontrivial_iff.mpr <| ne_top_of_le_ne_top (maximalIdeal.isMaximal S).ne_top hmR
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : FormallyUnramified R S
mR : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this_1 : Algebra.{u_1, u_2} (ResidueField R) (S ⧸ mR) :=
  { smul := Quotient.lift₂ (fun (x1 : R) (x2 : S) ↦ ⟦x1 • x2⟧) ⋯,
    algebraMap := Ideal.quotientMap (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (algebraMap R S) ⋯,
    commutes' := ⋯, smul_def' := ⋯ }
this_2 : IsScalarTower.{u_1, u_1, u_2} R (ResidueField R) (S ⧸ mR)
this_3 : FormallyUnramified.{u_2, u_1} (ResidueField R) (S ⧸ mR)
this_4 : EssFiniteType.{u_1, u_2} (ResidueField R) (S ⧸ mR)
this_5 : Module.Finite.{u_1, u_2} (ResidueField R) (S ⧸ mR)
this_6 : IsReduced.{u_2} (S ⧸ mR)
this_7 : IsArtinianRing.{u_2} (S ⧸ mR)
this : Nontrivial.{u_2} (S ⧸ mR)
⊢ IsLocalRing.{u_2} (S ⧸ mR)

Tactic:
have : IsLocalRing (S ⧸ mR) := .of_surjective' _ Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : FormallyUnramified R S
mR : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this_1 : Algebra.{u_1, u_2} (ResidueField R) (S ⧸ mR) :=
  { smul := Quotient.lift₂ (fun (x1 : R) (x2 : S) ↦ ⟦x1 • x2⟧) ⋯,
    algebraMap := Ideal.quotientMap (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (algebraMap R S) ⋯,
    commutes' := ⋯, smul_def' := ⋯ }
this_2 : IsScalarTower.{u_1, u_1, u_2} R (ResidueField R) (S ⧸ mR)
this_3 : FormallyUnramified.{u_2, u_1} (ResidueField R) (S ⧸ mR)
this_4 : EssFiniteType.{u_1, u_2} (ResidueField R) (S ⧸ mR)
this_5 : Module.Finite.{u_1, u_2} (ResidueField R) (S ⧸ mR)
this_6 : IsReduced.{u_2} (S ⧸ mR)
this_7 : IsArtinianRing.{u_2} (S ⧸ mR)
this_8 : Nontrivial.{u_2} (S ⧸ mR)
this : IsLocalRing.{u_2} (S ⧸ mR)
rw : Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) (Ideal.jacobson ⊥) ⊥
rw₁ : Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) (Ideal.radical ⊥) ⊥
rw₂ : Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) (Ideal.radical 0) 0
rw₃ : Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) (nilradical (S ⧸ mR)) 0
rw₄ rw₅ : Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) 0 0
⊢ Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) (maximalIdeal (S ⧸ mR)) ⊥

Tactic:
rw [← jacobson_eq_maximalIdeal _ bot_ne_top, IsArtinianRing.jacobson_eq_radical,
      ← Ideal.zero_eq_bot, ← nilradical, nilradical_eq_zero]

Premises used: nilradical_eq_zero, Ideal.zero_eq_bot, bot_ne_top, IsLocalRing.jacobson_eq_maximalIdeal, nilradical, IsArtinianRing.jacobson_eq_radical
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : FormallyUnramified R S
mR : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this_1 : Algebra.{u_1, u_2} (ResidueField R) (S ⧸ mR) :=
  { smul := Quotient.lift₂ (fun (x1 : R) (x2 : S) ↦ ⟦x1 • x2⟧) ⋯,
    algebraMap := Ideal.quotientMap (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (algebraMap R S) ⋯,
    commutes' := ⋯, smul_def' := ⋯ }
this_2 : IsScalarTower.{u_1, u_1, u_2} R (ResidueField R) (S ⧸ mR)
this_3 : FormallyUnramified.{u_2, u_1} (ResidueField R) (S ⧸ mR)
this_4 : EssFiniteType.{u_1, u_2} (ResidueField R) (S ⧸ mR)
this_5 : Module.Finite.{u_1, u_2} (ResidueField R) (S ⧸ mR)
this_6 : IsReduced.{u_2} (S ⧸ mR)
this_7 : IsArtinianRing.{u_2} (S ⧸ mR)
this_8 : Nontrivial.{u_2} (S ⧸ mR)
this : IsLocalRing.{u_2} (S ⧸ mR)
⊢ Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) (maximalIdeal (S ⧸ mR)) ⊥

Tactic:
have : maximalIdeal (S ⧸ mR) = ⊥ := by
    rw [← jacobson_eq_maximalIdeal _ bot_ne_top, IsArtinianRing.jacobson_eq_radical,
      ← Ideal.zero_eq_bot, ← nilradical, nilradical_eq_zero]
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : FormallyUnramified R S
mR : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this_1 : Algebra.{u_1, u_2} (ResidueField R) (S ⧸ mR) :=
  { smul := Quotient.lift₂ (fun (x1 : R) (x2 : S) ↦ ⟦x1 • x2⟧) ⋯,
    algebraMap := Ideal.quotientMap (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (algebraMap R S) ⋯,
    commutes' := ⋯, smul_def' := ⋯ }
this_2 : IsScalarTower.{u_1, u_1, u_2} R (ResidueField R) (S ⧸ mR)
this_3 : FormallyUnramified.{u_2, u_1} (ResidueField R) (S ⧸ mR)
this_4 : EssFiniteType.{u_1, u_2} (ResidueField R) (S ⧸ mR)
this_5 : Module.Finite.{u_1, u_2} (ResidueField R) (S ⧸ mR)
this_6 : IsReduced.{u_2} (S ⧸ mR)
this_7 : IsArtinianRing.{u_2} (S ⧸ mR)
this_8 : Nontrivial.{u_2} (S ⧸ mR)
this_9 : IsLocalRing.{u_2} (S ⧸ mR)
this : Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) (maximalIdeal (S ⧸ mR)) ⊥
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : IsField.{u_2} (S ⧸ mR)),
    IsField.{u_2} (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
⊢ IsField.{u_2} (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))

Tactic:
rwa [← isField_iff_maximalIdeal_eq] at this

Premises used: IsLocalRing.isField_iff_maximalIdeal_eq
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : FormallyUnramified R S
hI : Ideal.IsMaximal.{u_2} (α := S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R))
⊢ Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)

Tactic:
apply eq_maximalIdeal

Premises used: IsLocalRing.eq_maximalIdeal
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : FormallyUnramified R S
hI : IsField.{u_2} (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
⊢ Ideal.IsMaximal.{u_2} (α := S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R))

Tactic:
rw [Ideal.Quotient.maximal_ideal_iff_isField_quotient]

Premises used: Ideal.Quotient.maximal_ideal_iff_isField_quotient
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : FormallyUnramified R S
⊢ IsField.{u_2} (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))

Tactic:
isField_quotient_map_maximalIdeal

Premises used: Algebra.FormallyUnramified.isField_quotient_map_maximalIdeal
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : FormallyUnramified R S
⊢ IsField.{u_2} (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))

Tactic:
exact isField_quotient_map_maximalIdeal

Premises used: Algebra.FormallyUnramified.isField_quotient_map_maximalIdeal
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
subsingleton_kaehlerDifferential : Subsingleton.{u_2 + 1} Ω[S⁄R]
⊢ FormallyUnramified R S

Tactic:
constructor
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
⊢ FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)

Tactic:
have : FormallyUnramified (ResidueField R) (ResidueField S) := .of_isSeparable _ _
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
this : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
⊢ FormallyUnramified.{u_2, u_1} R (ResidueField S)

Tactic:
have : FormallyUnramified R (ResidueField S) := .comp _ (ResidueField R) _