awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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), R ≤ V.toSubring ∧ x ∉ V
have 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
Tactic: have ⟨V, hV⟩ := Ideal.image_subset_nonunits_valuationSubring _ this
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
K : Type u_3
inst : Field K
x : K
R : LocalSubring K
hxR : x ∉ R.toSubring
inst_1 : IsIntegrallyClosedIn (↥R.toSubring) K
⊢ ∃ (V : ValuationSubring K), R ≤ V.toLocalSubring ∧ x ∉ V
have inl : ∀ (hxR : 0 ∉ R.toSubring), ∃ (V : ValuationSubring K), R ≤ V.toLocalSubring ∧ 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 : 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
⊢ ∃ (V : ValuationSubring K), R ≤ V.toLocalSubring ∧ x ∉ V
have inr : ∀ (hx0 : x ≠ 0), ∃ (V : ValuationSubring K), R ≤ V.toLocalSubring ∧ 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 : 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)
⊢ ∃ (V : ValuationSubring K), R ≤ V.toLocalSubring ∧ x ∉ V
have this₁ : 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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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), R ≤ V.toLocalSubring ∧ x ∉ V
have 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
Tactic: have ⟨V, hV⟩ := Ideal.image_subset_nonunits_valuationSubring (A := B.toSubring) _ this
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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
have 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 sorry)
      (maximalIdeal ↥V.toLocalSubring.toSubring))
    r
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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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
⊢ Membership.mem (γ := Submodule ↥R.toSubring ↥R.toSubring)
    (Ideal.comap (F := ↥R.toSubring →+* ↥V.toLocalSubring.toSubring) (Subring.inclusion ⋯)
      (maximalIdeal ↥V.toLocalSubring.toSubring))
    r
have 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 sorry)
      (maximalIdeal ↥V.toLocalSubring.toSubring))
    r
Tactic: rw [← V.image_maximalIdeal] at hV
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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))
have 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)
Tactic: refine .trans ?_ Subring.eq_iInf_of_isIntegrallyClosedIn.symm
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
K : Type u_3
inst : Field K
s : Set K
⊢ 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)
have 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)
Tactic: simp_rw [iInf_subtype]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
K : Type u_3
inst : Field K
s : Set K
⊢ 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)
have h : ∀ (V : ValuationSubring K),
  s ⊆ (↑V.toSubring : Set K) ↔
    Subalgebra.toSubring (R := ↥(Subring.closure s)) (integralClosure (↥(Subring.closure s)) K) ≤ V.toSubring
Tactic: congr! with V
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (hypothesis)
Goal:
K : Type u_3
inst : Field K
s : Set K
V : ValuationSubring K
⊢ s ⊆ (↑V.toSubring : Set K) ↔
    Subalgebra.toSubring (R := ↥(Subring.closure s)) (integralClosure (↥(Subring.closure s)) K) ≤ V.toSubring
have this : IsIntegrallyClosedIn (↥V.toSubring) K
Tactic: have : IsIntegrallyClosedIn V.toSubring K := inferInstanceAs (IsIntegrallyClosedIn V K)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
K : Type u_3
inst : Field K
s : Set K
V : ValuationSubring K
this : IsIntegrallyClosedIn (↥V.toSubring) K
⊢ s ⊆ (↑V.toSubring : Set K) ↔
    Subalgebra.toSubring (R := ↥(Subring.closure s)) (integralClosure (↥(Subring.closure s)) K) ≤ V.toSubring
have h : s ⊆ (↑V.toSubring : Set K) ↔ Subring.ofClass (S := Subring K) (Subring.closure s) ≤ V.toSubring
Tactic: rw [Subring.integralClosure_subring_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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)
have 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)
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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)
⊢ 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)
have 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)
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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)
    (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))
have 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)
Tactic: convert! (IsFractionRing.injective R K)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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
⊢ 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)
have 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))
  (⇑(g.comp f) : (a : R) → K)
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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
V : ValuationSubring K := { toSubring := RingHom.range.{u_1, u_3} (R := R) (algebraMap R K), mem_or_inv_mem' := ⋯ }
this : LocalSubring.range g ≤ V.toLocalSubring
x : S
⊢ ∃ (a : R),
    Eq.{u_3 + 1} (α := ↥(RingHom.range.{u_2, u_3} (R := S) g))
      ((RingHom.comp g.rangeRestrict f : (a : R) → ↥g.range) a : ↥(RingHom.range.{u_2, u_3} (R := S) g))
      (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subring K) (RingHom.range.{u_2, u_3} (R := S) g) x)
          ((g : (a : S) → K) x) ⋯ :
        ↥(RingHom.range.{u_2, u_3} (R := S) g))
have obtain : ∀ (y : R) (hy : Eq.{u_3 + 1} (α := K) (((algebraMap R K : R →+* K) : (a : R) → K) y : K) ((g : (a : S) → K) x : K)),
  ∃ (a : R),
    Eq.{u_3 + 1} (α := ↥(RingHom.range.{u_2, u_3} (R := S) g))
      ((RingHom.comp g.rangeRestrict f : (a : R) → ↥g.range) a : ↥(RingHom.range.{u_2, u_3} (R := S) g))
      (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subring K) (RingHom.range.{u_2, u_3} (R := S) g) x)
          ((g : (a : S) → K) x) sorry :
        ↥(RingHom.range.{u_2, u_3} (R := S) g))
Tactic: obtain ⟨y, hy⟩ := this.1 ⟨x, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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
V : ValuationSubring K := { toSubring := RingHom.range.{u_1, u_3} (R := R) (algebraMap R K), mem_or_inv_mem' := ⋯ }
⊢ 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)
have refine_2 : LocalSubring.range g ≤ V.toLocalSubring
Tactic: suffices LocalSubring.range g ≤ V.toLocalSubring by
      rintro ⟨_, x, rfl⟩
      obtain ⟨y, hy⟩ := this.1 ⟨x, rfl⟩
      exact ⟨y, Subtype.ext (by simpa [← h] using hy)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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
V : ValuationSubring K := { toSubring := RingHom.range.{u_1, u_3} (R := R) (algebraMap R K), mem_or_inv_mem' := ⋯ }
⊢ LocalSubring.range g ≤ V.toLocalSubring
have refine_2 : V.toLocalSubring ≤ LocalSubring.range g
Tactic: apply V.isMax_toLocalSubring
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (hypothesis)
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
V : ValuationSubring K := { toSubring := RingHom.range.{u_1, u_3} (R := R) (algebraMap R K), mem_or_inv_mem' := ⋯ }
⊢ V.toLocalSubring ≤ LocalSubring.range g
have H : LE.le.{u_3} (α := Subring K) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R K)) (RingHom.range.{u_2, u_3} (R := S) g)
Tactic: have H : (algebraMap R K).range ≤ g.range := fun x ⟨a, ha⟩ ↦ ⟨f a, by simp [← ha, ← h]⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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
V : ValuationSubring K := { toSubring := RingHom.range.{u_1, u_3} (R := R) (algebraMap R K), mem_or_inv_mem' := ⋯ }
H :
  LE.le.{u_3} (α := Subring K) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R K))
    (RingHom.range.{u_2, u_3} (R := S) g)
⊢ V.toLocalSubring ≤ LocalSubring.range g
have refine_2 : ∀ (a : ↥V.toLocalSubring.toSubring),
  IsUnit (M := ↥(LocalSubring.range g).toSubring)
      ((Subring.inclusion H : (a : ↥V.toLocalSubring.toSubring) → ↥(LocalSubring.range g).toSubring) a :
        ↥(LocalSubring.range g).toSubring) →
    IsUnit a
Tactic: refine ⟨H, ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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
V : ValuationSubring K := { toSubring := RingHom.range.{u_1, u_3} (R := R) (algebraMap R K), mem_or_inv_mem' := ⋯ }
H :
  LE.le.{u_3} (α := Subring K) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R K))
    (RingHom.range.{u_2, u_3} (R := S) g)
a : R
ha :
  IsUnit.{u_3} (M := ↥(RingHom.range.{u_2, u_3} (R := S) g))
    (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subring K) (RingHom.range.{u_2, u_3} (R := S) g) x)
        ((algebraMap R K : (a : R) → K) a) ⋯ :
      ↥(RingHom.range.{u_2, u_3} (R := S) g))
⊢ IsUnit.{u_3} (M := ↥V.toLocalSubring.toSubring)
    (Subtype.mk (p := fun (x : K) ↦ x ∈ V.toLocalSubring.toSubring) (((algebraMap R K : R →+* K) : (a : R) → K) a) ⋯ :
      ↥V.toLocalSubring.toSubring)
have refine_2 : IsUnit a
Tactic: suffices IsUnit a from this.map (algebraMap R K).rangeRestrict
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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
V : ValuationSubring K := { toSubring := RingHom.range.{u_1, u_3} (R := R) (algebraMap R K), mem_or_inv_mem' := ⋯ }
H :
  LE.le.{u_3} (α := Subring K) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R K))
    (RingHom.range.{u_2, u_3} (R := S) g)
a : R
ha :
  IsUnit.{u_3} (M := ↥(RingHom.range.{u_2, u_3} (R := S) g))
    (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subring K) (RingHom.range.{u_2, u_3} (R := S) g) x)
        ((algebraMap R K : (a : R) → K) a) ⋯ :
      ↥(RingHom.range.{u_2, u_3} (R := S) g))
⊢ IsUnit a
have refine_2 : IsUnit.{u_2} (M := S) ((f : (a : R) → S) a : S)
Tactic: apply IsUnit.of_map f
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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
V : ValuationSubring K := { toSubring := RingHom.range.{u_1, u_3} (R := R) (algebraMap R K), mem_or_inv_mem' := ⋯ }
H :
  LE.le.{u_3} (α := Subring K) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R K))
    (RingHom.range.{u_2, u_3} (R := S) g)
a : R
ha :
  IsUnit.{u_3} (M := ↥(RingHom.range.{u_2, u_3} (R := S) g))
    (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subring K) (RingHom.range.{u_2, u_3} (R := S) g) x)
        ((algebraMap R K : (a : R) → K) a) ⋯ :
      ↥(RingHom.range.{u_2, u_3} (R := S) g))
⊢ IsUnit.{u_2} (M := S) ((f : (a : R) → S) a : S)
have refine_2 : IsUnit.{u_3} (M := ↥(RingHom.range.{u_2, u_3} (R := S) g))
  ((g.rangeRestrict : (a : S) → ↥g.range) ((f : (a : R) → S) a) : ↥(RingHom.range.{u_2, u_3} (R := S) g))
Tactic: apply (IsLocalHom.of_surjective g.rangeRestrict g.rangeRestrict_surjective).1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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
V : ValuationSubring K := { toSubring := RingHom.range.{u_1, u_3} (R := R) (algebraMap R K), mem_or_inv_mem' := ⋯ }
H :
  LE.le.{u_3} (α := Subring K) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R K))
    (RingHom.range.{u_2, u_3} (R := S) g)
a : R
ha :
  IsUnit.{u_3} (M := ↥(RingHom.range.{u_2, u_3} (R := S) g))
    (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subring K) (RingHom.range.{u_2, u_3} (R := S) g) x)
        ((algebraMap R K : (a : R) → K) a) ⋯ :
      ↥(RingHom.range.{u_2, u_3} (R := S) g))
⊢ IsUnit.{u_3} (M := ↥(RingHom.range.{u_2, u_3} (R := S) g))
    ((g.rangeRestrict : (a : S) → ↥g.range) ((f : (a : R) → S) a) : ↥(RingHom.range.{u_2, u_3} (R := S) g))
have h₁ : Eq.{u_3 + 1} (α := K) ((↑((g.rangeRestrict : (a : S) → ↥g.range) ((f : (a : R) → S) a)) : K) : K)
  ((algebraMap R K : (a : R) → K) a : K)
Tactic: convert! ha