awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
isIntegral : ∀ (x : S), IsIntegral R x
⊢ Algebra.IsIntegral R S

Tactic:
constructor
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
⊢ IsClosed (comap (mapRingHom f) '' zeroLocus {p})

Tactic:
have H := h _ (isClosed_zeroLocus {p})
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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})
⊢ 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

Premises used: PrimeSpectrum.zeroLocus_span, closure_eq_iff_isClosed, PrimeSpectrum.closure_image_comap_zeroLocus
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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])
rw : comap (mapRingHom f) '' zeroLocus (↑(Ideal.span {p}) : Set S[X]) ∩ zeroLocus (↑(Ideal.span {X}) : Set R[X]) = ∅
⊢ Membership.mem (γ := Ideal R[X]) (Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})) 1

Tactic:
rw [← Ideal.eq_top_iff_one, sup_comm, ← zeroLocus_empty_iff_eq_top, zeroLocus_sup, H]

Premises used: Ideal.eq_top_iff_one, sup_comm, PrimeSpectrum.zeroLocus_sup, PrimeSpectrum.zeroLocus_empty_iff_eq_top
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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])
this : ∀ (a : PrimeSpectrum S[X]), p ∈ a.asIdeal → X ∉ a.asIdeal
⊢ comap (mapRingHom f) '' zeroLocus (↑(Ideal.span {p}) : Set S[X]) ∩ zeroLocus (↑(Ideal.span {X}) : Set R[X]) = ∅

Tactic:
simpa [Set.eq_empty_iff_forall_notMem]

Premises used: Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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])
suffices : ∀ (a : PrimeSpectrum S[X]), p ∈ a.asIdeal → X ∉ a.asIdeal
⊢ comap (mapRingHom f) '' zeroLocus (↑(Ideal.span {p}) : Set S[X]) ∩ zeroLocus (↑(Ideal.span {X}) : Set R[X]) = ∅

Tactic:
suffices ∀ (a : PrimeSpectrum S[X]), p ∈ a.asIdeal → X ∉ a.asIdeal by
      simpa [Set.eq_empty_iff_forall_notMem]
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
⊢ 1 ∈ q.asIdeal

Tactic:
simpa [p] using (sub_mem (q.asIdeal.mul_mem_left (C r) hXq) hpq)

Premises used: Polynomial.C, sub_mem, Ideal.mul_mem_left, DFunLike.coe, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
⊢ 1 ∈ q.asIdeal

Tactic:
have : 1 ∈ q.asIdeal := by simpa [p] using (sub_mem (q.asIdeal.mul_mem_left (C r) hXq) hpq)
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
this : 1 ∈ q.asIdeal
⊢ False

Tactic:
q.2.ne_top (q.asIdeal.eq_top_iff_one.mpr this)

Premises used: Iff.mpr, PrimeSpectrum.isPrime, Ideal.eq_top_iff_one, Ideal.IsPrime.ne_top, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
this : 1 ∈ q.asIdeal
⊢ False

Tactic:
exact q.2.ne_top (q.asIdeal.eq_top_iff_one.mpr this)

Premises used: Iff.mpr, PrimeSpectrum.isPrime, Ideal.eq_top_iff_one, Ideal.IsPrime.ne_top, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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

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)
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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 :
  ∀ (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
⊢ IsIntegral R r

Tactic:
obtain ⟨a, b, hb, e⟩ := Ideal.mem_span_singleton_sup.mp this

Premises used: Ideal.mem_span_singleton_sup, Iff.mp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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 : ∀ (c : S[X]) (hc : map (algebraMap R S) b = p * c), IsIntegral R r
⊢ IsIntegral R r

Tactic:
obtain ⟨c, hc : b.map (algebraMap R S) = _⟩ := Ideal.mem_span_singleton.mp hb

Premises used: Algebra.algebraMap, Iff.mp, Polynomial.map, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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

Tactic:
⟨b.reverse * X ^ (1 + c.natDegree), ?_, ?_⟩

Premises used: HMul.hMul, RingHom.IsIntegralElem, IsIntegral, HPow.hPow, HAdd.hAdd, And.intro, Exists.intro, Polynomial.natDegree, OfNat.ofNat, Polynomial.X, Polynomial.reverse
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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₁ : eval₂ (algebraMap R S) r (b.reverse * HPow.hPow (α := R[X]) X (1 + c.natDegree)) = 0
⊢ IsIntegral R r

Tactic:
refine ⟨b.reverse * X ^ (1 + c.natDegree), ?_, ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
⊢ (HPow.hPow (α := R[X]) X (1 + c.natDegree)).Monic

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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.Monic
⊢ (b.reverse * HPow.hPow (α := R[X]) X (1 + c.natDegree)).Monic

Tactic:
refine Monic.mul ?_ (by simp)

Premises used: Polynomial.Monic.mul
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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.coeff 0 = 1

Tactic:
simpa using congr(($e).coeff 0)
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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.coeff 0 = 1

Tactic:
have h : b.coeff 0 = 1 := by simpa using congr(($e).coeff 0)
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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.natTrailingDegree = 0

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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.natTrailingDegree = 0

Tactic:
have : b.natTrailingDegree = 0 := by simp [h]
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
isIntegral₄ isIntegral₅ : Eq.{u_1 + 1} (α := R) 1 1
⊢ b.reverse.Monic

Tactic:
rw [Monic.def, reverse_leadingCoeff, trailingCoeff, this, h]

Premises used: Polynomial.trailingCoeff, Polynomial.Monic.def, Polynomial.reverse_leadingCoeff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
⊢ p.natDegree ≤ 1

Tactic:
simpa using natDegree_linear_le (a := r) (b := -1)

Premises used: Polynomial.natDegree_linear_le
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
⊢ p.natDegree ≤ 1

Tactic:
have : p.natDegree ≤ 1 := by simpa using natDegree_linear_le (a := r) (b := -1)
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
⊢ (HPow.hPow (α := S[X]) (β := ℕ) X 0).natDegree ≤ 1 + c.natDegree

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
⊢ 1 ≤ b.natDegree + 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
⊢ natDegree.{u_2} (R := S) ((C : (a : S) → S[X]) r) ≤ b.natDegree

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
⊢ natDegree.{u_2} (R := S) X ≤ 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
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
⊢ eval₂ (algebraMap R S) r (b.reverse * HPow.hPow (α := R[X]) X (1 + c.natDegree)) = 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)]

Premises used: Polynomial.reflect_sub, Polynomial.map_mul, le_rfl, add_assoc, Polynomial.reflect_map, Polynomial.revAt_zero, Polynomial.map_pow, Polynomial.reflect_monomial, Polynomial.map_X, Polynomial.eval_mul, pow_zero, Polynomial.reflect_mul, HAdd.hAdd, Polynomial.natDegree_map_le, LE.le.trans, mul_one, OfNat.ofNat, Polynomial.reverse, Polynomial.eval₂_eq_eval_map
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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 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:
simp [← pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
⊢ 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 _ _
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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)
⊢ Ideal.comap (F := R →+* S) (algebraMap R S) ⊥ ≤ p

Tactic:
simp [Ideal.comap_bot_of_injective (algebraMap R S) hinj]

Premises used: Algebra.algebraMap, Ideal.comap_bot_of_injective