awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (f * e) : K) b = b
hb : ¬b = 0
⊢ 1 = f * e
have hf₁ : HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (f * e) : K) b = 1 * b
Tactic: nth_rw 2 [← one_mul b] at hf
Cleared hypotheses: hf, hb
-- 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 : HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (f * e) : K) b = 1 * b
hb : ¬b = 0
⊢ 1 = f * e
have 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
Tactic: rw [← (algebraMap A K).map_one] at hf
Cleared hypotheses: hf, hb
-- 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
⊢ 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 this : 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
-- 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
this : IsUnit e
⊢ 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 : (MulAction.orbitRel Aˣ K : K → K → Prop) (e • b) b
Tactic: apply Quotient.sound'
-- 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_1 : ValueGroup A K
a : K
b_1 : ValueGroup A K
b : K
c_1 : ValueGroup A K
c : K
⊢ 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)
have mk : (MulAction.orbitRel Aˣ K : K → K → Prop) (a * b * c) (a * (b * c))
Tactic: apply Quotient.sound'
-- 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_1 : ValueGroup A K
a : K
b_1 : ValueGroup A K
b : K
c_1 : ValueGroup A K
c : K
⊢ (MulAction.orbitRel Aˣ K : K → K → Prop) (a * b * c) (a * (b * c))
have mk : (MulAction.orbitRel Aˣ K : K → K → Prop) (a * (b * c)) (a * (b * c))
Tactic: rw [mul_assoc]
-- 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_1 : ValueGroup A K
a : K
⊢ 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
have mk : (MulAction.orbitRel Aˣ K : K → K → Prop) (1 * a) a
Tactic: apply Quotient.sound'
-- 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_1 : ValueGroup A K
a : K
⊢ (MulAction.orbitRel Aˣ K : K → K → Prop) (1 * a) a
have mk : (MulAction.orbitRel Aˣ K : K → K → Prop) a a
Tactic: rw [one_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_1 : ValueGroup A K
a : K
⊢ 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
have mk : (MulAction.orbitRel Aˣ K : K → K → Prop) (a * 1) a
Tactic: apply Quotient.sound'
-- 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_1 : ValueGroup A K
a : K
⊢ (MulAction.orbitRel Aˣ K : K → K → Prop) (a * 1) a
have mk : (MulAction.orbitRel Aˣ K : K → K → Prop) a a
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
a_1 : ValueGroup A K
a : K
b_1 : ValueGroup A K
b : K
⊢ 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)
have mk : (MulAction.orbitRel Aˣ K : K → K → Prop) (a * b) (b * a)
Tactic: apply Quotient.sound'
-- 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_1 : ValueGroup A K
a : K
b_1 : ValueGroup A K
b : K
⊢ (MulAction.orbitRel Aˣ K : K → K → Prop) (a * b) (b * a)
have mk : (MulAction.orbitRel Aˣ K : K → K → Prop) (b * a) (b * a)
Tactic: rw [mul_comm]
-- 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_1 : ValueGroup A K
a : K
⊢ HMul.hMul (α := ValueGroup A K) 0 (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a) = 0
have mk : (MulAction.orbitRel Aˣ K : K → K → Prop) (0 * a) 0
Tactic: apply Quotient.sound'
-- 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_1 : ValueGroup A K
a : K
⊢ (MulAction.orbitRel Aˣ K : K → K → Prop) (0 * a) 0
have mk : (MulAction.orbitRel Aˣ K : K → K → Prop) 0 0
Tactic: rw [zero_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_1 : ValueGroup A K
a : K
⊢ HMul.hMul (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a) 0 = 0
have mk : (MulAction.orbitRel Aˣ K : K → K → Prop) (a * 0) 0
Tactic: apply Quotient.sound'
-- 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_1 : ValueGroup A K
a : K
⊢ (MulAction.orbitRel Aˣ K : K → K → Prop) (a * 0) 0
have mk : (MulAction.orbitRel Aˣ K : K → K → Prop) 0 0
Tactic: rw [mul_zero]
-- 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
⊢ Eq.{v + 1} (α := ValueGroup A K) 0⁻¹ 0
have a : (MulAction.orbitRel Aˣ K : K → K → Prop) 0⁻¹ 0
Tactic: apply Quotient.sound'
-- 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
⊢ (MulAction.orbitRel Aˣ K : K → K → Prop) 0⁻¹ 0
have a : (MulAction.orbitRel Aˣ K : K → K → Prop) 0 0
Tactic: rw [inv_zero]
-- 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_1 : ValueGroup A K
a : K
ha : Ne (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a) 0
⊢ 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
have mk : (MulAction.orbitRel Aˣ K : K → K → Prop) (a * a⁻¹) 1
Tactic: apply Quotient.sound'
-- 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_1 : ValueGroup A K
a : K
ha : Ne (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a) 0
⊢ (MulAction.orbitRel Aˣ K : K → K → Prop) (a * a⁻¹) 1
have h : (fun (m : Aˣ) ↦ HSMul.hSMul (β := K) m 1) 1 = a * a⁻¹
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_1 : ValueGroup A K
a : K
ha : Ne (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a) 0
⊢ (fun (m : Aˣ) ↦ HSMul.hSMul (β := K) m 1) 1 = a * a⁻¹
have h : 1 = a * a⁻¹
Tactic: simp only [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_1 : ValueGroup A K
a : K
ha : Ne (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a) 0
⊢ 1 = a * a⁻¹
have apply : a ≠ 0
Tactic: apply (mul_inv_cancel₀ _).symm
-- 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_1 : ValueGroup A K
a : K
ha : Ne (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a) 0
⊢ a ≠ 0
have contrapose : ∀ (ha : a = 0), Eq (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a) 0
Tactic: contrapose ha
Cleared hypotheses: ha
-- 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_1 : ValueGroup A K
a : K
ha : a = 0
⊢ Eq (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a) 0
have rw : Eq.{v + 1} (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) 0) 0
Tactic: rw [ha]
-- 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⦄ (ha : 0 < a) ⦃b c : ValueGroup A K⦄ (hbc : b < c), a * b < a * c
have simp_rw : ∀ ⦃a : ValueGroup A K⦄ (ha : ¬a ≤ 0) ⦃b c : ValueGroup A K⦄ (hbc : ¬c ≤ b), ¬a * c ≤ a * b
Tactic: simp_rw [← not_le]
-- 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_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)
⊢ ¬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)
have 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)
Tactic: contrapose hbc
Cleared hypotheses: hbc
-- 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_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)
⊢ 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)
have 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)
Tactic: obtain ⟨d, hd⟩ := hbc
Cleared hypotheses: hbc
-- 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_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
⊢ 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)
have hd₁ : 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
Cleared hypotheses: hd
-- 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_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
⊢ 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)
have 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)
Tactic: obtain rfl | rfl := hd
Cleared hypotheses: c, hd
-- 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_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)
⊢ 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)
have 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)
Tactic: obtain rfl | rfl := hd
Cleared hypotheses: a, ha, hd
-- 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 : K
⊢ LE.le (α := ValueGroup A K) (Quotient.mk'' (a + b)) (max (Quotient.mk'' a) (Quotient.mk'' b))
have 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))
Tactic: obtain ⟨xa, ya, hya, rfl⟩ := IsFractionRing.div_surjective A a
Cleared hypotheses: a
-- 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
b : K
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))
have 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))))
Tactic: obtain ⟨xb, yb, hyb, rfl⟩ := IsFractionRing.div_surjective A b
Cleared hypotheses: b
-- 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
xa ya : A
hya : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) ya
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))))
have this : 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
-- 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
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)
⊢ LE.le (α := ValueGroup A K)
    (Quotient.mk''
      (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K) +
        HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)))
    (max
      (Quotient.mk''
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K)))
      (Quotient.mk''
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K))))
have this₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
xa ya : A
hya : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) ya
xb yb : A
hyb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) yb
this_1 : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) ya : K) (0 : K)
this : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) yb : K) (0 : K)
⊢ LE.le (α := ValueGroup A K)
    (Quotient.mk''
      (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K) +
        HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K)))
    (max
      (Quotient.mk''
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xa : K) ((algebraMap A K : (a : A) → K) ya : K)))
      (Quotient.mk''
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) xb : K) ((algebraMap A K : (a : A) → K) yb : K))))
have 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))))
Tactic: obtain ⟨c, h | h⟩ := ValuationRing.cond (xa * yb) (xb * ya)