awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.Integral
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 : Nontrivial R
this : Nontrivial O
f : O[X]
hm : f.Monic
hf : eval₂ (algebraMap O R) x f = 0
hn : ∃ (x : O), (C : (a : O) → O[X]) x = f
pos :
  ∀ (c : O) (hm : Monic.{w} (R := O) ((C : (a : O) → O[X]) c))
    (hf : eval₂ (algebraMap O R) x ((C : (a : O) → O[X]) c) = 0),
    LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
obtain ⟨c, rfl⟩ := hn

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.Integral
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 : Nontrivial R
this : Nontrivial O
c : O
hm : Monic.{w} (R := O) ((C : (a : O) → O[X]) c)
hf : eval₂ (algebraMap O R) x ((C : (a : O) → O[X]) c) = 0
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
simp [map_eq_zero_iff _ hv.hom_inj, hm.ne_zero_of_C] at hf

Premises used: Valuation.Integers.hom_inj, map_eq_zero_iff, Polynomial.Monic.ne_zero_of_C
-- Module: Mathlib.RingTheory.Valuation.Integral
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 : Nontrivial R
this : Nontrivial O
f : O[X]
hm : f.Monic
hf : eval₂ (algebraMap O R) x f = 0
hn : ¬f.natDegree = 0
⊢ ∑ i ∈ Finset.range f.natDegree, HMul.hMul (α := R) ((algebraMap O R : (a : O) → R) (f.coeff i) : R) (x ^ i) =
    -x ^ f.natDegree

Tactic:
simp only [Polynomial.eval₂_eq_sum_range, Finset.sum_range_succ, hm.coeff_natDegree, map_one,
      one_mul, add_eq_zero_iff_eq_neg] at hf

Premises used: add_eq_zero_iff_eq_neg, map_one, Polynomial.Monic.coeff_natDegree, Polynomial.eval₂_eq_sum_range, Finset.sum_range_succ, one_mul
-- Module: Mathlib.RingTheory.Valuation.Integral
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 : Nontrivial R
this : Nontrivial O
f : O[X]
hm : f.Monic
hn : ¬f.natDegree = 0
hf :
  ∑ i ∈ Finset.range f.natDegree, HMul.hMul (α := R) ((algebraMap O R : (a : O) → R) (f.coeff i) : R) (x ^ i) =
    -x ^ f.natDegree
⊢ Eq.{v + 1} (α := Γ₀)
    ((v : (a : R) → Γ₀)
        (∑ i ∈ Finset.range f.natDegree, HMul.hMul (α := R) ((algebraMap O R : (a : O) → R) (f.coeff i) : R) (x ^ i)) :
      Γ₀)
    ((v : (a : R) → Γ₀) (-x ^ f.natDegree) : Γ₀)

Tactic:
apply_fun v at hf
-- Module: Mathlib.RingTheory.Valuation.Integral
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 : Nontrivial R
this : Nontrivial O
f : O[X]
hm : f.Monic
hn : ¬f.natDegree = 0
hf :
  Eq.{v + 1} (α := Γ₀)
    ((v : (a : R) → Γ₀)
        (∑ i ∈ Finset.range f.natDegree, HMul.hMul (α := R) ((algebraMap O R : (a : O) → R) (f.coeff i) : R) (x ^ i)) :
      Γ₀)
    ((v : (a : R) → Γ₀) (-x ^ f.natDegree) : Γ₀)
⊢ (v : (a : R) → Γ₀)
      (∑ i ∈ Finset.range f.natDegree, HMul.hMul (α := R) ((algebraMap O R : (a : O) → R) (f.coeff i) : R) (x ^ i)) =
    HPow.hPow (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) f.natDegree

Tactic:
simp only [map_neg, map_pow] at hf

Premises used: map_pow, Valuation.map_neg
-- Module: Mathlib.RingTheory.Valuation.Integral
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 : Nontrivial R
this : Nontrivial O
f : O[X]
hm : f.Monic
hn : ¬f.natDegree = 0
hf :
  (v : (a : R) → Γ₀)
      (∑ i ∈ Finset.range f.natDegree, HMul.hMul (α := R) ((algebraMap O R : (a : O) → R) (f.coeff i) : R) (x ^ i)) =
    HPow.hPow (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) f.natDegree
neg :
  ∀ (hf : LT.lt.{v} (α := Γ₀) (1 : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)),
    (v : (a : R) → Γ₀)
        (∑ i ∈ Finset.range f.natDegree, HMul.hMul (α := R) ((algebraMap O R : (a : O) → R) (f.coeff i) : R) (x ^ i)) ≠
      HPow.hPow (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) f.natDegree
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
contrapose! hf
-- Module: Mathlib.RingTheory.Valuation.Integral
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 : Nontrivial R
this : Nontrivial O
f : O[X]
hm : f.Monic
hn : ¬f.natDegree = 0
hf : LT.lt.{v} (α := Γ₀) (1 : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ (v : (a : R) → Γ₀)
      (∑ i ∈ Finset.range f.natDegree, HMul.hMul (α := R) ((algebraMap O R : (a : O) → R) (f.coeff i) : R) (x ^ i)) ≠
    HPow.hPow (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) f.natDegree

Tactic:
ne_of_lt (v.map_sum_lt ?_ ?_)

Premises used: Valuation.map_sum_lt, ne_of_lt
-- Module: Mathlib.RingTheory.Valuation.Integral
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 : Nontrivial R
this : Nontrivial O
f : O[X]
hm : f.Monic
hn : ¬f.natDegree = 0
hf : LT.lt.{v} (α := Γ₀) (1 : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
neg : HPow.hPow (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) f.natDegree ≠ 0
neg₁ :
  ∀ i ∈ Finset.range f.natDegree,
    (v : (a : R) → Γ₀) (HMul.hMul (α := R) ((algebraMap O R : (a : O) → R) (f.coeff i) : R) (x ^ i)) <
      HPow.hPow (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) f.natDegree
⊢ (v : (a : R) → Γ₀)
      (∑ i ∈ Finset.range f.natDegree, HMul.hMul (α := R) ((algebraMap O R : (a : O) → R) (f.coeff i) : R) (x ^ i)) ≠
    HPow.hPow (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) f.natDegree

Tactic:
refine ne_of_lt (v.map_sum_lt ?_ ?_)

Premises used: Valuation.map_sum_lt, ne_of_lt
-- Module: Mathlib.RingTheory.Valuation.Integral
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 : Nontrivial R
this : Nontrivial O
f : O[X]
hm : f.Monic
hn : ¬f.natDegree = 0
hf : LT.lt.{v} (α := Γ₀) (1 : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ HPow.hPow (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) f.natDegree ≠ 0

Tactic:
simp [hn, (hf.trans' (zero_lt_one)).ne']

Premises used: LT.lt.trans', LT.lt.ne', zero_lt_one
-- Module: Mathlib.RingTheory.Valuation.Integral
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 : Nontrivial R
this : Nontrivial O
f : O[X]
hm : f.Monic
hn : ¬f.natDegree = 0
hf : LT.lt.{v} (α := Γ₀) (1 : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
neg :
  ∀ i < f.natDegree,
    HMul.hMul (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) (f.coeff i) : R) : Γ₀)
        (HPow.hPow (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) i) <
      HPow.hPow (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) f.natDegree
⊢ ∀ i ∈ Finset.range f.natDegree,
    (v : (a : R) → Γ₀) (HMul.hMul (α := R) ((algebraMap O R : (a : O) → R) (f.coeff i) : R) (x ^ i)) <
      HPow.hPow (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) f.natDegree

Tactic:
simp only [Finset.mem_range, map_mul, map_pow]

Premises used: Finset.mem_range, map_pow, map_mul
-- Module: Mathlib.RingTheory.Valuation.Integral
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 : Nontrivial R
this : Nontrivial O
f : O[X]
hm : f.Monic
hn : ¬f.natDegree = 0
hf : LT.lt.{v} (α := Γ₀) (1 : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
i : ℕ
hi : i < f.natDegree
⊢ HMul.hMul (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) (f.coeff i) : R) : Γ₀)
      (HPow.hPow (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) i) <
    HPow.hPow (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) f.natDegree

Tactic:
mul_lt_of_le_one_of_lt (hv.map_le_one _) <| pow_lt_pow_right₀ hf hi

Premises used: Valuation.Integers.map_le_one, mul_lt_of_le_one_of_lt, pow_lt_pow_right₀
-- Module: Mathlib.RingTheory.Valuation.Integral
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 : Nontrivial R
this : Nontrivial O
f : O[X]
hm : f.Monic
hn : ¬f.natDegree = 0
hf : LT.lt.{v} (α := Γ₀) (1 : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
i : ℕ
hi : i < f.natDegree
⊢ HMul.hMul (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) (f.coeff i) : R) : Γ₀)
      (HPow.hPow (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) i) <
    HPow.hPow (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) f.natDegree

Tactic:
exact mul_lt_of_le_one_of_lt (hv.map_le_one _) <| pow_lt_pow_right₀ hf hi

Premises used: Valuation.Integers.map_le_one, mul_lt_of_le_one_of_lt, pow_lt_pow_right₀
-- Module: Mathlib.RingTheory.Valuation.Integral
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 : Γ₀)
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)
⊢ IsIntegral O x

Tactic:
obtain ⟨y, rfl⟩ := hv.exists_of_le_one h

Premises used: Valuation.Integers.exists_of_le_one, rfl
-- Module: Mathlib.RingTheory.Valuation.Integral
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
n : ℕ
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
n₁ : ℕ
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
n₂ : ℕ
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
n₃ : ℕ
⊢ (HSub.hSub (α := O[X]) (β := O[X]) X ((C : (a : O) → O[X]) y : O[X])).Monic

Tactic:
monicity
-- Module: Mathlib.RingTheory.Valuation.Integral
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 : Γ₀)
⊢ eval₂ (algebraMap O R) ((algebraMap O R : (a : O) → R) y)
      (HSub.hSub (α := O[X]) (β := O[X]) X ((C : (a : O) → O[X]) y : O[X])) =
    0

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Integral
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 : Γ₀)
⊢ IsIntegral.{w, u} O (A := R) ((algebraMap O R : (a : O) → R) y : R)

Tactic:
exact ⟨Polynomial.X - .C y, by monicity, by simp⟩
-- Module: Mathlib.RingTheory.Valuation.Integral
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
hx : IsIntegral O x
⊢ x ∈ v.integer

Tactic:
hv.isIntegral_iff_v_le_one.mp hx

Premises used: Set.Mem, setOf, Valuation.Integers.isIntegral_iff_v_le_one, Iff.mp
-- Module: Mathlib.RingTheory.Valuation.Integral
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
⊢ Eq (α := Subalgebra O R) (integralClosure O R) ⊥

Tactic:
bot_unique fun _ hr =>
    let ⟨x, hx⟩ := hv.3 (hv.mem_of_integral hr)
    Algebra.mem_bot.2 ⟨x, hx⟩

Premises used: Iff.mpr, Valuation.Integers.exists_of_le_one, Valuation.Integers.mem_of_integral, Algebra.mem_bot, _private.0.Valuation.Integers.integralClosure.match_1, Membership.mem, Bot.bot, Exists.intro, bot_unique
-- Module: Mathlib.RingTheory.Valuation.Integral
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
⊢ IsFractionRing O K

Tactic:
have : IsFractionRing O K := hv.isFractionRing
-- Module: Mathlib.RingTheory.Valuation.Integral
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
this : IsFractionRing O K
⊢ IsIntegrallyClosed O

Tactic:
(IsIntegrallyClosed.integralClosure_eq_bot_iff K).mp (Valuation.Integers.integralClosure hv)

Premises used: IsIntegrallyClosed.integralClosure_eq_bot_iff, Iff.mp, Valuation.Integers.integralClosure
-- Module: Mathlib.RingTheory.Valuation.Integral
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
this : IsFractionRing O K
⊢ IsIntegrallyClosed O

Tactic:
exact
    (IsIntegrallyClosed.integralClosure_eq_bot_iff K).mp (Valuation.Integers.integralClosure hv)

Premises used: IsIntegrallyClosed.integralClosure_eq_bot_iff, Iff.mp, Valuation.Integers.integralClosure
-- Module: Mathlib.RingTheory.Valuation.Integral
Goal:
K : Type u
Γ₀ : Type v
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v_1 : Valuation K Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O K
hv : v_1.Integers O
v : Valuation K Γ₀
⊢ IsIntegrallyClosed.{u} ↥v.integer

Tactic:
(Valuation.integer.integers v).isIntegrallyClosed

Premises used: Valuation.Integers.isIntegrallyClosed, Set.Mem, setOf, Valuation.integer.integers
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
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
n : ℕ
a : A
ha : a ≠ 0
⊢ (v : (a : B) → Γ) ((aeval w : (a : A[X]) → B) ((monomial n : (a : A) → A[X]) a : A[X]) : B) =
    HPow.hPow (α := Γ) ((v : (a : B) → Γ) w : Γ) n

Tactic:
simp [← C_mul_X_pow_eq_monomial, map_mul, map_pow, one_mul, hv.eq_one a ha]

Premises used: Valuation.IsTrivialOn.eq_one, Polynomial.C_mul_X_pow_eq_monomial, map_pow, map_mul, one_mul
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
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
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) :
      Γ)
⊢ (v : (a : B) → Γ) ((aeval w : (a : A[X]) → B) p : B) = HPow.hPow (α := Γ) ((v : (a : B) → Γ) w : Γ) p.natDegree

Tactic:
rw [← valuation_aeval_monomial_eq_valuation_pow _ _ (leadingCoeff_ne_zero.mpr hp)]

Premises used: Iff.mpr, Polynomial.leadingCoeff_ne_zero, Polynomial.valuation_aeval_monomial_eq_valuation_pow
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
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
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) :
      Γ)
⊢ 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:
nth_rw 1 [as_sum_range p, map_sum]

Premises used: Polynomial.as_sum_range, map_sum
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
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
⊢ p.natDegree ∈ Finset.range (p.natDegree + 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
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
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) :
        Γ)
⊢ 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:
apply Valuation.map_sum_eq_of_lt _ (by simp)

Premises used: Valuation.map_sum_eq_of_lt
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
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}
⊢ 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

Premises used: lt_iff_le_and_ne, Finset.mem_singleton, Nat.lt_add_one_iff, Finset.mem_range, Finset.mem_sdiff
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
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
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)
⊢ 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:
simp only [← C_mul_X_pow_eq_monomial, map_mul, aeval_C, map_pow, aeval_X, coeff_natDegree]

Premises used: Polynomial.coeff_natDegree, Polynomial.C_mul_X_pow_eq_monomial, map_pow, map_mul, Polynomial.aeval_C, Polynomial.aeval_X
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
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)
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)
⊢ 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

Premises used: Polynomial.coeff
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
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
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:
simp [hv.eq_one p.leadingCoeff (leadingCoeff_ne_zero.mpr hp),
      h0, pow_pos (lt_of_le_of_lt zero_le_one hpos) p.natDegree]

Premises used: Iff.mpr, lt_of_le_of_lt, pow_pos, Valuation.IsTrivialOn.eq_one, Polynomial.leadingCoeff, zero_le_one, Polynomial.leadingCoeff_ne_zero, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Valuation.IsTrivialOn
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
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:
simp [hv.eq_one p.leadingCoeff (leadingCoeff_ne_zero.mpr hp),
      hv.eq_one _ h0, pow_lt_pow_right₀ hpos hi]

Premises used: Iff.mpr, Valuation.IsTrivialOn.eq_one, Polynomial.leadingCoeff, pow_lt_pow_right₀, Polynomial.leadingCoeff_ne_zero