awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
inst_4 : IsPrincipalIdealRing O
hv : v.Integers O
H : DenselyOrdered.{v} (↑(range.{v, u + 1} (ι := F) (⇑v : (a : F) → Γ₀)) : Type v)
I : Ideal O :=
  {
    carrier :=
      preimage.{w, v} (β := Γ₀)
        (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)) (Iio 1),
    add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
x : O
hx₁ : LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) (1 : Γ₀)
hx :
  Membership.mem.{v, v} (α := Γ₀) (γ := Set Γ₀)
    (upperBounds
      (Iio 1 ∩
        range.{v, w + 1} (ι := O)
          (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F))))
    ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
y : F
hy : LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) ((v : (a : F) → Γ₀) y : Γ₀)
hy₁ : LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) y : Γ₀) (1 : Γ₀)
⊢ False
have obtain : ∀ (z : O)
  (hy :
    LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) z : F) : Γ₀))
  (hy₁ : LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) z : F) : Γ₀) (1 : Γ₀)), False
Tactic: obtain ⟨z, rfl⟩ := hv.exists_of_le_one hy₁.le
Cleared hypotheses: y, hy, hy₁
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
x : ↥v.integer
⊢ ¬IsUnit x ↔ LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) (↑x : F) : Γ₀) (1 : Γ₀)
have rw : LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap (↥v.integer) F : (a : ↥v.integer) → F) x : F) : Γ₀) (1 : Γ₀) ∧
    LE.le.{v} (α := Γ₀) (1 : Γ₀) ((v : (a : F) → Γ₀) ((algebraMap (↥v.integer) F : (a : ↥v.integer) → F) x : F) : Γ₀) ↔
  LE.le.{v} (α := Γ₀) (1 : Γ₀) ((v : (a : F) → Γ₀) (↑x : F) : Γ₀)
Tactic: rw [← not_le, not_iff_not, isUnit_iff_valuation_eq_one (F := F) (Γ₀ := Γ₀),
    le_antisymm_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
x : ↥v.integer
rw :
  LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap (↥v.integer) F : (a : ↥v.integer) → F) x : F) : Γ₀) (1 : Γ₀) ∧
      LE.le.{v} (α := Γ₀) (1 : Γ₀)
        ((v : (a : F) → Γ₀) ((algebraMap (↥v.integer) F : (a : ↥v.integer) → F) x : F) : Γ₀) ↔
    LE.le.{v} (α := Γ₀) (1 : Γ₀) ((v : (a : F) → Γ₀) (↑x : F) : Γ₀)
⊢ ¬IsUnit x ↔ LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) (↑x : F) : Γ₀) (1 : Γ₀)
have hv : v.Integers ↥v.integer
Tactic: rw [← not_le, not_iff_not, isUnit_iff_valuation_eq_one (F := F) (Γ₀ := Γ₀),
    le_antisymm_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
⊢ v.leSubmodule 0 = ⊥
have h : ∀ (x : K), x ∈ v.leSubmodule 0 ↔ Membership.mem (γ := Submodule (↥v.integer) K) ⊥ x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
S : Submodule (↥v.integer) K
x : K
hx : x ∈ S
⊢ v.leSubmodule ((v : (a : K) → Γ₀) x) ≤ S
have inl : ∀ (hx : 0 ∈ S), v.leSubmodule ((v : (a : K) → Γ₀) 0) ≤ S
Tactic: rcases eq_or_ne x 0 with rfl | hx0
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
S : Submodule (↥v.integer) K
x : K
hx : x ∈ S
inl : ∀ (hx : 0 ∈ S), v.leSubmodule ((v : (a : K) → Γ₀) 0) ≤ S
⊢ v.leSubmodule ((v : (a : K) → Γ₀) x) ≤ S
have inr : ∀ (hx0 : x ≠ 0), v.leSubmodule ((v : (a : K) → Γ₀) x) ≤ S
Tactic: rcases eq_or_ne x 0 with rfl | hx0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (hypothesis)
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
S : Submodule (↥v.integer) K
x : K
hx : x ∈ S
hx0 : x ≠ 0
y : K
hy : y ∈ v.leSubmodule ((v : (a : K) → Γ₀) x)
⊢ y ∈ S
have this : LE.le.{v} (α := Γ₀) ((v : (a : K) → Γ₀) (y / x) : Γ₀) (1 : Γ₀)
Tactic: have : v ((y : K) / x) ≤ 1 := by simp [div_le_one_of_le₀ hy]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : Γ₀ˣ
r x : ↥v.integer
h :
  Membership.mem (γ := Set ↥v.integer)
    (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup
          (AddSubgroup.toAddSubmonoid ((v.ltAddSubgroup γ).addSubgroupOf v.integer.toAddSubgroup))) :
      Set ↥v.integer.toAddSubgroup)
    x
⊢ Membership.mem (γ := Set ↥v.integer)
    (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup
          (AddSubgroup.toAddSubmonoid ((v.ltAddSubgroup γ).addSubgroupOf v.integer.toAddSubgroup))) :
      Set ↥v.integer.toAddSubgroup)
    (r • x)
have change : (v : (a : R) → Γ₀) ((↑r : R) * (↑x : R)) < (↑γ : Γ₀)
Tactic: change v ((r : R) * x) < γ
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
⊢ v.leIdeal 0 = ⊥
have h : ∀ (x : ↥v.integer), x ∈ v.leIdeal 0 ↔ Membership.mem (γ := Ideal ↥v.integer) ⊥ x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
γ : Γ₀
⊢ Submodule.map (Algebra.linearMap (↥v.integer) K) (v.leIdeal γ) = v.leSubmodule (min 1 γ)
have h : ∀ (x : K),
  Membership.mem (γ := Submodule (↥v.integer) K) (Submodule.map (Algebra.linearMap (↥v.integer) K) (v.leIdeal γ)) x ↔
    x ∈ v.leSubmodule (min 1 γ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
⊢ Membership.mem (γ := Submodule (↥v.integer) K) (Submodule.map (Algebra.linearMap (↥v.integer) K) (v.leIdeal γ)) x ↔
    x ∈ v.leSubmodule (min 1 γ)
have h : (∃ (y : ↥v.integer), (v : (a : K) → Γ₀) (↑y : K) ≤ γ ∧ (algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y = x) ↔
  (v : (a : K) → Γ₀) x ≤ min 1 γ
Tactic: simp only [Submodule.mem_map, mem_leIdeal_iff, Algebra.linearMap_apply, mem_leSubmodule_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
⊢ (∃ (y : ↥v.integer), (v : (a : K) → Γ₀) (↑y : K) ≤ γ ∧ (algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y = x) ↔
    (v : (a : K) → Γ₀) x ≤ min 1 γ
have h : (∃ (y : ↥v.integer), (v : (a : K) → Γ₀) (↑y : K) ≤ γ ∧ (algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y = x) →
  (v : (a : K) → Γ₀) x ≤ min 1 γ
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
h :
  (∃ (y : ↥v.integer), (v : (a : K) → Γ₀) (↑y : K) ≤ γ ∧ (algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y = x) →
    (v : (a : K) → Γ₀) x ≤ min 1 γ
⊢ (∃ (y : ↥v.integer), (v : (a : K) → Γ₀) (↑y : K) ≤ γ ∧ (algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y = x) ↔
    (v : (a : K) → Γ₀) x ≤ min 1 γ
have h₁ : (v : (a : K) → Γ₀) x ≤ min 1 γ →
  ∃ (y : ↥v.integer), (v : (a : K) → Γ₀) (↑y : K) ≤ γ ∧ (algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
γ : Γ₀
y : ↥v.integer
hy : (v : (a : K) → Γ₀) (↑y : K) ≤ γ
⊢ (v : (a : K) → Γ₀) ((algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y : K) ≤ min 1 γ
have h : ∀ (h : min 1 γ = 1), 1 ≤ γ → (v : (a : K) → Γ₀) ((algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y : K) ≤ min 1 γ
Tactic: rcases min_cases 1 γ with ⟨h, _⟩ | ⟨h, _⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
γ : Γ₀
y : ↥v.integer
hy : (v : (a : K) → Γ₀) (↑y : K) ≤ γ
h : ∀ (h : min 1 γ = 1), 1 ≤ γ → (v : (a : K) → Γ₀) ((algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y : K) ≤ min 1 γ
⊢ (v : (a : K) → Γ₀) ((algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y : K) ≤ min 1 γ
have h₁ : ∀ (h : min 1 γ = γ), γ < 1 → (v : (a : K) → Γ₀) ((algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y : K) ≤ min 1 γ
Tactic: rcases min_cases 1 γ with ⟨h, _⟩ | ⟨h, _⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
γ : Γ₀
y : ↥v.integer
hy : (v : (a : K) → Γ₀) (↑y : K) ≤ γ
h : min 1 γ = 1
right : 1 ≤ γ
⊢ (v : (a : K) → Γ₀) ((algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y : K) ≤ min 1 γ
have h₁ : LE.le.{v} (α := Γ₀) ((v : (a : K) → Γ₀) ((algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y : K) : Γ₀) (1 : Γ₀)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
γ : Γ₀
y : ↥v.integer
hy : (v : (a : K) → Γ₀) (↑y : K) ≤ γ
h : min 1 γ = γ
right : γ < 1
⊢ (v : (a : K) → Γ₀) ((algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y : K) ≤ min 1 γ
have h₁ : (v : (a : K) → Γ₀) ((algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y : K) ≤ γ
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
hx : (v : (a : K) → Γ₀) x ≤ min 1 γ
⊢ ∃ (y : ↥v.integer), (v : (a : K) → Γ₀) (↑y : K) ≤ γ ∧ (algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y = x
have h : ∀ (h : min 1 γ = 1) (h' : 1 ≤ γ),
  ∃ (y : ↥v.integer), (v : (a : K) → Γ₀) (↑y : K) ≤ γ ∧ (algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y = x
Tactic: rcases min_cases 1 γ with ⟨h, h'⟩ | ⟨h, h'⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
hx : (v : (a : K) → Γ₀) x ≤ min 1 γ
h :
  ∀ (h : min 1 γ = 1) (h' : 1 ≤ γ),
    ∃ (y : ↥v.integer), (v : (a : K) → Γ₀) (↑y : K) ≤ γ ∧ (algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y = x
⊢ ∃ (y : ↥v.integer), (v : (a : K) → Γ₀) (↑y : K) ≤ γ ∧ (algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y = x
have h₁ : ∀ (h : min 1 γ = γ) (h' : γ < 1),
  ∃ (y : ↥v.integer), (v : (a : K) → Γ₀) (↑y : K) ≤ γ ∧ (algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y = x
Tactic: rcases min_cases 1 γ with ⟨h, h'⟩ | ⟨h, h'⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (hypothesis)
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
hx : (v : (a : K) → Γ₀) x ≤ min 1 γ
h : min 1 γ = 1
h' : 1 ≤ γ
⊢ ∃ (y : ↥v.integer), (v : (a : K) → Γ₀) (↑y : K) ≤ γ ∧ (algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y = x
have hx₁ : LE.le.{v} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: rw [h] at hx
Cleared hypotheses: hx, h, h'
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (hypothesis)
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
hx : (v : (a : K) → Γ₀) x ≤ min 1 γ
h : min 1 γ = γ
h' : γ < 1
⊢ ∃ (y : ↥v.integer), (v : (a : K) → Γ₀) (↑y : K) ≤ γ ∧ (algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y = x
have hx₁ : (v : (a : K) → Γ₀) x ≤ γ
Tactic: rw [h] at hx
Cleared hypotheses: hx, h, h'
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
I : Ideal ↥v.integer
x : ↥v.integer
hx : x ∈ I
⊢ v.leIdeal ((v : (a : K) → Γ₀) (↑x : K)) ≤ I
have inl : ∀ (hx : 0 ∈ I), v.leIdeal ((v : (a : K) → Γ₀) (↑0 : K)) ≤ I
Tactic: rcases eq_or_ne x 0 with rfl | hx0
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
I : Ideal ↥v.integer
x : ↥v.integer
hx : x ∈ I
inl : ∀ (hx : 0 ∈ I), v.leIdeal ((v : (a : K) → Γ₀) (↑0 : K)) ≤ I
⊢ v.leIdeal ((v : (a : K) → Γ₀) (↑x : K)) ≤ I
have inr : ∀ (hx0 : x ≠ 0), v.leIdeal ((v : (a : K) → Γ₀) (↑x : K)) ≤ I
Tactic: rcases eq_or_ne x 0 with rfl | hx0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (hypothesis)
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
I : Ideal ↥v.integer
x : ↥v.integer
hx : x ∈ I
hx0 : x ≠ 0
y : ↥v.integer
hy : y ∈ v.leIdeal ((v : (a : K) → Γ₀) (↑x : K))
⊢ y ∈ I
have this : LE.le.{v} (α := Γ₀) ((v : (a : K) → Γ₀) ((↑y : K) / (↑x : K)) : Γ₀) (1 : Γ₀)
Tactic: have : v ((y : K) / x) ≤ 1 := by simpa using div_le_one_of_le₀ hy zero_le'
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
I : Ideal ↥v.integer
x : ↥v.integer
hx : x ∈ I
hx0 : x ≠ 0
y : ↥v.integer
hy : y ∈ v.leIdeal ((v : (a : K) → Γ₀) (↑x : K))
this : LE.le.{v} (α := Γ₀) ((v : (a : K) → Γ₀) ((↑y : K) / (↑x : K)) : Γ₀) (1 : Γ₀)
⊢ y ∈ I
have h : y = HSMul.hSMul (α := ↥v.integer) (Subtype.mk (p := fun (x : K) ↦ x ∈ v.integer) ((↑y : K) / (↑x : K)) this) x
Tactic: convert! I.smul_mem ⟨_, this⟩ hx using 1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integral (hypothesis)
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
⊢ IsIntegral O x ↔ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integral (hypothesis)
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
⊢ IsIntegral O x ↔ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
have this : Nontrivial O
Tactic: have : Nontrivial O := hv.nontrivial_iff.mpr inferInstance
-- 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 : Nontrivial R
this : Nontrivial O
⊢ IsIntegral O x ↔ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
have mp : IsIntegral O x → LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: constructor
-- 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 : Nontrivial R
this : Nontrivial O
mp : IsIntegral O x → LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ IsIntegral O x ↔ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
have mpr : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀) → IsIntegral O x
Tactic: constructor
-- 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 : Nontrivial R
this : Nontrivial O
f : O[X]
hm : f.Monic
hf : eval₂ (algebraMap O R) x f = 0
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
have pos : ∀ (hn : f.natDegree = 0), LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: by_cases hn : f.natDegree = 0
-- 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 : Nontrivial R
this : Nontrivial O
f : O[X]
hm : f.Monic
hf : eval₂ (algebraMap O R) x f = 0
pos : ∀ (hn : f.natDegree = 0), LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
have neg : ∀ (hn : ¬f.natDegree = 0), LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: by_cases hn : f.natDegree = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integral (hypothesis)
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
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
have hn₁ : ∃ (x : O), (C : (a : O) → O[X]) x = f
Tactic: rw [Polynomial.natDegree_eq_zero] at hn
Cleared hypotheses: hn
-- 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 : 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
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
have 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 : Γ₀)
Tactic: obtain ⟨c, rfl⟩ := hn
Cleared hypotheses: f, hm, hf, hn
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integral (hypothesis)
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
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
have hf₁ : ∑ 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
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integral (hypothesis)
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
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
have 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) : Γ₀)
Tactic: apply_fun v at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integral (hypothesis)
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) : Γ₀)
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
have 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
Tactic: simp only [map_neg, map_pow] at hf
Cleared hypotheses: hf
-- 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 : 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
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
have 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
Tactic: contrapose! hf
Cleared hypotheses: hf
-- 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 : 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
have neg : HPow.hPow (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) f.natDegree ≠ 0
Tactic: refine ne_of_lt (v.map_sum_lt ?_ ?_)
-- 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 : 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
⊢ (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
have 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
Tactic: refine ne_of_lt (v.map_sum_lt ?_ ?_)
-- 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 : 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 ∈ 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
have 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
Tactic: simp only [Finset.mem_range, map_mul, map_pow]