-- Mathlib/RingTheory/Valuation/Integers.lean
theorem dvdNotUnit_iff_lt (hv : Integers v O) {x y : O} :
    DvdNotUnit x y ↔ v (algebraMap O F y) < v (algebraMap O F x)

Proof state:
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x y : O
⊢ DvdNotUnit x y ↔ x ∣ y ∧ ¬y ∣ x

Tactic:
refine ⟨?_, And.elim dvdNotUnit_of_dvd_of_not_dvd⟩

Result:
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x y : O
⊢ DvdNotUnit x y → x ∣ y ∧ ¬y ∣ x

Proof state:
case intro.intro.intro
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : O
hx0 : x ≠ 0
d : O
hdu : v ((algebraMap O F) x) ≤ v ((algebraMap O F) x) * v ((algebraMap O F) d)
⊢ 0 < v ((algebraMap O F) x)

Tactic:
simp [hv.valuation_pos_iff_ne_zero, hx0]

Result:
no goals

Proof state:
case intro.intro.intro
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : O
hx0 : x ≠ 0
d : O
hdu : v ((algebraMap O F) d) < 1
⊢ ¬v ((algebraMap O F) x) ≤ v ((algebraMap O F) (x * d))

Tactic:
simp only [_root_.map_mul, not_le]

Result:
case intro.intro.intro
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : O
hx0 : x ≠ 0
d : O
hdu : v ((algebraMap O F) d) < 1
⊢ v ((algebraMap O F) x) * v ((algebraMap O F) d) < v ((algebraMap O F) x)

Proof state:
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x y : O
⊢ DvdNotUnit x y ↔ v ((algebraMap O F) y) < v ((algebraMap O F) x)

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

Result:
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x y : O
⊢ DvdNotUnit x y ↔ x ∣ y ∧ ¬y ∣ x

Proof state:
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x y : O
⊢ DvdNotUnit x y → x ∣ y ∧ ¬y ∣ x

Tactic:
rintro ⟨hx0, d, hdu, rfl⟩

Result:
case intro.intro.intro
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : O
hx0 : x ≠ 0
d : O
hdu : ¬IsUnit d
⊢ x ∣ x * d ∧ ¬x * d ∣ x

Proof state:
case intro.intro.intro
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : O
hx0 : x ≠ 0
d : O
hdu : ¬IsUnit d
⊢ ¬x * d ∣ x

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

Result:
case intro.intro.intro
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : O
hx0 : x ≠ 0
d : O
hdu : v ((algebraMap O F) d) < 1
⊢ ¬x * d ∣ x

Proof state:
case intro.intro.intro
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : O
hx0 : x ≠ 0
d : O
hdu : v ((algebraMap O F) d) < 1
⊢ v ((algebraMap O F) x) * v ((algebraMap O F) d) < v ((algebraMap O F) x)

Tactic:
contrapose! hdu

Result:
case intro.intro.intro
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : O
hx0 : x ≠ 0
d : O
hdu : v ((algebraMap O F) x) ≤ v ((algebraMap O F) x) * v ((algebraMap O F) d)
⊢ 1 ≤ v ((algebraMap O F) d)

Proof state:
case intro.intro.intro
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : O
hx0 : x ≠ 0
d : O
hdu : ¬IsUnit d
⊢ x ∣ x * d ∧ ¬x * d ∣ x

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

Result:
case intro.intro.intro
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : O
hx0 : x ≠ 0
d : O
hdu : ¬IsUnit d
⊢ ¬x * d ∣ x

Proof state:
case intro.intro.intro
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : O
hx0 : x ≠ 0
d : O
hdu : v ((algebraMap O F) d) < 1
⊢ ¬x * d ∣ x

Tactic:
rw [dvd_iff_le hv]

Result:
case intro.intro.intro
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : O
hx0 : x ≠ 0
d : O
hdu : v ((algebraMap O F) d) < 1
⊢ ¬v ((algebraMap O F) x) ≤ v ((algebraMap O F) (x * d))

Proof state:
case intro.intro.intro
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : O
hx0 : x ≠ 0
d : O
hdu : v ((algebraMap O F) x) ≤ v ((algebraMap O F) x) * v ((algebraMap O F) d)
⊢ 1 ≤ v ((algebraMap O F) d)

Tactic:
refine one_le_of_le_mul_left₀ ?_ hdu

Result:
case intro.intro.intro
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : O
hx0 : x ≠ 0
d : O
hdu : v ((algebraMap O F) x) ≤ v ((algebraMap O F) x) * v ((algebraMap O F) d)
⊢ 0 < v ((algebraMap O F) x)