[GOAL]
R : Type u
Γ₀ : Type v
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y : R
hx : x ∈ {x | ↑v x ≤ 1}
hy : y ∈ {x | ↑v x ≤ 1}
⊢ x * y ∈ {x | ↑v x ≤ 1}
[PROOFSTEP]
simp only [Set.mem_setOf_eq, _root_.map_mul, mul_le_one' hx hy]
[GOAL]
R : Type u
Γ₀ : Type v
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ 0 ∈
    {
          toSubsemigroup :=
            { carrier := {x | ↑v x ≤ 1},
              mul_mem' := (_ : ∀ {x y : R}, x ∈ {x | ↑v x ≤ 1} → y ∈ {x | ↑v x ≤ 1} → ↑v (x * y) ≤ 1) },
          one_mem' := (_ : ↑v 1 ≤ 1) }.toSubsemigroup.carrier
[PROOFSTEP]
simp only [Set.mem_setOf_eq, _root_.map_zero, zero_le']
[GOAL]
R : Type u
Γ₀ : Type v
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
hx :
  x ∈
    {
            toSubmonoid :=
              {
                toSubsemigroup :=
                  { carrier := {x | ↑v x ≤ 1},
                    mul_mem' := (_ : ∀ {x y : R}, x ∈ {x | ↑v x ≤ 1} → y ∈ {x | ↑v x ≤ 1} → ↑v (x * y) ≤ 1) },
                one_mem' := (_ : ↑v 1 ≤ 1) },
            add_mem' :=
              (_ :
                ∀ {x y : R},
                  x ∈
                      {
                            toSubsemigroup :=
                              { carrier := {x | ↑v x ≤ 1},
                                mul_mem' :=
                                  (_ : ∀ {x y : R}, x ∈ {x | ↑v x ≤ 1} → y ∈ {x | ↑v x ≤ 1} → ↑v (x * y) ≤ 1) },
                            one_mem' := (_ : ↑v 1 ≤ 1) }.toSubsemigroup.carrier →
                    y ∈
                        {
                              toSubsemigroup :=
                                { carrier := {x | ↑v x ≤ 1},
                                  mul_mem' :=
                                    (_ : ∀ {x y : R}, x ∈ {x | ↑v x ≤ 1} → y ∈ {x | ↑v x ≤ 1} → ↑v (x * y) ≤ 1) },
                              one_mem' := (_ : ↑v 1 ≤ 1) }.toSubsemigroup.carrier →
                      ↑v (x + y) ≤ 1),
            zero_mem' := (_ : ↑v 0 ≤ 1) }.toSubmonoid.toSubsemigroup.carrier
⊢ -x ∈
    {
            toSubmonoid :=
              {
                toSubsemigroup :=
                  { carrier := {x | ↑v x ≤ 1},
                    mul_mem' := (_ : ∀ {x y : R}, x ∈ {x | ↑v x ≤ 1} → y ∈ {x | ↑v x ≤ 1} → ↑v (x * y) ≤ 1) },
                one_mem' := (_ : ↑v 1 ≤ 1) },
            add_mem' :=
              (_ :
                ∀ {x y : R},
                  x ∈
                      {
                            toSubsemigroup :=
                              { carrier := {x | ↑v x ≤ 1},
                                mul_mem' :=
                                  (_ : ∀ {x y : R}, x ∈ {x | ↑v x ≤ 1} → y ∈ {x | ↑v x ≤ 1} → ↑v (x * y) ≤ 1) },
                            one_mem' := (_ : ↑v 1 ≤ 1) }.toSubsemigroup.carrier →
                    y ∈
                        {
                              toSubsemigroup :=
                                { carrier := {x | ↑v x ≤ 1},
                                  mul_mem' :=
                                    (_ : ∀ {x y : R}, x ∈ {x | ↑v x ≤ 1} → y ∈ {x | ↑v x ≤ 1} → ↑v (x * y) ≤ 1) },
                              one_mem' := (_ : ↑v 1 ≤ 1) }.toSubsemigroup.carrier →
                      ↑v (x + y) ≤ 1),
            zero_mem' := (_ : ↑v 0 ≤ 1) }.toSubmonoid.toSubsemigroup.carrier
[PROOFSTEP]
simp only [Set.mem_setOf_eq] at hx 
[GOAL]
R : Type u
Γ₀ : Type v
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
hx : ↑v x ≤ 1
⊢ -x ∈
    {
            toSubmonoid :=
              {
                toSubsemigroup :=
                  { carrier := {x | ↑v x ≤ 1},
                    mul_mem' := (_ : ∀ {x y : R}, x ∈ {x | ↑v x ≤ 1} → y ∈ {x | ↑v x ≤ 1} → ↑v (x * y) ≤ 1) },
                one_mem' := (_ : ↑v 1 ≤ 1) },
            add_mem' :=
              (_ :
                ∀ {x y : R},
                  x ∈
                      {
                            toSubsemigroup :=
                              { carrier := {x | ↑v x ≤ 1},
                                mul_mem' :=
                                  (_ : ∀ {x y : R}, x ∈ {x | ↑v x ≤ 1} → y ∈ {x | ↑v x ≤ 1} → ↑v (x * y) ≤ 1) },
                            one_mem' := (_ : ↑v 1 ≤ 1) }.toSubsemigroup.carrier →
                    y ∈
                        {
                              toSubsemigroup :=
                                { carrier := {x | ↑v x ≤ 1},
                                  mul_mem' :=
                                    (_ : ∀ {x y : R}, x ∈ {x | ↑v x ≤ 1} → y ∈ {x | ↑v x ≤ 1} → ↑v (x * y) ≤ 1) },
                              one_mem' := (_ : ↑v 1 ≤ 1) }.toSubsemigroup.carrier →
                      ↑v (x + y) ≤ 1),
            zero_mem' := (_ : ↑v 0 ≤ 1) }.toSubmonoid.toSubsemigroup.carrier
[PROOFSTEP]
simpa only [Set.mem_setOf_eq, map_neg]
[GOAL]
R : Type u
Γ₀ : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝³ : CommRing O
inst✝² : Algebra O R
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : O
hx : IsUnit x
u : Oˣ
hu : ↑u = x
⊢ 1 ≤ ↑v (↑(algebraMap O R) x)
[PROOFSTEP]
rw [← 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]
[GOAL]
R : Type u
Γ₀ : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝³ : CommRing O
inst✝² : Algebra O R
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : O
hx : IsUnit x
u : Oˣ
hu : ↑u = x
⊢ ↑v (↑(algebraMap O R) x) * ↑v (↑(algebraMap O R) ↑u⁻¹) ≤ ↑v (↑(algebraMap O R) x) * 1
[PROOFSTEP]
exact mul_le_mul_left' (hv.2 (u⁻¹ : Units O)) _
[GOAL]
R : Type u
Γ₀ : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝³ : CommRing O
inst✝² : Algebra O R
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : O
hx : IsUnit (↑(algebraMap O R) x)
hvx : ↑v (↑(algebraMap O R) x) = 1
u : ((fun x => R) x)ˣ
hu : ↑u = ↑(algebraMap O R) x
h1 : ↑v ↑u ≤ 1
⊢ ↑v ↑u⁻¹ ≤ 1
[PROOFSTEP]
rw [← one_mul (v _), ← hvx, ← v.map_mul, ← hu, u.mul_inv, hu, hvx, v.map_one]
[GOAL]
R : Type u
Γ₀ : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝³ : CommRing O
inst✝² : Algebra O R
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : O
hx : IsUnit (↑(algebraMap O R) x)
hvx : ↑v (↑(algebraMap O R) x) = 1
u : ((fun x => R) x)ˣ
hu : ↑u = ↑(algebraMap O R) x
h1 : ↑v ↑u ≤ 1
h2 : ↑v ↑u⁻¹ ≤ 1
r1 : O
hr1 : ↑(algebraMap O R) r1 = ↑u
r2 : O
hr2 : ↑(algebraMap O R) r2 = ↑u⁻¹
⊢ ↑(algebraMap O R) (r1 * r2) = ↑(algebraMap O R) 1
[PROOFSTEP]
rw [RingHom.map_mul, RingHom.map_one, hr1, hr2, Units.mul_inv]
[GOAL]
R : Type u
Γ₀ : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝³ : CommRing O
inst✝² : Algebra O R
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : O
hx : IsUnit (↑(algebraMap O R) x)
hvx : ↑v (↑(algebraMap O R) x) = 1
u : ((fun x => R) x)ˣ
hu : ↑u = ↑(algebraMap O R) x
h1 : ↑v ↑u ≤ 1
h2 : ↑v ↑u⁻¹ ≤ 1
r1 : O
hr1 : ↑(algebraMap O R) r1 = ↑u
r2 : O
hr2 : ↑(algebraMap O R) r2 = ↑u⁻¹
⊢ ↑(algebraMap O R) (r2 * r1) = ↑(algebraMap O R) 1
[PROOFSTEP]
rw [RingHom.map_mul, RingHom.map_one, hr1, hr2, Units.inv_mul]
[GOAL]
R : Type u
Γ₀ : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝³ : CommRing O
inst✝² : Algebra O R
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x y : O
h : x ∣ y
⊢ ↑v (↑(algebraMap O R) y) ≤ ↑v (↑(algebraMap O R) x)
[PROOFSTEP]
let ⟨z, hz⟩ := h
[GOAL]
R : Type u
Γ₀ : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝³ : CommRing O
inst✝² : Algebra O R
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x y : O
h : x ∣ y
z : O
hz : y = x * z
⊢ ↑v (↑(algebraMap O R) y) ≤ ↑v (↑(algebraMap O R) x)
[PROOFSTEP]
rw [← mul_one (v (algebraMap O R x)), hz, RingHom.map_mul, v.map_mul]
[GOAL]
R : Type u
Γ₀ : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝³ : CommRing O
inst✝² : Algebra O R
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x y : O
h : x ∣ y
z : O
hz : y = x * z
⊢ ↑v (↑(algebraMap O R) x) * ↑v (↑(algebraMap O R) z) ≤ ↑v (↑(algebraMap O R) x) * 1
[PROOFSTEP]
exact mul_le_mul_left' (hv.2 z) _
[GOAL]
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : Integers v O
x y : O
h : ↑v (↑(algebraMap O F) x) ≤ ↑v (↑(algebraMap O F) y)
hy : ↑(algebraMap O F) y ≠ 0
⊢ ↑v ((↑(algebraMap O F) y)⁻¹ * ↑(algebraMap O F) x) ≤ 1
[PROOFSTEP]
rw [← v.map_one, ← inv_mul_cancel hy, v.map_mul, v.map_mul]
[GOAL]
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : Integers v O
x y : O
h : ↑v (↑(algebraMap O F) x) ≤ ↑v (↑(algebraMap O F) y)
hy : ↑(algebraMap O F) y ≠ 0
⊢ ↑v (↑(algebraMap O F) y)⁻¹ * ↑v (↑(algebraMap O F) x) ≤ ↑v (↑(algebraMap O F) y)⁻¹ * ↑v (↑(algebraMap O F) y)
[PROOFSTEP]
exact mul_le_mul_left' h _
