awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integral (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
x : R
h_1 : Nontrivial R
this : Nontrivial O
h : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ IsIntegral O x
have mpr : ∀ (y : O) (h : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) y : R) : Γ₀) (1 : Γ₀)),
  IsIntegral.{w, u} O (A := R) ((algebraMap O R : (a : O) → R) y : R)
Tactic: obtain ⟨y, rfl⟩ := hv.exists_of_le_one h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integral (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
h_1 : Nontrivial R
this : Nontrivial O
y : O
h : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) y : R) : Γ₀) (1 : Γ₀)
⊢ (HSub.hSub (α := O[X]) (β := O[X]) X ((C : (a : O) → O[X]) y : O[X])).Monic
have pn : (HSub.hSub (α := O[X]) (β := O[X]) X ((C : (a : O) → O[X]) y : O[X])).natDegree ≤ max 1 0
Tactic: monicity
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integral (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
h_1 : Nontrivial R
this : Nontrivial O
y : O
h : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) y : R) : Γ₀) (1 : Γ₀)
pn : (HSub.hSub (α := O[X]) (β := O[X]) X ((C : (a : O) → O[X]) y : O[X])).natDegree ≤ max 1 0
⊢ (HSub.hSub (α := O[X]) (β := O[X]) X ((C : (a : O) → O[X]) y : O[X])).Monic
have p1 : (HSub.hSub (α := O[X]) (β := O[X]) X ((C : (a : O) → O[X]) y : O[X])).coeff (max 1 0) = 1
Tactic: monicity
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integral (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
h_1 : Nontrivial R
this : Nontrivial O
y : O
h : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) y : R) : Γ₀) (1 : Γ₀)
pn : (HSub.hSub (α := O[X]) (β := O[X]) X ((C : (a : O) → O[X]) y : O[X])).natDegree ≤ max 1 0
p1 : (HSub.hSub (α := O[X]) (β := O[X]) X ((C : (a : O) → O[X]) y : O[X])).coeff (max 1 0) = 1
⊢ (HSub.hSub (α := O[X]) (β := O[X]) X ((C : (a : O) → O[X]) y : O[X])).Monic
have n : ℕ
Tactic: monicity
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integral (hypothesis)
Goal:
K : Type u
Γ₀ : Type v
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O K
hv : v.Integers O
⊢ IsIntegrallyClosed O
have this : IsFractionRing O K
Tactic: have : IsFractionRing O K := hv.isFractionRing
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.IsTrivialOn (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : CommSemiring A
B : Type u_3
inst_2 : Ring B
inst_3 : Algebra A B
v : Valuation B Γ
hv : Valuation.IsTrivialOn A v
w : B
hpos : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : B) → Γ) w : Γ)
p : A[X]
hp : p ≠ 0
⊢ (v : (a : B) → Γ) ((aeval w : (a : A[X]) → B) p : B) = HPow.hPow (α := Γ) ((v : (a : B) → Γ) w : Γ) p.natDegree
have rw : Eq.{u_1 + 1} (α := Γ) ((v : (a : B) → Γ) ((aeval w : (a : A[X]) → B) p : B) : Γ)
  ((v : (a : B) → Γ) ((aeval w : (a : A[X]) → B) ((monomial p.natDegree : (a : A) → A[X]) p.leadingCoeff : A[X]) : B) :
    Γ)
Tactic: rw [← valuation_aeval_monomial_eq_valuation_pow _ _ (leadingCoeff_ne_zero.mpr hp)]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.IsTrivialOn (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : CommSemiring A
B : Type u_3
inst_2 : Ring B
inst_3 : Algebra A B
v : Valuation B Γ
hv : Valuation.IsTrivialOn A v
w : B
hpos : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : B) → Γ) w : Γ)
p : A[X]
hp : p ≠ 0
⊢ Eq.{u_1 + 1} (α := Γ) ((v : (a : B) → Γ) ((aeval w : (a : A[X]) → B) p : B) : Γ)
    ((v : (a : B) → Γ)
        ((aeval w : (a : A[X]) → B) ((monomial p.natDegree : (a : A) → A[X]) p.leadingCoeff : A[X]) : B) :
      Γ)
have nth_rw : Eq.{u_1 + 1} (α := Γ)
  ((v : (a : B) → Γ)
      (∑ x ∈ Finset.range (p.natDegree + 1),
        (aeval w : (a : A[X]) → B) ((monomial x : (a : A) → A[X]) (p.coeff x) : A[X])) :
    Γ)
  ((v : (a : B) → Γ) ((aeval w : (a : A[X]) → B) ((monomial p.natDegree : (a : A) → A[X]) p.leadingCoeff : A[X]) : B) :
    Γ)
Tactic: nth_rw 1 [as_sum_range p, map_sum]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.IsTrivialOn (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : CommSemiring A
B : Type u_3
inst_2 : Ring B
inst_3 : Algebra A B
v : Valuation B Γ
hv : Valuation.IsTrivialOn A v
w : B
hpos : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : B) → Γ) w : Γ)
p : A[X]
hp : p ≠ 0
⊢ Eq.{u_1 + 1} (α := Γ)
    ((v : (a : B) → Γ)
        (∑ x ∈ Finset.range (p.natDegree + 1),
          (aeval w : (a : A[X]) → B) ((monomial x : (a : A) → A[X]) (p.coeff x) : A[X])) :
      Γ)
    ((v : (a : B) → Γ)
        ((aeval w : (a : A[X]) → B) ((monomial p.natDegree : (a : A) → A[X]) p.leadingCoeff : A[X]) : B) :
      Γ)
have apply : ∀ i ∈ Finset.range (p.natDegree + 1) \ {p.natDegree},
  LT.lt.{u_1} (α := Γ)
    ((v : (a : B) → Γ) ((aeval w : (a : A[X]) → B) ((monomial i : (a : A) → A[X]) (p.coeff i) : A[X]) : B) : Γ)
    ((v : (a : B) → Γ)
        ((aeval w : (a : A[X]) → B) ((monomial p.natDegree : (a : A) → A[X]) (p.coeff p.natDegree) : A[X]) : B) :
      Γ)
Tactic: apply Valuation.map_sum_eq_of_lt _ (by simp)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.IsTrivialOn (hypothesis)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : CommSemiring A
B : Type u_3
inst_2 : Ring B
inst_3 : Algebra A B
v : Valuation B Γ
hv : Valuation.IsTrivialOn A v
w : B
hpos : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : B) → Γ) w : Γ)
p : A[X]
hp : p ≠ 0
i : ℕ
hi : i ∈ Finset.range (p.natDegree + 1) \ {p.natDegree}
⊢ LT.lt.{u_1} (α := Γ)
    ((v : (a : B) → Γ) ((aeval w : (a : A[X]) → B) ((monomial i : (a : A) → A[X]) (p.coeff i) : A[X]) : B) : Γ)
    ((v : (a : B) → Γ)
        ((aeval w : (a : A[X]) → B) ((monomial p.natDegree : (a : A) → A[X]) (p.coeff p.natDegree) : A[X]) : B) :
      Γ)
have hi₁ : i < p.natDegree
Tactic: simp only [Finset.mem_sdiff, Finset.mem_range, Nat.lt_add_one_iff, Finset.mem_singleton,
    ← lt_iff_le_and_ne] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.IsTrivialOn (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : CommSemiring A
B : Type u_3
inst_2 : Ring B
inst_3 : Algebra A B
v : Valuation B Γ
hv : Valuation.IsTrivialOn A v
w : B
hpos : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : B) → Γ) w : Γ)
p : A[X]
hp : p ≠ 0
i : ℕ
hi : i < p.natDegree
⊢ LT.lt.{u_1} (α := Γ)
    ((v : (a : B) → Γ) ((aeval w : (a : A[X]) → B) ((monomial i : (a : A) → A[X]) (p.coeff i) : A[X]) : B) : Γ)
    ((v : (a : B) → Γ)
        ((aeval w : (a : A[X]) → B) ((monomial p.natDegree : (a : A) → A[X]) (p.coeff p.natDegree) : A[X]) : B) :
      Γ)
have simp : HMul.hMul (α := Γ) ((v : (a : B) → Γ) ((algebraMap A B : (a : A) → B) (p.coeff i) : B) : Γ)
    (HPow.hPow (α := Γ) ((v : (a : B) → Γ) w : Γ) i) <
  HMul.hMul (α := Γ) ((v : (a : B) → Γ) ((algebraMap A B : (a : A) → B) p.leadingCoeff : B) : Γ)
    (HPow.hPow (α := Γ) ((v : (a : B) → Γ) w : Γ) p.natDegree)
Tactic: simp only [← C_mul_X_pow_eq_monomial, map_mul, aeval_C, map_pow, aeval_X, coeff_natDegree]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.IsTrivialOn (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : CommSemiring A
B : Type u_3
inst_2 : Ring B
inst_3 : Algebra A B
v : Valuation B Γ
hv : Valuation.IsTrivialOn A v
w : B
hpos : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : B) → Γ) w : Γ)
p : A[X]
hp : p ≠ 0
i : ℕ
hi : i < p.natDegree
⊢ HMul.hMul (α := Γ) ((v : (a : B) → Γ) ((algebraMap A B : (a : A) → B) (p.coeff i) : B) : Γ)
      (HPow.hPow (α := Γ) ((v : (a : B) → Γ) w : Γ) i) <
    HMul.hMul (α := Γ) ((v : (a : B) → Γ) ((algebraMap A B : (a : A) → B) p.leadingCoeff : B) : Γ)
      (HPow.hPow (α := Γ) ((v : (a : B) → Γ) w : Γ) p.natDegree)
have pos : ∀ (h0 : p.coeff i = 0),
  HMul.hMul (α := Γ) ((v : (a : B) → Γ) ((algebraMap A B : (a : A) → B) (p.coeff i) : B) : Γ)
      (HPow.hPow (α := Γ) ((v : (a : B) → Γ) w : Γ) i) <
    HMul.hMul (α := Γ) ((v : (a : B) → Γ) ((algebraMap A B : (a : A) → B) p.leadingCoeff : B) : Γ)
      (HPow.hPow (α := Γ) ((v : (a : B) → Γ) w : Γ) p.natDegree)
Tactic: by_cases h0 : (p.coeff i) = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.IsTrivialOn (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : CommSemiring A
B : Type u_3
inst_2 : Ring B
inst_3 : Algebra A B
v : Valuation B Γ
hv : Valuation.IsTrivialOn A v
w : B
hpos : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : B) → Γ) w : Γ)
p : A[X]
hp : p ≠ 0
i : ℕ
hi : i < p.natDegree
pos :
  ∀ (h0 : p.coeff i = 0),
    HMul.hMul (α := Γ) ((v : (a : B) → Γ) ((algebraMap A B : (a : A) → B) (p.coeff i) : B) : Γ)
        (HPow.hPow (α := Γ) ((v : (a : B) → Γ) w : Γ) i) <
      HMul.hMul (α := Γ) ((v : (a : B) → Γ) ((algebraMap A B : (a : A) → B) p.leadingCoeff : B) : Γ)
        (HPow.hPow (α := Γ) ((v : (a : B) → Γ) w : Γ) p.natDegree)
⊢ HMul.hMul (α := Γ) ((v : (a : B) → Γ) ((algebraMap A B : (a : A) → B) (p.coeff i) : B) : Γ)
      (HPow.hPow (α := Γ) ((v : (a : B) → Γ) w : Γ) i) <
    HMul.hMul (α := Γ) ((v : (a : B) → Γ) ((algebraMap A B : (a : A) → B) p.leadingCoeff : B) : Γ)
      (HPow.hPow (α := Γ) ((v : (a : B) → Γ) w : Γ) p.natDegree)
have neg : ∀ (h0 : ¬p.coeff i = 0),
  HMul.hMul (α := Γ) ((v : (a : B) → Γ) ((algebraMap A B : (a : A) → B) (p.coeff i) : B) : Γ)
      (HPow.hPow (α := Γ) ((v : (a : B) → Γ) w : Γ) i) <
    HMul.hMul (α := Γ) ((v : (a : B) → Γ) ((algebraMap A B : (a : A) → B) p.leadingCoeff : B) : Γ)
      (HPow.hPow (α := Γ) ((v : (a : B) → Γ) w : Γ) p.natDegree)
Tactic: by_cases h0 : (p.coeff i) = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.IsTrivialOn (goal)
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 : Γ)
⊢ Transcendental A y
have 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
Tactic: wlog! hlt : 1 < v y generalizing y
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.IsTrivialOn (goal)
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
⊢ Transcendental A y
have 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
Tactic: wlog! hlt : 1 < v y generalizing y
Cleared hypotheses: y, h0, hy
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.IsTrivialOn (goal)
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 : Γ)
⊢ Transcendental A y
have inr : ¬IsAlgebraic A y⁻¹
Tactic: rw [Transcendental, ← IsAlgebraic.inv_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.IsTrivialOn (goal)
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 : Γ)
⊢ ¬IsAlgebraic A y⁻¹
have inr : LT.lt.{u_1} (α := Γ) (1 : Γ) ((v : (a : K) → Γ) y⁻¹ : Γ)
Tactic: apply this _ (by simpa) (by simpa)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.IsTrivialOn (goal)
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} (α := Γ) (1 : Γ) ((v : (a : K) → Γ) y⁻¹ : Γ)
have inr : LT.lt.{u_1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
Tactic: rw [← val_lt_one_iff _ h0]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.IsTrivialOn (hypothesis)
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 : Γ)
⊢ Transcendental A y
have h0₁ : ¬y = 0
Tactic: simp_all only [ne_eq, Transcendental]
Cleared hypotheses: h0, hy, hlt
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.IsTrivialOn (hypothesis)
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
⊢ Transcendental A y
have hy₁ : ¬Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) y : Γ) (1 : Γ)
Tactic: simp_all only [ne_eq, Transcendental]
Cleared hypotheses: h0, hy, hlt
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.IsTrivialOn (goal)
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
⊢ False
have 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
Tactic: replace ⟨p, hpnt, hp⟩ : IsAlgebraic A y := .algebraMap this
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.IsTrivialOn (goal)
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)
⊢ False
have suffices : HPow.hPow (α := Γ) ((v : (a : K) → Γ) y : Γ) p.natDegree = 0
Tactic: suffices v y ^ p.natDegree = 0 by simp_all
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.IsTrivialOn (goal)
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)
⊢ HPow.hPow (α := Γ) ((v : (a : K) → Γ) y : Γ) p.natDegree = 0
have rw : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((aeval y : (a : A[X]) → K) p : K) : Γ) (0 : Γ)
Tactic: rw [← valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X _ hlt]
-- 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
V : ValuationSubring K
⊢ IsIntegrallyClosed.{u_3} ↥V.toSubring
have rw : IsIntegrallyClosed.{u_3} ↥V.valuation.integer
Tactic: rw [← V.integer_valuation]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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)
⊢ mR = ⊤
have by_contra : ∀ (h_is_not_top : ¬mR = ⊤), False
Tactic: by_contra h_is_not_top
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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 = ⊤
⊢ False
have obtain : ∀ (M : Ideal ↥S) (h_is_max : M.IsMaximal) (h_incl : mR ≤ M), False
Tactic: obtain ⟨M, h_is_max, h_incl⟩ := Ideal.exists_le_maximal _ h_is_not_top
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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ₘ
have refine : LE.le (α := Ideal ↥fSₘ.toSubring)
  (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥fSₘ.toSubring) (Subring.inclusion sorry)
    (maximalIdeal ↥R.toSubring))
  (maximalIdeal ↥fSₘ.toSubring)
Tactic: refine ⟨hS.le.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
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
| maximalIdeal ↥fSₘ.toSubring
have rw : Ideal.map (F := ↥S →+* ↥fSₘ.toSubring) (algebraMap ↥S ↥fSₘ.toSubring) M
Tactic: rw [← IsLocalization.AtPrime.map_eq_maximalIdeal M]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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))
    (maximalIdeal ↥fSₘ.toSubring)
have conv_rhs : LE.le (α := Ideal ↥fSₘ.toSubring)
  (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥fSₘ.toSubring) (Subring.inclusion sorry)
    (maximalIdeal ↥R.toSubring))
  (Ideal.map (F := ↥S →+* ↥fSₘ.toSubring) (algebraMap ↥S ↥fSₘ.toSubring) M)
Tactic: conv_rhs => rw [← IsLocalization.AtPrime.map_eq_maximalIdeal M]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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)
have refine : LE.le (α := Ideal ↥fSₘ.toSubring)
  (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥fSₘ.toSubring) (Subring.inclusion sorry)
    (maximalIdeal ↥R.toSubring))
  (Ideal.map (F := ↥S →+* ↥fSₘ.toSubring) (algebraMap ↥S ↥fSₘ.toSubring) mR)
Tactic: refine .trans ?_ (Ideal.map_mono h_incl)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
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) mR)
have rw : LE.le (α := Ideal ↥fSₘ.toSubring)
  (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥fSₘ.toSubring) (Subring.inclusion sorry)
    (maximalIdeal ↥R.toSubring))
  (Ideal.map (R := ↥R.toSubring) (F := ↥R.toSubring →+* ↥fSₘ.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
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
⊢ False
have h_RleSₘ : 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
-- 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]
⊢ x ∈ R.toSubring
have this : Algebra.IsIntegral.{u_3, u_3} ↥R.toSubring ↥S
Tactic: have : Algebra.IsIntegral R.toSubring S := Algebra.IsIntegral.adjoin (by simpa)
-- 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
⊢ x ∈ R.toSubring
have 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
Tactic: obtain ⟨Q : Ideal S.toSubring, hQ, e⟩ := Ideal.exists_ideal_over_maximal_of_isIntegral
    (S := S) (maximalIdeal R.toSubring) (le_maximalIdeal (by simp))