awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (hypothesis)
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x]
this : Algebra.IsIntegral.{u_3, u_3} ↥R.toSubring ↥S
Q : Ideal ↥S.toSubring
hQ : Q.IsMaximal
e :
  Eq (α := Ideal ↥R.toSubring) (Ideal.comap (F := ↥R.toSubring →+* ↥S) (algebraMap ↥R.toSubring ↥S) Q)
    (maximalIdeal ↥R.toSubring)
⊢ R = ofPrime S.toSubring Q
have hRS : R.toSubring ≤ S.toSubring
Tactic: have hRS : R.toSubring ≤ S.toSubring := fun r hr ↦ algebraMap_mem S ⟨r, hr⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x]
this : Algebra.IsIntegral.{u_3, u_3} ↥R.toSubring ↥S
Q : Ideal ↥S.toSubring
hQ : Q.IsMaximal
e :
  Eq (α := Ideal ↥R.toSubring) (Ideal.comap (F := ↥R.toSubring →+* ↥S) (algebraMap ↥R.toSubring ↥S) Q)
    (maximalIdeal ↥R.toSubring)
hRS : R.toSubring ≤ S.toSubring
⊢ R = ofPrime S.toSubring Q
have refine : LE.le (α := Ideal ↥(ofPrime S.toSubring Q).toSubring)
  (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥(ofPrime S.toSubring Q).toSubring) (Subring.inclusion sorry)
    (maximalIdeal ↥R.toSubring))
  (maximalIdeal ↥(ofPrime S.toSubring Q).toSubring)
Tactic: refine hR.eq_of_le ⟨hRS.trans (LocalSubring.le_ofPrime _ _), ((local_hom_TFAE _).out 2 0).mp ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x]
this : Algebra.IsIntegral.{u_3, u_3} ↥R.toSubring ↥S
Q : Ideal ↥S.toSubring
hQ : Q.IsMaximal
e :
  Eq (α := Ideal ↥R.toSubring) (Ideal.comap (F := ↥R.toSubring →+* ↥S) (algebraMap ↥R.toSubring ↥S) Q)
    (maximalIdeal ↥R.toSubring)
hRS : R.toSubring ≤ S.toSubring
| maximalIdeal ↥(ofPrime S.toSubring Q).toSubring
have rw : Ideal.map (F := ↥S.toSubring →+* ↥(ofPrime S.toSubring Q).toSubring)
  (algebraMap ↥S.toSubring ↥(ofPrime S.toSubring Q).toSubring) Q
Tactic: rw [← IsLocalization.AtPrime.map_eq_maximalIdeal Q]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x]
this : Algebra.IsIntegral.{u_3, u_3} ↥R.toSubring ↥S
Q : Ideal ↥S.toSubring
hQ : Q.IsMaximal
e :
  Eq (α := Ideal ↥R.toSubring) (Ideal.comap (F := ↥R.toSubring →+* ↥S) (algebraMap ↥R.toSubring ↥S) Q)
    (maximalIdeal ↥R.toSubring)
hRS : R.toSubring ≤ S.toSubring
⊢ LE.le (α := Ideal ↥(ofPrime S.toSubring Q).toSubring)
    (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥(ofPrime S.toSubring Q).toSubring) (Subring.inclusion ⋯)
      (maximalIdeal ↥R.toSubring))
    (maximalIdeal ↥(ofPrime S.toSubring Q).toSubring)
have conv_rhs : LE.le (α := Ideal ↥(ofPrime S.toSubring Q).toSubring)
  (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥(ofPrime S.toSubring Q).toSubring) (Subring.inclusion sorry)
    (maximalIdeal ↥R.toSubring))
  (Ideal.map (F := ↥S.toSubring →+* ↥(ofPrime S.toSubring Q).toSubring)
    (algebraMap ↥S.toSubring ↥(ofPrime S.toSubring Q).toSubring) Q)
Tactic: conv_rhs => rw [← IsLocalization.AtPrime.map_eq_maximalIdeal Q]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x]
this : Algebra.IsIntegral.{u_3, u_3} ↥R.toSubring ↥S
Q : Ideal ↥S.toSubring
hQ : Q.IsMaximal
e :
  Eq (α := Ideal ↥R.toSubring) (Ideal.comap (F := ↥R.toSubring →+* ↥S) (algebraMap ↥R.toSubring ↥S) Q)
    (maximalIdeal ↥R.toSubring)
hRS : R.toSubring ≤ S.toSubring
⊢ LE.le (α := Ideal ↥(ofPrime S.toSubring Q).toSubring)
    (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥(ofPrime S.toSubring Q).toSubring) (Subring.inclusion ⋯)
      (maximalIdeal ↥R.toSubring))
    (Ideal.map (F := ↥S.toSubring →+* ↥(ofPrime S.toSubring Q).toSubring)
      (algebraMap ↥S.toSubring ↥(ofPrime S.toSubring Q).toSubring) Q)
have refine : LE.le (α := Ideal ↥(ofPrime S.toSubring Q).toSubring)
  (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥(ofPrime S.toSubring Q).toSubring) (Subring.inclusion sorry)
    (maximalIdeal ↥R.toSubring))
  (Ideal.map (R := ↥S.toSubring) (F := ↥S.toSubring →+* ↥(ofPrime S.toSubring Q).toSubring)
    (algebraMap ↥S.toSubring ↥(ofPrime S.toSubring Q).toSubring)
    (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥S) (algebraMap ↥R.toSubring ↥S) (maximalIdeal ↥R.toSubring)))
Tactic: refine .trans ?_ (Ideal.map_mono <| Ideal.map_le_iff_le_comap.mpr e.ge)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x]
this : Algebra.IsIntegral.{u_3, u_3} ↥R.toSubring ↥S
Q : Ideal ↥S.toSubring
hQ : Q.IsMaximal
e :
  Eq (α := Ideal ↥R.toSubring) (Ideal.comap (F := ↥R.toSubring →+* ↥S) (algebraMap ↥R.toSubring ↥S) Q)
    (maximalIdeal ↥R.toSubring)
hRS : R.toSubring ≤ S.toSubring
⊢ LE.le (α := Ideal ↥(ofPrime S.toSubring Q).toSubring)
    (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥(ofPrime S.toSubring Q).toSubring) (Subring.inclusion ⋯)
      (maximalIdeal ↥R.toSubring))
    (Ideal.map (R := ↥S.toSubring) (F := ↥S.toSubring →+* ↥(ofPrime S.toSubring Q).toSubring)
      (algebraMap ↥S.toSubring ↥(ofPrime S.toSubring Q).toSubring)
      (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥S) (algebraMap ↥R.toSubring ↥S)
        (maximalIdeal ↥R.toSubring)))
have rw : LE.le (α := Ideal ↥(ofPrime S.toSubring Q).toSubring)
  (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥(ofPrime S.toSubring Q).toSubring) (Subring.inclusion sorry)
    (maximalIdeal ↥R.toSubring))
  (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥(ofPrime S.toSubring Q).toSubring) (Subring.inclusion sorry)
    (maximalIdeal ↥R.toSubring))
Tactic: rw [Ideal.map_map]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (hypothesis)
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x]
this : Algebra.IsIntegral.{u_3, u_3} ↥R.toSubring ↥S
Q : Ideal ↥S.toSubring
hQ : Q.IsMaximal
e :
  Eq (α := Ideal ↥R.toSubring) (Ideal.comap (F := ↥R.toSubring →+* ↥S) (algebraMap ↥R.toSubring ↥S) Q)
    (maximalIdeal ↥R.toSubring)
⊢ x ∈ R.toSubring
have this₁ : R = ofPrime S.toSubring Q
Tactic: have : R = .ofPrime S.toSubring Q := by
    have hRS : R.toSubring ≤ S.toSubring := fun r hr ↦ algebraMap_mem S ⟨r, hr⟩
    refine hR.eq_of_le ⟨hRS.trans (LocalSubring.le_ofPrime _ _), ((local_hom_TFAE _).out 2 0).mp ?_⟩
    conv_rhs => rw [← IsLocalization.AtPrime.map_eq_maximalIdeal Q]
    refine .trans ?_ (Ideal.map_mono <| Ideal.map_le_iff_le_comap.mpr e.ge)
    rw [Ideal.map_map]; rfl
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : IsIntegral (↥R.toSubring) x
S : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x]
this_1 : Algebra.IsIntegral.{u_3, u_3} ↥R.toSubring ↥S
Q : Ideal ↥S.toSubring
hQ : Q.IsMaximal
e :
  Eq (α := Ideal ↥R.toSubring) (Ideal.comap (F := ↥R.toSubring →+* ↥S) (algebraMap ↥R.toSubring ↥S) Q)
    (maximalIdeal ↥R.toSubring)
this : R = ofPrime S.toSubring Q
⊢ x ∈ R.toSubring
have rw : x ∈ (ofPrime S.toSubring Q).toSubring
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
K : Type u_3
inst : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
⊢ S ≤ R.toLocalSubring
have refine : ∀ (x : K) (hx : x ∈ S.toSubring) (h : x⁻¹ ∈ R.carrier), x ∈ R.toLocalSubring.toSubring
Tactic: refine (LocalSubring.toSubring_injective (hS.1.antisymm fun x hx ↦ (R.2 x).elim id fun h ↦ ?_)).ge
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
K : Type u_3
inst : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
h : x⁻¹ ∈ R.carrier
⊢ x ∈ R.toLocalSubring.toSubring
have by_contra : ∀ (h' : x ∉ R.toLocalSubring.toSubring), False
Tactic: by_contra h'
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (hypothesis)
Goal:
K : Type u_3
inst : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
h : x⁻¹ ∈ R.carrier
h' : x ∉ R.toLocalSubring.toSubring
⊢ False
have hx0 : x ≠ 0
Tactic: have hx0 : x ≠ 0 := by rintro rfl; exact h' R.zero_mem
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (hypothesis)
Goal:
K : Type u_3
inst : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
h : x⁻¹ ∈ R.carrier
h' : x ∉ R.toLocalSubring.toSubring
hx0 : x ≠ 0
⊢ False
have this : IsUnit (M := ↥S.toSubring)
  ((Subring.inclusion sorry : (a : ↥R.toLocalSubring.toSubring) → ↥S.toSubring)
      (Subtype.mk (p := fun (x : K) ↦ x ∈ R.toLocalSubring.toSubring) x⁻¹ h) :
    ↥S.toSubring)
Tactic: have : IsUnit (Subring.inclusion hS.1 ⟨x⁻¹, h⟩) :=
    isUnit_iff_exists_inv.mpr ⟨⟨x, hx⟩, Subtype.ext (inv_mul_cancel₀ hx0)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
K : Type u_3
inst : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
h : x⁻¹ ∈ R.carrier
h' : x ∉ R.toLocalSubring.toSubring
hx0 : x ≠ 0
this :
  IsUnit (M := ↥S.toSubring)
    ((Subring.inclusion ⋯ : (a : ↥R.toLocalSubring.toSubring) → ↥S.toSubring)
        (Subtype.mk (p := fun (x : K) ↦ x ∈ R.toLocalSubring.toSubring) x⁻¹ h) :
      ↥S.toSubring)
⊢ False
have obtain : ∀ (x' : ↥R.toLocalSubring.toSubring)
  (hx' : Subtype.mk (p := fun (x : K) ↦ x ∈ R.toLocalSubring.toSubring) x⁻¹ h * x' = 1), False
Tactic: obtain ⟨x', hx'⟩ := isUnit_iff_exists_inv.mp (hS.2.1 _ this)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (hypothesis)
Goal:
K : Type u_3
inst : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
h : x⁻¹ ∈ R.carrier
h' : x ∉ R.toLocalSubring.toSubring
hx0 : x ≠ 0
this :
  IsUnit (M := ↥S.toSubring)
    ((Subring.inclusion ⋯ : (a : ↥R.toLocalSubring.toSubring) → ↥S.toSubring)
        (Subtype.mk (p := fun (x : K) ↦ x ∈ R.toLocalSubring.toSubring) x⁻¹ h) :
      ↥S.toSubring)
x' : ↥R.toLocalSubring.toSubring
hx' : Subtype.mk (p := fun (x : K) ↦ x ∈ R.toLocalSubring.toSubring) x⁻¹ h * x' = 1
⊢ False
have this₁ : (↑x' : K) = x
Tactic: have : x' = x := by simpa [Subtype.ext_iff, inv_mul_eq_iff_eq_mul₀ hx0] using hx'
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
hR : IsMax R
⊢ ∃ (R' : ValuationSubring K), R'.toLocalSubring = R
have suffices : ∀ x ∉ R.toSubring, x⁻¹ ∈ R.toSubring
Tactic: suffices ∀ x ∉ R.toSubring, x⁻¹ ∈ R.toSubring from
    ⟨⟨R.toSubring, fun x ↦ or_iff_not_imp_left.mpr (this x)⟩, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
hR : IsMax R
⊢ ∀ x ∉ R.toSubring, x⁻¹ ∈ R.toSubring
have refine : ∀ (x : K) (hx : x ∉ R.toSubring), IsIntegral (↥R.toSubring) x⁻¹
Tactic: refine fun x hx ↦ mem_of_isMax_of_isIntegral hR ?_
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (hypothesis)
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
⊢ IsIntegral (↥R.toSubring) x⁻¹
have hx0 : x ≠ 0
Tactic: have hx0 : x ≠ 0 := fun e ↦ hx (e ▸ zero_mem _)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (hypothesis)
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
this : Invertible x := invertibleOfNonzero hx0
S : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x]
⊢ IsIntegral (↥R.toSubring) x⁻¹
have this₁ : R.toSubring < S.toSubring
Tactic: have : R.toSubring < S.toSubring := SetLike.lt_iff_le_and_exists.mpr
    ⟨fun r hr ↦ algebraMap_mem S ⟨r, hr⟩, ⟨x, self_mem_adjoin_singleton _ _, hx⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
this_1 : Invertible x := invertibleOfNonzero hx0
S : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x]
this : R.toSubring < S.toSubring
⊢ IsIntegral (↥R.toSubring) x⁻¹
have have : ∀ (p : Polynomial ↥R.toSubring)
  (hp : Membership.mem (γ := Ideal ↥R.toSubring) (maximalIdeal ↥R.toSubring) (p.leadingCoeff - 1))
  (hpx :
    Eq (α := K)
      ((Polynomial.aeval (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) :
            (a : Polynomial ↥R.toSubring) → K)
          p :
        K)
      (0 : K)),
  IsIntegral (↥R.toSubring) x⁻¹
Tactic: have ⟨p, hp, hpx⟩ := exists_aeval_invOf_eq_zero_of_idealMap_adjoin_sup_span_eq_top x _
    (maximalIdeal.isMaximal R.toSubring).ne_top
    (top_unique <| (map_maximalIdeal_eq_top_of_isMax hR this).ge.trans le_self_add)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (hypothesis)
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
this_1 : Invertible x := invertibleOfNonzero hx0
S : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x]
this : R.toSubring < S.toSubring
p : Polynomial ↥R.toSubring
hp : Membership.mem (γ := Ideal ↥R.toSubring) (maximalIdeal ↥R.toSubring) (p.leadingCoeff - 1)
hpx :
  Eq (α := K)
    ((Polynomial.aeval (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) :
          (a : Polynomial ↥R.toSubring) → K)
        p :
      K)
    (0 : K)
⊢ IsIntegral (↥R.toSubring) x⁻¹
have H : IsUnit p.leadingCoeff
Tactic: have H : IsUnit p.leadingCoeff := of_not_not fun h ↦ by simpa using sub_mem h hp
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
K : Type u_3
inst : Field K
A : LocalSubring K
this : ∃ (B : LocalSubring K), A ≤ B ∧ IsMax B
⊢ ∃ (B : ValuationSubring K), A ≤ B.toLocalSubring
have obtain : ∀ (B : LocalSubring K) (hB : A ≤ B) (hB' : IsMax B), ∃ (B : ValuationSubring K), A ≤ B.toLocalSubring
Tactic: obtain ⟨B, hB, hB'⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
K : Type u_3
inst : Field K
A B : LocalSubring K
hB : A ≤ B
hB' : IsMax B
⊢ ∃ (B : ValuationSubring K), A ≤ B.toLocalSubring
have obtain : ∀ (B : ValuationSubring K) (hB : A ≤ B.toLocalSubring) (hB' : IsMax B.toLocalSubring),
  ∃ (B : ValuationSubring K), A ≤ B.toLocalSubring
Tactic: obtain ⟨B, rfl⟩ := B.exists_valuationRing_of_isMax hB'
Cleared hypotheses: B, hB, hB'
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
K : Type u_3
inst : Field K
A : LocalSubring K
⊢ ∃ (B : ValuationSubring K), A ≤ B.toLocalSubring
have suffices : ∃ (B : LocalSubring K), A ≤ B ∧ IsMax B
Tactic: suffices ∃ B, A ≤ B ∧ IsMax B by
    obtain ⟨B, hB, hB'⟩ := this
    obtain ⟨B, rfl⟩ := B.exists_valuationRing_of_isMax hB'
    exact ⟨B, hB⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
K : Type u_3
inst : Field K
A : LocalSubring K
⊢ ∃ (B : LocalSubring K), A ≤ B ∧ IsMax B
have refine : ∀ c ⊆ Set.Ici A, IsChain (fun (x1 x2 : LocalSubring K) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ (ub : LocalSubring K), ∀ z ∈ c, z ≤ ub
Tactic: refine zorn_le_nonempty_Ici₀ _ ?_ _ le_rfl
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (hypothesis)
Goal:
K : Type u_3
inst : Field K
A : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A
H : IsChain (fun (x1 x2 : LocalSubring K) ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
⊢ ∃ (ub : LocalSubring K), ∀ z ∈ s, z ≤ ub
have inst : Nonempty.{u_3 + 1} (↑s : Type u_3)
Tactic: have inst : Nonempty s := ⟨⟨y, hys⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (hypothesis)
Goal:
K : Type u_3
inst_1 : Field K
A : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A
H : IsChain (fun (x1 x2 : LocalSubring K) ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty.{u_3 + 1} (↑s : Type u_3)
⊢ ∃ (ub : LocalSubring K), ∀ z ∈ s, z ≤ ub
have 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))
Tactic: have hdir := H.directed.mono_comp _ LocalSubring.toSubring_mono
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
K : Type u_3
inst_1 : Field K
A : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A
H : IsChain (fun (x1 x2 : LocalSubring K) ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty.{u_3 + 1} (↑s : Type u_3)
hdir :
  Directed.{u_3, u_3 + 1} (α := Subring K) (ι := { a : LocalSubring K // a ∈ s }) LE.le
    (toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K))
⊢ ∃ (ub : LocalSubring K), ∀ z ∈ s, z ≤ ub
have refine_1 : ∀ {a b : ↥(⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring)} (h : a + b = 1), IsUnit a ∨ IsUnit b
Tactic: refine ⟨@LocalSubring.mk _ _ (⨆ i : s, i.1.toSubring) ⟨?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
K : Type u_3
inst_1 : Field K
A : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A
H : IsChain (fun (x1 x2 : LocalSubring K) ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty.{u_3 + 1} (↑s : Type u_3)
hdir :
  Directed.{u_3, u_3 + 1} (α := Subring K) (ι := { a : LocalSubring K // a ∈ s }) LE.le
    (toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K))
refine_1 : ∀ {a b : ↥(⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring)} (h : a + b = 1), IsUnit a ∨ IsUnit b
⊢ ∃ (ub : LocalSubring K), ∀ z ∈ s, z ≤ ub
have refine_2 : ∀ z ∈ s, z ≤ { toSubring := ⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring, isLocalRing := sorry }
Tactic: refine ⟨@LocalSubring.mk _ _ (⨆ i : s, i.1.toSubring) ⟨?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
K : Type u_3
inst_1 : Field K
A : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A
H : IsChain (fun (x1 x2 : LocalSubring K) ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty.{u_3 + 1} (↑s : Type u_3)
hdir :
  Directed.{u_3, u_3 + 1} (α := Subring K) (ι := { a : LocalSubring K // a ∈ s }) LE.le
    (toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K))
a : K
ha : Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) a
⊢ ∀ {b : ↥(⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring)}
    (h :
      Subtype.mk (p := fun (x : K) ↦
            Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha +
          b =
        1),
    IsUnit
        (Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha) ∨
      IsUnit b
have refine_1 : ∀ (b : K) (hb : Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) b)
  (h :
    Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha +
        Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) b hb =
      1),
  IsUnit
      (Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha) ∨
    IsUnit
      (Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) b hb)
Tactic: ⟨b, hb⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
K : Type u_3
inst_1 : Field K
A : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A
H : IsChain (fun (x1 x2 : LocalSubring K) ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty.{u_3 + 1} (↑s : Type u_3)
hdir :
  Directed.{u_3, u_3 + 1} (α := Subring K) (ι := { a : LocalSubring K // a ∈ s }) LE.le
    (toSubring ∘ fun (x : { a : LocalSubring K // a ∈ s }) ↦ (↑x : LocalSubring K))
a : K
ha : Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) a
b : K
hb : Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) b
e :
  Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha +
      Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) b hb =
    1
⊢ 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 : ∀ (A : { a : LocalSubring K // a ∈ s }) (haA : a ∈ (↑A : LocalSubring K).toSubring),
  IsUnit
      (Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) a ha) ∨
    IsUnit
      (Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (⨆ (i : (↑s : Type u_3)), (↑i : LocalSubring K).toSubring) x) b hb)
Tactic: obtain ⟨A, haA : a ∈ A.1.toSubring⟩ := (Subring.mem_iSup_of_directed hdir).mp 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 : 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
⊢ 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 : ∀ (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)
Tactic: obtain ⟨B, hbB : b ∈ B.1.toSubring⟩ := (Subring.mem_iSup_of_directed hdir).mp hb