awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
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 : LocalSubring K
hA : A ∈ s
⊢ A ≤ { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ }

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

Premises used: IsLocalHom.mk, le_iSup, Subtype.mk, LocalSubring.toSubring, Exists.intro, 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 : LocalSubring K
hA : A ∈ s
refine_2 :
  ∀ (a : ↥A.toSubring),
    IsUnit (M :=
        ↥(toSubring { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ }))
        (((Subring.inclusion ⋯ :
                ↥A.toSubring →+*
                  ↥(toSubring
                      { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ })) :
              (a : ↥A.toSubring) →
                ↥{ toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ }.toSubring)
            a :
          ↥(toSubring { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ })) →
      IsUnit a
⊢ A ≤ { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ }

Tactic:
refine ⟨le_iSup (fun i : s ↦ i.1.toSubring) ⟨A, hA⟩, ⟨?_⟩⟩
-- 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 : LocalSubring K
hA : A ∈ s
a : K
haA : a ∈ A.toSubring
h :
  IsUnit (M := ↥(toSubring { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ }))
    (((Subring.inclusion ⋯ :
            ↥A.toSubring →+*
              ↥(toSubring
                  { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ })) :
          (a : ↥A.toSubring) →
            ↥{ toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ }.toSubring)
        (Subtype.mk (p := fun (x : K) ↦ x ∈ A.toSubring) a haA) :
      ↥(toSubring { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ }))
refine_2 :
  ∀ (b : K)
    (hb :
      Membership.mem (γ := Subring K)
        (toSubring { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ }) b)
    (e :
      HMul.hMul (α :=
          ↥(toSubring
              { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ :
                LocalSubring K }))
          (((Subring.inclusion ⋯ :
                  ↥A.toSubring →+*
                    ↥(toSubring
                        { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ :
                          LocalSubring K })) :
                (a : ↥A.toSubring) →
                  ↥{ toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring,
                        isLocalRing := ⋯ }.toSubring)
              (Subtype.mk (p := fun (x : K) ↦ x ∈ A.toSubring) a haA) :
            ↥(toSubring
                { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ :
                  LocalSubring K }))
          (Subtype.mk (p := fun (x : K) ↦
            Membership.mem (γ := Subring K)
              (toSubring
                { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ :
                  LocalSubring K })
              x)
            b hb) =
        1),
    IsUnit (Subtype.mk (p := fun (x : K) ↦ x ∈ A.toSubring) a haA)
⊢ IsUnit (Subtype.mk (p := fun (x : K) ↦ x ∈ A.toSubring) a haA)

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

Premises used: isUnit_iff_exists_inv, 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 : LocalSubring K
hA : A ∈ s
a : K
haA : a ∈ A.toSubring
h :
  IsUnit (M := ↥(toSubring { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ }))
    (((Subring.inclusion ⋯ :
            ↥A.toSubring →+*
              ↥(toSubring
                  { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ })) :
          (a : ↥A.toSubring) →
            ↥{ toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ }.toSubring)
        (Subtype.mk (p := fun (x : K) ↦ x ∈ A.toSubring) a haA) :
      ↥(toSubring { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ }))
b : K
hb :
  Membership.mem (γ := Subring K)
    (toSubring { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ }) b
e :
  HMul.hMul (α :=
      ↥(toSubring
          { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ : LocalSubring K }))
      (((Subring.inclusion ⋯ :
              ↥A.toSubring →+*
                ↥(toSubring
                    { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ :
                      LocalSubring K })) :
            (a : ↥A.toSubring) →
              ↥{ toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ }.toSubring)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ A.toSubring) a haA) :
        ↥(toSubring
            { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ :
              LocalSubring K }))
      (Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K)
          (toSubring
            { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := ⋯ :
              LocalSubring K })
          x)
        b hb) =
    1
refine_2 :
  ∀ (B : { a : LocalSubring K // a ∈ s }) (hbB : b ∈ (↑B : LocalSubring K).toSubring),
    IsUnit (Subtype.mk (p := fun (x : K) ↦ x ∈ A.toSubring) a haA)
⊢ IsUnit (Subtype.mk (p := fun (x : K) ↦ x ∈ A.toSubring) a haA)

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 : Field K
A : Subring K
I : Ideal ↥A
hI : I ≠ ⊤
have :
  ∀ (M : Ideal ↥A) (hM : M.IsMaximal) (le : I ≤ M),
    ∃ (B : ValuationSubring K), A ≤ B.toSubring ∧ (⇑A.subtype : (a : ↥A) → K) '' (↑I : Set ↥A) ⊆ (↑B.nonunits : Set K)
⊢ ∃ (B : ValuationSubring K), A ≤ B.toSubring ∧ (⇑A.subtype : (a : ↥A) → K) '' (↑I : Set ↥A) ⊆ (↑B.nonunits : Set K)

Tactic:
have ⟨M, hM, le⟩ := I.exists_le_maximal hI
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
A : Subring K
I : Ideal ↥A
hI : I ≠ ⊤
M : Ideal ↥A
hM : M.IsMaximal
le : I ≤ M
have :
  ∀ (V : ValuationSubring K) (hV : LocalSubring.ofPrime A M ≤ V.toLocalSubring),
    ∃ (B : ValuationSubring K), A ≤ B.toSubring ∧ (⇑A.subtype : (a : ↥A) → K) '' (↑I : Set ↥A) ⊆ (↑B.nonunits : Set K)
⊢ ∃ (B : ValuationSubring K), A ≤ B.toSubring ∧ (⇑A.subtype : (a : ↥A) → K) '' (↑I : Set ↥A) ⊆ (↑B.nonunits : Set K)

Tactic:
have ⟨V, hV⟩ := (LocalSubring.ofPrime A M).exists_le_valuationSubring
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
A : Subring K
I : Ideal ↥A
hI : I ≠ ⊤
M : Ideal ↥A
hM : M.IsMaximal
le : I ≤ M
V : ValuationSubring K
hV : LocalSubring.ofPrime A M ≤ V.toLocalSubring
⊢ ∃ (B : ValuationSubring K), A ≤ B.toSubring ∧ (⇑A.subtype : (a : ↥A) → K) '' (↑I : Set ↥A) ⊆ (↑B.nonunits : Set K)

Tactic:
⟨V, (LocalSubring.le_ofPrime ..).trans hV.1, ?_⟩

Premises used: LocalSubring.le_ofPrime, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
A : Subring K
I : Ideal ↥A
hI : I ≠ ⊤
M : Ideal ↥A
hM : M.IsMaximal
le : I ≤ M
V : ValuationSubring K
hV : LocalSubring.ofPrime A M ≤ V.toLocalSubring
refine : (⇑A.subtype : (a : ↥A) → K) '' (↑I : Set ↥A) ⊆ (↑V.nonunits : Set K)
⊢ ∃ (B : ValuationSubring K), A ≤ B.toSubring ∧ (⇑A.subtype : (a : ↥A) → K) '' (↑I : Set ↥A) ⊆ (↑B.nonunits : Set K)

Tactic:
refine ⟨V, (LocalSubring.le_ofPrime ..).trans hV.1, ?_⟩
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
A : Subring K
I : Ideal ↥A
hI : I ≠ ⊤
M : Ideal ↥A
hM : M.IsMaximal
le : I ≤ M
V : ValuationSubring K
hV : LocalSubring.ofPrime A M ≤ V.toLocalSubring
rw :
  (⇑A.subtype : (a : ↥A) → K) '' (↑I : Set ↥A) ⊆ Subtype.val (p := fun (x : K) ↦ x ∈ V) '' (↑(maximalIdeal ↥V) : Set ↥V)
⊢ (⇑A.subtype : (a : ↥A) → K) '' (↑I : Set ↥A) ⊆ (↑V.nonunits : Set K)

Tactic:
rw [← V.image_maximalIdeal]

Premises used: ValuationSubring.image_maximalIdeal
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
A : Subring K
I : Ideal ↥A
hI : I ≠ ⊤
M : Ideal ↥A
hM : M.IsMaximal
le : I ≤ M
V : ValuationSubring K
hV : LocalSubring.ofPrime A M ≤ V.toLocalSubring
⊢ (⇑A.subtype : (a : ↥A) → K) '' (↑I : Set ↥A) ⊆ Subtype.val (p := fun (x : K) ↦ x ∈ V) '' (↑(maximalIdeal ↥V) : Set ↥V)

Tactic:
.trans ?_ (Set.image_mono <| ((local_hom_TFAE _).out 0 2).mp hV.2)

Premises used: Set.image_mono, HasSubset.Subset.trans, List.TFAE.out, Iff.mp, OfNat.ofNat, IsLocalRing.local_hom_TFAE
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
A : Subring K
I : Ideal ↥A
hI : I ≠ ⊤
M : Ideal ↥A
hM : M.IsMaximal
le : I ≤ M
V : ValuationSubring K
hV : LocalSubring.ofPrime A M ≤ V.toLocalSubring
refine :
  (⇑A.subtype : (a : ↥A) → K) '' (↑I : Set ↥A) ⊆
    Subtype.val (p := fun (x : K) ↦ x ∈ V) ''
      (↑(map (R := ↥(LocalSubring.ofPrime A M).toSubring) (F :=
            ↥(LocalSubring.ofPrime A M).toSubring →+* ↥V.toLocalSubring.toSubring) (Subring.inclusion ⋯)
            (maximalIdeal ↥(LocalSubring.ofPrime A M).toSubring)) :
        Set ↥V.toLocalSubring.toSubring)
⊢ (⇑A.subtype : (a : ↥A) → K) '' (↑I : Set ↥A) ⊆ Subtype.val (p := fun (x : K) ↦ x ∈ V) '' (↑(maximalIdeal ↥V) : Set ↥V)

Tactic:
refine .trans ?_ (Set.image_mono <| ((local_hom_TFAE _).out 0 2).mp hV.2)
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
A : Subring K
I : Ideal ↥A
hI : I ≠ ⊤
M : Ideal ↥A
hM : M.IsMaximal
le : I ≤ M
V : ValuationSubring K
hV : LocalSubring.ofPrime A M ≤ V.toLocalSubring
rw :
  (⇑A.subtype : (a : ↥A) → K) '' (↑I : Set ↥A) ⊆
    Subtype.val (p := fun (x : K) ↦ x ∈ V) ''
      (↑(map (F := ↥A →+* ↥V.toLocalSubring.toSubring)
            (RingHom.comp (β := ↥(LocalSubring.ofPrime A M).toSubring) (Subring.inclusion ⋯)
              (algebraMap ↥A ↥(LocalSubring.ofPrime A M).toSubring))
            M) :
        Set ↥V.toLocalSubring.toSubring)
⊢ (⇑A.subtype : (a : ↥A) → K) '' (↑I : Set ↥A) ⊆
    Subtype.val (p := fun (x : K) ↦ x ∈ V) ''
      (↑(map (R := ↥(LocalSubring.ofPrime A M).toSubring) (F :=
            ↥(LocalSubring.ofPrime A M).toSubring →+* ↥V.toLocalSubring.toSubring) (Subring.inclusion ⋯)
            (maximalIdeal ↥(LocalSubring.ofPrime A M).toSubring)) :
        Set ↥V.toLocalSubring.toSubring)

Tactic:
rw [← IsLocalization.AtPrime.map_eq_maximalIdeal M, map_map]

Premises used: IsLocalization.AtPrime.map_eq_maximalIdeal, Ideal.map_map
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
A : Subring K
I : Ideal ↥A
hI : I ≠ ⊤
M : Ideal ↥A
hM : M.IsMaximal
le : I ≤ M
V : ValuationSubring K
hV : LocalSubring.ofPrime A M ≤ V.toLocalSubring
⊢ (⇑A.subtype : (a : ↥A) → K) '' (↑I : Set ↥A) ⊆
    Subtype.val (p := fun (x : K) ↦ x ∈ V) ''
      (↑(map (F := ↥A →+* ↥V.toLocalSubring.toSubring)
            (RingHom.comp (β := ↥(LocalSubring.ofPrime A M).toSubring) (Subring.inclusion ⋯)
              (algebraMap ↥A ↥(LocalSubring.ofPrime A M).toSubring))
            M) :
        Set ↥V.toLocalSubring.toSubring)

Tactic:
.trans ?_ (Set.image_mono <| map_mono le)

Premises used: Set.image_mono, HasSubset.Subset.trans, Ideal.map_mono
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
A : Subring K
I : Ideal ↥A
hI : I ≠ ⊤
M : Ideal ↥A
hM : M.IsMaximal
le : I ≤ M
V : ValuationSubring K
hV : LocalSubring.ofPrime A M ≤ V.toLocalSubring
refine :
  (⇑A.subtype : (a : ↥A) → K) '' (↑I : Set ↥A) ⊆
    Subtype.val (p := fun (x : K) ↦ x ∈ V) ''
      (↑(map (F := ↥A →+* ↥V.toLocalSubring.toSubring)
            (RingHom.comp (β := ↥(LocalSubring.ofPrime A M).toSubring) (Subring.inclusion ⋯)
              (algebraMap ↥A ↥(LocalSubring.ofPrime A M).toSubring))
            I) :
        Set ↥V)
⊢ (⇑A.subtype : (a : ↥A) → K) '' (↑I : Set ↥A) ⊆
    Subtype.val (p := fun (x : K) ↦ x ∈ V) ''
      (↑(map (F := ↥A →+* ↥V.toLocalSubring.toSubring)
            (RingHom.comp (β := ↥(LocalSubring.ofPrime A M).toSubring) (Subring.inclusion ⋯)
              (algebraMap ↥A ↥(LocalSubring.ofPrime A M).toSubring))
            M) :
        Set ↥V.toLocalSubring.toSubring)

Tactic:
refine .trans ?_ (Set.image_mono <| map_mono le)
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
A : Subring K
I : Ideal ↥A
hI : I ≠ ⊤
M : Ideal ↥A
hM : M.IsMaximal
le : I ≤ M
V : ValuationSubring K
hV : LocalSubring.ofPrime A M ≤ V.toLocalSubring
a : ↥A
ha : a ∈ (↑I : Set ↥A)
⊢ Membership.mem (α := K)
    (Subtype.val (p := fun (x : K) ↦ x ∈ V) ''
      (↑(map (F := ↥A →+* ↥V.toLocalSubring.toSubring)
            (RingHom.comp (β := ↥(LocalSubring.ofPrime A M).toSubring) (Subring.inclusion ⋯)
              (algebraMap ↥A ↥(LocalSubring.ofPrime A M).toSubring))
            I) :
        Set ↥V))
    ((A.subtype : (a : ↥A) → K) a : K)

Tactic:
⟨_, mem_map_of_mem _ ha, rfl⟩

Premises used: Ideal.mem_map_of_mem, Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
A : Subring K
I : Ideal ↥A
hI : I ≠ ⊤
M : Ideal ↥A
hM : M.IsMaximal
le : I ≤ M
V : ValuationSubring K
hV : LocalSubring.ofPrime A M ≤ V.toLocalSubring
a : ↥A
ha : a ∈ (↑I : Set ↥A)
⊢ Membership.mem (α := K)
    (Subtype.val (p := fun (x : K) ↦ x ∈ V) ''
      (↑(map (F := ↥A →+* ↥V.toLocalSubring.toSubring)
            (RingHom.comp (β := ↥(LocalSubring.ofPrime A M).toSubring) (Subring.inclusion ⋯)
              (algebraMap ↥A ↥(LocalSubring.ofPrime A M).toSubring))
            I) :
        Set ↥V))
    ((A.subtype : (a : ↥A) → K) a : K)

Tactic:
exact ⟨_, mem_map_of_mem _ ha, rfl⟩
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
x : K
R : Subring K
hxR : x ∉ R
inst_1 : IsIntegrallyClosedIn (↥R) K
inl : ∀ (hxR : 0 ∉ R), ∃ (V : ValuationSubring K), R ≤ V.toSubring ∧ 0 ∉ V
inr : ∀ (hx0 : x ≠ 0), ∃ (V : ValuationSubring K), R ≤ V.toSubring ∧ x ∉ V
⊢ ∃ (V : ValuationSubring K), R ≤ V.toSubring ∧ x ∉ V

Tactic:
obtain rfl | hx0 := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
R : Subring K
inst_1 : IsIntegrallyClosedIn (↥R) K
hxR : 0 ∉ R
⊢ ∃ (V : ValuationSubring K), R ≤ V.toSubring ∧ 0 ∉ V

Tactic:
(hxR R.zero_mem).elim

Premises used: Subring.zero_mem, False.elim
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
R : Subring K
inst_1 : IsIntegrallyClosedIn (↥R) K
hxR : 0 ∉ R
⊢ ∃ (V : ValuationSubring K), R ≤ V.toSubring ∧ 0 ∉ V

Tactic:
exact (hxR R.zero_mem).elim

Premises used: Subring.zero_mem, False.elim
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
x : K
R : Subring K
hxR : x ∉ R
inst_1 : IsIntegrallyClosedIn (↥R) K
hx0 : x ≠ 0
this : Invertible x := invertibleOfNonzero hx0
B : Subalgebra (↥R) K := (↥R)[x⁻¹]
xinv : ↥B.toSubring := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
eq : Eq (α := Ideal ↥B.toSubring) (Ideal.span {xinv}) ⊤
p : (↥R)[X]
hp : Membership.mem (γ := Ideal ↥R) ⊥ (p.leadingCoeff - 1)
hpx :
  Eq (α := K) ((aeval (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x⁻¹ _) : (a : (↥R)[X]) → K) p : K)
    (0 : K)
⊢ p.Monic

Tactic:
simpa [Monic, sub_eq_zero] using hp

Premises used: sub_eq_zero, Polynomial.Monic
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
x : K
R : Subring K
hxR : x ∉ R
inst_1 : IsIntegrallyClosedIn (↥R) K
hx0 : x ≠ 0
this : Invertible x := invertibleOfNonzero hx0
B : Subalgebra (↥R) K := (↥R)[x⁻¹]
xinv : ↥B.toSubring := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Ne (α := Ideal ↥B.toSubring) (Ideal.span {xinv}) ⊤

Tactic:
have : Ideal.span {xinv} ≠ ⊤ := fun eq ↦ hxR <|
    have ⟨p, hp, hpx⟩ := exists_aeval_invOf_eq_zero_of_idealMap_adjoin_sup_span_eq_top _
      (⊥ : Ideal R) bot_ne_top (top_unique <| eq.ge.trans le_add_self)
    (Subring.isIntegrallyClosedIn_iff).mp ‹_› ⟨p, by simpa [Monic, sub_eq_zero] using hp, hpx⟩
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
x : K
R : Subring K
hxR : x ∉ R
inst_1 : IsIntegrallyClosedIn (↥R) K
hx0 : x ≠ 0
this_1 : Invertible x := invertibleOfNonzero hx0
B : Subalgebra (↥R) K := (↥R)[x⁻¹]
xinv : ↥B.toSubring := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : Ne (α := Ideal ↥B.toSubring) (Ideal.span {xinv}) ⊤
inr :
  ∀ (V : ValuationSubring K)
    (hV :
      B.toSubring ≤ V.toSubring ∧
        (⇑B.toSubring.subtype : (a : ↥B.toSubring) → K) '' (↑(Ideal.span {xinv}) : Set ↥B.toSubring) ⊆
          (↑V.nonunits : Set K)),
    ∃ (V : ValuationSubring K), R ≤ V.toSubring ∧ x ∉ V
⊢ ∃ (V : ValuationSubring K), R ≤ V.toSubring ∧ x ∉ V

Tactic:
have ⟨V, hV⟩ := Ideal.image_subset_nonunits_valuationSubring _ this
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
x : K
R : Subring K
hxR : x ∉ R
inst_1 : IsIntegrallyClosedIn (↥R) K
hx0 : x ≠ 0
this_1 : Invertible x := invertibleOfNonzero hx0
B : Subalgebra (↥R) K := (↥R)[x⁻¹]
xinv : ↥B.toSubring := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : Ne (α := Ideal ↥B.toSubring) (Ideal.span {xinv}) ⊤
V : ValuationSubring K
hV :
  B.toSubring ≤ V.toSubring ∧
    (⇑B.toSubring.subtype : (a : ↥B.toSubring) → K) '' (↑(Ideal.span {xinv}) : Set ↥B.toSubring) ⊆ (↑V.nonunits : Set K)
⊢ ∃ (V : ValuationSubring K), R ≤ V.toSubring ∧ x ∉ V

Tactic:
⟨V, fun r hr ↦ hV.1 (B.algebraMap_mem ⟨r, hr⟩),
    (V.inv_mem_nonunits_iff.mp <| hV.2 ⟨_, Ideal.subset_span rfl, rfl⟩).resolve_left hx0⟩

Premises used: Ideal.subset_span, Or.resolve_left, Subtype.mk, And.right, And.left, ValuationSubring.inv_mem_nonunits_iff, And.intro, Exists.intro, Iff.mp, Subalgebra.algebraMap_mem, rfl
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
x : K
R : Subring K
hxR : x ∉ R
inst_1 : IsIntegrallyClosedIn (↥R) K
hx0 : x ≠ 0
this_1 : Invertible x := invertibleOfNonzero hx0
B : Subalgebra (↥R) K := (↥R)[x⁻¹]
xinv : ↥B.toSubring := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : Ne (α := Ideal ↥B.toSubring) (Ideal.span {xinv}) ⊤
V : ValuationSubring K
hV :
  B.toSubring ≤ V.toSubring ∧
    (⇑B.toSubring.subtype : (a : ↥B.toSubring) → K) '' (↑(Ideal.span {xinv}) : Set ↥B.toSubring) ⊆ (↑V.nonunits : Set K)
⊢ ∃ (V : ValuationSubring K), R ≤ V.toSubring ∧ x ∉ V

Tactic:
exact ⟨V, fun r hr ↦ hV.1 (B.algebraMap_mem ⟨r, hr⟩),
    (V.inv_mem_nonunits_iff.mp <| hV.2 ⟨_, Ideal.subset_span rfl, rfl⟩).resolve_left hx0⟩
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
x : K
R : LocalSubring K
hxR : x ∉ R.toSubring
inst_1 : IsIntegrallyClosedIn (↥R.toSubring) K
inl : ∀ (hxR : 0 ∉ R.toSubring), ∃ (V : ValuationSubring K), R ≤ V.toLocalSubring ∧ 0 ∉ V
inr : ∀ (hx0 : x ≠ 0), ∃ (V : ValuationSubring K), R ≤ V.toLocalSubring ∧ x ∉ V
⊢ ∃ (V : ValuationSubring K), R ≤ V.toLocalSubring ∧ x ∉ V

Tactic:
obtain rfl | hx0 := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
inst_1 : IsIntegrallyClosedIn (↥R.toSubring) K
hxR : 0 ∉ R.toSubring
⊢ ∃ (V : ValuationSubring K), R ≤ V.toLocalSubring ∧ 0 ∉ V

Tactic:
(hxR R.toSubring.zero_mem).elim

Premises used: Subring.zero_mem, False.elim, LocalSubring.toSubring
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
inst_1 : IsIntegrallyClosedIn (↥R.toSubring) K
hxR : 0 ∉ R.toSubring
⊢ ∃ (V : ValuationSubring K), R ≤ V.toLocalSubring ∧ 0 ∉ V

Tactic:
exact (hxR R.toSubring.zero_mem).elim

Premises used: Subring.zero_mem, False.elim, LocalSubring.toSubring