-- 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.intro.mk.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
⊢ IsUnit ⟨a, haA⟩

Tactic:
obtain ⟨C, hCA, hCB⟩ := H.directed ⟨A, hA⟩ B

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

Proof state:
case refine_2
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 ≤ mk (⨆ i, (↑i).toSubring)

Tactic:
refine ⟨le_iSup (fun i : s ↦ i.1.toSubring) ⟨A, hA⟩, ⟨?_⟩⟩

Result:
case refine_2
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 : ↥A.toSubring), IsUnit ((Subring.inclusion ⋯) a) → IsUnit a

Proof state:
case refine_1.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 : K
ha : a ∈ ⨆ i, (↑i).toSubring
b : K
hb : b ∈ ⨆ i, (↑i).toSubring
e : ⟨a, ha⟩ + ⟨b, hb⟩ = 1
A : { a // a ∈ s }
haA : a ∈ (↑A).toSubring
B : { a // a ∈ s }
hbB : b ∈ (↑B).toSubring
⊢ IsUnit ⟨a, ha⟩ ∨ IsUnit ⟨b, hb⟩

Tactic:
obtain ⟨C, hCA, hCB⟩ := hdir A B

Result:
case refine_1.intro.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 : K
ha : a ∈ ⨆ i, (↑i).toSubring
b : K
hb : b ∈ ⨆ i, (↑i).toSubring
e : ⟨a, ha⟩ + ⟨b, hb⟩ = 1
A : { a // a ∈ s }
haA : a ∈ (↑A).toSubring
B : { a // a ∈ s }
hbB : b ∈ (↑B).toSubring
C : { a // a ∈ s }
hCA : (toSubring ∘ fun x => ↑x) A ≤ (toSubring ∘ fun x => ↑x) C
hCB : (toSubring ∘ fun x => ↑x) B ≤ (toSubring ∘ fun x => ↑x) C
⊢ 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
inst : Nonempty ↑s
hdir : Directed LE.le (toSubring ∘ fun x => ↑x)
⊢ ∃ ub, ∀ z ∈ s, z ≤ ub

Tactic:
refine ⟨@LocalSubring.mk _ _ (⨆ i : s, i.1.toSubring) ⟨?_⟩, ?_⟩

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 b : ↥(⨆ i, (↑i).toSubring)}, a + b = 1 → IsUnit a ∨ IsUnit b

case refine_2
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)
⊢ ∀ z ∈ s, z ≤ mk (⨆ i, (↑i).toSubring)

Proof state:
case refine_1.intro.intro.intro.intro.refine_2
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
A : { a // a ∈ s }
haA : a ∈ (↑A).toSubring
B : { a // a ∈ s }
hbB : b ∈ (↑B).toSubring
C : { a // a ∈ s }
hCA : (toSubring ∘ fun x => ↑x) A ≤ (toSubring ∘ fun x => ↑x) C
hCB : (toSubring ∘ fun x => ↑x) B ≤ (toSubring ∘ fun x => ↑x) C
⊢ IsUnit ⟨b, ⋯⟩ → IsUnit ⟨b, hb⟩

Tactic:
exact fun h ↦ h.map (Subring.inclusion (le_iSup (fun i : s ↦ i.1.toSubring) C))

Result:
no goals

Proof state:
case refine_2
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 : ↥A.toSubring), IsUnit ((Subring.inclusion ⋯) a) → IsUnit a

Tactic:
rintro ⟨a, haA⟩ h

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

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

Tactic:
intro s hs H 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
⊢ ∃ ub, ∀ z ∈ s, z ≤ ub

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

Tactic:
obtain ⟨B, hB, hB'⟩ := this

Result:
case intro.intro
K : Type u_3
inst✝ : Field K
A B : LocalSubring K
hB : A ≤ B
hB' : IsMax B
⊢ ∃ B, A ≤ B.toLocalSubring

Proof state:
case intro.intro.intro
K : Type u_3
inst✝ : Field K
A : LocalSubring K
B : ValuationSubring K
hB : A ≤ B.toLocalSubring
hB' : IsMax B.toLocalSubring
⊢ ∃ B, A ≤ B.toLocalSubring

Tactic:
exact ⟨B, hB⟩

Result:
no goals

Proof state:
case refine_1.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 : K
ha : a ∈ ⨆ i, (↑i).toSubring
b : K
hb : b ∈ ⨆ i, (↑i).toSubring
e : ⟨a, ha⟩ + ⟨b, hb⟩ = 1
A : { a // a ∈ s }
haA : a ∈ (↑A).toSubring
⊢ IsUnit ⟨a, ha⟩ ∨ IsUnit ⟨b, hb⟩

Tactic:
obtain ⟨B, hbB : b ∈ B.1.toSubring⟩ := (Subring.mem_iSup_of_directed hdir).mp hb

Result:
case refine_1.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 : K
ha : a ∈ ⨆ i, (↑i).toSubring
b : K
hb : b ∈ ⨆ i, (↑i).toSubring
e : ⟨a, ha⟩ + ⟨b, hb⟩ = 1
A : { a // a ∈ s }
haA : a ∈ (↑A).toSubring
B : { a // a ∈ s }
hbB : b ∈ (↑B).toSubring
⊢ IsUnit ⟨a, ha⟩ ∨ IsUnit ⟨b, hb⟩