-- Mathlib/RingTheory/Valuation/LocalSubring.lean
@[stacks 052K]
lemma ValuationSubring.isMax_toLocalSubring (R : ValuationSubring K) :
    IsMax R.toLocalSubring

Proof state:
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
⊢ S ≤ R.toLocalSubring

Tactic:
suffices R.toLocalSubring = S from this.ge

Result:
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
⊢ R.toLocalSubring = S

Proof state:
case intro
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
h : x⁻¹ ∈ R.carrier
h' : x ∉ R.toLocalSubring.toSubring
hx0 : x ≠ 0
this✝ : IsUnit ((Subring.inclusion ⋯) ⟨x⁻¹, h⟩)
x' : ↥R.toLocalSubring.toSubring
hx' : ⟨x⁻¹, h⟩ * x' = 1
this : ↑x' = x
⊢ False

Tactic:
exact h' (this ▸ x'.2)

Result:
no goals

Proof state:
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
⊢ S.toSubring ≤ R.toLocalSubring.toSubring

Tactic:
intro x hx

Result:
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
⊢ x ∈ R.toLocalSubring.toSubring

Proof state:
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
h : x⁻¹ ∈ R.carrier
h' : x ∉ R.toLocalSubring.toSubring
hx0 : x ≠ 0
this : IsUnit ((Subring.inclusion ⋯) ⟨x⁻¹, h⟩)
x' : ↥R.toLocalSubring.toSubring
hx' : ⟨x⁻¹, h⟩ * x' = 1
⊢ ↑x' = x

Tactic:
simpa [Subtype.ext_iff, inv_mul_eq_iff_eq_mul₀ hx0] using hx'

Result:
no goals

Proof state:
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
h : x⁻¹ ∈ R.carrier
h' : x ∉ R.toLocalSubring.toSubring
hx0 : x ≠ 0
this : IsUnit ((Subring.inclusion ⋯) ⟨x⁻¹, h⟩)
⊢ False

Tactic:
obtain ⟨x', hx'⟩ := isUnit_iff_exists_inv.mp (hS.2.1 _ this)

Result:
case intro
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
h : x⁻¹ ∈ R.carrier
h' : x ∉ R.toLocalSubring.toSubring
hx0 : x ≠ 0
this : IsUnit ((Subring.inclusion ⋯) ⟨x⁻¹, h⟩)
x' : ↥R.toLocalSubring.toSubring
hx' : ⟨x⁻¹, h⟩ * x' = 1
⊢ False

Proof state:
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
⊢ R.toLocalSubring = S

Tactic:
refine LocalSubring.toSubring_injective (le_antisymm hS.1 ?_)

Result:
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
⊢ S.toSubring ≤ R.toLocalSubring.toSubring

Proof state:
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
h : x⁻¹ ∈ R.carrier
h' : x ∉ R.toLocalSubring.toSubring
⊢ x ≠ 0

Tactic:
rintro rfl

Result:
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
hx : 0 ∈ S.toSubring
h : 0⁻¹ ∈ R.carrier
h' : 0 ∉ R.toLocalSubring.toSubring
⊢ False

Proof state:
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
⊢ x ∈ R.toLocalSubring.toSubring

Tactic:
refine (R.2 x).elim id fun h ↦ ?_

Result:
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
h : x⁻¹ ∈ R.carrier
⊢ x ∈ R.toLocalSubring.toSubring

Proof state:
case intro
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
h : x⁻¹ ∈ R.carrier
h' : x ∉ R.toLocalSubring.toSubring
hx0 : x ≠ 0
this : IsUnit ((Subring.inclusion ⋯) ⟨x⁻¹, h⟩)
x' : ↥R.toLocalSubring.toSubring
hx' : ⟨x⁻¹, h⟩ * x' = 1
⊢ False

Tactic:
have : x'.1 = x := by simpa [Subtype.ext_iff, inv_mul_eq_iff_eq_mul₀ hx0] using hx'

Result:
case intro
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
h : x⁻¹ ∈ R.carrier
h' : x ∉ R.toLocalSubring.toSubring
hx0 : x ≠ 0
this✝ : IsUnit ((Subring.inclusion ⋯) ⟨x⁻¹, h⟩)
x' : ↥R.toLocalSubring.toSubring
hx' : ⟨x⁻¹, h⟩ * x' = 1
this : ↑x' = x
⊢ False

Proof state:
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
⊢ IsMax R.toLocalSubring

Tactic:
intro S hS

Result:
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
⊢ S ≤ R.toLocalSubring

Proof state:
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
h : x⁻¹ ∈ R.carrier
h' : x ∉ R.toLocalSubring.toSubring
hx0 : x ≠ 0
⊢ False

Tactic:
have : IsUnit (Subring.inclusion hS.1 ⟨x⁻¹, h⟩) :=
  isUnit_iff_exists_inv.mpr ⟨⟨x, hx⟩, Subtype.ext (inv_mul_cancel₀ hx0)⟩

Result:
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
h : x⁻¹ ∈ R.carrier
h' : x ∉ R.toLocalSubring.toSubring
hx0 : x ≠ 0
this : IsUnit ((Subring.inclusion ⋯) ⟨x⁻¹, h⟩)
⊢ False

Proof state:
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
h : x⁻¹ ∈ R.carrier
h' : x ∉ R.toLocalSubring.toSubring
⊢ False

Tactic:
have hx0 : x ≠ 0 := by rintro rfl; exact h' (zero_mem R)

Result:
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
h : x⁻¹ ∈ R.carrier
h' : x ∉ R.toLocalSubring.toSubring
hx0 : x ≠ 0
⊢ False

Proof state:
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
hx : 0 ∈ S.toSubring
h : 0⁻¹ ∈ R.carrier
h' : 0 ∉ R.toLocalSubring.toSubring
⊢ False

Tactic:
exact h' (zero_mem R)

Result:
no goals

Proof state:
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
h : x⁻¹ ∈ R.carrier
⊢ x ∈ R.toLocalSubring.toSubring

Tactic:
by_contra h'

Result:
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
h : x⁻¹ ∈ R.carrier
h' : x ∉ R.toLocalSubring.toSubring
⊢ False