-- Mathlib/RingTheory/Valuation/LocalSubring.lean
@[stacks 00IC]
lemma LocalSubring.mem_of_isMax_of_isIntegral {R : LocalSubring K}
    (hR : IsMax R) {x : K} (hx : IsIntegral R.toSubring x) : x ∈ R.toSubring

Proof state:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
this✝ : Algebra.IsIntegral ↥R.toSubring ↥S
this : FaithfulSMul ↥R.toSubring ↥S
Q : Ideal ↥S.toSubring
hQ : Q.IsMaximal
e : Ideal.comap (algebraMap ↥R.toSubring ↥S) Q = maximalIdeal ↥R.toSubring
hRS : R.toSubring ≤ S.toSubring
⊢ R = ofPrime S.toSubring Q

Tactic:
apply hR.eq_of_le ⟨hRS.trans (LocalSubring.le_ofPrime _ _), ⟨?_⟩⟩

Result:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
this✝ : Algebra.IsIntegral ↥R.toSubring ↥S
this : FaithfulSMul ↥R.toSubring ↥S
Q : Ideal ↥S.toSubring
hQ : Q.IsMaximal
e : Ideal.comap (algebraMap ↥R.toSubring ↥S) Q = maximalIdeal ↥R.toSubring
hRS : R.toSubring ≤ S.toSubring
⊢ ∀ (a : ↥R.toSubring), IsUnit ((Subring.inclusion ⋯) a) → IsUnit a

Proof state:
case intro.intro
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
this✝¹ : Algebra.IsIntegral ↥R.toSubring ↥S
this✝ : FaithfulSMul ↥R.toSubring ↥S
Q : Ideal ↥S.toSubring
hQ : Q.IsMaximal
e : Ideal.comap (algebraMap ↥R.toSubring ↥S) Q = maximalIdeal ↥R.toSubring
this : R = ofPrime S.toSubring Q
⊢ x ∈ R.toSubring

Tactic:
rw [this]

Result:
case intro.intro
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
this✝¹ : Algebra.IsIntegral ↥R.toSubring ↥S
this✝ : FaithfulSMul ↥R.toSubring ↥S
Q : Ideal ↥S.toSubring
hQ : Q.IsMaximal
e : Ideal.comap (algebraMap ↥R.toSubring ↥S) Q = maximalIdeal ↥R.toSubring
this : R = ofPrime S.toSubring Q
⊢ x ∈ (ofPrime S.toSubring Q).toSubring

Proof state:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
this✝ : Algebra.IsIntegral ↥R.toSubring ↥S
this : FaithfulSMul ↥R.toSubring ↥S
Q : Ideal ↥S.toSubring
hQ : Q.IsMaximal
e : Ideal.comap (algebraMap ↥R.toSubring ↥S) Q = maximalIdeal ↥R.toSubring
hRS : R.toSubring ≤ S.toSubring
⊢ ∀ (a : ↥R.toSubring), IsUnit ((Subring.inclusion ⋯) a) → IsUnit a

Tactic:
intro r hr

Result:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
this✝ : Algebra.IsIntegral ↥R.toSubring ↥S
this : FaithfulSMul ↥R.toSubring ↥S
Q : Ideal ↥S.toSubring
hQ : Q.IsMaximal
e : Ideal.comap (algebraMap ↥R.toSubring ↥S) Q = maximalIdeal ↥R.toSubring
hRS : R.toSubring ≤ S.toSubring
r : ↥R.toSubring
hr : IsUnit ((Subring.inclusion ⋯) r)
⊢ IsUnit r

Proof state:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
this✝¹ : Algebra.IsIntegral ↥R.toSubring ↥S
this✝ : FaithfulSMul ↥R.toSubring ↥S
Q : Ideal ↥S.toSubring
hQ : Q.IsMaximal
e : Ideal.comap (algebraMap ↥R.toSubring ↥S) Q = maximalIdeal ↥R.toSubring
hRS : R.toSubring ≤ S.toSubring
r : ↥R.toSubring
hr : IsUnit ((Subring.inclusion ⋯) r)
this : ⟨↑r, ⋯⟩ ∈ Q.primeCompl
h : ¬IsUnit r
⊢ False

Tactic:
rw [← mem_nonunits_iff, ← mem_maximalIdeal, ← e] at h

Result:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
this✝¹ : Algebra.IsIntegral ↥R.toSubring ↥S
this✝ : FaithfulSMul ↥R.toSubring ↥S
Q : Ideal ↥S.toSubring
hQ : Q.IsMaximal
e : Ideal.comap (algebraMap ↥R.toSubring ↥S) Q = maximalIdeal ↥R.toSubring
hRS : R.toSubring ≤ S.toSubring
r : ↥R.toSubring
hr : IsUnit ((Subring.inclusion ⋯) r)
this : ⟨↑r, ⋯⟩ ∈ Q.primeCompl
h : r ∈ Ideal.comap (algebraMap ↥R.toSubring ↥S) Q
⊢ False

Proof state:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
this✝ : Algebra.IsIntegral ↥R.toSubring ↥S
this : FaithfulSMul ↥R.toSubring ↥S
⊢ x ∈ R.toSubring

Tactic:
obtain ⟨Q : Ideal S.toSubring, hQ, e⟩ := Ideal.exists_ideal_over_maximal_of_isIntegral
  (R := R.toSubring) (S := S) (maximalIdeal _) (le_maximalIdeal (by simp))

Result:
case intro.intro
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
this✝ : Algebra.IsIntegral ↥R.toSubring ↥S
this : FaithfulSMul ↥R.toSubring ↥S
Q : Ideal ↥S.toSubring
hQ : Q.IsMaximal
e : Ideal.comap (algebraMap ↥R.toSubring ↥S) Q = maximalIdeal ↥R.toSubring
⊢ x ∈ R.toSubring

Proof state:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
this✝ : Algebra.IsIntegral ↥R.toSubring ↥S
this : FaithfulSMul ↥R.toSubring ↥S
Q : Ideal ↥S.toSubring
hQ : Q.IsMaximal
e : Ideal.comap (algebraMap ↥R.toSubring ↥S) Q = maximalIdeal ↥R.toSubring
⊢ R = ofPrime S.toSubring Q

Tactic:
have hRS : R.toSubring ≤ S.toSubring := fun r hr ↦ algebraMap_mem S ⟨r, hr⟩

Result:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
this✝ : Algebra.IsIntegral ↥R.toSubring ↥S
this : FaithfulSMul ↥R.toSubring ↥S
Q : Ideal ↥S.toSubring
hQ : Q.IsMaximal
e : Ideal.comap (algebraMap ↥R.toSubring ↥S) Q = maximalIdeal ↥R.toSubring
hRS : R.toSubring ≤ S.toSubring
⊢ R = ofPrime S.toSubring Q

Proof state:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
this✝¹ : Algebra.IsIntegral ↥R.toSubring ↥S
this✝ : FaithfulSMul ↥R.toSubring ↥S
Q : Ideal ↥S.toSubring
hQ : Q.IsMaximal
e : Ideal.comap (algebraMap ↥R.toSubring ↥S) Q = maximalIdeal ↥R.toSubring
hRS : R.toSubring ≤ S.toSubring
r : ↥R.toSubring
hr : IsUnit ((Subring.inclusion ⋯) r)
this : ⟨↑r, ⋯⟩ ∈ Q.primeCompl
h : r ∈ Ideal.comap (algebraMap ↥R.toSubring ↥S) Q
⊢ False

Tactic:
exact this h

Result:
no goals

Proof state:
case intro.intro
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
this✝¹ : Algebra.IsIntegral ↥R.toSubring ↥S
this✝ : FaithfulSMul ↥R.toSubring ↥S
Q : Ideal ↥S.toSubring
hQ : Q.IsMaximal
e : Ideal.comap (algebraMap ↥R.toSubring ↥S) Q = maximalIdeal ↥R.toSubring
this : R = ofPrime S.toSubring Q
⊢ x ∈ (ofPrime S.toSubring Q).toSubring

Tactic:
exact LocalSubring.le_ofPrime _ _ (Algebra.self_mem_adjoin_singleton _ _)

Result:
no goals

Proof state:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
this✝ : Algebra.IsIntegral ↥R.toSubring ↥S
this : FaithfulSMul ↥R.toSubring ↥S
⊢ RingHom.ker (algebraMap ↥R.toSubring ↥S) ≠ ⊤

Tactic:
simp

Result:
no goals