awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
f : ↥J ⧸ HSMul.hSMul (β := Submodule R ↥J) I ⊤ →ₗ[R] R ⧸ I :=
  (HSMul.hSMul (β := Submodule R ↥J) I ⊤).mapQ I (Submodule.subtype J) ⋯
x : R ⧸ I
x_1 : ↥J
⊢ Eq (α := (R ⧸ I) ⊗[R] R)
    (((((AlgebraTensorModule.curry (LinearMap.lTensor (R ⧸ I) (Submodule.subtype J)) :
                  R ⧸ I →ₗ[R] ↥J →ₗ[R] (R ⧸ I) ⊗[R] R) :
                (a : R ⧸ I) → ↥J →ₗ[R] (R ⧸ I) ⊗[R] R)
              x :
            ↥J →ₗ[R] (R ⧸ I) ⊗[R] R) :
          (a : ↥J) → (R ⧸ I) ⊗[R] R)
        x_1 :
      (R ⧸ I) ⊗[R] R)
    (((((AlgebraTensorModule.curry
                    ((↑(LinearEquiv.symm (TensorProduct.rid R (R ⧸ I))) : R ⧸ I →ₗ[R] (R ⧸ I) ⊗[R] R) ∘ₗ
                      f ∘ₗ (↑(quotTensorEquivQuotSMul (↥J) I) : (R ⧸ I) ⊗[R] ↥J →ₗ[R] ↥J ⧸ I • ⊤)) :
                  R ⧸ I →ₗ[R] ↥J →ₗ[R] (R ⧸ I) ⊗[R] R) :
                (a : R ⧸ I) → ↥J →ₗ[R] (R ⧸ I) ⊗[R] R)
              x :
            ↥J →ₗ[R] (R ⧸ I) ⊗[R] R) :
          (a : ↥J) → (R ⧸ I) ⊗[R] R)
        x_1 :
      (R ⧸ I) ⊗[R] R)
have a : Eq (α := (R ⧸ I) ⊗[R] R) (x ⊗ₜ[R] (↑x_1 : R))
  (((HSMul.hSMul (β := Submodule R ↥J) I ⊤).mapQ I (Submodule.subtype J) sorry : (a : ↥J ⧸ I • ⊤) → R ⧸ I)
      (((quotTensorEquivQuotSMul (↥J) I : (R ⧸ I) ⊗[R] ↥J ≃ₗ[R] ↥J ⧸ HSMul.hSMul (β := Submodule R ↥J) I ⊤) :
          (a : (R ⧸ I) ⊗[R] ↥J) → ↥J ⧸ I • ⊤)
        (x ⊗ₜ[R] x_1)) ⊗ₜ[R]
    1)
Tactic: simp [f, ← Ideal.Quotient.algebraMap_eq, Algebra.TensorProduct.tmul_one_eq_one_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
f : ↥J ⧸ HSMul.hSMul (β := Submodule R ↥J) I ⊤ →ₗ[R] R ⧸ I :=
  (HSMul.hSMul (β := Submodule R ↥J) I ⊤).mapQ I (Submodule.subtype J) ⋯
⊢ Function.Injective (α := (R ⧸ I) ⊗[R] ↥J) (β := (R ⧸ I) ⊗[R] R)
      (⇑(LinearMap.lTensor (R ⧸ I) (Submodule.subtype J)) : (a : (R ⧸ I) ⊗[R] ↥J) → (R ⧸ I) ⊗[R] R) ↔
    I ⊓ J = I * J
have this : LinearMap.lTensor (R ⧸ I) (Submodule.subtype J) =
  (↑(LinearEquiv.symm (TensorProduct.rid R (R ⧸ I))) : R ⧸ I →ₗ[R] (R ⧸ I) ⊗[R] R) ∘ₗ
    f ∘ₗ (↑(quotTensorEquivQuotSMul (↥J) I) : (R ⧸ I) ⊗[R] ↥J →ₗ[R] ↥J ⧸ I • ⊤)
Tactic: have : J.subtype.lTensor (R ⧸ I) =
      (TensorProduct.rid R (R ⧸ I)).symm ∘ₗ f ∘ₗ TensorProduct.quotTensorEquivQuotSMul J I := by
    ext
    simp [f, ← Ideal.Quotient.algebraMap_eq, Algebra.TensorProduct.tmul_one_eq_one_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
f : ↥J ⧸ HSMul.hSMul (β := Submodule R ↥J) I ⊤ →ₗ[R] R ⧸ I :=
  (HSMul.hSMul (β := Submodule R ↥J) I ⊤).mapQ I (Submodule.subtype J) ⋯
this :
  LinearMap.lTensor (R ⧸ I) (Submodule.subtype J) =
    (↑(LinearEquiv.symm (TensorProduct.rid R (R ⧸ I))) : R ⧸ I →ₗ[R] (R ⧸ I) ⊗[R] R) ∘ₗ
      f ∘ₗ (↑(quotTensorEquivQuotSMul (↥J) I) : (R ⧸ I) ⊗[R] ↥J →ₗ[R] ↥J ⧸ I • ⊤)
⊢ Function.Injective (α := (R ⧸ I) ⊗[R] ↥J) (β := (R ⧸ I) ⊗[R] R)
      (⇑(LinearMap.lTensor (R ⧸ I) (Submodule.subtype J)) : (a : (R ⧸ I) ⊗[R] ↥J) → (R ⧸ I) ⊗[R] R) ↔
    I ⊓ J = I * J
have rw : Function.Injective (α := (R ⧸ I) ⊗[R] ↥J) (β := (R ⧸ I) ⊗[R] R)
    (⇑((↑(LinearEquiv.symm (TensorProduct.rid R (R ⧸ I))) : R ⧸ I →ₗ[R] (R ⧸ I) ⊗[R] R) ∘ₗ
          f ∘ₗ (↑(quotTensorEquivQuotSMul (↥J) I) : (R ⧸ I) ⊗[R] ↥J →ₗ[R] ↥J ⧸ I • ⊤)) :
      (a : (R ⧸ I) ⊗[R] ↥J) → (R ⧸ I) ⊗[R] R) ↔
  I ⊓ J = I * J
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
f : ↥J ⧸ HSMul.hSMul (β := Submodule R ↥J) I ⊤ →ₗ[R] R ⧸ I :=
  (HSMul.hSMul (β := Submodule R ↥J) I ⊤).mapQ I (Submodule.subtype J) ⋯
this :
  LinearMap.lTensor (R ⧸ I) (Submodule.subtype J) =
    (↑(LinearEquiv.symm (TensorProduct.rid R (R ⧸ I))) : R ⧸ I →ₗ[R] (R ⧸ I) ⊗[R] R) ∘ₗ
      f ∘ₗ (↑(quotTensorEquivQuotSMul (↥J) I) : (R ⧸ I) ⊗[R] ↥J →ₗ[R] ↥J ⧸ I • ⊤)
⊢ Function.Injective (α := (R ⧸ I) ⊗[R] ↥J) (β := (R ⧸ I) ⊗[R] R)
      (⇑((↑(LinearEquiv.symm (TensorProduct.rid R (R ⧸ I))) : R ⧸ I →ₗ[R] (R ⧸ I) ⊗[R] R) ∘ₗ
            f ∘ₗ (↑(quotTensorEquivQuotSMul (↥J) I) : (R ⧸ I) ⊗[R] ↥J →ₗ[R] ↥J ⧸ I • ⊤)) :
        (a : (R ⧸ I) ⊗[R] ↥J) → (R ⧸ I) ⊗[R] R) ↔
    I ⊓ J = I * J
have simp : Submodule.map (Submodule.subtype J) (Submodule.comap (Submodule.subtype J) I) ≤
    Submodule.map (Submodule.subtype J) (HSMul.hSMul (β := Submodule R ↥J) I ⊤) ↔
  I ⊓ J = I * J
Tactic: simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, EmbeddingLike.comp_injective,
    EquivLike.injective_comp, ← LinearMap.ker_eq_bot, f, Submodule.ker_mapQ,
    ← LinearMap.le_ker_iff_map, Submodule.ker_mkQ,
    ← (Submodule.map_le_map_iff_of_injective J.injective_subtype)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.Pure
⊢ I ⊓ J = I * J
have rw : Function.Injective (α := (R ⧸ I) ⊗[R] ↥J) (β := (R ⧸ I) ⊗[R] R)
  (⇑(LinearMap.lTensor (R ⧸ I) (Submodule.subtype J)) : (a : (R ⧸ I) ⊗[R] ↥J) → (R ⧸ I) ⊗[R] R)
Tactic: rw [← injective_lTensor_quotient_iff_inf_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.Pure
⊢ Function.Injective (α := (R ⧸ I) ⊗[R] ↥J) (β := (R ⧸ I) ⊗[R] R)
    (⇑(LinearMap.lTensor (R ⧸ I) (Submodule.subtype J)) : (a : (R ⧸ I) ⊗[R] ↥J) → (R ⧸ I) ⊗[R] R)
have hf : Function.Injective (α := ↥J) (β := R) (⇑(Submodule.subtype J) : (a : ↥J) → R)
Tactic: apply Module.Flat.lTensor_preserves_injective_linearMap
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I.FG
h' : IsIdempotentElem I
⊢ I.Pure
have h'₁ : ∃ (e : R), IsIdempotentElem e ∧ I = R ∙ e
Tactic: rw [Ideal.isIdempotentElem_iff_of_fg _ h] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I.FG
h' : ∃ (e : R), IsIdempotentElem e ∧ I = R ∙ e
⊢ I.Pure
have obtain : ∀ (e : R) (he : IsIdempotentElem e) (h : FG (R ∙ e)), Pure (R ∙ e)
Tactic: obtain ⟨e, he, rfl⟩ := h'
Cleared hypotheses: I, h, h'
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
h : FG (R ∙ e)
⊢ Pure (R ∙ e)
have this : Module.Flat R
  (HasQuotient.Quotient R (B := Submodule R R) (R ∙ e) × HasQuotient.Quotient R (B := Ideal R) (span {1 - e}))
Tactic: have : Module.Flat R ((R ⧸ R ∙ e) × R ⧸ span {1 - e}) :=
    .of_linearEquiv <| AlgEquiv.prodQuotientOfIsIdempotentElem R he he.one_sub (by simp)
      (by grind [IsIdempotentElem]) |>.toLinearEquiv.symm
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
h : FG (R ∙ e)
this :
  Module.Flat R
    (HasQuotient.Quotient R (B := Submodule R R) (R ∙ e) × HasQuotient.Quotient R (B := Ideal R) (span {1 - e}))
⊢ Pure (R ∙ e)
have apply : Eq (α := HasQuotient.Quotient R (B := Ideal R) (R ∙ e) →ₗ[R] HasQuotient.Quotient R (B := Ideal R) (R ∙ e))
  (LinearMap.fst R (HasQuotient.Quotient R (B := Ideal R) (R ∙ e))
      (HasQuotient.Quotient R (B := Ideal R) (span {1 - e})) ∘ₗ
    LinearMap.inl R (HasQuotient.Quotient R (B := Ideal R) (R ∙ e))
      (HasQuotient.Quotient R (B := Ideal R) (span {1 - e})))
  LinearMap.id
Tactic: apply Module.Flat.of_retract (LinearMap.inl R _ (R ⧸ span {1 - e})) (LinearMap.fst R _ _)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
H : ∀ ⦃J : Ideal R⦄, J.FG → I ⊓ J = I * J
⊢ I.Pure
have rw : ∀ ⦃I_1 : Ideal R⦄,
  I_1.FG →
    Function.Injective (α := (R ⧸ I) ⊗[R] ↥I_1) (β := (R ⧸ I) ⊗[R] R)
      (⇑(LinearMap.lTensor (R ⧸ I) (Submodule.subtype I_1)) : (a : (R ⧸ I) ⊗[R] ↥I_1) → (R ⧸ I) ⊗[R] R)
Tactic: rw [Pure, Module.Flat.iff_lTensor_injective]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
H : ∀ ⦃J : Ideal R⦄, J.FG → I ⊓ J = I * J
J : Ideal R
hJ : J.FG
⊢ Function.Injective (α := (R ⧸ I) ⊗[R] ↥J) (β := (R ⧸ I) ⊗[R] R)
    (⇑(LinearMap.lTensor (R ⧸ I) (Submodule.subtype J)) : (a : (R ⧸ I) ⊗[R] ↥J) → (R ⧸ I) ⊗[R] R)
have rw : I ⊓ J = I * J
Tactic: rw [injective_lTensor_quotient_iff_inf_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.Pure
x : R
hx : x ∈ I
h : x ∈ I * span {x}
⊢ ∃ y ∈ I, x = x * y
have h₁ : ∃ z ∈ I, z * x = x
Tactic: rw [Ideal.mem_mul_span_singleton] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.Pure
x : R
hx : x ∈ I
⊢ ∃ y ∈ I, x = x * y
have suffices : x ∈ I * span {x}
Tactic: suffices h : x ∈ I * Ideal.span {x} by
    rw [Ideal.mem_mul_span_singleton] at h
    grind
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.Pure
x : R
hx : x ∈ I
⊢ x ∈ I * span {x}
have rw : x ∈ I ⊓ span {x}
Tactic: rw [← I.inf_eq_mul_of_pure]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
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
⊢ Membership.mem (γ := Submodule R R)
    (RingHom.ker (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p))) x
have obtain : ∀ (y : R) (hy : y ∈ I) (heq : x = x * y),
  Membership.mem (γ := Submodule R R)
    (RingHom.ker (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p))) x
Tactic: obtain ⟨y, hy, heq⟩ := h _ hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
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
⊢ IsUnit (M := Localization.AtPrime p)
    ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (1 - y) : Localization.AtPrime p)
have rw : ∃ m ∈ p.primeCompl, 1 - y ∣ m
Tactic: rw [IsLocalization.algebraMap_isUnit_iff p.primeCompl]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
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
⊢ ∃ m ∈ p.primeCompl, 1 - y ∣ m
have refine : ∀ (hz : 1 - y ∈ (↑p : Set R)), 1 ∈ p
Tactic: refine ⟨1 - y, fun hz ↦ p.one_notMem ?_, by simp⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
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
hz : 1 - y ∈ (↑p : Set R)
⊢ 1 ∈ p
have rw : 1 - y + y ∈ p
Tactic: rw [← sub_add_cancel 1 y]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (hypothesis)
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
⊢ Membership.mem (γ := Submodule R R)
    (RingHom.ker (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p))) x
have this : IsUnit (M := Localization.AtPrime p)
  ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (1 - y) : Localization.AtPrime p)
Tactic: have : IsUnit (algebraMap R (Localization.AtPrime p) (1 - y)) := by
    rw [IsLocalization.algebraMap_isUnit_iff p.primeCompl]
    refine ⟨1 - y, fun hz ↦ p.one_notMem ?_, by simp⟩
    rw [← sub_add_cancel 1 y]
    exact Ideal.add_mem _ hz (hle hy)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (hypothesis)
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)
⊢ Membership.mem (γ := Submodule R R)
    (RingHom.ker (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p))) x
have hzero : x * (1 - y) = 0
Tactic: have hzero : x * (1 - y) = 0 := by simp [mul_sub, ← heq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
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
have 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
Tactic: refine le_antisymm ?_ fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
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
⊢ 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
have 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
Tactic: refine le_antisymm ?_ fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
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
have 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
Tactic: rw [Pi.ker_ringHom]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
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
have 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)))
Tactic: refine le_trans ?_ I.iInf_ker_le
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.Pure
⊢ 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)))
have 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)))
Tactic: simp only [le_iInf_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.Pure
x : R
hx : x ∈ I
⊢ 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)
have 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)
Tactic: ext p
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
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
have refine : ∀ (h : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R))), I = J
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h ▸ rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
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))
⊢ I = J
have 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)))
Tactic: rw [← I.ker_piRingHom_atPrime_eq_of_pure, ← J.ker_piRingHom_atPrime_eq_of_pure]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
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))
⊢ 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)))
have 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)))
Tactic: generalize hs : zeroLocus (I : Set R) = s
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
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
⊢ 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)))
have 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)))
Tactic: generalize ht : zeroLocus (J : Set R) = t