-- 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:
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
⊢ ∃ p', p'.IsPrime ∧ comap f p' = p

Tactic:
have := H.1.1

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
⊢ ∃ p', p'.IsPrime ∧ comap f p' = 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
⊢ comap (algebraMap R (Localization p.primeCompl))
      (comap (IsLocalization.map (Localization (Submonoid.map f p.primeCompl)) f ⋯) M) ≤
    p

Tactic:
intro x hx

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)
⊢ x ∈ p

Proof state:
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)

Tactic:
apply IsLocalization.map_units _ (show p.primeCompl from ⟨x, h⟩)

Result:
no goals

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
⊢ comap (algebraMap R (Localization p.primeCompl))
      (comap (IsLocalization.map (Localization (Submonoid.map f p.primeCompl)) f ⋯) M) =
    p

Tactic:
suffices _ ≤ p by exact this.antisymm (H.2 ⟨inferInstance, bot_le⟩ this)

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 (algebraMap R (Localization p.primeCompl))
      (comap (IsLocalization.map (Localization (Submonoid.map f p.primeCompl)) f ⋯) M) ≤
    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
⊢ False

Tactic:
apply hM.ne_top

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
⊢ M = ⊤

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
⊢ comap f (comap (algebraMap S (Localization (Submonoid.map f p.primeCompl))) M) = p

Tactic:
rw [Ideal.comap_comap, ← @IsLocalization.map_comp _ _ _ _ _ _ _ _ Localization.isLocalization
    _ _ _ _ _ Localization.isLocalization p.primeCompl.le_comap_map,
  ← Ideal.comap_comap]

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 (algebraMap R (Localization p.primeCompl))
      (comap (IsLocalization.map (Localization (Submonoid.map f p.primeCompl)) f ⋯) M) =
    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
⊢ M = ⊤

Tactic:
apply M.eq_top_of_isUnit_mem hx

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
⊢ IsUnit
    ((IsLocalization.map (Localization (Submonoid.map f p.primeCompl)) f ⋯)
      ((algebraMap R (Localization p.primeCompl)) x))

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))
M : Ideal (Localization (Submonoid.map f p.primeCompl))
hM : M.IsMaximal
this : ?m.37890 ≤ p
⊢ comap (algebraMap R (Localization p.primeCompl))
      (comap (IsLocalization.map (Localization (Submonoid.map f p.primeCompl)) f ⋯) M) =
    p

Tactic:
exact this.antisymm (H.2 ⟨inferInstance, bot_le⟩ this)

Result:
no goals