-- 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_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⟩

Tactic:
obtain ⟨A, haA : a ∈ A.1.toSubring⟩ := (Subring.mem_iSup_of_directed hdir).mp ha

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

Proof state:
case refine_1.intro.intro.intro.intro.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
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, ⋯⟩ → IsUnit ⟨a, ha⟩

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

Result:
no goals

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

Tactic:
obtain ⟨B, rfl⟩ := B.exists_valuationRing_of_isMax hB'

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

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

Tactic:
refine (C.1.2.2 (a := ⟨a, hCA haA⟩) (b := ⟨b, hCB hbB⟩) (Subtype.ext congr(($e).1))).imp ?_ ?_

Result:
case refine_1.intro.intro.intro.intro.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
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, ⋯⟩ → IsUnit ⟨a, ha⟩

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⟩

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

Tactic:
exact isUnit_iff_exists_inv.mpr ⟨⟨b, hCB.1 hbB⟩, Subtype.ext congr(($e).1)⟩

Result:
no goals

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
⊢ ∃ ub, ∀ z ∈ s, z ≤ ub

Tactic:
have hdir := H.directed.mono_comp _ LocalSubring.toSubring_mono

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
hdir : Directed LE.le (toSubring ∘ fun x => ↑x)
⊢ ∃ ub, ∀ z ∈ s, z ≤ ub

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

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

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

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

Tactic:
intro 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 ≤ mk (⨆ i, (↑i).toSubring)