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

Tactic:
rw [inv_eq_iff_eq_inv, ← one_div, eq_div_iff this] at ha

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 = 1
h0 : ¬a = 0
this : (algebraMap 𝒪 K) a ≠ 0
⊢ ∃ x_1, x * (algebraMap 𝒪 K) ↑x_1.2 = (algebraMap 𝒪 K) x_1.1

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
⊢ x * (algebraMap 𝒪 K) ↑(a, 1).2 = (algebraMap 𝒪 K) (a, 1).1

Tactic:
simpa

Result:
no goals

Proof state:
case refine_2.surj'.intro
𝒪 : 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
⊢ ∃ x_1, x * (algebraMap 𝒪 K) ↑x_1.2 = (algebraMap 𝒪 K) x_1.1

Tactic:
by_cases h0 : a = 0

Result:
case pos
𝒪 : 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

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

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 = 1
h0 : ¬a = 0
this : (algebraMap 𝒪 K) a ≠ 0
⊢ ∃ x_1, x * (algebraMap 𝒪 K) ↑x_1.2 = (algebraMap 𝒪 K) x_1.1

Tactic:
cases ha with
| inl ha => exact ⟨⟨a, 1⟩, by simpa⟩
| inr ha => exact ⟨⟨1, ⟨a, mem_nonZeroDivisors_of_ne_zero h0⟩⟩, by simpa using ha⟩

Result:
no goals

Proof state:
case neg.inl
𝒪 : 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
⊢ ∃ x_1, x * (algebraMap 𝒪 K) ↑x_1.2 = (algebraMap 𝒪 K) x_1.1

Tactic:
exact ⟨⟨a, 1⟩, by simpa⟩

Result:
no goals

Proof state:
case neg.inr
𝒪 : 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_1, x * (algebraMap 𝒪 K) ↑x_1.2 = (algebraMap 𝒪 K) x_1.1

Tactic:
exact ⟨⟨1, ⟨a, mem_nonZeroDivisors_of_ne_zero h0⟩⟩, by simpa using ha⟩

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)
⊢ ∀ (y : ↥(nonZeroDivisors 𝒪)), IsUnit ((algebraMap 𝒪 K) ↑y)

Tactic:
intro a

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)
a : ↥(nonZeroDivisors 𝒪)
⊢ IsUnit ((algebraMap 𝒪 K) ↑a)

Proof state:
case pos
𝒪 : 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:
exact ⟨⟨0, 1⟩, by simpa [h0] 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 : K
a : 𝒪
ha : x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a
h0 : ¬a = 0
⊢ (algebraMap 𝒪 K) a ≠ 0

Tactic:
simpa using h.2.ne_iff.mpr h0

Result:
no goals

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✝ : 𝒪
hab : (algebraMap 𝒪 K) x✝ = (algebraMap 𝒪 K) y✝
⊢ ∃ c, ↑c * x✝ = ↑c * y✝

Tactic:
exact ⟨1, by simp only [OneMemClass.coe_one, h.2 hab, one_mul]⟩

Result:
no goals

Proof state:
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

Tactic:
intro x

Result:
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)
x : K
⊢ ∃ x_1, x * (algebraMap 𝒪 K) ↑x_1.2 = (algebraMap 𝒪 K) x_1.1

Proof state:
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)
x : K
⊢ ∃ x_1, x * (algebraMap 𝒪 K) ↑x_1.2 = (algebraMap 𝒪 K) x_1.1

Tactic:
obtain ⟨a, ha⟩ := h.1 x

Result:
case refine_2.surj'.intro
𝒪 : 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
⊢ ∃ x_1, x * (algebraMap 𝒪 K) ↑x_1.2 = (algebraMap 𝒪 K) x_1.1