awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
h : ∀ (x : K), ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
hinj : Function.Injective.{u + 1, v + 1} (α := 𝒪) (β := K) (⇑(algebraMap 𝒪 K) : (a : 𝒪) → K)
this_1 : IsDomain 𝒪
this_2 : FaithfulSMul 𝒪 K
this : IsDomain 𝒪
x y : 𝒪
hab : Eq.{v + 1} (α := K) ((algebraMap 𝒪 K : (a : 𝒪) → K) x : K) ((algebraMap 𝒪 K : (a : 𝒪) → K) y : K)
⊢ (↑1 : 𝒪) * x = (↑1 : 𝒪) * y

Tactic:
simpa using hab
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
h : ∀ (x : K), ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
hinj : Function.Injective.{u + 1, v + 1} (α := 𝒪) (β := K) (⇑(algebraMap 𝒪 K) : (a : 𝒪) → K)
this_1 : IsDomain 𝒪
this_2 : FaithfulSMul 𝒪 K
this : IsDomain 𝒪
refine :
  ∀ (z : K),
    ∃ (x : 𝒪 × ↥(nonZeroDivisors 𝒪 : Submonoid 𝒪)),
      HMul.hMul (β := K) z ((algebraMap 𝒪 K : (a : 𝒪) → K) (↑x.2 : 𝒪) : K) = (algebraMap 𝒪 K : (a : 𝒪) → K) x.1
⊢ IsFractionRing 𝒪 K

Tactic:
refine ⟨by simp, ?_, fun hab ↦ ⟨1, by simpa using hab⟩⟩
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
h : ∀ (x : K), ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
hinj : Function.Injective.{u + 1, v + 1} (α := 𝒪) (β := K) (⇑(algebraMap 𝒪 K) : (a : 𝒪) → K)
this_1 : IsDomain 𝒪
this_2 : FaithfulSMul 𝒪 K
this : IsDomain 𝒪
x : K
obtain :
  ∀ (a : 𝒪) (ha : x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a),
    ∃ (x_1 : 𝒪 × ↥(nonZeroDivisors 𝒪 : Submonoid 𝒪)),
      HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) (↑x_1.2 : 𝒪) : K) = (algebraMap 𝒪 K : (a : 𝒪) → K) x_1.1
⊢ ∃ (x_1 : 𝒪 × ↥(nonZeroDivisors 𝒪 : Submonoid 𝒪)),
    HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) (↑x_1.2 : 𝒪) : K) = (algebraMap 𝒪 K : (a : 𝒪) → K) x_1.1

Tactic:
obtain ⟨a, ha⟩ := h x
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
h : ∀ (x : K), ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
hinj : Function.Injective.{u + 1, v + 1} (α := 𝒪) (β := K) (⇑(algebraMap 𝒪 K) : (a : 𝒪) → K)
this_1 : IsDomain 𝒪
this_2 : FaithfulSMul 𝒪 K
this : IsDomain 𝒪
x : K
a : 𝒪
ha : x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
pos :
  ∀ (h0 : a = 0),
    ∃ (x_1 : 𝒪 × ↥(nonZeroDivisors 𝒪 : Submonoid 𝒪)),
      HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) (↑x_1.2 : 𝒪) : K) = (algebraMap 𝒪 K : (a : 𝒪) → K) x_1.1
neg :
  ∀ (h0 : ¬a = 0),
    ∃ (x_1 : 𝒪 × ↥(nonZeroDivisors 𝒪 : Submonoid 𝒪)),
      HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) (↑x_1.2 : 𝒪) : K) = (algebraMap 𝒪 K : (a : 𝒪) → K) x_1.1
⊢ ∃ (x_1 : 𝒪 × ↥(nonZeroDivisors 𝒪 : Submonoid 𝒪)),
    HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) (↑x_1.2 : 𝒪) : K) = (algebraMap 𝒪 K : (a : 𝒪) → K) x_1.1

Tactic:
by_cases h0 : a = 0
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
h : ∀ (x : K), ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
hinj : Function.Injective.{u + 1, v + 1} (α := 𝒪) (β := K) (⇑(algebraMap 𝒪 K) : (a : 𝒪) → K)
this_1 : IsDomain 𝒪
this_2 : FaithfulSMul 𝒪 K
this : IsDomain 𝒪
x : K
a : 𝒪
ha : x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
h0 : a = 0
⊢ HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) (↑(0, 1).2 : 𝒪) : K) = (algebraMap 𝒪 K : (a : 𝒪) → K) (0, 1).1

Tactic:
simpa [h0, eq_comm] using ha

Premises used: eq_comm
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
h : ∀ (x : K), ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
hinj : Function.Injective.{u + 1, v + 1} (α := 𝒪) (β := K) (⇑(algebraMap 𝒪 K) : (a : 𝒪) → K)
this_1 : IsDomain 𝒪
this_2 : FaithfulSMul 𝒪 K
this : IsDomain 𝒪
x : K
a : 𝒪
ha : x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
h0 : a = 0
⊢ ∃ (x_1 : 𝒪 × ↥(nonZeroDivisors 𝒪 : Submonoid 𝒪)),
    HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) (↑x_1.2 : 𝒪) : K) = (algebraMap 𝒪 K : (a : 𝒪) → K) x_1.1

Tactic:
refine ⟨⟨0, 1⟩, by simpa [h0, eq_comm] using ha⟩
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
h : ∀ (x : K), ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
hinj : Function.Injective.{u + 1, v + 1} (α := 𝒪) (β := K) (⇑(algebraMap 𝒪 K) : (a : 𝒪) → K)
this_1 : IsDomain 𝒪
this_2 : FaithfulSMul 𝒪 K
this : IsDomain 𝒪
x : K
a : 𝒪
ha : x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
h0 : ¬a = 0
⊢ Ne.{v + 1} (α := K) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) (0 : K)

Tactic:
simpa using h0
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
h : ∀ (x : K), ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
hinj : Function.Injective.{u + 1, v + 1} (α := 𝒪) (β := K) (⇑(algebraMap 𝒪 K) : (a : 𝒪) → K)
this_1 : IsDomain 𝒪
this_2 : FaithfulSMul 𝒪 K
this : IsDomain 𝒪
x : K
a : 𝒪
ha : x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
h0 : ¬a = 0
⊢ Ne.{v + 1} (α := K) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) (0 : K)

Tactic:
have : algebraMap 𝒪 K a ≠ 0 := by simpa using h0
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
h : ∀ (x : K), ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
hinj : Function.Injective.{u + 1, v + 1} (α := 𝒪) (β := K) (⇑(algebraMap 𝒪 K) : (a : 𝒪) → K)
this_1 : IsDomain 𝒪
this_2 : FaithfulSMul 𝒪 K
this_3 : IsDomain 𝒪
x : K
a : 𝒪
ha : x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
h0 : ¬a = 0
this : Ne.{v + 1} (α := K) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) (0 : K)
⊢ x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) = 1

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

Premises used: one_div, eq_div_iff, inv_eq_iff_eq_inv
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
h : ∀ (x : K), ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
hinj : Function.Injective.{u + 1, v + 1} (α := 𝒪) (β := K) (⇑(algebraMap 𝒪 K) : (a : 𝒪) → K)
this_1 : IsDomain 𝒪
this_2 : FaithfulSMul 𝒪 K
this_3 : IsDomain 𝒪
x : K
a : 𝒪
ha : x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
h0 : ¬a = 0
this : Ne.{v + 1} (α := K) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) (0 : K)
ha₁ : x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) = 1
⊢ ¬a = 0

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

Premises used: one_div, eq_div_iff, inv_eq_iff_eq_inv
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
h : ∀ (x : K), ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
hinj : Function.Injective.{u + 1, v + 1} (α := 𝒪) (β := K) (⇑(algebraMap 𝒪 K) : (a : 𝒪) → K)
this_1 : IsDomain 𝒪
this_2 : FaithfulSMul 𝒪 K
this_3 : IsDomain 𝒪
x : K
a : 𝒪
ha : x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
h0 : ¬a = 0
this : Ne.{v + 1} (α := K) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) (0 : K)
ha₁ : x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) = 1
h0₁ : ¬a = 0
⊢ Ne.{v + 1} (α := K) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) (0 : K)

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

Premises used: one_div, eq_div_iff, inv_eq_iff_eq_inv
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
h : ∀ (x : K), ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
hinj : Function.Injective.{u + 1, v + 1} (α := 𝒪) (β := K) (⇑(algebraMap 𝒪 K) : (a : 𝒪) → K)
this_1 : IsDomain 𝒪
this_2 : FaithfulSMul 𝒪 K
this_3 : IsDomain 𝒪
x : K
a : 𝒪
h0 : ¬a = 0
this : Ne.{v + 1} (α := K) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) (0 : K)
ha : x = (algebraMap 𝒪 K : (a : 𝒪) → K) a
⊢ HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) (↑(a, 1).2 : 𝒪) : K) = (algebraMap 𝒪 K : (a : 𝒪) → K) (a, 1).1

Tactic:
simpa
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
h : ∀ (x : K), ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
hinj : Function.Injective.{u + 1, v + 1} (α := 𝒪) (β := K) (⇑(algebraMap 𝒪 K) : (a : 𝒪) → K)
this_1 : IsDomain 𝒪
this_2 : FaithfulSMul 𝒪 K
this_3 : IsDomain 𝒪
x : K
a : 𝒪
h0 : ¬a = 0
this : Ne.{v + 1} (α := K) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) (0 : K)
ha : x = (algebraMap 𝒪 K : (a : 𝒪) → K) a
⊢ ∃ (x_1 : 𝒪 × ↥(nonZeroDivisors 𝒪 : Submonoid 𝒪)),
    HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) (↑x_1.2 : 𝒪) : K) = (algebraMap 𝒪 K : (a : 𝒪) → K) x_1.1

Tactic:
exact ⟨⟨a, 1⟩, by simpa⟩
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
h : ∀ (x : K), ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
hinj : Function.Injective.{u + 1, v + 1} (α := 𝒪) (β := K) (⇑(algebraMap 𝒪 K) : (a : 𝒪) → K)
this_1 : IsDomain 𝒪
this_2 : FaithfulSMul 𝒪 K
this_3 : IsDomain 𝒪
x : K
a : 𝒪
h0 : ¬a = 0
this : Ne.{v + 1} (α := K) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) (0 : K)
ha : HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) = 1
⊢ HMul.hMul (β := K) x
      ((algebraMap 𝒪 K : (a : 𝒪) → K)
          (↑(1,
                  Subtype.mk (p := fun (x : 𝒪) ↦ Membership.mem (γ := Submonoid 𝒪) (nonZeroDivisors 𝒪 : Submonoid 𝒪) x)
                    a ⋯).2 :
            𝒪) :
        K) =
    (algebraMap 𝒪 K : (a : 𝒪) → K)
      (1, Subtype.mk (p := fun (x : 𝒪) ↦ Membership.mem (γ := Submonoid 𝒪) (nonZeroDivisors 𝒪 : Submonoid 𝒪) x) a ⋯).1

Tactic:
simpa using ha
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
h : ∀ (x : K), ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
hinj : Function.Injective.{u + 1, v + 1} (α := 𝒪) (β := K) (⇑(algebraMap 𝒪 K) : (a : 𝒪) → K)
this_1 : IsDomain 𝒪
this_2 : FaithfulSMul 𝒪 K
this_3 : IsDomain 𝒪
x : K
a : 𝒪
h0 : ¬a = 0
this : Ne.{v + 1} (α := K) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) (0 : K)
ha : HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) = 1
⊢ ∃ (x_1 : 𝒪 × ↥(nonZeroDivisors 𝒪 : Submonoid 𝒪)),
    HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) (↑x_1.2 : 𝒪) : K) = (algebraMap 𝒪 K : (a : 𝒪) → K) x_1.1

Tactic:
exact ⟨⟨1, ⟨a, mem_nonZeroDivisors_of_ne_zero h0⟩⟩, by simpa using ha⟩
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
h : ∀ (x : K), ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
hinj : Function.Injective.{u + 1, v + 1} (α := 𝒪) (β := K) (⇑(algebraMap 𝒪 K) : (a : 𝒪) → K)
this_1 : IsDomain 𝒪
this_2 : FaithfulSMul 𝒪 K
this_3 : IsDomain 𝒪
x : K
a : 𝒪
ha : x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) = 1
h0 : ¬a = 0
this : Ne.{v + 1} (α := K) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) (0 : K)
neg :
  ∀ (ha : x = (algebraMap 𝒪 K : (a : 𝒪) → K) a),
    ∃ (x_1 : 𝒪 × ↥(nonZeroDivisors 𝒪 : Submonoid 𝒪)),
      HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) (↑x_1.2 : 𝒪) : K) = (algebraMap 𝒪 K : (a : 𝒪) → K) x_1.1
neg₁ :
  ∀ (ha : HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) = 1),
    ∃ (x_1 : 𝒪 × ↥(nonZeroDivisors 𝒪 : Submonoid 𝒪)),
      HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) (↑x_1.2 : 𝒪) : K) = (algebraMap 𝒪 K : (a : 𝒪) → K) x_1.1
⊢ ∃ (x_1 : 𝒪 × ↥(nonZeroDivisors 𝒪 : Submonoid 𝒪)),
    HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) (↑x_1.2 : 𝒪) : K) = (algebraMap 𝒪 K : (a : 𝒪) → 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⟩
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
Γ : Type w
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hv : v.Integers 𝒪
⊢ IsFractionRing 𝒪 K

Tactic:
isFractionRing_of_exists_eq_algebraMap_or_inv_eq_algebraMap_of_injective
    hv.eq_algebraMap_or_inv_eq_algebraMap hv.hom_inj

Premises used: Valuation.Integers.hom_inj, Valuation.Integers.eq_algebraMap_or_inv_eq_algebraMap, isFractionRing_of_exists_eq_algebraMap_or_inv_eq_algebraMap_of_injective
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
Γ : Type w
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
⊢ IsFractionRing (↥v.integer) K

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

Premises used: Set.Mem, setOf, Valuation.integer.integers, Valuation.Integers.isFractionRing
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
Γ : Type w
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
⊢ IsDomain 𝒪

Tactic:
haveI := hh.hom_inj.isDomain
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
Γ : Type w
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
suffices : PreValuationRing 𝒪
⊢ ValuationRing 𝒪

Tactic:
suffices PreValuationRing 𝒪 from .mk
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
Γ : Type w
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
cond' : ∀ (a b : 𝒪), ∃ (c : 𝒪), a * c = b ∨ b * c = a
⊢ PreValuationRing 𝒪

Tactic:
constructor
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
Γ : Type w
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
a b : 𝒪
cond' :
  ∀
    (h :
      LE.le.{w} (α := Γ) ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) : Γ)
        ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) b : K) : Γ)),
    ∃ (c : 𝒪), a * c = b ∨ b * c = a
cond'₁ :
  ∀
    (h :
      LE.le.{w} (α := Γ) ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) b : K) : Γ)
        ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) : Γ)),
    ∃ (c : 𝒪), a * c = b ∨ b * c = a
⊢ ∃ (c : 𝒪), a * c = b ∨ b * c = a

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

Premises used: Algebra.algebraMap, le_total, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
Γ : Type w
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
a b : 𝒪
h :
  LE.le.{w} (α := Γ) ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) : Γ)
    ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) b : K) : Γ)
cond' : ∀ (c : 𝒪) (hc : a = b * c), ∃ (c : 𝒪), a * c = b ∨ b * c = a
⊢ ∃ (c : 𝒪), a * c = b ∨ b * c = a

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

Premises used: Valuation.Integers.dvd_of_le
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
Γ : Type w
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
a b : 𝒪
h :
  LE.le.{w} (α := Γ) ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) : Γ)
    ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) b : K) : Γ)
c : 𝒪
hc : a = b * c
h₁ : a * c = b ∨ b * c = a
⊢ ∃ (c : 𝒪), a * c = b ∨ b * c = a

Tactic:
use c
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
Γ : Type w
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
a b : 𝒪
h :
  LE.le.{w} (α := Γ) ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) : Γ)
    ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) b : K) : Γ)
c : 𝒪
hc : a = b * c
⊢ a * c = b ∨ b * c = a

Tactic:
Or.inr hc.symm

Premises used: Eq.symm, Or.inr
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
Γ : Type w
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
a b : 𝒪
h :
  LE.le.{w} (α := Γ) ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) : Γ)
    ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) b : K) : Γ)
c : 𝒪
hc : a = b * c
⊢ a * c = b ∨ b * c = a

Tactic:
exact Or.inr hc.symm

Premises used: Eq.symm, Or.inr
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
Γ : Type w
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
a b : 𝒪
h :
  LE.le.{w} (α := Γ) ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) b : K) : Γ)
    ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) : Γ)
cond' : ∀ (c : 𝒪) (hc : b = a * c), ∃ (c : 𝒪), a * c = b ∨ b * c = a
⊢ ∃ (c : 𝒪), a * c = b ∨ b * c = a

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

Premises used: Valuation.Integers.dvd_of_le
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
Γ : Type w
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
a b : 𝒪
h :
  LE.le.{w} (α := Γ) ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) b : K) : Γ)
    ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) : Γ)
c : 𝒪
hc : b = a * c
h₁ : a * c = b ∨ b * c = a
⊢ ∃ (c : 𝒪), a * c = b ∨ b * c = a

Tactic:
use c
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
Γ : Type w
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
a b : 𝒪
h :
  LE.le.{w} (α := Γ) ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) b : K) : Γ)
    ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) : Γ)
c : 𝒪
hc : b = a * c
⊢ a * c = b ∨ b * c = a

Tactic:
Or.inl hc.symm

Premises used: Or.inl, Eq.symm
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
Γ : Type w
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
a b : 𝒪
h :
  LE.le.{w} (α := Γ) ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) b : K) : Γ)
    ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) : Γ)
c : 𝒪
hc : b = a * c
⊢ a * c = b ∨ b * c = a

Tactic:
exact Or.inl hc.symm

Premises used: Or.inl, Eq.symm
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
Γ : Type w
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
⊢ ValuationRing.{v} ↥v.integer

Tactic:
of_integers (v := v) (Valuation.integer.integers v)

Premises used: Set.Mem, setOf, Valuation.integer.integers, ValuationRing.of_integers
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : IsDomain 𝒪
inst_4 : ValuationRing 𝒪
⊢ IsFractionRing 𝒪 K ↔
    (∀ (x : K), ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a) ∧
      Function.Injective.{u + 1, v + 1} (α := 𝒪) (β := K) (⇑(algebraMap 𝒪 K) : (a : 𝒪) → K)

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

Premises used: IsFractionRing.injective, And.intro, Iff.intro
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : IsDomain 𝒪
inst_4 : ValuationRing 𝒪
refine_1 :
  ∀ (h : IsFractionRing 𝒪 K) (x : K),
    ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
refine_2 :
  ∀
    (h :
      (∀ (x : K), ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a) ∧
        Function.Injective.{u + 1, v + 1} (α := 𝒪) (β := K) (⇑(algebraMap 𝒪 K) : (a : 𝒪) → K)),
    IsFractionRing 𝒪 K
⊢ IsFractionRing 𝒪 K ↔
    (∀ (x : K), ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a) ∧
      Function.Injective.{u + 1, v + 1} (α := 𝒪) (β := K) (⇑(algebraMap 𝒪 K) : (a : 𝒪) → K)

Tactic:
refine ⟨fun h ↦ ⟨fun x ↦ ?_, IsFractionRing.injective _ _⟩, fun h ↦ ?_⟩
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : IsDomain 𝒪
inst_4 : ValuationRing 𝒪
h : IsFractionRing 𝒪 K
x : K
refine_1 :
  ∀ (a : 𝒪) (e : (algebraMap 𝒪 K : (a : 𝒪) → K) a = x),
    ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
refine_1₁ :
  ∀ (a : 𝒪) (e : (algebraMap 𝒪 K : (a : 𝒪) → K) a = x⁻¹),
    ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
⊢ ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a

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

Premises used: ValuationRing.isInteger_or_isInteger
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : IsDomain 𝒪
inst_4 : ValuationRing 𝒪
h : IsFractionRing 𝒪 K
x : K
a : 𝒪
e : (algebraMap 𝒪 K : (a : 𝒪) → K) a = x
⊢ ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a

Tactic:
⟨a, .inl e.symm⟩

Premises used: Exists.intro, Or.inl, Eq.symm
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : IsDomain 𝒪
inst_4 : ValuationRing 𝒪
h : IsFractionRing 𝒪 K
x : K
a : 𝒪
e : (algebraMap 𝒪 K : (a : 𝒪) → K) a = x⁻¹
⊢ ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a

Tactic:
⟨a, .inr e.symm⟩

Premises used: Exists.intro, Eq.symm, Or.inr
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : IsDomain 𝒪
inst_4 : ValuationRing 𝒪
h : IsFractionRing 𝒪 K
x : K
a : 𝒪
e : (algebraMap 𝒪 K : (a : 𝒪) → K) a = x
⊢ ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a

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