awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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
⊢ 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)
have 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)
Tactic: obtain ⟨C, hCA, hCB⟩ := hdir A B
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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)
have refine_1 : IsUnit (Subtype.mk (p := fun (x : K) ↦ x ∈ (↑C : LocalSubring K).toSubring) a sorry) →
  IsUnit
    (Subtype.mk (p := fun (x : K) ↦
      Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha)
Tactic: refine (C.1.2.2 (a := ⟨a, hCA haA⟩) (b := ⟨b, hCB hbB⟩) (Subtype.ext congr(($e).1))).imp ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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)
⊢ 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)
have refine_1₁ : IsUnit (Subtype.mk (p := fun (x : K) ↦ x ∈ (↑C : LocalSubring K).toSubring) b sorry) →
  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 ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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 := ⋯ }
have refine_2 : ∀ (a : ↥A.toSubring),
  IsUnit (M := ↥(toSubring { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := sorry }))
      (((Subring.inclusion sorry :
              ↥A.toSubring →+*
                ↥(toSubring
                    { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := sorry })) :
            (a : ↥A.toSubring) →
              ↥{ toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := sorry }.toSubring)
          a :
        ↥(toSubring { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := sorry })) →
    IsUnit a
Tactic: refine ⟨le_iSup (fun i : s ↦ i.1.toSubring) ⟨A, hA⟩, ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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 := ⋯ }))
⊢ IsUnit (Subtype.mk (p := fun (x : K) ↦ x ∈ A.toSubring) a haA)
have refine_2 : ∀ (b : K)
  (hb :
    Membership.mem (γ := Subring K)
      (toSubring { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := sorry }) b)
  (e :
    HMul.hMul (α :=
        ↥(toSubring
            { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := sorry :
              LocalSubring K }))
        (((Subring.inclusion sorry :
                ↥A.toSubring →+*
                  ↥(toSubring
                      { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := sorry :
                        LocalSubring K })) :
              (a : ↥A.toSubring) →
                ↥{ toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := sorry }.toSubring)
            (Subtype.mk (p := fun (x : K) ↦ x ∈ A.toSubring) a haA) :
          ↥(toSubring
              { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := sorry :
                LocalSubring K }))
        (Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K)
            (toSubring
              { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := sorry :
                LocalSubring K })
            x)
          b hb) =
      1),
  IsUnit (Subtype.mk (p := fun (x : K) ↦ x ∈ A.toSubring) a haA)
Tactic: obtain ⟨⟨b, hb⟩, e⟩ := isUnit_iff_exists_inv.mp h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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
⊢ IsUnit (Subtype.mk (p := fun (x : K) ↦ x ∈ A.toSubring) a haA)
have 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)
Tactic: obtain ⟨B, hbB : b ∈ B.1.toSubring⟩ := (Subring.mem_iSup_of_directed hdir).mp hb
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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
B : { a : LocalSubring K // a ∈ s }
hbB : b ∈ (↑B : LocalSubring K).toSubring
⊢ IsUnit (Subtype.mk (p := fun (x : K) ↦ x ∈ A.toSubring) a haA)
have refine_2 : ∀ (C : { a : LocalSubring K // a ∈ s })
  (hCA :
    LE.le.{u_3} (α := LocalSubring K)
      ((fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K))
        (Subtype.mk (p := fun (a : LocalSubring K) ↦ a ∈ s) A hA))
      ((fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) C))
  (hCB :
    LE.le.{u_3} (α := LocalSubring K) ((fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) B)
      ((fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K)) C)),
  IsUnit (Subtype.mk (p := fun (x : K) ↦ x ∈ A.toSubring) a haA)
Tactic: obtain ⟨C, hCA, hCB⟩ := H.directed ⟨A, hA⟩ B
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
K : Type u_3
inst : Field K
A : Subring K
I : Ideal ↥A
hI : I ≠ ⊤
⊢ ∃ (B : ValuationSubring K), A ≤ B.toSubring ∧ (⇑A.subtype : (a : ↥A) → K) '' (↑I : Set ↥A) ⊆ (↑B.nonunits : Set K)
have 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)
Tactic: have ⟨M, hM, le⟩ := I.exists_le_maximal hI
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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
⊢ ∃ (B : ValuationSubring K), A ≤ B.toSubring ∧ (⇑A.subtype : (a : ↥A) → K) '' (↑I : Set ↥A) ⊆ (↑B.nonunits : Set K)
have 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)
Tactic: have ⟨V, hV⟩ := (LocalSubring.ofPrime A M).exists_le_valuationSubring
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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)
have refine : (⇑A.subtype : (a : ↥A) → K) '' (↑I : Set ↥A) ⊆ (↑V.nonunits : Set K)
Tactic: refine ⟨V, (LocalSubring.le_ofPrime ..).trans hV.1, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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) ⊆ (↑V.nonunits : Set K)
have rw : (⇑A.subtype : (a : ↥A) → K) '' (↑I : Set ↥A) ⊆ Subtype.val (p := fun (x : K) ↦ x ∈ V) '' (↑(maximalIdeal ↥V) : Set ↥V)
Tactic: rw [← V.image_maximalIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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)
have 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 sorry)
          (maximalIdeal ↥(LocalSubring.ofPrime A M).toSubring)) :
      Set ↥V.toLocalSubring.toSubring)
Tactic: refine .trans ?_ (Set.image_mono <| ((local_hom_TFAE _).out 0 2).mp hV.2)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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 (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)
have 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 sorry)
            (algebraMap ↥A ↥(LocalSubring.ofPrime A M).toSubring))
          M) :
      Set ↥V.toLocalSubring.toSubring)
Tactic: rw [← IsLocalization.AtPrime.map_eq_maximalIdeal M, map_map]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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)
have 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 sorry)
            (algebraMap ↥A ↥(LocalSubring.ofPrime A M).toSubring))
          I) :
      Set ↥V)
Tactic: refine .trans ?_ (Set.image_mono <| map_mono le)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
K : Type u_3
inst : Field K
x : K
R : Subring K
hxR : x ∉ R
inst_1 : IsIntegrallyClosedIn (↥R) K
⊢ ∃ (V : ValuationSubring K), R ≤ V.toSubring ∧ x ∉ V
have inl : ∀ (hxR : 0 ∉ R), ∃ (V : ValuationSubring K), R ≤ V.toSubring ∧ 0 ∉ V
Tactic: obtain rfl | hx0 := eq_or_ne x 0
Cleared hypotheses: x, hxR
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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
⊢ ∃ (V : ValuationSubring K), R ≤ V.toSubring ∧ x ∉ V
have inr : ∀ (hx0 : x ≠ 0), ∃ (V : ValuationSubring K), R ≤ V.toSubring ∧ x ∉ V
Tactic: obtain rfl | hx0 := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (hypothesis)
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)
⊢ ∃ (V : ValuationSubring K), R ≤ V.toSubring ∧ x ∉ V
have this₁ : 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⟩