-- 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)
⊢ (Polynomial.C ↑H.unit⁻¹ * (p - 1).reverse).Monic

Tactic:
have : (p - 1).natTrailingDegree = 0 := by
  simp only [Polynomial.natTrailingDegree_eq_zero,
    Polynomial.coeff_sub, Polynomial.coeff_one_zero, ne_eq, sub_eq_zero]
  exact .inr fun h ↦ (IsLocalRing.not_mem_maximalIdeal.mpr isUnit_one (h ▸ hp 0))

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

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).coeff 0 = 1

Tactic:
simp

Result:
no goals

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

Tactic:
simp [← Polynomial.aeval_def, this]

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

Tactic:
simpa

Result:
no goals

Proof state:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
⊢ ∃ R', R'.toLocalSubring = R

Tactic:
suffices ∀ x ∉ R.toSubring, x⁻¹ ∈ R.toSubring from
  ⟨⟨R.toSubring, fun x ↦ or_iff_not_imp_left.mpr (this x)⟩, rfl⟩

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

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

Tactic:
have := map_maximalIdeal_eq_top_of_isMax hR 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 : 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}
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)
⊢ (p - 1).natTrailingDegree = 0

Tactic:
simp only [Polynomial.natTrailingDegree_eq_zero,
  Polynomial.coeff_sub, Polynomial.coeff_one_zero, ne_eq, sub_eq_zero]

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)
⊢ p = 1 ∨ ¬p.coeff 0 = 1

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

Tactic:
obtain ⟨p, hp, hp'⟩ := (Algebra.mem_ideal_map_adjoin _ _).mp 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
⊢ 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)
⊢ p = 1 ∨ ¬p.coeff 0 = 1

Tactic:
exact .inr fun h ↦ (IsLocalRing.not_mem_maximalIdeal.mpr isUnit_one (h ▸ hp 0))

Result:
no goals