R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this : IsPrime p
⊢ ∃ p', IsPrime p' ∧ comap f p' = p
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
⊢ ∃ p', IsPrime p' ∧ comap f p' = p
have := H.1.1
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
⊢ ∃ p', IsPrime p' ∧ comap f p' = p
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
⊢ ∃ p', IsPrime p' ∧ comap f p' = p
obtain ⟨M, hM⟩ := Ideal.exists_maximal (Localization (Submonoid.map f p.primeCompl))
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
⊢ comap f (comap (algebraMap S (Localization (Submonoid.map f (primeCompl p)))) M) = p
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
⊢ ∃ p', IsPrime p' ∧ comap f p' = p
refine' ⟨M.comap (algebraMap S <| Localization (Submonoid.map f p.primeCompl)), inferInstance, _⟩
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
⊢ comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M) =
    p
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
⊢ comap f (comap (algebraMap S (Localization (Submonoid.map f (primeCompl p)))) M) = p
rw [Ideal.comap_comap, ← @IsLocalization.map_comp _ _ _ _ _ _ _ _ Localization.isLocalization
    _ _ _ _ p.primeCompl.le_comap_map _ Localization.isLocalization,
  ← Ideal.comap_comap]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
⊢ comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M) ≤
    p
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
⊢ comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M) =
    p
suffices _ ≤ p by exact this.antisymm (H.2 ⟨inferInstance, bot_le⟩ this)
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
x : R
hx :
  x ∈
    comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M)
⊢ x ∈ p
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
⊢ comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M) ≤
    p
intro x hx
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
x : R
hx :
  x ∈
    comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M)
h : ¬x ∈ p
⊢ False
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
x : R
hx :
  x ∈
    comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M)
⊢ x ∈ p
by_contra h
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
x : R
hx :
  x ∈
    comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M)
h : ¬x ∈ p
⊢ M = ⊤
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
x : R
hx :
  x ∈
    comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M)
h : ¬x ∈ p
⊢ False
apply hM.ne_top
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
x : R
hx :
  x ∈
    comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M)
h : ¬x ∈ p
⊢ IsUnit
    (↑(IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
      (↑(algebraMap R (Localization (primeCompl p))) x))
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
x : R
hx :
  x ∈
    comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M)
h : ¬x ∈ p
⊢ M = ⊤
apply M.eq_top_of_isUnit_mem hx
case intro.h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
x : R
hx :
  x ∈
    comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M)
h : ¬x ∈ p
⊢ IsUnit (↑(algebraMap R (Localization (primeCompl p))) x)
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
x : R
hx :
  x ∈
    comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M)
h : ¬x ∈ p
⊢ IsUnit
    (↑(IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
      (↑(algebraMap R (Localization (primeCompl p))) x))
apply IsUnit.map
no goals
case intro.h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
x : R
hx :
  x ∈
    comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M)
h : ¬x ∈ p
⊢ IsUnit (↑(algebraMap R (Localization (primeCompl p))) x)
apply IsLocalization.map_units _ (show p.primeCompl from ⟨x, h⟩)
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this : IsPrime p
⊢ 1 ≠ 0
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this : IsPrime p
⊢ Nontrivial (Localization (Submonoid.map f (primeCompl p)))
refine' ⟨⟨1, 0, _⟩⟩
case h.e'_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this : IsPrime p
⊢ 1 =
    ↑(IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
      1

case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this : IsPrime p
⊢ 0 =
    ↑(IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
      0
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this : IsPrime p
⊢ 1 ≠ 0
convert (IsLocalization.map_injective_of_injective p.primeCompl (Localization.AtPrime p)
    (Localization <| p.primeCompl.map f) hf).ne one_ne_zero
no goals
case h.e'_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this : IsPrime p
⊢ 1 =
    ↑(IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
      1
rw [map_one]
no goals
case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this : IsPrime p
⊢ 0 =
    ↑(IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
      0
rw [map_zero]
no goals
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝¹ : IsPrime p
this✝ : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
this : ?m.47324 ≤ p
⊢ comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M) =
    p
exact this.antisymm (H.2 ⟨inferInstance, bot_le⟩ this)