awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h_1 : HasGoingDown R S
Q : PrimeSpectrum S
p : PrimeSpectrum R
hp : p ≤ PrimeSpectrum.comap (algebraMap R S) Q
P : Ideal S
hle : P ≤ Q.asIdeal
hP : P.IsPrime
h : P.LiesOver p.asIdeal
refine_1 :
  PrimeSpectrum.asIdeal (PrimeSpectrum.comap (algebraMap R S) { asIdeal := P, isPrime := hP : PrimeSpectrum S }) =
    p.asIdeal
⊢ PrimeSpectrum.comap (algebraMap R S) { asIdeal := P, isPrime := hP : PrimeSpectrum S } = p

Tactic:
ext : 1
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h_1 : HasGoingDown R S
Q : PrimeSpectrum S
p : PrimeSpectrum R
hp : p ≤ PrimeSpectrum.comap (algebraMap R S) Q
P : Ideal S
hle : P ≤ Q.asIdeal
hP : P.IsPrime
h : P.LiesOver p.asIdeal
⊢ PrimeSpectrum.asIdeal (PrimeSpectrum.comap (algebraMap R S) { asIdeal := P, isPrime := hP : PrimeSpectrum S }) =
    p.asIdeal

Tactic:
h.over.symm

Premises used: Ideal.LiesOver.over, Ideal.comap, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h_1 : HasGoingDown R S
Q : PrimeSpectrum S
p : PrimeSpectrum R
hp : p ≤ PrimeSpectrum.comap (algebraMap R S) Q
P : Ideal S
hle : P ≤ Q.asIdeal
hP : P.IsPrime
h : P.LiesOver p.asIdeal
⊢ PrimeSpectrum.asIdeal (PrimeSpectrum.comap (algebraMap R S) { asIdeal := P, isPrime := hP : PrimeSpectrum S }) =
    p.asIdeal

Tactic:
exact h.over.symm

Premises used: Ideal.LiesOver.over, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : GeneralizingMap (X := PrimeSpectrum S) (Y := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
p : Ideal R
hp : p.IsPrime
Q : Ideal S
hQ : Q.IsPrime
hlt : p < Ideal.under R Q
⊢ { asIdeal := p, isPrime := hp : PrimeSpectrum R } ⤳
    PrimeSpectrum.comap (algebraMap R S) { asIdeal := Q, isPrime := hQ : PrimeSpectrum S }

Tactic:
have : (⟨p, hp⟩ : PrimeSpectrum R) ⤳ (PrimeSpectrum.comap (algebraMap R S) ⟨Q, hQ⟩) :=
      (PrimeSpectrum.le_iff_specializes _ _).mp hlt.le
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : GeneralizingMap (X := PrimeSpectrum S) (Y := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
p : Ideal R
hp : p.IsPrime
Q : Ideal S
hQ : Q.IsPrime
hlt : p < Ideal.under R Q
this :
  { asIdeal := p, isPrime := hp : PrimeSpectrum R } ⤳
    PrimeSpectrum.comap (algebraMap R S) { asIdeal := Q, isPrime := hQ : PrimeSpectrum S }
refine_2 :
  ∀ (P : PrimeSpectrum S) (hs : P ⤳ { asIdeal := Q, isPrime := hQ })
    (heq : PrimeSpectrum.comap (algebraMap R S) P = { asIdeal := p, isPrime := hp : PrimeSpectrum R }),
    ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
obtain ⟨P, hs, heq⟩ := h this
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : GeneralizingMap (X := PrimeSpectrum S) (Y := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
p : Ideal R
hp : p.IsPrime
Q : Ideal S
hQ : Q.IsPrime
hlt : p < Ideal.under R Q
this :
  { asIdeal := p, isPrime := hp : PrimeSpectrum R } ⤳
    PrimeSpectrum.comap (algebraMap R S) { asIdeal := Q, isPrime := hQ : PrimeSpectrum S }
P : PrimeSpectrum S
hs : P ⤳ { asIdeal := Q, isPrime := hQ }
heq : PrimeSpectrum.comap (algebraMap R S) P = { asIdeal := p, isPrime := hp : PrimeSpectrum R }
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
⟨P.asIdeal, (PrimeSpectrum.le_iff_specializes _ _).mpr hs, P.2, ⟨?_⟩⟩

Premises used: Iff.mpr, PrimeSpectrum.isPrime, Ideal.LiesOver.mk, PrimeSpectrum.le_iff_specializes, And.intro, Exists.intro, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : GeneralizingMap (X := PrimeSpectrum S) (Y := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
p : Ideal R
hp : p.IsPrime
Q : Ideal S
hQ : Q.IsPrime
hlt : p < Ideal.under R Q
this :
  { asIdeal := p, isPrime := hp : PrimeSpectrum R } ⤳
    PrimeSpectrum.comap (algebraMap R S) { asIdeal := Q, isPrime := hQ : PrimeSpectrum S }
P : PrimeSpectrum S
hs : P ⤳ { asIdeal := Q, isPrime := hQ }
heq : PrimeSpectrum.comap (algebraMap R S) P = { asIdeal := p, isPrime := hp : PrimeSpectrum R }
refine_2 : p = Ideal.under R P.asIdeal
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
refine ⟨P.asIdeal, (PrimeSpectrum.le_iff_specializes _ _).mpr hs, P.2, ⟨?_⟩⟩
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : GeneralizingMap (X := PrimeSpectrum S) (Y := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
p : Ideal R
hp : p.IsPrime
Q : Ideal S
hQ : Q.IsPrime
hlt : p < Ideal.under R Q
this :
  { asIdeal := p, isPrime := hp : PrimeSpectrum R } ⤳
    PrimeSpectrum.comap (algebraMap R S) { asIdeal := Q, isPrime := hQ : PrimeSpectrum S }
P : PrimeSpectrum S
hs : P ⤳ { asIdeal := Q, isPrime := hQ }
heq : PrimeSpectrum.comap (algebraMap R S) P = { asIdeal := p, isPrime := hp : PrimeSpectrum R }
⊢ p = Ideal.under R P.asIdeal

Tactic:
simpa [PrimeSpectrum.ext_iff] using heq.symm

Premises used: PrimeSpectrum.ext_iff, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : HasGoingDown R S
inst_8 : HasGoingDown S T
rw :
  GeneralizingMap (X := PrimeSpectrum T) (Y := PrimeSpectrum R)
    (PrimeSpectrum.comap (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap R S)))
⊢ HasGoingDown R T

Tactic:
rw [iff_generalizingMap_primeSpectrumComap, IsScalarTower.algebraMap_eq R S T]

Premises used: Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap, IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : HasGoingDown R S
inst_8 : HasGoingDown S T
simp :
  GeneralizingMap (X := PrimeSpectrum T) (Y := PrimeSpectrum R)
    (Function.comp (β := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.comap (algebraMap S T)))
⊢ GeneralizingMap (X := PrimeSpectrum T) (Y := PrimeSpectrum R)
    (PrimeSpectrum.comap (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap R S)))

Tactic:
simp only [PrimeSpectrum.comap_comp]

Premises used: PrimeSpectrum.comap_comp
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : HasGoingDown R S
inst_8 : HasGoingDown S T
hf : GeneralizingMap (X := PrimeSpectrum T) (Y := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap S T))
hg : GeneralizingMap (X := PrimeSpectrum S) (Y := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
⊢ GeneralizingMap (X := PrimeSpectrum T) (Y := PrimeSpectrum R)
    (Function.comp (β := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.comap (algebraMap S T)))

Tactic:
apply GeneralizingMap.comp

Premises used: GeneralizingMap.comp
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : HasGoingDown R S
inst_8 hf hf₁ hf₂ hf₃ : HasGoingDown S T
⊢ GeneralizingMap (X := PrimeSpectrum T) (Y := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap S T))

Tactic:
rwa [← iff_generalizingMap_primeSpectrumComap]

Premises used: Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : HasGoingDown R S
inst_8 : HasGoingDown S T
hg hg₁ hg₂ hg₃ : HasGoingDown R S
⊢ GeneralizingMap (X := PrimeSpectrum S) (Y := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))

Tactic:
rwa [← iff_generalizingMap_primeSpectrumComap]

Premises used: Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
H :
  ∀ (P : Ideal S) [inst_3 : P.IsPrime],
    Function.Surjective (α := PrimeSpectrum (Localization.AtPrime P)) (β :=
      PrimeSpectrum (Localization.AtPrime (Ideal.under R P)))
      (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
p : Ideal R
h : p.IsPrime
Q : Ideal S
h_1 : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (F := R →+* Localization.AtPrime (Ideal.under R Q)) (algebraMap R (Localization.AtPrime (Ideal.under R Q)))
    p
⊢ pl.IsPrime

Tactic:
have : pl.IsPrime :=
      Ideal.isPrime_map_of_isLocalizationAtPrime (Q.under R) hlt.le
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
H :
  ∀ (P : Ideal S) [inst_3 : P.IsPrime],
    Function.Surjective (α := PrimeSpectrum (Localization.AtPrime P)) (β :=
      PrimeSpectrum (Localization.AtPrime (Ideal.under R P)))
      (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
p : Ideal R
h : p.IsPrime
Q : Ideal S
h_1 : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (F := R →+* Localization.AtPrime (Ideal.under R Q)) (algebraMap R (Localization.AtPrime (Ideal.under R Q)))
    p
this : pl.IsPrime
obtain :
  ∀ (Pl : Ideal (Localization.AtPrime Q)) (isPrime : Pl.IsPrime)
    (hl :
      PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R Q) Q (algebraMap R S) ⋯)
          { asIdeal := Pl, isPrime := isPrime : PrimeSpectrum (Localization.AtPrime Q) } =
        { asIdeal := pl, isPrime := ⋯ : PrimeSpectrum (Localization.AtPrime (Ideal.under R Q)) }),
    ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
obtain ⟨⟨Pl, _⟩, hl⟩ := H Q ⟨pl, inferInstance⟩

Premises used: PrimeSpectrum.mk, inferInstance
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
H :
  ∀ (P : Ideal S) [inst_3 : P.IsPrime],
    Function.Surjective (α := PrimeSpectrum (Localization.AtPrime P)) (β :=
      PrimeSpectrum (Localization.AtPrime (Ideal.under R P)))
      (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
p : Ideal R
h : p.IsPrime
Q : Ideal S
h_1 : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (F := R →+* Localization.AtPrime (Ideal.under R Q)) (algebraMap R (Localization.AtPrime (Ideal.under R Q)))
    p
this : pl.IsPrime
Pl : Ideal (Localization.AtPrime Q)
isPrime : Pl.IsPrime
hl :
  PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R Q) Q (algebraMap R S) ⋯)
      { asIdeal := Pl, isPrime := isPrime : PrimeSpectrum (Localization.AtPrime Q) } =
    { asIdeal := pl, isPrime := ⋯ : PrimeSpectrum (Localization.AtPrime (Ideal.under R Q)) }
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
⟨Pl.under S, ?_, Ideal.IsPrime.under S Pl, ⟨?_⟩⟩

Premises used: Ideal.LiesOver.mk, And.intro, Exists.intro, Ideal.IsPrime.under, Ideal.under
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
H :
  ∀ (P : Ideal S) [inst_3 : P.IsPrime],
    Function.Surjective (α := PrimeSpectrum (Localization.AtPrime P)) (β :=
      PrimeSpectrum (Localization.AtPrime (Ideal.under R P)))
      (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
p : Ideal R
h : p.IsPrime
Q : Ideal S
h_1 : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (F := R →+* Localization.AtPrime (Ideal.under R Q)) (algebraMap R (Localization.AtPrime (Ideal.under R Q)))
    p
this : pl.IsPrime
Pl : Ideal (Localization.AtPrime Q)
isPrime : Pl.IsPrime
hl :
  PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R Q) Q (algebraMap R S) ⋯)
      { asIdeal := Pl, isPrime := isPrime : PrimeSpectrum (Localization.AtPrime Q) } =
    { asIdeal := pl, isPrime := ⋯ : PrimeSpectrum (Localization.AtPrime (Ideal.under R Q)) }
refine_1 : Ideal.under S Pl ≤ Q
refine_2 : p = Ideal.under R (Ideal.under S Pl)
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
refine ⟨Pl.under S, ?_, Ideal.IsPrime.under S Pl, ⟨?_⟩⟩
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
H :
  ∀ (P : Ideal S) [inst_3 : P.IsPrime],
    Function.Surjective (α := PrimeSpectrum (Localization.AtPrime P)) (β :=
      PrimeSpectrum (Localization.AtPrime (Ideal.under R P)))
      (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
p : Ideal R
h : p.IsPrime
Q : Ideal S
h_1 : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (F := R →+* Localization.AtPrime (Ideal.under R Q)) (algebraMap R (Localization.AtPrime (Ideal.under R Q)))
    p
this : pl.IsPrime
Pl : Ideal (Localization.AtPrime Q)
isPrime : Pl.IsPrime
hl :
  PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R Q) Q (algebraMap R S) ⋯)
      { asIdeal := Pl, isPrime := isPrime : PrimeSpectrum (Localization.AtPrime Q) } =
    { asIdeal := pl, isPrime := ⋯ : PrimeSpectrum (Localization.AtPrime (Ideal.under R Q)) }
⊢ Ideal.under S Pl ≤ Q

Tactic:
(IsLocalization.AtPrime.orderIsoOfPrime _ Q ⟨Pl, inferInstance⟩).2.2

Premises used: IsLocalization.AtPrime.orderIsoOfPrime, Set.Mem, inferInstance, Subtype.mk, And.right, DFunLike.coe, Subtype.property
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
H :
  ∀ (P : Ideal S) [inst_3 : P.IsPrime],
    Function.Surjective (α := PrimeSpectrum (Localization.AtPrime P)) (β :=
      PrimeSpectrum (Localization.AtPrime (Ideal.under R P)))
      (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
p : Ideal R
h : p.IsPrime
Q : Ideal S
h_1 : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (F := R →+* Localization.AtPrime (Ideal.under R Q)) (algebraMap R (Localization.AtPrime (Ideal.under R Q)))
    p
this : pl.IsPrime
Pl : Ideal (Localization.AtPrime Q)
isPrime : Pl.IsPrime
hl :
  PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R Q) Q (algebraMap R S) ⋯)
      { asIdeal := Pl, isPrime := isPrime : PrimeSpectrum (Localization.AtPrime Q) } =
    { asIdeal := pl, isPrime := ⋯ : PrimeSpectrum (Localization.AtPrime (Ideal.under R Q)) }
⊢ Ideal.under S Pl ≤ Q

Tactic:
exact (IsLocalization.AtPrime.orderIsoOfPrime _ Q ⟨Pl, inferInstance⟩).2.2

Premises used: IsLocalization.AtPrime.orderIsoOfPrime, inferInstance, Subtype.mk, And.right, DFunLike.coe, Subtype.property
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
H :
  ∀ (P : Ideal S) [inst_3 : P.IsPrime],
    Function.Surjective (α := PrimeSpectrum (Localization.AtPrime P)) (β :=
      PrimeSpectrum (Localization.AtPrime (Ideal.under R P)))
      (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
p : Ideal R
h : p.IsPrime
Q : Ideal S
h_1 : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (F := R →+* Localization.AtPrime (Ideal.under R Q)) (algebraMap R (Localization.AtPrime (Ideal.under R Q)))
    p
this_1 : pl.IsPrime
Pl : Ideal (Localization.AtPrime Q)
isPrime : Pl.IsPrime
hl :
  PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R Q) Q (algebraMap R S) ⋯)
      { asIdeal := Pl, isPrime := isPrime : PrimeSpectrum (Localization.AtPrime Q) } =
    { asIdeal := pl, isPrime := ⋯ : PrimeSpectrum (Localization.AtPrime (Ideal.under R Q)) }
this : Algebra.{u_3, u_4} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
⊢ Ideal.under (Localization.AtPrime (Ideal.under R Q)) Pl = pl

Tactic:
simpa [PrimeSpectrum.ext_iff] using hl

Premises used: PrimeSpectrum.ext_iff
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
H :
  ∀ (P : Ideal S) [inst_3 : P.IsPrime],
    Function.Surjective (α := PrimeSpectrum (Localization.AtPrime P)) (β :=
      PrimeSpectrum (Localization.AtPrime (Ideal.under R P)))
      (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
p : Ideal R
h : p.IsPrime
Q : Ideal S
h_1 : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (F := R →+* Localization.AtPrime (Ideal.under R Q)) (algebraMap R (Localization.AtPrime (Ideal.under R Q)))
    p
this_1 : pl.IsPrime
Pl : Ideal (Localization.AtPrime Q)
isPrime : Pl.IsPrime
hl :
  PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R Q) Q (algebraMap R S) ⋯)
      { asIdeal := Pl, isPrime := isPrime : PrimeSpectrum (Localization.AtPrime Q) } =
    { asIdeal := pl, isPrime := ⋯ : PrimeSpectrum (Localization.AtPrime (Ideal.under R Q)) }
this : Algebra.{u_3, u_4} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
⊢ Ideal.under (Localization.AtPrime (Ideal.under R Q)) Pl = pl

Tactic:
replace hl : Pl.under _ = pl := by simpa [PrimeSpectrum.ext_iff] using hl
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
H :
  ∀ (P : Ideal S) [inst_3 : P.IsPrime],
    Function.Surjective (α := PrimeSpectrum (Localization.AtPrime P)) (β :=
      PrimeSpectrum (Localization.AtPrime (Ideal.under R P)))
      (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
p : Ideal R
h : p.IsPrime
Q : Ideal S
h_1 : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (F := R →+* Localization.AtPrime (Ideal.under R Q)) (algebraMap R (Localization.AtPrime (Ideal.under R Q)))
    p
this_1 : pl.IsPrime
Pl : Ideal (Localization.AtPrime Q)
isPrime : Pl.IsPrime
this : Algebra.{u_3, u_4} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
hl : Ideal.under (Localization.AtPrime (Ideal.under R Q)) Pl = pl
refine_2 : p = Ideal.under R Pl
refine_2₁ :
  p =
    Ideal.under R (B := Localization.AtPrime (Ideal.under R Q))
      (Ideal.under (Localization.AtPrime (Ideal.under R Q)) Pl)
refine_2₂ : p = Ideal.under R pl
refine_2₃ refine_2₄ : p = p
⊢ p = Ideal.under R (Ideal.under S Pl)

Tactic:
rw [Ideal.under_under, ← Ideal.under_under (B := (Localization.AtPrime <| Q.under R)) Pl, hl,
        Ideal.under_map_of_isLocalizationAtPrime (Q.under R) hlt.le]

Premises used: Ideal.under_under, Ideal.under_map_of_isLocalizationAtPrime, LT.lt.le, Ideal.under
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R : Type u_3
S : Type u_4
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
inst_6 : Module.Flat R S
H :
  ∀ (P : Ideal S) [inst : P.IsPrime],
    Function.Surjective (α := PrimeSpectrum (Localization.AtPrime P)) (β :=
      PrimeSpectrum (Localization.AtPrime (Ideal.under R P)))
      (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
⊢ HasGoingDown R S

Tactic:
apply of_comap_localRingHom_surjective

Premises used: Algebra.HasGoingDown.of_comap_localRingHom_surjective
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R : Type u_3
S : Type u_4
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
inst_6 : Module.Flat R S
P : Ideal S
hP : P.IsPrime
this : Algebra.{u_3, u_4} (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) P
rw :
  IsLocalHom (R := Localization.AtPrime (Ideal.under R P)) (S := Localization.AtPrime P) (F :=
    RingHom.{u_3, u_4} (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P))
    (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯)
⊢ IsLocalHom (R := Localization.AtPrime (Ideal.under R P)) (S := Localization.AtPrime P) (F :=
    RingHom.{u_3, u_4} (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P))
    (algebraMap (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P))

Tactic:
rw [RingHom.algebraMap_toAlgebra]

Premises used: RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R : Type u_3
S : Type u_4
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
inst_6 : Module.Flat R S
P : Ideal S
hP : P.IsPrime
this : Algebra.{u_3, u_4} (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) P
⊢ IsLocalHom (R := Localization.AtPrime (Ideal.under R P)) (S := Localization.AtPrime P) (F :=
    RingHom.{u_3, u_4} (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P))
    (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯)

Tactic:
Localization.isLocalHom_localRingHom (P.under R) P (algebraMap R S) Ideal.LiesOver.over

Premises used: Algebra.algebraMap, Ideal.LiesOver.over, Localization.isLocalHom_localRingHom, Ideal.under
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R : Type u_3
S : Type u_4
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
inst_6 : Module.Flat R S
P : Ideal S
hP : P.IsPrime
this : Algebra.{u_3, u_4} (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) P
⊢ IsLocalHom (R := Localization.AtPrime (Ideal.under R P)) (S := Localization.AtPrime P) (F :=
    RingHom.{u_3, u_4} (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P))
    (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯)

Tactic:
exact Localization.isLocalHom_localRingHom (P.under R) P (algebraMap R S) Ideal.LiesOver.over

Premises used: Algebra.algebraMap, Ideal.LiesOver.over, Localization.isLocalHom_localRingHom, Ideal.under
-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R : Type u_3
S : Type u_4
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
inst_6 : Module.Flat R S
P : Ideal S
hP : P.IsPrime
this : Algebra.{u_3, u_4} (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) P
⊢ IsLocalHom (R := Localization.AtPrime (Ideal.under R P)) (S := Localization.AtPrime P) (F :=
    RingHom.{u_3, u_4} (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P))
    (algebraMap (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P))

Tactic:
have : IsLocalHom (algebraMap (Localization.AtPrime <| P.under R) (Localization.AtPrime P)) := by
    rw [RingHom.algebraMap_toAlgebra]
    exact Localization.isLocalHom_localRingHom (P.under R) P (algebraMap R S) Ideal.LiesOver.over