awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst : Algebra R S := f.toAlgebra
h_1 : Nontrivial R
h_2 : Nontrivial S
r : S
p : S[X] := HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) r : S[X]) X - 1
this_1 : Membership.mem (γ := Ideal R[X]) (Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})) 1
a b : R[X]
hb : Membership.mem (γ := Ideal R[X]) (Ideal.comap (mapRingHom f) (Ideal.span {p})) b
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
this : p.natDegree ≤ 1
⊢ eval₂ (algebraMap R S) r (b.reverse * HPow.hPow (α := R[X]) X (1 + c.natDegree)) = 0
have isIntegral : eval r
      (HMul.hMul (α := S[X]) (reflect b.natDegree ((C : (a : S) → S[X]) r)) (reflect 1 X) -
        reflect (b.natDegree + 1) 1) *
    eval r (reflect c.natDegree c) =
  0
Tactic: rw [eval₂_eq_eval_map, reverse, Polynomial.map_mul, ← reflect_map, Polynomial.map_pow,
      map_X, ← revAt_zero (1 + _), ← reflect_monomial,
      ← reflect_mul _ _ natDegree_map_le (by simp), pow_zero, mul_one, hc,
      ← add_assoc, reflect_mul _ _ (this.trans (by simp)) le_rfl,
      eval_mul, reflect_sub, reflect_mul _ _ (by simp) (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : FaithfulSMul R S
p : Ideal R
hp : p.IsPrime
⊢ ∃ (a : PrimeSpectrum S), comap (algebraMap R S) a = { asIdeal := p, isPrime := hp : PrimeSpectrum R }
have hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
Tactic: have hinj : Function.Injective (algebraMap R S) := FaithfulSMul.algebraMap_injective _ _
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : FaithfulSMul R S
p : Ideal R
hp : p.IsPrime
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ ∃ (a : PrimeSpectrum S), comap (algebraMap R S) a = { asIdeal := p, isPrime := hp : PrimeSpectrum R }
have obtain : ∀ Q ≥ ⊥,
  ∀ (hQ : Q.IsPrime) (hp : Ideal.IsPrime (Ideal.comap (F := R →+* S) (algebraMap R S) Q)),
    ∃ (a : PrimeSpectrum S),
      comap (algebraMap R S) a =
        { asIdeal := Ideal.comap (F := R →+* S) (algebraMap R S) Q, isPrime := hp : PrimeSpectrum R }
Tactic: obtain ⟨Q, _, hQ, rfl⟩ := Ideal.exists_ideal_over_prime_of_isIntegral p (⊥ : Ideal S)
    (by simp [Ideal.comap_bot_of_injective (algebraMap R S) hinj])
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.IsIntegral
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ Function.Surjective (comap f)
have algebraizeInst : let algInst := f.toAlgebra;
Algebra.IsIntegral R S
Tactic: algebraize [f]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.IsIntegral
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.IsIntegral R S
⊢ Function.Surjective (comap f)
have this : FaithfulSMul R S
Tactic: have : FaithfulSMul R S := (faithfulSMul_iff_algebraMap_injective R S).mpr hinj
-- 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
I : Ideal R
e : (↑{p : Ideal R | p.IsPrime ∧ I ≤ p} : Type u) ≃o (↑(zeroLocus (↑I : Set R)) : Type u) :=
  RelIso.mk (r := fun (x1 x2 : (↑{p : Ideal R | p.IsPrime ∧ I ≤ p} : Type u)) ↦ x1 ≤ x2) (s :=
    fun (x1 x2 : (↑(zeroLocus (↑I : Set R)) : Type u)) ↦ x1 ≤ x2)
    {
      toFun := fun (x : (↑{p : Ideal R | p.IsPrime ∧ I ≤ p} : Type u)) ↦
        Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
          Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) x)
          { asIdeal := (↑x : Ideal R), isPrime := ⋯ } ⋯,
      invFun := fun (x : (↑(zeroLocus (↑I : Set R)) : Type u)) ↦
        Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p.IsPrime ∧ I ≤ p} x)
          (↑x : PrimeSpectrum R).asIdeal ⋯,
      left_inv := ⋯, right_inv := ⋯ }
    ⋯
⊢ (↑I.minimalPrimes : Type u) ≃o (↑(irreducibleComponents (↑(zeroLocus (↑I : Set R)) : Type u)) : Type u)ᵒᵈ
have rw : (↑I.minimalPrimes : Type u) ≃o
  (↑{s : Set (↑(zeroLocus (↑I : Set R)) : Type u) |
          Maximal (fun (x : Set (↑(zeroLocus (↑I : Set R)) : Type u)) ↦ IsClosed x ∧ IsIrreducible x) s} :
      Type u)ᵒᵈ
Tactic: rw [irreducibleComponents_eq_maximals_closed]
-- 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
e : (↑{p : Ideal R | p.IsPrime ∧ ⊥ ≤ p} : Type u) ≃o PrimeSpectrum R :=
  RelIso.mk (r := fun (x1 x2 : (↑{p : Ideal R | p.IsPrime ∧ ⊥ ≤ p} : Type u)) ↦ x1 ≤ x2) (s :=
    fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2)
    { toFun := fun (x : (↑{p : Ideal R | p.IsPrime ∧ ⊥ ≤ p} : Type u)) ↦ { asIdeal := (↑x : Ideal R), isPrime := ⋯ },
      invFun := fun (x : PrimeSpectrum R) ↦
        Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p.IsPrime ∧ ⊥ ≤ p} x)
          x.asIdeal ⋯,
      left_inv := ⋯, right_inv := ⋯ }
    ⋯
⊢ (↑(minimalPrimes R) : Type u) ≃o (↑(irreducibleComponents (PrimeSpectrum R)) : Type u)ᵒᵈ
have rw : (↑(minimalPrimes R) : Type u) ≃o
  (↑{s : Set (PrimeSpectrum R) | Maximal (fun (x : Set (PrimeSpectrum R)) ↦ IsClosed x ∧ IsIrreducible x) s} : Type u)ᵒᵈ
Tactic: rw [irreducibleComponents_eq_maximals_closed]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := Set (Ideal R)) (vanishingIdeal '' irreducibleComponents (PrimeSpectrum R)) (minimalPrimes R)
have rw : Eq.{u + 1} (α := Set (Ideal R))
  {x : Ideal R |
    Minimal
      (fun (x : Ideal R) ↦ ∃ (x₀ : Set (PrimeSpectrum R)), (IsClosed x₀ ∧ IsIrreducible x₀) ∧ vanishingIdeal x₀ = x) x}
  {x : Ideal R |
    Minimal
      (Membership.mem (γ := Set (Ideal R))
        (vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsClosed s ∧ IsIrreducible s}))
      x}
Tactic: rw [irreducibleComponents_eq_maximals_closed, minimalPrimes_eq_minimals,
    image_antitone_setOf_maximal (fun s t hs _ ↦ (vanishingIdeal_anti_mono_iff hs.1).symm),
    ← funext (@Set.mem_setOf_eq _ · Ideal.IsPrime), ← vanishingIdeal_isClosed_isIrreducible]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := Set (Set (PrimeSpectrum R))) (Set.image (α := Ideal R) (zeroLocus ∘ SetLike.coe) (minimalPrimes R))
    (irreducibleComponents (PrimeSpectrum R))
have rw : Set.EqOn (α := Set (PrimeSpectrum R)) ((zeroLocus ∘ SetLike.coe) ∘ vanishingIdeal) id
  (irreducibleComponents (PrimeSpectrum R))
Tactic: rw [← vanishingIdeal_irreducibleComponents, ← Set.image_comp, Set.EqOn.image_eq_self]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) (vanishingIdeal s) ↔
    Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R)) (closure s)
have mp : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) (vanishingIdeal s) →
  Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R)) (closure s)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
mp :
  Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) (vanishingIdeal s) →
    Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R)) (closure s)
⊢ Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) (vanishingIdeal s) ↔
    Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R)) (closure s)
have mpr : Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R)) (closure s) →
  Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) (vanishingIdeal s)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) (vanishingIdeal s) →
    Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R)) (closure s)
have mp : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) (vanishingIdeal s) →
  Membership.mem (γ := Set (Set (PrimeSpectrum R)))
    (Set.image (α := Ideal R) (zeroLocus ∘ SetLike.coe) (minimalPrimes R)) (zeroLocus (↑(vanishingIdeal s) : Set R))
Tactic: rw [← zeroLocus_minimalPrimes, ← zeroLocus_vanishingIdeal_eq_closure]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R)) (closure s) →
    Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) (vanishingIdeal s)
have mpr : Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R)) (closure s) →
  Membership.mem (γ := Set (Ideal R)) (vanishingIdeal '' irreducibleComponents (PrimeSpectrum R))
    (vanishingIdeal (closure s))
Tactic: rw [← vanishingIdeal_irreducibleComponents, ← vanishingIdeal_closure]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
⊢ Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) ↔
    Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I.radical
have rw : Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) ↔
  Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) (vanishingIdeal (zeroLocus (↑I : Set R)))
Tactic: rw [← vanishingIdeal_zeroLocus_eq_radical]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
| Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R)) (zeroLocus (↑I : Set R))
have rw : Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R))
  (closure (zeroLocus (↑I : Set R)))
Tactic: rw [← (isClosed_zeroLocus _).closure_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
⊢ Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) ↔
    Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) (vanishingIdeal (zeroLocus (↑I : Set R)))
have conv_lhs : Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R))
    (closure (zeroLocus (↑I : Set R))) ↔
  Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) (vanishingIdeal (zeroLocus (↑I : Set R)))
Tactic: conv_lhs => rw [← (isClosed_zeroLocus _).closure_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsLocalRing R
S : Type v
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
⊢ IsLocalHom (R := R) (S := S) f ↔ PrimeSpectrum.comap f (closedPoint S) = closedPoint R
have this : IsLocalHom (R := R) (S := S) f ↔ Eq (α := Ideal R) (Ideal.comap f (maximalIdeal S)) (maximalIdeal R)
Tactic: have := (local_hom_TFAE f).out 0 4
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsLocalRing R
S : Type v
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
this : IsLocalHom (R := R) (S := S) f ↔ Eq (α := Ideal R) (Ideal.comap f (maximalIdeal S)) (maximalIdeal R)
⊢ IsLocalHom (R := R) (S := S) f ↔ PrimeSpectrum.comap f (closedPoint S) = closedPoint R
have rw : Eq (α := Ideal R) (Ideal.comap f (maximalIdeal S)) (maximalIdeal R) ↔
  (PrimeSpectrum.comap f (closedPoint S)).asIdeal = PrimeSpectrum.asIdeal (closedPoint R)
Tactic: rw [this, PrimeSpectrum.ext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ closedPoint R ∈ U ↔ U = ⊤
have mp : closedPoint R ∈ U → U = ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
mp : closedPoint R ∈ U → U = ⊤
⊢ closedPoint R ∈ U ↔ U = ⊤
have mpr : U = ⊤ → closedPoint R ∈ U
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ closedPoint R ∈ U → U = ⊤
have mp : closedPoint R ∈ U → ⊤ ≤ U
Tactic: rw [eq_top_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
T : Type u
inst : CommRing T
inst_1 : IsLocalRing T
x : PrimeSpectrum (ResidueField T)
⊢ PrimeSpectrum.comap (residue T) x = closedPoint T
have rw : Eq (α := PrimeSpectrum T) (PrimeSpectrum.comap (S := ResidueField T) (residue T) ⊥) (closedPoint T)
Tactic: rw [Subsingleton.elim x ⊥]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
T : Type u
inst : CommRing T
inst_1 : IsLocalRing T
x : PrimeSpectrum (ResidueField T)
⊢ Eq (α := PrimeSpectrum T) (PrimeSpectrum.comap (S := ResidueField T) (residue T) ⊥) (closedPoint T)
have asIdeal : Eq (α := Ideal T) (PrimeSpectrum.asIdeal (PrimeSpectrum.comap (S := ResidueField T) (residue T) ⊥))
  (PrimeSpectrum.asIdeal (closedPoint T))
Tactic: ext1
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsLocalRing R
⊢ IsClosed (X := PrimeSpectrum R) {closedPoint R}
have rw : Ideal.IsMaximal (PrimeSpectrum.asIdeal { asIdeal := maximalIdeal R, isPrime := sorry })
Tactic: rw [PrimeSpectrum.isClosed_singleton_iff_isMaximal, closedPoint]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommRing R
e : R
he : IsIdempotentElem e
⊢ zeroLocus {e} = (↑(basicOpen (1 - e)) : Set (PrimeSpectrum R))
have rw : Eq (α := Set (PrimeSpectrum R)) (zeroLocus {e}) (zeroLocus {1 - (1 - e)})
Tactic: rw [basicOpen_eq_zeroLocus_of_isIdempotentElem _ he.one_sub, sub_sub_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommRing R
e : R
he : IsIdempotentElem e
rw : Eq (α := Set (PrimeSpectrum R)) (zeroLocus {e}) (zeroLocus {1 - (1 - e)})
⊢ zeroLocus {e} = (↑(basicOpen (1 - e)) : Set (PrimeSpectrum R))
have rw₁ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus {e}) (zeroLocus {e})
Tactic: rw [basicOpen_eq_zeroLocus_of_isIdempotentElem _ he.one_sub, sub_sub_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommRing R
s : Set (PrimeSpectrum R)
⊢ IsClopen s ↔ ∃ (e : R), IsIdempotentElem e ∧ s = (↑(basicOpen e) : Set (PrimeSpectrum R))
have refine : (∃ (e : R), IsIdempotentElem e ∧ s = (↑(basicOpen e) : Set (PrimeSpectrum R))) → IsClopen s
Tactic: refine ⟨exists_idempotent_basicOpen_eq_of_isClopen, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommRing R
e : R
he : IsIdempotentElem e
⊢ IsClopen (↑(basicOpen e) : Set (PrimeSpectrum R))
have refine : IsClosed (↑(basicOpen e) : Set (PrimeSpectrum R))
Tactic: refine ⟨?_, (basicOpen e).2⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommRing R
e : R
he : IsIdempotentElem e
⊢ IsClosed (↑(basicOpen e) : Set (PrimeSpectrum R))
have rw : IsClosed (X := PrimeSpectrum R) (zeroLocus {1 - e})
Tactic: rw [PrimeSpectrum.basicOpen_eq_zeroLocus_of_isIdempotentElem e he]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔ ∃ (m : M), ∀ r ∉ p.asIdeal, r • m ≠ 0
have rw : (¬∀ (m : M), ∃ r ∉ p.asIdeal, r • m = 0) ↔ ∃ (m : M), ∀ r ∉ p.asIdeal, r • m ≠ 0
Tactic: rw [← @not_not (_ ∈ _), notMem_support_iff']
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
⊢ (¬∀ (m : M), ∃ r ∉ p.asIdeal, r • m = 0) ↔ ∃ (m : M), ∀ r ∉ p.asIdeal, r • m ≠ 0
have push : (∃ (m : M), ∀ (r : R) (_ : r ∉ p.asIdeal), r • m ≠ 0) ↔ ∃ (m : M), ∀ r ∉ p.asIdeal, r • m ≠ 0
Tactic: push Not
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔
    ∃ (m : M), Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal
have rw : (∃ (m : M), ∀ r ∉ p.asIdeal, r • m ≠ 0) ↔ ∃ (m : M), Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal
Tactic: rw [Module.mem_support_iff']
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
⊢ (∃ (m : M), ∀ r ∉ p.asIdeal, r • m ≠ 0) ↔ ∃ (m : M), Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal
have simp_rw : (∃ (m : M), ∀ (r : R), r • m = 0 → r ∈ p.asIdeal) ↔ ∃ (m : M), Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal
Tactic: simp_rw [not_imp_not, SetLike.le_def, Submodule.mem_annihilator_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
simp_rw :
  (∃ (m : M), ∀ (r : R), r • m = 0 → r ∈ p.asIdeal) ↔ ∃ (m : M), Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal
⊢ (∃ (m : M), ∀ r ∉ p.asIdeal, r • m ≠ 0) ↔ ∃ (m : M), Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal
have simp_rw₁ : (∃ (m : M), ∀ (r : R), r • m = 0 → r ∈ p.asIdeal) ↔
  ∃ (m : M), ∀ ⦃x : R⦄, Membership.mem (γ := Ideal R) (Submodule.annihilator (M := M) (R ∙ m)) x → x ∈ p.asIdeal
Tactic: simp_rw [not_imp_not, SetLike.le_def, Submodule.mem_annihilator_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p q : PrimeSpectrum R
H : p ≤ q
hp : Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) q
have rw : ∀ (hp : ∃ (m : M), Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal),
  ∃ (m : M), Submodule.annihilator (M := M) (R ∙ m) ≤ q.asIdeal
Tactic: rw [Module.mem_support_iff_exists_annihilator] at hp ⊢
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
s : Set M
hs : Eq (α := Submodule R M) (Submodule.span R s) ⊤
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔
    ∃ m ∈ s, Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal
have mp : Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p →
  ∃ m ∈ s, Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
s : Set M
hs : Eq (α := Submodule R M) (Submodule.span R s) ⊤
mp :
  Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p →
    ∃ m ∈ s, Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔
    ∃ m ∈ s, Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal
have mpr : (∃ m ∈ s, Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal) →
  Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
s : Set M
hs : Eq (α := Submodule R M) (Submodule.span R s) ⊤
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p →
    ∃ m ∈ s, Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal
have mp : (¬∃ m ∈ s, Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal) → p ∉ support R M
Tactic: contrapose
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
s : Set M
hs : Eq (α := Submodule R M) (Submodule.span R s) ⊤
⊢ (¬∃ m ∈ s, Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal) → p ∉ support R M
have mp : (¬∃ m ∈ s, Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal) →
  ∀ x ∈ s, x ∈ (↑(LinearMap.ker (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M)) : Set M)
Tactic: rw [notMem_support_iff, LocalizedModule.subsingleton_iff_ker_eq_top, ← top_le_iff,
      ← hs, Submodule.span_le, Set.subset_def]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
s : Set M
hs : Eq (α := Submodule R M) (Submodule.span R s) ⊤
⊢ (¬∃ m ∈ s, Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal) →
    ∀ x ∈ s, x ∈ (↑(LinearMap.ker (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M)) : Set M)
have mp : (¬∃ m ∈ s, ∀ ⦃x : R⦄, x • m = 0 → x ∈ p.asIdeal) → ∀ x ∈ s, ∃ r ∈ p.asIdeal.primeCompl, r • x = 0
Tactic: simp_rw [SetLike.le_def, Submodule.mem_annihilator_span_singleton, SetLike.mem_coe,
      LocalizedModule.mem_ker_mkLinearMap_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
s : Set M
hs : Eq (α := Submodule R M) (Submodule.span R s) ⊤
⊢ (¬∃ m ∈ s, ∀ ⦃x : R⦄, x • m = 0 → x ∈ p.asIdeal) → ∀ x ∈ s, ∃ r ∈ p.asIdeal.primeCompl, r • x = 0
have mp : (∀ (m : M) (_ : m ∈ s), ∃ (x : R), x • m = 0 ∧ x ∉ p.asIdeal) → ∀ x ∈ s, ∃ r ∈ p.asIdeal.primeCompl, r • x = 0
Tactic: push Not
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
s : Set M
hs : Eq (α := Submodule R M) (Submodule.span R s) ⊤
⊢ (∀ (m : M) (_ : m ∈ s), ∃ (x : R), x • m = 0 ∧ x ∉ p.asIdeal) → ∀ x ∈ s, ∃ r ∈ p.asIdeal.primeCompl, r • x = 0
have mp : (∀ (m : M) (_ : m ∈ s), ∃ x ∉ p.asIdeal, x • m = 0) → ∀ x ∈ s, ∃ r ∈ p.asIdeal.primeCompl, r • x = 0
Tactic: simp_rw [and_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
hp : Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p
⊢ annihilator R M ≤ p.asIdeal
have obtain : ∀ (m : M) (hm : Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal), annihilator R M ≤ p.asIdeal
Tactic: obtain ⟨m, hm⟩ := mem_support_iff_exists_annihilator.mp hp
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
⊢ Subsingleton (LocalizedModule.Away f M) ↔
    Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f})
have rw : (∀ (m : M), ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0) ↔
  Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f})
Tactic: rw [LocalizedModule.subsingleton_iff]