awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
s : Clopens (PrimeSpectrum R)
⊢ ∃ (a : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }),
    (fun (e : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }) ↦
          { carrier := (↑(basicOpen (↑e : R × R).1) : Set (PrimeSpectrum R)), isClopen' := ⋯ :
            Clopens (PrimeSpectrum R) })
        a =
      s
have refine_2 : ∀ (e f : R) (mul : e * f = 0) (add : e + f = 1) (eq : s.carrier = (↑(basicOpen e) : Set (PrimeSpectrum R))),
  ∃ (a : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }),
    (fun (e : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }) ↦
          { carrier := (↑(basicOpen (↑e : R × R).1) : Set (PrimeSpectrum R)), isClopen' := sorry :
            Clopens (PrimeSpectrum R) })
        a =
      s
Tactic: have ⟨e, f, mul, add, eq⟩ := isClopen_iff_mul_add.mp s.2
-- 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
a b : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
⊢ LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen (↑a : R × R).1) (basicOpen (↑b : R × R).1) ↔ a ≤ b
have rw : Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen ((↑a : R × R).1 * (↑b : R × R).1))
    (basicOpen (↑a : R × R).1) ↔
  a ≤ b
Tactic: rw [← inf_eq_left, ← basicOpen_mul]
-- 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
a b : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
⊢ Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen ((↑a : R × R).1 * (↑b : R × R).1))
      (basicOpen (↑a : R × R).1) ↔
    a ≤ b
have refine : ∀
  (h :
    Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen ((↑a : R × R).1 * (↑b : R × R).1))
      (basicOpen (↑a : R × R).1)),
  a ≤ b
Tactic: refine ⟨fun h ↦ ?_, (by rw [·])⟩
-- 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
a b : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
h :
  Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen ((↑a : R × R).1 * (↑b : R × R).1))
    (basicOpen (↑a : R × R).1)
⊢ a ≤ b
have rw : a ⊓ b = a
Tactic: rw [← inf_eq_left]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
a b : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
h :
  Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen ((↑a : R × R).1 * (↑b : R × R).1))
    (basicOpen (↑a : R × R).1)
⊢ a ⊓ b = a
have this : IsIdempotentElem (↑a : R × R).1
Tactic: have := (IsIdempotentElem.of_mul_add a.2.1 a.2.2).1
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.FG
⊢ IsRetrocompact (X := PrimeSpectrum R) (zeroLocus (↑I : Set R))ᶜ
have obtain : ∀ (s : Finset R), IsRetrocompact (X := PrimeSpectrum R) (zeroLocus (↑(Ideal.span (↑s : Set R)) : Set R))ᶜ
Tactic: obtain ⟨s, rfl⟩ := hI
Cleared hypotheses: I, hI
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Finset R
⊢ IsRetrocompact (X := PrimeSpectrum R) (zeroLocus (↑(Ideal.span (↑s : Set R)) : Set R))ᶜ
have rw : IsRetrocompact (X := PrimeSpectrum R) (zeroLocus (↑s : Set R))ᶜ
Tactic: rw [zeroLocus_span]
-- 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
hf : f.IsIntegral
⊢ IsClosedMap (comap f)
have refine : ∀ (s : Set (PrimeSpectrum S)) (hs : IsClosed s), StableUnderSpecialization (comap f '' s)
Tactic: refine fun s hs ↦ isClosed_image_of_stableUnderSpecialization _ _ hs ?_
-- 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
s : Set (PrimeSpectrum S)
hs : IsClosed s
y : PrimeSpectrum R
x : PrimeSpectrum S
hx : x ∈ s
e : comap f x ⤳ y
⊢ y ∈ comap f '' s
have algebraizeInst : let algInst := f.toAlgebra;
Algebra.IsIntegral R S
Tactic: algebraize [f]
-- 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
hf : f.IsIntegral
s : Set (PrimeSpectrum S)
hs : IsClosed s
y : PrimeSpectrum R
x : PrimeSpectrum S
hx : x ∈ s
e : comap f x ⤳ y
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.IsIntegral R S
⊢ y ∈ comap f '' s
have obtain : ∀ (q : Ideal S) (hq₁ : q ≥ x.asIdeal) (hq₂ : q.IsPrime)
  (hq₃ : Ideal.comap (F := R →+* S) (algebraMap R S) q = y.asIdeal), y ∈ comap f '' s
Tactic: obtain ⟨q, hq₁, hq₂, hq₃⟩ := Ideal.exists_ideal_over_prime_of_isIntegral y.asIdeal x.asIdeal
    ((le_iff_specializes _ _).mpr e)
-- 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
I : Ideal S
⊢ closure (comap f '' zeroLocus (↑I : Set S)) = zeroLocus (↑(Ideal.comap f I) : Set R)
have a : closure (comap f '' zeroLocus (↑I : Set S)) ⊆ zeroLocus (↑(Ideal.comap f I) : Set R)
Tactic: apply subset_antisymm
-- 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
I : Ideal S
a : closure (comap f '' zeroLocus (↑I : Set S)) ⊆ zeroLocus (↑(Ideal.comap f I) : Set R)
⊢ closure (comap f '' zeroLocus (↑I : Set S)) = zeroLocus (↑(Ideal.comap f I) : Set R)
have a₁ : zeroLocus (↑(Ideal.comap f I) : Set R) ⊆ closure (comap f '' zeroLocus (↑I : Set S))
Tactic: apply subset_antisymm
-- 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
I : Ideal S
⊢ closure (comap f '' zeroLocus (↑I : Set S)) ⊆ zeroLocus (↑(Ideal.comap f I) : Set R)
have a : Subset (α := Set (PrimeSpectrum S)) (zeroLocus (↑I : Set S))
  (zeroLocus ((⇑f : (a : R) → S) '' (↑(Ideal.comap f I) : Set R)))
Tactic: rw [(isClosed_zeroLocus _).closure_subset_iff, Set.image_subset_iff, preimage_comap_zeroLocus]
-- 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
I : Ideal S
x : PrimeSpectrum R
hx : Ideal.comap f I ≤ x.asIdeal
⊢ x ∈ closure (comap f '' zeroLocus (↑I : Set S))
have a : ∀ (q : Ideal R) (hq₁ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (Ideal.comap f I)) q)
  (hq₂ : q ≤ x.asIdeal), x ∈ closure (comap f '' zeroLocus (↑I : Set S))
Tactic: obtain ⟨q, hq₁, hq₂⟩ := Ideal.exists_minimalPrimes_le hx
-- 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
I : Ideal S
x : PrimeSpectrum R
hx : Ideal.comap f I ≤ x.asIdeal
q : Ideal R
hq₁ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (Ideal.comap f I)) q
hq₂ : q ≤ x.asIdeal
⊢ x ∈ closure (comap f '' zeroLocus (↑I : Set S))
have a : ∀ (p' : Ideal S) (hp' : p'.IsPrime) (hp'' : I ≤ p')
  (hq₁ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (Ideal.comap f I)) (Ideal.comap f p'))
  (hq₂ : Ideal.comap f p' ≤ x.asIdeal), x ∈ closure (comap f '' zeroLocus (↑I : Set S))
Tactic: obtain ⟨p', hp', hp'', rfl⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes f _ hq₁
Cleared hypotheses: q, hq₁, hq₂
-- 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
this : Algebra.IsIntegral R S
⊢ f.IsIntegral
have rwa : ∀ (this : ∀ (x : S), IsIntegral R x), f.IsIntegral
Tactic: rwa [Algebra.isIntegral_def] at this
Cleared hypotheses: this
-- 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
⊢ f.IsIntegral
have suffices : Algebra.IsIntegral R S
Tactic: suffices Algebra.IsIntegral R S by rwa [Algebra.isIntegral_def] at this
-- 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
h : IsClosedMap (comap (mapRingHom f))
algInst : Algebra R S := f.toAlgebra
⊢ Algebra.IsIntegral R S
have a : Nontrivial R
Tactic: nontriviality R
-- 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
h : IsClosedMap (comap (mapRingHom f))
algInst : Algebra R S := f.toAlgebra
h_1 : Nontrivial R
⊢ Algebra.IsIntegral R S
have a : Nontrivial S
Tactic: nontriviality S
-- 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
⊢ Algebra.IsIntegral R S
have isIntegral : ∀ (x : S), IsIntegral R x
Tactic: constructor
-- 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
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
⊢ Membership.mem (γ := Ideal R[X]) (Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})) 1
have H : IsClosed (comap (mapRingHom f) '' zeroLocus {p})
Tactic: have H := h _ (isClosed_zeroLocus {p})
-- 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
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
H : IsClosed (comap (mapRingHom f) '' zeroLocus {p})
⊢ Membership.mem (γ := Ideal R[X]) (Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})) 1
have H₁ : zeroLocus (↑(Ideal.comap (mapRingHom f) (Ideal.span {p})) : Set R[X]) =
  comap (mapRingHom f) '' zeroLocus (↑(Ideal.span {p}) : Set S[X])
Tactic: rw [← zeroLocus_span, ← closure_eq_iff_isClosed, closure_image_comap_zeroLocus] at H
Cleared hypotheses: H
-- 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
H :
  zeroLocus (↑(Ideal.comap (mapRingHom f) (Ideal.span {p})) : Set R[X]) =
    comap (mapRingHom f) '' zeroLocus (↑(Ideal.span {p}) : Set S[X])
⊢ Membership.mem (γ := Ideal R[X]) (Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})) 1
have rw : comap (mapRingHom f) '' zeroLocus (↑(Ideal.span {p}) : Set S[X]) ∩ zeroLocus (↑(Ideal.span {X}) : Set R[X]) = ∅
Tactic: rw [← Ideal.eq_top_iff_one, sup_comm, ← zeroLocus_empty_iff_eq_top, zeroLocus_sup, H]
-- 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
H :
  zeroLocus (↑(Ideal.comap (mapRingHom f) (Ideal.span {p})) : Set R[X]) =
    comap (mapRingHom f) '' zeroLocus (↑(Ideal.span {p}) : Set S[X])
⊢ comap (mapRingHom f) '' zeroLocus (↑(Ideal.span {p}) : Set S[X]) ∩ zeroLocus (↑(Ideal.span {X}) : Set R[X]) = ∅
have suffices : ∀ (a : PrimeSpectrum S[X]), p ∈ a.asIdeal → X ∉ a.asIdeal
Tactic: suffices ∀ (a : PrimeSpectrum S[X]), p ∈ a.asIdeal → X ∉ a.asIdeal by
      simpa [Set.eq_empty_iff_forall_notMem]
-- 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
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
H :
  zeroLocus (↑(Ideal.comap (mapRingHom f) (Ideal.span {p})) : Set R[X]) =
    comap (mapRingHom f) '' zeroLocus (↑(Ideal.span {p}) : Set S[X])
q : PrimeSpectrum S[X]
hpq : p ∈ q.asIdeal
hXq : X ∈ q.asIdeal
⊢ False
have this : 1 ∈ q.asIdeal
Tactic: have : 1 ∈ q.asIdeal := by simpa [p] using (sub_mem (q.asIdeal.mul_mem_left (C r) hXq) hpq)
-- 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
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
⊢ IsIntegral R r
have this : Membership.mem (γ := Ideal R[X]) (Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})) 1
Tactic: have : (1 : R[X]) ∈ Ideal.span {X} ⊔ (Ideal.span {p}).comap (mapRingHom f) := by
    have H := h _ (isClosed_zeroLocus {p})
    rw [← zeroLocus_span, ← closure_eq_iff_isClosed, closure_image_comap_zeroLocus] at H
    rw [← Ideal.eq_top_iff_one, sup_comm, ← zeroLocus_empty_iff_eq_top, zeroLocus_sup, H]
    suffices ∀ (a : PrimeSpectrum S[X]), p ∈ a.asIdeal → X ∉ a.asIdeal by
      simpa [Set.eq_empty_iff_forall_notMem]
    intro q hpq hXq
    have : 1 ∈ q.asIdeal := by simpa [p] using (sub_mem (q.asIdeal.mul_mem_left (C r) hXq) hpq)
    exact q.2.ne_top (q.asIdeal.eq_top_iff_one.mpr this)
-- 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 : Membership.mem (γ := Ideal R[X]) (Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})) 1
⊢ IsIntegral R r
have isIntegral : ∀ (a b : R[X]) (hb : Membership.mem (γ := Ideal R[X]) (Ideal.comap (mapRingHom f) (Ideal.span {p})) b)
  (e : a * X + b = 1), IsIntegral R r
Tactic: obtain ⟨a, b, hb, e⟩ := Ideal.mem_span_singleton_sup.mp this
-- 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 : 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
⊢ IsIntegral R r
have isIntegral : ∀ (c : S[X]) (hc : map (algebraMap R S) b = p * c), IsIntegral R r
Tactic: obtain ⟨c, hc : b.map (algebraMap R S) = _⟩ := Ideal.mem_span_singleton.mp hb
-- 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 : 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
⊢ IsIntegral R r
have isIntegral : (b.reverse * HPow.hPow (α := R[X]) X (1 + c.natDegree)).Monic
Tactic: refine ⟨b.reverse * X ^ (1 + c.natDegree), ?_, ?_⟩
-- 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 : 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
isIntegral : (b.reverse * HPow.hPow (α := R[X]) X (1 + c.natDegree)).Monic
⊢ IsIntegral R r
have isIntegral₁ : eval₂ (algebraMap R S) r (b.reverse * HPow.hPow (α := R[X]) X (1 + c.natDegree)) = 0
Tactic: refine ⟨b.reverse * X ^ (1 + c.natDegree), ?_, ?_⟩
-- 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 : 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
⊢ (b.reverse * HPow.hPow (α := R[X]) X (1 + c.natDegree)).Monic
have isIntegral : b.reverse.Monic
Tactic: refine Monic.mul ?_ (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
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 : 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
⊢ b.reverse.Monic
have h₁ : b.coeff 0 = 1
Tactic: have h : b.coeff 0 = 1 := by simpa using congr(($e).coeff 0)
-- 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
h_1 : IsClosedMap (comap (mapRingHom f))
algInst : Algebra R S := f.toAlgebra
h_2 : Nontrivial R
h_3 : Nontrivial S
r : S
p : S[X] := HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) r : S[X]) X - 1
this : 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
h : b.coeff 0 = 1
⊢ b.reverse.Monic
have this₁ : b.natTrailingDegree = 0
Tactic: have : b.natTrailingDegree = 0 := by simp [h]
-- 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_1 : IsClosedMap (comap (mapRingHom f))
algInst : Algebra R S := f.toAlgebra
h_2 : Nontrivial R
h_3 : 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
h : b.coeff 0 = 1
this : b.natTrailingDegree = 0
⊢ b.reverse.Monic
have isIntegral : b.reverse.leadingCoeff = 1
Tactic: rw [Monic.def, reverse_leadingCoeff, trailingCoeff, this, h]
-- 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_1 : IsClosedMap (comap (mapRingHom f))
algInst : Algebra R S := f.toAlgebra
h_2 : Nontrivial R
h_3 : 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
h : b.coeff 0 = 1
this : b.natTrailingDegree = 0
isIntegral : b.reverse.leadingCoeff = 1
⊢ b.reverse.Monic
have isIntegral₁ : b.trailingCoeff = 1
Tactic: rw [Monic.def, reverse_leadingCoeff, trailingCoeff, this, h]
-- 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_1 : IsClosedMap (comap (mapRingHom f))
algInst : Algebra R S := f.toAlgebra
h_2 : Nontrivial R
h_3 : 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
h : b.coeff 0 = 1
this : b.natTrailingDegree = 0
isIntegral : b.reverse.leadingCoeff = 1
isIntegral₁ : b.trailingCoeff = 1
⊢ b.reverse.Monic
have isIntegral₂ : b.coeff b.natTrailingDegree = 1
Tactic: rw [Monic.def, reverse_leadingCoeff, trailingCoeff, this, h]
-- 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_1 : IsClosedMap (comap (mapRingHom f))
algInst : Algebra R S := f.toAlgebra
h_2 : Nontrivial R
h_3 : 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
h : b.coeff 0 = 1
this : b.natTrailingDegree = 0
isIntegral : b.reverse.leadingCoeff = 1
isIntegral₁ : b.trailingCoeff = 1
isIntegral₂ : b.coeff b.natTrailingDegree = 1
isIntegral₃ : b.coeff 0 = 1
⊢ b.reverse.Monic
have isIntegral₄ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [Monic.def, reverse_leadingCoeff, trailingCoeff, this, h]
-- 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
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 : 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
⊢ eval₂ (algebraMap R S) r (b.reverse * HPow.hPow (α := R[X]) X (1 + c.natDegree)) = 0
have this₁ : p.natDegree ≤ 1
Tactic: have : p.natDegree ≤ 1 := by simpa using natDegree_linear_le (a := r) (b := -1)