awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
H : ValuationRing R
y : R
hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y
this : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) y : K) (0 : K)
s : R
rwa :
  HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) s : K) ((algebraMap R K : (a : R) → K) y : K) =
    (algebraMap R K : (a : R) → K) (y * s)
rwa₁ : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) y : K) (0 : K)
rwa₂ :
  HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) s : K) ((algebraMap R K : (a : R) → K) y : K) =
    HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) y : K) ((algebraMap R K : (a : R) → K) s : K)
rwa₃ : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) y : K) (0 : K)
rwa₄ :
  HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) y : K) ((algebraMap R K : (a : R) → K) s : K) =
    HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) y : K) ((algebraMap R K : (a : R) → K) s : K)
rwa₅ : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) y : K) (0 : K)
rwa₆ :
  HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) y : K) ((algebraMap R K : (a : R) → K) s : K) =
    HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) y : K) ((algebraMap R K : (a : R) → K) s : K)
rwa₇ rwa₈ rwa₉ : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) y : K) (0 : K)
⊢ (algebraMap R K : (a : R) → K) s =
    HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) (y * s) : K) ((algebraMap R K : (a : R) → K) y : K)

Tactic:
rwa [eq_div_iff, map_mul, mul_comm]

Premises used: map_mul, mul_comm, eq_div_iff
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
H : ValuationRing R
y : R
hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y
this : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) y : K) (0 : K)
s : R
⊢ IsLocalization.IsInteger R
      (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) (y * s) : K)
        ((algebraMap R K : (a : R) → K) y : K)) ∨
    IsLocalization.IsInteger R
      (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) (y * s) : K)
          ((algebraMap R K : (a : R) → K) y : K))⁻¹

Tactic:
exact Or.inl ⟨s, by rwa [eq_div_iff, map_mul, mul_comm]⟩

Premises used: Or.inl
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
mpr : PreValuationRing R
⊢ ValuationRing R

Tactic:
suffices PreValuationRing R from mk
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
mpr : ∀ (a b : R), ∃ (c : R), a * c = b ∨ b * c = a
⊢ PreValuationRing R

Tactic:
constructor
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
pos : ∀ (ha : a = 0), ∃ (c : R), a * c = b ∨ b * c = a
neg : ∀ (ha : ¬a = 0), ∃ (c : R), a * c = b ∨ b * c = a
⊢ ∃ (c : R), a * c = b ∨ b * c = a

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : a = 0
pos : ∃ (c : R), 0 * c = b ∨ b * c = 0
⊢ ∃ (c : R), a * c = b ∨ b * c = a

Tactic:
subst ha
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
b : R
⊢ ∃ (c : R), 0 * c = b ∨ b * c = 0

Tactic:
⟨0, Or.inr <| mul_zero b⟩

Premises used: MulZeroClass.mul_zero, Exists.intro, OfNat.ofNat, Or.inr
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
b : R
⊢ ∃ (c : R), 0 * c = b ∨ b * c = 0

Tactic:
exact ⟨0, Or.inr <| mul_zero b⟩
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : ¬a = 0
pos : ∀ (hb : b = 0), ∃ (c : R), a * c = b ∨ b * c = a
neg : ∀ (hb : ¬b = 0), ∃ (c : R), a * c = b ∨ b * c = a
⊢ ∃ (c : R), a * c = b ∨ b * c = a

Tactic:
by_cases hb : b = 0
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : ¬a = 0
hb : b = 0
pos : ∃ (c : R), a * c = 0 ∨ 0 * c = a
⊢ ∃ (c : R), a * c = b ∨ b * c = a

Tactic:
subst hb
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a : R
ha : ¬a = 0
⊢ ∃ (c : R), a * c = 0 ∨ 0 * c = a

Tactic:
⟨0, Or.inl <| mul_zero a⟩

Premises used: MulZeroClass.mul_zero, Exists.intro, Or.inl, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a : R
ha : ¬a = 0
⊢ ∃ (c : R), a * c = 0 ∨ 0 * c = a

Tactic:
exact ⟨0, Or.inl <| mul_zero a⟩
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : ¬a = 0
hb : ¬b = 0
⊢ Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)

Tactic:
replace ha := (map_ne_zero_iff _ (IsFractionRing.injective R K)).mpr ha
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
hb : ¬b = 0
ha : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
⊢ Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) b : K) (0 : K)

Tactic:
replace hb := (map_ne_zero_iff _ (IsFractionRing.injective R K)).mpr hb
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
hb : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) b : K) (0 : K)
neg :
  ∀ (c : R)
    (e :
      (algebraMap R K : (a : R) → K) c =
        HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) a : K) ((algebraMap R K : (a : R) → K) b : K)),
    ∃ (c : R), a * c = b ∨ b * c = a
neg₁ :
  ∀ (c : R)
    (e :
      (algebraMap R K : (a : R) → K) c =
        (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) a : K) ((algebraMap R K : (a : R) → K) b : K))⁻¹),
    ∃ (c : R), a * c = b ∨ b * c = a
⊢ ∃ (c : R), a * c = b ∨ b * c = a

Tactic:
obtain ⟨c, e⟩ | ⟨c, e⟩ := H (algebraMap R K a / algebraMap R K b)

Premises used: Algebra.algebraMap, HDiv.hDiv, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
hb : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) b : K) (0 : K)
c : R
e :
  (algebraMap R K : (a : R) → K) c =
    HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) a : K) ((algebraMap R K : (a : R) → K) b : K)
⊢ b * c = a

Tactic:
rw [eq_div_iff hb, ← map_mul, (IsFractionRing.injective R K).eq_iff, mul_comm] at e

Premises used: IsFractionRing.injective, Function.Injective.eq_iff, map_mul, mul_comm, eq_div_iff
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
hb : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) b : K) (0 : K)
c : R
e : b * c = a
⊢ ∃ (c : R), a * c = b ∨ b * c = a

Tactic:
⟨c, Or.inr e⟩

Premises used: Exists.intro, Or.inr
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
hb : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) b : K) (0 : K)
c : R
e : b * c = a
⊢ ∃ (c : R), a * c = b ∨ b * c = a

Tactic:
exact ⟨c, Or.inr e⟩
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
hb : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) b : K) (0 : K)
c : R
e :
  (algebraMap R K : (a : R) → K) c =
    (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) a : K) ((algebraMap R K : (a : R) → K) b : K))⁻¹
⊢ a * c = b

Tactic:
rw [inv_div, eq_div_iff ha, ← map_mul, (IsFractionRing.injective R K).eq_iff, mul_comm c] at e

Premises used: IsFractionRing.injective, Function.Injective.eq_iff, map_mul, mul_comm, inv_div, eq_div_iff
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
hb : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) b : K) (0 : K)
c : R
e : a * c = b
⊢ ∃ (c : R), a * c = b ∨ b * c = a

Tactic:
⟨c, Or.inl e⟩

Premises used: Exists.intro, Or.inl
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
hb : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) b : K) (0 : K)
c : R
e : a * c = b
⊢ ∃ (c : R), a * c = b ∨ b * c = a

Tactic:
exact ⟨c, Or.inl e⟩
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
h : ValuationRing R
x : K
⊢ IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹

Tactic:
(iff_isInteger_or_isInteger R K).mp h x

Premises used: ValuationRing.iff_isInteger_or_isInteger, Iff.mp
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : ValuationRing R
rw : ∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})
⊢ IsBezout R

Tactic:
rw [IsBezout.iff_span_pair_isPrincipal]

Premises used: IsBezout.iff_span_pair_isPrincipal
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : ValuationRing R
x y : R
rw : Submodule.IsPrincipal (R := R) (max (Ideal.span {x}) (Ideal.span {y}))
⊢ Submodule.IsPrincipal (R := R) (Ideal.span {x, y})

Tactic:
rw [Ideal.span_insert]

Premises used: Ideal.span_insert
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : ValuationRing R
x y : R
inl :
  ∀ (h : LE.le (α := Ideal R) (Ideal.span {x}) (Ideal.span {y})),
    Submodule.IsPrincipal (R := R) (max (Ideal.span {x}) (Ideal.span {y}))
inr :
  ∀ (h : LE.le (α := Ideal R) (Ideal.span {y}) (Ideal.span {x})),
    Submodule.IsPrincipal (R := R) (max (Ideal.span {x}) (Ideal.span {y}))
⊢ Submodule.IsPrincipal (R := R) (max (Ideal.span {x}) (Ideal.span {y}))

Tactic:
rcases le_total (Ideal.span {x} : Ideal R) (Ideal.span {y}) with h | h

Premises used: le_total, Ideal.span, Singleton.singleton
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : ValuationRing R
x y : R
h : LE.le (α := Ideal R) (Ideal.span {x}) (Ideal.span {y})
inl : Submodule.IsPrincipal (R := R) (Ideal.span {y})
⊢ Submodule.IsPrincipal (R := R) (max (Ideal.span {x}) (Ideal.span {y}))

Tactic:
rw [sup_eq_right.mpr h]

Premises used: Iff.mpr, sup_eq_right
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : ValuationRing R
x y : R
h : LE.le (α := Ideal R) (Ideal.span {x}) (Ideal.span {y})
⊢ Submodule.IsPrincipal (R := R) (Ideal.span {y})

Tactic:
⟨⟨_, rfl⟩⟩

Premises used: Submodule.IsPrincipal.mk, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : ValuationRing R
x y : R
h : LE.le (α := Ideal R) (Ideal.span {x}) (Ideal.span {y})
⊢ Submodule.IsPrincipal (R := R) (Ideal.span {y})

Tactic:
exact ⟨⟨_, rfl⟩⟩
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : ValuationRing R
x y : R
h : LE.le (α := Ideal R) (Ideal.span {y}) (Ideal.span {x})
inr : Submodule.IsPrincipal (R := R) (Ideal.span {x})
⊢ Submodule.IsPrincipal (R := R) (max (Ideal.span {x}) (Ideal.span {y}))

Tactic:
rw [sup_eq_left.mpr h]

Premises used: Iff.mpr, sup_eq_left
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : ValuationRing R
x y : R
h : LE.le (α := Ideal R) (Ideal.span {y}) (Ideal.span {x})
⊢ Submodule.IsPrincipal (R := R) (Ideal.span {x})

Tactic:
⟨⟨_, rfl⟩⟩

Premises used: Submodule.IsPrincipal.mk, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : ValuationRing R
x y : R
h : LE.le (α := Ideal R) (Ideal.span {y}) (Ideal.span {x})
⊢ Submodule.IsPrincipal (R := R) (Ideal.span {x})

Tactic:
exact ⟨⟨_, rfl⟩⟩
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : ValuationRing R
rw rw₁ rw₂ rw₃ : ∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})
rw₄ : ∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x} ⊔ Ideal.span {y})
inl :
  ∀ (x y : R) (h : LE.le (α := Ideal R) (Ideal.span {x}) (Ideal.span {y})),
    Submodule.IsPrincipal (R := R) (Ideal.span {x} ⊔ Ideal.span {y})
inr inr₁ :
  ∀ (x y : R) (h : LE.le (α := Ideal R) (Ideal.span {y}) (Ideal.span {x})),
    Submodule.IsPrincipal (R := R) (Ideal.span {x} ⊔ Ideal.span {y})
⊢ IsBezout R

Tactic:
classical
  rw [IsBezout.iff_span_pair_isPrincipal]
  intro x y
  rw [Ideal.span_insert]
  rcases le_total (Ideal.span {x} : Ideal R) (Ideal.span {y}) with h | h
  · rw [sup_eq_right.mpr h]; exact ⟨⟨_, rfl⟩⟩
  · rw [sup_eq_left.mpr h]; exact ⟨⟨_, rfl⟩⟩

Premises used: IsBezout.iff_span_pair_isPrincipal, Ideal.span_insert
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : IsLocalRing R
inst_6 : IsBezout R
⊢ ValuationRing R

Tactic:
iff_dvd_total.mpr ⟨fun a b => ?_⟩

Premises used: Iff.mpr, Std.Total.mk, ValuationRing.iff_dvd_total
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : IsLocalRing R
inst_6 : IsBezout R
refine : ∀ (a b : R), a ∣ b ∨ b ∣ a
⊢ ValuationRing R

Tactic:
refine iff_dvd_total.mpr ⟨fun a b => ?_⟩

Premises used: Iff.mpr, Std.Total.mk, ValuationRing.iff_dvd_total
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : IsLocalRing R
inst_6 : IsBezout R
a b : R
obtain : ∀ (g : R) (e : Eq (α := Ideal R) (Ideal.span {a, b}) (Ideal.span {g})), a ∣ b ∨ b ∣ a
⊢ a ∣ b ∨ b ∣ a

Tactic:
obtain ⟨g, e : _ = Ideal.span _⟩ := IsBezout.span_pair_isPrincipal a b

Premises used: Ideal.span, IsBezout.span_pair_isPrincipal
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : IsLocalRing R
inst_6 : IsBezout R
a b g : R
e : Eq (α := Ideal R) (Ideal.span {a, b}) (Ideal.span {g})
rw : Membership.mem (γ := Ideal R) (Ideal.span {a, b}) a
⊢ Membership.mem (γ := Ideal R) (Ideal.span {g}) a

Tactic:
rw [← e]
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : IsLocalRing R
inst_6 : IsBezout R
a b g : R
e : Eq (α := Ideal R) (Ideal.span {a, b}) (Ideal.span {g})
⊢ Membership.mem (γ := Set R) {a, b} a

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : IsLocalRing R
inst_6 : IsBezout R
a b g : R
e : Eq (α := Ideal R) (Ideal.span {a, b}) (Ideal.span {g})
⊢ Membership.mem (γ := Ideal R) (Ideal.span {a, b}) a

Tactic:
exact Ideal.subset_span (by simp)

Premises used: Ideal.subset_span
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : IsLocalRing R
inst_6 : IsBezout R
a b g : R
e : Eq (α := Ideal R) (Ideal.span {a, b}) (Ideal.span {g})
obtain : ∀ (a : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b}) (Ideal.span {g})), a * g ∣ b ∨ b ∣ a * g
⊢ a ∣ b ∨ b ∣ a

Tactic:
obtain ⟨a, rfl⟩ := Ideal.mem_span_singleton'.mp
      (show a ∈ Ideal.span {g} by rw [← e]; exact Ideal.subset_span (by simp))

Premises used: Ideal.mem_span_singleton', Iff.mp, rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : IsLocalRing R
inst_6 : IsBezout R
b g a : R
e : Eq (α := Ideal R) (Ideal.span {a * g, b}) (Ideal.span {g})
rw : Membership.mem (γ := Ideal R) (Ideal.span {a * g, b}) b
⊢ Membership.mem (γ := Ideal R) (Ideal.span {g}) b

Tactic:
rw [← e]
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : IsLocalRing R
inst_6 : IsBezout R
b g a : R
e : Eq (α := Ideal R) (Ideal.span {a * g, b}) (Ideal.span {g})
⊢ Membership.mem (γ := Set R) {a * g, b} b

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : IsLocalRing R
inst_6 : IsBezout R
b g a : R
e : Eq (α := Ideal R) (Ideal.span {a * g, b}) (Ideal.span {g})
⊢ Membership.mem (γ := Ideal R) (Ideal.span {a * g, b}) b

Tactic:
exact Ideal.subset_span (by simp)

Premises used: Ideal.subset_span
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : IsLocalRing R
inst_6 : IsBezout R
b g a : R
e : Eq (α := Ideal R) (Ideal.span {a * g, b}) (Ideal.span {g})
obtain : ∀ (b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})), a * g ∣ b * g ∨ b * g ∣ a * g
⊢ a * g ∣ b ∨ b ∣ a * g

Tactic:
obtain ⟨b, rfl⟩ := Ideal.mem_span_singleton'.mp
      (show b ∈ Ideal.span {g} by rw [← e]; exact Ideal.subset_span (by simp))

Premises used: Ideal.mem_span_singleton', Iff.mp, rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : IsLocalRing R
inst_6 : IsBezout R
g a b : R
e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})
rw : Membership.mem (γ := Ideal R) (Ideal.span {g}) g
⊢ Membership.mem (γ := Ideal R) (Ideal.span {a * g, b * g}) g

Tactic:
rw [e]
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : IsLocalRing R
inst_6 : IsBezout R
g a b : R
e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})
⊢ Membership.mem (γ := Set R) {g} g

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : IsLocalRing R
inst_6 : IsBezout R
g a b : R
e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})
⊢ Membership.mem (γ := Ideal R) (Ideal.span {g}) g

Tactic:
exact Ideal.subset_span (by simp)

Premises used: Ideal.subset_span
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : IsLocalRing R
inst_6 : IsBezout R
g a b : R
e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})
obtain : ∀ (x y : R) (e' : x * (a * g) + y * (b * g) = g), a * g ∣ b * g ∨ b * g ∣ a * g
⊢ a * g ∣ b * g ∨ b * g ∣ a * g

Tactic:
obtain ⟨x, y, e'⟩ := Ideal.mem_span_pair.mp
      (show g ∈ Ideal.span {a * g, b * g} by rw [e]; exact Ideal.subset_span (by simp))

Premises used: Iff.mp, Ideal.mem_span_pair