-- 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 : ↥R.toSubring
hr : IsUnit ((Subring.inclusion ⋯) r)
⊢ IsUnit r

Tactic:
have := (IsLocalization.AtPrime.isUnit_to_map_iff (R := S.toSubring) _ Q ⟨_, hRS r.2⟩).mp 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)
this : ⟨↑r, ⋯⟩ ∈ Q.primeCompl
⊢ IsUnit r

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
⊢ x ∈ R.toSubring

Tactic:
have : R = .ofPrime S.toSubring Q := by
  have hRS : R.toSubring ≤ S.toSubring := fun r hr ↦ algebraMap_mem S ⟨r, hr⟩
  apply hR.eq_of_le ⟨hRS.trans (LocalSubring.le_ofPrime _ _), ⟨?_⟩⟩
  intro r hr
  have := (IsLocalization.AtPrime.isUnit_to_map_iff (R := S.toSubring) _ Q ⟨_, hRS r.2⟩).mp hr
  by_contra h
  rw [← mem_nonunits_iff, ← mem_maximalIdeal, ← e] at h
  exact this h

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 ∈ 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
⊢ x ∈ R.toSubring

Tactic:
have : FaithfulSMul R.toSubring S := NoZeroSMulDivisors.instFaithfulSMulOfNontrivial

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
⊢ 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}
⊢ ∀ x_1 ∈ {x}, IsIntegral (↥R.toSubring) x_1

Tactic:
simpa

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
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
⊢ IsUnit r

Tactic:
by_contra 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 : ¬IsUnit r
⊢ 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}
⊢ x ∈ R.toSubring

Tactic:
have : Algebra.IsIntegral R.toSubring S := Algebra.IsIntegral.adjoin (by simpa)

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
⊢ 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
⊢ x ∈ R.toSubring

Tactic:
let S := Algebra.adjoin R.toSubring {x}

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}
⊢ x ∈ R.toSubring