awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ Monotone v.ltSubmodule

Tactic:
ltAddSubgroup_monotone v

Premises used: Set.Mem, Valuation.ltAddSubgroup_monotone, Monotone, Valuation.ltAddSubgroup, Valuation.ltSubmodule
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : Γ₀ˣ
⊢ v.ltSubmodule γ ≤ v.leSubmodule (↑γ : Γ₀)

Tactic:
ltAddSubgroup_le_leAddSubgroup v γ

Premises used: Set.Mem, Valuation.ltAddSubgroup_le_leAddSubgroup
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : Γ₀
x : R
⊢ x ∈ v.leSubmodule γ ↔ (v : (a : R) → Γ₀) x ≤ γ

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : Γ₀ˣ
x : R
⊢ x ∈ v.ltSubmodule γ ↔ (v : (a : R) → Γ₀) x < (↑γ : Γ₀)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
h : ∀ (x : K), x ∈ v.leSubmodule 0 ↔ Membership.mem (γ := Submodule (↥v.integer) K) ⊥ x
⊢ v.leSubmodule 0 = ⊥

Tactic:
ext
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
x : K
⊢ x ∈ v.leSubmodule 0 ↔ Membership.mem (γ := Submodule (↥v.integer) K) ⊥ x

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Integers
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
inr : ∀ (hx0 : x ≠ 0), v.leSubmodule ((v : (a : K) → Γ₀) x) ≤ S
⊢ v.leSubmodule ((v : (a : K) → Γ₀) x) ≤ S

Tactic:
rcases eq_or_ne x 0 with rfl | hx0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
S : Submodule (↥v.integer) K
hx : 0 ∈ S
⊢ v.leSubmodule ((v : (a : K) → Γ₀) 0) ≤ S

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Integers
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)
⊢ LE.le.{v} (α := Γ₀) ((v : (a : K) → Γ₀) (y / x) : Γ₀) (1 : Γ₀)

Tactic:
simp [div_le_one_of_le₀ hy]

Premises used: div_le_one_of_le₀
-- Module: Mathlib.RingTheory.Valuation.Integers
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)
⊢ LE.le.{v} (α := Γ₀) ((v : (a : K) → Γ₀) (y / x) : Γ₀) (1 : Γ₀)

Tactic:
have : v ((y : K) / x) ≤ 1 := by simp [div_le_one_of_le₀ hy]
-- Module: Mathlib.RingTheory.Valuation.Integers
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)
this : LE.le.{v} (α := Γ₀) ((v : (a : K) → Γ₀) (y / x) : Γ₀) (1 : Γ₀)
⊢ y ∈ S

Tactic:
simpa [Subring.smul_def, div_mul_cancel₀ _ hx0] using S.smul_mem ⟨_, this⟩ hx

Premises used: div_mul_cancel₀, Subtype.mk, Subring.smul_def, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Valuation.Integers
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
hxv : Ne.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)
⊢ v.ltSubmodule (Units.mk0 ((v : (a : K) → Γ₀) x) hxv) ≤ S

Tactic:
(leSubmodule_v_le_of_mem v hx).trans' (ltSubmodule_le_leSubmodule _ _)

Premises used: Valuation.leSubmodule_v_le_of_mem, Valuation.ltSubmodule_le_leSubmodule, LE.le.trans'
-- Module: Mathlib.RingTheory.Valuation.Integers
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.leAddSubgroup γ).addSubgroupOf v.integer.toAddSubgroup))) :
      Set ↥v.integer.toAddSubgroup)
    x
⊢ (↑(r • x) : R) ∈ v.leAddSubgroup γ

Tactic:
simpa using mul_le_of_le_one_of_le r.prop h

Premises used: mul_le_of_le_one_of_le, Subtype.prop
-- Module: Mathlib.RingTheory.Valuation.Integers
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
change : (v : (a : R) → Γ₀) ((↑r : R) * (↑x : R)) < (↑γ : Γ₀)
⊢ Membership.mem (γ := Set ↥v.integer)
    (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup
          (AddSubgroup.toAddSubmonoid ((v.ltAddSubgroup γ).addSubgroupOf v.integer.toAddSubgroup))) :
      Set ↥v.integer.toAddSubgroup)
    (r • x)

Tactic:
change v ((r : R) * x) < γ

Premises used: HMul.hMul, Subtype.val, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.Integers
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
⊢ (v : (a : R) → Γ₀) ((↑r : R) * (↑x : R)) < (↑γ : Γ₀)

Tactic:
simpa [Subring.smul_def] using mul_lt_of_le_one_of_lt r.prop h

Premises used: mul_lt_of_le_one_of_lt, Subtype.prop, Subring.smul_def
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ Monotone v.leIdeal

Tactic:
fun _ _ h _ ↦ h.trans'

Premises used: Set.Mem, Monotone, setOf, Set.preimage, LE.le.trans'
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ Monotone v.ltIdeal

Tactic:
fun _ _ h _ ↦ (Units.val_le_val.mpr h).trans_lt'

Premises used: Iff.mpr, Set.Mem, Monotone, setOf, Units.val_le_val, Set.preimage, LE.le.trans_lt'
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : Γ₀ˣ
⊢ v.ltIdeal γ ≤ v.leIdeal (↑γ : Γ₀)

Tactic:
fun _ h ↦ h.le

Premises used: Set.Mem, setOf, LT.lt.le, Set.preimage
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : Γ₀
x : ↥v.integer
⊢ x ∈ v.leIdeal γ ↔ (v : (a : R) → Γ₀) (↑x : R) ≤ γ

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : Γ₀ˣ
x : ↥v.integer
⊢ x ∈ v.ltIdeal γ ↔ (v : (a : R) → Γ₀) (↑x : R) < (↑γ : Γ₀)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
h : ∀ (x : ↥v.integer), x ∈ v.leIdeal 0 ↔ Membership.mem (γ := Ideal ↥v.integer) ⊥ x
⊢ v.leIdeal 0 = ⊥

Tactic:
ext
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
x : ↥v.integer
⊢ x ∈ v.leIdeal 0 ↔ Membership.mem (γ := Ideal ↥v.integer) ⊥ x

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
γ : Γ₀
⊢ Submodule.comap (Algebra.linearMap (↥v.integer) K) (v.leSubmodule γ) = v.leIdeal γ

Tactic:
Submodule.ext fun _ ↦ Iff.rfl

Premises used: Iff.rfl, Submodule.ext
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
γ : Γ₀
h :
  ∀ (x : K),
    Membership.mem (γ := Submodule (↥v.integer) K) (Submodule.map (Algebra.linearMap (↥v.integer) K) (v.leIdeal γ)) x ↔
      x ∈ v.leSubmodule (min 1 γ)
⊢ Submodule.map (Algebra.linearMap (↥v.integer) K) (v.leIdeal γ) = v.leSubmodule (min 1 γ)

Tactic:
ext x
-- Module: Mathlib.RingTheory.Valuation.Integers
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 γ
⊢ Membership.mem (γ := Submodule (↥v.integer) K) (Submodule.map (Algebra.linearMap (↥v.integer) K) (v.leIdeal γ)) x ↔
    x ∈ v.leSubmodule (min 1 γ)

Tactic:
simp only [Submodule.mem_map, mem_leIdeal_iff, Algebra.linearMap_apply, mem_leSubmodule_iff]

Premises used: Valuation.mem_leSubmodule_iff, Submodule.mem_map, Algebra.linearMap_apply, Valuation.mem_leIdeal_iff
-- Module: Mathlib.RingTheory.Valuation.Integers
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 γ
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
⊢ (∃ (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
-- Module: Mathlib.RingTheory.Valuation.Integers
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 γ
h₁ :
  ∀ (h : min 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 γ

Tactic:
rcases min_cases 1 γ with ⟨h, _⟩ | ⟨h, _⟩

Premises used: min_cases, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.Integers
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 ≤ γ
h₁ : LE.le.{v} (α := Γ₀) ((v : (a : K) → Γ₀) ((algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y : K) : Γ₀) (1 : Γ₀)
⊢ (v : (a : K) → Γ₀) ((algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y : K) ≤ min 1 γ

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.Valuation.Integers
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 ≤ γ
⊢ LE.le.{v} (α := Γ₀) ((v : (a : K) → Γ₀) ((algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y : K) : Γ₀) (1 : Γ₀)

Tactic:
y.prop

Premises used: Set.Mem, setOf, Subtype.prop
-- Module: Mathlib.RingTheory.Valuation.Integers
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 ≤ γ
⊢ LE.le.{v} (α := Γ₀) ((v : (a : K) → Γ₀) ((algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y : K) : Γ₀) (1 : Γ₀)

Tactic:
exact y.prop

Premises used: Subtype.prop
-- Module: Mathlib.RingTheory.Valuation.Integers
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
h₁ : (v : (a : K) → Γ₀) ((algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y : K) ≤ γ
⊢ (v : (a : K) → Γ₀) ((algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y : K) ≤ min 1 γ

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.Valuation.Integers
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) ≤ γ

Tactic:
hy
-- Module: Mathlib.RingTheory.Valuation.Integers
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) ≤ γ

Tactic:
exact hy
-- Module: Mathlib.RingTheory.Valuation.Integers
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
h₁ :
  ∀ (h : min 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

Tactic:
rcases min_cases 1 γ with ⟨h, h'⟩ | ⟨h, h'⟩

Premises used: min_cases, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.Integers
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 ≤ γ
⊢ LE.le.{v} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
rw [h] at hx
-- Module: Mathlib.RingTheory.Valuation.Integers
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 ≤ γ
hx₁ : LE.le.{v} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ min 1 γ = 1

Tactic:
rw [h] at hx
-- Module: Mathlib.RingTheory.Valuation.Integers
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 ≤ γ
hx₁ : LE.le.{v} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
h₁ : min 1 γ = 1
⊢ 1 ≤ γ

Tactic:
rw [h] at hx
-- Module: Mathlib.RingTheory.Valuation.Integers
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
⊢ (v : (a : K) → Γ₀) x ≤ γ

Tactic:
rw [h] at hx
-- Module: Mathlib.RingTheory.Valuation.Integers
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
hx₁ : (v : (a : K) → Γ₀) x ≤ γ
⊢ min 1 γ = γ

Tactic:
rw [h] at hx
-- Module: Mathlib.RingTheory.Valuation.Integers
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
hx₁ : (v : (a : K) → Γ₀) x ≤ γ
h₁ : min 1 γ = γ
⊢ γ < 1

Tactic:
rw [h] at hx
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
hx : LE.le.{v} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (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

Tactic:
⟨⟨x, hx⟩, hx.trans h', rfl⟩

Premises used: Subtype.mk, And.intro, Exists.intro, LE.le.trans, rfl
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
hx : LE.le.{v} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (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

Tactic:
exact ⟨⟨x, hx⟩, hx.trans h', rfl⟩
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
hx : (v : (a : K) → Γ₀) x ≤ γ
h : min 1 γ = γ
h' : γ < 1
⊢ ∃ (y : ↥v.integer), (v : (a : K) → Γ₀) (↑y : K) ≤ γ ∧ (algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y = x

Tactic:
⟨⟨x, hx.trans h'.le⟩, hx, rfl⟩

Premises used: LT.lt.le, Subtype.mk, And.intro, Exists.intro, LE.le.trans, rfl
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
hx : (v : (a : K) → Γ₀) x ≤ γ
h : min 1 γ = γ
h' : γ < 1
⊢ ∃ (y : ↥v.integer), (v : (a : K) → Γ₀) (↑y : K) ≤ γ ∧ (algebraMap (↥v.integer) K : (a : ↥v.integer) → K) y = x

Tactic:
exact ⟨⟨x, hx.trans h'.le⟩, hx, rfl⟩
-- Module: Mathlib.RingTheory.Valuation.Integers
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
inr : ∀ (hx0 : x ≠ 0), v.leIdeal ((v : (a : K) → Γ₀) (↑x : K)) ≤ I
⊢ v.leIdeal ((v : (a : K) → Γ₀) (↑x : K)) ≤ I

Tactic:
rcases eq_or_ne x 0 with rfl | hx0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst_1 : Field K
v : Valuation K Γ₀
I : Ideal ↥v.integer
hx : 0 ∈ I
⊢ v.leIdeal ((v : (a : K) → Γ₀) (↑0 : K)) ≤ I

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Integers
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))
⊢ LE.le.{v} (α := Γ₀) ((v : (a : K) → Γ₀) ((↑y : K) / (↑x : K)) : Γ₀) (1 : Γ₀)

Tactic:
simpa using div_le_one_of_le₀ hy zero_le'

Premises used: div_le_one_of_le₀, zero_le'
-- Module: Mathlib.RingTheory.Valuation.Integers
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))
⊢ 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'
-- Module: Mathlib.RingTheory.Valuation.Integers
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 : Γ₀)
⊢ HSMul.hSMul (α := ↥v.integer) (Subtype.mk (p := fun (x : K) ↦ x ∈ v.integer) ((↑y : K) / (↑x : K)) this) x ∈ I

Tactic:
I.smul_mem ⟨_, this⟩ hx

Premises used: Subtype.mk, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Valuation.Integers
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 : Γ₀)
h : y = HSMul.hSMul (α := ↥v.integer) (Subtype.mk (p := fun (x : K) ↦ x ∈ v.integer) ((↑y : K) / (↑x : K)) this) x
⊢ y ∈ I

Tactic:
convert! I.smul_mem ⟨_, this⟩ hx using 1

Premises used: Subtype.mk, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Valuation.Integers
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 = HSMul.hSMul (α := ↥v.integer) (Subtype.mk (p := fun (x : K) ↦ x ∈ v.integer) ((↑y : K) / (↑x : K)) this) x

Tactic:
simp [Subtype.ext_iff, div_mul_cancel₀ _ (ZeroMemClass.coe_eq_zero.not.mpr hx0)]

Premises used: ZeroMemClass.coe_eq_zero, Iff.mpr, div_mul_cancel₀, Iff.not, Subtype.ext_iff
-- Module: Mathlib.RingTheory.Valuation.Integers
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
hxv : Ne.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀) (0 : Γ₀)
⊢ v.ltIdeal (Units.mk0 ((v : (a : K) → Γ₀) (↑x : K)) hxv) ≤ I

Tactic:
(leIdeal_v_le_of_mem v hx).trans' (ltIdeal_le_leIdeal _ _)

Premises used: Valuation.ltIdeal_le_leIdeal, Valuation.leIdeal_v_le_of_mem, LE.le.trans'
-- 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
⊢ Nontrivial R

Tactic:
nontriviality R
-- 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
⊢ Nontrivial O

Tactic:
have : Nontrivial O := hv.nontrivial_iff.mpr inferInstance
-- 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
mp : IsIntegral O x → LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
mpr : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀) → IsIntegral O x
⊢ IsIntegral O x ↔ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
constructor
-- 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
pos : ∀ (hn : f.natDegree = 0), LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
neg : ∀ (hn : ¬f.natDegree = 0), LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
by_cases hn : f.natDegree = 0

Premises used: Polynomial.natDegree
-- 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
⊢ ∃ (x : O), (C : (a : O) → O[X]) x = f

Tactic:
rw [Polynomial.natDegree_eq_zero] at hn

Premises used: Polynomial.natDegree_eq_zero