-- Mathlib/RingTheory/Ideal/GoingDown.lean
/-- If for every prime of `S`, the map `Spec Sₚ → Spec Rₚ` is surjective,
the algebra satisfies going down. -/
lemma of_specComap_localRingHom_surjective
    (H : ∀ (P : Ideal S) [P.IsPrime], Function.Surjective
      (Localization.localRingHom (P.under R) P (algebraMap R S) rfl).specComap) :
    Algebra.HasGoingDown R S where
  exists_ideal_le_liesOver_of_lt {p} _ Q _ hlt

Proof state:
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H :
  ∀ (P : Ideal S) [inst : P.IsPrime],
    Function.Surjective (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯).specComap
p : Ideal R
x✝¹ : p.IsPrime
Q : Ideal S
x✝ : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (algebraMap R (Localization.AtPrime (Ideal.under R Q))) p
this : pl.IsPrime
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

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

Result:
case intro.mk
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H :
  ∀ (P : Ideal S) [inst : P.IsPrime],
    Function.Surjective (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯).specComap
p : Ideal R
x✝¹ : p.IsPrime
Q : Ideal S
x✝ : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (algebraMap R (Localization.AtPrime (Ideal.under R Q))) p
this : pl.IsPrime
Pl : Ideal (Localization.AtPrime Q)
isPrime✝ : Pl.IsPrime
hl :
  (Localization.localRingHom (Ideal.under R Q) Q (algebraMap R S) ⋯).specComap { asIdeal := Pl, isPrime := isPrime✝ } =
    { asIdeal := pl, isPrime := ⋯ }
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Proof state:
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H :
  ∀ (P : Ideal S) [inst : P.IsPrime],
    Function.Surjective (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯).specComap
p : Ideal R
x✝¹ : p.IsPrime
Q : Ideal S
x✝ : Q.IsPrime
hlt : p < Ideal.under R Q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
let pl : Ideal (Localization.AtPrime <| Q.under R) := p.map (algebraMap R _)

Result:
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H :
  ∀ (P : Ideal S) [inst : P.IsPrime],
    Function.Surjective (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯).specComap
p : Ideal R
x✝¹ : p.IsPrime
Q : Ideal S
x✝ : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (algebraMap R (Localization.AtPrime (Ideal.under R Q))) p
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Proof state:
case intro.mk.refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H :
  ∀ (P : Ideal S) [inst : P.IsPrime],
    Function.Surjective (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯).specComap
p : Ideal R
x✝¹ : p.IsPrime
Q : Ideal S
x✝ : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (algebraMap R (Localization.AtPrime (Ideal.under R Q))) p
this : pl.IsPrime
Pl : Ideal (Localization.AtPrime Q)
isPrime✝ : Pl.IsPrime
hl : Ideal.under (Localization.AtPrime (Ideal.under R Q)) Pl = pl
⊢ 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]

Result:
no goals

Proof state:
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H :
  ∀ (P : Ideal S) [inst : P.IsPrime],
    Function.Surjective (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯).specComap
p : Ideal R
x✝¹ : p.IsPrime
Q : Ideal S
x✝ : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (algebraMap R (Localization.AtPrime (Ideal.under R Q))) p
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
have : pl.IsPrime :=
  Ideal.isPrime_map_of_isLocalizationAtPrime (Q.under R) hlt.le

Result:
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H :
  ∀ (P : Ideal S) [inst : P.IsPrime],
    Function.Surjective (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯).specComap
p : Ideal R
x✝¹ : p.IsPrime
Q : Ideal S
x✝ : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (algebraMap R (Localization.AtPrime (Ideal.under R Q))) p
this : pl.IsPrime
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Proof state:
case intro.mk.refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H :
  ∀ (P : Ideal S) [inst : P.IsPrime],
    Function.Surjective (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯).specComap
p : Ideal R
x✝¹ : p.IsPrime
Q : Ideal S
x✝ : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (algebraMap R (Localization.AtPrime (Ideal.under R Q))) p
this : pl.IsPrime
Pl : Ideal (Localization.AtPrime Q)
isPrime✝ : Pl.IsPrime
hl :
  (Localization.localRingHom (Ideal.under R Q) Q (algebraMap R S) ⋯).specComap { asIdeal := Pl, isPrime := isPrime✝ } =
    { asIdeal := pl, isPrime := ⋯ }
⊢ p = Ideal.under R (Ideal.under S Pl)

Tactic:
replace hl : Pl.under _ = pl := by simpa using hl

Result:
case intro.mk.refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H :
  ∀ (P : Ideal S) [inst : P.IsPrime],
    Function.Surjective (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯).specComap
p : Ideal R
x✝¹ : p.IsPrime
Q : Ideal S
x✝ : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (algebraMap R (Localization.AtPrime (Ideal.under R Q))) p
this : pl.IsPrime
Pl : Ideal (Localization.AtPrime Q)
isPrime✝ : Pl.IsPrime
hl : Ideal.under (Localization.AtPrime (Ideal.under R Q)) Pl = pl
⊢ p = Ideal.under R (Ideal.under S Pl)