awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : ∀ x ∈ I, ∃ y ∈ I, x = x * y
p : Ideal R
inst_1 : p.IsPrime
hle : I ≤ p
x : R
hx : x ∈ I
y : R
hy : y ∈ I
heq : x = x * y
this :
  IsUnit (M := Localization.AtPrime p)
    ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (1 - y) : Localization.AtPrime p)
⊢ x * (1 - y) = 0

Tactic:
simp [mul_sub, ← heq]

Premises used: mul_sub
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : ∀ x ∈ I, ∃ y ∈ I, x = x * y
p : Ideal R
inst_1 : p.IsPrime
hle : I ≤ p
x : R
hx : x ∈ I
y : R
hy : y ∈ I
heq : x = x * y
this :
  IsUnit (M := Localization.AtPrime p)
    ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (1 - y) : Localization.AtPrime p)
⊢ x * (1 - y) = 0

Tactic:
have hzero : x * (1 - y) = 0 := by simp [mul_sub, ← heq]
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : ∀ x ∈ I, ∃ y ∈ I, x = x * y
p : Ideal R
inst_1 : p.IsPrime
hle : I ≤ p
x : R
hx : x ∈ I
y : R
hy : y ∈ I
heq : x = x * y
this :
  IsUnit (M := Localization.AtPrime p)
    ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (1 - y) : Localization.AtPrime p)
hzero : x * (1 - y) = 0
⊢ Membership.mem (γ := Submodule R R)
    (RingHom.ker (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p))) x

Tactic:
simp only [RingHom.mem_ker, ← this.mul_left_eq_zero, ← RingHom.map_mul, hzero, RingHom.map_zero]

Premises used: RingHom.mem_ker, IsUnit.mul_left_eq_zero, RingHom.map_zero, RingHom.map_mul
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.Pure
⊢ RingHom.ker (F :=
      R →+* (i : (↑(zeroLocus (↑I : Set R)) : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
      (Pi.ringHom (f := fun (p : (↑(zeroLocus (↑I : Set R)) : Type u_1)) ↦
        Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal) fun (p : (↑(zeroLocus (↑I : Set R)) : Type u_1)) ↦
        algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)) =
    I

Tactic:
le_antisymm ?_ fun x hx ↦ ?_

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.Pure
refine_1 :
  RingHom.ker (F :=
      R →+* (i : (↑(zeroLocus (↑I : Set R)) : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
      (Pi.ringHom (f := fun (p : (↑(zeroLocus (↑I : Set R)) : Type u_1)) ↦
        Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal) fun (p : (↑(zeroLocus (↑I : Set R)) : Type u_1)) ↦
        algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)) ≤
    I
refine_2 :
  ∀ (x : R) (hx : x ∈ I),
    Membership.mem (γ := Submodule R R)
      (RingHom.ker (F :=
        R →+* (i : (↑(zeroLocus (↑I : Set R)) : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
        (Pi.ringHom (f := fun (p : (↑(zeroLocus (↑I : Set R)) : Type u_1)) ↦
          Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal) fun (p : (↑(zeroLocus (↑I : Set R)) : Type u_1)) ↦
          algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)))
      x
⊢ RingHom.ker (F :=
      R →+* (i : (↑(zeroLocus (↑I : Set R)) : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
      (Pi.ringHom (f := fun (p : (↑(zeroLocus (↑I : Set R)) : Type u_1)) ↦
        Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal) fun (p : (↑(zeroLocus (↑I : Set R)) : Type u_1)) ↦
        algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)) =
    I

Tactic:
refine le_antisymm ?_ fun x hx ↦ ?_

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.Pure
refine_1 :
  ⨅ (i : (↑(zeroLocus (↑I : Set R)) : Type u_1)),
      RingHom.ker (F := R →+* Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
        (algebraMap R (Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)) ≤
    I
⊢ RingHom.ker (F :=
      R →+* (i : (↑(zeroLocus (↑I : Set R)) : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
      (Pi.ringHom (f := fun (p : (↑(zeroLocus (↑I : Set R)) : Type u_1)) ↦
        Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal) fun (p : (↑(zeroLocus (↑I : Set R)) : Type u_1)) ↦
        algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)) ≤
    I

Tactic:
rw [Pi.ker_ringHom]

Premises used: Pi.ker_ringHom
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.Pure
⊢ ⨅ (i : (↑(zeroLocus (↑I : Set R)) : Type u_1)),
      RingHom.ker (F := R →+* Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
        (algebraMap R (Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)) ≤
    I

Tactic:
le_trans ?_ I.iInf_ker_le

Premises used: Ideal.iInf_ker_le, le_trans
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.Pure
refine_1 :
  LE.le.{u_1} (α := Ideal R)
    (⨅ (i : (↑(zeroLocus (↑I : Set R)) : Type u_1)),
      RingHom.ker (F := R →+* Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
        (algebraMap R (Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)))
    (⨅ (p : Ideal R),
      ⨅ (x : p.IsPrime),
        ⨅ (_ : I ≤ p), RingHom.ker (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)))
⊢ ⨅ (i : (↑(zeroLocus (↑I : Set R)) : Type u_1)),
      RingHom.ker (F := R →+* Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
        (algebraMap R (Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)) ≤
    I

Tactic:
refine le_trans ?_ I.iInf_ker_le

Premises used: Ideal.iInf_ker_le, le_trans
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.Pure
refine_1 :
  ∀ (i : Ideal R) (i_1 : i.IsPrime) (i_2 : I ≤ i),
    LE.le (α := Ideal R)
      (⨅ (i : (↑(zeroLocus (↑I : Set R)) : Type u_1)),
        RingHom.ker (F := R →+* Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
          (algebraMap R (Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)))
      (RingHom.ker (F := R →+* Localization.AtPrime i) (algebraMap R (Localization.AtPrime i)))
⊢ LE.le.{u_1} (α := Ideal R)
    (⨅ (i : (↑(zeroLocus (↑I : Set R)) : Type u_1)),
      RingHom.ker (F := R →+* Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
        (algebraMap R (Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)))
    (⨅ (p : Ideal R),
      ⨅ (x : p.IsPrime),
        ⨅ (_ : I ≤ p), RingHom.ker (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)))

Tactic:
simp only [le_iInf_iff]

Premises used: le_iInf_iff
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.Pure
⊢ ∀ (i : Ideal R) (i_1 : i.IsPrime) (i_2 : I ≤ i),
    LE.le (α := Ideal R)
      (⨅ (i : (↑(zeroLocus (↑I : Set R)) : Type u_1)),
        RingHom.ker (F := R →+* Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
          (algebraMap R (Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)))
      (RingHom.ker (F := R →+* Localization.AtPrime i) (algebraMap R (Localization.AtPrime i)))

Tactic:
fun i hi hle ↦ iInf_le_of_le ⟨⟨i, hi⟩, hle⟩ le_rfl

Premises used: PrimeSpectrum.mk, le_rfl, Set.Mem, Subtype.mk, iInf_le_of_le
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.Pure
⊢ ∀ (i : Ideal R) (i_1 : i.IsPrime) (i_2 : I ≤ i),
    LE.le (α := Ideal R)
      (⨅ (i : (↑(zeroLocus (↑I : Set R)) : Type u_1)),
        RingHom.ker (F := R →+* Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
          (algebraMap R (Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)))
      (RingHom.ker (F := R →+* Localization.AtPrime i) (algebraMap R (Localization.AtPrime i)))

Tactic:
exact fun i hi hle ↦ iInf_le_of_le ⟨⟨i, hi⟩, hle⟩ le_rfl

Premises used: le_rfl, iInf_le_of_le
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.Pure
x : R
hx : x ∈ I
refine_2 :
  ∀ (p : (↑(zeroLocus (↑I : Set R)) : Type u_1)),
    Eq (α := Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)
      ((Pi.ringHom (f := fun (p : (↑(zeroLocus (↑I : Set R)) : Type u_1)) ↦
              Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal) fun (p : (↑(zeroLocus (↑I : Set R)) : Type u_1)) ↦
              algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal) :
            (a : R) →
              (i : (↑(zeroLocus (↑I : Set R)) : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
          x p :
        Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)
      (0 p : Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)
⊢ Eq (α := (i : (↑(zeroLocus (↑I : Set R)) : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
    ((Pi.ringHom (f := fun (p : (↑(zeroLocus (↑I : Set R)) : Type u_1)) ↦
            Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal) fun (p : (↑(zeroLocus (↑I : Set R)) : Type u_1)) ↦
            algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal) :
          (a : R) → (i : (↑(zeroLocus (↑I : Set R)) : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
        x :
      (i : (↑(zeroLocus (↑I : Set R)) : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
    (0 : (i : (↑(zeroLocus (↑I : Set R)) : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)

Tactic:
ext p
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.Pure
x : R
hx : x ∈ I
p : (↑(zeroLocus (↑I : Set R)) : Type u_1)
⊢ Eq (α := Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)
    ((algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal) :
          (a : R) → Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)
        x :
      Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)
    (0 : Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)

Tactic:
Ideal.le_ker_atPrime_of_forall_exists_eq_mul
      (fun x hx ↦ Ideal.exists_eq_mul_of_pure hx) p.2 hx

Premises used: Ideal.exists_eq_mul_of_pure, Set.Mem, setOf, Set.preimage, Set.singleton, Ideal.le_ker_atPrime_of_forall_exists_eq_mul, Subtype.property
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.Pure
x : R
hx : x ∈ I
p : (↑(zeroLocus (↑I : Set R)) : Type u_1)
⊢ Eq (α := Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)
    ((algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal) :
          (a : R) → Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)
        x :
      Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)
    (0 : Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)

Tactic:
exact Ideal.le_ker_atPrime_of_forall_exists_eq_mul
      (fun x hx ↦ Ideal.exists_eq_mul_of_pure hx) p.2 hx

Premises used: Ideal.exists_eq_mul_of_pure, Ideal.le_ker_atPrime_of_forall_exists_eq_mul, Subtype.property
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.Pure
inst_2 : J.Pure
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R)) ↔ I = J

Tactic:
⟨fun h ↦ ?_, fun h ↦ h ▸ rfl⟩

Premises used: Eq.rec, Iff.intro, rfl
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.Pure
inst_2 : J.Pure
refine : ∀ (h : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R))), I = J
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R)) ↔ I = J

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h ▸ rfl⟩
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.Pure
inst_2 : J.Pure
h : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R))
rw :
  Eq (α := Ideal R)
    (RingHom.ker (F :=
      R →+* (i : (↑(zeroLocus (↑I : Set R)) : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
      (Pi.ringHom (f := fun (p : (↑(zeroLocus (↑I : Set R)) : Type u_1)) ↦
        Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal) fun (p : (↑(zeroLocus (↑I : Set R)) : Type u_1)) ↦
        algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)))
    (RingHom.ker (F :=
      R →+* (i : (↑(zeroLocus (↑J : Set R)) : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
      (Pi.ringHom (f := fun (p : (↑(zeroLocus (↑J : Set R)) : Type u_1)) ↦
        Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal) fun (p : (↑(zeroLocus (↑J : Set R)) : Type u_1)) ↦
        algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)))
⊢ I = J

Tactic:
rw [← I.ker_piRingHom_atPrime_eq_of_pure, ← J.ker_piRingHom_atPrime_eq_of_pure]

Premises used: Ideal.ker_piRingHom_atPrime_eq_of_pure
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.Pure
inst_2 : J.Pure
h : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R))
generalize :
  ∀ (s : Set (PrimeSpectrum R)) (hs : zeroLocus (↑I : Set R) = s),
    Eq (α := Ideal R)
      (RingHom.ker (F := R →+* (i : (↑s : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
        (Pi.ringHom (f := fun (p : (↑s : Type u_1)) ↦ Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)
          fun (p : (↑s : Type u_1)) ↦ algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)))
      (RingHom.ker (F :=
        R →+* (i : (↑(zeroLocus (↑J : Set R)) : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
        (Pi.ringHom (f := fun (p : (↑(zeroLocus (↑J : Set R)) : Type u_1)) ↦
          Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal) fun (p : (↑(zeroLocus (↑J : Set R)) : Type u_1)) ↦
          algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)))
⊢ Eq (α := Ideal R)
    (RingHom.ker (F :=
      R →+* (i : (↑(zeroLocus (↑I : Set R)) : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
      (Pi.ringHom (f := fun (p : (↑(zeroLocus (↑I : Set R)) : Type u_1)) ↦
        Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal) fun (p : (↑(zeroLocus (↑I : Set R)) : Type u_1)) ↦
        algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)))
    (RingHom.ker (F :=
      R →+* (i : (↑(zeroLocus (↑J : Set R)) : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
      (Pi.ringHom (f := fun (p : (↑(zeroLocus (↑J : Set R)) : Type u_1)) ↦
        Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal) fun (p : (↑(zeroLocus (↑J : Set R)) : Type u_1)) ↦
        algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)))

Tactic:
generalize hs : zeroLocus (I : Set R) = s

Premises used: PrimeSpectrum.zeroLocus, SetLike.coe
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.Pure
inst_2 : J.Pure
h : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R))
s : Set (PrimeSpectrum R)
hs : zeroLocus (↑I : Set R) = s
generalize :
  ∀ (t : Set (PrimeSpectrum R)) (ht : zeroLocus (↑J : Set R) = t),
    Eq (α := Ideal R)
      (RingHom.ker (F := R →+* (i : (↑s : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
        (Pi.ringHom (f := fun (p : (↑s : Type u_1)) ↦ Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)
          fun (p : (↑s : Type u_1)) ↦ algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)))
      (RingHom.ker (F := R →+* (i : (↑t : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
        (Pi.ringHom (f := fun (p : (↑t : Type u_1)) ↦ Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)
          fun (p : (↑t : Type u_1)) ↦ algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)))
⊢ Eq (α := Ideal R)
    (RingHom.ker (F := R →+* (i : (↑s : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
      (Pi.ringHom (f := fun (p : (↑s : Type u_1)) ↦ Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)
        fun (p : (↑s : Type u_1)) ↦ algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)))
    (RingHom.ker (F :=
      R →+* (i : (↑(zeroLocus (↑J : Set R)) : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
      (Pi.ringHom (f := fun (p : (↑(zeroLocus (↑J : Set R)) : Type u_1)) ↦
        Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal) fun (p : (↑(zeroLocus (↑J : Set R)) : Type u_1)) ↦
        algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)))

Tactic:
generalize ht : zeroLocus (J : Set R) = t

Premises used: PrimeSpectrum.zeroLocus, SetLike.coe
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.Pure
inst_2 : J.Pure
h : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R))
s : Set (PrimeSpectrum R)
hs : zeroLocus (↑I : Set R) = s
t : Set (PrimeSpectrum R)
ht : zeroLocus (↑J : Set R) = t
rw : zeroLocus (↑I : Set R) = t
rw₁ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R))
rw₂ rw₃ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑J : Set R)) (zeroLocus (↑J : Set R))
⊢ s = t

Tactic:
rw [← hs, ← ht, h]
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.Pure
inst_2 : J.Pure
h : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R))
s : Set (PrimeSpectrum R)
hs : zeroLocus (↑I : Set R) = s
t : Set (PrimeSpectrum R)
ht : zeroLocus (↑J : Set R) = t
obtain :
  ∀ (ht : zeroLocus (↑J : Set R) = s),
    Eq (α := Ideal R)
      (RingHom.ker (F := R →+* (i : (↑s : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
        (Pi.ringHom (f := fun (p : (↑s : Type u_1)) ↦ Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)
          fun (p : (↑s : Type u_1)) ↦ algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)))
      (RingHom.ker (F := R →+* (i : (↑s : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
        (Pi.ringHom (f := fun (p : (↑s : Type u_1)) ↦ Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)
          fun (p : (↑s : Type u_1)) ↦ algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)))
⊢ Eq (α := Ideal R)
    (RingHom.ker (F := R →+* (i : (↑s : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
      (Pi.ringHom (f := fun (p : (↑s : Type u_1)) ↦ Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)
        fun (p : (↑s : Type u_1)) ↦ algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)))
    (RingHom.ker (F := R →+* (i : (↑t : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
      (Pi.ringHom (f := fun (p : (↑t : Type u_1)) ↦ Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)
        fun (p : (↑t : Type u_1)) ↦ algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)))

Tactic:
obtain rfl : s = t := by rw [← hs, ← ht, h]

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.Pure
inst_2 : J.Pure
h : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R))
s : Set (PrimeSpectrum R)
hs : zeroLocus (↑I : Set R) = s
ht : zeroLocus (↑J : Set R) = s
⊢ Eq (α := Ideal R)
    (RingHom.ker (F := R →+* (i : (↑s : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
      (Pi.ringHom (f := fun (p : (↑s : Type u_1)) ↦ Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)
        fun (p : (↑s : Type u_1)) ↦ algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)))
    (RingHom.ker (F := R →+* (i : (↑s : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
      (Pi.ringHom (f := fun (p : (↑s : Type u_1)) ↦ Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)
        fun (p : (↑s : Type u_1)) ↦ algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
R : Type u_3
inst : Ring R
f : ι → R
inst_1 : IsTwoSided (span (range f))
i : ι
rw : Membership.mem (γ := Ideal R) (span (range f)) (f i)
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (span (range f)))
    ((mk (span (range f)) : (a : R) → R ⧸ span (range f)) (f i) :
      HasQuotient.Quotient R (B := Ideal R) (span (range f)))
    (0 : HasQuotient.Quotient R (B := Ideal R) (span (range f)))

Tactic:
rw [Ideal.Quotient.eq_zero_iff_mem]

Premises used: Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
R : Type u_3
inst : Ring R
f : ι → R
inst_1 : IsTwoSided (span (range f))
i : ι
⊢ Membership.mem (γ := Ideal R) (span (range f)) (f i)

Tactic:
Ideal.subset_span ⟨i, rfl⟩

Premises used: Ideal.subset_span, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
R : Type u_3
inst : Ring R
f : ι → R
inst_1 : IsTwoSided (span (range f))
i : ι
⊢ Membership.mem (γ := Ideal R) (span (range f)) (f i)

Tactic:
exact Ideal.subset_span ⟨i, rfl⟩
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
⊢ Eq.{u_3 + 1} (α := R ⧸ I) 0 1 ↔ I = ⊤

Tactic:
eq_comm.trans <| (Submodule.Quotient.mk_eq_zero _).trans (eq_top_iff_one _).symm

Premises used: eq_comm, Ideal.eq_top_iff_one, Iff.trans, Iff.symm, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
⊢ Ne.{u_3 + 1} (α := R ⧸ I) 0 1 ↔ I ≠ ⊤

Tactic:
not_congr zero_eq_one_iff

Premises used: Ideal.Quotient.zero_eq_one_iff, not_congr
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
⊢ Subsingleton.{u_3 + 1} (R ⧸ I) ↔ I = ⊤

Tactic:
Submodule.Quotient.subsingleton_iff

Premises used: Submodule.Quotient.subsingleton_iff
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
⊢ Nontrivial.{u_3} (R ⧸ I) ↔ I ≠ ⊤

Tactic:
Submodule.Quotient.nontrivial_iff

Premises used: Submodule.Quotient.nontrivial_iff
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a b x_1 y : R
a_1 : HasQuotient.Quotient R (B := Ideal R) ⊤
x : R
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) ⊤) (Quot.mk (⇑(Submodule.quotientRel ⊤) : R → R → Prop) x) default

Tactic:
Quotient.eq_zero_iff_mem.mpr Submodule.mem_top

Premises used: Iff.mpr, Submodule.Quotient.mk, Ideal.Quotient.eq_zero_iff_mem, Submodule.mem_top
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a b x_1 y : R
a_1 : HasQuotient.Quotient R (B := Ideal R) ⊤
x : R
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) ⊤) (Quot.mk (⇑(Submodule.quotientRel ⊤) : R → R → Prop) x) default

Tactic:
exact Quotient.eq_zero_iff_mem.mpr Submodule.mem_top

Premises used: Iff.mpr, Ideal.Quotient.eq_zero_iff_mem, Submodule.mem_top
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a b x y : R
inst_1 : I.IsTwoSided
α : Type u_5
inst_2 : SMul α R
inst_3 : IsScalarTower α R R
⊢ IsScalarTower.{u_5, u_3, u_3} α (R ⧸ I) (R ⧸ I)

Tactic:
(Quotient.ringCon I).isScalarTower_right

Premises used: RingCon.isScalarTower_right, RingCon.Quotient, Ideal.Quotient.ringCon, Submodule.quotientRel, AddAction.orbitRel
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a b x y : R
inst_1 : I.IsTwoSided
α : Type u_5
inst_2 : SMul α R
inst_3 : IsScalarTower α R R
inst_4 : SMulCommClass α R R
⊢ SMulCommClass.{u_5, u_3, u_3} α (R ⧸ I) (R ⧸ I)

Tactic:
(Quotient.ringCon I).smulCommClass

Premises used: RingCon.smulCommClass, RingCon.Quotient, Ideal.Quotient.ringCon, Submodule.quotientRel, AddAction.orbitRel
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a b x y : R
inst_1 : I.IsTwoSided
α : Type u_5
inst_2 : SMul α R
inst_3 : IsScalarTower α R R
inst_4 : SMulCommClass R α R
⊢ SMulCommClass.{u_3, u_5, u_3} (R ⧸ I) α (R ⧸ I)

Tactic:
(Quotient.ringCon I).smulCommClass'

Premises used: RingCon.Quotient, RingCon.smulCommClass', Ideal.Quotient.ringCon, Submodule.quotientRel, AddAction.orbitRel