case h
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.255999
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
⊢ x ∈ Set.range ↑(comap (algebraMap R S)) ↔ x ∈ {p | Disjoint ↑M ↑p.asIdeal}
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.255999
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ Set.range ↑(comap (algebraMap R S)) = {p | Disjoint ↑M ↑p.asIdeal}
ext x
case h.mp
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.255999
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
⊢ x ∈ Set.range ↑(comap (algebraMap R S)) → x ∈ {p | Disjoint ↑M ↑p.asIdeal}

case h.mpr
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.255999
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
⊢ x ∈ {p | Disjoint ↑M ↑p.asIdeal} → x ∈ Set.range ↑(comap (algebraMap R S))
case h
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.255999
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
⊢ x ∈ Set.range ↑(comap (algebraMap R S)) ↔ x ∈ {p | Disjoint ↑M ↑p.asIdeal}
constructor
case h.mp
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.255999
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
⊢ x ∈ Set.range ↑(comap (algebraMap R S)) → x ∈ {p | ↑M ⊓ ↑p.asIdeal ≤ ⊥}
case h.mp
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.255999
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
⊢ x ∈ Set.range ↑(comap (algebraMap R S)) → x ∈ {p | Disjoint ↑M ↑p.asIdeal}
simp_rw [disjoint_iff_inf_le]
case h.mp.intro.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.255999
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
p : PrimeSpectrum S
x : R
hx₁ : x ∈ ↑M
hx₂ : x ∈ ↑(↑(comap (algebraMap R S)) p).asIdeal
⊢ x ∈ ⊥
case h.mp
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.255999
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
⊢ x ∈ Set.range ↑(comap (algebraMap R S)) → x ∈ {p | ↑M ⊓ ↑p.asIdeal ≤ ⊥}
rintro ⟨p, rfl⟩ x ⟨hx₁, hx₂⟩
no goals
case h.mp.intro.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.255999
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
p : PrimeSpectrum S
x : R
hx₁ : x ∈ ↑M
hx₂ : x ∈ ↑(↑(comap (algebraMap R S)) p).asIdeal
⊢ x ∈ ⊥
exact (p.2.1 : ¬_) (p.asIdeal.eq_top_of_isUnit_mem hx₂ (IsLocalization.map_units S ⟨x, hx₁⟩))
case h.mpr
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.255999
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
h : x ∈ {p | Disjoint ↑M ↑p.asIdeal}
⊢ x ∈ Set.range ↑(comap (algebraMap R S))
case h.mpr
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.255999
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
⊢ x ∈ {p | Disjoint ↑M ↑p.asIdeal} → x ∈ Set.range ↑(comap (algebraMap R S))
intro h
case h.mpr
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.255999
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
h : x ∈ {p | Disjoint ↑M ↑p.asIdeal}
⊢ ↑(comap (algebraMap R S))
      { asIdeal := Ideal.map (algebraMap R S) x.asIdeal,
        IsPrime := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) x.asIdeal)) } =
    x
case h.mpr
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.255999
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
h : x ∈ {p | Disjoint ↑M ↑p.asIdeal}
⊢ x ∈ Set.range ↑(comap (algebraMap R S))
use ⟨x.asIdeal.map (algebraMap R S), IsLocalization.isPrime_of_isPrime_disjoint M S _ x.2 h⟩
case h.mpr.asIdeal
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.255999
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
h : x ∈ {p | Disjoint ↑M ↑p.asIdeal}
⊢ (↑(comap (algebraMap R S))
        { asIdeal := Ideal.map (algebraMap R S) x.asIdeal,
          IsPrime := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) x.asIdeal)) }).asIdeal =
    x.asIdeal
case h.mpr
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.255999
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
h : x ∈ {p | Disjoint ↑M ↑p.asIdeal}
⊢ ↑(comap (algebraMap R S))
      { asIdeal := Ideal.map (algebraMap R S) x.asIdeal,
        IsPrime := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) x.asIdeal)) } =
    x
ext1
no goals
case h.mpr.asIdeal
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.255999
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
h : x ∈ {p | Disjoint ↑M ↑p.asIdeal}
⊢ (↑(comap (algebraMap R S))
        { asIdeal := Ideal.map (algebraMap R S) x.asIdeal,
          IsPrime := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) x.asIdeal)) }).asIdeal =
    x.asIdeal
exact IsLocalization.comap_map_of_isPrime_disjoint M S _ x.2 h