awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (hypothesis)
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
r : S
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)
              m) :
          S ⊗[R] S →ₗ[S] S ⊗[R] M) :
        (a : S ⊗[R] S) → S ⊗[R] M)
      (HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] r) (elem R S)) =
    HSMul.hSMul (β := S ⊗[R] M) r
      (((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)
                  m) :
              S ⊗[R] S →ₗ[S] S ⊗[R] M) :
            (a : S ⊗[R] S) → S ⊗[R] M)
          (elem R S) :
        S ⊗[R] M)
have this : HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] r) (r ⊗ₜ[R] 1) * elem R S = 0
Tactic: have := one_tmul_sub_tmul_one_mul_elem (R := R) r
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (hypothesis)
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
r : S
m : M
this : HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] r) (r ⊗ₜ[R] 1) * elem R S = 0
⊢ ((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)
              m) :
          S ⊗[R] S →ₗ[S] S ⊗[R] M) :
        (a : S ⊗[R] S) → S ⊗[R] M)
      (HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] r) (elem R S)) =
    HSMul.hSMul (β := S ⊗[R] M) r
      (((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)
                  m) :
              S ⊗[R] S →ₗ[S] S ⊗[R] M) :
            (a : S ⊗[R] S) → S ⊗[R] M)
          (elem R S) :
        S ⊗[R] M)
have this₁ : HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] r) (elem R S) = HMul.hMul (α := S ⊗[R] S) (r ⊗ₜ[R] 1) (elem R S)
Tactic: rw [sub_mul, sub_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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
r : S
m : M
this : HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] r) (elem R S) = HMul.hMul (α := S ⊗[R] S) (r ⊗ₜ[R] 1) (elem R S)
⊢ ((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)
              m) :
          S ⊗[R] S →ₗ[S] S ⊗[R] M) :
        (a : S ⊗[R] S) → S ⊗[R] M)
      (HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] r) (elem R S)) =
    HSMul.hSMul (β := S ⊗[R] M) r
      (((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)
                  m) :
              S ⊗[R] S →ₗ[S] S ⊗[R] M) :
            (a : S ⊗[R] S) → S ⊗[R] M)
          (elem R S) :
        S ⊗[R] M)
have rw : ((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)
            m) :
        S ⊗[R] S →ₗ[S] S ⊗[R] M) :
      (a : S ⊗[R] S) → S ⊗[R] M)
    (HMul.hMul (α := S ⊗[R] S) (r ⊗ₜ[R] 1) (elem R S)) =
  HSMul.hSMul (β := S ⊗[R] M) r
    (((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)
                m) :
            S ⊗[R] S →ₗ[S] S ⊗[R] M) :
          (a : S ⊗[R] S) → S ⊗[R] M)
        (elem R S) :
      S ⊗[R] M)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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
r : S
m : M
this : HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] r) (elem R S) = HMul.hMul (α := S ⊗[R] S) (r ⊗ₜ[R] 1) (elem R S)
⊢ ((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)
              m) :
          S ⊗[R] S →ₗ[S] S ⊗[R] M) :
        (a : S ⊗[R] S) → S ⊗[R] M)
      (HMul.hMul (α := S ⊗[R] S) (r ⊗ₜ[R] 1) (elem R S)) =
    HSMul.hSMul (β := S ⊗[R] M) r
      (((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)
                  m) :
              S ⊗[R] S →ₗ[S] S ⊗[R] M) :
            (a : S ⊗[R] S) → S ⊗[R] M)
          (elem R S) :
        S ⊗[R] M)
have zero : ((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)
            m) :
        S ⊗[R] S →ₗ[S] S ⊗[R] M) :
      (a : S ⊗[R] S) → S ⊗[R] M)
    (HMul.hMul (α := S ⊗[R] S) (r ⊗ₜ[R] 1) 0) =
  HSMul.hSMul (β := S ⊗[R] M) r
    (((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)
              m) :
          S ⊗[R] S →ₗ[S] S ⊗[R] M) :
        (a : S ⊗[R] S) → S ⊗[R] M)
      0)
Tactic: induction elem R S using TensorProduct.induction_on
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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
⊢ Eq (α := M →ₗ[S] M)
    ((TensorProduct.AlgebraTensorModule.lift
          (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))) :
        S ⊗[R] M →ₗ[S] M) ∘ₗ
      (sec R S M : M →ₗ[S] S ⊗[R] M))
    LinearMap.id
have h : ∀ (x : M),
  Eq (α := M)
    (((TensorProduct.AlgebraTensorModule.lift
                (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))) :
              S ⊗[R] M →ₗ[S] M) ∘ₗ
            (sec R S M : M →ₗ[S] S ⊗[R] M) :
          (a : M) → M)
        x :
      M)
    ((LinearMap.id : (a : M) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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
⊢ HSMul.hSMul (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (elem R S) : S) x = x
have rw : HSMul.hSMul.{u_2, u_3, u_3} (α := S) 1 x = x
Tactic: rw [lmul_elem, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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
⊢ HSMul.hSMul (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (elem R S) : S) x = x
have rw₁ : x = x
Tactic: rw [lmul_elem, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (hypothesis)
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)
⊢ IsField.{u_2} (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
have hmR : mR ≤ maximalIdeal S
Tactic: have hmR : mR ≤ maximalIdeal S := ((local_hom_TFAE (algebraMap R S)).out 0 2 rfl rfl).mp ‹_›
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (hypothesis)
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' := ⋯ }
⊢ IsField.{u_2} (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
have this₁ : IsScalarTower.{u_1, u_1, u_2} R (ResidueField R) (S ⧸ mR)
Tactic: have : IsScalarTower R (ResidueField R) (S ⧸ mR) := inferInstanceAs (IsScalarTower R (R ⧸ _) _)
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (hypothesis)
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)
⊢ IsField.{u_2} (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
have this₁ : FormallyUnramified.{u_2, u_1} (ResidueField R) (S ⧸ mR)
Tactic: have : FormallyUnramified (ResidueField R) (S ⧸ mR) := .of_restrictScalars R _ _
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (hypothesis)
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)
⊢ IsField.{u_2} (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
have this₁ : EssFiniteType.{u_1, u_2} (ResidueField R) (S ⧸ mR)
Tactic: have : EssFiniteType (ResidueField R) (S ⧸ mR) := .of_comp R _ _
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (hypothesis)
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)
⊢ IsField.{u_2} (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
have this₁ : Module.Finite.{u_1, u_2} (ResidueField R) (S ⧸ mR)
Tactic: have : Module.Finite (ResidueField R) (S ⧸ mR) := FormallyUnramified.finite_of_free _ _
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (hypothesis)
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)
⊢ IsField.{u_2} (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
have this₁ : IsReduced.{u_2} (S ⧸ mR)
Tactic: have : IsReduced (S ⧸ mR) := FormallyUnramified.isReduced_of_field (ResidueField R) (S ⧸ mR)
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (hypothesis)
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)
⊢ IsField.{u_2} (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
have this₁ : IsArtinianRing.{u_2} (S ⧸ mR)
Tactic: have : IsArtinianRing (S ⧸ mR) := isArtinian_of_tower (ResidueField R) inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (hypothesis)
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)
⊢ IsField.{u_2} (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
have this₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (hypothesis)
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)
⊢ IsField.{u_2} (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
have this₁ : IsLocalRing.{u_2} (S ⧸ mR)
Tactic: have : IsLocalRing (S ⧸ mR) := .of_surjective' _ Ideal.Quotient.mk_surjective
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (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 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)) ⊥
have rw : Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) (Ideal.jacobson ⊥) ⊥
Tactic: rw [← jacobson_eq_maximalIdeal _ bot_ne_top, IsArtinianRing.jacobson_eq_radical,
      ← Ideal.zero_eq_bot, ← nilradical, nilradical_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (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 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 ⊥) ⊥
⊢ Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) (maximalIdeal (S ⧸ mR)) ⊥
have rw₁ : Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) (Ideal.radical ⊥) ⊥
Tactic: rw [← jacobson_eq_maximalIdeal _ bot_ne_top, IsArtinianRing.jacobson_eq_radical,
      ← Ideal.zero_eq_bot, ← nilradical, nilradical_eq_zero]