-- Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean
theorem Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective {f : R →+* S}
    (hf : Function.Injective f) (p) (H : p ∈ minimalPrimes R) :
    ∃ p' : Ideal S, p'.IsPrime ∧ p'.comap f = p

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Injective ⇑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : p.IsPrime
this : Nontrivial (Localization (Submonoid.map f p.primeCompl))
M : Ideal (Localization (Submonoid.map f p.primeCompl))
hM : M.IsMaximal
x : R
hx :
  x ∈
    comap (algebraMap R (Localization p.primeCompl))
      (comap (IsLocalization.map (Localization (Submonoid.map f p.primeCompl)) f ⋯) M)
h : x ∉ p
⊢ IsUnit
    ((IsLocalization.map (Localization (Submonoid.map f p.primeCompl)) f ⋯)
      ((algebraMap R (Localization p.primeCompl)) x))

Tactic:
apply IsUnit.map

Result:
case intro.h
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Injective ⇑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : p.IsPrime
this : Nontrivial (Localization (Submonoid.map f p.primeCompl))
M : Ideal (Localization (Submonoid.map f p.primeCompl))
hM : M.IsMaximal
x : R
hx :
  x ∈
    comap (algebraMap R (Localization p.primeCompl))
      (comap (IsLocalization.map (Localization (Submonoid.map f p.primeCompl)) f ⋯) M)
h : x ∉ p
⊢ IsUnit ((algebraMap R (Localization p.primeCompl)) x)

Proof state:
case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Injective ⇑f
p : Ideal R
H : p ∈ minimalPrimes R
this : p.IsPrime
⊢ 0 = (IsLocalization.map (Localization (Submonoid.map f p.primeCompl)) f ⋯) 0

Tactic:
rw [map_zero]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Injective ⇑f
p : Ideal R
H : p ∈ minimalPrimes R
this : p.IsPrime
⊢ Nontrivial (Localization (Submonoid.map f p.primeCompl))

Tactic:
refine ⟨⟨1, 0, ?_⟩⟩

Result:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Injective ⇑f
p : Ideal R
H : p ∈ minimalPrimes R
this : p.IsPrime
⊢ 1 ≠ 0

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Injective ⇑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : p.IsPrime
this : Nontrivial (Localization (Submonoid.map f p.primeCompl))
⊢ ∃ p', p'.IsPrime ∧ comap f p' = p

Tactic:
obtain ⟨M, hM⟩ := Ideal.exists_maximal (Localization (Submonoid.map f p.primeCompl))

Result:
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Injective ⇑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : p.IsPrime
this : Nontrivial (Localization (Submonoid.map f p.primeCompl))
M : Ideal (Localization (Submonoid.map f p.primeCompl))
hM : M.IsMaximal
⊢ ∃ p', p'.IsPrime ∧ comap f p' = p

Proof state:
case h.e'_2
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Injective ⇑f
p : Ideal R
H : p ∈ minimalPrimes R
this : p.IsPrime
⊢ 1 = (IsLocalization.map (Localization (Submonoid.map f p.primeCompl)) f ⋯) 1

Tactic:
rw [map_one]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Injective ⇑f
p : Ideal R
H : p ∈ minimalPrimes R
this : p.IsPrime
⊢ 1 ≠ 0

Tactic:
convert (IsLocalization.map_injective_of_injective p.primeCompl (Localization.AtPrime p)
    (Localization <| p.primeCompl.map f) hf).ne one_ne_zero

Result:
case h.e'_2
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Injective ⇑f
p : Ideal R
H : p ∈ minimalPrimes R
this : p.IsPrime
⊢ 1 = (IsLocalization.map (Localization (Submonoid.map f p.primeCompl)) f ⋯) 1

case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Injective ⇑f
p : Ideal R
H : p ∈ minimalPrimes R
this : p.IsPrime
⊢ 0 = (IsLocalization.map (Localization (Submonoid.map f p.primeCompl)) f ⋯) 0

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Injective ⇑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : p.IsPrime
this : Nontrivial (Localization (Submonoid.map f p.primeCompl))
M : Ideal (Localization (Submonoid.map f p.primeCompl))
hM : M.IsMaximal
x : R
hx :
  x ∈
    comap (algebraMap R (Localization p.primeCompl))
      (comap (IsLocalization.map (Localization (Submonoid.map f p.primeCompl)) f ⋯) M)
⊢ x ∈ p

Tactic:
by_contra h

Result:
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Injective ⇑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : p.IsPrime
this : Nontrivial (Localization (Submonoid.map f p.primeCompl))
M : Ideal (Localization (Submonoid.map f p.primeCompl))
hM : M.IsMaximal
x : R
hx :
  x ∈
    comap (algebraMap R (Localization p.primeCompl))
      (comap (IsLocalization.map (Localization (Submonoid.map f p.primeCompl)) f ⋯) M)
h : x ∉ p
⊢ False

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Injective ⇑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : p.IsPrime
this : Nontrivial (Localization (Submonoid.map f p.primeCompl))
M : Ideal (Localization (Submonoid.map f p.primeCompl))
hM : M.IsMaximal
⊢ ∃ p', p'.IsPrime ∧ comap f p' = p

Tactic:
refine ⟨M.comap (algebraMap S <| Localization (Submonoid.map f p.primeCompl)), inferInstance, ?_⟩

Result:
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Injective ⇑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : p.IsPrime
this : Nontrivial (Localization (Submonoid.map f p.primeCompl))
M : Ideal (Localization (Submonoid.map f p.primeCompl))
hM : M.IsMaximal
⊢ comap f (comap (algebraMap S (Localization (Submonoid.map f p.primeCompl))) M) = p