-- Mathlib/RingTheory/Unramified/Field.lean
theorem isField_of_isAlgClosed_of_isLocalRing
    [IsAlgClosed K] [IsLocalRing A] : IsField A

Proof state:
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
⊢ IsLocalRing.maximalIdeal A ≤ ⊥

Tactic:
intro x hx

Result:
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
x : A
hx : x ∈ IsLocalRing.maximalIdeal A
⊢ x ∈ ⊥

Proof state:
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
x : A
hx : x ∈ IsLocalRing.maximalIdeal A
⊢ x ∈ ⊥

Tactic:
obtain ⟨x, rfl⟩ := (bijective_of_isAlgClosed_of_isLocalRing K A).surjective x

Result:
case intro
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
x : K
hx : (algebraMap K A) x ∈ IsLocalRing.maximalIdeal A
⊢ (algebraMap K A) x ∈ ⊥

Proof state:
case intro
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
x : K
hx : (algebraMap K A) x ∈ IsLocalRing.maximalIdeal A
hx' : ¬(algebraMap K A) x = (algebraMap K A) 0
⊢ False

Tactic:
exact hx ((isUnit_iff_ne_zero.mpr
  (fun e ↦ hx' ((algebraMap K A).congr_arg e))).map (algebraMap K A))

Result:
no goals

Proof state:
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
⊢ IsField A

Tactic:
rw [IsLocalRing.isField_iff_maximalIdeal_eq, eq_bot_iff]

Result:
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
⊢ IsLocalRing.maximalIdeal A ≤ ⊥

Proof state:
case intro
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
x : K
hx : (algebraMap K A) x ∈ IsLocalRing.maximalIdeal A
⊢ (algebraMap K A) x = (algebraMap K A) 0

Tactic:
by_contra hx'

Result:
case intro
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
x : K
hx : (algebraMap K A) x ∈ IsLocalRing.maximalIdeal A
hx' : ¬(algebraMap K A) x = (algebraMap K A) 0
⊢ False

Proof state:
case intro
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
x : K
hx : (algebraMap K A) x ∈ IsLocalRing.maximalIdeal A
⊢ (algebraMap K A) x = 0

Tactic:
rw [← (algebraMap K A).map_zero]

Result:
case intro
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
x : K
hx : (algebraMap K A) x ∈ IsLocalRing.maximalIdeal A
⊢ (algebraMap K A) x = (algebraMap K A) 0

Proof state:
case intro
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
x : K
hx : (algebraMap K A) x ∈ IsLocalRing.maximalIdeal A
⊢ (algebraMap K A) x ∈ ⊥

Tactic:
show _ = 0

Result:
case intro
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
x : K
hx : (algebraMap K A) x ∈ IsLocalRing.maximalIdeal A
⊢ (algebraMap K A) x = 0