-- Mathlib/RingTheory/Valuation/LocalSubring.lean
@[stacks 00IB]
lemma LocalSubring.exists_valuationRing_of_isMax {R : LocalSubring K} (hR : IsMax R) :
    ∃ R' : ValuationSubring K, R'.toLocalSubring = R

Proof state:
case intro.intro.refine_1
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
this✝³ : R.toSubring < S.toSubring
this✝² : 1 ∈ Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
p : Polynomial ↥R.toSubring
hp : ∀ (i : ℕ), p.coeff i ∈ maximalIdeal ↥R.toSubring
hp' : (Polynomial.aeval x) p = ↑1
this✝¹ : Invertible x
this✝ : (Polynomial.aeval x⁻¹) (p - 1).reverse = 0
H : IsUnit ((p - 1).coeff 0)
this : (p - 1).natTrailingDegree = 0
⊢ (Polynomial.C ↑H.unit⁻¹).leadingCoeff * (p - 1).reverse.leadingCoeff ≠ 0

Tactic:
have : p - 1 ≠ 0 := fun e ↦ by simp [e] at H

Result:
case intro.intro.refine_1
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
this✝⁴ : R.toSubring < S.toSubring
this✝³ : 1 ∈ Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
p : Polynomial ↥R.toSubring
hp : ∀ (i : ℕ), p.coeff i ∈ maximalIdeal ↥R.toSubring
hp' : (Polynomial.aeval x) p = ↑1
this✝² : Invertible x
this✝¹ : (Polynomial.aeval x⁻¹) (p - 1).reverse = 0
H : IsUnit ((p - 1).coeff 0)
this✝ : (p - 1).natTrailingDegree = 0
this : p - 1 ≠ 0
⊢ (Polynomial.C ↑H.unit⁻¹).leadingCoeff * (p - 1).reverse.leadingCoeff ≠ 0

Proof state:
case intro.intro
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
this✝² : R.toSubring < S.toSubring
this✝¹ : 1 ∈ Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
p : Polynomial ↥R.toSubring
hp : ∀ (i : ℕ), p.coeff i ∈ maximalIdeal ↥R.toSubring
hp' : (Polynomial.aeval x) p = ↑1
this✝ : Invertible x
this : (Polynomial.aeval ⅟x) (p - 1).reverse = 0
⊢ IsIntegral (↥R.toSubring) x⁻¹

Tactic:
rw [invOf_eq_right_inv (mul_inv_cancel₀ hx0)] at this

Result:
case intro.intro
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
this✝² : R.toSubring < S.toSubring
this✝¹ : 1 ∈ Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
p : Polynomial ↥R.toSubring
hp : ∀ (i : ℕ), p.coeff i ∈ maximalIdeal ↥R.toSubring
hp' : (Polynomial.aeval x) p = ↑1
this✝ : Invertible x
this : (Polynomial.aeval x⁻¹) (p - 1).reverse = 0
⊢ IsIntegral (↥R.toSubring) x⁻¹

Proof state:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
⊢ ∀ x ∉ R.toSubring, x⁻¹ ∈ R.toSubring

Tactic:
intros x hx

Result:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
⊢ x⁻¹ ∈ R.toSubring

Proof state:
case intro.intro
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
this✝² : R.toSubring < S.toSubring
this✝¹ : 1 ∈ Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
p : Polynomial ↥R.toSubring
hp : ∀ (i : ℕ), p.coeff i ∈ maximalIdeal ↥R.toSubring
hp' : (Polynomial.aeval x) p = ↑1
this✝ : Invertible x
this : (Polynomial.aeval x⁻¹) (p - 1).reverse = 0
⊢ IsIntegral (↥R.toSubring) x⁻¹

Tactic:
have H : IsUnit ((p - 1).coeff 0) := by
  by_contra h
  simpa using sub_mem (hp 0) h

Result:
case intro.intro
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
this✝² : R.toSubring < S.toSubring
this✝¹ : 1 ∈ Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
p : Polynomial ↥R.toSubring
hp : ∀ (i : ℕ), p.coeff i ∈ maximalIdeal ↥R.toSubring
hp' : (Polynomial.aeval x) p = ↑1
this✝ : Invertible x
this : (Polynomial.aeval x⁻¹) (p - 1).reverse = 0
H : IsUnit ((p - 1).coeff 0)
⊢ IsIntegral (↥R.toSubring) x⁻¹

Proof state:
case intro.intro
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
this✝ : R.toSubring < S.toSubring
this : 1 ∈ Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
p : Polynomial ↥R.toSubring
hp : ∀ (i : ℕ), p.coeff i ∈ maximalIdeal ↥R.toSubring
hp' : (Polynomial.aeval x) p = ↑1
⊢ IsIntegral (↥R.toSubring) x⁻¹

Tactic:
have := IsUnit.invertible (isUnit_iff_ne_zero.mpr hx0)

Result:
case intro.intro
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
this✝¹ : R.toSubring < S.toSubring
this✝ : 1 ∈ Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
p : Polynomial ↥R.toSubring
hp : ∀ (i : ℕ), p.coeff i ∈ maximalIdeal ↥R.toSubring
hp' : (Polynomial.aeval x) p = ↑1
this : Invertible x
⊢ IsIntegral (↥R.toSubring) x⁻¹

Proof state:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
this✝³ : R.toSubring < S.toSubring
this✝² : 1 ∈ Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
p : Polynomial ↥R.toSubring
hp : ∀ (i : ℕ), p.coeff i ∈ maximalIdeal ↥R.toSubring
hp' : (Polynomial.aeval x) p = ↑1
this✝¹ : Invertible x
this✝ : (Polynomial.aeval x⁻¹) (p - 1).reverse = 0
H : IsUnit ((p - 1).coeff 0)
this : (p - 1).natTrailingDegree = 0
e : p - 1 = 0
⊢ False

Tactic:
simp [e] at 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 : x ∉ R.toSubring
hx0 : x ≠ 0
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
this✝² : R.toSubring < S.toSubring
this✝¹ : 1 ∈ Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
p : Polynomial ↥R.toSubring
hp : ∀ (i : ℕ), p.coeff i ∈ maximalIdeal ↥R.toSubring
hp' : (Polynomial.aeval x) p = ↑1
this✝ : Invertible x
this : (Polynomial.aeval x⁻¹) (p - 1).reverse = 0
H : IsUnit ((p - 1).coeff 0)
⊢ IsIntegral (↥R.toSubring) x⁻¹

Tactic:
refine ⟨.C (H.unit⁻¹).1 * (p - 1).reverse, ?_, ?_⟩

Result:
case intro.intro.refine_1
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
this✝² : R.toSubring < S.toSubring
this✝¹ : 1 ∈ Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
p : Polynomial ↥R.toSubring
hp : ∀ (i : ℕ), p.coeff i ∈ maximalIdeal ↥R.toSubring
hp' : (Polynomial.aeval x) p = ↑1
this✝ : Invertible x
this : (Polynomial.aeval x⁻¹) (p - 1).reverse = 0
H : IsUnit ((p - 1).coeff 0)
⊢ (Polynomial.C ↑H.unit⁻¹ * (p - 1).reverse).Monic

case intro.intro.refine_2
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
this✝² : R.toSubring < S.toSubring
this✝¹ : 1 ∈ Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
p : Polynomial ↥R.toSubring
hp : ∀ (i : ℕ), p.coeff i ∈ maximalIdeal ↥R.toSubring
hp' : (Polynomial.aeval x) p = ↑1
this✝ : Invertible x
this : (Polynomial.aeval x⁻¹) (p - 1).reverse = 0
H : IsUnit ((p - 1).coeff 0)
⊢ Polynomial.eval₂ (algebraMap (↥R.toSubring) K) x⁻¹ (Polynomial.C ↑H.unit⁻¹ * (p - 1).reverse) = 0

Proof state:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
⊢ x⁻¹ ∈ R.toSubring

Tactic:
have hx0 : x ≠ 0 := fun e ↦ hx (e ▸ zero_mem _)

Result:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
⊢ x⁻¹ ∈ R.toSubring