awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
xa ya : A
hya : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) ya
xb yb : A
hyb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) yb
this_1 : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) ya : K) (0 : K)
this : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) yb : K) (0 : K)
inl :
  ∀ (c : A) (h : xa * yb * c = xb * ya),
    LE.le (α := ValueGroup A K)
      (Quotient.mk''
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K) +
          HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)))
      (max
        (Quotient.mk''
          (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K)))
        (Quotient.mk''
          (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K)
            ((algebraMap A K : (a : A) → K) yb : K))))
⊢ LE.le (α := ValueGroup A K)
    (Quotient.mk''
      (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K) +
        HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)))
    (max
      (Quotient.mk''
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K)))
      (Quotient.mk''
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K))))
have inr : ∀ (c : A) (h : xb * ya * c = xa * yb),
  LE.le (α := ValueGroup A K)
    (Quotient.mk''
      (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K) +
        HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)))
    (max
      (Quotient.mk''
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K)))
      (Quotient.mk''
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K))))
Tactic: obtain ⟨c, h | h⟩ := ValuationRing.cond (xa * yb) (xb * ya)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
xa ya : A
hya : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) ya
xb yb : A
hyb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) yb
this_1 : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) ya : K) (0 : K)
this : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) yb : K) (0 : K)
c : A
h : xa * yb * c = xb * ya
⊢ LE.le (α := ValueGroup A K)
    (Quotient.mk''
      (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K) +
        HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)))
    (max
      (Quotient.mk''
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K)))
      (Quotient.mk''
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K))))
have apply : LE.le (α := ValueGroup A K)
  (Quotient.mk''
    (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K) +
      HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)))
  (Quotient.mk''
    (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K)))
Tactic: apply le_trans _ (le_max_left _ _)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
xa ya : A
hya : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) ya
xb yb : A
hyb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) yb
this_1 : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) ya : K) (0 : K)
this : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) yb : K) (0 : K)
c : A
h : xa * yb * c = xb * ya
⊢ LE.le (α := ValueGroup A K)
    (Quotient.mk''
      (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K) +
        HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)))
    (Quotient.mk''
      (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K)))
have h₁ : (c + 1) • HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K) =
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K) +
    HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)
Tactic: use c + 1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
xa ya : A
hya : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) ya
xb yb : A
hyb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) yb
this_1 : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) ya : K) (0 : K)
this : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) yb : K) (0 : K)
c : A
h : xa * yb * c = xb * ya
⊢ (c + 1) •
      HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K) =
    HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K) +
      HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)
have h₁ : HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (c + 1) : K)
    (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K)) =
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K) +
    HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)
Tactic: rw [Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
xa ya : A
hya : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) ya
xb yb : A
hyb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) yb
this_1 : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) ya : K) (0 : K)
this : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) yb : K) (0 : K)
c : A
h : xa * yb * c = xb * ya
⊢ HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (c + 1) : K)
      (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K)) =
    HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K) +
      HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)
have h₁ : HMul.hMul (β := K)
    (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (c + 1) : K) ((algebraMap A K : (a : A) → K) xa : K))
    ((algebraMap A K : (a : A) → K) yb : K) =
  HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) yb : K) +
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) ya : K) ((algebraMap A K : (a : A) → K) xb : K)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
xa ya : A
hya : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) ya
xb yb : A
hyb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) yb
this_1 : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) ya : K) (0 : K)
this : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) yb : K) (0 : K)
c : A
h : xa * yb * c = xb * ya
⊢ HMul.hMul (β := K)
      (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (c + 1) : K) ((algebraMap A K : (a : A) → K) xa : K))
      ((algebraMap A K : (a : A) → K) yb : K) =
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) yb : K) +
      HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) ya : K) ((algebraMap A K : (a : A) → K) xb : K)
have h₁ : Eq.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) ((c + 1) * xa * yb) : K)
  ((algebraMap A K : (a : A) → K) (xa * yb + ya * xb) : K)
Tactic: simp only [← map_mul, ← map_add]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
xa ya : A
hya : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) ya
xb yb : A
hyb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) yb
this_1 : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) ya : K) (0 : K)
this : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) yb : K) (0 : K)
c : A
h : xa * yb * c = xb * ya
⊢ Eq.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) ((c + 1) * xa * yb) : K)
    ((algebraMap A K : (a : A) → K) (xa * yb + ya * xb) : K)
have h₁ : (c + 1) * xa * yb = xa * yb + ya * xb
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
xa ya : A
hya : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) ya
xb yb : A
hyb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) yb
this_1 : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) ya : K) (0 : K)
this : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) yb : K) (0 : K)
c : A
h : xb * ya * c = xa * yb
⊢ LE.le (α := ValueGroup A K)
    (Quotient.mk''
      (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K) +
        HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)))
    (max
      (Quotient.mk''
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K)))
      (Quotient.mk''
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K))))
have apply : LE.le (α := ValueGroup A K)
  (Quotient.mk''
    (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K) +
      HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)))
  (Quotient.mk''
    (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)))
Tactic: apply le_trans _ (le_max_right _ _)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
xa ya : A
hya : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) ya
xb yb : A
hyb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) yb
this_1 : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) ya : K) (0 : K)
this : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) yb : K) (0 : K)
c : A
h : xb * ya * c = xa * yb
⊢ LE.le (α := ValueGroup A K)
    (Quotient.mk''
      (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K) +
        HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)))
    (Quotient.mk''
      (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)))
have h₁ : (c + 1) • HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K) =
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K) +
    HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)
Tactic: use c + 1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
xa ya : A
hya : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) ya
xb yb : A
hyb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) yb
this_1 : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) ya : K) (0 : K)
this : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) yb : K) (0 : K)
c : A
h : xb * ya * c = xa * yb
⊢ (c + 1) •
      HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K) =
    HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K) +
      HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)
have h₁ : HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (c + 1) : K)
    (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)) =
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K) +
    HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)
Tactic: rw [Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
xa ya : A
hya : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) ya
xb yb : A
hyb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) yb
this_1 : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) ya : K) (0 : K)
this : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) yb : K) (0 : K)
c : A
h : xb * ya * c = xa * yb
⊢ HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (c + 1) : K)
      (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)) =
    HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K) +
      HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)
have h₁ : HMul.hMul (β := K)
    (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (c + 1) : K) ((algebraMap A K : (a : A) → K) xb : K))
    ((algebraMap A K : (a : A) → K) ya : K) =
  HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) yb : K) ((algebraMap A K : (a : A) → K) xa : K) +
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) ya : K)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
xa ya : A
hya : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) ya
xb yb : A
hyb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) yb
this_1 : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) ya : K) (0 : K)
this : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) yb : K) (0 : K)
c : A
h : xb * ya * c = xa * yb
⊢ HMul.hMul (β := K)
      (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (c + 1) : K) ((algebraMap A K : (a : A) → K) xb : K))
      ((algebraMap A K : (a : A) → K) ya : K) =
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) yb : K) ((algebraMap A K : (a : A) → K) xa : K) +
      HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) ya : K)
have h₁ : Eq.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) ((c + 1) * xb * ya) : K)
  ((algebraMap A K : (a : A) → K) (yb * xa + xb * ya) : K)
Tactic: simp only [← map_mul, ← map_add]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
xa ya : A
hya : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) ya
xb yb : A
hyb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) yb
this_1 : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) ya : K) (0 : K)
this : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) yb : K) (0 : K)
c : A
h : xb * ya * c = xa * yb
⊢ Eq.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) ((c + 1) * xb * ya) : K)
    ((algebraMap A K : (a : A) → K) (yb * xa + xb * ya) : K)
have h₁ : (c + 1) * xb * ya = yb * xa + xb * ya
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
x : K
⊢ Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x ↔
    ∃ (a : A), (algebraMap A K : (a : A) → K) a = x
have mp : Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x →
  ∃ (a : A), (algebraMap A K : (a : A) → K) a = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
x : K
mp :
  Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x →
    ∃ (a : A), (algebraMap A K : (a : A) → K) a = x
⊢ Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x ↔
    ∃ (a : A), (algebraMap A K : (a : A) → K) a = x
have mpr : (∃ (a : A), (algebraMap A K : (a : A) → K) a = x) →
  Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
c : A
⊢ ∃ (a : A), (algebraMap A K : (a : A) → K) a = HSMul.hSMul (β := K) c 1
have h : (algebraMap A K : (a : A) → K) c = HSMul.hSMul (β := K) c 1
Tactic: use c
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
c : A
⊢ (algebraMap A K : (a : A) → K) c = HSMul.hSMul (β := K) c 1
have h : (algebraMap A K : (a : A) → K) c = HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c : K) (1 : K)
Tactic: rw [Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
c : A
h : (algebraMap A K : (a : A) → K) c = HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c : K) (1 : K)
⊢ (algebraMap A K : (a : A) → K) c = HSMul.hSMul (β := K) c 1
have h₁ : Eq.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) c : K) ((algebraMap A K : (a : A) → K) c : K)
Tactic: rw [Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
c : A
⊢ Membership.mem (α := K) (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))
    ((algebraMap A K : (a : A) → K) c : K)
have h : HSMul.hSMul (β := K) c 1 = (algebraMap A K : (a : A) → K) c
Tactic: use c
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
c : A
⊢ HSMul.hSMul (β := K) c 1 = (algebraMap A K : (a : A) → K) c
have h : HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c : K) (1 : K) = (algebraMap A K : (a : A) → K) c
Tactic: rw [Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
c : A
h : HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c : K) (1 : K) = (algebraMap A K : (a : A) → K) c
⊢ HSMul.hSMul (β := K) c 1 = (algebraMap A K : (a : A) → K) c
have h₁ : Eq.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) c : K) ((algebraMap A K : (a : A) → K) c : K)
Tactic: rw [Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
x x_1 : A
⊢ Subtype.mk (p := fun (x : K) ↦
      Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
      ((algebraMap A K : (a : A) → K) (x * x_1)) ⋯ =
    HMul.hMul (α := ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) (β :=
      ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
      (Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
          ((algebraMap A K : (a : A) → K) x) ⋯ :
        ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
      (Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
          ((algebraMap A K : (a : A) → K) x_1) ⋯ :
        ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
have a : (↑(Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
        ((algebraMap A K : (a : A) → K) (x * x_1)) sorry) :
    K) =
  (↑(HMul.hMul (α := ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) (β :=
        ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
        (Subtype.mk (p := fun (x : K) ↦
            Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
            ((algebraMap A K : (a : A) → K) x) sorry :
          ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
        (Subtype.mk (p := fun (x : K) ↦
            Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
            ((algebraMap A K : (a : A) → K) x_1) sorry :
          ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))) :
    K)
Tactic: ext1