awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit.{u} (M := R) ((algebraMap O R : (a : O) → R) x : R)
hvx : Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
u : Rˣ
hu : (↑u : R) = (algebraMap O R : (a : O) → R) x
h1 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀) (1 : Γ₀)
rw : HMul.hMul (α := Γ₀) (β := Γ₀) (1 : Γ₀) ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) ≤ 1
rw₁ :
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
      ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) ≤
    (v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R)
rw₂ :
  LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (HMul.hMul (α := R) ((algebraMap O R : (a : O) → R) x : R) (↑u⁻¹ : R)) : Γ₀)
    ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
rw₃ : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((↑u : R) * (↑u⁻¹ : R)) : Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀)
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) (1 : Γ₀)
have rw₄ : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀)
Tactic: rw [← one_mul (v _), ← hvx, ← v.map_mul, ← hu, u.mul_inv, hu, hvx, v.map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit.{u} (M := R) ((algebraMap O R : (a : O) → R) x : R)
hvx : Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
u : Rˣ
hu : (↑u : R) = (algebraMap O R : (a : O) → R) x
h1 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀) (1 : Γ₀)
rw : HMul.hMul (α := Γ₀) (β := Γ₀) (1 : Γ₀) ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) ≤ 1
rw₁ :
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
      ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) ≤
    (v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R)
rw₂ :
  LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (HMul.hMul (α := R) ((algebraMap O R : (a : O) → R) x : R) (↑u⁻¹ : R)) : Γ₀)
    ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
rw₃ : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((↑u : R) * (↑u⁻¹ : R)) : Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀)
rw₄ : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀)
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) (1 : Γ₀)
have rw₅ : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
Tactic: rw [← one_mul (v _), ← hvx, ← v.map_mul, ← hu, u.mul_inv, hu, hvx, v.map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit.{u} (M := R) ((algebraMap O R : (a : O) → R) x : R)
hvx : Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
u : Rˣ
hu : (↑u : R) = (algebraMap O R : (a : O) → R) x
h1 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀) (1 : Γ₀)
rw : HMul.hMul (α := Γ₀) (β := Γ₀) (1 : Γ₀) ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) ≤ 1
rw₁ :
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
      ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) ≤
    (v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R)
rw₂ :
  LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (HMul.hMul (α := R) ((algebraMap O R : (a : O) → R) x : R) (↑u⁻¹ : R)) : Γ₀)
    ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
rw₃ : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((↑u : R) * (↑u⁻¹ : R)) : Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀)
rw₄ : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀)
rw₅ : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) (1 : Γ₀)
have rw₆ : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) (1 : Γ₀)
Tactic: rw [← one_mul (v _), ← hvx, ← v.map_mul, ← hu, u.mul_inv, hu, hvx, v.map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit.{u} (M := R) ((algebraMap O R : (a : O) → R) x : R)
hvx : Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
u : Rˣ
hu : (↑u : R) = (algebraMap O R : (a : O) → R) x
h1 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀) (1 : Γ₀)
rw : HMul.hMul (α := Γ₀) (β := Γ₀) (1 : Γ₀) ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) ≤ 1
rw₁ :
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
      ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) ≤
    (v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R)
rw₂ :
  LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (HMul.hMul (α := R) ((algebraMap O R : (a : O) → R) x : R) (↑u⁻¹ : R)) : Γ₀)
    ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
rw₃ : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((↑u : R) * (↑u⁻¹ : R)) : Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀)
rw₄ : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀)
rw₅ : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
rw₆ : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) (1 : Γ₀)
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) (1 : Γ₀)
have rw₇ : LE.le.{v} (α := Γ₀) 1 1
Tactic: rw [← one_mul (v _), ← hvx, ← v.map_mul, ← hu, u.mul_inv, hu, hvx, v.map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit.{u} (M := R) ((algebraMap O R : (a : O) → R) x : R)
hvx : Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
u : Rˣ
hu : (↑u : R) = (algebraMap O R : (a : O) → R) x
h1 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀) (1 : Γ₀)
h2 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) (1 : Γ₀)
r1 : O
hr1 : (algebraMap O R : (a : O) → R) r1 = (↑u : R)
r2 : O
hr2 : (algebraMap O R : (a : O) → R) r2 = (↑u⁻¹ : R)
⊢ Eq.{u + 1} (α := R) ((algebraMap O R : (a : O) → R) (r1 * r2) : R) ((algebraMap O R : (a : O) → R) 1 : R)
have rw : HMul.hMul (α := R) (β := R) ((algebraMap O R : (a : O) → R) r1 : R) ((algebraMap O R : (a : O) → R) r2 : R) =
  (algebraMap O R : (a : O) → R) 1
Tactic: rw [map_mul, map_one, hr1, hr2, Units.mul_inv]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit.{u} (M := R) ((algebraMap O R : (a : O) → R) x : R)
hvx : Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
u : Rˣ
hu : (↑u : R) = (algebraMap O R : (a : O) → R) x
h1 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀) (1 : Γ₀)
h2 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) (1 : Γ₀)
r1 : O
hr1 : (algebraMap O R : (a : O) → R) r1 = (↑u : R)
r2 : O
hr2 : (algebraMap O R : (a : O) → R) r2 = (↑u⁻¹ : R)
rw :
  HMul.hMul (α := R) (β := R) ((algebraMap O R : (a : O) → R) r1 : R) ((algebraMap O R : (a : O) → R) r2 : R) =
    (algebraMap O R : (a : O) → R) 1
⊢ Eq.{u + 1} (α := R) ((algebraMap O R : (a : O) → R) (r1 * r2) : R) ((algebraMap O R : (a : O) → R) 1 : R)
have rw₁ : HMul.hMul (α := R) (β := R) ((algebraMap O R : (a : O) → R) r1 : R) ((algebraMap O R : (a : O) → R) r2 : R) = 1
Tactic: rw [map_mul, map_one, hr1, hr2, Units.mul_inv]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit.{u} (M := R) ((algebraMap O R : (a : O) → R) x : R)
hvx : Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
u : Rˣ
hu : (↑u : R) = (algebraMap O R : (a : O) → R) x
h1 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀) (1 : Γ₀)
h2 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) (1 : Γ₀)
r1 : O
hr1 : (algebraMap O R : (a : O) → R) r1 = (↑u : R)
r2 : O
hr2 : (algebraMap O R : (a : O) → R) r2 = (↑u⁻¹ : R)
rw :
  HMul.hMul (α := R) (β := R) ((algebraMap O R : (a : O) → R) r1 : R) ((algebraMap O R : (a : O) → R) r2 : R) =
    (algebraMap O R : (a : O) → R) 1
rw₁ : HMul.hMul (α := R) (β := R) ((algebraMap O R : (a : O) → R) r1 : R) ((algebraMap O R : (a : O) → R) r2 : R) = 1
⊢ Eq.{u + 1} (α := R) ((algebraMap O R : (a : O) → R) (r1 * r2) : R) ((algebraMap O R : (a : O) → R) 1 : R)
have rw₂ : HMul.hMul (β := R) (↑u : R) ((algebraMap O R : (a : O) → R) r2 : R) = 1
Tactic: rw [map_mul, map_one, hr1, hr2, Units.mul_inv]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit.{u} (M := R) ((algebraMap O R : (a : O) → R) x : R)
hvx : Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
u : Rˣ
hu : (↑u : R) = (algebraMap O R : (a : O) → R) x
h1 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀) (1 : Γ₀)
h2 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) (1 : Γ₀)
r1 : O
hr1 : (algebraMap O R : (a : O) → R) r1 = (↑u : R)
r2 : O
hr2 : (algebraMap O R : (a : O) → R) r2 = (↑u⁻¹ : R)
rw :
  HMul.hMul (α := R) (β := R) ((algebraMap O R : (a : O) → R) r1 : R) ((algebraMap O R : (a : O) → R) r2 : R) =
    (algebraMap O R : (a : O) → R) 1
rw₁ : HMul.hMul (α := R) (β := R) ((algebraMap O R : (a : O) → R) r1 : R) ((algebraMap O R : (a : O) → R) r2 : R) = 1
rw₂ : HMul.hMul (β := R) (↑u : R) ((algebraMap O R : (a : O) → R) r2 : R) = 1
⊢ Eq.{u + 1} (α := R) ((algebraMap O R : (a : O) → R) (r1 * r2) : R) ((algebraMap O R : (a : O) → R) 1 : R)
have rw₃ : (↑u : R) * (↑u⁻¹ : R) = 1
Tactic: rw [map_mul, map_one, hr1, hr2, Units.mul_inv]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit.{u} (M := R) ((algebraMap O R : (a : O) → R) x : R)
hvx : Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
u : Rˣ
hu : (↑u : R) = (algebraMap O R : (a : O) → R) x
h1 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀) (1 : Γ₀)
h2 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) (1 : Γ₀)
r1 : O
hr1 : (algebraMap O R : (a : O) → R) r1 = (↑u : R)
r2 : O
hr2 : (algebraMap O R : (a : O) → R) r2 = (↑u⁻¹ : R)
rw :
  HMul.hMul (α := R) (β := R) ((algebraMap O R : (a : O) → R) r1 : R) ((algebraMap O R : (a : O) → R) r2 : R) =
    (algebraMap O R : (a : O) → R) 1
rw₁ : HMul.hMul (α := R) (β := R) ((algebraMap O R : (a : O) → R) r1 : R) ((algebraMap O R : (a : O) → R) r2 : R) = 1
rw₂ : HMul.hMul (β := R) (↑u : R) ((algebraMap O R : (a : O) → R) r2 : R) = 1
rw₃ : (↑u : R) * (↑u⁻¹ : R) = 1
⊢ Eq.{u + 1} (α := R) ((algebraMap O R : (a : O) → R) (r1 * r2) : R) ((algebraMap O R : (a : O) → R) 1 : R)
have rw₄ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [map_mul, map_one, hr1, hr2, Units.mul_inv]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit.{u} (M := R) ((algebraMap O R : (a : O) → R) x : R)
hvx : Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
u : Rˣ
hu : (↑u : R) = (algebraMap O R : (a : O) → R) x
h1 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀) (1 : Γ₀)
h2 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) (1 : Γ₀)
r1 : O
hr1 : (algebraMap O R : (a : O) → R) r1 = (↑u : R)
r2 : O
hr2 : (algebraMap O R : (a : O) → R) r2 = (↑u⁻¹ : R)
⊢ Eq.{u + 1} (α := R) ((algebraMap O R : (a : O) → R) (r2 * r1) : R) ((algebraMap O R : (a : O) → R) 1 : R)
have rw : HMul.hMul (α := R) (β := R) ((algebraMap O R : (a : O) → R) r2 : R) ((algebraMap O R : (a : O) → R) r1 : R) =
  (algebraMap O R : (a : O) → R) 1
Tactic: rw [map_mul, map_one, hr1, hr2, Units.inv_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit.{u} (M := R) ((algebraMap O R : (a : O) → R) x : R)
hvx : Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
u : Rˣ
hu : (↑u : R) = (algebraMap O R : (a : O) → R) x
h1 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀) (1 : Γ₀)
h2 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) (1 : Γ₀)
r1 : O
hr1 : (algebraMap O R : (a : O) → R) r1 = (↑u : R)
r2 : O
hr2 : (algebraMap O R : (a : O) → R) r2 = (↑u⁻¹ : R)
rw :
  HMul.hMul (α := R) (β := R) ((algebraMap O R : (a : O) → R) r2 : R) ((algebraMap O R : (a : O) → R) r1 : R) =
    (algebraMap O R : (a : O) → R) 1
⊢ Eq.{u + 1} (α := R) ((algebraMap O R : (a : O) → R) (r2 * r1) : R) ((algebraMap O R : (a : O) → R) 1 : R)
have rw₁ : HMul.hMul (α := R) (β := R) ((algebraMap O R : (a : O) → R) r2 : R) ((algebraMap O R : (a : O) → R) r1 : R) = 1
Tactic: rw [map_mul, map_one, hr1, hr2, Units.inv_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit.{u} (M := R) ((algebraMap O R : (a : O) → R) x : R)
hvx : Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
u : Rˣ
hu : (↑u : R) = (algebraMap O R : (a : O) → R) x
h1 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀) (1 : Γ₀)
h2 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) (1 : Γ₀)
r1 : O
hr1 : (algebraMap O R : (a : O) → R) r1 = (↑u : R)
r2 : O
hr2 : (algebraMap O R : (a : O) → R) r2 = (↑u⁻¹ : R)
rw :
  HMul.hMul (α := R) (β := R) ((algebraMap O R : (a : O) → R) r2 : R) ((algebraMap O R : (a : O) → R) r1 : R) =
    (algebraMap O R : (a : O) → R) 1
rw₁ : HMul.hMul (α := R) (β := R) ((algebraMap O R : (a : O) → R) r2 : R) ((algebraMap O R : (a : O) → R) r1 : R) = 1
⊢ Eq.{u + 1} (α := R) ((algebraMap O R : (a : O) → R) (r2 * r1) : R) ((algebraMap O R : (a : O) → R) 1 : R)
have rw₂ : HMul.hMul (α := R) ((algebraMap O R : (a : O) → R) r2 : R) (↑u : R) = 1
Tactic: rw [map_mul, map_one, hr1, hr2, Units.inv_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit.{u} (M := R) ((algebraMap O R : (a : O) → R) x : R)
hvx : Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
u : Rˣ
hu : (↑u : R) = (algebraMap O R : (a : O) → R) x
h1 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀) (1 : Γ₀)
h2 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) (1 : Γ₀)
r1 : O
hr1 : (algebraMap O R : (a : O) → R) r1 = (↑u : R)
r2 : O
hr2 : (algebraMap O R : (a : O) → R) r2 = (↑u⁻¹ : R)
rw :
  HMul.hMul (α := R) (β := R) ((algebraMap O R : (a : O) → R) r2 : R) ((algebraMap O R : (a : O) → R) r1 : R) =
    (algebraMap O R : (a : O) → R) 1
rw₁ : HMul.hMul (α := R) (β := R) ((algebraMap O R : (a : O) → R) r2 : R) ((algebraMap O R : (a : O) → R) r1 : R) = 1
rw₂ : HMul.hMul (α := R) ((algebraMap O R : (a : O) → R) r2 : R) (↑u : R) = 1
⊢ Eq.{u + 1} (α := R) ((algebraMap O R : (a : O) → R) (r2 * r1) : R) ((algebraMap O R : (a : O) → R) 1 : R)
have rw₃ : (↑u⁻¹ : R) * (↑u : R) = 1
Tactic: rw [map_mul, map_one, hr1, hr2, Units.inv_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit.{u} (M := R) ((algebraMap O R : (a : O) → R) x : R)
hvx : Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
u : Rˣ
hu : (↑u : R) = (algebraMap O R : (a : O) → R) x
h1 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀) (1 : Γ₀)
h2 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) (1 : Γ₀)
r1 : O
hr1 : (algebraMap O R : (a : O) → R) r1 = (↑u : R)
r2 : O
hr2 : (algebraMap O R : (a : O) → R) r2 = (↑u⁻¹ : R)
rw :
  HMul.hMul (α := R) (β := R) ((algebraMap O R : (a : O) → R) r2 : R) ((algebraMap O R : (a : O) → R) r1 : R) =
    (algebraMap O R : (a : O) → R) 1
rw₁ : HMul.hMul (α := R) (β := R) ((algebraMap O R : (a : O) → R) r2 : R) ((algebraMap O R : (a : O) → R) r1 : R) = 1
rw₂ : HMul.hMul (α := R) ((algebraMap O R : (a : O) → R) r2 : R) (↑u : R) = 1
rw₃ : (↑u⁻¹ : R) * (↑u : R) = 1
⊢ Eq.{u + 1} (α := R) ((algebraMap O R : (a : O) → R) (r2 * r1) : R) ((algebraMap O R : (a : O) → R) 1 : R)
have rw₄ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [map_mul, map_one, hr1, hr2, Units.inv_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
x y : O
h : x ∣ y
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) y : R) : Γ₀)
    ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
have obtain : ∀ (z : O),
  LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) (x * z) : R) : Γ₀)
    ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
Tactic: obtain ⟨z, rfl⟩ := h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
x z : O
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) (x * z) : R) : Γ₀)
    ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
have grw : (v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) (x * z) : R) ≤
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
Tactic: grw [← mul_one (v (algebraMap O R x)), map_mul, v.map_mul, hv.2 z]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
x z : O
grw :
  (v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) (x * z) : R) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) (x * z) : R) : Γ₀)
    ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
have grw₁ : (v : (a : R) → Γ₀)
    (HMul.hMul (α := R) (β := R) ((algebraMap O R : (a : O) → R) x : R) ((algebraMap O R : (a : O) → R) z : R)) ≤
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
Tactic: grw [← mul_one (v (algebraMap O R x)), map_mul, v.map_mul, hv.2 z]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
x z : O
grw :
  (v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) (x * z) : R) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
grw₁ :
  (v : (a : R) → Γ₀)
      (HMul.hMul (α := R) (β := R) ((algebraMap O R : (a : O) → R) x : R) ((algebraMap O R : (a : O) → R) z : R)) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) (x * z) : R) : Γ₀)
    ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
have grw₂ : HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
    ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) z : R) : Γ₀) ≤
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
Tactic: grw [← mul_one (v (algebraMap O R x)), map_mul, v.map_mul, hv.2 z]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
x z : O
grw :
  (v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) (x * z) : R) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
grw₁ :
  (v : (a : R) → Γ₀)
      (HMul.hMul (α := R) (β := R) ((algebraMap O R : (a : O) → R) x : R) ((algebraMap O R : (a : O) → R) z : R)) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
grw₂ :
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
      ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) z : R) : Γ₀) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) (x * z) : R) : Γ₀)
    ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
have grw₃ : HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀) ≤
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
Tactic: grw [← mul_one (v (algebraMap O R x)), map_mul, v.map_mul, hv.2 z]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
⊢ Nontrivial O ↔ Nontrivial R
have mp : Nontrivial O → Nontrivial R
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
mp : Nontrivial O → Nontrivial R
⊢ Nontrivial O ↔ Nontrivial R
have mpr : Nontrivial R → Nontrivial O
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
h : Nontrivial R
⊢ Nontrivial O
have mpr : ∀ (o0 : O) (ho0 : Eq.{u + 1} (α := R) ((algebraMap O R : (a : O) → R) o0 : R) (0 : R)), Nontrivial O
Tactic: obtain ⟨o0, ho0⟩ := hv.exists_of_le_one (r := 0) (by simp)