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
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})
x y : R
e' : x * (a * g) + y * (b * g) = g
inl : ∀ (h : g = 0), a * g ∣ b * g ∨ b * g ∣ a * g
inr : ∀ (h : g ≠ 0), a * g ∣ b * g ∨ b * g ∣ a * g
⊢ a * g ∣ b * g ∨ b * g ∣ a * g

Tactic:
rcases eq_or_ne g 0 with h | h

Premises used: eq_or_ne, 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
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})
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g = 0
⊢ a * g ∣ b * g ∨ b * g ∣ a * g

Tactic:
simp [h]
-- 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})
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
a₁ : Eq.{u_1 + 1} (α := R) ((fun (a : R) ↦ a * g) (x * a + y * b)) ((fun (a : R) ↦ a * g) 1)
⊢ x * a + y * b = 1

Tactic:
apply mul_left_injective₀ h

Premises used: mul_left_injective₀
-- 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})
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
⊢ x * (a * g) + y * (b * g) = g

Tactic:
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})
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
h₁ : (fun (a : R) ↦ a * g) (x * a + y * b) = x * (a * g) + y * (b * g)
h₂ : (fun (a : R) ↦ a * g) 1 = g
⊢ Eq.{u_1 + 1} (α := R) ((fun (a : R) ↦ a * g) (x * a + y * b)) ((fun (a : R) ↦ a * g) 1)

Tactic:
convert! e' using 1
-- 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})
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
⊢ (fun (a : R) ↦ a * g) (x * a + y * b) = x * (a * g) + y * (b * g)

Tactic:
ring
-- 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})
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
⊢ (fun (a : R) ↦ a * g) 1 = g

Tactic:
ring
-- 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})
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
⊢ x * a + y * b = 1

Tactic:
have : x * a + y * b = 1 := by
    apply mul_left_injective₀ h; convert! e' using 1 <;> ring
-- 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})
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
inr : ∀ (h' : IsUnit (x * a)), a * g ∣ b * g ∨ b * g ∣ a * g
inr₁ : ∀ (h' : IsUnit (y * b)), a * g ∣ b * g ∨ b * g ∣ a * g
⊢ a * g ∣ b * g ∨ b * g ∣ a * g

Tactic:
rcases IsLocalRing.isUnit_or_isUnit_of_add_one this with h' | h'

Premises used: IsLocalRing.isUnit_or_isUnit_of_add_one
-- 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})
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
h' : IsUnit (x * a)
inr : a * g ∣ b * g
⊢ a * g ∣ b * g ∨ b * g ∣ a * g

Tactic:
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 : IsLocalRing R
inst_6 : IsBezout R
g a b : R
e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
h' : IsUnit (y * b)
inr : b * g ∣ a * g
⊢ a * g ∣ b * g ∨ b * g ∣ a * g

Tactic:
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 : IsLocalRing R
inst_6 : IsBezout R
g a b : R
e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
inr : ∀ (h' : IsUnit (x * a)), a * g ∣ b * g
inr₁ : ∀ (h' : IsUnit (y * b)), b * g ∣ a * g
⊢ a * g ∣ b * g ∨ b * g ∣ a * g

Tactic:
rcases IsLocalRing.isUnit_or_isUnit_of_add_one this with h' | h' <;> [left; right]

Premises used: IsLocalRing.isUnit_or_isUnit_of_add_one
-- 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})
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
h' : IsUnit (x * a)
⊢ a * g ∣ b * g

Tactic:
mul_dvd_mul_right (isUnit_iff_forall_dvd.mp (isUnit_of_mul_isUnit_right h') _) _

Premises used: mul_dvd_mul_right, isUnit_of_mul_isUnit_right, Iff.mp, isUnit_iff_forall_dvd
-- 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})
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
h' : IsUnit (x * a)
⊢ a * g ∣ b * g

Tactic:
exact mul_dvd_mul_right (isUnit_iff_forall_dvd.mp (isUnit_of_mul_isUnit_right h') _) _

Premises used: mul_dvd_mul_right, isUnit_of_mul_isUnit_right, Iff.mp, isUnit_iff_forall_dvd
-- 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})
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
h' : IsUnit (y * b)
⊢ b * g ∣ a * g

Tactic:
mul_dvd_mul_right (isUnit_iff_forall_dvd.mp (isUnit_of_mul_isUnit_right h') _) _

Premises used: mul_dvd_mul_right, isUnit_of_mul_isUnit_right, Iff.mp, isUnit_iff_forall_dvd
-- 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})
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
h' : IsUnit (y * b)
⊢ b * g ∣ a * g

Tactic:
exact mul_dvd_mul_right (isUnit_iff_forall_dvd.mp (isUnit_of_mul_isUnit_right h') _) _

Premises used: mul_dvd_mul_right, isUnit_of_mul_isUnit_right, Iff.mp, isUnit_iff_forall_dvd
-- 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
refine₁ : ∀ (a b g : R) (e : Eq (α := Ideal R) (Ideal.span {a, b}) (Ideal.span {g})), a ∣ b ∨ b ∣ a
refine₂ : ∀ (b g a : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b}) (Ideal.span {g})), a * g ∣ b ∨ b ∣ a * g
refine₃ :
  ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})), a * g ∣ b * g ∨ b * g ∣ a * g
refine₄ :
  ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})) (x y : R)
    (e' : x * (a * g) + y * (b * g) = g), a * g ∣ b * g ∨ b * g ∣ a * g
inl :
  ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})) (x y : R)
    (e' : x * (a * g) + y * (b * g) = g) (h : g = 0), a * g ∣ b * g ∨ b * g ∣ a * g
inr inr₁ :
  ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})) (x y : R)
    (e' : x * (a * g) + y * (b * g) = g) (h : g ≠ 0), a * g ∣ b * g ∨ b * g ∣ a * g
inr₂ :
  ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})) (x y : R)
    (e' : x * (a * g) + y * (b * g) = g) (h : g ≠ 0) (this : x * a + y * b = 1), a * g ∣ b * g ∨ b * g ∣ a * g
inr₃ :
  ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})) (x y : R)
    (e' : x * (a * g) + y * (b * g) = g) (h : g ≠ 0) (this : x * a + y * b = 1) (h' : IsUnit (x * a)), a * g ∣ b * g
inr₄ :
  ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})) (x y : R)
    (e' : x * (a * g) + y * (b * g) = g) (h : g ≠ 0) (this : x * a + y * b = 1) (h' : IsUnit (y * b)), b * g ∣ a * g
⊢ ValuationRing R

Tactic:
classical
  refine iff_dvd_total.mpr ⟨fun a b => ?_⟩
  obtain ⟨g, e : _ = Ideal.span _⟩ := IsBezout.span_pair_isPrincipal a b
  obtain ⟨a, rfl⟩ := Ideal.mem_span_singleton'.mp
      (show a ∈ Ideal.span {g} by rw [← e]; exact Ideal.subset_span (by simp))
  obtain ⟨b, rfl⟩ := Ideal.mem_span_singleton'.mp
      (show b ∈ Ideal.span {g} by rw [← e]; exact Ideal.subset_span (by simp))
  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))
  rcases eq_or_ne g 0 with h | h
  · simp [h]
  have : x * a + y * b = 1 := by
    apply mul_left_injective₀ h; convert! e' using 1 <;> ring
  rcases IsLocalRing.isUnit_or_isUnit_of_add_one this with h' | h' <;> [left; right]
  all_goals exact mul_dvd_mul_right (isUnit_iff_forall_dvd.mp (isUnit_of_mul_isUnit_right h') _) _

Premises used: Iff.mpr, Ideal.span, Std.Total.mk, ValuationRing.iff_dvd_total, rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
⊢ ValuationRing R ↔ IsLocalRing R ∧ IsBezout R

Tactic:
⟨fun _ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ ↦ inferInstance⟩

Premises used: _private.0.ValuationRing.iff_local_bezout_domain.match_1, inferInstance, And.intro, Iff.intro, ValuationRing
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
⊢ ValuationRing R

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
⊢ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
⊢ ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹

Tactic:
1 ↔ 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
⊢ ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹

Tactic:
tfae_have 1 ↔ 2 := iff_isInteger_or_isInteger R _

Premises used: ValuationRing.iff_isInteger_or_isInteger
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
⊢ ValuationRing R

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
⊢ Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
⊢ ValuationRing R ↔ Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2

Tactic:
1 ↔ 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
⊢ ValuationRing R ↔ Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2

Tactic:
tfae_have 1 ↔ 3 := iff_dvd_total

Premises used: ValuationRing.iff_dvd_total
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
tfae_1_iff_3 : ValuationRing R ↔ Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2
⊢ ValuationRing R

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
tfae_1_iff_3 : ValuationRing R ↔ Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2
⊢ Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
tfae_1_iff_3 : ValuationRing R ↔ Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2
⊢ ValuationRing R ↔ Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2

Tactic:
1 ↔ 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
tfae_1_iff_3 : ValuationRing R ↔ Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2
⊢ ValuationRing R ↔ Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2

Tactic:
tfae_have 1 ↔ 4 := iff_ideal_total

Premises used: ValuationRing.iff_ideal_total
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
tfae_1_iff_3 : ValuationRing R ↔ Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2
tfae_1_iff_4 : ValuationRing R ↔ Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2
⊢ ValuationRing R

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
tfae_1_iff_3 : ValuationRing R ↔ Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2
tfae_1_iff_4 : ValuationRing R ↔ Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2
⊢ IsLocalRing R ∧ IsBezout R

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
tfae_1_iff_3 : ValuationRing R ↔ Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2
tfae_1_iff_4 : ValuationRing R ↔ Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2
⊢ ValuationRing R ↔ IsLocalRing R ∧ IsBezout R

Tactic:
1 ↔ 5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
tfae_1_iff_3 : ValuationRing R ↔ Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2
tfae_1_iff_4 : ValuationRing R ↔ Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2
⊢ ValuationRing R ↔ IsLocalRing R ∧ IsBezout R

Tactic:
tfae_have 1 ↔ 5 := iff_local_bezout_domain

Premises used: ValuationRing.iff_local_bezout_domain
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
tfae_1_iff_3 : ValuationRing R ↔ Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2
tfae_1_iff_4 : ValuationRing R ↔ Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2
tfae_1_iff_5 : ValuationRing R ↔ IsLocalRing R ∧ IsBezout R
⊢ [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2, Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2, IsLocalRing R ∧ IsBezout R].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
S : Type u_2
inst : Mul R
inst_1 : PreValuationRing R
inst_2 : Mul S
f : R →ₙ* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
a b : S
obtain :
  ∀ (a b : R),
    ∃ (c : S),
      HMul.hMul (α := S) ((f : (a : R) → S) a : S) c = (f : (a : R) → S) b ∨
        HMul.hMul (α := S) ((f : (a : R) → S) b : S) c = (f : (a : R) → S) a
⊢ ∃ (c : S), a * c = b ∨ b * c = a

Tactic:
obtain ⟨⟨a, rfl⟩, ⟨b, rfl⟩⟩ := hf a, hf b

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
S : Type u_2
inst : Mul R
inst_1 : PreValuationRing R
inst_2 : Mul S
f : R →ₙ* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
a b : R
inl :
  ∀ (c : R),
    ∃ (c_1 : S),
      HMul.hMul (α := S) ((f : (a : R) → S) a : S) c_1 = (f : (a : R) → S) (a * c) ∨
        HMul.hMul (α := S) ((f : (a : R) → S) (a * c) : S) c_1 = (f : (a : R) → S) a
inr :
  ∀ (c : R),
    ∃ (c_1 : S),
      HMul.hMul (α := S) ((f : (a : R) → S) (b * c) : S) c_1 = (f : (a : R) → S) b ∨
        HMul.hMul (α := S) ((f : (a : R) → S) b : S) c_1 = (f : (a : R) → S) (b * c)
⊢ ∃ (c : S),
    HMul.hMul (α := S) ((f : (a : R) → S) a : S) c = (f : (a : R) → S) b ∨
      HMul.hMul (α := S) ((f : (a : R) → S) b : S) c = (f : (a : R) → S) a

Tactic:
obtain ⟨c, rfl | rfl⟩ := PreValuationRing.cond a b

Premises used: PreValuationRing.cond, rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
S : Type u_2
inst : Mul R
inst_1 : PreValuationRing R
inst_2 : Mul S
f : R →ₙ* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
a c : R
⊢ ∃ (c_1 : S),
    HMul.hMul (α := S) ((f : (a : R) → S) a : S) c_1 = (f : (a : R) → S) (a * c) ∨
      HMul.hMul (α := S) ((f : (a : R) → S) (a * c) : S) c_1 = (f : (a : R) → S) a

Tactic:
⟨f c, Or.inl <| (map_mul _ _ _).symm⟩

Premises used: map_mul, Exists.intro, Or.inl, Eq.symm, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
S : Type u_2
inst : Mul R
inst_1 : PreValuationRing R
inst_2 : Mul S
f : R →ₙ* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
b c : R
⊢ ∃ (c_1 : S),
    HMul.hMul (α := S) ((f : (a : R) → S) (b * c) : S) c_1 = (f : (a : R) → S) b ∨
      HMul.hMul (α := S) ((f : (a : R) → S) b : S) c_1 = (f : (a : R) → S) (b * c)

Tactic:
⟨f c, Or.inr <| (map_mul _ _ _).symm⟩

Premises used: map_mul, Exists.intro, Eq.symm, DFunLike.coe, Or.inr
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
S : Type u_2
inst : Mul R
inst_1 : PreValuationRing R
inst_2 : Mul S
f : R →ₙ* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
a c : R
⊢ ∃ (c_1 : S),
    HMul.hMul (α := S) ((f : (a : R) → S) a : S) c_1 = (f : (a : R) → S) (a * c) ∨
      HMul.hMul (α := S) ((f : (a : R) → S) (a * c) : S) c_1 = (f : (a : R) → S) a

Tactic:
exacts [⟨f c, Or.inl <| (map_mul _ _ _).symm⟩, ⟨f c, Or.inr <| (map_mul _ _ _).symm⟩]
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : PreValuationRing R
inst_2 : CommRing S
inst_3 : IsDomain S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ ValuationRing S

Tactic:
have : PreValuationRing S := Function.Surjective.preValuationRing (R := R) f hf
  .mk

Premises used: MulHomClass.toMulHom, Function.Surjective.preValuationRing, ValuationRing.mk
-- 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)
⊢ IsDomain 𝒪

Tactic:
have : IsDomain 𝒪 := hinj.isDomain
-- 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 : IsDomain 𝒪
⊢ FaithfulSMul 𝒪 K

Tactic:
have := (faithfulSMul_iff_algebraMap_injective ..).2 hinj
-- 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 : FaithfulSMul 𝒪 K
⊢ IsDomain 𝒪

Tactic:
have := IsDomain.of_faithfulSMul 𝒪 K
-- 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 𝒪
⊢ ∀ (y : ↥(nonZeroDivisors 𝒪 : Submonoid 𝒪)), IsUnit.{v} (M := K) ((algebraMap 𝒪 K : (a : 𝒪) → K) (↑y : 𝒪) : K)

Tactic:
simp