-- Mathlib/RingTheory/Valuation/ValuationSubring.lean
theorem ofPrime_idealOfLE (R S : ValuationSubring K) (h : R ≤ S) :
    ofPrime R (idealOfLE R S h) = S

Proof state:
case pos
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
hr : x ∈ R
⊢ x ∈ R.ofPrime (R.idealOfLE S h)

Tactic:
exact R.le_ofPrime _ hr

Result:
no goals

Proof state:
case neg
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
hr : x ∉ R
this : x ≠ 0
⊢ x ∈ R.ofPrime (R.idealOfLE S h)

Tactic:
replace hr := (R.mem_or_inv_mem x).resolve_left hr

Result:
case neg
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
this : x ≠ 0
hr : x⁻¹ ∈ R
⊢ x ∈ R.ofPrime (R.idealOfLE S h)

Proof state:
case neg.refine_1
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
this : x ≠ 0
hr : x⁻¹ ∈ R
⊢ ⟨x⁻¹, hr⟩ ∈ (R.idealOfLE S h).primeCompl

Tactic:
simp only [Ideal.primeCompl, Submonoid.mem_mk, Subsemigroup.mem_mk, Set.mem_compl_iff,
  SetLike.mem_coe, idealOfLE, Ideal.mem_comap, IsLocalRing.mem_maximalIdeal, mem_nonunits_iff,
  not_not]

Result:
case neg.refine_1
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
this : x ≠ 0
hr : x⁻¹ ∈ R
⊢ IsUnit ((R.inclusion S h) ⟨x⁻¹, hr⟩)

Proof state:
case neg.refine_1
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
this : x ≠ 0
hr : x⁻¹ ∈ R
⊢ IsUnit ⟨x⁻¹, ⋯⟩

Tactic:
apply isUnit_of_mul_eq_one _ (⟨x, hx⟩ : S)

Result:
case neg.refine_1
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
this : x ≠ 0
hr : x⁻¹ ∈ R
⊢ ⟨x⁻¹, ⋯⟩ * ⟨x, hx⟩ = 1

Proof state:
case neg.refine_1
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
this : x ≠ 0
hr : x⁻¹ ∈ R
⊢ IsUnit ((R.inclusion S h) ⟨x⁻¹, hr⟩)

Tactic:
change IsUnit (⟨x⁻¹, h hr⟩ : S)

Result:
case neg.refine_1
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
this : x ≠ 0
hr : x⁻¹ ∈ R
⊢ IsUnit ⟨x⁻¹, ⋯⟩

Proof state:
case h.mp
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
⊢ x ∈ R.ofPrime (R.idealOfLE S h) → x ∈ S

Tactic:
rintro ⟨a, r, hr, rfl⟩

Result:
case h.mp.intro.intro.intro
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ (algebraMap (↥R) K) a * ((algebraMap (↥R) K) r)⁻¹ ∈ S

Proof state:
case neg.refine_2
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
this : x ≠ 0
hr : x⁻¹ ∈ R
⊢ x = (algebraMap (↥R) K) 1 * ((algebraMap (↥R) K) ⟨x⁻¹, hr⟩)⁻¹

Tactic:
field_simp

Result:
no goals

Proof state:
case h.mp.intro.intro.intro.a
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ (algebraMap (↥R) K) a ∈ S

Tactic:
exact h a.2

Result:
no goals

Proof state:
case h.mpr
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
⊢ x ∈ S → x ∈ R.ofPrime (R.idealOfLE S h)

Tactic:
intro hx

Result:
case h.mpr
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
⊢ x ∈ R.ofPrime (R.idealOfLE S h)

Proof state:
case h.mp.intro.intro.intro.a
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ 1 ≤ S.valuation ((algebraMap (↥R) K) r)

Tactic:
exact not_lt.1 ((not_iff_not.2 <| valuation_lt_one_iff S _).1 hr)

Result:
no goals

Proof state:
case neg
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
hr : x ∉ R
⊢ x ∈ R.ofPrime (R.idealOfLE S h)

Tactic:
have : x ≠ 0 := fun h => hr (by rw [h]; exact R.zero_mem)

Result:
case neg
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
hr : x ∉ R
this : x ≠ 0
⊢ x ∈ R.ofPrime (R.idealOfLE S h)

Proof state:
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h✝ : R ≤ S
x : K
hx : x ∈ S
hr : x ∉ R
h : x = 0
⊢ x ∈ R

Tactic:
rw [h]

Result:
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h✝ : R ≤ S
x : K
hx : x ∈ S
hr : x ∉ R
h : x = 0
⊢ 0 ∈ R

Proof state:
case h.mpr
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
⊢ x ∈ R.ofPrime (R.idealOfLE S h)

Tactic:
by_cases hr : x ∈ R

Result:
case pos
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
hr : x ∈ R
⊢ x ∈ R.ofPrime (R.idealOfLE S h)

case neg
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
hr : x ∉ R
⊢ x ∈ R.ofPrime (R.idealOfLE S h)

Proof state:
case h.mp.intro.intro.intro.a.hb
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ 0 < 1

Tactic:
exact zero_lt_one

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h✝ : R ≤ S
x : K
hx : x ∈ S
hr : x ∉ R
h : x = 0
⊢ 0 ∈ R

Tactic:
exact R.zero_mem

Result:
no goals

Proof state:
case neg.refine_1
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
this : x ≠ 0
hr : x⁻¹ ∈ R
⊢ ⟨x⁻¹, ⋯⟩ * ⟨x, hx⟩ = 1

Tactic:
ext

Result:
case neg.refine_1.a
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
this : x ≠ 0
hr : x⁻¹ ∈ R
⊢ ↑(⟨x⁻¹, ⋯⟩ * ⟨x, hx⟩) = ↑1

Proof state:
case neg
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
this : x ≠ 0
hr : x⁻¹ ∈ R
⊢ x ∈ R.ofPrime (R.idealOfLE S h)

Tactic:
refine ⟨1, ⟨x⁻¹, hr⟩, ?_, ?_⟩

Result:
case neg.refine_1
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
this : x ≠ 0
hr : x⁻¹ ∈ R
⊢ ⟨x⁻¹, hr⟩ ∈ (R.idealOfLE S h).primeCompl

case neg.refine_2
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
this : x ≠ 0
hr : x⁻¹ ∈ R
⊢ x = (algebraMap (↥R) K) 1 * ((algebraMap (↥R) K) ⟨x⁻¹, hr⟩)⁻¹

Proof state:
case neg.refine_1.a
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
this : x ≠ 0
hr : x⁻¹ ∈ R
⊢ ↑(⟨x⁻¹, ⋯⟩ * ⟨x, hx⟩) = ↑1

Tactic:
field_simp

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
⊢ R.ofPrime (R.idealOfLE S h) = S

Tactic:
ext x

Result:
case h
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
⊢ x ∈ R.ofPrime (R.idealOfLE S h) ↔ x ∈ S

Proof state:
case h
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
⊢ x ∈ R.ofPrime (R.idealOfLE S h) ↔ x ∈ S

Tactic:
constructor

Result:
case h.mp
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
⊢ x ∈ R.ofPrime (R.idealOfLE S h) → x ∈ S

case h.mpr
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
⊢ x ∈ S → x ∈ R.ofPrime (R.idealOfLE S h)

Proof state:
case h.mp.intro.intro.intro.a
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ ((algebraMap (↥R) K) r)⁻¹ ∈ S

Tactic:
rw [← valuation_le_one_iff, map_inv₀, ← inv_one, inv_le_inv₀]

Result:
case h.mp.intro.intro.intro.a
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ 1 ≤ S.valuation ((algebraMap (↥R) K) r)

case h.mp.intro.intro.intro.a.ha
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ 0 < S.valuation ((algebraMap (↥R) K) r)

case h.mp.intro.intro.intro.a.hb
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ 0 < 1

Proof state:
case h.mp.intro.intro.intro
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ (algebraMap (↥R) K) a * ((algebraMap (↥R) K) r)⁻¹ ∈ S

Tactic:
apply mul_mem

Result:
case h.mp.intro.intro.intro.a
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ (algebraMap (↥R) K) a ∈ S

case h.mp.intro.intro.intro.a
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ ((algebraMap (↥R) K) r)⁻¹ ∈ S