awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalRing.LocalSubring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
A_1 : Subring K
P_1 : Ideal ↥A_1
inst_3 : P_1.IsPrime
A : Subring K
P : Ideal ↥A
inst_4 : P.IsPrime
⊢ ∀ (y : ↥P.primeCompl), IsUnit (M := K) ((A.subtype : (a : ↥A) → K) (↑y : ↥A) : K)

Tactic:
simp [Ideal.primeCompl, not_imp_not]

Premises used: Ideal.primeCompl, not_imp_not
-- Module: Mathlib.RingTheory.LocalRing.LocalSubring
Goal:
K : Type u_3
inst : Field K
A : Subring K
P : Ideal ↥A
inst_1 : P.IsPrime
x : K
hx : x ∈ A
⊢ (IsLocalization.lift (M := P.primeCompl) ⋯ : (a : Localization.AtPrime P) → K)
      ((algebraMap (↥A) (Localization.AtPrime P) : (a : ↥A) → Localization.AtPrime P)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ A) x hx) :
        Localization.AtPrime P) =
    x

Tactic:
simp
-- Module: Mathlib.RingTheory.LocalRing.LocalSubring
Goal:
K : Type u_3
inst : Field K
A : Subring K
P : Ideal ↥A
inst_1 : P.IsPrime
x : K
hx : x ∈ A
⊢ x ∈ (ofPrime A P).toSubring

Tactic:
exact ⟨algebraMap A _ ⟨x, hx⟩, by simp⟩
-- Module: Mathlib.RingTheory.LocalRing.LocalSubring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
A : Subring K
P : Ideal ↥A
inst_3 : P.IsPrime
⊢ IsScalarTower (↥A) (↥(ofPrime A P).toSubring) K

Tactic:
.of_algebraMap_eq (fun _ ↦ rfl)

Premises used: IsScalarTower.of_algebraMap_eq, rfl
-- Module: Mathlib.RingTheory.LocalRing.LocalSubring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
A : Subring K
P : Ideal ↥A
inst_3 : P.IsPrime
refine :
  Function.Injective.{u_3 + 1, u_3 + 1} (α := Localization.AtPrime P) (β := K)
    (⇑(IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
            Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
          Localization.AtPrime P →ₐ[↥A] K) :
      (a : Localization.AtPrime P) → K)
⊢ Localization.AtPrime P ≃ₐ[↥A] ↥(ofPrime A P).toSubring

Tactic:
refine AlgEquiv.ofInjective (IsLocalization.liftAlgHom (M := P.primeCompl)
    (S := Localization.AtPrime P) (f := Algebra.ofId A K) _) ?_

Premises used: AlgEquiv.ofInjective, IsLocalization.liftAlgHom
-- Module: Mathlib.RingTheory.LocalRing.LocalSubring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
A : Subring K
P : Ideal ↥A
inst_3 : P.IsPrime
x y : Localization.AtPrime P
e :
  Eq (α := K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        x :
      K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        y :
      K)
obtain :
  ∀ (x : ↥A) (s : ↥P.primeCompl)
    (e :
      Eq (α := K)
        (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
                  Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
                Localization.AtPrime P →ₐ[↥A] K) :
              (a : Localization.AtPrime P) → K)
            (IsLocalization.mk' (Localization.AtPrime P) x s) :
          K)
        (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
                  Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
                Localization.AtPrime P →ₐ[↥A] K) :
              (a : Localization.AtPrime P) → K)
            y :
          K)),
    IsLocalization.mk' (Localization.AtPrime P) x s = y
⊢ x = y

Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq P.primeCompl x

Premises used: Ideal.primeCompl, rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.LocalRing.LocalSubring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
A : Subring K
P : Ideal ↥A
inst_3 : P.IsPrime
y : Localization.AtPrime P
x : ↥A
s : ↥P.primeCompl
e :
  Eq (α := K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) x s) :
      K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        y :
      K)
obtain :
  ∀ (y : ↥A) (t : ↥P.primeCompl)
    (e :
      Eq (α := K)
        (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
                  Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
                Localization.AtPrime P →ₐ[↥A] K) :
              (a : Localization.AtPrime P) → K)
            (IsLocalization.mk' (Localization.AtPrime P) x s) :
          K)
        (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
                  Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
                Localization.AtPrime P →ₐ[↥A] K) :
              (a : Localization.AtPrime P) → K)
            (IsLocalization.mk' (Localization.AtPrime P) y t) :
          K)),
    Eq (α := Localization.AtPrime P) (IsLocalization.mk' (Localization.AtPrime P) x s)
      (IsLocalization.mk' (Localization.AtPrime P) y t)
⊢ IsLocalization.mk' (Localization.AtPrime P) x s = y

Tactic:
obtain ⟨y, t, rfl⟩ := IsLocalization.exists_mk'_eq P.primeCompl y

Premises used: Ideal.primeCompl, rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.LocalRing.LocalSubring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
A : Subring K
P : Ideal ↥A
inst_3 : P.IsPrime
x : ↥A
s : ↥P.primeCompl
y : ↥A
t : ↥P.primeCompl
e :
  Eq (α := K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) x s) :
      K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) y t) :
      K)
hx : 0 ∈ P.primeCompl
⊢ False

Tactic:
aesop
-- Module: Mathlib.RingTheory.LocalRing.LocalSubring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
A : Subring K
P : Ideal ↥A
inst_3 : P.IsPrime
x : ↥A
s : ↥P.primeCompl
y : ↥A
t : ↥P.primeCompl
e :
  Eq (α := K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) x s) :
      K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) y t) :
      K)
⊢ ∀ (x : ↥P.primeCompl), (↑x : ↥A) ≠ 0

Tactic:
have H : ∀ x : P.primeCompl, x.1 ≠ 0 := by rintro ⟨x, hx⟩ rfl; aesop
-- Module: Mathlib.RingTheory.LocalRing.LocalSubring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
A : Subring K
P : Ideal ↥A
inst_3 : P.IsPrime
x : ↥A
s : ↥P.primeCompl
y : ↥A
t : ↥P.primeCompl
e :
  Eq (α := K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) x s) :
      K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) y t) :
      K)
H : ∀ (x : ↥P.primeCompl), (↑x : ↥A) ≠ 0
⊢ (↑x : K) = (↑y : K) * (↑(↑t : ↥A) : K)⁻¹ * (↑(↑s : ↥A) : K)

Tactic:
simpa [IsLocalization.lift_mk', Algebra.ofId_apply, H,
      Algebra.algebraMap_ofSubsemiring_apply, IsUnit.coe_liftRight] using congr($e * s.1.1)

Premises used: Algebra.algebraMap_ofSubsemiring_apply, IsLocalization.lift_mk', IsUnit.coe_liftRight, Algebra.ofId_apply, Subtype.val
-- Module: Mathlib.RingTheory.LocalRing.LocalSubring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
A : Subring K
P : Ideal ↥A
inst_3 : P.IsPrime
x : ↥A
s : ↥P.primeCompl
y : ↥A
t : ↥P.primeCompl
e :
  Eq (α := K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) x s) :
      K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) y t) :
      K)
H : ∀ (x : ↥P.primeCompl), (↑x : ↥A) ≠ 0
⊢ (↑x : K) = (↑y : K) * (↑(↑t : ↥A) : K)⁻¹ * (↑(↑s : ↥A) : K)

Tactic:
have : x.1 = y.1 * t.1.1⁻¹ * s.1.1 := by
    simpa [IsLocalization.lift_mk', Algebra.ofId_apply, H,
      Algebra.algebraMap_ofSubsemiring_apply, IsUnit.coe_liftRight] using congr($e * s.1.1)
-- Module: Mathlib.RingTheory.LocalRing.LocalSubring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
A : Subring K
P : Ideal ↥A
inst_3 : P.IsPrime
x : ↥A
s : ↥P.primeCompl
y : ↥A
t : ↥P.primeCompl
e :
  Eq (α := K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) x s) :
      K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) y t) :
      K)
H : ∀ (x : ↥P.primeCompl), (↑x : ↥A) ≠ 0
this : (↑x : K) = (↑y : K) * (↑(↑t : ↥A) : K)⁻¹ * (↑(↑s : ↥A) : K)
rw :
  Eq (α := Localization.AtPrime P)
    ((algebraMap (↥A) (Localization.AtPrime P) : (a : ↥A) → Localization.AtPrime P) ((↑t : ↥A) * x) :
      Localization.AtPrime P)
    ((algebraMap (↥A) (Localization.AtPrime P) : (a : ↥A) → Localization.AtPrime P) ((↑s : ↥A) * y) :
      Localization.AtPrime P)
⊢ Eq (α := Localization.AtPrime P) (IsLocalization.mk' (Localization.AtPrime P) x s)
    (IsLocalization.mk' (Localization.AtPrime P) y t)

Tactic:
rw [IsLocalization.mk'_eq_iff_eq]

Premises used: IsLocalization.mk'_eq_iff_eq
-- Module: Mathlib.RingTheory.LocalRing.LocalSubring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
A : Subring K
P : Ideal ↥A
inst_3 : P.IsPrime
x : ↥A
s : ↥P.primeCompl
y : ↥A
t : ↥P.primeCompl
e :
  Eq (α := K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) x s) :
      K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) y t) :
      K)
H : ∀ (x : ↥P.primeCompl), (↑x : ↥A) ≠ 0
this : (↑x : K) = (↑y : K) * (↑(↑t : ↥A) : K)⁻¹ * (↑(↑s : ↥A) : K)
h : (↑t : ↥A) * x = (↑s : ↥A) * y
⊢ Eq (α := Localization.AtPrime P)
    ((algebraMap (↥A) (Localization.AtPrime P) : (a : ↥A) → Localization.AtPrime P) ((↑t : ↥A) * x) :
      Localization.AtPrime P)
    ((algebraMap (↥A) (Localization.AtPrime P) : (a : ↥A) → Localization.AtPrime P) ((↑s : ↥A) * y) :
      Localization.AtPrime P)

Tactic:
congr 1
-- Module: Mathlib.RingTheory.LocalRing.LocalSubring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
A : Subring K
P : Ideal ↥A
inst_3 : P.IsPrime
x : ↥A
s : ↥P.primeCompl
y : ↥A
t : ↥P.primeCompl
e :
  Eq (α := K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) x s) :
      K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) y t) :
      K)
H : ∀ (x : ↥P.primeCompl), (↑x : ↥A) ≠ 0
this : (↑x : K) = (↑y : K) * (↑(↑t : ↥A) : K)⁻¹ * (↑(↑s : ↥A) : K)
h : (↑((↑t : ↥A) * x) : K) = (↑((↑s : ↥A) * y) : K)
⊢ (↑t : ↥A) * x = (↑s : ↥A) * y

Tactic:
ext
-- Module: Mathlib.RingTheory.LocalRing.LocalSubring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
A : Subring K
P : Ideal ↥A
inst_3 : P.IsPrime
x : ↥A
s : ↥P.primeCompl
y : ↥A
t : ↥P.primeCompl
e :
  Eq (α := K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) x s) :
      K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) y t) :
      K)
H : ∀ (x : ↥P.primeCompl), (↑x : ↥A) ≠ 0
this : (↑x : K) = (↑y : K) * (↑(↑t : ↥A) : K)⁻¹ * (↑(↑s : ↥A) : K)
⊢ (↑((↑t : ↥A) * x) : K) = (↑((↑s : ↥A) * y) : K)

Tactic:
simp [field, H t, this, mul_comm]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.LocalRing.LocalSubring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
A : Subring K
P : Ideal ↥A
inst_3 : P.IsPrime
⊢ IsLocalization.AtPrime (↥(ofPrime A P).toSubring) P

Tactic:
IsLocalization.isLocalization_of_algEquiv _ (ofPrimeEquiv A P)

Premises used: LocalSubring.ofPrimeEquiv, IsLocalization.isLocalization_of_algEquiv
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
x : R
⊢ Membership.mem (γ := Ideal R) (maximalIdeal R) x ↔ x ∈ nonunits R

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, nonunits, Not
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommSemiring R
inst_1 : IsLocalRing R
rw : 1 ∉ maximalIdeal R ∧ ∀ (J : Ideal R) (x : R), maximalIdeal R ≤ J → x ∉ maximalIdeal R → x ∈ J → 1 ∈ J
⊢ Ideal.IsMaximal (maximalIdeal R)

Tactic:
rw [Ideal.isMaximal_iff]

Premises used: Ideal.isMaximal_iff
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommSemiring R
inst_1 : IsLocalRing R
left : 1 ∉ maximalIdeal R
right : ∀ (J : Ideal R) (x : R), maximalIdeal R ≤ J → x ∉ maximalIdeal R → x ∈ J → 1 ∈ J
⊢ 1 ∉ maximalIdeal R ∧ ∀ (J : Ideal R) (x : R), maximalIdeal R ≤ J → x ∉ maximalIdeal R → x ∈ J → 1 ∈ J

Tactic:
constructor
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommSemiring R
inst_1 : IsLocalRing R
h : Membership.mem (γ := Ideal R) (maximalIdeal R) 1
left : IsUnit.{u_1} (M := R) 1
⊢ False

Tactic:
apply h
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommSemiring R
inst_1 : IsLocalRing R
h : Membership.mem (γ := Ideal R) (maximalIdeal R) 1
⊢ IsUnit.{u_1} (M := R) 1

Tactic:
isUnit_one

Premises used: isUnit_one
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommSemiring R
inst_1 : IsLocalRing R
h : Membership.mem (γ := Ideal R) (maximalIdeal R) 1
⊢ IsUnit.{u_1} (M := R) 1

Tactic:
exact isUnit_one

Premises used: isUnit_one
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommSemiring R
inst_1 : IsLocalRing R
I : Ideal R
x : R
right : maximalIdeal R ≤ I → x ∉ maximalIdeal R → x ∈ I → 1 ∈ I
⊢ maximalIdeal R ≤ I → x ∉ maximalIdeal R → x ∈ I → 1 ∈ I

Tactic:
_
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommSemiring R
inst_1 : IsLocalRing R
I : Ideal R
x : R
h : maximalIdeal R ≤ I
hx : x ∉ maximalIdeal R
H : x ∈ I
⊢ IsUnit x

Tactic:
rw [mem_maximalIdeal, mem_nonunits_iff, Classical.not_not] at hx

Premises used: Classical.not_not, mem_nonunits_iff, IsLocalRing.mem_maximalIdeal
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommSemiring R
inst_1 : IsLocalRing R
I : Ideal R
x : R
h : maximalIdeal R ≤ I
hx : x ∉ maximalIdeal R
H : x ∈ I
hx₁ : IsUnit x
⊢ x ∈ I

Tactic:
rw [mem_maximalIdeal, mem_nonunits_iff, Classical.not_not] at hx

Premises used: Classical.not_not, mem_nonunits_iff, IsLocalRing.mem_maximalIdeal
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommSemiring R
inst_1 : IsLocalRing R
I : Ideal R
x : R
h : maximalIdeal R ≤ I
hx : IsUnit x
H : x ∈ I
right : ∀ (u : Rˣ) (H : (↑u : R) ∈ I), 1 ∈ I
⊢ 1 ∈ I

Tactic:
rcases hx with ⟨u, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommSemiring R
inst_1 : IsLocalRing R
I : Ideal R
h : maximalIdeal R ≤ I
u : Rˣ
H : (↑u : R) ∈ I
⊢ 1 ∈ I

Tactic:
simpa using I.mul_mem_left (↑u⁻¹) H

Premises used: Units.val, Inv.inv, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
⊢ ∃! I : Ideal R, I.IsMaximal

Tactic:
simp [isMaximal_iff]

Premises used: IsLocalRing.isMaximal_iff
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
I : Ideal R
hI : I.IsMaximal
⊢ I = maximalIdeal R

Tactic:
ExistsUnique.unique (maximal_ideal_unique R) hI <| maximalIdeal.isMaximal R

Premises used: IsLocalRing.maximal_ideal_unique, IsLocalRing.maximalIdeal.isMaximal, ExistsUnique.unique
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Subsingleton.{u_1 + 1} (MaximalSpectrum R)
inst_2 : Nonempty.{u_1 + 1} (MaximalSpectrum R)
⊢ IsLocalRing R

Tactic:
let m := Classical.arbitrary (MaximalSpectrum R)
  .of_unique_max_ideal ⟨m.asIdeal, m.isMaximal,
    fun I hI ↦ MaximalSpectrum.mk.inj <| Subsingleton.elim ⟨I, hI⟩ m⟩

Premises used: MaximalSpectrum.asIdeal, MaximalSpectrum.mk.inj, MaximalSpectrum.isMaximal, IsLocalRing.of_unique_max_ideal, MaximalSpectrum, And.intro, Exists.intro, Classical.arbitrary
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
J : Ideal R
hJ : J ≠ ⊤
rcases : ∀ (M : Ideal R) (hM1 : M.IsMaximal) (hM2 : J ≤ M), J ≤ maximalIdeal R
⊢ J ≤ maximalIdeal R

Tactic:
rcases Ideal.exists_le_maximal J hJ with ⟨M, hM1, hM2⟩

Premises used: Ideal.exists_le_maximal
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
J : Ideal R
hJ : J ≠ ⊤
M : Ideal R
hM1 : M.IsMaximal
hM2 rwa rwa₁ rwa₂ rwa₃ : J ≤ M
⊢ J ≤ maximalIdeal R

Tactic:
rwa [← eq_maximalIdeal hM1]

Premises used: IsLocalRing.eq_maximalIdeal
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
p : Ideal R
hp : p.IsPrime
⊢ p ≤ maximalIdeal R

Tactic:
le_maximalIdeal hp.ne_top

Premises used: IsLocalRing.le_maximalIdeal, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
x : R
⊢ x ∉ maximalIdeal R ↔ IsUnit x

Tactic:
simp only [mem_maximalIdeal, mem_nonunits_iff, not_not]

Premises used: Classical.not_not, mem_nonunits_iff, IsLocalRing.mem_maximalIdeal
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
⊢ IsField R ↔ Eq (α := Ideal R) (maximalIdeal R) ⊥

Tactic:
not_iff_not.mp
    ⟨Ring.ne_bot_of_isMaximal_of_not_isField inferInstance, fun h =>
      Ring.not_isField_iff_exists_prime.mpr ⟨_, h, Ideal.IsMaximal.isPrime' _⟩⟩

Premises used: not_iff_not, Iff.mpr, Ring.ne_bot_of_isMaximal_of_not_isField, IsLocalRing.maximalIdeal, inferInstance, Ring.not_isField_iff_exists_prime, And.intro, Iff.intro, Exists.intro, Iff.mp, Ideal.IsMaximal.isPrime'
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
I : Ideal R
⊢ maximalIdeal R ≤ I.jacobson

Tactic:
le_sInf fun _ ⟨_, h⟩ => le_of_eq (IsLocalRing.eq_maximalIdeal h).symm

Premises used: Set.Mem, IsLocalRing.maximalIdeal, _private.0.IsLocalRing.maximalIdeal_le_jacobson.match_1, LE.le, le_sInf, le_of_eq, Eq.symm, IsLocalRing.eq_maximalIdeal
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
I : Ideal R
h : I ≠ ⊤
⊢ I.jacobson = maximalIdeal R

Tactic:
le_antisymm (sInf_le ⟨le_maximalIdeal h, maximalIdeal.isMaximal R⟩)
              (maximalIdeal_le_jacobson I)

Premises used: IsLocalRing.maximalIdeal_le_jacobson, le_antisymm, IsLocalRing.maximalIdeal.isMaximal, sInf_le, And.intro, IsLocalRing.le_maximalIdeal
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
⊢ Eq (α := Ideal R) (Ring.jacobson R) (maximalIdeal R)

Tactic:
Ideal.jacobson_bot.symm.trans (jacobson_eq_maximalIdeal _ top_ne_bot.symm)

Premises used: Ideal.jacobson_bot, top_ne_bot, Ne.symm, IsLocalRing.jacobson_eq_maximalIdeal, Eq.symm, Eq.trans