awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.Integers
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 : Nontrivial R
o0 : O
ho0 : Eq.{u + 1} (α := R) ((algebraMap O R : (a : O) → R) o0 : R) (0 : R)
o1 : O
ho1 : Eq.{u + 1} (α := R) ((algebraMap O R : (a : O) → R) o1 : R) (1 : R)
mpr : o0 ≠ o1
⊢ Nontrivial O

Tactic:
refine ⟨o0, o1, ?_⟩
-- Module: Mathlib.RingTheory.Valuation.Integers
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 : Nontrivial R
o0 : O
ho0 : Eq.{u + 1} (α := R) ((algebraMap O R : (a : O) → R) o0 : R) (0 : R)
ho1 : Eq.{u + 1} (α := R) ((algebraMap O R : (a : O) → R) o0 : R) (1 : R)
⊢ False

Tactic:
simp [ho1] at ho0
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ Nontrivial.{u} ↥v.integer ↔ Nontrivial R

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

Premises used: Valuation.integer.integers, Valuation.Integers.nontrivial_iff
-- 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
x y : O
h :
  LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
    ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
hy : Ne.{u + 1} (α := F) ((algebraMap O F : (a : O) → F) y : F) (0 : F)
grw :
  LE.le.{v} (α := Γ₀)
    ((v : (a : F) → Γ₀)
        (HMul.hMul (α := F) (β := F) (((algebraMap O F : (a : O) → F) y)⁻¹ : F)
          ((algebraMap O F : (a : O) → F) x : F)) :
      Γ₀)
    ((v : (a : F) → Γ₀) 1 : Γ₀)
grw₁ :
  LE.le.{v} (α := Γ₀)
    ((v : (a : F) → Γ₀)
        (HMul.hMul (α := F) (β := F) (((algebraMap O F : (a : O) → F) y)⁻¹ : F)
          ((algebraMap O F : (a : O) → F) x : F)) :
      Γ₀)
    ((v : (a : F) → Γ₀)
        (HMul.hMul (α := F) (β := F) (((algebraMap O F : (a : O) → F) y)⁻¹ : F)
          ((algebraMap O F : (a : O) → F) y : F)) :
      Γ₀)
grw₂ :
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) (((algebraMap O F : (a : O) → F) y)⁻¹ : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) ≤
    (v : (a : F) → Γ₀)
      (HMul.hMul (α := F) (β := F) (((algebraMap O F : (a : O) → F) y)⁻¹ : F) ((algebraMap O F : (a : O) → F) y : F))
grw₃ :
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) (((algebraMap O F : (a : O) → F) y)⁻¹ : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) (((algebraMap O F : (a : O) → F) y)⁻¹ : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
grw₄ grw₅ :
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) (((algebraMap O F : (a : O) → F) y)⁻¹ : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) (((algebraMap O F : (a : O) → F) y)⁻¹ : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
⊢ LE.le.{v} (α := Γ₀)
    ((v : (a : F) → Γ₀)
        (HMul.hMul (α := F) (β := F) (((algebraMap O F : (a : O) → F) y)⁻¹ : F)
          ((algebraMap O F : (a : O) → F) x : F)) :
      Γ₀)
    (1 : Γ₀)

Tactic:
grw [← v.map_one, ← inv_mul_cancel₀ hy, v.map_mul, v.map_mul, h]

Premises used: Valuation.map_mul, Valuation.map_one, inv_mul_cancel₀
-- 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
x y : O
⊢ x ∣ y ↔
    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) : Γ₀)

Tactic:
⟨hv.le_of_dvd, hv.dvd_of_le⟩

Premises used: Valuation.Integers.le_of_dvd, Valuation.Integers.dvd_of_le, Iff.intro
-- 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
x y : O
⊢ LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀) ↔
    y ∣ x

Tactic:
⟨hv.dvd_of_le, hv.le_of_dvd⟩

Premises used: Valuation.Integers.le_of_dvd, Valuation.Integers.dvd_of_le, Iff.intro
-- 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
x : O
hvx : Eq.{v + 1} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) (1 : Γ₀)
⊢ IsUnit x

Tactic:
isUnit_of_one hv (IsUnit.mk0 _ ?_) hvx

Premises used: Valuation.Integers.isUnit_of_one, IsUnit.mk0
-- 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
x : O
hvx : Eq.{v + 1} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) (1 : Γ₀)
refine : Ne.{u + 1} (α := F) ((algebraMap O F : (a : O) → F) x : F) (0 : F)
⊢ IsUnit x

Tactic:
refine isUnit_of_one hv (IsUnit.mk0 _ ?_) hvx

Premises used: Valuation.Integers.isUnit_of_one, IsUnit.mk0
-- 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
x : O
hvx : Eq.{v + 1} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) (1 : Γ₀)
⊢ Ne.{u + 1} (α := F) ((algebraMap O F : (a : O) → F) x : F) (0 : F)

Tactic:
simp only [← v.ne_zero_iff, hvx, ne_eq, one_ne_zero, not_false_eq_true]

Premises used: ne_eq, Valuation.ne_zero_iff, one_ne_zero, not_false_eq_true
-- 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
x : O
⊢ IsUnit x ↔ Eq.{v + 1} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) (1 : Γ₀)

Tactic:
⟨hv.one_of_isUnit, hv.isUnit_of_one'⟩

Premises used: Valuation.Integers.isUnit_of_one', Iff.intro, Valuation.Integers.one_of_isUnit
-- 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
ϖ : O
h : Irreducible ϖ
⊢ LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) ϖ : F) : Γ₀) (1 : Γ₀)

Tactic:
lt_of_le_of_ne (hv.map_le_one ϖ) (mt hv.isUnit_iff_valuation_eq_one.mpr h.not_isUnit)

Premises used: Iff.mpr, Valuation.Integers.map_le_one, Irreducible.not_isUnit, mt, Valuation.Integers.isUnit_iff_valuation_eq_one, lt_of_le_of_ne
-- 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
x : Oˣ
⊢ Eq.{v + 1} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) (↑x : O) : F) : Γ₀) (1 : Γ₀)

Tactic:
simp [← hv.isUnit_iff_valuation_eq_one]

Premises used: 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 Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
x : O
rw : ¬LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) (0 : Γ₀) ↔ x ≠ 0
⊢ LT.lt.{v} (α := Γ₀) (0 : Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) ↔ x ≠ 0

Tactic:
rw [← not_le]

Premises used: not_le
-- 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
x : O
⊢ ¬LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) (0 : Γ₀) ↔ x ≠ 0

Tactic:
not_congr ?_

Premises used: not_congr
-- 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
x : O
refine : LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) (0 : Γ₀) ↔ x = 0
⊢ ¬LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) (0 : Γ₀) ↔ x ≠ 0

Tactic:
refine not_congr ?_

Premises used: not_congr
-- 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
x : O
⊢ LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) (0 : Γ₀) ↔ x = 0

Tactic:
simp [map_eq_zero_iff _ hv.hom_inj]

Premises used: Valuation.Integers.hom_inj, map_eq_zero_iff
-- 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
ϖ : O
h : Irreducible ϖ
⊢ LT.lt.{v} (α := Γ₀) (0 : Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) ϖ : F) : Γ₀)

Tactic:
hv.valuation_pos_iff_ne_zero.mpr h.ne_zero

Premises used: Iff.mpr, Valuation.Integers.valuation_pos_iff_ne_zero, Irreducible.ne_zero
-- 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
x y : O
rw : DvdNotUnit x y ↔ x ∣ y ∧ ¬y ∣ x
⊢ DvdNotUnit x y ↔
    LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)

Tactic:
rw [lt_iff_le_not_ge, hv.le_iff_dvd, hv.le_iff_dvd]

Premises used: lt_iff_le_not_ge, 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
x y : O
⊢ DvdNotUnit x y ↔ x ∣ y ∧ ¬y ∣ x

Tactic:
⟨?_, And.elim dvdNotUnit_of_dvd_of_not_dvd⟩

Premises used: And.elim, dvdNotUnit_of_dvd_of_not_dvd, Iff.intro
-- 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
x y : O
refine : DvdNotUnit x y → x ∣ y ∧ ¬y ∣ x
⊢ DvdNotUnit x y ↔ x ∣ y ∧ ¬y ∣ x

Tactic:
refine ⟨?_, And.elim dvdNotUnit_of_dvd_of_not_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
x : O
hx0 : x ≠ 0
d : O
hdu : ¬IsUnit d
⊢ x ∣ x * d ∧ ¬x * d ∣ x

Tactic:
⟨⟨d, rfl⟩, ?_⟩

Premises used: And.intro, Exists.intro, 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
hv : v.Integers O
x : O
hx0 : x ≠ 0
d : O
hdu : ¬IsUnit d
refine : ¬x * d ∣ x
⊢ x ∣ x * d ∧ ¬x * d ∣ x

Tactic:
refine ⟨⟨d, 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
hv : v.Integers O
x : O
hx0 : x ≠ 0
d : O
hdu : ¬IsUnit d
⊢ LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) d : F) : Γ₀) (1 : Γ₀)

Tactic:
rw [hv.isUnit_iff_valuation_eq_one, ← ne_eq, ne_iff_lt_iff_le.mpr (hv.map_le_one d)] at hdu

Premises used: Iff.mpr, Valuation.Integers.map_le_one, ne_eq, ne_iff_lt_iff_le, 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 Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
x : O
hx0 : x ≠ 0
d : O
hdu : LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) d : F) : Γ₀) (1 : Γ₀)
rw :
  ¬LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) (x * d) : F) : Γ₀)
⊢ ¬x * d ∣ x

Tactic:
rw [dvd_iff_le hv]

Premises used: Valuation.Integers.dvd_iff_le
-- 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
x : O
hx0 : x ≠ 0
d : O
hdu : LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) d : F) : Γ₀) (1 : Γ₀)
simp :
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) d : F) : Γ₀) <
    (v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F)
⊢ ¬LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) (x * d) : F) : Γ₀)

Tactic:
simp only [map_mul, not_le]

Premises used: not_le, map_mul
-- 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
x : O
hx0 : x ≠ 0
d : O
hdu : LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) d : F) : Γ₀) (1 : Γ₀)
contrapose! :
  ∀
    (hdu :
      (v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) ≤
        HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
          ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) d : F) : Γ₀)),
    LE.le.{v} (α := Γ₀) (1 : Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) d : F) : Γ₀)
⊢ HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) d : F) : Γ₀) <
    (v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F)

Tactic:
contrapose! hdu
-- 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
x : O
hx0 : x ≠ 0
d : O
hdu :
  (v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) d : F) : Γ₀)
⊢ LE.le.{v} (α := Γ₀) (1 : Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) d : F) : Γ₀)

Tactic:
one_le_of_le_mul_left₀ ?_ hdu

Premises used: one_le_of_le_mul_left₀
-- 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
x : O
hx0 : x ≠ 0
d : O
hdu :
  (v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) d : F) : Γ₀)
refine : LT.lt.{v} (α := Γ₀) (0 : Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
⊢ LE.le.{v} (α := Γ₀) (1 : Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) d : F) : Γ₀)

Tactic:
refine one_le_of_le_mul_left₀ ?_ hdu

Premises used: one_le_of_le_mul_left₀
-- 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
x : O
hx0 : x ≠ 0
d : O
hdu :
  (v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) d : F) : Γ₀)
⊢ LT.lt.{v} (α := Γ₀) (0 : Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)

Tactic:
simp [hv.valuation_pos_iff_ne_zero, hx0]

Premises used: Valuation.Integers.valuation_pos_iff_ne_zero
-- 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
x : F
inl :
  ∀ (h : LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) x : Γ₀) (1 : Γ₀)),
    ∃ (a : O), x = (algebraMap O F : (a : O) → F) a ∨ x⁻¹ = (algebraMap O F : (a : O) → F) a
inr :
  ∀ (h : LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)),
    ∃ (a : O), x = (algebraMap O F : (a : O) → F) a ∨ x⁻¹ = (algebraMap O F : (a : O) → F) a
⊢ ∃ (a : O), x = (algebraMap O F : (a : O) → F) a ∨ x⁻¹ = (algebraMap O F : (a : O) → F) a

Tactic:
rcases val_le_one_or_val_inv_le_one v x with h | h

Premises used: Valuation.val_le_one_or_val_inv_le_one
-- 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
x : F
h : LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) x : Γ₀) (1 : Γ₀)
inl :
  ∀ (a : O) (ha : (algebraMap O F : (a : O) → F) a = x),
    ∃ (a : O), x = (algebraMap O F : (a : O) → F) a ∨ x⁻¹ = (algebraMap O F : (a : O) → F) a
⊢ ∃ (a : O), x = (algebraMap O F : (a : O) → F) a ∨ x⁻¹ = (algebraMap O F : (a : O) → F) a

Tactic:
obtain ⟨a, ha⟩ := exists_of_le_one hv h

Premises used: Valuation.Integers.exists_of_le_one
-- 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
x : F
h : LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)
inr :
  ∀ (a : O) (ha : (algebraMap O F : (a : O) → F) a = x⁻¹),
    ∃ (a : O), x = (algebraMap O F : (a : O) → F) a ∨ x⁻¹ = (algebraMap O F : (a : O) → F) a
⊢ ∃ (a : O), x = (algebraMap O F : (a : O) → F) a ∨ x⁻¹ = (algebraMap O F : (a : O) → F) a

Tactic:
obtain ⟨a, ha⟩ := exists_of_le_one hv h

Premises used: Valuation.Integers.exists_of_le_one
-- 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
x : F
h : LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) x : Γ₀) (1 : Γ₀)
a : O
ha : (algebraMap O F : (a : O) → F) a = x
⊢ ∃ (a : O), x = (algebraMap O F : (a : O) → F) a ∨ x⁻¹ = (algebraMap O F : (a : O) → F) a

Tactic:
⟨a, Or.inl ha.symm⟩

Premises used: Exists.intro, Or.inl, Eq.symm
-- 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
x : F
h : LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)
a : O
ha : (algebraMap O F : (a : O) → F) a = x⁻¹
⊢ ∃ (a : O), x = (algebraMap O F : (a : O) → F) a ∨ x⁻¹ = (algebraMap O F : (a : O) → F) a

Tactic:
⟨a, Or.inr ha.symm⟩

Premises used: Exists.intro, Eq.symm, Or.inr
-- 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
x : F
h : LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) x : Γ₀) (1 : Γ₀)
a : O
ha : (algebraMap O F : (a : O) → F) a = x
⊢ ∃ (a : O), x = (algebraMap O F : (a : O) → F) a ∨ x⁻¹ = (algebraMap O F : (a : O) → F) a

Tactic:
exacts [⟨a, Or.inl ha.symm⟩, ⟨a, Or.inr ha.symm⟩]
-- 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
x : O
inl :
  (↑(Ideal.span {0}) : 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) 0 : F) : Γ₀)}
inr :
  ∀ (hx : x ≠ 0),
    (↑(Ideal.span {x}) : 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) : Γ₀)}
⊢ (↑(Ideal.span {x}) : 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) : Γ₀)}

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Premises used: eq_or_ne, OfNat.ofNat, 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
hv : v.Integers O
⊢ (↑(Ideal.span {0}) : 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) 0 : F) : Γ₀)}

Tactic:
simp [Set.singleton_zero, map_eq_zero_iff _ hv.hom_inj]

Premises used: Valuation.Integers.hom_inj, map_eq_zero_iff, Set.singleton_zero
-- 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
x : O
hx : x ≠ 0
inr :
  ∀ (x_1 : O),
    x_1 ∈ (↑(Ideal.span {x}) : Set O) ↔
      Membership.mem (γ := 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_1
⊢ (↑(Ideal.span {x}) : 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) : Γ₀)}

Tactic:
ext
-- 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
x : O
hx : x ≠ 0
x_1 : O
⊢ x_1 ∈ (↑(Ideal.span {x}) : Set O) ↔
    Membership.mem (γ := 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_1

Tactic:
simp [SetLike.mem_coe, Ideal.mem_span_singleton, hv.dvd_iff_le]

Premises used: SetLike.mem_coe, Ideal.mem_span_singleton, Valuation.Integers.dvd_iff_le
-- 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
inst_4 : Subsingleton.{v + 1} (↥(MonoidHom.mrange v))ˣ
⊢ Function.Bijective.{w + 1, u + 1} (α := O) (β := F) (⇑(algebraMap O F) : (a : O) → F)

Tactic:
⟨hv.hom_inj, fun x ↦ hv.exists_of_le_one ?_⟩

Premises used: Valuation.Integers.exists_of_le_one, Valuation.Integers.hom_inj, And.intro, Function.Bijective