awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.TensorProduct (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g p₂.asIdeal
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
h₁ : HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∈ p₁.asIdeal
h₂ : HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∉ p₂.asIdeal
h₄ : a ∉ Ideal.comap (F := S →+* S ⊗[R] T) (algebraMap S (S ⊗[R] T)) p₂.asIdeal
h₃ : t ∉ Ideal.comap g p₁.asIdeal
⊢ False
have h₅ : a ∉ Ideal.comap (F := S →+* S ⊗[R] T) (algebraMap S (S ⊗[R] T)) p₁.asIdeal
Tactic: replace h₄ : a ∉ p₁.asIdeal.comap (algebraMap S (S ⊗[R] T)) := by
    rwa [show p₁.asIdeal.comap (algebraMap S (S ⊗[R] T)) = p₂.asIdeal.comap _ from congr($h.1.1)]
Cleared hypotheses: h₄
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
⊢ IsEmbedding (X := PrimeSpectrum (S ⊗[R] T)) (tensorProductTo R S T)
have refine : IsInducing (X := PrimeSpectrum (S ⊗[R] T)) (tensorProductTo R S T)
Tactic: refine ⟨?_, fun p₁ p₂ e ↦
    (isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux R S T hRT p₁ p₂ e).antisymm
      (isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux R S T hRT p₂ p₁ e.symm)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
⊢ IsInducing (X := PrimeSpectrum (S ⊗[R] T)) (tensorProductTo R S T)
have refine : ∀ (U : TopologicalSpace.Opens (PrimeSpectrum (S ⊗[R] T))),
  Membership.mem (γ := Set (TopologicalSpace.Opens (PrimeSpectrum (S ⊗[R] T)))) (Set.range basicOpen) U →
    IsOpen[TopologicalSpace.induced (tensorProductTo R S T) instTopologicalSpaceProd]
      (↑U : Set (PrimeSpectrum (S ⊗[R] T)))
Tactic: refine ⟨(continuous_tensorProductTo ..).le_induced.antisymm (isBasis_basic_opens.le_iff.mpr ?_)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : S ⊗[R] T
⊢ IsOpen[TopologicalSpace.induced (tensorProductTo R S T) instTopologicalSpaceProd]
    (↑(basicOpen f) : Set (PrimeSpectrum (S ⊗[R] T)))
have rw : ∀ x ∈ (↑(basicOpen f) : Set (PrimeSpectrum (S ⊗[R] T))),
  ∃ t ⊆ (↑(basicOpen f) : Set (PrimeSpectrum (S ⊗[R] T))),
    IsOpen[TopologicalSpace.induced (tensorProductTo R S T) instTopologicalSpaceProd] t ∧ x ∈ t
Tactic: rw [@isOpen_iff_forall_mem_open]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
⊢ ∃ t ⊆ (↑(basicOpen f) : Set (PrimeSpectrum (S ⊗[R] T))),
    IsOpen[TopologicalSpace.induced (tensorProductTo R S T) instTopologicalSpaceProd] t ∧ J ∈ t
have obtain : ∀ (t : T) (r : R) (a : S) (ht : r • t ∉ Ideal.comap g J.asIdeal) (e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t),
  ∃ t ⊆ (↑(basicOpen f) : Set (PrimeSpectrum (S ⊗[R] T))),
    IsOpen[TopologicalSpace.induced (tensorProductTo R S T) instTopologicalSpaceProd] t ∧ J ∈ t
Tactic: obtain ⟨t, r, a, ht, e⟩ := hRT.exists_mul_eq_tmul f
    (J.asIdeal.comap g) inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
⊢ ∃ t ⊆ (↑(basicOpen f) : Set (PrimeSpectrum (S ⊗[R] T))),
    IsOpen[TopologicalSpace.induced (tensorProductTo R S T) instTopologicalSpaceProd] t ∧ J ∈ t
have refine_1 : tensorProductTo R S T ⁻¹'
    SProd.sprod (α := Set (PrimeSpectrum S)) (β := Set (PrimeSpectrum T)) (TopologicalSpace.Opens.carrier (basicOpen a))
      (TopologicalSpace.Opens.carrier (basicOpen t)) ⊆
  (↑(basicOpen f) : Set (PrimeSpectrum (S ⊗[R] T)))
Tactic: refine ⟨_, ?_, ⟨_, (basicOpen a).2.prod (basicOpen t).2, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
refine_1 :
  tensorProductTo R S T ⁻¹'
      SProd.sprod (α := Set (PrimeSpectrum S)) (β := Set (PrimeSpectrum T))
        (TopologicalSpace.Opens.carrier (basicOpen a)) (TopologicalSpace.Opens.carrier (basicOpen t)) ⊆
    (↑(basicOpen f) : Set (PrimeSpectrum (S ⊗[R] T)))
⊢ ∃ t ⊆ (↑(basicOpen f) : Set (PrimeSpectrum (S ⊗[R] T))),
    IsOpen[TopologicalSpace.induced (tensorProductTo R S T) instTopologicalSpaceProd] t ∧ J ∈ t
have refine_2 : Membership.mem (γ := Set (PrimeSpectrum (S ⊗[R] T)))
  (tensorProductTo R S T ⁻¹'
    SProd.sprod (α := Set (PrimeSpectrum S)) (β := Set (PrimeSpectrum T)) (TopologicalSpace.Opens.carrier (basicOpen a))
      (TopologicalSpace.Opens.carrier (basicOpen t)))
  J
Tactic: refine ⟨_, ?_, ⟨_, (basicOpen a).2.prod (basicOpen t).2, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
x : PrimeSpectrum (S ⊗[R] T)
hx₁ : a ⊗ₜ[R] 1 ∉ x.asIdeal
hx₂ : 1 ⊗ₜ[R] t ∉ x.asIdeal
hx₃ : f ∈ x.asIdeal
⊢ False
have refine_1 : HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∈ (↑x.asIdeal : Set (S ⊗[R] T))
Tactic: apply x.asIdeal.primeCompl.mul_mem hx₁ hx₂
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
x : PrimeSpectrum (S ⊗[R] T)
hx₁ : a ⊗ₜ[R] 1 ∉ x.asIdeal
hx₂ : 1 ⊗ₜ[R] t ∉ x.asIdeal
hx₃ : f ∈ x.asIdeal
⊢ HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∈ (↑x.asIdeal : Set (S ⊗[R] T))
have refine_1 : 1 ⊗ₜ[R] (r • t) * f ∈ (↑x.asIdeal : Set (S ⊗[R] T))
Tactic: rw [Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul, ← e]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
⊢ HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∉ J.asIdeal
have rw : 1 ⊗ₜ[R] (r • t) * f ∉ J.asIdeal
Tactic: rw [Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul, ← e]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.TensorProduct (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
⊢ Membership.mem (γ := Set (PrimeSpectrum (S ⊗[R] T)))
    (tensorProductTo R S T ⁻¹'
      SProd.sprod (α := Set (PrimeSpectrum S)) (β := Set (PrimeSpectrum T))
        (TopologicalSpace.Opens.carrier (basicOpen a)) (TopologicalSpace.Opens.carrier (basicOpen t)))
    J
have this : HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∉ J.asIdeal
Tactic: have : a ⊗ₜ[R] (1 : T) * (1 : S) ⊗ₜ[R] t ∉ J.asIdeal := by
      rw [Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul, ← e]
      exact J.asIdeal.primeCompl.mul_mem ht hJ
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
this : HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∉ J.asIdeal
⊢ Membership.mem (γ := Set (PrimeSpectrum (S ⊗[R] T)))
    (tensorProductTo R S T ⁻¹'
      SProd.sprod (α := Set (PrimeSpectrum S)) (β := Set (PrimeSpectrum T))
        (TopologicalSpace.Opens.carrier (basicOpen a)) (TopologicalSpace.Opens.carrier (basicOpen t)))
    J
have refine_2 : ∀ (this : ¬(a ⊗ₜ[R] 1 ∈ J.asIdeal ∨ 1 ⊗ₜ[R] t ∈ J.asIdeal)),
  Membership.mem (γ := Set (PrimeSpectrum (S ⊗[R] T)))
    (tensorProductTo R S T ⁻¹'
      SProd.sprod (α := Set (PrimeSpectrum S)) (β := Set (PrimeSpectrum T))
        (TopologicalSpace.Opens.carrier (basicOpen a)) (TopologicalSpace.Opens.carrier (basicOpen t)))
    J
Tactic: rwa [J.isPrime.mul_mem_iff_mem_or_mem.not, not_or] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
this : HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∉ J.asIdeal
refine_2 :
  ∀ (this : ¬(a ⊗ₜ[R] 1 ∈ J.asIdeal ∨ 1 ⊗ₜ[R] t ∈ J.asIdeal)),
    Membership.mem (γ := Set (PrimeSpectrum (S ⊗[R] T)))
      (tensorProductTo R S T ⁻¹'
        SProd.sprod (α := Set (PrimeSpectrum S)) (β := Set (PrimeSpectrum T))
          (TopologicalSpace.Opens.carrier (basicOpen a)) (TopologicalSpace.Opens.carrier (basicOpen t)))
      J
⊢ Membership.mem (γ := Set (PrimeSpectrum (S ⊗[R] T)))
    (tensorProductTo R S T ⁻¹'
      SProd.sprod (α := Set (PrimeSpectrum S)) (β := Set (PrimeSpectrum T))
        (TopologicalSpace.Opens.carrier (basicOpen a)) (TopologicalSpace.Opens.carrier (basicOpen t)))
    J
have refine_2₁ : ∀ (this : a ⊗ₜ[R] 1 ∉ J.asIdeal ∧ 1 ⊗ₜ[R] t ∉ J.asIdeal),
  Membership.mem (γ := Set (PrimeSpectrum (S ⊗[R] T)))
    (tensorProductTo R S T ⁻¹'
      SProd.sprod (α := Set (PrimeSpectrum S)) (β := Set (PrimeSpectrum T))
        (TopologicalSpace.Opens.carrier (basicOpen a)) (TopologicalSpace.Opens.carrier (basicOpen t)))
    J
Tactic: rwa [J.isPrime.mul_mem_iff_mem_or_mem.not, not_or] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
Zs : Set (Set (PrimeSpectrum R))
h : Zs ⊆ Set.range zeroLocus
⊢ Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range zeroLocus) (⋂₀ Zs)
have rw : Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range zeroLocus)
  (⋂ (i : (↑Zs : Type u)), (↑i : Set (PrimeSpectrum R)))
Tactic: rw [Set.sInter_eq_iInter]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
Zs : Set (Set (PrimeSpectrum R))
h : Zs ⊆ Set.range zeroLocus
⊢ Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range zeroLocus)
    (⋂ (i : (↑Zs : Type u)), (↑i : Set (PrimeSpectrum R)))
have choose : ∀ (f : (i : (↑Zs : Type u)) → Set R) (hf : ∀ (i : (↑Zs : Type u)), zeroLocus (f i) = (↑i : Set (PrimeSpectrum R))),
  Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range zeroLocus)
    (⋂ (i : (↑Zs : Type u)), (↑i : Set (PrimeSpectrum R)))
Tactic: choose f hf using fun i : Zs => h i.prop
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
Zs : Set (Set (PrimeSpectrum R))
h : Zs ⊆ Set.range zeroLocus
f : (i : (↑Zs : Type u)) → Set R
hf : ∀ (i : (↑Zs : Type u)), zeroLocus (f i) = (↑i : Set (PrimeSpectrum R))
⊢ Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range zeroLocus)
    (⋂ (i : (↑Zs : Type u)), (↑i : Set (PrimeSpectrum R)))
have simp : Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range zeroLocus) (⋂ (i : (↑Zs : Type u)), zeroLocus (f i))
Tactic: simp only [← hf]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
U : Set (PrimeSpectrum R)
⊢ IsOpen U ↔ ∃ (s : Set R), Uᶜ = zeroLocus s
have simp : IsOpen U ↔ ∃ (s : Set R), zeroLocus s = Uᶜ
Tactic: simp only [@eq_comm _ Uᶜ]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
Z : Set (PrimeSpectrum R)
⊢ IsClosed Z ↔ ∃ (s : Set R), Z = zeroLocus s
have rw : IsOpen Zᶜ ↔ ∃ (s : Set R), Z = zeroLocus s
Tactic: rw [← isOpen_compl_iff, isOpen_iff, compl_compl]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
Z : Set (PrimeSpectrum R)
rw : IsOpen Zᶜ ↔ ∃ (s : Set R), Z = zeroLocus s
⊢ IsClosed Z ↔ ∃ (s : Set R), Z = zeroLocus s
have rw₁ : (∃ (s : Set R), Zᶜᶜ = zeroLocus s) ↔ ∃ (s : Set R), Z = zeroLocus s
Tactic: rw [← isOpen_compl_iff, isOpen_iff, compl_compl]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
Z : Set (PrimeSpectrum R)
rw : IsOpen Zᶜ ↔ ∃ (s : Set R), Z = zeroLocus s
rw₁ : (∃ (s : Set R), Zᶜᶜ = zeroLocus s) ↔ ∃ (s : Set R), Z = zeroLocus s
⊢ IsClosed Z ↔ ∃ (s : Set R), Z = zeroLocus s
have rw₂ : (∃ (s : Set R), Z = zeroLocus s) ↔ ∃ (s : Set R), Z = zeroLocus s
Tactic: rw [← isOpen_compl_iff, isOpen_iff, compl_compl]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Set R
⊢ IsClosed (X := PrimeSpectrum R) (zeroLocus s)
have rw : ∃ (s_1 : Set R), Eq (α := Set (PrimeSpectrum R)) (zeroLocus s) (zeroLocus s_1)
Tactic: rw [isClosed_iff_zeroLocus]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
t : Set (PrimeSpectrum R)
⊢ zeroLocus (↑(vanishingIdeal t) : Set R) = closure t
have rcases : ∀ (I : Set R) (hI : closure t = zeroLocus I), zeroLocus (↑(vanishingIdeal t) : Set R) = closure t
Tactic: rcases isClosed_iff_zeroLocus (closure t) |>.mp isClosed_closure with ⟨I, hI⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
t : Set (PrimeSpectrum R)
I : Set R
hI : closure t = zeroLocus I
⊢ zeroLocus (↑(vanishingIdeal t) : Set R) = closure t
have rw : t ⊆ closure t ∧ t ⊆ zeroLocus (↑(vanishingIdeal t) : Set R)
Tactic: rw [subset_antisymm_iff, (isClosed_zeroLocus _).closure_subset_iff, hI,
      subset_zeroLocus_iff_subset_vanishingIdeal, (gc R).u_l_u_eq_u,
      ← subset_zeroLocus_iff_subset_vanishingIdeal, ← hI]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
⊢ Eq (α := Set (PrimeSpectrum R)) (closure {x}) (zeroLocus (↑x.asIdeal : Set R))
have rw : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(vanishingIdeal {x}) : Set R)) (zeroLocus (↑x.asIdeal : Set R))
Tactic: rw [← zeroLocus_vanishingIdeal_eq_closure, vanishingIdeal_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
rw : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(vanishingIdeal {x}) : Set R)) (zeroLocus (↑x.asIdeal : Set R))
⊢ Eq (α := Set (PrimeSpectrum R)) (closure {x}) (zeroLocus (↑x.asIdeal : Set R))
have rw₁ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑x.asIdeal : Set R)) (zeroLocus (↑x.asIdeal : Set R))
Tactic: rw [← zeroLocus_vanishingIdeal_eq_closure, vanishingIdeal_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
⊢ IsClosed (X := PrimeSpectrum R) {x} ↔ x.asIdeal.IsMaximal
have rw : Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑x.asIdeal : Set R)) {x} ↔ x.asIdeal.IsMaximal
Tactic: rw [← closure_subset_iff_isClosed, ← zeroLocus_vanishingIdeal_eq_closure,
      vanishingIdeal_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
⊢ Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑x.asIdeal : Set R)) {x} ↔ x.asIdeal.IsMaximal
have mp : Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑x.asIdeal : Set R)) {x} → x.asIdeal.IsMaximal
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
mp : Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑x.asIdeal : Set R)) {x} → x.asIdeal.IsMaximal
⊢ Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑x.asIdeal : Set R)) {x} ↔ x.asIdeal.IsMaximal
have mpr : x.asIdeal.IsMaximal → Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑x.asIdeal : Set R)) {x}
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
H : Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑x.asIdeal : Set R)) {x}
⊢ x.asIdeal.IsMaximal
have mp : ∀ (m : Ideal R) (hm : m.IsMaximal) (hxm : x.asIdeal ≤ m), x.asIdeal.IsMaximal
Tactic: rcases x.asIdeal.exists_le_maximal x.2.1 with ⟨m, hm, hxm⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (vanishingIdeal s).IsRadical
have rw : (vanishingIdeal s).radical.IsRadical
Tactic: rw [← vanishingIdeal_closure, ← zeroLocus_vanishingIdeal_eq_closure,
    vanishingIdeal_zeroLocus_eq_radical]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R)) ↔ I.radical = J.radical
have mp : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R)) → I.radical = J.radical
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
mp : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R)) → I.radical = J.radical
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R)) ↔ I.radical = J.radical
have mpr : I.radical = J.radical → Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R))
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
h : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R))
⊢ I.radical = J.radical
have mp : Eq (α := Ideal R) (vanishingIdeal (zeroLocus (↑I : Set R))) (vanishingIdeal (zeroLocus (↑J : Set R)))
Tactic: simp_rw [← vanishingIdeal_zeroLocus_eq_radical, h]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
h : I.radical = J.radical
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R))
have mpr : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I.radical : Set R)) (zeroLocus (↑J : Set R))
Tactic: rw [← zeroLocus_radical, h, zeroLocus_radical]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
h : I.radical = J.radical
mpr : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I.radical : Set R)) (zeroLocus (↑J : Set R))
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R))
have mpr₁ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑J.radical : Set R)) (zeroLocus (↑J : Set R))
Tactic: rw [← zeroLocus_radical, h, zeroLocus_radical]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
h : I.radical = J.radical
mpr : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I.radical : Set R)) (zeroLocus (↑J : Set R))
mpr₁ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑J.radical : Set R)) (zeroLocus (↑J : Set R))
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R))
have mpr₂ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑J : Set R)) (zeroLocus (↑J : Set R))
Tactic: rw [← zeroLocus_radical, h, zeroLocus_radical]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ s ⊆ t
have rw : closure s ⊆ closure t
Tactic: rw [← ht.closure_subset_iff, ← ht.closure_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ closure s ⊆ closure t
have h₁ : zeroLocus (↑(vanishingIdeal s) : Set R) = closure s
Tactic: convert! ← zeroLocus_anti_mono_ideal h
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
h₁ : zeroLocus (↑(vanishingIdeal s) : Set R) = closure s
⊢ closure s ⊆ closure t
have h₂ : zeroLocus (↑(vanishingIdeal t) : Set R) = closure t
Tactic: convert! ← zeroLocus_anti_mono_ideal h
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
s t : Set (PrimeSpectrum R)
hs : IsClosed s
ht : IsClosed t
⊢ s ⊂ t ↔ vanishingIdeal t < vanishingIdeal s
have rw : s ⊆ t ∧ ¬t ⊆ s ↔ vanishingIdeal t < vanishingIdeal s
Tactic: rw [Set.ssubset_def, vanishingIdeal_anti_mono_iff hs, vanishingIdeal_anti_mono_iff ht,
    lt_iff_le_not_ge]