-- Mathlib/RingTheory/Valuation/LocalSubring.lean
@[stacks 00IA]
lemma LocalSubring.exists_le_valuationSubring (A : LocalSubring K) :
    ∃ B : ValuationSubring K, A ≤ B.toLocalSubring

Proof state:
case refine_2.mk
K : Type u_3
inst✝ : Field K
A✝ : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A✝
H : IsChain (fun x1 x2 => x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty ↑s
hdir : Directed LE.le (toSubring ∘ fun x => ↑x)
A : LocalSubring K
hA : A ∈ s
a : K
haA : a ∈ A.toSubring
h : IsUnit ((Subring.inclusion ⋯) ⟨a, haA⟩)
⊢ IsUnit ⟨a, haA⟩

Tactic:
obtain ⟨⟨b, hb⟩, e⟩ := isUnit_iff_exists_inv.mp h

Result:
case refine_2.mk.intro.mk
K : Type u_3
inst✝ : Field K
A✝ : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A✝
H : IsChain (fun x1 x2 => x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty ↑s
hdir : Directed LE.le (toSubring ∘ fun x => ↑x)
A : LocalSubring K
hA : A ∈ s
a : K
haA : a ∈ A.toSubring
h : IsUnit ((Subring.inclusion ⋯) ⟨a, haA⟩)
b : K
hb : b ∈ (mk (⨆ i, (↑i).toSubring)).toSubring
e : (Subring.inclusion ⋯) ⟨a, haA⟩ * ⟨b, hb⟩ = 1
⊢ IsUnit ⟨a, haA⟩

Proof state:
case refine_1
K : Type u_3
inst✝ : Field K
A : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A
H : IsChain (fun x1 x2 => x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty ↑s
hdir : Directed LE.le (toSubring ∘ fun x => ↑x)
⊢ ∀ {a b : ↥(⨆ i, (↑i).toSubring)}, a + b = 1 → IsUnit a ∨ IsUnit b

Tactic:
intro ⟨a, ha⟩ ⟨b, hb⟩ e

Result:
case refine_1
K : Type u_3
inst✝ : Field K
A : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A
H : IsChain (fun x1 x2 => x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty ↑s
hdir : Directed LE.le (toSubring ∘ fun x => ↑x)
a : K
ha : a ∈ ⨆ i, (↑i).toSubring
b : K
hb : b ∈ ⨆ i, (↑i).toSubring
e : ⟨a, ha⟩ + ⟨b, hb⟩ = 1
⊢ IsUnit ⟨a, ha⟩ ∨ IsUnit ⟨b, hb⟩

Proof state:
K : Type u_3
inst✝ : Field K
A : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A
H : IsChain (fun x1 x2 => x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
⊢ ∃ ub, ∀ z ∈ s, z ≤ ub

Tactic:
have inst : Nonempty s := ⟨⟨y, hys⟩⟩

Result:
K : Type u_3
inst✝ : Field K
A : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A
H : IsChain (fun x1 x2 => x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty ↑s
⊢ ∃ ub, ∀ z ∈ s, z ≤ ub

Proof state:
K : Type u_3
inst✝ : Field K
A : LocalSubring K
⊢ ∃ B, A ≤ B ∧ IsMax B

Tactic:
refine zorn_le_nonempty_Ici₀ _ ?_ _ le_rfl

Result:
K : Type u_3
inst✝ : Field K
A : LocalSubring K
⊢ ∀ c ⊆ Set.Ici A, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub

Proof state:
K : Type u_3
inst✝ : Field K
A : LocalSubring K
⊢ ∃ B, A ≤ B.toLocalSubring

Tactic:
suffices ∃ B, A ≤ B ∧ IsMax B by
  obtain ⟨B, hB, hB'⟩ := this
  obtain ⟨B, rfl⟩ := B.exists_valuationRing_of_isMax hB'
  exact ⟨B, hB⟩

Result:
K : Type u_3
inst✝ : Field K
A : LocalSubring K
⊢ ∃ B, A ≤ B ∧ IsMax B

Proof state:
case refine_2.mk.intro.mk.intro.intro.intro
K : Type u_3
inst✝ : Field K
A✝ : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A✝
H : IsChain (fun x1 x2 => x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty ↑s
hdir : Directed LE.le (toSubring ∘ fun x => ↑x)
A : LocalSubring K
hA : A ∈ s
a : K
haA : a ∈ A.toSubring
h : IsUnit ((Subring.inclusion ⋯) ⟨a, haA⟩)
b : K
hb : b ∈ (mk (⨆ i, (↑i).toSubring)).toSubring
e : (Subring.inclusion ⋯) ⟨a, haA⟩ * ⟨b, hb⟩ = 1
B : { a // a ∈ s }
hbB : b ∈ (↑B).toSubring
C : { a // a ∈ s }
hCA : (fun x => ↑x) ⟨A, hA⟩ ≤ (fun x => ↑x) C
hCB : (fun x => ↑x) B ≤ (fun x => ↑x) C
⊢ IsUnit ⟨a, haA⟩

Tactic:
apply hCA.2.1

Result:
case refine_2.mk.intro.mk.intro.intro.intro.a
K : Type u_3
inst✝ : Field K
A✝ : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A✝
H : IsChain (fun x1 x2 => x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty ↑s
hdir : Directed LE.le (toSubring ∘ fun x => ↑x)
A : LocalSubring K
hA : A ∈ s
a : K
haA : a ∈ A.toSubring
h : IsUnit ((Subring.inclusion ⋯) ⟨a, haA⟩)
b : K
hb : b ∈ (mk (⨆ i, (↑i).toSubring)).toSubring
e : (Subring.inclusion ⋯) ⟨a, haA⟩ * ⟨b, hb⟩ = 1
B : { a // a ∈ s }
hbB : b ∈ (↑B).toSubring
C : { a // a ∈ s }
hCA : (fun x => ↑x) ⟨A, hA⟩ ≤ (fun x => ↑x) C
hCB : (fun x => ↑x) B ≤ (fun x => ↑x) C
⊢ IsUnit ((Subring.inclusion ⋯) ⟨a, haA⟩)