awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.Integers
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
hv : v.Integers O
I : Ideal O
a : O
ha : a ∈ I
hx :
  IsGreatest.{v} (α := Γ₀)
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) '' (↑I : Set O))
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) a)
b : O
h : b ∈ I
⊢ LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) b : F) : Γ₀)
    ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) a : F) : Γ₀)

Tactic:
exact hx.right (Set.mem_image_of_mem _ h)

Premises used: And.right, Set.mem_image_of_mem
-- Module: Mathlib.RingTheory.Valuation.Integers
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
hv : v.Integers O
I : Ideal O
a : O
ha : a ∈ I
hx :
  IsGreatest.{v} (α := Γ₀)
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) '' (↑I : Set O))
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) a)
b : O
h :
  LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) b : F) : Γ₀)
    ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) a : F) : Γ₀)
⊢ a ∣ b

Tactic:
rw [le_iff_dvd hv] at h

Premises used: Valuation.Integers.le_iff_dvd
-- Module: Mathlib.RingTheory.Valuation.Integers
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
hv : v.Integers O
I : Ideal O
a : O
ha : a ∈ I
hx :
  IsGreatest.{v} (α := Γ₀)
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) '' (↑I : Set O))
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) a)
b : O
h : a ∣ b
⊢ b ∈ I

Tactic:
Ideal.mem_of_dvd I h ha

Premises used: Ideal.mem_of_dvd
-- Module: Mathlib.RingTheory.Valuation.Integers
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
hv : v.Integers O
I : Ideal O
a : O
ha : a ∈ I
hx :
  IsGreatest.{v} (α := Γ₀)
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) '' (↑I : Set O))
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) a)
b : O
h : a ∣ b
⊢ b ∈ I

Tactic:
exact Ideal.mem_of_dvd I h ha

Premises used: Ideal.mem_of_dvd
-- Module: Mathlib.RingTheory.Valuation.Integers
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
hv : v.Integers O
I : Ideal O
x : O
hx :
  (↑I : Set O) =
    {y : O |
      LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
        ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)}
⊢ ∃ (x : Γ₀),
    IsGreatest
      (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) ''
        (↑I : Set O))
      x

Tactic:
⟨v (algebraMap O F x), Set.mem_image_of_mem _ ?_, ?_⟩

Premises used: Algebra.algebraMap, Set.mem_image_of_mem, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.Integers
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
hv : v.Integers O
I : Ideal O
x : O
hx :
  (↑I : Set O) =
    {y : O |
      LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
        ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)}
mpr : x ∈ (↑I : Set O)
mpr₁ :
  Membership.mem.{v, v} (α := Γ₀) (γ := Set Γ₀)
    (upperBounds
      (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) ''
        (↑I : Set O)))
    ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
⊢ ∃ (x : Γ₀),
    IsGreatest
      (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) ''
        (↑I : Set O))
      x

Tactic:
refine ⟨v (algebraMap O F x), Set.mem_image_of_mem _ ?_, ?_⟩
-- Module: Mathlib.RingTheory.Valuation.Integers
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
hv : v.Integers O
I : Ideal O
x : O
hx :
  (↑I : Set O) =
    {y : O |
      LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
        ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)}
⊢ x ∈ (↑I : Set O)

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.Valuation.Integers
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
hv : v.Integers O
I : Ideal O
x : O
hx :
  (↑I : Set O) =
    {y : O |
      LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
        ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)}
⊢ Membership.mem.{v, v} (α := Γ₀) (γ := Set Γ₀)
    (upperBounds
      (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) ''
        (↑I : Set O)))
    ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)

Tactic:
simp [hx, mem_upperBounds]

Premises used: mem_upperBounds
-- Module: Mathlib.RingTheory.Valuation.Integers
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)
a b : O
ha :
  Membership.mem (γ := Set O)
    (preimage.{w, v} (β := Γ₀)
      (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)) (Iio 1))
    a
hb :
  Membership.mem (γ := Set O)
    (preimage.{w, v} (β := Γ₀)
      (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)) (Iio 1))
    b
⊢ Membership.mem (γ := Set O)
    (preimage.{w, v} (β := Γ₀)
      (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)) (Iio 1))
    (a + b)

Tactic:
simpa using map_add_lt v ha hb

Premises used: Valuation.map_add_lt
-- Module: Mathlib.RingTheory.Valuation.Integers
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)
⊢ Membership.mem (γ := Set O)
    (preimage.{w, v} (β := Γ₀)
      (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)) (Iio 1))
    0

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Integers
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)
c x : O
simp :
  LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) (1 : Γ₀) →
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) c : F) : Γ₀)
        ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) <
      1
⊢ Membership.mem (γ := Set O)
      (preimage.{w, v} (β := Γ₀)
        (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)) (Iio 1))
      x →
    Membership.mem (γ := Set O)
      (preimage.{w, v} (β := Γ₀)
        (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)) (Iio 1))
      (c • x)

Tactic:
simp only [mem_preimage, Function.comp_apply, mem_Iio, smul_eq_mul, map_mul]

Premises used: Set.mem_Iio, map_mul, Function.comp_apply, smul_eq_mul, Set.mem_preimage
-- Module: Mathlib.RingTheory.Valuation.Integers
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)
c x : O
hx : LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) (1 : Γ₀)
⊢ HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) c : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) <
    1

Tactic:
Right.mul_lt_one_of_le_of_lt (hv.map_le_one c) hx

Premises used: Valuation.Integers.map_le_one, Right.mul_lt_one_of_le_of_lt
-- Module: Mathlib.RingTheory.Valuation.Integers
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)
c x : O
hx : LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) (1 : Γ₀)
⊢ HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) c : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) <
    1

Tactic:
exact Right.mul_lt_one_of_le_of_lt (hv.map_le_one c) hx

Premises used: Valuation.Integers.map_le_one, Right.mul_lt_one_of_le_of_lt
-- Module: Mathlib.RingTheory.Valuation.Integers
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),
    LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) (1 : Γ₀) ∧
      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) : Γ₀)

Tactic:
simpa [I, IsGreatest, hv.isPrincipal_iff_exists_isGreatest, ← image_preimage_eq_inter_range]
      using IsPrincipalIdealRing.principal I

Premises used: Valuation.Integers.isPrincipal_iff_exists_isGreatest, Set.image_preimage_eq_inter_range, IsGreatest, IsPrincipalIdealRing.principal
-- Module: Mathlib.RingTheory.Valuation.Integers
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' := ⋯ }
obtain :
  ∀ (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) : Γ₀)),
    False
⊢ False

Tactic:
obtain ⟨x, hx₁, hx⟩ :
    ∃ x, v (algebraMap O F x) < 1 ∧
      v (algebraMap O F x) ∈ upperBounds (Iio 1 ∩ range (v ∘ algebraMap O F)) := by
    simpa [I, IsGreatest, hv.isPrincipal_iff_exists_isGreatest, ← image_preimage_eq_inter_range]
      using IsPrincipalIdealRing.principal I

Premises used: Algebra.algebraMap, Function.comp, upperBounds, Inter.inter, Set.range, OfNat.ofNat, Set.Iio, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.Integers
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),
    LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) ((v : (a : F) → Γ₀) y : Γ₀) ∧
      LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) y : Γ₀) (1 : Γ₀)

Tactic:
simpa only [Subtype.exists, Subtype.mk_lt_mk, exists_range_iff, exists_prop]
      using H.dense ⟨v (algebraMap O F x), mem_range_self _⟩ ⟨1, 1, v.map_one⟩ hx₁

Premises used: Set.mem_range_self, Algebra.algebraMap, Subtype.mk_lt_mk, Subtype.exists, exists_prop, Subtype.mk, Valuation.map_one, Set.exists_range_iff, Exists.intro, OfNat.ofNat, DenselyOrdered.dense, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.Integers
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) : Γ₀)
obtain :
  ∀ (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
⊢ False

Tactic:
obtain ⟨y, hy, hy₁⟩ : ∃ y, v (algebraMap O F x) < v y ∧ v y < 1 := by
    simpa only [Subtype.exists, Subtype.mk_lt_mk, exists_range_iff, exists_prop]
      using H.dense ⟨v (algebraMap O F x), mem_range_self _⟩ ⟨1, 1, v.map_one⟩ hx₁

Premises used: Algebra.algebraMap, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.Integers
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 : Γ₀)
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
⊢ False

Tactic:
obtain ⟨z, rfl⟩ := hv.exists_of_le_one hy₁.le

Premises used: Valuation.Integers.exists_of_le_one, LT.lt.le, rfl
-- Module: Mathlib.RingTheory.Valuation.Integers
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) : Γ₀)
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:
hy.not_ge <| hx ⟨hy₁, mem_range_self _⟩

Premises used: Set.mem_range_self, And.intro, LT.lt.not_ge
-- Module: Mathlib.RingTheory.Valuation.Integers
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) : Γ₀)
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:
exact hy.not_ge <| hx ⟨hy₁, mem_range_self _⟩

Premises used: Set.mem_range_self, And.intro, LT.lt.not_ge
-- Module: Mathlib.RingTheory.Valuation.Integers
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) : Γ₀)
hv : v.Integers ↥v.integer
rw₁ : Valuation F Γ₀
⊢ ¬IsUnit x ↔ LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) (↑x : F) : Γ₀) (1 : Γ₀)

Tactic:
rw [← not_le, not_iff_not, isUnit_iff_valuation_eq_one (F := F) (Γ₀ := Γ₀),
    le_antisymm_iff]

Premises used: not_le, not_iff_not, le_antisymm_iff, Valuation.Integers.isUnit_iff_valuation_eq_one
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
x : ↥v.integer
⊢ 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:
and_iff_right x.2

Premises used: and_iff_right, Subtype.property
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
x : ↥v.integer
⊢ v.Integers ↥v.integer

Tactic:
integer.integers v

Premises used: Set.Mem, setOf, Valuation.integer.integers
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
ϖ : ↥v.integer
h : Irreducible ϖ
⊢ LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) (↑ϖ : F) : Γ₀) (1 : Γ₀)

Tactic:
(Valuation.integer.integers v).valuation_irreducible_lt_one h

Premises used: Valuation.Integers.valuation_irreducible_lt_one, Valuation.integer.integers
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
ϖ : ↥v.integer
h : Irreducible ϖ
⊢ LT.lt.{v} (α := Γ₀) (0 : Γ₀) ((v : (a : F) → Γ₀) (↑ϖ : F) : Γ₀)

Tactic:
(Valuation.integer.integers v).valuation_irreducible_pos h

Premises used: Valuation.integer.integers, Valuation.Integers.valuation_irreducible_pos
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
x : ↥v.integer
⊢ (↑(Ideal.span {x}) : Set ↥v.integer) =
    {y : ↥v.integer | LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) (↑y : F) : Γ₀) ((v : (a : F) → Γ₀) (↑x : F) : Γ₀)}

Tactic:
(Valuation.integer.integers v).coe_span_singleton_eq_setOf_le_v_algebraMap x

Premises used: Set.Mem, setOf, Valuation.integer.integers, Valuation.Integers.coe_span_singleton_eq_setOf_le_v_algebraMap
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : Γ₀
r : ↥v.integer
x : R
h : x ∈ (v.leAddSubgroup γ).carrier
⊢ r • x ∈ (v.leAddSubgroup γ).carrier

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

Premises used: mul_le_of_le_one_of_le, 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 Γ₀
γ : Γ₀ˣ
r : ↥v.integer
x : R
h : x ∈ (v.ltAddSubgroup γ).carrier
⊢ r • x ∈ (v.ltAddSubgroup γ).carrier

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.leSubmodule

Tactic:
leAddSubgroup_monotone v

Premises used: Set.Mem, Monotone, Valuation.leAddSubgroup, Valuation.leSubmodule, Valuation.leAddSubgroup_monotone