awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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
b : K
xa ya : A
hya : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) ya
obtain :
  ∀ (xb yb : A) (hyb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) 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))))
⊢ 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) + b))
    (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'' b))

Tactic:
obtain ⟨xb, yb, hyb, rfl⟩ := IsFractionRing.div_surjective A b

Premises used: IsFractionRing.div_surjective, rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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
⊢ Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) ya : K) (0 : K)

Tactic:
have : (algebraMap A K) ya ≠ 0 := IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors hya
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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 : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) ya : K) (0 : K)
⊢ Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) yb : K) (0 : K)

Tactic:
have : (algebraMap A K) yb ≠ 0 := IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors hyb
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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))))
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))))
⊢ 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)

Premises used: HMul.hMul, ValuationRing.cond
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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
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)))
⊢ 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:
apply le_trans _ (le_max_left _ _)

Premises used: le_max_left, le_trans
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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
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)
⊢ 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:
use c + 1
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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
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)
⊢ (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:
rw [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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
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)
⊢ 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:
field_simp
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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
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)
⊢ 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:
simp only [← map_mul, ← map_add]

Premises used: map_add, map_mul
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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
h₁ : (c + 1) * xa * yb = xa * yb + ya * xb
⊢ 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:
congr 1
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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) * xa * yb = xa * yb + ya * xb

Tactic:
linear_combination h
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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
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)))
⊢ 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:
apply le_trans _ (le_max_right _ _)

Premises used: le_max_right, le_trans
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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
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)
⊢ 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:
use c + 1
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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
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)
⊢ (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:
rw [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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
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)
⊢ 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:
field_simp
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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
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)
⊢ 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:
simp only [← map_mul, ← map_add]

Premises used: map_add, map_mul
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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
h₁ : (c + 1) * xb * ya = yb * xa + xb * ya
⊢ 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:
congr 1
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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) * xb * ya = yb * xa + xb * ya

Tactic:
linear_combination h
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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
mpr :
  (∃ (a : A), (algebraMap A K : (a : A) → K) a = x) →
    Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x
⊢ 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
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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 = HSMul.hSMul (β := K) c 1
⊢ ∃ (a : A), (algebraMap A K : (a : A) → K) a = HSMul.hSMul (β := K) c 1

Tactic:
use c
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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)
h₁ h₂ : Eq.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) c : K) ((algebraMap A K : (a : A) → K) c : K)
⊢ (algebraMap A K : (a : A) → K) c = HSMul.hSMul (β := K) c 1

Tactic:
rw [Algebra.smul_def, mul_one]

Premises used: Algebra.smul_def, mul_one
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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 : HSMul.hSMul (β := K) c 1 = (algebraMap A K : (a : A) → K) c
⊢ Membership.mem (α := K) (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))
    ((algebraMap A K : (a : A) → K) c : K)

Tactic:
use c
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
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
h₁ h₂ : Eq.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) c : K) ((algebraMap A K : (a : A) → K) c : K)
⊢ HSMul.hSMul (β := K) c 1 = (algebraMap A K : (a : A) → K) c

Tactic:
rw [Algebra.smul_def, mul_one]

Premises used: Algebra.smul_def, mul_one