awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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
⊢ Submodule.IsPrincipal (R := R) (max (Ideal.span {x}) (Ideal.span {y}))
have inl : ∀ (h : LE.le (α := Ideal R) (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
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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}))
⊢ Submodule.IsPrincipal (R := R) (max (Ideal.span {x}) (Ideal.span {y}))
have inr : ∀ (h : LE.le (α := Ideal R) (Ideal.span {y}) (Ideal.span {x})),
  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
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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) (max (Ideal.span {x}) (Ideal.span {y}))
have inl : Submodule.IsPrincipal (R := R) (Ideal.span {y})
Tactic: rw [sup_eq_right.mpr h]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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) (max (Ideal.span {x}) (Ideal.span {y}))
have inr : Submodule.IsPrincipal (R := R) (Ideal.span {x})
Tactic: rw [sup_eq_left.mpr h]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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
⊢ IsBezout R
have rw : ∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})
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⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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})
⊢ IsBezout R
have rw₄ : ∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x} ⊔ Ideal.span {y})
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⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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})
⊢ IsBezout R
have 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})
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⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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})
⊢ IsBezout R
have 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})
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⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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
have refine : ∀ (a b : R), a ∣ b ∨ b ∣ a
Tactic: refine iff_dvd_total.mpr ⟨fun a b => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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
⊢ a ∣ b ∨ b ∣ a
have obtain : ∀ (g : R) (e : Eq (α := Ideal R) (Ideal.span {a, b}) (Ideal.span {g})), a ∣ b ∨ b ∣ a
Tactic: obtain ⟨g, e : _ = Ideal.span _⟩ := IsBezout.span_pair_isPrincipal a b
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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 {g}) a
have rw : Membership.mem (γ := Ideal R) (Ideal.span {a, b}) a
Tactic: rw [← e]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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})
⊢ a ∣ b ∨ b ∣ a
have obtain : ∀ (a : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b}) (Ideal.span {g})), a * g ∣ b ∨ b ∣ a * g
Tactic: obtain ⟨a, rfl⟩ := Ideal.mem_span_singleton'.mp
      (show a ∈ Ideal.span {g} by rw [← e]; exact Ideal.subset_span (by simp))
Cleared hypotheses: a, e
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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 {g}) b
have rw : Membership.mem (γ := Ideal R) (Ideal.span {a * g, b}) b
Tactic: rw [← e]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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})
⊢ a * g ∣ b ∨ b ∣ a * g
have obtain : ∀ (b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})), a * g ∣ b * g ∨ b * g ∣ 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))
Cleared hypotheses: b, e
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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 {a * g, b * g}) g
have rw : Membership.mem (γ := Ideal R) (Ideal.span {g}) g
Tactic: rw [e]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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})
⊢ a * g ∣ b * g ∨ b * g ∣ a * g
have obtain : ∀ (x y : R) (e' : x * (a * g) + y * (b * g) = 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))
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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
⊢ a * g ∣ b * g ∨ b * g ∣ a * g
have inl : ∀ (h : g = 0), a * g ∣ b * g ∨ b * g ∣ a * g
Tactic: rcases eq_or_ne g 0 with h | h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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
⊢ a * g ∣ b * g ∨ b * g ∣ a * g
have inr : ∀ (h : g ≠ 0), a * g ∣ b * g ∨ b * g ∣ a * g
Tactic: rcases eq_or_ne g 0 with h | h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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
have a₁ : Eq.{u_1 + 1} (α := R) ((fun (a : R) ↦ a * g) (x * a + y * b)) ((fun (a : R) ↦ a * g) 1)
Tactic: apply mul_left_injective₀ h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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
⊢ Eq.{u_1 + 1} (α := R) ((fun (a : R) ↦ a * g) (x * a + y * b)) ((fun (a : R) ↦ a * g) 1)
have h₁ : (fun (a : R) ↦ a * g) (x * a + y * b) = x * (a * g) + y * (b * g)
Tactic: convert! e' using 1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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)
⊢ Eq.{u_1 + 1} (α := R) ((fun (a : R) ↦ a * g) (x * a + y * b)) ((fun (a : R) ↦ a * g) 1)
have h₂ : (fun (a : R) ↦ a * g) 1 = g
Tactic: convert! e' using 1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (hypothesis)
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
have this : x * a + y * b = 1
Tactic: have : x * a + y * b = 1 := by
    apply mul_left_injective₀ h; convert! e' using 1 <;> ring
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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
⊢ a * g ∣ b * g ∨ b * g ∣ a * g
have inr : ∀ (h' : IsUnit (x * a)), a * g ∣ b * g ∨ b * g ∣ a * g
Tactic: rcases IsLocalRing.isUnit_or_isUnit_of_add_one this with h' | h'
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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
⊢ a * g ∣ b * g ∨ b * g ∣ a * g
have inr₁ : ∀ (h' : IsUnit (y * b)), a * g ∣ b * g ∨ b * g ∣ a * g
Tactic: rcases IsLocalRing.isUnit_or_isUnit_of_add_one this with h' | h'
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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 ∨ b * g ∣ a * g
have inr : a * g ∣ b * g
Tactic: left
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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)
⊢ a * g ∣ b * g ∨ b * g ∣ a * g
have inr : b * g ∣ a * g
Tactic: right
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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
⊢ a * g ∣ b * g ∨ b * g ∣ a * g
have inr : ∀ (h' : IsUnit (x * a)), a * g ∣ b * g
Tactic: rcases IsLocalRing.isUnit_or_isUnit_of_add_one this with h' | h' <;> [left; right]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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
⊢ a * g ∣ b * g ∨ b * g ∣ a * g
have inr₁ : ∀ (h' : IsUnit (y * b)), b * g ∣ a * g
Tactic: rcases IsLocalRing.isUnit_or_isUnit_of_add_one this with h' | h' <;> [left; right]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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
have refine : ∀ (a b : R), a ∣ b ∨ b ∣ a
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') _) _
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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
have refine₁ : ∀ (a b g : R) (e : Eq (α := Ideal R) (Ideal.span {a, b}) (Ideal.span {g})), a ∣ b ∨ b ∣ a
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') _) _
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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
⊢ ValuationRing R
have refine₂ : ∀ (b g a : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b}) (Ideal.span {g})), a * g ∣ b ∨ b ∣ a * g
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') _) _
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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
⊢ ValuationRing R
have 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
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') _) _
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
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
⊢ ValuationRing R
have 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
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') _) _