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
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)
⊢ 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)))
have 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)))
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
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)))
⊢ 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)))
have 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)))
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
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
⊢ 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)))
have 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)))
Tactic: 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
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
⊢ 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)))
have 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)
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
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 • 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 : 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
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
⊢ 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)
have 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)
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
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
⊢ 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)
have h₁ : Eq.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) (c * xa * yb) : K) ((algebraMap A K : (a : A) → K) (ya * xb) : K)
Tactic: simp only [← map_mul]
-- 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
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
⊢ Eq.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) (c * xa * yb) : K) ((algebraMap A K : (a : A) → K) (ya * xb) : K)
have h₁ : c * 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
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
⊢ 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)))
have 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)))
Tactic: 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
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
⊢ 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)))
have 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)
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
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 • 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)
have 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)
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
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
⊢ 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)
have 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)
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
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
⊢ 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)
have h₁ : Eq.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) (c * xb * ya) : K) ((algebraMap A K : (a : A) → K) (yb * xa) : K)
Tactic: simp only [← map_mul]
-- 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
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
⊢ Eq.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) (c * xb * ya) : K) ((algebraMap A K : (a : A) → K) (yb * xa) : K)
have h₁ : c * xb * ya = yb * xa
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
a : ValueGroup A K
a_1 : K
⊢ 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)
have h : HSMul.hSMul.{u, v, v} (α := A) 1 a_1 = a_1
Tactic: use 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
a : ValueGroup A K
a_1 : K
⊢ HSMul.hSMul.{u, v, v} (α := A) 1 a_1 = a_1
have h : a_1 = a_1
Tactic: rw [one_smul]
-- 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
a b c_1 : ValueGroup A K
c : K
e f : A
⊢ 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)
have h : (e * f) • c = e • f • c
Tactic: use e * f
-- 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
a b c_1 : ValueGroup A K
c : K
e f : A
⊢ (e * f) • c = e • f • c
have h : e • f • c = e • f • c
Tactic: rw [mul_smul]
-- 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
a b_1 : ValueGroup A K
b : K
e f : A
hf : f • e • b = 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)
have 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)
Tactic: by_cases hb : b = 0
-- 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
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)
⊢ 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)
have 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)
Tactic: by_cases hb : b = 0
-- 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
a b_1 : ValueGroup A K
b : K
e f : A
hf : f • e • b = b
hb : ¬b = 0
⊢ IsUnit e
have h : e ∣ 1
Tactic: apply isUnit_of_dvd_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
a b_1 : ValueGroup A K
b : K
e f : A
hf : f • e • b = b
hb : ¬b = 0
⊢ e ∣ 1
have h : 1 = e * f
Tactic: use f
-- 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
a b_1 : ValueGroup A K
b : K
e f : A
hf : f • e • b = b
hb : ¬b = 0
⊢ 1 = e * f
have h : 1 = f * e
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (hypothesis)
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
⊢ 1 = f * e
have hf₁ : HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (f * e) : K) b = b
Tactic: rw [← mul_smul, Algebra.smul_def] at hf
Cleared hypotheses: hf, hb