-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem t1Space_iff_isField [IsDomain R] : T1Space (PrimeSpectrum R) ↔ IsField R

Proof state:
case pos
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
h : IsField R
x : PrimeSpectrum R
hx : x.asIdeal = ⊥
this : Semifield R := h.toSemifield
⊢ x.asIdeal.IsMaximal

Tactic:
exact hx.symm ▸ Ideal.bot_isMaximal

Result:
no goals

Proof state:
case refine_1
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
h : T1Space (PrimeSpectrum R)
⊢ IsField R

Tactic:
have hbot : Ideal.IsPrime (⊥ : Ideal R) := Ideal.bot_prime

Result:
case refine_1
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
h : T1Space (PrimeSpectrum R)
hbot : ⊥.IsPrime
⊢ IsField R

Proof state:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
⊢ T1Space (PrimeSpectrum R) ↔ IsField R

Tactic:
refine ⟨?_, fun h => ?_⟩

Result:
case refine_1
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
⊢ T1Space (PrimeSpectrum R) → IsField R

case refine_2
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
h : IsField R
⊢ T1Space (PrimeSpectrum R)

Proof state:
case refine_1
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
h : T1Space (PrimeSpectrum R)
hbot : ⊥.IsPrime
⊢ IsField R

Tactic:
exact
  Classical.not_not.1
    (mt
      (Ring.ne_bot_of_isMaximal_of_not_isField <|
        (isClosed_singleton_iff_isMaximal _).1 (T1Space.t1 ⟨⊥, hbot⟩))
      (by simp))

Result:
no goals

Proof state:
case refine_2
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
h : IsField R
x : PrimeSpectrum R
⊢ x.asIdeal.IsMaximal

Tactic:
by_cases hx : x.asIdeal = ⊥

Result:
case pos
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
h : IsField R
x : PrimeSpectrum R
hx : x.asIdeal = ⊥
⊢ x.asIdeal.IsMaximal

case neg
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
h : IsField R
x : PrimeSpectrum R
hx : ¬x.asIdeal = ⊥
⊢ x.asIdeal.IsMaximal

Proof state:
case refine_1
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
⊢ T1Space (PrimeSpectrum R) → IsField R

Tactic:
intro h

Result:
case refine_1
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
h : T1Space (PrimeSpectrum R)
⊢ IsField R

Proof state:
case refine_2
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
h : IsField R
⊢ T1Space (PrimeSpectrum R)

Tactic:
refine ⟨fun x => (isClosed_singleton_iff_isMaximal x).2 ?_⟩

Result:
case refine_2
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
h : IsField R
x : PrimeSpectrum R
⊢ x.asIdeal.IsMaximal

Proof state:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
h : T1Space (PrimeSpectrum R)
hbot : ⊥.IsPrime
⊢ ¬{ asIdeal := ⊥, isPrime := hbot }.asIdeal ≠ ⊥

Tactic:
simp

Result:
no goals

Proof state:
case neg
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
h : IsField R
x : PrimeSpectrum R
hx : ¬x.asIdeal = ⊥
⊢ x.asIdeal.IsMaximal

Tactic:
exact absurd h (Ring.not_isField_iff_exists_prime.2 ⟨x.asIdeal, ⟨hx, x.2⟩⟩)

Result:
no goals

Proof state:
case pos
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
h : IsField R
x : PrimeSpectrum R
hx : x.asIdeal = ⊥
⊢ x.asIdeal.IsMaximal

Tactic:
letI := h.toSemifield

Result:
case pos
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
h : IsField R
x : PrimeSpectrum R
hx : x.asIdeal = ⊥
this : Semifield R := h.toSemifield
⊢ x.asIdeal.IsMaximal