-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem localization_specComap_injective [Algebra R S] (M : Submonoid R) [IsLocalization M S] :
    Function.Injective (algebraMap R S).specComap

Proof state:
case asIdeal
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
p q : PrimeSpectrum S
h : p.asIdeal = q.asIdeal
⊢ p.asIdeal = q.asIdeal

Tactic:
exact h

Result:
no goals

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
p q : PrimeSpectrum S
h :
  (fun x => Ideal.map (algebraMap R S) x.asIdeal) ((algebraMap R S).specComap p) =
    (fun x => Ideal.map (algebraMap R S) x.asIdeal) ((algebraMap R S).specComap q)
⊢ p = q

Tactic:
dsimp only [RingHom.specComap] at h

Result:
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
p q : PrimeSpectrum S
h :
  Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) p.asIdeal) =
    Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) q.asIdeal)
⊢ p = q

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
p q : PrimeSpectrum S
h :
  Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) p.asIdeal) =
    Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) q.asIdeal)
⊢ p = q

Tactic:
rw [IsLocalization.map_comap M S, IsLocalization.map_comap M S] at h

Result:
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
p q : PrimeSpectrum S
h : p.asIdeal = q.asIdeal
⊢ p = q

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
p q : PrimeSpectrum S
h : (algebraMap R S).specComap p = (algebraMap R S).specComap q
⊢ p = q

Tactic:
replace h := _root_.congr_arg (fun x : PrimeSpectrum R => Ideal.map (algebraMap R S) x.asIdeal) h

Result:
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
p q : PrimeSpectrum S
h :
  (fun x => Ideal.map (algebraMap R S) x.asIdeal) ((algebraMap R S).specComap p) =
    (fun x => Ideal.map (algebraMap R S) x.asIdeal) ((algebraMap R S).specComap q)
⊢ p = q

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
⊢ Function.Injective (algebraMap R S).specComap

Tactic:
intro p q h

Result:
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
p q : PrimeSpectrum S
h : (algebraMap R S).specComap p = (algebraMap R S).specComap q
⊢ p = q

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
p q : PrimeSpectrum S
h : p.asIdeal = q.asIdeal
⊢ p = q

Tactic:
ext1

Result:
case asIdeal
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
p q : PrimeSpectrum S
h : p.asIdeal = q.asIdeal
⊢ p.asIdeal = q.asIdeal