awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
A : LocalSubring K
this : ∃ (B : LocalSubring K), A ≤ B ∧ IsMax B
obtain : ∀ (B : LocalSubring K) (hB : A ≤ B) (hB' : IsMax B), ∃ (B : ValuationSubring K), A ≤ B.toLocalSubring
⊢ ∃ (B : ValuationSubring K), A ≤ B.toLocalSubring

Tactic:
obtain ⟨B, hB, hB'⟩ := this
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
A B : LocalSubring K
hB : A ≤ B
hB' : IsMax B
obtain :
  ∀ (B : ValuationSubring K) (hB : A ≤ B.toLocalSubring) (hB' : IsMax B.toLocalSubring),
    ∃ (B : ValuationSubring K), A ≤ B.toLocalSubring
⊢ ∃ (B : ValuationSubring K), A ≤ B.toLocalSubring

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

Premises used: LocalSubring.exists_valuationRing_of_isMax, rfl
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
A : LocalSubring K
B : ValuationSubring K
hB : A ≤ B.toLocalSubring
hB' : IsMax B.toLocalSubring
⊢ ∃ (B : ValuationSubring K), A ≤ B.toLocalSubring

Tactic:
⟨B, hB⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
A : LocalSubring K
B : ValuationSubring K
hB : A ≤ B.toLocalSubring
hB' : IsMax B.toLocalSubring
⊢ ∃ (B : ValuationSubring K), A ≤ B.toLocalSubring

Tactic:
exact ⟨B, hB⟩
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
A : LocalSubring K
suffices : ∃ (B : LocalSubring K), A ≤ B ∧ IsMax B
⊢ ∃ (B : ValuationSubring K), 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⟩
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
A : LocalSubring K
⊢ ∃ (B : LocalSubring K), A ≤ B ∧ IsMax B

Tactic:
zorn_le_nonempty_Ici₀ _ ?_ _ le_rfl

Premises used: le_rfl, zorn_le_nonempty_Ici₀
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
A : LocalSubring K
refine :
  ∀ c ⊆ Set.Ici A,
    IsChain (fun (x1 x2 : LocalSubring K) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ (ub : LocalSubring K), ∀ z ∈ c, z ≤ ub
⊢ ∃ (B : LocalSubring K), A ≤ B ∧ IsMax B

Tactic:
refine zorn_le_nonempty_Ici₀ _ ?_ _ le_rfl

Premises used: le_rfl, zorn_le_nonempty_Ici₀
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
A : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A
H : IsChain (fun (x1 x2 : LocalSubring K) ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
⊢ Nonempty.{u_3 + 1} (↑s : Type u_3)

Tactic:
have inst : Nonempty s := ⟨⟨y, hys⟩⟩
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst_1 : Field K
A : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A
H : IsChain (fun (x1 x2 : LocalSubring K) ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty.{u_3 + 1} (↑s : Type u_3)
⊢ Directed.{u_3, u_3 + 1} (α := Subring K) (ι := { a : LocalSubring K // a ∈ s }) LE.le
    (toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K))

Tactic:
have hdir := H.directed.mono_comp _ LocalSubring.toSubring_mono
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst_1 : Field K
A : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A
H : IsChain (fun (x1 x2 : LocalSubring K) ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty.{u_3 + 1} (↑s : Type u_3)
hdir :
  Directed.{u_3, u_3 + 1} (α := Subring K) (ι := { a : LocalSubring K // a ∈ s }) LE.le
    (toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K))
⊢ ∃ (ub : LocalSubring K), ∀ z ∈ s, z ≤ ub

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

Premises used: LocalSubring.mk, iSup, LocalSubring.toSubring, Exists.intro, Subtype.val
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst_1 : Field K
A : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A
H : IsChain (fun (x1 x2 : LocalSubring K) ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty.{u_3 + 1} (↑s : Type u_3)
hdir :
  Directed.{u_3, u_3 + 1} (α := Subring K) (ι := { a : LocalSubring K // a ∈ s }) LE.le
    (toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K))
refine_1 : ∀ {a b : ↥(⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring)} (h : a + b = 1), IsUnit a ∨ IsUnit b
refine_2 : ∀ z ∈ s, z ≤ { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ }
⊢ ∃ (ub : LocalSubring K), ∀ z ∈ s, z ≤ ub

Tactic:
refine ⟨@LocalSubring.mk _ _ (⨆ i : s, i.1.toSubring) ⟨?_⟩, ?_⟩
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst_1 : Field K
A : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A
H : IsChain (fun (x1 x2 : LocalSubring K) ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty.{u_3 + 1} (↑s : Type u_3)
hdir :
  Directed.{u_3, u_3 + 1} (α := Subring K) (ι := { a : LocalSubring K // a ∈ s }) LE.le
    (toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K))
a : K
ha : Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) a
refine_1 :
  ∀ (b : K) (hb : Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) b)
    (h :
      Subtype.mk (p := fun (x : K) ↦
            Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha +
          Subtype.mk (p := fun (x : K) ↦
            Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) b hb =
        1),
    IsUnit
        (Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha) ∨
      IsUnit
        (Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) b hb)
⊢ ∀ {b : ↥(⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring)}
    (h :
      Subtype.mk (p := fun (x : K) ↦
            Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha +
          b =
        1),
    IsUnit
        (Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha) ∨
      IsUnit b

Tactic:
⟨b, hb⟩
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst_1 : Field K
A : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A
H : IsChain (fun (x1 x2 : LocalSubring K) ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty.{u_3 + 1} (↑s : Type u_3)
hdir :
  Directed.{u_3, u_3 + 1} (α := Subring K) (ι := { a : LocalSubring K // a ∈ s }) LE.le
    (toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K))
a : K
ha : Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) a
b : K
hb : Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) b
e :
  Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha +
      Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) b hb =
    1
refine_1 :
  ∀ (A : { a : LocalSubring K // a ∈ s }) (haA : a ∈ (↑A : LocalSubring K).toSubring),
    IsUnit
        (Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha) ∨
      IsUnit
        (Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) b hb)
⊢ IsUnit
      (Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha) ∨
    IsUnit
      (Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) b hb)

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

Premises used: Subring.toSubsemiring, Subsemiring.toSubring, Subring.mem_iSup_of_directed, LocalSubring.toSubring, Iff.mp
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst_1 : Field K
A_1 : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A_1
H : IsChain (fun (x1 x2 : LocalSubring K) ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty.{u_3 + 1} (↑s : Type u_3)
hdir :
  Directed.{u_3, u_3 + 1} (α := Subring K) (ι := { a : LocalSubring K // a ∈ s }) LE.le
    (toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K))
a : K
ha : Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) a
b : K
hb : Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) b
e :
  Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha +
      Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) b hb =
    1
A : { a : LocalSubring K // a ∈ s }
haA : a ∈ (↑A : LocalSubring K).toSubring
refine_1 :
  ∀ (B : { a : LocalSubring K // a ∈ s }) (hbB : b ∈ (↑B : LocalSubring K).toSubring),
    IsUnit
        (Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha) ∨
      IsUnit
        (Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) b hb)
⊢ IsUnit
      (Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha) ∨
    IsUnit
      (Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) b hb)

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

Premises used: Subring.mem_iSup_of_directed, Iff.mp
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst_1 : Field K
A_1 : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A_1
H : IsChain (fun (x1 x2 : LocalSubring K) ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty.{u_3 + 1} (↑s : Type u_3)
hdir :
  Directed.{u_3, u_3 + 1} (α := Subring K) (ι := { a : LocalSubring K // a ∈ s }) LE.le
    (toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K))
a : K
ha : Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) a
b : K
hb : Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) b
e :
  Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha +
      Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) b hb =
    1
A : { a : LocalSubring K // a ∈ s }
haA : a ∈ (↑A : LocalSubring K).toSubring
B : { a : LocalSubring K // a ∈ s }
hbB : b ∈ (↑B : LocalSubring K).toSubring
refine_1 :
  ∀ (C : { a : LocalSubring K // a ∈ s })
    (hCA :
      LE.le (α := Subring K) ((toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) A)
        ((toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) C))
    (hCB :
      LE.le (α := Subring K) ((toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) B)
        ((toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) C)),
    IsUnit
        (Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha) ∨
      IsUnit
        (Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) b hb)
⊢ IsUnit
      (Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha) ∨
    IsUnit
      (Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) b hb)

Tactic:
obtain ⟨C, hCA, hCB⟩ := hdir A B
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst_1 : Field K
A_1 : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A_1
H : IsChain (fun (x1 x2 : LocalSubring K) ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty.{u_3 + 1} (↑s : Type u_3)
hdir :
  Directed.{u_3, u_3 + 1} (α := Subring K) (ι := { a : LocalSubring K // a ∈ s }) LE.le
    (toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K))
a : K
ha : Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) a
b : K
hb : Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) b
e :
  Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha +
      Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) b hb =
    1
A : { a : LocalSubring K // a ∈ s }
haA : a ∈ (↑A : LocalSubring K).toSubring
B : { a : LocalSubring K // a ∈ s }
hbB : b ∈ (↑B : LocalSubring K).toSubring
C : { a : LocalSubring K // a ∈ s }
hCA :
  LE.le (α := Subring K) ((toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) A)
    ((toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) C)
hCB :
  LE.le (α := Subring K) ((toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) B)
    ((toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) C)
⊢ IsUnit
      (Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha) ∨
    IsUnit
      (Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) b hb)

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

Premises used: congrArg, id, IsLocalRing.isUnit_or_isUnit_of_add_one, Or.imp, Subtype.val, Subtype.ext
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst_1 : Field K
A_1 : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A_1
H : IsChain (fun (x1 x2 : LocalSubring K) ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty.{u_3 + 1} (↑s : Type u_3)
hdir :
  Directed.{u_3, u_3 + 1} (α := Subring K) (ι := { a : LocalSubring K // a ∈ s }) LE.le
    (toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K))
a : K
ha : Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) a
b : K
hb : Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) b
e :
  Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha +
      Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) b hb =
    1
A : { a : LocalSubring K // a ∈ s }
haA : a ∈ (↑A : LocalSubring K).toSubring
B : { a : LocalSubring K // a ∈ s }
hbB : b ∈ (↑B : LocalSubring K).toSubring
C : { a : LocalSubring K // a ∈ s }
hCA :
  LE.le (α := Subring K) ((toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) A)
    ((toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) C)
hCB :
  LE.le (α := Subring K) ((toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) B)
    ((toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) C)
refine_1 :
  IsUnit (Subtype.mk (p := fun (x : K) ↦ x ∈ (↑C : LocalSubring K).toSubring) a ⋯) →
    IsUnit
      (Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha)
refine_1₁ :
  IsUnit (Subtype.mk (p := fun (x : K) ↦ x ∈ (↑C : LocalSubring K).toSubring) b ⋯) →
    IsUnit
      (Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) b hb)
⊢ IsUnit
      (Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha) ∨
    IsUnit
      (Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) b hb)

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

Premises used: congrArg, id, IsLocalRing.isUnit_or_isUnit_of_add_one, Or.imp, Subtype.val, Subtype.ext
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst_1 : Field K
A_1 : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A_1
H : IsChain (fun (x1 x2 : LocalSubring K) ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty.{u_3 + 1} (↑s : Type u_3)
hdir :
  Directed.{u_3, u_3 + 1} (α := Subring K) (ι := { a : LocalSubring K // a ∈ s }) LE.le
    (toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K))
a : K
ha : Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) a
b : K
hb : Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) b
e :
  Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha +
      Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) b hb =
    1
A : { a : LocalSubring K // a ∈ s }
haA : a ∈ (↑A : LocalSubring K).toSubring
B : { a : LocalSubring K // a ∈ s }
hbB : b ∈ (↑B : LocalSubring K).toSubring
C : { a : LocalSubring K // a ∈ s }
hCA :
  LE.le (α := Subring K) ((toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) A)
    ((toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) C)
hCB :
  LE.le (α := Subring K) ((toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) B)
    ((toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) C)
⊢ IsUnit (Subtype.mk (p := fun (x : K) ↦ x ∈ (↑C : LocalSubring K).toSubring) a ⋯) →
    IsUnit
      (Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha)

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

Premises used: Subring.inclusion, Set.Mem, le_iSup, LocalSubring.toSubring, IsUnit.map, Subtype.val
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst_1 : Field K
A_1 : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A_1
H : IsChain (fun (x1 x2 : LocalSubring K) ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty.{u_3 + 1} (↑s : Type u_3)
hdir :
  Directed.{u_3, u_3 + 1} (α := Subring K) (ι := { a : LocalSubring K // a ∈ s }) LE.le
    (toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K))
a : K
ha : Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) a
b : K
hb : Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) b
e :
  Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha +
      Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) b hb =
    1
A : { a : LocalSubring K // a ∈ s }
haA : a ∈ (↑A : LocalSubring K).toSubring
B : { a : LocalSubring K // a ∈ s }
hbB : b ∈ (↑B : LocalSubring K).toSubring
C : { a : LocalSubring K // a ∈ s }
hCA :
  LE.le (α := Subring K) ((toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) A)
    ((toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) C)
hCB :
  LE.le (α := Subring K) ((toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) B)
    ((toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) C)
⊢ IsUnit (Subtype.mk (p := fun (x : K) ↦ x ∈ (↑C : LocalSubring K).toSubring) a ⋯) →
    IsUnit
      (Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha)

Tactic:
exact fun h ↦ h.map (Subring.inclusion (le_iSup (fun i : s ↦ i.1.toSubring) C))
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst_1 : Field K
A_1 : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A_1
H : IsChain (fun (x1 x2 : LocalSubring K) ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty.{u_3 + 1} (↑s : Type u_3)
hdir :
  Directed.{u_3, u_3 + 1} (α := Subring K) (ι := { a : LocalSubring K // a ∈ s }) LE.le
    (toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K))
a : K
ha : Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) a
b : K
hb : Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) b
e :
  Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha +
      Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) b hb =
    1
A : { a : LocalSubring K // a ∈ s }
haA : a ∈ (↑A : LocalSubring K).toSubring
B : { a : LocalSubring K // a ∈ s }
hbB : b ∈ (↑B : LocalSubring K).toSubring
C : { a : LocalSubring K // a ∈ s }
hCA :
  LE.le (α := Subring K) ((toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) A)
    ((toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) C)
hCB :
  LE.le (α := Subring K) ((toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) B)
    ((toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) C)
⊢ IsUnit (Subtype.mk (p := fun (x : K) ↦ x ∈ (↑C : LocalSubring K).toSubring) b ⋯) →
    IsUnit
      (Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) b hb)

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

Premises used: Subring.inclusion, Set.Mem, le_iSup, LocalSubring.toSubring, IsUnit.map, Subtype.val