-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem localization_specComap_range [Algebra R S] (M : Submonoid R) [IsLocalization M S] :
    Set.range (algebraMap R S).specComap = { p | Disjoint (M : Set R) p.asIdeal }

Proof state:
case h
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
⊢ x ∈ Set.range (algebraMap R S).specComap ↔ x ∈ {p | Disjoint ↑M ↑p.asIdeal}

Tactic:
constructor

Result:
case h.mp
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
⊢ x ∈ Set.range (algebraMap R S).specComap → x ∈ {p | Disjoint ↑M ↑p.asIdeal}

case h.mpr
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
⊢ x ∈ {p | Disjoint ↑M ↑p.asIdeal} → x ∈ Set.range (algebraMap R S).specComap

Proof state:
case h.mpr
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring 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 (algebraMap R S).specComap

Tactic:
use ⟨x.asIdeal.map (algebraMap R S), IsLocalization.isPrime_of_isPrime_disjoint M S _ x.2 h⟩

Result:
case h
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
h : x ∈ {p | Disjoint ↑M ↑p.asIdeal}
⊢ (algebraMap R S).specComap { asIdeal := Ideal.map (algebraMap R S) x.asIdeal, isPrime := ⋯ } = x

Proof state:
case h.asIdeal
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
h : x ∈ {p | Disjoint ↑M ↑p.asIdeal}
⊢ ((algebraMap R S).specComap { asIdeal := Ideal.map (algebraMap R S) x.asIdeal, isPrime := ⋯ }).asIdeal = x.asIdeal

Tactic:
exact IsLocalization.comap_map_of_isPrime_disjoint M S _ x.2 h

Result:
no goals

Proof state:
case h.mp.intro.intro
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
p : PrimeSpectrum S
x : R
hx₁ : x ∈ ↑M
hx₂ : x ∈ ↑((algebraMap R S).specComap p).asIdeal
⊢ x ∈ ⊥

Tactic:
exact (p.2.1 : ¬_) (p.asIdeal.eq_top_of_isUnit_mem hx₂ (IsLocalization.map_units S ⟨x, hx₁⟩))

Result:
no goals

Proof state:
case h
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
h : x ∈ {p | Disjoint ↑M ↑p.asIdeal}
⊢ (algebraMap R S).specComap { asIdeal := Ideal.map (algebraMap R S) x.asIdeal, isPrime := ⋯ } = x

Tactic:
ext1

Result:
case h.asIdeal
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
h : x ∈ {p | Disjoint ↑M ↑p.asIdeal}
⊢ ((algebraMap R S).specComap { asIdeal := Ideal.map (algebraMap R S) x.asIdeal, isPrime := ⋯ }).asIdeal = x.asIdeal

Proof state:
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ Set.range (algebraMap R S).specComap = {p | Disjoint ↑M ↑p.asIdeal}

Tactic:
ext x

Result:
case h
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
⊢ x ∈ Set.range (algebraMap R S).specComap ↔ x ∈ {p | Disjoint ↑M ↑p.asIdeal}

Proof state:
case h.mp
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
⊢ x ∈ Set.range (algebraMap R S).specComap → x ∈ {p | Disjoint ↑M ↑p.asIdeal}

Tactic:
simp_rw [disjoint_iff_inf_le]

Result:
case h.mp
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
⊢ x ∈ Set.range (algebraMap R S).specComap → x ∈ {p | ↑M ⊓ ↑p.asIdeal ≤ ⊥}

Proof state:
case h.mpr
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
⊢ x ∈ {p | Disjoint ↑M ↑p.asIdeal} → x ∈ Set.range (algebraMap R S).specComap

Tactic:
intro h

Result:
case h.mpr
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring 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 (algebraMap R S).specComap

Proof state:
case h.mp
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
⊢ x ∈ Set.range (algebraMap R S).specComap → x ∈ {p | ↑M ⊓ ↑p.asIdeal ≤ ⊥}

Tactic:
rintro ⟨p, rfl⟩ x ⟨hx₁, hx₂⟩

Result:
case h.mp.intro.intro
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
p : PrimeSpectrum S
x : R
hx₁ : x ∈ ↑M
hx₂ : x ∈ ↑((algebraMap R S).specComap p).asIdeal
⊢ x ∈ ⊥