awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (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.HasGoingDown R S
q : PrimeSpectrum R
P : Ideal S
inst_4 : P.IsPrime
lo :
  P.LiesOver
    (RelSeries.last (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        (RelSeries.singleton
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b}
          q)).asIdeal
⊢ RelSeries.length (r :=
        {x : PrimeSpectrum S × PrimeSpectrum S |
          match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
          | (a, b) => a < b})
        (RelSeries.singleton
          {x : PrimeSpectrum S × PrimeSpectrum S |
            match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
            | (a, b) => a < b}
          { asIdeal := P, isPrime := ⋯ : PrimeSpectrum S }) =
      RelSeries.length (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        (RelSeries.singleton
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b}
          q) ∧
    RelSeries.last (r :=
          {x : PrimeSpectrum S × PrimeSpectrum S |
            match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
            | (a, b) => a < b})
          (RelSeries.singleton
            {x : PrimeSpectrum S × PrimeSpectrum S |
              match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
              | (a, b) => a < b}
            { asIdeal := P, isPrime := ⋯ : PrimeSpectrum S }) =
        { asIdeal := P, isPrime := ⋯ } ∧
      List.map (PrimeSpectrum.comap (algebraMap R S))
          (RelSeries.toList (r :=
            {x : PrimeSpectrum S × PrimeSpectrum S |
              match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
              | (a, b) => a < b})
            (RelSeries.singleton
              {x : PrimeSpectrum S × PrimeSpectrum S |
                match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
                | (a, b) => a < b}
              { asIdeal := P, isPrime := ⋯ : PrimeSpectrum S })) =
        RelSeries.toList (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          (RelSeries.singleton
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b}
            q)
have h : PrimeSpectrum.comap (algebraMap R S) { asIdeal := P, isPrime := sorry : PrimeSpectrum S } = q
Tactic: simp only [RelSeries.singleton_length, RelSeries.last_singleton, RelSeries.toList_singleton,
      List.map_cons, List.map_nil, List.cons.injEq, and_true, true_and]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (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.HasGoingDown R S
q : PrimeSpectrum R
P : Ideal S
inst_4 : P.IsPrime
lo :
  P.LiesOver
    (RelSeries.last (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        (RelSeries.singleton
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b}
          q)).asIdeal
⊢ PrimeSpectrum.comap (algebraMap R S) { asIdeal := P, isPrime := ⋯ : PrimeSpectrum S } = q
have h : PrimeSpectrum.asIdeal (PrimeSpectrum.comap (algebraMap R S) { asIdeal := P, isPrime := sorry : PrimeSpectrum S }) =
  q.asIdeal
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (goal)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ HasGoingDown R S ↔
    GeneralizingMap (X := PrimeSpectrum S) (Y := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
have refine_1 : HasGoingDown R S → GeneralizingMap (X := PrimeSpectrum S) (Y := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
Tactic: refine ⟨?_, fun h ↦ ⟨fun {p} hp Q hQ hlt ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (goal)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
refine_1 :
  HasGoingDown R S →
    GeneralizingMap (X := PrimeSpectrum S) (Y := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
⊢ HasGoingDown R S ↔
    GeneralizingMap (X := PrimeSpectrum S) (Y := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
have refine_2 : ∀ (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),
  ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
Tactic: refine ⟨?_, fun h ↦ ⟨fun {p} hp Q hQ hlt ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (hypothesis)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : HasGoingDown R S
Q : PrimeSpectrum S
p : PrimeSpectrum R
hp : p ⤳ PrimeSpectrum.comap (algebraMap R S) Q
⊢ ∃ (a' : PrimeSpectrum S), (fun (x1 x2 : PrimeSpectrum S) ↦ x1 ⤳ x2) a' Q ∧ PrimeSpectrum.comap (algebraMap R S) a' = p
have hp₁ : p ≤ PrimeSpectrum.comap (algebraMap R S) Q
Tactic: rw [← PrimeSpectrum.le_iff_specializes] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (goal)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : HasGoingDown R S
Q : PrimeSpectrum S
p : PrimeSpectrum R
hp : p ≤ PrimeSpectrum.comap (algebraMap R S) Q
⊢ ∃ (a' : PrimeSpectrum S), (fun (x1 x2 : PrimeSpectrum S) ↦ x1 ⤳ x2) a' Q ∧ PrimeSpectrum.comap (algebraMap R S) a' = p
have refine_1 : ∀ (P : Ideal S) (hle : P ≤ Q.asIdeal) (hP : P.IsPrime) (h : P.LiesOver p.asIdeal),
  ∃ (a' : PrimeSpectrum S), (fun (x1 x2 : PrimeSpectrum S) ↦ x1 ⤳ x2) a' Q ∧ PrimeSpectrum.comap (algebraMap R S) a' = p
Tactic: obtain ⟨P, hle, hP, h⟩ := Q.asIdeal.exists_ideal_le_liesOver_of_le (p := p.asIdeal)
      (q := Q.asIdeal.under R) hp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (goal)
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
⊢ ∃ (a' : PrimeSpectrum S), (fun (x1 x2 : PrimeSpectrum S) ↦ x1 ⤳ x2) a' Q ∧ PrimeSpectrum.comap (algebraMap R S) a' = p
have refine_1 : PrimeSpectrum.comap (algebraMap R S) { asIdeal := P, isPrime := hP : PrimeSpectrum S } = p
Tactic: refine ⟨⟨P, hP⟩, (PrimeSpectrum.le_iff_specializes _ Q).mp hle, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (goal)
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.comap (algebraMap R S) { asIdeal := P, isPrime := hP : PrimeSpectrum S } = p
have refine_1 : PrimeSpectrum.asIdeal (PrimeSpectrum.comap (algebraMap R S) { asIdeal := P, isPrime := hP : PrimeSpectrum S }) =
  p.asIdeal
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (hypothesis)
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
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
have this : { 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
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (goal)
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 ≤ Q, P.IsPrime ∧ P.LiesOver p
have 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
Tactic: obtain ⟨P, hs, heq⟩ := h this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (goal)
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
have refine_2 : p = Ideal.under R P.asIdeal
Tactic: refine ⟨P.asIdeal, (PrimeSpectrum.le_iff_specializes _ _).mpr hs, P.2, ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (goal)
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
⊢ HasGoingDown R T
have rw : GeneralizingMap (X := PrimeSpectrum T) (Y := PrimeSpectrum R)
  (PrimeSpectrum.comap (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap R S)))
Tactic: rw [iff_generalizingMap_primeSpectrumComap, IsScalarTower.algebraMap_eq R S T]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (goal)
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
⊢ GeneralizingMap (X := PrimeSpectrum T) (Y := PrimeSpectrum R)
    (PrimeSpectrum.comap (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap R S)))
have simp : GeneralizingMap (X := PrimeSpectrum T) (Y := PrimeSpectrum R)
  (Function.comp (β := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.comap (algebraMap S T)))
Tactic: simp only [PrimeSpectrum.comap_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (goal)
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
⊢ GeneralizingMap (X := PrimeSpectrum T) (Y := PrimeSpectrum R)
    (Function.comp (β := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.comap (algebraMap S T)))
have hf : GeneralizingMap (X := PrimeSpectrum T) (Y := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap S T))
Tactic: apply GeneralizingMap.comp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (goal)
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))
⊢ GeneralizingMap (X := PrimeSpectrum T) (Y := PrimeSpectrum R)
    (Function.comp (β := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.comap (algebraMap S T)))
have hg : GeneralizingMap (X := PrimeSpectrum S) (Y := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
Tactic: apply GeneralizingMap.comp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (hypothesis)
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
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
have this : pl.IsPrime
Tactic: have : pl.IsPrime :=
      Ideal.isPrime_map_of_isLocalizationAtPrime (Q.under R) hlt.le
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (goal)
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
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
have obtain : ∀ (Pl : Ideal (Localization.AtPrime Q)) (isPrime : Pl.IsPrime)
  (hl :
    PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R Q) Q (algebraMap R S) sorry)
        { asIdeal := Pl, isPrime := isPrime : PrimeSpectrum (Localization.AtPrime Q) } =
      { asIdeal := pl, isPrime := sorry : PrimeSpectrum (Localization.AtPrime (Ideal.under R Q)) }),
  ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
Tactic: obtain ⟨⟨Pl, _⟩, hl⟩ := H Q ⟨pl, inferInstance⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (goal)
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
have refine_1 : Ideal.under S Pl ≤ Q
Tactic: refine ⟨Pl.under S, ?_, Ideal.IsPrime.under S Pl, ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (goal)
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
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
have refine_2 : p = Ideal.under R (Ideal.under S Pl)
Tactic: refine ⟨Pl.under S, ?_, Ideal.IsPrime.under S Pl, ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (hypothesis)
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
⊢ p = Ideal.under R (Ideal.under S Pl)
have hl₁ : Ideal.under (Localization.AtPrime (Ideal.under R Q)) Pl = pl
Tactic: replace hl : Pl.under _ = pl := by simpa [PrimeSpectrum.ext_iff] using hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (goal)
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
⊢ p = Ideal.under R (Ideal.under S Pl)
have refine_2 : p = Ideal.under R 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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (goal)
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
⊢ p = Ideal.under R (Ideal.under S Pl)
have refine_2₁ : p =
  Ideal.under R (B := Localization.AtPrime (Ideal.under R Q)) (Ideal.under (Localization.AtPrime (Ideal.under R Q)) 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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (goal)
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)
⊢ p = Ideal.under R (Ideal.under S Pl)
have refine_2₂ : p = Ideal.under R 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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (goal)
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
⊢ p = Ideal.under R (Ideal.under S Pl)
have refine_2₃ : p = p
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]