awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (hypothesis)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
a b : ValueGroupWithZero R
H :
  a < b ∧
    LE.le (α := ℝ≥0) (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) b : ℝ≥0)
      (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) a : ℝ≥0)
H₁ : a < b
⊢ IsNontrivial R
have H' : LE.le (α := ℝ≥0) (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) b : ℝ≥0)
  (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) a : ℝ≥0)
Tactic: obtain ⟨H, H'⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
a b : ValueGroupWithZero R
H : a < b
H' :
  LE.le (α := ℝ≥0) (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) b : ℝ≥0)
    (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) a : ℝ≥0)
⊢ IsNontrivial R
have neg : ∀ (H : 0 < b)
  (H' :
    LE.le (α := ℝ≥0) (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) b : ℝ≥0)
      (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) 0 : ℝ≥0)),
  IsNontrivial R
Tactic: rcases eq_or_ne a 0 with rfl | ha
Cleared hypotheses: a, H, H'
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
a b : ValueGroupWithZero R
H : a < b
H' :
  LE.le (α := ℝ≥0) (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) b : ℝ≥0)
    (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) a : ℝ≥0)
neg :
  ∀ (H : 0 < b)
    (H' :
      LE.le (α := ℝ≥0) (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) b : ℝ≥0)
        (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) 0 : ℝ≥0)),
    IsNontrivial R
⊢ IsNontrivial R
have neg₁ : ∀ (ha : a ≠ 0), IsNontrivial R
Tactic: rcases eq_or_ne a 0 with rfl | ha
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
a b : ValueGroupWithZero R
H : a < b
H' :
  LE.le (α := ℝ≥0) (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) b : ℝ≥0)
    (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) a : ℝ≥0)
ha : a ≠ 0
⊢ IsNontrivial R
have neg : ∀ (H : 1 < b)
  (H' :
    LE.le (α := ℝ≥0) (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) b : ℝ≥0)
      (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) 1 : ℝ≥0))
  (ha : Ne.{u_3 + 1} (α := ValueGroupWithZero R) 1 0), IsNontrivial R
Tactic: rcases eq_or_ne a 1 with rfl | ha'
Cleared hypotheses: a, H, H', ha
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
a b : ValueGroupWithZero R
H : a < b
H' :
  LE.le (α := ℝ≥0) (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) b : ℝ≥0)
    (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) a : ℝ≥0)
ha : a ≠ 0
neg :
  ∀ (H : 1 < b)
    (H' :
      LE.le (α := ℝ≥0) (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) b : ℝ≥0)
        (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) 1 : ℝ≥0))
    (ha : Ne.{u_3 + 1} (α := ValueGroupWithZero R) 1 0), IsNontrivial R
⊢ IsNontrivial R
have neg₁ : ∀ (ha' : a ≠ 1), IsNontrivial R
Tactic: rcases eq_or_ne a 1 with rfl | ha'
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : CommRing R
inst_2 : ValuativeRel R
inst_3 : MulArchimedean Γ₀
v : Valuation R Γ₀
inst_4 : v.Compatible
⊢ IsRankLeOne R
have rw : MulArchimedean.{u_3} (ValueGroupWithZero R)
Tactic: rw [isRankLeOne_iff_mulArchimedean]
-- 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
x y : ValueGroup A K
a b : K
c d : Aˣ
⊢ Eq (α := Prop) ((fun (a b : K) ↦ ∃ (c : A), c • b = a) ((fun (m : Aˣ) ↦ m • a) c) ((fun (m : Aˣ) ↦ m • b) d))
    ((fun (a b : K) ↦ ∃ (c : A), c • b = a) a b)
have a₁ : (fun (a b : K) ↦ ∃ (c : A), c • b = a) ((fun (m : Aˣ) ↦ m • a) c) ((fun (m : Aˣ) ↦ m • b) d) ↔
  (fun (a b : K) ↦ ∃ (c : A), c • b = a) a b
Tactic: ext
-- 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
x y : ValueGroup A K
a b : K
c d : Aˣ
⊢ (fun (a b : K) ↦ ∃ (c : A), c • b = a) ((fun (m : Aˣ) ↦ m • a) c) ((fun (m : Aˣ) ↦ m • b) d) ↔
    (fun (a b : K) ↦ ∃ (c : A), c • b = a) a b
have a₁ : (fun (a b : K) ↦ ∃ (c : A), c • b = a) ((fun (m : Aˣ) ↦ m • a) c) ((fun (m : Aˣ) ↦ m • b) d) →
  (fun (a b : K) ↦ ∃ (c : A), c • b = a) a b
Tactic: constructor
-- 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
x y : ValueGroup A K
a b : K
c d : Aˣ
a₁ :
  (fun (a b : K) ↦ ∃ (c : A), c • b = a) ((fun (m : Aˣ) ↦ m • a) c) ((fun (m : Aˣ) ↦ m • b) d) →
    (fun (a b : K) ↦ ∃ (c : A), c • b = a) a b
⊢ (fun (a b : K) ↦ ∃ (c : A), c • b = a) ((fun (m : Aˣ) ↦ m • a) c) ((fun (m : Aˣ) ↦ m • b) d) ↔
    (fun (a b : K) ↦ ∃ (c : A), c • b = a) a b
have a₂ : (fun (a b : K) ↦ ∃ (c : A), c • b = a) a b →
  (fun (a b : K) ↦ ∃ (c : A), c • b = a) ((fun (m : Aˣ) ↦ m • a) c) ((fun (m : Aˣ) ↦ m • b) d)
Tactic: constructor
-- 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
x y : ValueGroup A K
a b : K
c d : Aˣ
e : A
he : HSMul.hSMul (β := K) e ((fun (m : Aˣ) ↦ m • b) d) = (fun (m : Aˣ) ↦ m • a) c
⊢ ∃ (c : A), c • b = a
have h : ((↑c⁻¹ : A) * e * (↑d : A)) • b = a
Tactic: use (c⁻¹ : Aˣ) * e * d
-- 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
x y : ValueGroup A K
a b : K
c d : Aˣ
e : A
he : HSMul.hSMul (β := K) e ((fun (m : Aˣ) ↦ m • b) d) = (fun (m : Aˣ) ↦ m • a) c
⊢ ((↑c⁻¹ : A) * e * (↑d : A)) • b = a
have he₁ : c⁻¹ • HSMul.hSMul (β := K) e ((fun (m : Aˣ) ↦ m • b) d) = HSMul.hSMul (β := K) c⁻¹ ((fun (m : Aˣ) ↦ m • a) c)
Tactic: apply_fun fun t => c⁻¹ • t at he
Cleared hypotheses: he
-- 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
x y : ValueGroup A K
a b : K
c d : Aˣ
e : A
he : e • b = a
⊢ ∃ (c_1 : A), c_1 • d • b = c • a
have h : ((↑c : A) * e * (↑d⁻¹ : A)) • d • b = c • a
Tactic: use c * e * (d⁻¹ : 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
x y : ValueGroup A K
a b : K
c d : Aˣ
e : A
he : e • b = a
⊢ ((↑c : A) * e * (↑d⁻¹ : A)) • d • b = c • a
have h : (↑c : A) • e • (↑d⁻¹ : A) • (↑d : A) • b = (↑c : A) • e • b
Tactic: simp_rw [Units.smul_def, ← he, 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
x y : ValueGroup A K
a b : K
c d : Aˣ
e : A
he : e • b = a
⊢ (↑c : A) • e • (↑d⁻¹ : A) • (↑d : A) • b = (↑c : A) • e • b
have h : (↑c : A) • e • ((↑d⁻¹ : A) * (↑d : A)) • b = (↑c : A) • e • b
Tactic: rw [← mul_smul _ _ b, Units.inv_mul, 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
x y : ValueGroup A K
a b : K
c d : Aˣ
e : A
he : e • b = a
h : (↑c : A) • e • ((↑d⁻¹ : A) * (↑d : A)) • b = (↑c : A) • e • b
⊢ (↑c : A) • e • (↑d⁻¹ : A) • (↑d : A) • b = (↑c : A) • e • b
have h₁ : (↑c : A) • e • HSMul.hSMul.{u, v, v} (α := A) 1 b = (↑c : A) • e • b
Tactic: rw [← mul_smul _ _ b, Units.inv_mul, 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
x y : ValueGroup A K
a b : K
c d : Aˣ
e : A
he : e • b = a
h : (↑c : A) • e • ((↑d⁻¹ : A) * (↑d : A)) • b = (↑c : A) • e • b
h₁ : (↑c : A) • e • HSMul.hSMul.{u, v, v} (α := A) 1 b = (↑c : A) • e • b
⊢ (↑c : A) • e • (↑d⁻¹ : A) • (↑d : A) • b = (↑c : A) • e • b
have h₂ : (↑c : A) • e • b = (↑c : A) • e • b
Tactic: rw [← mul_smul _ _ b, Units.inv_mul, 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
x y : ValueGroup A K
a b : K
c d : Aˣ
⊢ Eq.{v + 1} (α := ValueGroup A K)
    ((fun (a b : K) ↦ (Quotient.mk'' (a * b) : Quotient (MulAction.orbitRel.{u, v} Aˣ K))) ((fun (m : Aˣ) ↦ m • a) c)
      ((fun (m : Aˣ) ↦ m • b) d))
    ((fun (a b : K) ↦ (Quotient.mk'' (a * b) : Quotient (MulAction.orbitRel.{u, v} Aˣ K))) a b)
have a₁ : (MulAction.orbitRel Aˣ K : K → K → Prop) (HMul.hMul (α := K) ((fun (m : Aˣ) ↦ m • a) c) ((fun (m : Aˣ) ↦ m • b) d))
  (a * 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
x y : ValueGroup A K
a b : K
c d : Aˣ
⊢ (MulAction.orbitRel Aˣ K : K → K → Prop) (c • a * d • b) (a * b)
have h : (fun (m : Aˣ) ↦ m • (a * b)) (c * d) = c • a * d • b
Tactic: use c * d
-- 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
x y : ValueGroup A K
a b : K
c d : Aˣ
⊢ (fun (m : Aˣ) ↦ m • (a * b)) (c * d) = c • a * d • b
have h : HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑c : A) : K)
    (HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑d : A) : K) (a * b)) =
  HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑c : A) : K) a *
    HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑d : A) : K) b
Tactic: simp only [mul_smul, Algebra.smul_def, Units.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
x : ValueGroup A K
a : K
b : Aˣ
⊢ Eq.{v + 1} (α := ValueGroup A K)
    ((fun (a : K) ↦ (Quotient.mk'' a⁻¹ : Quotient (MulAction.orbitRel.{u, v} Aˣ K))) ((fun (m : Aˣ) ↦ m • a) b))
    ((fun (a : K) ↦ (Quotient.mk'' a⁻¹ : Quotient (MulAction.orbitRel.{u, v} Aˣ K))) a)
have a₁ : (MulAction.orbitRel Aˣ K : K → K → Prop) ((fun (m : Aˣ) ↦ m • a) 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
x : ValueGroup A K
a : K
b : Aˣ
⊢ (MulAction.orbitRel Aˣ K : K → K → Prop) ((fun (m : Aˣ) ↦ m • a) b)⁻¹ a⁻¹
have h : Eq.{v + 1} (α := K) ((fun (m : Aˣ) ↦ m • a⁻¹) b⁻¹) ((fun (m : Aˣ) ↦ m • a) b)⁻¹
Tactic: use b⁻¹
-- 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
x : ValueGroup A K
a : K
b : Aˣ
⊢ b⁻¹ • a⁻¹ = (b • a)⁻¹
have h : (↑b⁻¹ : A) • a⁻¹ = (b • a)⁻¹
Tactic: rw [Units.smul_def, Units.smul_def, Algebra.smul_def, Algebra.smul_def, mul_inv,
          map_units_inv]
-- 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
x : ValueGroup A K
a : K
b : Aˣ
h : (↑b⁻¹ : A) • a⁻¹ = (b • a)⁻¹
⊢ b⁻¹ • a⁻¹ = (b • a)⁻¹
have h₁ : (↑b⁻¹ : A) • a⁻¹ = ((↑b : A) • a)⁻¹
Tactic: rw [Units.smul_def, Units.smul_def, Algebra.smul_def, Algebra.smul_def, mul_inv,
          map_units_inv]
-- 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
x : ValueGroup A K
a : K
b : Aˣ
h : (↑b⁻¹ : A) • a⁻¹ = (b • a)⁻¹
h₁ : (↑b⁻¹ : A) • a⁻¹ = ((↑b : A) • a)⁻¹
⊢ b⁻¹ • a⁻¹ = (b • a)⁻¹
have h₂ : HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑b⁻¹ : A) : K) a⁻¹ = ((↑b : A) • a)⁻¹
Tactic: rw [Units.smul_def, Units.smul_def, Algebra.smul_def, Algebra.smul_def, mul_inv,
          map_units_inv]
-- 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
x : ValueGroup A K
a : K
b : Aˣ
h : (↑b⁻¹ : A) • a⁻¹ = (b • a)⁻¹
h₁ : (↑b⁻¹ : A) • a⁻¹ = ((↑b : A) • a)⁻¹
h₂ : HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑b⁻¹ : A) : K) a⁻¹ = ((↑b : A) • a)⁻¹
⊢ b⁻¹ • a⁻¹ = (b • a)⁻¹
have h₃ : HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑b⁻¹ : A) : K) a⁻¹ =
  (HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑b : A) : K) a)⁻¹
Tactic: rw [Units.smul_def, Units.smul_def, Algebra.smul_def, Algebra.smul_def, mul_inv,
          map_units_inv]
-- 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
x : ValueGroup A K
a : K
b : Aˣ
h : (↑b⁻¹ : A) • a⁻¹ = (b • a)⁻¹
h₁ : (↑b⁻¹ : A) • a⁻¹ = ((↑b : A) • a)⁻¹
h₂ : HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑b⁻¹ : A) : K) a⁻¹ = ((↑b : A) • a)⁻¹
h₃ :
  HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑b⁻¹ : A) : K) a⁻¹ =
    (HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑b : A) : K) a)⁻¹
⊢ b⁻¹ • a⁻¹ = (b • a)⁻¹
have h₄ : HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑b⁻¹ : A) : K) a⁻¹ =
  HMul.hMul (α := K) (((algebraMap A K : (a : A) → K) (↑b : A))⁻¹ : K) a⁻¹
Tactic: rw [Units.smul_def, Units.smul_def, Algebra.smul_def, Algebra.smul_def, mul_inv,
          map_units_inv]
-- 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
x : ValueGroup A K
a : K
b : Aˣ
h : (↑b⁻¹ : A) • a⁻¹ = (b • a)⁻¹
h₁ : (↑b⁻¹ : A) • a⁻¹ = ((↑b : A) • a)⁻¹
h₂ : HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑b⁻¹ : A) : K) a⁻¹ = ((↑b : A) • a)⁻¹
h₃ :
  HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑b⁻¹ : A) : K) a⁻¹ =
    (HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑b : A) : K) a)⁻¹
h₄ :
  HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑b⁻¹ : A) : K) a⁻¹ =
    HMul.hMul (α := K) (((algebraMap A K : (a : A) → K) (↑b : A))⁻¹ : K) a⁻¹
⊢ b⁻¹ • a⁻¹ = (b • a)⁻¹
have h₅ : HMul.hMul (α := K) (((algebraMap A K : (a : A) → K) (↑b : A))⁻¹ : K) a⁻¹ =
  HMul.hMul (α := K) (((algebraMap A K : (a : A) → K) (↑b : A))⁻¹ : K) a⁻¹
Tactic: rw [Units.smul_def, Units.smul_def, Algebra.smul_def, Algebra.smul_def, mul_inv,
          map_units_inv]
-- 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
c : Eq.{v + 1} (α := ValueGroup A K) 0 1
⊢ False
have obtain : ∀ (d : Aˣ) (hd : Eq.{v + 1} (α := K) ((fun (m : Aˣ) ↦ HSMul.hSMul (β := K) m 1) d) 0), False
Tactic: obtain ⟨d, hd⟩ := Quotient.exact' c
-- 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
c : Eq.{v + 1} (α := ValueGroup A K) 0 1
d : Aˣ
hd : Eq.{v + 1} (α := K) ((fun (m : Aˣ) ↦ HSMul.hSMul (β := K) m 1) d) 0
⊢ False
have hd₁ : HSMul.hSMul (β := K) d⁻¹ ((fun (m : Aˣ) ↦ HSMul.hSMul (β := K) m 1) d) = HSMul.hSMul (β := K) d⁻¹ 0
Tactic: apply_fun fun t => d⁻¹ • t 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 b : ValueGroup A K
⊢ a ≤ b ∨ b ≤ a
have mk : ∀ (a : K),
  Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a ≤ b ∨ b ≤ Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a
Tactic: rcases a with ⟨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
a_1 b : ValueGroup A K
a : K
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a ≤ b ∨ b ≤ Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a
have mk : ∀ (b : K),
  LE.le (α := 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) b)
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a)
Tactic: rcases b with ⟨b⟩
-- 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 b_1 : ValueGroup A K
a b : K
⊢ LE.le (α := 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) b)
      (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) a)
have mk : ∀ (xa ya : A) (hya : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) 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) b) ∨
    LE.le (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b)
      (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 ⟨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
a b_1 : ValueGroup A K
b : K
xa ya : A
hya : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) 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) b) ∨
    LE.le (α := ValueGroup A K) (Quot.mk (⇑(MulAction.orbitRel Aˣ K) : K → K → Prop) b)
      (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 : ∀ (xb yb : A) (hyb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) 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 ⟨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
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
⊢ 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 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
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 : Ne.{v + 1} (α := K) ((algebraMap A K : (a : A) → K) ya : 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 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