awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hx0 : x ≠ 0
this : Invertible x := invertibleOfNonzero hx0
B : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x⁻¹]
xinv : ↥B.toSubring := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
eq :
  HAdd.hAdd (α := Ideal ↥B)
      (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥B) (algebraMap ↥R.toSubring ↥B)
        (maximalIdeal ↥R.toSubring))
      (Ideal.span {xinv}) =
    ⊤
p : (↥R.toSubring)[X]
hp : Membership.mem (γ := Ideal ↥R.toSubring) (maximalIdeal ↥R.toSubring) (p.leadingCoeff - 1)
hpx :
  Eq (α := K)
    ((aeval (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x⁻¹ _) : (a : (↥R.toSubring)[X]) → K) p : K)
    (0 : K)
h : ¬IsUnit p.leadingCoeff
⊢ False

Tactic:
simpa using sub_mem h hp

Premises used: sub_mem
-- 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
hx0 : x ≠ 0
this : Invertible x := invertibleOfNonzero hx0
B : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x⁻¹]
xinv : ↥B.toSubring := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
eq :
  HAdd.hAdd (α := Ideal ↥B)
      (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥B) (algebraMap ↥R.toSubring ↥B)
        (maximalIdeal ↥R.toSubring))
      (Ideal.span {xinv}) =
    ⊤
p : (↥R.toSubring)[X]
hp : Membership.mem (γ := Ideal ↥R.toSubring) (maximalIdeal ↥R.toSubring) (p.leadingCoeff - 1)
hpx :
  Eq (α := K)
    ((aeval (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x⁻¹ _) : (a : (↥R.toSubring)[X]) → K) p : K)
    (0 : K)
H : IsUnit p.leadingCoeff
⊢ (HMul.hMul (α := (↥R.toSubring)[X])
      ((C : (a : ↥R.toSubring) → (↥R.toSubring)[X]) (↑H.unit⁻¹ : ↥R.toSubring) : (↥R.toSubring)[X]) p).Monic

Tactic:
simp [Polynomial.Monic]

Premises used: Polynomial.Monic
-- 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
hx0 : x ≠ 0
this : Invertible x := invertibleOfNonzero hx0
B : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x⁻¹]
xinv : ↥B.toSubring := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
eq :
  HAdd.hAdd (α := Ideal ↥B)
      (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥B) (algebraMap ↥R.toSubring ↥B)
        (maximalIdeal ↥R.toSubring))
      (Ideal.span {xinv}) =
    ⊤
p : (↥R.toSubring)[X]
hp : Membership.mem (γ := Ideal ↥R.toSubring) (maximalIdeal ↥R.toSubring) (p.leadingCoeff - 1)
hpx :
  Eq (α := K)
    ((aeval (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x⁻¹ _) : (a : (↥R.toSubring)[X]) → K) p : K)
    (0 : K)
H : IsUnit p.leadingCoeff
⊢ eval₂ (algebraMap (↥R.toSubring) K) x
      (HMul.hMul (α := (↥R.toSubring)[X])
        ((C : (a : ↥R.toSubring) → (↥R.toSubring)[X]) (↑H.unit⁻¹ : ↥R.toSubring) : (↥R.toSubring)[X]) p) =
    0

Tactic:
simpa using .inr hpx
-- 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
hx0 : x ≠ 0
this : Invertible x := invertibleOfNonzero hx0
B : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x⁻¹]
xinv : ↥B.toSubring := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ HAdd.hAdd (α := Ideal ↥B)
      (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥B) (algebraMap ↥R.toSubring ↥B)
        (maximalIdeal ↥R.toSubring))
      (Ideal.span {xinv}) ≠
    ⊤

Tactic:
have : (maximalIdeal R.toSubring).map (algebraMap _ B) + .span {xinv} ≠ ⊤ := fun eq ↦ hxR <|
    have ⟨p, hp, hpx⟩ := exists_aeval_invOf_eq_zero_of_idealMap_adjoin_sup_span_eq_top _ _
      (maximalIdeal.isMaximal R.toSubring).ne_top eq
    have H : IsUnit p.leadingCoeff := of_not_not fun h ↦ by simpa using sub_mem h hp
    (Subring.isIntegrallyClosedIn_iff).mp ‹_›
      ⟨.C H.unit⁻¹.1 * p, by simp [Polynomial.Monic], by simpa using .inr hpx⟩
-- 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
hx0 : x ≠ 0
this_1 : Invertible x := invertibleOfNonzero hx0
B : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x⁻¹]
xinv : ↥B.toSubring := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this :
  HAdd.hAdd (α := Ideal ↥B)
      (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥B) (algebraMap ↥R.toSubring ↥B)
        (maximalIdeal ↥R.toSubring))
      (Ideal.span {xinv}) ≠
    ⊤
inr :
  ∀ (V : ValuationSubring K)
    (hV :
      B.toSubring ≤ V.toSubring ∧
        (⇑B.toSubring.subtype : (a : ↥B.toSubring) → K) ''
            (↑(HAdd.hAdd (α := Ideal ↥B)
                  (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥B) (algebraMap ↥R.toSubring ↥B)
                    (maximalIdeal ↥R.toSubring))
                  (Ideal.span {xinv})) :
              Set ↥B.toSubring) ⊆
          (↑V.nonunits : Set K)),
    ∃ (V : ValuationSubring K), R ≤ V.toLocalSubring ∧ x ∉ V
⊢ ∃ (V : ValuationSubring K), R ≤ V.toLocalSubring ∧ x ∉ V

Tactic:
have ⟨V, hV⟩ := Ideal.image_subset_nonunits_valuationSubring (A := B.toSubring) _ this
-- 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
hx0 : x ≠ 0
this_1 : Invertible x := invertibleOfNonzero hx0
B : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x⁻¹]
xinv : ↥B.toSubring := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this :
  HAdd.hAdd (α := Ideal ↥B)
      (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥B) (algebraMap ↥R.toSubring ↥B)
        (maximalIdeal ↥R.toSubring))
      (Ideal.span {xinv}) ≠
    ⊤
V : ValuationSubring K
hV :
  B.toSubring ≤ V.toSubring ∧
    (⇑B.toSubring.subtype : (a : ↥B.toSubring) → K) ''
        (↑(HAdd.hAdd (α := Ideal ↥B)
              (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥B) (algebraMap ↥R.toSubring ↥B)
                (maximalIdeal ↥R.toSubring))
              (Ideal.span {xinv})) :
          Set ↥B.toSubring) ⊆
      (↑V.nonunits : Set K)
⊢ ∃ (V : ValuationSubring K), R ≤ V.toLocalSubring ∧ x ∉ V

Tactic:
⟨V, ⟨fun r hr ↦ hV.1 (B.algebraMap_mem ⟨r, hr⟩),
    ((local_hom_TFAE _).out 3 0).mp fun r hr ↦ ?_⟩, (V.inv_mem_nonunits_iff.mp <|
      hV.2 ⟨_, le_add_self (α := Ideal B) (Ideal.subset_span rfl), rfl⟩).resolve_left hx0⟩

Premises used: Ideal.subset_span, Or.resolve_left, Subtype.mk, List.TFAE.out, And.right, And.left, ValuationSubring.inv_mem_nonunits_iff, And.intro, Exists.intro, Iff.mp, Subalgebra.algebraMap_mem, OfNat.ofNat, le_add_self, IsLocalRing.local_hom_TFAE, rfl
-- 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
hx0 : x ≠ 0
this_1 : Invertible x := invertibleOfNonzero hx0
B : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x⁻¹]
xinv : ↥B.toSubring := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this :
  HAdd.hAdd (α := Ideal ↥B)
      (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥B) (algebraMap ↥R.toSubring ↥B)
        (maximalIdeal ↥R.toSubring))
      (Ideal.span {xinv}) ≠
    ⊤
V : ValuationSubring K
hV :
  B.toSubring ≤ V.toSubring ∧
    (⇑B.toSubring.subtype : (a : ↥B.toSubring) → K) ''
        (↑(HAdd.hAdd (α := Ideal ↥B)
              (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥B) (algebraMap ↥R.toSubring ↥B)
                (maximalIdeal ↥R.toSubring))
              (Ideal.span {xinv})) :
          Set ↥B.toSubring) ⊆
      (↑V.nonunits : Set K)
inr :
  ∀ (r : ↥R.toSubring) (hr : Membership.mem (γ := Submodule ↥R.toSubring ↥R.toSubring) (maximalIdeal ↥R.toSubring) r),
    Membership.mem (γ := Submodule ↥R.toSubring ↥R.toSubring)
      (Ideal.comap (F := ↥R.toSubring →+* ↥V.toLocalSubring.toSubring) (Subring.inclusion ⋯)
        (maximalIdeal ↥V.toLocalSubring.toSubring))
      r
⊢ ∃ (V : ValuationSubring K), R ≤ V.toLocalSubring ∧ x ∉ V

Tactic:
refine ⟨V, ⟨fun r hr ↦ hV.1 (B.algebraMap_mem ⟨r, hr⟩),
    ((local_hom_TFAE _).out 3 0).mp fun r hr ↦ ?_⟩, (V.inv_mem_nonunits_iff.mp <|
      hV.2 ⟨_, le_add_self (α := Ideal B) (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
hx0 : x ≠ 0
this_1 : Invertible x := invertibleOfNonzero hx0
B : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x⁻¹]
xinv : ↥B.toSubring := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this :
  HAdd.hAdd (α := Ideal ↥B)
      (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥B) (algebraMap ↥R.toSubring ↥B)
        (maximalIdeal ↥R.toSubring))
      (Ideal.span {xinv}) ≠
    ⊤
V : ValuationSubring K
hV :
  B.toSubring ≤ V.toSubring ∧
    (⇑B.toSubring.subtype : (a : ↥B.toSubring) → K) ''
        (↑(HAdd.hAdd (α := Ideal ↥B)
              (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥B) (algebraMap ↥R.toSubring ↥B)
                (maximalIdeal ↥R.toSubring))
              (Ideal.span {xinv})) :
          Set ↥B.toSubring) ⊆
      (↑V.nonunits : Set K)
r : ↥R.toSubring
hr : Membership.mem (γ := Submodule ↥R.toSubring ↥R.toSubring) (maximalIdeal ↥R.toSubring) r
inr :
  ∀
    (hV_1 :
      B.toSubring ≤ V.toSubring ∧
        (⇑B.toSubring.subtype : (a : ↥B.toSubring) → K) ''
            (↑(HAdd.hAdd (α := Ideal ↥B)
                  (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥B) (algebraMap ↥R.toSubring ↥B)
                    (maximalIdeal ↥R.toSubring))
                  (Ideal.span {xinv})) :
              Set ↥B.toSubring) ⊆
          Subtype.val (p := fun (x : K) ↦ x ∈ V) '' (↑(maximalIdeal ↥V) : Set ↥V))
    (r : ↥R.toSubring) (hr : Membership.mem (γ := Submodule ↥R.toSubring ↥R.toSubring) (maximalIdeal ↥R.toSubring) r),
    Membership.mem (γ := Submodule ↥R.toSubring ↥R.toSubring)
      (Ideal.comap (F := ↥R.toSubring →+* ↥V.toLocalSubring.toSubring) (Subring.inclusion ⋯)
        (maximalIdeal ↥V.toLocalSubring.toSubring))
      r
⊢ Membership.mem (γ := Submodule ↥R.toSubring ↥R.toSubring)
    (Ideal.comap (F := ↥R.toSubring →+* ↥V.toLocalSubring.toSubring) (Subring.inclusion ⋯)
      (maximalIdeal ↥V.toLocalSubring.toSubring))
    r

Tactic:
rw [← V.image_maximalIdeal] at hV

Premises used: ValuationSubring.image_maximalIdeal
-- 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
hx0 : x ≠ 0
this_1 : Invertible x := invertibleOfNonzero hx0
B : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x⁻¹]
xinv : ↥B.toSubring := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this :
  HAdd.hAdd (α := Ideal ↥B)
      (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥B) (algebraMap ↥R.toSubring ↥B)
        (maximalIdeal ↥R.toSubring))
      (Ideal.span {xinv}) ≠
    ⊤
V : ValuationSubring K
hV_1 :
  B.toSubring ≤ V.toSubring ∧
    (⇑B.toSubring.subtype : (a : ↥B.toSubring) → K) ''
        (↑(HAdd.hAdd (α := Ideal ↥B)
              (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥B) (algebraMap ↥R.toSubring ↥B)
                (maximalIdeal ↥R.toSubring))
              (Ideal.span {xinv})) :
          Set ↥B.toSubring) ⊆
      (↑V.nonunits : Set K)
hV :
  B.toSubring ≤ V.toSubring ∧
    (⇑B.toSubring.subtype : (a : ↥B.toSubring) → K) ''
        (↑(HAdd.hAdd (α := Ideal ↥B)
              (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥B) (algebraMap ↥R.toSubring ↥B)
                (maximalIdeal ↥R.toSubring))
              (Ideal.span {xinv})) :
          Set ↥B.toSubring) ⊆
      Subtype.val (p := fun (x : K) ↦ x ∈ V) '' (↑(maximalIdeal ↥V) : Set ↥V)
r : ↥R.toSubring
hr_1 : Membership.mem (γ := Submodule ↥R.toSubring ↥R.toSubring) (maximalIdeal ↥R.toSubring) r
property :
  Membership.mem (α := K) V
    ((B.toSubring.subtype : (a : ↥B.toSubring) → K) ((algebraMap ↥R.toSubring ↥B : (a : ↥R.toSubring) → ↥B) r : ↥B) : K)
hr :
  Membership.mem (α := ↥V) (↑(maximalIdeal ↥V) : Set ↥V)
    (Subtype.mk (p := fun (x : K) ↦ x ∈ V)
        ((B.toSubring.subtype : (a : ↥B.toSubring) → K) ((algebraMap ↥R.toSubring ↥B : (a : ↥R.toSubring) → ↥B) r : ↥B))
        property :
      ↥V)
⊢ Membership.mem (γ := Submodule ↥R.toSubring ↥R.toSubring)
    (Ideal.comap (F := ↥R.toSubring →+* ↥V.toLocalSubring.toSubring) (Subring.inclusion ⋯)
      (maximalIdeal ↥V.toLocalSubring.toSubring))
    r

Tactic:
hr

Premises used: iInf, Set.Mem, Set.iInter, setOf, nonunits, Set.preimage, Not
-- 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
hx0 : x ≠ 0
this_1 : Invertible x := invertibleOfNonzero hx0
B : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x⁻¹]
xinv : ↥B.toSubring := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this :
  HAdd.hAdd (α := Ideal ↥B)
      (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥B) (algebraMap ↥R.toSubring ↥B)
        (maximalIdeal ↥R.toSubring))
      (Ideal.span {xinv}) ≠
    ⊤
V : ValuationSubring K
hV_1 :
  B.toSubring ≤ V.toSubring ∧
    (⇑B.toSubring.subtype : (a : ↥B.toSubring) → K) ''
        (↑(HAdd.hAdd (α := Ideal ↥B)
              (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥B) (algebraMap ↥R.toSubring ↥B)
                (maximalIdeal ↥R.toSubring))
              (Ideal.span {xinv})) :
          Set ↥B.toSubring) ⊆
      (↑V.nonunits : Set K)
hV :
  B.toSubring ≤ V.toSubring ∧
    (⇑B.toSubring.subtype : (a : ↥B.toSubring) → K) ''
        (↑(HAdd.hAdd (α := Ideal ↥B)
              (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥B) (algebraMap ↥R.toSubring ↥B)
                (maximalIdeal ↥R.toSubring))
              (Ideal.span {xinv})) :
          Set ↥B.toSubring) ⊆
      Subtype.val (p := fun (x : K) ↦ x ∈ V) '' (↑(maximalIdeal ↥V) : Set ↥V)
r : ↥R.toSubring
hr_1 : Membership.mem (γ := Submodule ↥R.toSubring ↥R.toSubring) (maximalIdeal ↥R.toSubring) r
property :
  Membership.mem (α := K) V
    ((B.toSubring.subtype : (a : ↥B.toSubring) → K) ((algebraMap ↥R.toSubring ↥B : (a : ↥R.toSubring) → ↥B) r : ↥B) : K)
hr :
  Membership.mem (α := ↥V) (↑(maximalIdeal ↥V) : Set ↥V)
    (Subtype.mk (p := fun (x : K) ↦ x ∈ V)
        ((B.toSubring.subtype : (a : ↥B.toSubring) → K) ((algebraMap ↥R.toSubring ↥B : (a : ↥R.toSubring) → ↥B) r : ↥B))
        property :
      ↥V)
⊢ Membership.mem (γ := Submodule ↥R.toSubring ↥R.toSubring)
    (Ideal.comap (F := ↥R.toSubring →+* ↥V.toLocalSubring.toSubring) (Subring.inclusion ⋯)
      (maximalIdeal ↥V.toLocalSubring.toSubring))
    r

Tactic:
exact hr
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
R : Subring K
inst_1 : IsIntegrallyClosedIn (↥R) K
⊢ R = ⨅ (V : { V : ValuationSubring K // R ≤ V.toSubring }), (↑V : ValuationSubring K).toSubring

Tactic:
le_antisymm (le_iInf fun V ↦ V.2) fun _ h ↦ of_not_not fun hxR ↦
    have ⟨V, hV⟩ := R.exists_le_valuationSubring_of_isIntegrallyClosedIn hxR
    hV.2 (iInf_le_of_le (α := Subring K) ⟨V, hV.1⟩ le_rfl h)

Premises used: False, Subring.exists_le_valuationSubring_of_isIntegrallyClosedIn, le_iInf, le_antisymm, And.right, _private.0.Subring.eq_iInf_of_isIntegrallyClosedIn.match_1, of_not_not, Subtype.property
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
inst_1 : IsIntegrallyClosedIn (↥R.toSubring) K
⊢ R.toSubring = ⨅ (V : { V : ValuationSubring K // R ≤ V.toLocalSubring }), (↑V : ValuationSubring K).toSubring

Tactic:
le_antisymm (le_iInf fun V ↦ V.2.1) fun _ h ↦ of_not_not fun hxR ↦
    have ⟨V, hV⟩ := R.exists_le_valuationSubring_of_isIntegrallyClosedIn hxR
    hV.2 (iInf_le_of_le (α := Subring K) ⟨V, hV.1⟩ le_rfl h)

Premises used: False, LocalSubring.exists_le_valuationSubring_of_isIntegrallyClosedIn, le_iInf, le_antisymm, And.right, of_not_not, _private.0.LocalSubring.eq_iInf_of_isIntegrallyClosedIn.match_1, Subtype.property
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
s : Set K
⊢ Eq (α := Subring K)
    (⨅ (V : { V : ValuationSubring K // s ⊆ (↑V.toSubring : Set K) }), (↑V : ValuationSubring K).toSubring)
    (Subalgebra.toSubring (R := ↥(Subring.closure s)) (integralClosure (↥(Subring.closure s)) K))

Tactic:
.trans ?_ Subring.eq_iInf_of_isIntegrallyClosedIn.symm

Premises used: Subring.eq_iInf_of_isIntegrallyClosedIn, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
s : Set K
refine :
  Eq.{u_3 + 1} (α := Subring K)
    (⨅ (V : { V : ValuationSubring K // s ⊆ (↑V.toSubring : Set K) }), (↑V : ValuationSubring K).toSubring)
    (⨅ (V :
      { V : ValuationSubring K //
        Subalgebra.toSubring (R := ↥(Subring.closure s)) (integralClosure (↥(Subring.closure s)) K) ≤ V.toSubring }),
      (↑V : ValuationSubring K).toSubring)
⊢ Eq (α := Subring K)
    (⨅ (V : { V : ValuationSubring K // s ⊆ (↑V.toSubring : Set K) }), (↑V : ValuationSubring K).toSubring)
    (Subalgebra.toSubring (R := ↥(Subring.closure s)) (integralClosure (↥(Subring.closure s)) K))

Tactic:
refine .trans ?_ Subring.eq_iInf_of_isIntegrallyClosedIn.symm
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
s : Set K
simp_rw :
  Eq.{u_3 + 1} (α := Subring K) (⨅ (i : ValuationSubring K), ⨅ (_ : s ⊆ (↑i.toSubring : Set K)), i.toSubring)
    (⨅ (i : ValuationSubring K),
      ⨅ (_ : Subalgebra.toSubring (R := ↥(Subring.closure s)) (integralClosure (↥(Subring.closure s)) K) ≤ i.toSubring),
        i.toSubring)
⊢ Eq.{u_3 + 1} (α := Subring K)
    (⨅ (V : { V : ValuationSubring K // s ⊆ (↑V.toSubring : Set K) }), (↑V : ValuationSubring K).toSubring)
    (⨅ (V :
      { V : ValuationSubring K //
        Subalgebra.toSubring (R := ↥(Subring.closure s)) (integralClosure (↥(Subring.closure s)) K) ≤ V.toSubring }),
      (↑V : ValuationSubring K).toSubring)

Tactic:
simp_rw [iInf_subtype]

Premises used: iInf_subtype
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
s : Set K
h :
  ∀ (V : ValuationSubring K),
    s ⊆ (↑V.toSubring : Set K) ↔
      Subalgebra.toSubring (R := ↥(Subring.closure s)) (integralClosure (↥(Subring.closure s)) K) ≤ V.toSubring
⊢ Eq.{u_3 + 1} (α := Subring K) (⨅ (i : ValuationSubring K), ⨅ (_ : s ⊆ (↑i.toSubring : Set K)), i.toSubring)
    (⨅ (i : ValuationSubring K),
      ⨅ (_ : Subalgebra.toSubring (R := ↥(Subring.closure s)) (integralClosure (↥(Subring.closure s)) K) ≤ i.toSubring),
        i.toSubring)

Tactic:
congr! with V
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
s : Set K
V : ValuationSubring K
⊢ IsIntegrallyClosedIn (↥V.toSubring) K

Tactic:
have : IsIntegrallyClosedIn V.toSubring K := inferInstanceAs (IsIntegrallyClosedIn V K)
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
s : Set K
V : ValuationSubring K
this : IsIntegrallyClosedIn (↥V.toSubring) K
h : s ⊆ (↑V.toSubring : Set K) ↔ Subring.ofClass (S := Subring K) (Subring.closure s) ≤ V.toSubring
⊢ s ⊆ (↑V.toSubring : Set K) ↔
    Subalgebra.toSubring (R := ↥(Subring.closure s)) (integralClosure (↥(Subring.closure s)) K) ≤ V.toSubring

Tactic:
rw [Subring.integralClosure_subring_le_iff]

Premises used: Subring.integralClosure_subring_le_iff
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
s : Set K
V : ValuationSubring K
this : IsIntegrallyClosedIn (↥V.toSubring) K
⊢ s ⊆ (↑V.toSubring : Set K) ↔ Subring.ofClass (S := Subring K) (Subring.closure s) ≤ V.toSubring

Tactic:
Subring.closure_le.symm

Premises used: iInf, Set.Mem, Set.iInter, setOf, Subring.closure_le, Iff.symm
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
s : Set K
V : ValuationSubring K
this : IsIntegrallyClosedIn (↥V.toSubring) K
⊢ s ⊆ (↑V.toSubring : Set K) ↔ Subring.ofClass (S := Subring K) (Subring.closure s) ≤ V.toSubring

Tactic:
exact Subring.closure_le.symm

Premises used: Subring.closure_le, Iff.symm
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsLocalRing S
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst_8 : IsLocalHom (R := R) (S := S) f
⊢ Function.Bijective.{u_1 + 1, u_3 + 1} (α := R) (β := ↥(RingHom.range.{u_2, u_3} (R := S) g))
    (⇑(RingHom.comp g.rangeRestrict f) : (a : R) → ↥g.range)

Tactic:
⟨?_, ?_⟩

Premises used: And.intro, Function.Bijective
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsLocalRing S
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst_8 : IsLocalHom (R := R) (S := S) f
refine_1 :
  Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := ↥(RingHom.range.{u_2, u_3} (R := S) g))
    (⇑(RingHom.comp g.rangeRestrict f) : (a : R) → ↥g.range)
refine_2 :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := ↥(RingHom.range.{u_2, u_3} (R := S) g))
    (⇑(RingHom.comp g.rangeRestrict f) : (a : R) → ↥g.range)
⊢ Function.Bijective.{u_1 + 1, u_3 + 1} (α := R) (β := ↥(RingHom.range.{u_2, u_3} (R := S) g))
    (⇑(RingHom.comp g.rangeRestrict f) : (a : R) → ↥g.range)

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsLocalRing S
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst_8 : IsLocalHom (R := R) (S := S) f
⊢ Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)

Tactic:
(IsFractionRing.injective R K)

Premises used: IsFractionRing.injective
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsLocalRing S
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst_8 : IsLocalHom (R := R) (S := S) f
h₁ :
  Eq (α := R → K)
    (Function.comp (β := ↥(RingHom.range.{u_2, u_3} (R := S) g))
      (Subtype.val (p := fun (x : K) ↦ Membership.mem (γ := Subring K) (RingHom.range.{u_2, u_3} (R := S) g) x))
      (⇑(RingHom.comp g.rangeRestrict f) : (a : R) → ↥g.range))
    (⇑(algebraMap R K) : (a : R) → K)
⊢ Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := K)
    (Function.comp (β := ↥(RingHom.range.{u_2, u_3} (R := S) g))
      (Subtype.val (p := fun (x : K) ↦ Membership.mem (γ := Subring K) (RingHom.range.{u_2, u_3} (R := S) g) x))
      (⇑(RingHom.comp g.rangeRestrict f) : (a : R) → ↥g.range))

Tactic:
convert! (IsFractionRing.injective R K)

Premises used: IsFractionRing.injective