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

Tactic:
rw [← (algebraMap A K).map_one] at hf

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

Tactic:
rw [← (algebraMap A K).map_one] at hf

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

Tactic:
IsFractionRing.injective _ _ (mul_right_cancel₀ hb hf).symm

Premises used: IsFractionRing.injective, Eq.symm, mul_right_cancel₀
-- 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 =
    HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) 1 : K) b
hb : ¬b = 0
⊢ 1 = f * e

Tactic:
exact IsFractionRing.injective _ _ (mul_right_cancel₀ hb hf).symm

Premises used: IsFractionRing.injective, Eq.symm, mul_right_cancel₀
-- 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
⊢ IsUnit e

Tactic:
have : IsUnit e := by
      apply isUnit_of_dvd_one
      use f
      rw [mul_comm]
      rw [← mul_smul, Algebra.smul_def] at hf
      nth_rw 2 [← one_mul b] at hf
      rw [← (algebraMap A K).map_one] at hf
      exact IsFractionRing.injective _ _ (mul_right_cancel₀ hb hf).symm
-- 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
this : IsUnit e
neg : (MulAction.orbitRel Aˣ K : K → K → Prop) (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)

Tactic:
apply Quotient.sound'

Premises used: Quotient.sound'
-- 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
this : IsUnit e
⊢ (MulAction.orbitRel Aˣ K : K → K → Prop) (e • b) b

Tactic:
⟨this.unit, rfl⟩

Premises used: Set.Mem, setOf, MulAction.orbit, Exists.intro, IsUnit.unit, Set.range, 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
a b_1 : ValueGroup A K
b : K
e f : A
hf : f • e • b = b
hb : ¬b = 0
this : IsUnit e
⊢ (MulAction.orbitRel Aˣ K : K → K → Prop) (e • b) b

Tactic:
exact ⟨this.unit, 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
a_1 : ValueGroup A K
a : K
b_1 : ValueGroup A K
b : K
c_1 : ValueGroup A K
c : K
mk : (MulAction.orbitRel Aˣ K : K → K → Prop) (a * b * c) (a * (b * c))
⊢ HMul.hMul (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a)
        (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b) *
      Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) c =
    Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a *
      HMul.hMul (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b)
        (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) c)

Tactic:
apply Quotient.sound'

Premises used: Quotient.sound'
-- 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_1 : ValueGroup A K
a : K
b_1 : ValueGroup A K
b : K
c_1 : ValueGroup A K
c : K
mk mk₁ : (MulAction.orbitRel Aˣ K : K → K → Prop) (a * (b * c)) (a * (b * c))
⊢ (MulAction.orbitRel Aˣ K : K → K → Prop) (a * b * c) (a * (b * c))

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- 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_1 : ValueGroup A K
a : K
mk : (MulAction.orbitRel Aˣ K : K → K → Prop) (1 * a) a
⊢ HMul.hMul (α := ValueGroup A K) 1 (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a) =
    Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a

Tactic:
apply Quotient.sound'

Premises used: Quotient.sound'
-- 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_1 : ValueGroup A K
a : K
mk mk₁ : (MulAction.orbitRel Aˣ K : K → K → Prop) a a
⊢ (MulAction.orbitRel Aˣ K : K → K → Prop) (1 * a) a

Tactic:
rw [one_mul]

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_1 : ValueGroup A K
a : K
mk : (MulAction.orbitRel Aˣ K : K → K → Prop) (a * 1) a
⊢ HMul.hMul (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a) 1 =
    Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a

Tactic:
apply Quotient.sound'

Premises used: Quotient.sound'
-- 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_1 : ValueGroup A K
a : K
mk mk₁ : (MulAction.orbitRel Aˣ K : K → K → Prop) a a
⊢ (MulAction.orbitRel Aˣ K : K → K → Prop) (a * 1) a

Tactic:
rw [mul_one]

Premises used: 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
a_1 : ValueGroup A K
a : K
b_1 : ValueGroup A K
b : K
mk : (MulAction.orbitRel Aˣ K : K → K → Prop) (a * b) (b * a)
⊢ HMul.hMul (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a)
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b) =
    HMul.hMul (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b)
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a)

Tactic:
apply Quotient.sound'

Premises used: Quotient.sound'
-- 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_1 : ValueGroup A K
a : K
b_1 : ValueGroup A K
b : K
mk mk₁ : (MulAction.orbitRel Aˣ K : K → K → Prop) (b * a) (b * a)
⊢ (MulAction.orbitRel Aˣ K : K → K → Prop) (a * b) (b * a)

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_1 : ValueGroup A K
a : K
mk : (MulAction.orbitRel Aˣ K : K → K → Prop) (0 * a) 0
⊢ HMul.hMul (α := ValueGroup A K) 0 (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a) = 0

Tactic:
apply Quotient.sound'

Premises used: Quotient.sound'
-- 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_1 : ValueGroup A K
a : K
mk mk₁ : (MulAction.orbitRel Aˣ K : K → K → Prop) 0 0
⊢ (MulAction.orbitRel Aˣ K : K → K → Prop) (0 * a) 0

Tactic:
rw [zero_mul]

Premises used: MulZeroClass.zero_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_1 : ValueGroup A K
a : K
mk : (MulAction.orbitRel Aˣ K : K → K → Prop) (a * 0) 0
⊢ HMul.hMul (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a) 0 = 0

Tactic:
apply Quotient.sound'

Premises used: Quotient.sound'
-- 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_1 : ValueGroup A K
a : K
mk mk₁ : (MulAction.orbitRel Aˣ K : K → K → Prop) 0 0
⊢ (MulAction.orbitRel Aˣ K : K → K → Prop) (a * 0) 0

Tactic:
rw [mul_zero]

Premises used: MulZeroClass.mul_zero
-- 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 : (MulAction.orbitRel Aˣ K : K → K → Prop) 0⁻¹ 0
⊢ Eq.{v + 1} (α := ValueGroup A K) 0⁻¹ 0

Tactic:
apply Quotient.sound'

Premises used: Quotient.sound'
-- 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 a₁ : (MulAction.orbitRel Aˣ K : K → K → Prop) 0 0
⊢ (MulAction.orbitRel Aˣ K : K → K → Prop) 0⁻¹ 0

Tactic:
rw [inv_zero]

Premises used: inv_zero
-- 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_1 : ValueGroup A K
a : K
ha : Ne (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a) 0
mk : (MulAction.orbitRel Aˣ K : K → K → Prop) (a * a⁻¹) 1
⊢ HMul.hMul (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a)
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a)⁻¹ =
    1

Tactic:
apply Quotient.sound'

Premises used: Quotient.sound'
-- 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_1 : ValueGroup A K
a : K
ha : Ne (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a) 0
h : (fun (m : Aˣ) ↦ HSMul.hSMul (β := K) m 1) 1 = a * a⁻¹
⊢ (MulAction.orbitRel Aˣ K : K → K → Prop) (a * 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_1 : ValueGroup A K
a : K
ha : Ne (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a) 0
h : 1 = a * a⁻¹
⊢ (fun (m : Aˣ) ↦ HSMul.hSMul (β := K) m 1) 1 = a * a⁻¹

Tactic:
simp only [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_1 : ValueGroup A K
a : K
ha : Ne (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a) 0
apply : a ≠ 0
⊢ 1 = a * a⁻¹

Tactic:
apply (mul_inv_cancel₀ _).symm

Premises used: mul_inv_cancel₀, Eq.symm
-- 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_1 : ValueGroup A K
a : K
ha : Ne (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a) 0
contrapose : ∀ (ha : a = 0), Eq (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a) 0
⊢ a ≠ 0

Tactic:
contrapose ha
-- 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_1 : ValueGroup A K
a : K
ha : a = 0
rw : Eq.{v + 1} (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) 0) 0
⊢ Eq (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a) 0

Tactic:
rw [ha]
-- 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_1 : ValueGroup A K
a : K
ha : a = 0
⊢ Eq.{v + 1} (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) 0) 0

Tactic:
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
simp_rw : ∀ ⦃a : ValueGroup A K⦄ (ha : ¬a ≤ 0) ⦃b c : ValueGroup A K⦄ (hbc : ¬c ≤ b), ¬a * c ≤ a * b
⊢ ∀ ⦃a : ValueGroup A K⦄ (ha : 0 < a) ⦃b c : ValueGroup A K⦄ (hbc : b < c), a * b < a * c

Tactic:
simp_rw [← not_le]

Premises used: not_le
-- 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_1 : ValueGroup A K
a : K
ha : ¬LE.le (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a) 0
b_1 : ValueGroup A K
b : K
c_1 : ValueGroup A K
c : K
hbc :
  ¬LE.le (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) c)
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b)
mk :
  ∀
    (hbc :
      HMul.hMul (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a)
          (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) c) ≤
        HMul.hMul (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a)
          (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b)),
    LE.le (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) c)
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b)
⊢ ¬HMul.hMul (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a)
        (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) c) ≤
      HMul.hMul (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a)
        (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b)

Tactic:
contrapose hbc
-- 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_1 : ValueGroup A K
a : K
ha : ¬LE.le (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a) 0
b_1 : ValueGroup A K
b : K
c_1 : ValueGroup A K
c : K
hbc :
  HMul.hMul (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a)
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) c) ≤
    HMul.hMul (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a)
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b)
mk :
  ∀ (d : A) (hd : d • (a * b) = a * c),
    LE.le (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) c)
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b)
⊢ LE.le (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) c)
    (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b)

Tactic:
obtain ⟨d, hd⟩ := hbc
-- 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_1 : ValueGroup A K
a : K
ha : ¬LE.le (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a) 0
b_1 : ValueGroup A K
b : K
c_1 : ValueGroup A K
c : K
d : A
hd : d • (a * b) = a * c
⊢ HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) d : K) b = c ∨ a = 0

Tactic:
simp only [Algebra.smul_def, mul_left_comm, mul_eq_mul_left_iff] at hd

Premises used: mul_eq_mul_left_iff, mul_left_comm, 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_1 : ValueGroup A K
a : K
ha : ¬LE.le (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a) 0
b_1 : ValueGroup A K
b : K
c_1 : ValueGroup A K
c : K
d : A
hd : HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) d : K) b = c ∨ a = 0
mk :
  LE.le (α := ValueGroup A K)
    (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) (HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) d : K) b))
    (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b)
mk₁ :
  ∀ (ha : ¬LE.le.{v} (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) 0) 0),
    LE.le (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) c)
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b)
⊢ LE.le (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) c)
    (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b)

Tactic:
obtain rfl | rfl := hd

Premises used: 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
a_1 : ValueGroup A K
a : K
ha : ¬LE.le (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a) 0
b_1 : ValueGroup A K
b : K
c : ValueGroup A K
d : A
⊢ d • b = HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) d : K) b

Tactic:
simp [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_1 : ValueGroup A K
a : K
ha : ¬LE.le (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a) 0
b_1 : ValueGroup A K
b : K
c : ValueGroup A K
d : A
⊢ LE.le (α := ValueGroup A K)
    (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) (HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) d : K) b))
    (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b)

Tactic:
exact ⟨d, by simp [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_1 : ValueGroup A K
b : K
c_1 : ValueGroup A K
c : K
d : A
ha : ¬LE.le.{v} (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) 0) 0
⊢ LE.le (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) c)
    (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b)

Tactic:
cases ha le_rfl

Premises used: le_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
a_1 : ValueGroup A K
a : K
⊢ LE.le (α := ValueGroup A K) 0 (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a)

Tactic:
⟨0, zero_smul ..⟩

Premises used: zero_smul, Exists.intro, OfNat.ofNat, Quotient.liftOn₂'
-- 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_1 : ValueGroup A K
a : K
⊢ LE.le (α := ValueGroup A K) 0 (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a)

Tactic:
exact ⟨0, zero_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
b : ValueGroup A K
a : K
⊢ LE.le (α := ValueGroup A K) 0 (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a)

Tactic:
⟨0, zero_smul ..⟩

Premises used: zero_smul, Exists.intro, OfNat.ofNat, Quotient.liftOn₂'
-- 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 : ValueGroup A K
a : K
⊢ LE.le (α := ValueGroup A K) 0 (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a)

Tactic:
exact ⟨0, zero_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 : K
obtain :
  ∀ (xa ya : A) (hya : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) 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) +
          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))
⊢ LE.le (α := ValueGroup A K) (Quotient.mk'' (a + b)) (max (Quotient.mk'' a) (Quotient.mk'' b))

Tactic:
obtain ⟨xa, ya, hya, rfl⟩ := IsFractionRing.div_surjective A a

Premises used: IsFractionRing.div_surjective, rfl