-- Mathlib/RingTheory/Valuation/ValuationRing.lean
theorem isFractionRing_iff [ValuationRing 𝒪] :
    IsFractionRing 𝒪 K ↔
      (∀ (x : K), ∃ a : 𝒪, x = algebraMap 𝒪 K a ∨ x⁻¹ = algebraMap 𝒪 K a) ∧
        Function.Injective (algebraMap 𝒪 K)

Proof state:
case refine_1.inl.intro
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : ValuationRing 𝒪
h : IsFractionRing 𝒪 K
x : K
a : 𝒪
e : (algebraMap 𝒪 K) a = x
⊢ ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a

case refine_1.inr.intro
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : ValuationRing 𝒪
h : IsFractionRing 𝒪 K
x : K
a : 𝒪
e : (algebraMap 𝒪 K) a = x⁻¹
⊢ ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a

Tactic:
exacts [⟨a, .inl e.symm⟩, ⟨a, .inr e.symm⟩]

Result:
no goals

Proof state:
case refine_2.map_units'
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : ValuationRing 𝒪
h : (∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a) ∧ Function.Injective ⇑(algebraMap 𝒪 K)
a : ↥(nonZeroDivisors 𝒪)
⊢ IsUnit ((algebraMap 𝒪 K) ↑a)

Tactic:
simpa using h.2.ne_iff.mpr (nonZeroDivisors.ne_zero a.2)

Result:
no goals

Proof state:
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : ValuationRing 𝒪
h : (∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a) ∧ Function.Injective ⇑(algebraMap 𝒪 K)
x : K
a : 𝒪
ha : x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a
h0 : a = 0
⊢ x * (algebraMap 𝒪 K) ↑(0, 1).2 = (algebraMap 𝒪 K) (0, 1).1

Tactic:
simpa [h0] using ha

Result:
no goals

Proof state:
case refine_2
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : ValuationRing 𝒪
h : (∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a) ∧ Function.Injective ⇑(algebraMap 𝒪 K)
⊢ IsFractionRing 𝒪 K

Tactic:
constructor

Result:
case refine_2.map_units'
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : ValuationRing 𝒪
h : (∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a) ∧ Function.Injective ⇑(algebraMap 𝒪 K)
⊢ ∀ (y : ↥(nonZeroDivisors 𝒪)), IsUnit ((algebraMap 𝒪 K) ↑y)

case refine_2.surj'
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : ValuationRing 𝒪
h : (∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a) ∧ Function.Injective ⇑(algebraMap 𝒪 K)
⊢ ∀ (z : K), ∃ x, z * (algebraMap 𝒪 K) ↑x.2 = (algebraMap 𝒪 K) x.1

case refine_2.exists_of_eq
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : ValuationRing 𝒪
h : (∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a) ∧ Function.Injective ⇑(algebraMap 𝒪 K)
⊢ ∀ {x y : 𝒪}, (algebraMap 𝒪 K) x = (algebraMap 𝒪 K) y → ∃ c, ↑c * x = ↑c * y

Proof state:
case refine_1
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : ValuationRing 𝒪
h : IsFractionRing 𝒪 K
x : K
⊢ ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a

Tactic:
obtain (⟨a, e⟩ | ⟨a, e⟩) := isInteger_or_isInteger 𝒪 x

Result:
case refine_1.inl.intro
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : ValuationRing 𝒪
h : IsFractionRing 𝒪 K
x : K
a : 𝒪
e : (algebraMap 𝒪 K) a = x
⊢ ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a

case refine_1.inr.intro
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : ValuationRing 𝒪
h : IsFractionRing 𝒪 K
x : K
a : 𝒪
e : (algebraMap 𝒪 K) a = x⁻¹
⊢ ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a

Proof state:
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : ValuationRing 𝒪
h : (∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a) ∧ Function.Injective ⇑(algebraMap 𝒪 K)
x : K
a : 𝒪
h0 : ¬a = 0
this : (algebraMap 𝒪 K) a ≠ 0
ha : x * (algebraMap 𝒪 K) a = 1
⊢ x * (algebraMap 𝒪 K) ↑(1, ⟨a, ⋯⟩).2 = (algebraMap 𝒪 K) (1, ⟨a, ⋯⟩).1

Tactic:
simpa using ha

Result:
no goals

Proof state:
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : ValuationRing 𝒪
h : (∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a) ∧ Function.Injective ⇑(algebraMap 𝒪 K)
x✝ y✝ : 𝒪
hab : (algebraMap 𝒪 K) x✝ = (algebraMap 𝒪 K) y✝
⊢ ↑1 * x✝ = ↑1 * y✝

Tactic:
simp only [OneMemClass.coe_one, h.2 hab, one_mul]

Result:
no goals

Proof state:
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : ValuationRing 𝒪
⊢ IsFractionRing 𝒪 K ↔
    (∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a) ∧ Function.Injective ⇑(algebraMap 𝒪 K)

Tactic:
refine ⟨fun h ↦ ⟨fun x ↦ ?_, IsFractionRing.injective _ _⟩, fun h ↦ ?_⟩

Result:
case refine_1
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : ValuationRing 𝒪
h : IsFractionRing 𝒪 K
x : K
⊢ ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a

case refine_2
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : ValuationRing 𝒪
h : (∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a) ∧ Function.Injective ⇑(algebraMap 𝒪 K)
⊢ IsFractionRing 𝒪 K

Proof state:
case refine_2.exists_of_eq
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : ValuationRing 𝒪
h : (∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a) ∧ Function.Injective ⇑(algebraMap 𝒪 K)
⊢ ∀ {x y : 𝒪}, (algebraMap 𝒪 K) x = (algebraMap 𝒪 K) y → ∃ c, ↑c * x = ↑c * y

Tactic:
intro _ _ hab

Result:
case refine_2.exists_of_eq
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : ValuationRing 𝒪
h : (∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a) ∧ Function.Injective ⇑(algebraMap 𝒪 K)
x✝ y✝ : 𝒪
hab : (algebraMap 𝒪 K) x✝ = (algebraMap 𝒪 K) y✝
⊢ ∃ c, ↑c * x✝ = ↑c * y✝

Proof state:
case neg
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : ValuationRing 𝒪
h : (∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a) ∧ Function.Injective ⇑(algebraMap 𝒪 K)
x : K
a : 𝒪
ha : x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a
h0 : ¬a = 0
⊢ ∃ x_1, x * (algebraMap 𝒪 K) ↑x_1.2 = (algebraMap 𝒪 K) x_1.1

Tactic:
have : algebraMap 𝒪 K a ≠ 0 := by simpa using h.2.ne_iff.mpr h0

Result:
case neg
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : IsDomain 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : ValuationRing 𝒪
h : (∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a) ∧ Function.Injective ⇑(algebraMap 𝒪 K)
x : K
a : 𝒪
ha : x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a
h0 : ¬a = 0
this : (algebraMap 𝒪 K) a ≠ 0
⊢ ∃ x_1, x * (algebraMap 𝒪 K) ↑x_1.2 = (algebraMap 𝒪 K) x_1.1