awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
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

Tactic:
hR.eq_of_le ⟨hRS.trans (LocalSubring.le_ofPrime _ _), ((local_hom_TFAE _).out 2 0).mp ?_⟩

Premises used: LocalSubring.le_ofPrime, List.TFAE.out, IsMax.eq_of_le, Exists.intro, Iff.mp, LE.le.trans, OfNat.ofNat, IsLocalRing.local_hom_TFAE
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
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
refine :
  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)
⊢ R = ofPrime S.toSubring Q

Tactic:
refine hR.eq_of_le ⟨hRS.trans (LocalSubring.le_ofPrime _ _), ((local_hom_TFAE _).out 2 0).mp ?_⟩

Premises used: LocalSubring.le_ofPrime, List.TFAE.out, IsMax.eq_of_le, Exists.intro, Iff.mp, LE.le.trans, OfNat.ofNat, IsLocalRing.local_hom_TFAE
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
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
rw :
  Ideal.map (F := ↥S.toSubring →+* ↥(ofPrime S.toSubring Q).toSubring)
    (algebraMap ↥S.toSubring ↥(ofPrime S.toSubring Q).toSubring) Q
| maximalIdeal ↥(ofPrime S.toSubring Q).toSubring

Tactic:
rw [← IsLocalization.AtPrime.map_eq_maximalIdeal Q]

Premises used: IsLocalization.AtPrime.map_eq_maximalIdeal
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
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
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 ⋯)
      (maximalIdeal ↥R.toSubring))
    (Ideal.map (F := ↥S.toSubring →+* ↥(ofPrime S.toSubring Q).toSubring)
      (algebraMap ↥S.toSubring ↥(ofPrime S.toSubring Q).toSubring) Q)
⊢ 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)

Tactic:
conv_rhs => rw [← IsLocalization.AtPrime.map_eq_maximalIdeal Q]

Premises used: IsLocalization.AtPrime.map_eq_maximalIdeal
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
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)

Tactic:
.trans ?_ (Ideal.map_mono <| Ideal.map_le_iff_le_comap.mpr e.ge)

Premises used: Iff.mpr, Eq.ge, Ideal.map_le_iff_le_comap, Ideal.map_mono, LE.le.trans
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
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
refine :
  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)))
⊢ 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)

Tactic:
refine .trans ?_ (Ideal.map_mono <| Ideal.map_le_iff_le_comap.mpr e.ge)
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
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
rw :
  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 := ↥R.toSubring) (F := ↥R.toSubring →+* ↥(ofPrime S.toSubring Q).toSubring) (Subring.inclusion ⋯)
      (maximalIdeal ↥R.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)))

Tactic:
rw [Ideal.map_map]

Premises used: Ideal.map_map
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
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 := ↥R.toSubring) (F := ↥R.toSubring →+* ↥(ofPrime S.toSubring Q).toSubring) (Subring.inclusion ⋯)
      (maximalIdeal ↥R.toSubring))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
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

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
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
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
rw : x ∈ (ofPrime S.toSubring Q).toSubring
⊢ x ∈ R.toSubring

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
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 ∈ (ofPrime S.toSubring Q).toSubring

Tactic:
LocalSubring.le_ofPrime _ _ (self_mem_adjoin_singleton _ _)

Premises used: LocalSubring.le_ofPrime, Algebra.self_mem_adjoin_singleton
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
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 ∈ (ofPrime S.toSubring Q).toSubring

Tactic:
exact LocalSubring.le_ofPrime _ _ (self_mem_adjoin_singleton _ _)

Premises used: LocalSubring.le_ofPrime
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
⊢ S ≤ R.toLocalSubring

Tactic:
(LocalSubring.toSubring_injective (hS.1.antisymm fun x hx ↦ (R.2 x).elim id fun h ↦ ?_)).ge

Premises used: Eq.ge, LE.le.antisymm, id, ValuationSubring.mem_or_inv_mem', Or.elim, LocalSubring.toSubring_injective
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
refine : ∀ (x : K) (hx : x ∈ S.toSubring) (h : x⁻¹ ∈ R.carrier), x ∈ R.toLocalSubring.toSubring
⊢ S ≤ R.toLocalSubring

Tactic:
refine (LocalSubring.toSubring_injective (hS.1.antisymm fun x hx ↦ (R.2 x).elim id fun h ↦ ?_)).ge

Premises used: Eq.ge, LE.le.antisymm, id, ValuationSubring.mem_or_inv_mem', Or.elim, LocalSubring.toSubring_injective
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
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
by_contra : ∀ (h' : x ∉ R.toLocalSubring.toSubring), False
⊢ x ∈ R.toLocalSubring.toSubring

Tactic:
by_contra h'
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
hx : 0 ∈ S.toSubring
h : 0⁻¹ ∈ R.carrier
h' : 0 ∉ R.toLocalSubring.toSubring
⊢ False

Tactic:
h' R.zero_mem

Premises used: ValuationSubring.zero_mem
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
hx : 0 ∈ S.toSubring
h : 0⁻¹ ∈ R.carrier
h' : 0 ∉ R.toLocalSubring.toSubring
⊢ False

Tactic:
exact h' R.zero_mem

Premises used: ValuationSubring.zero_mem
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
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
⊢ x ≠ 0

Tactic:
have hx0 : x ≠ 0 := by rintro rfl; exact h' R.zero_mem
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
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
⊢ 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)

Tactic:
have : IsUnit (Subring.inclusion hS.1 ⟨x⁻¹, h⟩) :=
    isUnit_iff_exists_inv.mpr ⟨⟨x, hx⟩, Subtype.ext (inv_mul_cancel₀ hx0)⟩
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
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)
obtain :
  ∀ (x' : ↥R.toLocalSubring.toSubring)
    (hx' : Subtype.mk (p := fun (x : K) ↦ x ∈ R.toLocalSubring.toSubring) x⁻¹ h * x' = 1), False
⊢ False

Tactic:
obtain ⟨x', hx'⟩ := isUnit_iff_exists_inv.mp (hS.2.1 _ this)

Premises used: IsLocalHom.map_nonunit, isUnit_iff_exists_inv, Iff.mp
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
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
⊢ (↑x' : K) = x

Tactic:
simpa [Subtype.ext_iff, inv_mul_eq_iff_eq_mul₀ hx0] using hx'

Premises used: inv_mul_eq_iff_eq_mul₀, Subtype.ext_iff
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
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
⊢ (↑x' : K) = x

Tactic:
have : x' = x := by simpa [Subtype.ext_iff, inv_mul_eq_iff_eq_mul₀ hx0] using hx'
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
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_1 :
  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
this : (↑x' : K) = x
⊢ False

Tactic:
h' (this ▸ x'.2)

Premises used: Eq.rec, Subtype.property
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
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_1 :
  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
this : (↑x' : K) = x
⊢ False

Tactic:
exact h' (this ▸ x'.2)

Premises used: Eq.rec, Subtype.property
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
hR : IsMax R
suffices : ∀ x ∉ R.toSubring, x⁻¹ ∈ R.toSubring
⊢ ∃ (R' : ValuationSubring K), R'.toLocalSubring = R

Tactic:
suffices ∀ x ∉ R.toSubring, x⁻¹ ∈ R.toSubring from
    ⟨⟨R.toSubring, fun x ↦ or_iff_not_imp_left.mpr (this x)⟩, rfl⟩
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
hR : IsMax R
⊢ ∀ x ∉ R.toSubring, x⁻¹ ∈ R.toSubring

Tactic:
fun x hx ↦ mem_of_isMax_of_isIntegral hR ?_

Premises used: LocalSubring.mem_of_isMax_of_isIntegral
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
hR : IsMax R
refine : ∀ (x : K) (hx : x ∉ R.toSubring), IsIntegral (↥R.toSubring) x⁻¹
⊢ ∀ x ∉ R.toSubring, x⁻¹ ∈ R.toSubring

Tactic:
refine fun x hx ↦ mem_of_isMax_of_isIntegral hR ?_

Premises used: LocalSubring.mem_of_isMax_of_isIntegral
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
⊢ x ≠ 0

Tactic:
have hx0 : x ≠ 0 := fun e ↦ hx (e ▸ zero_mem _)
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
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]
⊢ 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⟩⟩
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
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
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⁻¹
⊢ 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)
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
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)
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
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)
⊢ IsUnit p.leadingCoeff

Tactic:
have H : IsUnit p.leadingCoeff := of_not_not fun h ↦ by simpa using sub_mem h hp
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
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)
H : IsUnit p.leadingCoeff
⊢ (HMul.hMul (α := Polynomial ↥R.toSubring)
      ((Polynomial.C : (a : ↥R.toSubring) → Polynomial ↥R.toSubring) (↑H.unit⁻¹ : ↥R.toSubring) :
        Polynomial ↥R.toSubring)
      p).Monic

Tactic:
simp [Polynomial.Monic]

Premises used: Polynomial.Monic
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
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)
H : IsUnit p.leadingCoeff
⊢ Polynomial.eval₂ (algebraMap (↥R.toSubring) K) x⁻¹
      (HMul.hMul (α := Polynomial ↥R.toSubring)
        ((Polynomial.C : (a : ↥R.toSubring) → Polynomial ↥R.toSubring) (↑H.unit⁻¹ : ↥R.toSubring) :
          Polynomial ↥R.toSubring)
        p) =
    0

Tactic:
simpa using .inr hpx
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
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)
H : IsUnit p.leadingCoeff
⊢ IsIntegral (↥R.toSubring) x⁻¹

Tactic:
exact ⟨.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
A : LocalSubring K
⊢ IsMax A ↔ ∃ (B : ValuationSubring K), B.toLocalSubring = A

Tactic:
⟨exists_valuationRing_of_isMax, fun ⟨B, e⟩ ↦ e ▸ B.isMax_toLocalSubring⟩

Premises used: ValuationSubring.isMax_toLocalSubring, Eq.rec, LocalSubring.exists_valuationRing_of_isMax, Iff.intro, _private.0.LocalSubring.isMax_iff.match_1, IsMax