awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Extension (goal)
Goal:
A : Type u_2
inst : Ring A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra K A
ΓA : Type u_7
ΓK : Type u_8
inst_3 : LinearOrderedCommGroupWithZero ΓK
inst_4 : LinearOrderedCommGroupWithZero ΓA
vK : Valuation K ΓK
vA : Valuation A ΓA
h : Subring.comap (algebraMap K A) vA.integer = vK.integer
x : K
simp_rw : x ∈ vK.integer ↔ Membership.mem (γ := Subring K) (integer (comap (algebraMap K A) vA)) x
simp_rw₁ :
  Membership.mem (γ := Subring K) (Subring.comap (algebraMap K A) vA.integer) x ↔
    Membership.mem (γ := Subring K) (integer (comap (algebraMap K A) vA)) x
simp_rw₂ :
  Membership.mem (α := A) vA.integer (((algebraMap K A : K →+* A) : (a : K) → A) x : A) ↔
    Membership.mem (γ := Subring K) (integer (comap (algebraMap K A) vA)) x
⊢ LE.le.{u_8} (α := ΓK) ((vK : (a : K) → ΓK) x : ΓK) (1 : ΓK) ↔
    LE.le.{u_7} (α := ΓA) ((comap (algebraMap K A) vA : (a : K) → ΓA) x : ΓA) (1 : ΓA)
have simp_rw₃ : LE.le.{u_7} (α := ΓA) ((vA : (a : A) → ΓA) (((algebraMap K A : K →+* A) : (a : K) → A) x : A) : ΓA) (1 : ΓA) ↔
  LE.le.{u_7} (α := ΓA) ((comap (algebraMap K A) vA : (a : K) → ΓA) x : ΓA) (1 : ΓA)
Tactic: simp_rw [← Valuation.mem_integer_iff, ← h, Subring.mem_comap, mem_integer_iff, comap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Extension (goal)
Goal:
R : Type u_1
A : Type u_2
ΓR_1 : Type u_3
ΓA_1 : Type u_4
inst : CommRing R
inst_1 : Ring A
inst_2 : LinearOrderedCommMonoidWithZero ΓR_1
inst_3 : LinearOrderedCommMonoidWithZero ΓA_1
inst_4 : Algebra R A
vR_1 : Valuation R ΓR_1
vA_1 : Valuation A ΓA_1
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K A
ΓR : Type u_6
ΓA : Type u_7
ΓK : Type u_8
inst_7 : LinearOrderedCommGroupWithZero ΓR
inst_8 : LinearOrderedCommGroupWithZero ΓK
inst_9 : LinearOrderedCommGroupWithZero ΓA
vR : Valuation R ΓR
vK : Valuation K ΓK
vA : Valuation A ΓA
inst_10 : vR.HasExtension vA
x : ↥vR.integer
y : ↥vA.integer
z : A
⊢ (x • y) • z = x • y • z
have simp : HMul.hMul (α := ↥vA.integer) ((algebraMap ↥vR.integer ↥vA.integer : (a : ↥vR.integer) → ↥vA.integer) x : ↥vA.integer)
      y •
    z =
  HMul.hMul (α := A) ((algebraMap (↥vR.integer) A : (a : ↥vR.integer) → A) x : A) (y • z)
Tactic: simp only [Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Extension (goal)
Goal:
R : Type u_1
inst : CommRing R
ΓR : Type u_6
inst_1 : LinearOrderedCommGroupWithZero ΓR
vR : Valuation R ΓR
S : Type u_9
ΓS : Type u_10
inst_2 : CommRing S
inst_3 : LinearOrderedCommGroupWithZero ΓS
inst_4 : Algebra R S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
vS : Valuation S ΓS
inst_6 : vR.HasExtension vS
r : ↥vR.integer
hr :
  IsUnit.{u_9} (M := ↥vS.integer)
    ((algebraMap ↥vR.integer ↥vS.integer : (a : ↥vR.integer) → ↥vS.integer) r : ↥vS.integer)
⊢ IsUnit r
have hx : IsUnit (M := R) ((algebraMap (↥vR.integer) R : (a : ↥vR.integer) → R) r : R)
Tactic: apply (Valuation.integer.integers (v := vR)).isUnit_of_one
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Extension (goal)
Goal:
R : Type u_1
inst : CommRing R
ΓR : Type u_6
inst_1 : LinearOrderedCommGroupWithZero ΓR
vR : Valuation R ΓR
S : Type u_9
ΓS : Type u_10
inst_2 : CommRing S
inst_3 : LinearOrderedCommGroupWithZero ΓS
inst_4 : Algebra R S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
vS : Valuation S ΓS
inst_6 : vR.HasExtension vS
r : ↥vR.integer
hr :
  IsUnit.{u_9} (M := ↥vS.integer)
    ((algebraMap ↥vR.integer ↥vS.integer : (a : ↥vR.integer) → ↥vS.integer) r : ↥vS.integer)
hx : IsUnit (M := R) ((algebraMap (↥vR.integer) R : (a : ↥vR.integer) → R) r : R)
⊢ IsUnit r
have hvx : Eq.{u_6 + 1} (α := ΓR) ((vR : (a : R) → ΓR) ((algebraMap (↥vR.integer) R : (a : ↥vR.integer) → R) r : R) : ΓR) (1 : ΓR)
Tactic: apply (Valuation.integer.integers (v := vR)).isUnit_of_one
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Extension (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
ΓR : Type u_6
inst_1 : LinearOrderedCommGroupWithZero ΓR
vR : Valuation R ΓR
S : Type u_9
ΓS : Type u_10
inst_2 : CommRing S
inst_3 : LinearOrderedCommGroupWithZero ΓS
inst_4 : Algebra R S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
vS : Valuation S ΓS
inst_6 : vR.HasExtension vS
r : ↥vR.integer
hr :
  IsUnit.{u_9} (M := ↥vS.integer)
    ((algebraMap ↥vR.integer ↥vS.integer : (a : ↥vR.integer) → ↥vS.integer) r : ↥vS.integer)
⊢ Eq.{u_6 + 1} (α := ΓR) ((vR : (a : R) → ΓR) ((algebraMap (↥vR.integer) R : (a : ↥vR.integer) → R) r : R) : ΓR)
    (1 : ΓR)
have hr₁ : Eq.{u_10 + 1} (α := ΓS)
  ((vS : (a : S) → ΓS)
      ((algebraMap (↥vS.integer) S : (a : ↥vS.integer) → S)
          ((algebraMap ↥vR.integer ↥vS.integer : (a : ↥vR.integer) → ↥vS.integer) r : ↥vS.integer) :
        S) :
    ΓS)
  (1 : ΓS)
Tactic: apply (Valuation.integer.integers (v := vS)).one_of_isUnit at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Extension (goal)
Goal:
K : Type u_5
L : Type u_6
Γ₀ : Type u_7
Γ₁ : Type u_8
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : LinearOrderedCommGroupWithZero Γ₀
inst_4 : LinearOrderedCommGroupWithZero Γ₁
vK : Valuation K Γ₀
vL : Valuation L Γ₁
inst_5 : vK.HasExtension vL
x : ↥K₀
⊢ Membership.mem (α := L) L₀ ((algebraMap K L : (a : K) → L) (↑x : K) : L)
have rw : LE.le.{u_7} (α := Γ₀) ((vK : (a : K) → Γ₀) (↑x : K) : Γ₀) (1 : Γ₀)
Tactic: rw [mem_valuationSubring_iff, ← _root_.map_one vL, ← _root_.map_one (algebraMap K L),
    val_map_le_iff (vR := vK), _root_.map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Extension (goal)
Goal:
K : Type u_5
L : Type u_6
Γ₀ : Type u_7
Γ₁ : Type u_8
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : LinearOrderedCommGroupWithZero Γ₀
inst_4 : LinearOrderedCommGroupWithZero Γ₁
vK : Valuation K Γ₀
vL : Valuation L Γ₁
inst_5 : vK.HasExtension vL
x : ↥K₀
⊢ Membership.mem (γ := Ideal ↥K₀)
      (Ideal.comap (F := RingHom.{u_5, u_6} ↥K₀ ↥L₀) (algebraMap ↥K₀ ↥L₀) (maximalIdeal ↥L₀)) x ↔
    Membership.mem (γ := Ideal ↥K₀) (maximalIdeal ↥K₀) x
have rw : Membership.mem.{u_6, u_6} (α := ↥L₀) (γ := Ideal ↥L₀) (maximalIdeal ↥L₀)
    ((algebraMap ↥K₀ ↥L₀ : (a : ↥K₀) → ↥L₀) x : ↥L₀) ↔
  Membership.mem (γ := Ideal ↥K₀) (maximalIdeal ↥K₀) x
Tactic: rw [Ideal.mem_comap, algebraMap_mem_maximalIdeal_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Extension (goal)
Goal:
K : Type u_5
L : Type u_6
Γ₀ : Type u_7
Γ₁ : Type u_8
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : LinearOrderedCommGroupWithZero Γ₀
inst_4 : LinearOrderedCommGroupWithZero Γ₁
vK : Valuation K Γ₀
vL : Valuation L Γ₁
inst_5 : vK.HasExtension vL
x : ↥K₀
rw :
  Membership.mem.{u_6, u_6} (α := ↥L₀) (γ := Ideal ↥L₀) (maximalIdeal ↥L₀)
      ((algebraMap ↥K₀ ↥L₀ : (a : ↥K₀) → ↥L₀) x : ↥L₀) ↔
    Membership.mem (γ := Ideal ↥K₀) (maximalIdeal ↥K₀) x
⊢ Membership.mem (γ := Ideal ↥K₀)
      (Ideal.comap (F := RingHom.{u_5, u_6} ↥K₀ ↥L₀) (algebraMap ↥K₀ ↥L₀) (maximalIdeal ↥L₀)) x ↔
    Membership.mem (γ := Ideal ↥K₀) (maximalIdeal ↥K₀) x
have rw₁ : Membership.mem (γ := Ideal ↥K₀) (maximalIdeal ↥K₀) x ↔ Membership.mem (γ := Ideal ↥K₀) (maximalIdeal ↥K₀) x
Tactic: rw [Ideal.mem_comap, algebraMap_mem_maximalIdeal_iff]
-- 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
x : O
hx : IsUnit x
H : ∀ (x : O), LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
u : Oˣ
hu : (↑u : O) = x
⊢ LE.le.{v} (α := Γ₀) (1 : Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
have grw : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
Tactic: grw [← v.map_one, ← (algebraMap O R).map_one, ← u.mul_inv, ← mul_one (v (algebraMap O R x)), hu,
      (algebraMap O R).map_mul, v.map_mul, H (u⁻¹ : Units O)]
-- 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
x : O
hx : IsUnit x
H : ∀ (x : O), LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
u : Oˣ
hu : (↑u : O) = x
grw : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
⊢ LE.le.{v} (α := Γ₀) (1 : Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
have grw₁ : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) 1 : R) : Γ₀)
  ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
Tactic: grw [← v.map_one, ← (algebraMap O R).map_one, ← u.mul_inv, ← mul_one (v (algebraMap O R x)), hu,
      (algebraMap O R).map_mul, v.map_mul, H (u⁻¹ : Units O)]
-- 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
x : O
hx : IsUnit x
H : ∀ (x : O), LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
u : Oˣ
hu : (↑u : O) = x
grw : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
grw₁ :
  LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) 1 : R) : Γ₀)
    ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
⊢ LE.le.{v} (α := Γ₀) (1 : Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
have grw₂ : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) ((↑u : O) * (↑u⁻¹ : O)) : R) : Γ₀)
  ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
Tactic: grw [← v.map_one, ← (algebraMap O R).map_one, ← u.mul_inv, ← mul_one (v (algebraMap O R x)), hu,
      (algebraMap O R).map_mul, v.map_mul, H (u⁻¹ : Units O)]
-- 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
x : O
hx : IsUnit x
H : ∀ (x : O), LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
u : Oˣ
hu : (↑u : O) = x
grw : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
grw₁ :
  LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) 1 : R) : Γ₀)
    ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
grw₂ :
  LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) ((↑u : O) * (↑u⁻¹ : O)) : R) : Γ₀)
    ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
⊢ LE.le.{v} (α := Γ₀) (1 : Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
have grw₃ : (v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) ((↑u : O) * (↑u⁻¹ : O)) : R) ≤
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
Tactic: grw [← v.map_one, ← (algebraMap O R).map_one, ← u.mul_inv, ← mul_one (v (algebraMap O R x)), hu,
      (algebraMap O R).map_mul, v.map_mul, H (u⁻¹ : Units O)]
-- 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
x : O
hx : IsUnit x
H : ∀ (x : O), LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
u : Oˣ
hu : (↑u : O) = x
grw : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
grw₁ :
  LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) 1 : R) : Γ₀)
    ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
grw₂ :
  LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) ((↑u : O) * (↑u⁻¹ : O)) : R) : Γ₀)
    ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
grw₃ :
  (v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) ((↑u : O) * (↑u⁻¹ : O)) : R) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
⊢ LE.le.{v} (α := Γ₀) (1 : Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
have grw₄ : (v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) (x * (↑u⁻¹ : O)) : R) ≤
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
Tactic: grw [← v.map_one, ← (algebraMap O R).map_one, ← u.mul_inv, ← mul_one (v (algebraMap O R x)), hu,
      (algebraMap O R).map_mul, v.map_mul, H (u⁻¹ : Units O)]
-- 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
x : O
hx : IsUnit x
H : ∀ (x : O), LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
u : Oˣ
hu : (↑u : O) = x
grw : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
grw₁ :
  LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) 1 : R) : Γ₀)
    ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
grw₂ :
  LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) ((↑u : O) * (↑u⁻¹ : O)) : R) : Γ₀)
    ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
grw₃ :
  (v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) ((↑u : O) * (↑u⁻¹ : O)) : R) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
grw₄ :
  (v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) (x * (↑u⁻¹ : O)) : R) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
⊢ LE.le.{v} (α := Γ₀) (1 : Γ₀) ((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) (↑u⁻¹ : O) : R)) ≤
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
Tactic: grw [← v.map_one, ← (algebraMap O R).map_one, ← u.mul_inv, ← mul_one (v (algebraMap O R x)), hu,
      (algebraMap O R).map_mul, v.map_mul, H (u⁻¹ : Units O)]
-- 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
x : O
hx : IsUnit x
H : ∀ (x : O), LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
u : Oˣ
hu : (↑u : O) = x
grw : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
grw₁ :
  LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) 1 : R) : Γ₀)
    ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
grw₂ :
  LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) ((↑u : O) * (↑u⁻¹ : O)) : R) : Γ₀)
    ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
grw₃ :
  (v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) ((↑u : O) * (↑u⁻¹ : O)) : R) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
grw₄ :
  (v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) (x * (↑u⁻¹ : O)) : 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) (↑u⁻¹ : O) : R)) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
⊢ LE.le.{v} (α := Γ₀) (1 : Γ₀) ((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) (↑u⁻¹ : O) : R) : Γ₀) ≤
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
Tactic: grw [← v.map_one, ← (algebraMap O R).map_one, ← u.mul_inv, ← mul_one (v (algebraMap O R x)), hu,
      (algebraMap O R).map_mul, v.map_mul, H (u⁻¹ : Units O)]
-- 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
x : O
hx : IsUnit x
H : ∀ (x : O), LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
u : Oˣ
hu : (↑u : O) = x
grw : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
grw₁ :
  LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) 1 : R) : Γ₀)
    ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
grw₂ :
  LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) ((↑u : O) * (↑u⁻¹ : O)) : R) : Γ₀)
    ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
grw₃ :
  (v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) ((↑u : O) * (↑u⁻¹ : O)) : R) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
grw₄ :
  (v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) (x * (↑u⁻¹ : O)) : 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) (↑u⁻¹ : O) : 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) (↑u⁻¹ : O) : R) : Γ₀) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
⊢ LE.le.{v} (α := Γ₀) (1 : Γ₀) ((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 [← v.map_one, ← (algebraMap O R).map_one, ← u.mul_inv, ← mul_one (v (algebraMap O R x)), hu,
      (algebraMap O R).map_mul, v.map_mul, H (u⁻¹ : Units O)]
-- 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 : Γ₀)
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) (1 : Γ₀)
have rw : HMul.hMul (α := Γ₀) (β := Γ₀) (1 : Γ₀) ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) ≤ 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
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) (1 : Γ₀)
have 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)
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)
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) (1 : Γ₀)
have 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) : Γ₀)
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) : Γ₀)
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) (1 : Γ₀)
have rw₃ : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((↑u : R) * (↑u⁻¹ : R)) : Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀)
Tactic: rw [← one_mul (v _), ← hvx, ← v.map_mul, ← hu, u.mul_inv, hu, hvx, v.map_one]