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
refine : ∀ (H : Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) (a b : R), a ∣ b ∨ b ∣ a
⊢ PreValuationRing R ↔ Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2
have refine₁ : ∀ (H : Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) (a b : R)
  (this :
    LE.le (α := Ideal R) (Ideal.span {a}) (Ideal.span {b}) ∨ LE.le (α := Ideal R) (Ideal.span {b}) (Ideal.span {a})),
  a ∣ b ∨ b ∣ a
Tactic: classical
  refine ⟨fun _ => ⟨le_total⟩, fun H => PreValuationRing.iff_dvd_total.mpr ⟨fun a b => ?_⟩⟩
  have := H.total (Ideal.span {a}) (Ideal.span {b})
  simp_rw [Ideal.span_singleton_le_span_singleton] at this
  exact this.symm
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
refine : ∀ (H : Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) (a b : R), a ∣ b ∨ b ∣ a
refine₁ :
  ∀ (H : Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) (a b : R)
    (this :
      LE.le (α := Ideal R) (Ideal.span {a}) (Ideal.span {b}) ∨ LE.le (α := Ideal R) (Ideal.span {b}) (Ideal.span {a})),
    a ∣ b ∨ b ∣ a
⊢ PreValuationRing R ↔ Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2
have refine₂ : ∀ (H : Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) (a b : R) (this : b ∣ a ∨ a ∣ b), a ∣ b ∨ b ∣ a
Tactic: classical
  refine ⟨fun _ => ⟨le_total⟩, fun H => PreValuationRing.iff_dvd_total.mpr ⟨fun a b => ?_⟩⟩
  have := H.total (Ideal.span {a}) (Ideal.span {b})
  simp_rw [Ideal.span_singleton_le_span_singleton] at this
  exact this.symm
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : PreValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
⊢ Associated p q
have this : p ∣ q ∨ q ∣ p
Tactic: have := dvd_total p q
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : PreValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
this : p ∣ q ∨ q ∣ p
⊢ Associated p q
have this₁ : q ∣ p
Tactic: rw [Irreducible.dvd_comm hp hq, or_self_iff] at this
Cleared hypotheses: this
-- 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
⊢ ValuationRing R ↔ ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
have mp : ValuationRing R → ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
Tactic: constructor
-- 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
mp : ValuationRing R → ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
⊢ ValuationRing R ↔ ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
have mpr : (∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹) → ValuationRing R
Tactic: constructor
-- 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
H : ValuationRing R
x : K
⊢ IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
have mp : ∀ (x y : R) (hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y),
  IsLocalization.IsInteger R
      (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K)) ∨
    IsLocalization.IsInteger R
      (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K))⁻¹
Tactic: obtain ⟨x : R, y, hy, rfl⟩ := IsFractionRing.div_surjective R x
Cleared hypotheses: x
-- 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
H : ValuationRing R
x y : R
hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y
⊢ IsLocalization.IsInteger R
      (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K)) ∨
    IsLocalization.IsInteger R
      (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K))⁻¹
have this : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) y : K) (0 : K)
Tactic: have := (map_ne_zero_iff _ (IsFractionRing.injective R K)).mpr (nonZeroDivisors.ne_zero hy)
-- 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
H : ValuationRing R
x 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)
⊢ IsLocalization.IsInteger R
      (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K)) ∨
    IsLocalization.IsInteger R
      (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K))⁻¹
have mp : ∀ (s : R) (hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (x * s))
  (this : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (x * s) : K) (0 : K)),
  IsLocalization.IsInteger R
      (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K)
        ((algebraMap R K : (a : R) → K) (x * s) : K)) ∨
    IsLocalization.IsInteger R
      (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K)
          ((algebraMap R K : (a : R) → K) (x * s) : K))⁻¹
Tactic: obtain ⟨s, rfl | rfl⟩ := ValuationRing.cond x y
Cleared hypotheses: y, hy, this
-- 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
H : ValuationRing R
x 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)
mp :
  ∀ (s : R) (hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (x * s))
    (this : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (x * s) : K) (0 : K)),
    IsLocalization.IsInteger R
        (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K)
          ((algebraMap R K : (a : R) → K) (x * s) : K)) ∨
      IsLocalization.IsInteger R
        (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K)
            ((algebraMap R K : (a : R) → K) (x * s) : K))⁻¹
⊢ IsLocalization.IsInteger R
      (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K)) ∨
    IsLocalization.IsInteger R
      (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K))⁻¹
have mp₁ : ∀ (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: obtain ⟨s, rfl | rfl⟩ := ValuationRing.cond x y
Cleared hypotheses: x
-- 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
H : ValuationRing R
x s : R
hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (x * s)
this : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (x * s) : K) (0 : K)
⊢ HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) s : K)
      (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K)
        ((algebraMap R K : (a : R) → K) (x * s) : K)) =
    1
have rwa : HDiv.hDiv (β := K)
    (HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) s : K) ((algebraMap R K : (a : R) → K) x : K))
    ((algebraMap R K : (a : R) → K) (x * s) : K) =
  1
Tactic: rwa [mul_div, div_eq_one_iff_eq, map_mul, mul_comm]
-- 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
H : ValuationRing R
x s : R
hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (x * s)
this : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (x * s) : K) (0 : K)
rwa :
  HDiv.hDiv (β := K)
      (HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) s : K) ((algebraMap R K : (a : R) → K) x : K))
      ((algebraMap R K : (a : R) → K) (x * s) : K) =
    1
⊢ HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) s : K)
      (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K)
        ((algebraMap R K : (a : R) → K) (x * s) : K)) =
    1
have rwa₁ : HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) s : K) ((algebraMap R K : (a : R) → K) x : K) =
  (algebraMap R K : (a : R) → K) (x * s)
Tactic: rwa [mul_div, div_eq_one_iff_eq, map_mul, mul_comm]
-- 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
H : ValuationRing R
x s : R
hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (x * s)
this : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (x * s) : K) (0 : K)
rwa :
  HDiv.hDiv (β := K)
      (HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) s : K) ((algebraMap R K : (a : R) → K) x : K))
      ((algebraMap R K : (a : R) → K) (x * s) : K) =
    1
rwa₁ :
  HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) s : K) ((algebraMap R K : (a : R) → K) x : K) =
    (algebraMap R K : (a : R) → K) (x * s)
rwa₂ : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (x * s) : K) (0 : K)
⊢ HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) s : K)
      (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K)
        ((algebraMap R K : (a : R) → K) (x * s) : K)) =
    1
have rwa₃ : HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) s : K) ((algebraMap R K : (a : R) → K) x : K) =
  HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) s : K)
Tactic: rwa [mul_div, div_eq_one_iff_eq, map_mul, mul_comm]
-- 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
H : ValuationRing R
x s : R
hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (x * s)
this : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (x * s) : K) (0 : K)
rwa :
  HDiv.hDiv (β := K)
      (HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) s : K) ((algebraMap R K : (a : R) → K) x : K))
      ((algebraMap R K : (a : R) → K) (x * s) : K) =
    1
rwa₁ :
  HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) s : K) ((algebraMap R K : (a : R) → K) x : K) =
    (algebraMap R K : (a : R) → K) (x * s)
rwa₂ : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (x * s) : K) (0 : K)
rwa₃ :
  HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) s : K) ((algebraMap R K : (a : R) → K) x : K) =
    HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) s : K)
rwa₄ : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (x * s) : K) (0 : K)
⊢ HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) s : K)
      (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K)
        ((algebraMap R K : (a : R) → K) (x * s) : K)) =
    1
have rwa₅ : HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) s : K) =
  HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) s : K)
Tactic: rwa [mul_div, div_eq_one_iff_eq, map_mul, mul_comm]
-- 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
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
⊢ (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)
have 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)
Tactic: rwa [eq_div_iff, map_mul, mul_comm]
-- 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
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)
⊢ (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)
have 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)
Tactic: rwa [eq_div_iff, map_mul, mul_comm]
-- 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
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)
⊢ (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)
have 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)
Tactic: rwa [eq_div_iff, map_mul, mul_comm]
-- 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
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
⊢ ValuationRing R
have mpr : PreValuationRing R
Tactic: suffices PreValuationRing R from mk
-- 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
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
⊢ PreValuationRing R
have mpr : ∀ (a b : R), ∃ (c : R), a * c = b ∨ b * c = a
Tactic: constructor
-- 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
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
⊢ ∃ (c : R), a * c = b ∨ b * c = a
have pos : ∀ (ha : a = 0), ∃ (c : R), a * c = b ∨ b * c = a
Tactic: by_cases ha : a = 0
-- 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
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
⊢ ∃ (c : R), a * c = b ∨ b * c = a
have neg : ∀ (ha : ¬a = 0), ∃ (c : R), a * c = b ∨ b * c = a
Tactic: by_cases ha : a = 0
-- 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
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : a = 0
⊢ ∃ (c : R), a * c = b ∨ b * c = a
have pos : ∃ (c : R), 0 * c = b ∨ b * c = 0
Tactic: subst ha
Cleared hypotheses: a, ha
-- 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
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : ¬a = 0
⊢ ∃ (c : R), a * c = b ∨ b * c = a
have pos : ∀ (hb : b = 0), ∃ (c : R), a * c = b ∨ b * c = a
Tactic: by_cases hb : b = 0
-- 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
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
⊢ ∃ (c : R), a * c = b ∨ b * c = a
have neg : ∀ (hb : ¬b = 0), ∃ (c : R), a * c = b ∨ b * c = a
Tactic: by_cases hb : b = 0
-- 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
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : ¬a = 0
hb : b = 0
⊢ ∃ (c : R), a * c = b ∨ b * c = a
have pos : ∃ (c : R), a * c = 0 ∨ 0 * c = a
Tactic: subst hb
Cleared hypotheses: b, hb
-- 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
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : ¬a = 0
hb : ¬b = 0
⊢ ∃ (c : R), a * c = b ∨ b * c = a
have ha₁ : 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
Cleared hypotheses: ha
-- 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
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)
⊢ ∃ (c : R), a * c = b ∨ b * c = a
have hb₁ : 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
Cleared hypotheses: hb
-- 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
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), a * c = b ∨ b * c = a
have 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
Tactic: obtain ⟨c, e⟩ | ⟨c, e⟩ := H (algebraMap R K a / algebraMap R K 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
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
⊢ ∃ (c : R), a * c = b ∨ b * c = a
have 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
Tactic: obtain ⟨c, e⟩ | ⟨c, e⟩ := H (algebraMap R K a / algebraMap R K b)
-- 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
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)
⊢ ∃ (c : R), a * c = b ∨ b * c = a
have e₁ : b * c = a
Tactic: rw [eq_div_iff hb, ← map_mul, (IsFractionRing.injective R K).eq_iff, mul_comm] at e
Cleared hypotheses: e
-- 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
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))⁻¹
⊢ ∃ (c : R), a * c = b ∨ b * c = a
have e₁ : a * c = b
Tactic: rw [inv_div, eq_div_iff ha, ← map_mul, (IsFractionRing.injective R K).eq_iff, mul_comm c] at e
Cleared hypotheses: 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 : ValuationRing R
⊢ IsBezout R
have rw : ∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})
Tactic: rw [IsBezout.iff_span_pair_isPrincipal]
-- 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) (Ideal.span {x, y})
have rw : Submodule.IsPrincipal (R := R) (max (Ideal.span {x}) (Ideal.span {y}))
Tactic: rw [Ideal.span_insert]