awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : CommRing A
K : Type u_3
inst_2 : Field K
inst_3 : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : y ≠ 0
hy : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
inr :
  ∀
    (this :
      ∀ (y : K) (h0 : y ≠ 0) (hy : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ))
        (hlt : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : K) → Γ) y : Γ)), Transcendental A y)
    (hlt : LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)), Transcendental A y
wlog! :
  ∀ (y : K) (h0 : y ≠ 0) (hy : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ))
    (hlt : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : K) → Γ) y : Γ)), Transcendental A y
⊢ Transcendental A y

Tactic:
wlog! hlt : 1 < v y generalizing y

Premises used: DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : CommRing A
K : Type u_3
inst_2 : Field K
inst_3 : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : y ≠ 0
hy : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
this :
  ∀ (y : K) (h0 : y ≠ 0) (hy : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ))
    (hlt : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : K) → Γ) y : Γ)), Transcendental A y
hlt : LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
inr : ¬IsAlgebraic A y⁻¹
⊢ Transcendental A y

Tactic:
rw [Transcendental, ← IsAlgebraic.inv_iff]

Premises used: Transcendental, IsAlgebraic.inv_iff
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : CommRing A
K : Type u_3
inst_2 : Field K
inst_3 : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : y ≠ 0
hy : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
this :
  ∀ (y : K) (h0 : y ≠ 0) (hy : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ))
    (hlt : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : K) → Γ) y : Γ)), Transcendental A y
hlt : LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
⊢ y⁻¹ ≠ 0

Tactic:
simpa
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : CommRing A
K : Type u_3
inst_2 : Field K
inst_3 : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : y ≠ 0
hy : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
this :
  ∀ (y : K) (h0 : y ≠ 0) (hy : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ))
    (hlt : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : K) → Γ) y : Γ)), Transcendental A y
hlt : LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
⊢ Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y⁻¹ : Γ) (1 : Γ)

Tactic:
simpa
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : CommRing A
K : Type u_3
inst_2 : Field K
inst_3 : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : y ≠ 0
hy : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
this :
  ∀ (y : K) (h0 : y ≠ 0) (hy : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ))
    (hlt : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : K) → Γ) y : Γ)), Transcendental A y
hlt : LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
inr : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : K) → Γ) y⁻¹ : Γ)
⊢ ¬IsAlgebraic A y⁻¹

Tactic:
apply this _ (by simpa) (by simpa)
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : CommRing A
K : Type u_3
inst_2 : Field K
inst_3 : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : y ≠ 0
hy : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
this :
  ∀ (y : K) (h0 : y ≠ 0) (hy : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ))
    (hlt : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : K) → Γ) y : Γ)), Transcendental A y
hlt : LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
inr : LT.lt.{u_1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
⊢ LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : K) → Γ) y⁻¹ : Γ)

Tactic:
rw [← val_lt_one_iff _ h0]

Premises used: Valuation.val_lt_one_iff
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : CommRing A
K : Type u_3
inst_2 : Field K
inst_3 : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : y ≠ 0
hy : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
this :
  ∀ (y : K) (h0 : y ≠ 0) (hy : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ))
    (hlt : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : K) → Γ) y : Γ)), Transcendental A y
hlt : LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
⊢ LT.lt.{u_1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)

Tactic:
lt_of_le_of_ne hlt hy

Premises used: lt_of_le_of_ne
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : CommRing A
K : Type u_3
inst_2 : Field K
inst_3 : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : y ≠ 0
hy : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
this :
  ∀ (y : K) (h0 : y ≠ 0) (hy : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ))
    (hlt : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : K) → Γ) y : Γ)), Transcendental A y
hlt : LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
⊢ LT.lt.{u_1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)

Tactic:
exact lt_of_le_of_ne hlt hy

Premises used: lt_of_le_of_ne
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : CommRing A
K : Type u_3
inst_2 : Field K
inst_3 : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : y ≠ 0
hy : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
hlt : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : K) → Γ) y : Γ)
⊢ ¬y = 0

Tactic:
simp_all only [ne_eq, Transcendental]

Premises used: ne_eq, Transcendental
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : CommRing A
K : Type u_3
inst_2 : Field K
inst_3 : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : y ≠ 0
hy : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
hlt : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : K) → Γ) y : Γ)
h0₁ : ¬y = 0
⊢ ¬Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)

Tactic:
simp_all only [ne_eq, Transcendental]

Premises used: ne_eq, Transcendental
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : CommRing A
K : Type u_3
inst_2 : Field K
inst_3 : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : y ≠ 0
hy : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
hlt : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : K) → Γ) y : Γ)
h0₁ : ¬y = 0
hy₁ : ¬Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
⊢ LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : K) → Γ) y : Γ)

Tactic:
simp_all only [ne_eq, Transcendental]

Premises used: ne_eq, Transcendental
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : CommRing A
K : Type u_3
inst_2 : Field K
inst_3 : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : ¬y = 0
hy : ¬Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
hlt : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : K) → Γ) y : Γ)
by_contra! : ∀ (this : IsAlgebraic A y), False
⊢ ¬IsAlgebraic A y

Tactic:
by_contra!
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : CommRing A
K : Type u_3
inst_2 : Field K
inst_3 : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : ¬y = 0
hy : ¬Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
hlt : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : K) → Γ) y : Γ)
this : IsAlgebraic A y
replace :
  ∀ (p : A[X]) (hpnt : p ≠ 0)
    (hp :
      Eq.{u_3 + 1} (α := K) (((aeval ((algebraMap K K : (a : K) → K) y) : A[X] →ₐ[A] K) : (a : A[X]) → K) p : K)
        (0 : K)),
    False
⊢ False

Tactic:
replace ⟨p, hpnt, hp⟩ : IsAlgebraic A y := .algebraMap this
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : CommRing A
K : Type u_3
inst_2 : Field K
inst_3 : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : ¬y = 0
hy : ¬Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
hlt : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : K) → Γ) y : Γ)
this_1 : IsAlgebraic A y
p : A[X]
hpnt : p ≠ 0
hp : Eq.{u_3 + 1} (α := K) (((aeval ((algebraMap K K : (a : K) → K) y) : A[X] →ₐ[A] K) : (a : A[X]) → K) p : K) (0 : K)
this : HPow.hPow (α := Γ) ((v : (a : K) → Γ) y : Γ) p.natDegree = 0
⊢ False

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : CommRing A
K : Type u_3
inst_2 : Field K
inst_3 : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : ¬y = 0
hy : ¬Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
hlt : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : K) → Γ) y : Γ)
this : IsAlgebraic A y
p : A[X]
hpnt : p ≠ 0
hp : Eq.{u_3 + 1} (α := K) (((aeval ((algebraMap K K : (a : K) → K) y) : A[X] →ₐ[A] K) : (a : A[X]) → K) p : K) (0 : K)
suffices : HPow.hPow (α := Γ) ((v : (a : K) → Γ) y : Γ) p.natDegree = 0
⊢ False

Tactic:
suffices v y ^ p.natDegree = 0 by simp_all
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : CommRing A
K : Type u_3
inst_2 : Field K
inst_3 : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : ¬y = 0
hy : ¬Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
hlt : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : K) → Γ) y : Γ)
this : IsAlgebraic A y
p : A[X]
hpnt : p ≠ 0
hp : Eq.{u_3 + 1} (α := K) (((aeval ((algebraMap K K : (a : K) → K) y) : A[X] →ₐ[A] K) : (a : A[X]) → K) p : K) (0 : K)
rw : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((aeval y : (a : A[X]) → K) p : K) : Γ) (0 : Γ)
rw₁ : p ≠ 0
⊢ HPow.hPow (α := Γ) ((v : (a : K) → Γ) y : Γ) p.natDegree = 0

Tactic:
rw [← valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X _ hlt]

Premises used: Polynomial.valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : CommRing A
K : Type u_3
inst_2 : Field K
inst_3 : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : ¬y = 0
hy : ¬Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
hlt : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : K) → Γ) y : Γ)
this : IsAlgebraic A y
p : A[X]
hpnt : p ≠ 0
hp : Eq.{u_3 + 1} (α := K) (((aeval ((algebraMap K K : (a : K) → K) y) : A[X] →ₐ[A] K) : (a : A[X]) → K) p : K) (0 : K)
⊢ Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((aeval y : (a : A[X]) → K) p : K) : Γ) (0 : Γ)

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : CommRing A
K : Type u_3
inst_2 : Field K
inst_3 : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : ¬y = 0
hy : ¬Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
hlt : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : K) → Γ) y : Γ)
this : IsAlgebraic A y
p : A[X]
hpnt : p ≠ 0
hp : Eq.{u_3 + 1} (α := K) (((aeval ((algebraMap K K : (a : K) → K) y) : A[X] →ₐ[A] K) : (a : A[X]) → K) p : K) (0 : K)
⊢ p ≠ 0

Tactic:
simp_all
-- 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
V : ValuationSubring K
rw : IsIntegrallyClosed.{u_3} ↥V.valuation.integer
⊢ IsIntegrallyClosed.{u_3} ↥V.toSubring

Tactic:
rw [← V.integer_valuation]

Premises used: ValuationSubring.integer_valuation
-- 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
V : ValuationSubring K
⊢ IsIntegrallyClosed.{u_3} ↥V.valuation.integer

Tactic:
infer_instance
-- 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
V : ValuationSubring K
⊢ IsIntegrallyClosed.{u_3} ↥V

Tactic:
inferInstanceAs (IsIntegrallyClosed V.toSubring)

Premises used: _private.0.instIsIntegrallyClosedSubtypeMemValuationSubring._proof_1
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
⊢ Function.Injective.{u_3 + 1, u_3 + 1} (α := ValuationSubring K) toLocalSubring

Tactic:
fun _ _ h ↦ ValuationSubring.toSubring_injective congr(($h).toSubring)

Premises used: congrArg, id, LocalSubring.toSubring, ValuationSubring.toSubring_injective, Function.Injective
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
hR : IsMax R
S : Subring K
hS : R.toSubring < S
set :
  let mR : Ideal ↥S := Ideal.map (R := ↥R.toSubring) (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring);
  mR = ⊤
⊢ Eq (α := Ideal ↥S) (Ideal.map (R := ↥R.toSubring) (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)) ⊤

Tactic:
set mR := (maximalIdeal R.toSubring).map (Subring.inclusion hS.le)

Premises used: Subring.inclusion, IsLocalRing.maximalIdeal, Membership.mem, Subtype, Ideal.map, LT.lt.le, LocalSubring.toSubring
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
hR : IsMax R
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (R := ↥R.toSubring) (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
by_contra : ∀ (h_is_not_top : ¬mR = ⊤), False
⊢ mR = ⊤

Tactic:
by_contra h_is_not_top
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
hR : IsMax R
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (R := ↥R.toSubring) (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
h_is_not_top : ¬mR = ⊤
obtain : ∀ (M : Ideal ↥S) (h_is_max : M.IsMaximal) (h_incl : mR ≤ M), False
⊢ False

Tactic:
obtain ⟨M, h_is_max, h_incl⟩ := Ideal.exists_le_maximal _ h_is_not_top

Premises used: Ideal.exists_le_maximal
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
hR : IsMax R
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (R := ↥R.toSubring) (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
h_is_not_top : ¬mR = ⊤
M : Ideal ↥S
h_is_max : M.IsMaximal
h_incl : mR ≤ M
fSₘ : LocalSubring K := ofPrime S M
⊢ R ≤ fSₘ

Tactic:
⟨hS.le.trans (LocalSubring.le_ofPrime ..), ((local_hom_TFAE _).out 2 0).mp ?_⟩

Premises used: LT.lt.le, LocalSubring.le_ofPrime, List.TFAE.out, 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
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (R := ↥R.toSubring) (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
h_is_not_top : ¬mR = ⊤
M : Ideal ↥S
h_is_max : M.IsMaximal
h_incl : mR ≤ M
fSₘ : LocalSubring K := ofPrime S M
refine :
  LE.le (α := Ideal ↥fSₘ.toSubring)
    (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥fSₘ.toSubring) (Subring.inclusion ⋯)
      (maximalIdeal ↥R.toSubring))
    (maximalIdeal ↥fSₘ.toSubring)
⊢ R ≤ fSₘ

Tactic:
refine ⟨hS.le.trans (LocalSubring.le_ofPrime ..), ((local_hom_TFAE _).out 2 0).mp ?_⟩
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
hR : IsMax R
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (R := ↥R.toSubring) (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
h_is_not_top : ¬mR = ⊤
M : Ideal ↥S
h_is_max : M.IsMaximal
h_incl : mR ≤ M
fSₘ : LocalSubring K := ofPrime S M
rw : Ideal.map (F := ↥S →+* ↥fSₘ.toSubring) (algebraMap ↥S ↥fSₘ.toSubring) M
| maximalIdeal ↥fSₘ.toSubring

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

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
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (R := ↥R.toSubring) (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
h_is_not_top : ¬mR = ⊤
M : Ideal ↥S
h_is_max : M.IsMaximal
h_incl : mR ≤ M
fSₘ : LocalSubring K := ofPrime S M
conv_rhs :
  LE.le (α := Ideal ↥fSₘ.toSubring)
    (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥fSₘ.toSubring) (Subring.inclusion ⋯)
      (maximalIdeal ↥R.toSubring))
    (Ideal.map (F := ↥S →+* ↥fSₘ.toSubring) (algebraMap ↥S ↥fSₘ.toSubring) M)
⊢ LE.le (α := Ideal ↥fSₘ.toSubring)
    (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥fSₘ.toSubring) (Subring.inclusion ⋯)
      (maximalIdeal ↥R.toSubring))
    (maximalIdeal ↥fSₘ.toSubring)

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

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
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (R := ↥R.toSubring) (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
h_is_not_top : ¬mR = ⊤
M : Ideal ↥S
h_is_max : M.IsMaximal
h_incl : mR ≤ M
fSₘ : LocalSubring K := ofPrime S M
⊢ LE.le (α := Ideal ↥fSₘ.toSubring)
    (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥fSₘ.toSubring) (Subring.inclusion ⋯)
      (maximalIdeal ↥R.toSubring))
    (Ideal.map (F := ↥S →+* ↥fSₘ.toSubring) (algebraMap ↥S ↥fSₘ.toSubring) M)

Tactic:
.trans ?_ (Ideal.map_mono h_incl)

Premises used: 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
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (R := ↥R.toSubring) (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
h_is_not_top : ¬mR = ⊤
M : Ideal ↥S
h_is_max : M.IsMaximal
h_incl : mR ≤ M
fSₘ : LocalSubring K := ofPrime S M
refine :
  LE.le (α := Ideal ↥fSₘ.toSubring)
    (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥fSₘ.toSubring) (Subring.inclusion ⋯)
      (maximalIdeal ↥R.toSubring))
    (Ideal.map (F := ↥S →+* ↥fSₘ.toSubring) (algebraMap ↥S ↥fSₘ.toSubring) mR)
⊢ LE.le (α := Ideal ↥fSₘ.toSubring)
    (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥fSₘ.toSubring) (Subring.inclusion ⋯)
      (maximalIdeal ↥R.toSubring))
    (Ideal.map (F := ↥S →+* ↥fSₘ.toSubring) (algebraMap ↥S ↥fSₘ.toSubring) M)

Tactic:
refine .trans ?_ (Ideal.map_mono h_incl)
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
hR : IsMax R
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (R := ↥R.toSubring) (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
h_is_not_top : ¬mR = ⊤
M : Ideal ↥S
h_is_max : M.IsMaximal
h_incl : mR ≤ M
fSₘ : LocalSubring K := ofPrime S M
rw :
  LE.le (α := Ideal ↥fSₘ.toSubring)
    (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥fSₘ.toSubring) (Subring.inclusion ⋯)
      (maximalIdeal ↥R.toSubring))
    (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥fSₘ.toSubring) (Subring.inclusion ⋯)
      (maximalIdeal ↥R.toSubring))
⊢ LE.le (α := Ideal ↥fSₘ.toSubring)
    (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥fSₘ.toSubring) (Subring.inclusion ⋯)
      (maximalIdeal ↥R.toSubring))
    (Ideal.map (F := ↥S →+* ↥fSₘ.toSubring) (algebraMap ↥S ↥fSₘ.toSubring) mR)

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
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (R := ↥R.toSubring) (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
h_is_not_top : ¬mR = ⊤
M : Ideal ↥S
h_is_max : M.IsMaximal
h_incl : mR ≤ M
fSₘ : LocalSubring K := ofPrime S M
⊢ LE.le (α := Ideal ↥fSₘ.toSubring)
    (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥fSₘ.toSubring) (Subring.inclusion ⋯)
      (maximalIdeal ↥R.toSubring))
    (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥fSₘ.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
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (R := ↥R.toSubring) (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
h_is_not_top : ¬mR = ⊤
M : Ideal ↥S
h_is_max : M.IsMaximal
h_incl : mR ≤ M
fSₘ : LocalSubring K := ofPrime S M
⊢ R ≤ fSₘ

Tactic:
have h_RleSₘ : R ≤ fSₘ := by
    refine ⟨hS.le.trans (LocalSubring.le_ofPrime ..), ((local_hom_TFAE _).out 2 0).mp ?_⟩
    conv_rhs => rw [← IsLocalization.AtPrime.map_eq_maximalIdeal M]
    refine .trans ?_ (Ideal.map_mono h_incl)
    rw [Ideal.map_map]; rfl
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
K : Type u_3
inst : Field K
R : LocalSubring K
hR : IsMax R
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (R := ↥R.toSubring) (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
h_is_not_top : ¬mR = ⊤
M : Ideal ↥S
h_is_max : M.IsMaximal
h_incl : mR ≤ M
fSₘ : LocalSubring K := ofPrime S M
h_RleSₘ : R ≤ fSₘ
⊢ False

Tactic:
exact (hR.eq_of_le h_RleSₘ ▸ hS).not_ge (LocalSubring.le_ofPrime ..)
-- 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]
⊢ ∀ (x_1 : K), Membership.mem (γ := Set K) {x} x_1 → IsIntegral (↥R.toSubring) x_1

Tactic:
simpa
-- 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]
⊢ Algebra.IsIntegral.{u_3, u_3} ↥R.toSubring ↥S

Tactic:
have : Algebra.IsIntegral R.toSubring S := Algebra.IsIntegral.adjoin (by simpa)
-- 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
⊢ Ne (α := Ideal ↥R.toSubring) (RingHom.ker (F := ↥R.toSubring →+* ↥S) (algebraMap ↥R.toSubring ↥S)) ⊤

Tactic:
simp
-- 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
obtain :
  ∀ (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
⊢ x ∈ R.toSubring

Tactic:
obtain ⟨Q : Ideal S.toSubring, hQ, e⟩ := Ideal.exists_ideal_over_maximal_of_isIntegral
    (S := S) (maximalIdeal R.toSubring) (le_maximalIdeal (by simp))

Premises used: IsLocalRing.maximalIdeal, Membership.mem, Subtype, Ideal, LocalSubring.toSubring, Subalgebra.toSubring, IsLocalRing.le_maximalIdeal, Ideal.exists_ideal_over_maximal_of_isIntegral
-- 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.toSubring ≤ S.toSubring

Tactic:
have hRS : R.toSubring ≤ S.toSubring := fun r hr ↦ algebraMap_mem S ⟨r, hr⟩