-- 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:
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

Tactic:
apply mem_of_isMax_of_isIntegral hR

Result:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
⊢ 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 : Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring) = ⊤
⊢ IsIntegral (↥R.toSubring) x⁻¹

Tactic:
rw [Ideal.eq_top_iff_one] at this

Result:
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)
⊢ 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}
⊢ IsIntegral (↥R.toSubring) x⁻¹

Tactic:
have : R.toSubring < S.toSubring := SetLike.lt_iff_le_and_exists.mpr
  ⟨fun r hr ↦ algebraMap_mem S ⟨r, hr⟩, ⟨x, Algebra.self_mem_adjoin_singleton _ _, hx⟩⟩

Result:
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
⊢ 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
this : Invertible x
⊢ IsIntegral (↥R.toSubring) x⁻¹

Tactic:
have : Polynomial.aeval (⅟x) (p - 1).reverse = 0 := by
  simpa [← Polynomial.aeval_def, hp'] using
    Polynomial.eval₂_reverse_eq_zero_iff (algebraMap R.toSubring K) x (p - 1)

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 : 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
⊢ (Polynomial.aeval ⅟x) (p - 1).reverse = 0

Tactic:
simpa [← Polynomial.aeval_def, hp'] using
  Polynomial.eval₂_reverse_eq_zero_iff (algebraMap R.toSubring K) x (p - 1)

Result:
no goals

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)
⊢ False

Tactic:
simpa using sub_mem (hp 0) h

Result:
no goals

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⁻¹ * (p - 1).reverse).Monic

Tactic:
rw [Polynomial.Monic.def, Polynomial.leadingCoeff_mul', Polynomial.reverse_leadingCoeff,
  Polynomial.trailingCoeff, this]

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
⊢ (Polynomial.C ↑H.unit⁻¹).leadingCoeff * (p - 1).coeff 0 = 1

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

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
⊢ IsUnit ((p - 1).coeff 0)

Tactic:
by_contra h

Result:
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)
⊢ False

Proof state:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
⊢ IsIntegral (↥R.toSubring) x⁻¹

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 : x ∉ R.toSubring
hx0 : x ≠ 0
S : Subalgebra (↥R.toSubring) K := Algebra.adjoin ↥R.toSubring {x}
⊢ IsIntegral (↥R.toSubring) x⁻¹