-- Mathlib/RingTheory/Valuation/ValuationRing.lean
theorem of_integers (v : Valuation K Γ) (hh : v.Integers 𝒪) : ValuationRing 𝒪

Proof state:
case cond'.inr
𝒪 : Type u
K : Type v
Γ : Type w
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
a b : 𝒪
h : v ((algebraMap 𝒪 K) b) ≤ v ((algebraMap 𝒪 K) a)
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
obtain ⟨c, hc⟩ := Valuation.Integers.dvd_of_le hh h

Result:
case cond'.inr.intro
𝒪 : Type u
K : Type v
Γ : Type w
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
a b : 𝒪
h : v ((algebraMap 𝒪 K) b) ≤ v ((algebraMap 𝒪 K) a)
c : 𝒪
hc : b = a * c
⊢ ∃ c, a * c = b ∨ b * c = a

Proof state:
𝒪 : Type u
K : Type v
Γ : Type w
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
⊢ ValuationRing 𝒪

Tactic:
suffices PreValuationRing 𝒪 from .mk

Result:
𝒪 : Type u
K : Type v
Γ : Type w
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
⊢ PreValuationRing 𝒪

Proof state:
case cond'.inl.intro
𝒪 : Type u
K : Type v
Γ : Type w
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
a b : 𝒪
h : v ((algebraMap 𝒪 K) a) ≤ v ((algebraMap 𝒪 K) b)
c : 𝒪
hc : a = b * c
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
use c

Result:
case h
𝒪 : Type u
K : Type v
Γ : Type w
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
a b : 𝒪
h : v ((algebraMap 𝒪 K) a) ≤ v ((algebraMap 𝒪 K) b)
c : 𝒪
hc : a = b * c
⊢ a * c = b ∨ b * c = a

Proof state:
case cond'
𝒪 : Type u
K : Type v
Γ : Type w
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
⊢ ∀ (a b : 𝒪), ∃ c, a * c = b ∨ b * c = a

Tactic:
intro a b

Result:
case cond'
𝒪 : Type u
K : Type v
Γ : Type w
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
a b : 𝒪
⊢ ∃ c, a * c = b ∨ b * c = a

Proof state:
case h
𝒪 : Type u
K : Type v
Γ : Type w
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
a b : 𝒪
h : v ((algebraMap 𝒪 K) a) ≤ v ((algebraMap 𝒪 K) b)
c : 𝒪
hc : a = b * c
⊢ a * c = b ∨ b * c = a

Tactic:
exact Or.inr hc.symm

Result:
no goals

Proof state:
case cond'.inl
𝒪 : Type u
K : Type v
Γ : Type w
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
a b : 𝒪
h : v ((algebraMap 𝒪 K) a) ≤ v ((algebraMap 𝒪 K) b)
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
obtain ⟨c, hc⟩ := Valuation.Integers.dvd_of_le hh h

Result:
case cond'.inl.intro
𝒪 : Type u
K : Type v
Γ : Type w
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
a b : 𝒪
h : v ((algebraMap 𝒪 K) a) ≤ v ((algebraMap 𝒪 K) b)
c : 𝒪
hc : a = b * c
⊢ ∃ c, a * c = b ∨ b * c = a

Proof state:
case h
𝒪 : Type u
K : Type v
Γ : Type w
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
a b : 𝒪
h : v ((algebraMap 𝒪 K) b) ≤ v ((algebraMap 𝒪 K) a)
c : 𝒪
hc : b = a * c
⊢ a * c = b ∨ b * c = a

Tactic:
exact Or.inl hc.symm

Result:
no goals

Proof state:
case cond'
𝒪 : Type u
K : Type v
Γ : Type w
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
a b : 𝒪
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
rcases le_total (v (algebraMap 𝒪 K a)) (v (algebraMap 𝒪 K b)) with h | h

Result:
case cond'.inl
𝒪 : Type u
K : Type v
Γ : Type w
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
a b : 𝒪
h : v ((algebraMap 𝒪 K) a) ≤ v ((algebraMap 𝒪 K) b)
⊢ ∃ c, a * c = b ∨ b * c = a

case cond'.inr
𝒪 : Type u
K : Type v
Γ : Type w
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
a b : 𝒪
h : v ((algebraMap 𝒪 K) b) ≤ v ((algebraMap 𝒪 K) a)
⊢ ∃ c, a * c = b ∨ b * c = a

Proof state:
𝒪 : Type u
K : Type v
Γ : Type w
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
⊢ PreValuationRing 𝒪

Tactic:
constructor

Result:
case cond'
𝒪 : Type u
K : Type v
Γ : Type w
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
⊢ ∀ (a b : 𝒪), ∃ c, a * c = b ∨ b * c = a

Proof state:
case cond'.inr.intro
𝒪 : Type u
K : Type v
Γ : Type w
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
a b : 𝒪
h : v ((algebraMap 𝒪 K) b) ≤ v ((algebraMap 𝒪 K) a)
c : 𝒪
hc : b = a * c
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
use c

Result:
case h
𝒪 : Type u
K : Type v
Γ : Type w
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
a b : 𝒪
h : v ((algebraMap 𝒪 K) b) ≤ v ((algebraMap 𝒪 K) a)
c : 𝒪
hc : b = a * c
⊢ a * c = b ∨ b * c = a