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
a b : ValueGroup 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)
mk :
  ∀ (c : A) (h : xa * yb * c = xb * ya),
    LE.le (α := ValueGroup A K)
        (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
          (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K)))
        (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
          (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)
        (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
          (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)))
        (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
          (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K)))
mk₁ :
  ∀ (c : A) (h : xb * ya * c = xa * yb),
    LE.le (α := ValueGroup A K)
        (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
          (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K)))
        (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
          (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)
        (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
          (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)))
        (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
          (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)
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K)))
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
        (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)
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)))
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : 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
a b : ValueGroup 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
mk :
  LE.le (α := ValueGroup A K)
    (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
      (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)))
    (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
      (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)
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K)))
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
        (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)
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)))
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K)))

Tactic:
right
-- 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
a b : ValueGroup 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 • 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)
    (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
      (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)))
    (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
      (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : 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
a b : ValueGroup 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 : 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 • 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
a b : ValueGroup 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 : 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 : 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
a b : ValueGroup 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 * xa * yb) : K) ((algebraMap A K : (a : A) → K) (ya * xb) : K)
⊢ HMul.hMul (β := K)
      (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c : 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]

Premises used: 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
a b : ValueGroup 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 * xa * yb = ya * xb
⊢ Eq.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) (c * xa * yb) : K) ((algebraMap A K : (a : A) → K) (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
a b : ValueGroup 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 * 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
a b : ValueGroup 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
mk :
  LE.le (α := ValueGroup A K)
    (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
      (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K)))
    (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
      (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)
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K)))
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
        (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)
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)))
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K)))

Tactic:
left
-- 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
a b : ValueGroup 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 • 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)
⊢ LE.le (α := ValueGroup A K)
    (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
      (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K)))
    (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop)
      (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : 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
a b : ValueGroup 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 : 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)
⊢ c • 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)

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
a b : ValueGroup 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 : 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) ((algebraMap A K : (a : A) → K) c : 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)

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
a b : ValueGroup 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 * xb * ya) : K) ((algebraMap A K : (a : A) → K) (yb * xa) : K)
⊢ HMul.hMul (β := K)
      (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c : 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)

Tactic:
simp only [← map_mul]

Premises used: 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
a b : ValueGroup 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 * xb * ya = yb * xa
⊢ Eq.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) (c * xb * ya) : K) ((algebraMap A K : (a : A) → K) (yb * xa) : 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
a b : ValueGroup 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 * xb * ya = yb * xa

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
a : ValueGroup A K
a_1 : K
h : HSMul.hSMul.{u, v, v} (α := A) 1 a_1 = a_1
⊢ LE.le (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a_1)
    (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a_1)

Tactic:
use 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
a : ValueGroup A K
a_1 : K
h h₁ : a_1 = a_1
⊢ HSMul.hSMul.{u, v, v} (α := A) 1 a_1 = a_1

Tactic:
rw [one_smul]

Premises used: one_smul
-- 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
a b c_1 : ValueGroup A K
c : K
e f : A
h : (e * f) • c = e • f • c
⊢ LE.le (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) (e • f • c))
    (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) c)

Tactic:
use e * f
-- 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
a b c_1 : ValueGroup A K
c : K
e f : A
h h₁ : e • f • c = e • f • c
⊢ (e * f) • c = e • f • c

Tactic:
rw [mul_smul]

Premises used: SemigroupAction.mul_smul
-- 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
a b_1 : ValueGroup A K
b : K
e f : A
hf : f • e • b = b
pos :
  ∀ (hb : b = 0),
    Eq (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) (e • b))
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b)
neg :
  ∀ (hb : ¬b = 0),
    Eq (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) (e • b))
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b)
⊢ Eq (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) (e • b))
    (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b)

Tactic:
by_cases hb : b = 0
-- 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
a b_1 : ValueGroup A K
b : K
e f : A
hf : f • e • b = b
hb : b = 0
⊢ Eq (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) (e • b))
    (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b)

Tactic:
simp [hb]
-- 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
a b_1 : ValueGroup A K
b : K
e f : A
hf : f • e • b = b
hb : ¬b = 0
h : e ∣ 1
⊢ IsUnit e

Tactic:
apply isUnit_of_dvd_one

Premises used: isUnit_of_dvd_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
a b_1 : ValueGroup A K
b : K
e f : A
hf : f • e • b = b
hb : ¬b = 0
h : 1 = e * f
⊢ e ∣ 1

Tactic:
use f
-- 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
a b_1 : ValueGroup A K
b : K
e f : A
hf : f • e • b = b
hb : ¬b = 0
h : 1 = f * e
⊢ 1 = e * f

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- 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
a b_1 : ValueGroup A K
b : K
e f : A
hf : f • e • b = b
hb : ¬b = 0
⊢ HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (f * e) : K) b = b

Tactic:
rw [← mul_smul, Algebra.smul_def] at hf

Premises used: Algebra.smul_def, SemigroupAction.mul_smul
-- 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
a b_1 : ValueGroup A K
b : K
e f : A
hf : f • e • b = b
hb : ¬b = 0
hf₁ : HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (f * e) : K) b = b
⊢ ¬b = 0

Tactic:
rw [← mul_smul, Algebra.smul_def] at hf

Premises used: Algebra.smul_def, SemigroupAction.mul_smul
-- 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
a b_1 : ValueGroup A K
b : K
e f : A
hf : HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (f * e) : K) b = b
hb : ¬b = 0
⊢ HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (f * e) : K) b = 1 * b

Tactic:
nth_rw 2 [← one_mul b] at hf

Premises used: one_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
a b_1 : ValueGroup A K
b : K
e f : A
hf : HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (f * e) : K) b = b
hb : ¬b = 0
hf₁ : HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (f * e) : K) b = 1 * b
⊢ ¬b = 0

Tactic:
nth_rw 2 [← one_mul b] at hf

Premises used: one_mul