R : Type ?u.41349
A : Type u_1
K : Type ?u.41355
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
P : Ideal A
hP : P ≠ ⊥
pP : Ideal.IsPrime P
Aₘ : Type u_2
inst✝² : CommRing Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
h : IsField Aₘ
⊢ False
R : Type ?u.41349
A : Type u_1
K : Type ?u.41355
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
P : Ideal A
hP : P ≠ ⊥
pP : Ideal.IsPrime P
Aₘ : Type u_2
inst✝² : CommRing Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
⊢ ¬IsField Aₘ
intro h
R : Type ?u.41349
A : Type u_1
K : Type ?u.41355
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
P : Ideal A
hP : P ≠ ⊥
pP : Ideal.IsPrime P
Aₘ : Type u_2
inst✝² : CommRing Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
h : IsField Aₘ
this : Field Aₘ := IsField.toField h
⊢ False
R : Type ?u.41349
A : Type u_1
K : Type ?u.41355
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
P : Ideal A
hP : P ≠ ⊥
pP : Ideal.IsPrime P
Aₘ : Type u_2
inst✝² : CommRing Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
h : IsField Aₘ
⊢ False
letI := h.toField
case intro.intro
R : Type ?u.41349
A : Type u_1
K : Type ?u.41355
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
P : Ideal A
hP : P ≠ ⊥
pP : Ideal.IsPrime P
Aₘ : Type u_2
inst✝² : CommRing Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
h : IsField Aₘ
this : Field Aₘ := IsField.toField h
x : A
x_mem : x ∈ P
x_ne : x ≠ 0
⊢ False
R : Type ?u.41349
A : Type u_1
K : Type ?u.41355
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
P : Ideal A
hP : P ≠ ⊥
pP : Ideal.IsPrime P
Aₘ : Type u_2
inst✝² : CommRing Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
h : IsField Aₘ
this : Field Aₘ := IsField.toField h
⊢ False
obtain ⟨x, x_mem, x_ne⟩ := P.ne_bot_iff.mp hP
no goals
case intro.intro
R : Type ?u.41349
A : Type u_1
K : Type ?u.41355
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
P : Ideal A
hP : P ≠ ⊥
pP : Ideal.IsPrime P
Aₘ : Type u_2
inst✝² : CommRing Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
h : IsField Aₘ
this : Field Aₘ := IsField.toField h
x : A
x_mem : x ∈ P
x_ne : x ≠ 0
⊢ False
exact
  (LocalRing.maximalIdeal.isMaximal _).ne_top
    (Ideal.eq_top_of_isUnit_mem _
      ((IsLocalization.AtPrime.to_map_mem_maximal_iff Aₘ P _).mpr x_mem)
      (isUnit_iff_ne_zero.mpr
        ((map_ne_zero_iff (algebraMap A Aₘ)
              (IsLocalization.injective Aₘ P.primeCompl_le_nonZeroDivisors)).mpr
          x_ne)))