awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_3 : IsLocalization.AtPrime S P
this_1 : Nontrivial S := ⋯
x y : S
hx : x ∈ nonunits S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
hxyz : (x + y) * z = 1
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hry : mk' S ry sy = y
rcases : ∀ (rz : R) (sz : ↥P.primeCompl) (hrz : mk' S rz sz = z), False
⊢ False

Tactic:
rcases exists_mk'_eq P.primeCompl z with ⟨rz, sz, hrz⟩

Premises used: Ideal.primeCompl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_3 : IsLocalization.AtPrime S P
this_1 : Nontrivial S := ⋯
x y : S
hx : x ∈ nonunits S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
hxyz : (x + y) * z = 1
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hrz : mk' S rz sz = z
rw :
  ∀ (hrx : mk' S rx sx = x) (ry : R) (sy : ↥P.primeCompl) (hry : mk' S ry sy = y) (rz : R) (sz : ↥P.primeCompl)
    (hxyz :
      mk' S ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) (sx * sy * sz) =
        mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ P.primeCompl) 1 ⋯))
    (hrz : mk' S rz sz = z), False
⊢ False

Tactic:
rw [← hrx, ← hry, ← hrz, ← mk'_add, ← mk'_mul, ← mk'_self S P.primeCompl.one_mem] at hxyz

Premises used: IsLocalization.mk'_self, Submonoid.one_mem, Ideal.primeCompl, IsLocalization.mk'_add, IsLocalization.mk'_mul
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_3 : IsLocalization.AtPrime S P
this_1 : Nontrivial S := ⋯
x y : S
hx : x ∈ nonunits S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hxyz :
  mk' S ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) (sx * sy * sz) =
    mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ P.primeCompl) 1 ⋯)
hrz : mk' S rz sz = z
rw :
  ∀ (hx : mk' S rx sx ∈ nonunits S) (hrx : mk' S rx sx = x) (ry : R) (sy : ↥P.primeCompl) (hry : mk' S ry sy = y)
    (rz : R) (sz : ↥P.primeCompl)
    (hxyz :
      mk' S ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) (sx * sy * sz) =
        mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ P.primeCompl) 1 ⋯))
    (hrz : mk' S rz sz = z), False
⊢ False

Tactic:
rw [← hrx] at hx
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_3 : IsLocalization.AtPrime S P
this_1 : Nontrivial S := ⋯
x y : S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hxyz :
  mk' S ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) (sx * sy * sz) =
    mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ P.primeCompl) 1 ⋯)
hrz : mk' S rz sz = z
rw :
  ∀ (hy : mk' S ry sy ∈ nonunits S) (hry : mk' S ry sy = y) (rz : R) (sz : ↥P.primeCompl)
    (hxyz :
      mk' S ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) (sx * sy * sz) =
        mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ P.primeCompl) 1 ⋯))
    (hrz : mk' S rz sz = z), False
⊢ False

Tactic:
rw [← hry] at hy
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_3 : IsLocalization.AtPrime S P
this_1 : Nontrivial S := ⋯
x y : S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hy : mk' S ry sy ∈ nonunits S
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hxyz :
  mk' S ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) (sx * sy * sz) =
    mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ P.primeCompl) 1 ⋯)
hrz : mk' S rz sz = z
obtain :
  ∀ (t : ↥P.primeCompl)
    (ht :
      (↑t : R) *
          ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ P.primeCompl) 1 ⋯) : R) * ((rx * (↑sy : R) + ry * (↑sx : R)) * rz)) =
        (↑t : R) * ((↑(sx * sy * sz) : R) * 1)),
    False
⊢ False

Tactic:
obtain ⟨t, ht⟩ := IsLocalization.eq.1 hxyz

Premises used: Iff.mp, IsLocalization.eq
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_3 : IsLocalization.AtPrime S P
this_1 : Nontrivial S := ⋯
x y : S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hy : mk' S ry sy ∈ nonunits S
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hxyz :
  mk' S ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) (sx * sy * sz) =
    mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ P.primeCompl) 1 ⋯)
hrz : mk' S rz sz = z
t : ↥P.primeCompl
ht :
  (↑t : R) *
      ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ P.primeCompl) 1 ⋯) : R) * ((rx * (↑sy : R) + ry * (↑sx : R)) * rz)) =
    (↑t : R) * ((↑(sx * sy * sz) : R) * 1)
⊢ (↑t : R) * ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) = (↑t : R) * ((↑sx : R) * (↑sy : R) * (↑sz : R))

Tactic:
simp only [mul_one, one_mul, Submonoid.coe_mul] at ht

Premises used: mul_one, one_mul, Submonoid.coe_mul
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_3 : IsLocalization.AtPrime S P
this_1 : Nontrivial S := ⋯
x y : S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hy : mk' S ry sy ∈ nonunits S
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hxyz :
  mk' S ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) (sx * sy * sz) =
    mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ P.primeCompl) 1 ⋯)
hrz : mk' S rz sz = z
t : ↥P.primeCompl
ht : (↑t : R) * ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) = (↑t : R) * ((↑sx : R) * (↑sy : R) * (↑sz : R))
suffices : (↑t : R) * ((↑sx : R) * (↑sy : R) * (↑sz : R)) ∈ P
⊢ False

Tactic:
suffices (t : R) * (sx * sy * sz) ∈ P from
        not_or_intro (mt hp.mem_or_mem <| not_or_intro sx.2 sy.2) sz.2
          (hp.mem_or_mem <| (hp.mem_or_mem this).resolve_left t.2)
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_3 : IsLocalization.AtPrime S P
this_1 : Nontrivial S := ⋯
x y : S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hy : mk' S ry sy ∈ nonunits S
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hxyz :
  mk' S ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) (sx * sy * sz) =
    mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ P.primeCompl) 1 ⋯)
hrz : mk' S rz sz = z
t : ↥P.primeCompl
ht : (↑t : R) * ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) = (↑t : R) * ((↑sx : R) * (↑sy : R) * (↑sz : R))
rw : (↑t : R) * ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) ∈ P
⊢ (↑t : R) * ((↑sx : R) * (↑sy : R) * (↑sz : R)) ∈ P

Tactic:
rw [← ht]
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_3 : IsLocalization.AtPrime S P
this_1 : Nontrivial S := ⋯
x y : S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hy : mk' S ry sy ∈ nonunits S
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hxyz :
  mk' S ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) (sx * sy * sz) =
    mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ P.primeCompl) 1 ⋯)
hrz : mk' S rz sz = z
t : ↥P.primeCompl
ht : (↑t : R) * ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) = (↑t : R) * ((↑sx : R) * (↑sy : R) * (↑sz : R))
⊢ (↑t : R) * ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) ∈ P

Tactic:
P.mul_mem_left _ <| P.mul_mem_right _ <|
            P.add_mem (P.mul_mem_right _ <| this hx) <| P.mul_mem_right _ <| this hy

Premises used: Ideal.add_mem, Ideal.mul_mem_right, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_3 : IsLocalization.AtPrime S P
this_1 : Nontrivial S := ⋯
x y : S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hy : mk' S ry sy ∈ nonunits S
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hxyz :
  mk' S ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) (sx * sy * sz) =
    mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ P.primeCompl) 1 ⋯)
hrz : mk' S rz sz = z
t : ↥P.primeCompl
ht : (↑t : R) * ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) = (↑t : R) * ((↑sx : R) * (↑sy : R) * (↑sz : R))
⊢ (↑t : R) * ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) ∈ P

Tactic:
exact
        P.mul_mem_left _ <| P.mul_mem_right _ <|
            P.add_mem (P.mul_mem_right _ <| this hx) <| P.mul_mem_right _ <| this hy

Premises used: Ideal.add_mem, Ideal.mul_mem_right, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P_1 : Type u_3
inst_3 : CommSemiring P_1
P_2 : Ideal R
hp : P_2.IsPrime
A : Type u_4
inst_4 : CommRing A
inst_5 : IsDomain A
P : Ideal A
h : P.IsPrime
⊢ IsDomain.{u_4} (Localization.AtPrime P)

Tactic:
isDomain_localization P.primeCompl_le_nonZeroDivisors

Premises used: IsLocalization.isDomain_localization, Ideal.primeCompl_le_nonZeroDivisors
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P_1 : Type u_3
inst_3 : CommSemiring P_1
P : Ideal R
hp : P.IsPrime
⊢ IsLocalRing.{u_1} (Localization (M := R) P.primeCompl)

Tactic:
IsLocalization.AtPrime.isLocalRing (Localization P.primeCompl) P

Premises used: Localization, IsLocalization.AtPrime.isLocalRing, Ideal.primeCompl
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
P_2 : Ideal R_1
hp : P_2.IsPrime
R : Type u_4
S : Type u_5
inst_4 : CommRing R
inst_5 : IsDomain R
P : Ideal R
inst_6 : CommRing S
inst_7 : Algebra R S
inst_8 : IsTorsionFree R S
inst_9 : IsDomain S
inst_10 : P.IsPrime
⊢ IsTorsionFree.{u_4, u_5} (Localization.AtPrime P) (Localization (M := S) (Algebra.algebraMapSubmonoid S P.primeCompl))

Tactic:
.of_isLocalization R S P.primeCompl_le_nonZeroDivisors

Premises used: Module.IsTorsionFree.of_isLocalization, Ideal.primeCompl_le_nonZeroDivisors
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
S : Type u_2
inst : CommSemiring S
R : Type u_4
inst_1 : CommRing R
inst_2 : NoZeroDivisors R
inst_3 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_4 : IsLocalization.AtPrime S P
rw : ∀ (c : ↥P.primeCompl), IsRegular (↑c : R)
⊢ FaithfulSMul R S

Tactic:
rw [faithfulSMul_iff_algebraMap_injective, IsLocalization.injective_iff_isRegular P.primeCompl]

Premises used: faithfulSMul_iff_algebraMap_injective, IsLocalization.injective_iff_isRegular, Ideal.primeCompl
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
S : Type u_2
inst : CommSemiring S
R : Type u_4
inst_1 : CommRing R
inst_2 : NoZeroDivisors R
inst_3 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_4 : IsLocalization.AtPrime S P
x : ↥P.primeCompl
val : R
h : val ∈ P.primeCompl
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ P.primeCompl) val h) : R) ≠ 0

Tactic:
aesop
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
S : Type u_2
inst : CommSemiring S
R : Type u_4
inst_1 : CommRing R
inst_2 : NoZeroDivisors R
inst_3 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_4 : IsLocalization.AtPrime S P
⊢ ∀ (c : ↥P.primeCompl), IsRegular (↑c : R)

Tactic:
exact fun ⟨_, h⟩ ↦ .of_ne_zero <| by aesop
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R_1 S
P_1 : Type u_3
inst_3 : CommSemiring P_1
P_2 : Ideal R_1
hp_1 : P_2.IsPrime
R : Type u_4
inst_4 : CommRing R
inst_5 : NoZeroDivisors R
P : Ideal R
hp : P.IsPrime
⊢ FaithfulSMul R (Localization.AtPrime P)

Tactic:
IsLocalization.AtPrime.faithfulSMul _ _ P

Premises used: IsLocalization.AtPrime.faithfulSMul
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
A : Type u_4
inst : CommRing A
inst_1 : IsDomain A
S : Type u_5
inst_2 : CommSemiring S
inst_3 : Algebra A S
P : Ideal A
inst_4 : P.IsPrime
inst_5 : IsLocalization.AtPrime S P
⊢ IsDomain S

Tactic:
isDomain_of_le_nonZeroDivisors S P.primeCompl_le_nonZeroDivisors

Premises used: IsLocalization.isDomain_of_le_nonZeroDivisors, Ideal.primeCompl_le_nonZeroDivisors
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
A : Type u_4
inst_4 : CommRing A
inst_5 : IsDomain A
I : Ideal R
hI : I.IsPrime
inst_6 : IsLocalization.AtPrime S I
h :
  ∀ (x : Ideal R),
    Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p.IsPrime ∧ Disjoint (↑I.primeCompl : Set R) (↑p : Set R)} x ↔
      Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p.IsPrime ∧ p ≤ I} x
⊢ Eq.{u_1 + 1} (α := Set (Ideal R)) {p : Ideal R | p.IsPrime ∧ Disjoint (↑I.primeCompl : Set R) (↑p : Set R)}
    {p : Ideal R | p.IsPrime ∧ p ≤ I}

Tactic:
ext
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
A : Type u_4
inst_4 : CommRing A
inst_5 : IsDomain A
I : Ideal R
hI : I.IsPrime
inst_6 : IsLocalization.AtPrime S I
x : Ideal R
⊢ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p.IsPrime ∧ Disjoint (↑I.primeCompl : Set R) (↑p : Set R)} x ↔
    Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p.IsPrime ∧ p ≤ I} x

Tactic:
simp [Ideal.primeCompl, ← le_compl_iff_disjoint_left]

Premises used: le_compl_iff_disjoint_left, Ideal.primeCompl
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
I : Ideal R
hI : I.IsPrime
inst_3 : IsLocalization.AtPrime S I
x : R
⊢ IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) x : S) ↔ x ∈ I.primeCompl

Tactic:
⟨fun h hx =>
    (isPrime_of_isPrime_disjoint I.primeCompl S I hI disjoint_compl_left).ne_top <|
      (Ideal.map (algebraMap R S) I).eq_top_of_isUnit_mem (Ideal.mem_map_of_mem _ hx) h,
    fun h => map_units S ⟨x, h⟩⟩

Premises used: Algebra.algebraMap, Ideal.mem_map_of_mem, Ideal.eq_top_of_isUnit_mem, disjoint_compl_left, Ideal.map, IsLocalization.isPrime_of_isPrime_disjoint, Subtype.mk, Iff.intro, IsLocalization.map_units, Ideal.primeCompl, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
I : Ideal R
hI : I.IsPrime
inst_3 : IsLocalization.AtPrime S I
x : R
h : IsLocalRing S
⊢ ((algebraMap R S : (a : R) → S) x : S) ∉ IsLocalRing.maximalIdeal S ↔ x ∉ I

Tactic:
simpa only [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff, Classical.not_not] using
      isUnit_to_map_iff S I x

Premises used: Classical.not_not, mem_nonunits_iff, IsLocalRing.mem_maximalIdeal, IsLocalization.AtPrime.isUnit_to_map_iff
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
I : Ideal R
hI : I.IsPrime
inst_3 : IsLocalization.AtPrime S I
h : IsLocalRing S
x : R
⊢ Membership.mem (γ := Ideal R) (Ideal.under R (IsLocalRing.maximalIdeal S)) x ↔ x ∈ I

Tactic:
simpa only [Ideal.mem_comap] using to_map_mem_maximal_iff _ I x

Premises used: IsLocalization.AtPrime.to_map_mem_maximal_iff, IsLocalization.AtPrime.isLocalRing, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
A : Type u_4
inst_4 : CommRing A
inst_5 : IsDomain A
I : Ideal R
hI : I.IsPrime
inst_6 : IsLocalization.AtPrime S I
h : IsLocalRing S
⊢ Ideal.LiesOver (IsLocalRing.maximalIdeal S) I

Tactic:
(Ideal.liesOver_iff _ _).mpr (under_maximalIdeal _ _).symm

Premises used: Iff.mpr, Ideal.liesOver_iff, IsLocalization.AtPrime.isLocalRing, IsLocalization.AtPrime.under_maximalIdeal, Eq.symm
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
I : Ideal R
hI : I.IsPrime
inst_3 : IsLocalization.AtPrime S I
x : R
y : ↥I.primeCompl
⊢ IsUnit (mk' S x y) ↔ x ∈ I.primeCompl

Tactic:
⟨fun h hx => mk'_mem_iff.mpr ((to_map_mem_maximal_iff S I x).mpr hx) h, fun h =>
    isUnit_iff_exists_inv.mpr ⟨mk' S ↑y ⟨x, h⟩, mk'_mul_mk'_eq_one ⟨x, h⟩ y⟩⟩

Premises used: Iff.mpr, IsLocalization.mk'_mem_iff, isUnit_iff_exists_inv, IsLocalization.AtPrime.to_map_mem_maximal_iff, Subtype.mk, IsLocalization.mk', IsLocalization.AtPrime.isLocalRing, Iff.intro, Exists.intro
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
I : Ideal R
hI : I.IsPrime
inst_3 : IsLocalization.AtPrime S I
x : R
y : ↥I.primeCompl
h : IsLocalRing S
⊢ mk' S x y ∉ IsLocalRing.maximalIdeal S ↔ x ∉ I

Tactic:
simpa only [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff, Classical.not_not] using
      isUnit_mk'_iff S I x y

Premises used: Classical.not_not, mem_nonunits_iff, IsLocalRing.mem_maximalIdeal, IsLocalization.AtPrime.isUnit_mk'_iff
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hI : I.IsPrime
⊢ Ideal.under R (B := Localization (M := R) I.primeCompl)
      (IsLocalRing.maximalIdeal (Localization (M := R) I.primeCompl)) =
    I

Tactic:
IsLocalization.AtPrime.under_maximalIdeal _ _

Premises used: IsLocalization.AtPrime.isLocalRing, IsLocalization.AtPrime.under_maximalIdeal
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hI : I.IsPrime
⊢ Eq (α := Ideal (Localization.AtPrime I))
    (Ideal.map (F := R →+* Localization.AtPrime I) (algebraMap R (Localization.AtPrime I)) I)
    (Ideal.map (F := R →+* Localization.AtPrime I) (algebraMap R (Localization.AtPrime I))
      (Ideal.under R (B := Localization (M := R) I.primeCompl)
        (IsLocalRing.maximalIdeal (Localization (M := R) I.primeCompl))))

Tactic:
congr_arg (Ideal.map _) AtPrime.under_maximalIdeal.symm

Premises used: Ideal.map, Localization.AtPrime.under_maximalIdeal, congr_arg, Eq.symm
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hI : I.IsPrime
h :
  Eq (α := Ideal (Localization.AtPrime I)) (IsLocalRing.maximalIdeal (Localization (M := R) I.primeCompl))
    (Ideal.map (F := R →+* Localization.AtPrime I) (algebraMap R (Localization.AtPrime I))
      (Ideal.under R (B := Localization (M := R) I.primeCompl)
        (IsLocalRing.maximalIdeal (Localization (M := R) I.primeCompl))))
convert_8 : I.IsPrime
⊢ Eq (α := Ideal (Localization.AtPrime I))
    (Ideal.map (F := R →+* Localization.AtPrime I) (algebraMap R (Localization.AtPrime I)) I)
    (IsLocalRing.maximalIdeal (Localization (M := R) I.primeCompl))

Tactic:
convert! congr_arg (Ideal.map _) AtPrime.under_maximalIdeal.symm

Premises used: Ideal.map, Localization.AtPrime.under_maximalIdeal, congr_arg, Eq.symm
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hI : I.IsPrime
J : Ideal (Localization.AtPrime I)
h : Ideal.under R J = I
⊢ IsLocalRing.maximalIdeal (Localization.AtPrime I) ≤ J

Tactic:
simpa [← AtPrime.map_eq_maximalIdeal, ← h] using Ideal.map_comap_le

Premises used: Ideal.map_comap_le, Localization.AtPrime.map_eq_maximalIdeal
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_3
inst_1 : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst_2 : J.IsPrime
f : R →+* P
h : I.primeCompl ≤ Submonoid.comap f J.primeCompl
x : R
hx : Membership.mem (γ := Submodule R R) (Ideal.comap f J) x
contrapose : ∀ (hx : x ∉ I), x ∉ Ideal.comap f J
⊢ x ∈ I

Tactic:
contrapose hx
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_3
inst_1 : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst_2 : J.IsPrime
f : R →+* P
h : I.primeCompl ≤ Submonoid.comap f J.primeCompl
x : R
hx : x ∉ I
⊢ x ∉ Ideal.comap f J

Tactic:
h hx

Premises used: Set.Mem, setOf, Set.preimage, Not
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_3
inst_1 : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst_2 : J.IsPrime
f : R →+* P
h : I.primeCompl ≤ Submonoid.comap f J.primeCompl
x : R
hx : x ∉ I
⊢ x ∉ Ideal.comap f J

Tactic:
exact h hx
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_3
inst_1 : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst_2 : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
x : R
⊢ Eq.{u_3 + 1} (α := Localization.AtPrime J)
    (((localRingHom I J f hIJ : RingHom.{u_1, u_3} (Localization.AtPrime I) (Localization.AtPrime J)) :
          (a : Localization.AtPrime I) → Localization.AtPrime J)
        ((algebraMap R (Localization.AtPrime I) : (a : R) → Localization.AtPrime I) x) :
      Localization.AtPrime J)
    ((algebraMap P (Localization.AtPrime J) : (a : P) → Localization.AtPrime J) ((f : (a : R) → P) x) :
      Localization.AtPrime J)

Tactic:
map_eq _ _

Premises used: IsLocalization.map_eq
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_3
inst_1 : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst_2 : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
x : R
y : ↥I.primeCompl
⊢ Eq.{u_3 + 1} (α := Localization.AtPrime J)
    (((localRingHom I J f hIJ : RingHom.{u_1, u_3} (Localization.AtPrime I) (Localization.AtPrime J)) :
          (a : Localization.AtPrime I) → Localization.AtPrime J)
        (mk' (Localization.AtPrime I) x y) :
      Localization.AtPrime J)
    (mk' (R := P) (M := J.primeCompl) (Localization.AtPrime J) ((f : (a : R) → P) x : P)
        (Subtype.mk (p := fun (x : P) ↦ x ∈ J.primeCompl) ((f : (a : R) → P) (↑y : R)) ⋯ : ↥J.primeCompl) :
      Localization.AtPrime J)

Tactic:
map_mk' _ _ _

Premises used: IsLocalization.map_mk'
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst_4 : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
x : R
y : ↥I.primeCompl
⊢ Membership.mem (α := P) J.primeCompl ((f : (a : R) → P) (↑y : R) : P)

Tactic:
aesop