case refine'_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
⊢ T1Space (PrimeSpectrum R) → IsField R

case refine'_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
h : IsField R
⊢ T1Space (PrimeSpectrum R)
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
⊢ T1Space (PrimeSpectrum R) ↔ IsField R
refine' ⟨_, fun h => _⟩
case refine'_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
h : T1Space (PrimeSpectrum R)
⊢ IsField R
case refine'_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
⊢ T1Space (PrimeSpectrum R) → IsField R
intro h
case refine'_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
h : T1Space (PrimeSpectrum R)
hbot : Ideal.IsPrime ⊥
⊢ IsField R
case refine'_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
h : T1Space (PrimeSpectrum R)
⊢ IsField R
have hbot : Ideal.IsPrime (⊥ : Ideal R) := Ideal.bot_prime
no goals
case refine'_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
h : T1Space (PrimeSpectrum R)
hbot : Ideal.IsPrime ⊥
⊢ IsField R
exact
  Classical.not_not.1
    (mt
      (Ring.ne_bot_of_isMaximal_of_not_isField <|
        (isClosed_singleton_iff_isMaximal _).1 (T1Space.t1 ⟨⊥, hbot⟩))
      (by aesop))
no goals
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
h : T1Space (PrimeSpectrum R)
hbot : Ideal.IsPrime ⊥
⊢ ¬{ asIdeal := ⊥, IsPrime := hbot }.asIdeal ≠ ⊥
aesop
case refine'_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
h : IsField R
x : PrimeSpectrum R
⊢ Ideal.IsMaximal x.asIdeal
case refine'_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
h : IsField R
⊢ T1Space (PrimeSpectrum R)
refine' ⟨fun x => (isClosed_singleton_iff_isMaximal x).2 _⟩
case pos
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
h : IsField R
x : PrimeSpectrum R
hx : x.asIdeal = ⊥
⊢ Ideal.IsMaximal x.asIdeal

case neg
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
h : IsField R
x : PrimeSpectrum R
hx : ¬x.asIdeal = ⊥
⊢ Ideal.IsMaximal x.asIdeal
case refine'_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
h : IsField R
x : PrimeSpectrum R
⊢ Ideal.IsMaximal x.asIdeal
by_cases hx : x.asIdeal = ⊥
case pos
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
h : IsField R
x : PrimeSpectrum R
hx : x.asIdeal = ⊥
this : Field R := IsField.toField h
⊢ Ideal.IsMaximal x.asIdeal
case pos
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
h : IsField R
x : PrimeSpectrum R
hx : x.asIdeal = ⊥
⊢ Ideal.IsMaximal x.asIdeal
letI := h.toField
no goals
case pos
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
h : IsField R
x : PrimeSpectrum R
hx : x.asIdeal = ⊥
this : Field R := IsField.toField h
⊢ Ideal.IsMaximal x.asIdeal
exact hx.symm ▸ Ideal.bot_isMaximal
no goals
case neg
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
h : IsField R
x : PrimeSpectrum R
hx : ¬x.asIdeal = ⊥
⊢ Ideal.IsMaximal x.asIdeal
exact absurd h (Ring.not_isField_iff_exists_prime.2 ⟨x.asIdeal, ⟨hx, x.2⟩⟩)