[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : OrderedSemiring S
abv f g : AbsoluteValue R S
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := f
[GOAL]
case mk.mk
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : OrderedSemiring S
abv g : AbsoluteValue R S
toFun✝ : R → S
map_mul'✝ : ∀ (x y : R), toFun✝ (x * y) = toFun✝ x * toFun✝ y
nonneg'✝ : ∀ (x : R), 0 ≤ MulHom.toFun { toFun := toFun✝, map_mul' := map_mul'✝ } x
eq_zero'✝ : ∀ (x : R), MulHom.toFun { toFun := toFun✝, map_mul' := map_mul'✝ } x = 0 ↔ x = 0
add_le'✝ :
  ∀ (x y : R),
    MulHom.toFun { toFun := toFun✝, map_mul' := map_mul'✝ } (x + y) ≤
      MulHom.toFun { toFun := toFun✝, map_mul' := map_mul'✝ } x +
        MulHom.toFun { toFun := toFun✝, map_mul' := map_mul'✝ } y
h :
  (fun f => f.toFun)
      { toMulHom := { toFun := toFun✝, map_mul' := map_mul'✝ }, nonneg' := nonneg'✝, eq_zero' := eq_zero'✝,
        add_le' := add_le'✝ } =
    (fun f => f.toFun) g
⊢ { toMulHom := { toFun := toFun✝, map_mul' := map_mul'✝ }, nonneg' := nonneg'✝, eq_zero' := eq_zero'✝,
      add_le' := add_le'✝ } =
    g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : OrderedSemiring S
abv : AbsoluteValue R S
toFun✝¹ : R → S
map_mul'✝¹ : ∀ (x y : R), toFun✝¹ (x * y) = toFun✝¹ x * toFun✝¹ y
nonneg'✝¹ : ∀ (x : R), 0 ≤ MulHom.toFun { toFun := toFun✝¹, map_mul' := map_mul'✝¹ } x
eq_zero'✝¹ : ∀ (x : R), MulHom.toFun { toFun := toFun✝¹, map_mul' := map_mul'✝¹ } x = 0 ↔ x = 0
add_le'✝¹ :
  ∀ (x y : R),
    MulHom.toFun { toFun := toFun✝¹, map_mul' := map_mul'✝¹ } (x + y) ≤
      MulHom.toFun { toFun := toFun✝¹, map_mul' := map_mul'✝¹ } x +
        MulHom.toFun { toFun := toFun✝¹, map_mul' := map_mul'✝¹ } y
toFun✝ : R → S
map_mul'✝ : ∀ (x y : R), toFun✝ (x * y) = toFun✝ x * toFun✝ y
nonneg'✝ : ∀ (x : R), 0 ≤ MulHom.toFun { toFun := toFun✝, map_mul' := map_mul'✝ } x
eq_zero'✝ : ∀ (x : R), MulHom.toFun { toFun := toFun✝, map_mul' := map_mul'✝ } x = 0 ↔ x = 0
add_le'✝ :
  ∀ (x y : R),
    MulHom.toFun { toFun := toFun✝, map_mul' := map_mul'✝ } (x + y) ≤
      MulHom.toFun { toFun := toFun✝, map_mul' := map_mul'✝ } x +
        MulHom.toFun { toFun := toFun✝, map_mul' := map_mul'✝ } y
h :
  (fun f => f.toFun)
      { toMulHom := { toFun := toFun✝¹, map_mul' := map_mul'✝¹ }, nonneg' := nonneg'✝¹, eq_zero' := eq_zero'✝¹,
        add_le' := add_le'✝¹ } =
    (fun f => f.toFun)
      { toMulHom := { toFun := toFun✝, map_mul' := map_mul'✝ }, nonneg' := nonneg'✝, eq_zero' := eq_zero'✝,
        add_le' := add_le'✝ }
⊢ { toMulHom := { toFun := toFun✝¹, map_mul' := map_mul'✝¹ }, nonneg' := nonneg'✝¹, eq_zero' := eq_zero'✝¹,
      add_le' := add_le'✝¹ } =
    { toMulHom := { toFun := toFun✝, map_mul' := map_mul'✝ }, nonneg' := nonneg'✝, eq_zero' := eq_zero'✝,
      add_le' := add_le'✝ }
[PROOFSTEP]
congr
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : OrderedSemiring S
abv : AbsoluteValue R S
h : IsLeftRegular (↑abv 1)
⊢ (fun x => ↑abv 1 * x) (↑abv 1) = (fun x => ↑abv 1 * x) 1
[PROOFSTEP]
simp [← abv.map_mul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : OrderedSemiring S
abv : AbsoluteValue R S
a b c : R
⊢ ↑abv (a - c) ≤ ↑abv (a - b) + ↑abv (b - c)
[PROOFSTEP]
simpa [sub_eq_add_neg, add_assoc] using abv.add_le (a - b) (b - c)
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : OrderedRing S
abv : AbsoluteValue R S
a b : R
⊢ ↑abv a ≤ ↑abv (a - b) + ↑abv b
[PROOFSTEP]
simpa using abv.add_le (a - b) b
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : OrderedCommRing S
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
⊢ ↑abv (-a) = ↑abv a
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : OrderedCommRing S
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : a = 0
⊢ ↑abv (-a) = ↑abv a
[PROOFSTEP]
simp [ha]
[GOAL]
case neg
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : OrderedCommRing S
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ ↑abv (-a) = ↑abv a
[PROOFSTEP]
refine' (mul_self_eq_mul_self_iff.mp (by rw [← abv.map_mul, neg_mul_neg, abv.map_mul])).resolve_right _
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : OrderedCommRing S
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ ↑abv (-a) * ↑abv (-a) = ↑abv a * ↑abv a
[PROOFSTEP]
rw [← abv.map_mul, neg_mul_neg, abv.map_mul]
[GOAL]
case neg
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : OrderedCommRing S
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ ¬↑abv (-a) = -↑abv a
[PROOFSTEP]
exact ((neg_lt_zero.mpr (abv.pos ha)).trans (abv.pos (neg_ne_zero.mpr ha))).ne'
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : OrderedCommRing S
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a b : R
⊢ ↑abv (a - b) = ↑abv (b - a)
[PROOFSTEP]
rw [← neg_sub, abv.map_neg]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrderedCommRing S
abv : AbsoluteValue R S
a b : R
⊢ ↑abv b - ↑abv a ≤ ↑abv (a - b)
[PROOFSTEP]
rw [abv.map_sub]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrderedCommRing S
abv : AbsoluteValue R S
a b : R
⊢ ↑abv b - ↑abv a ≤ ↑abv (b - a)
[PROOFSTEP]
apply abv.le_sub
[GOAL]
S : Type u_1
inst✝² : OrderedRing S
R : Type u_2
inst✝¹ : Ring R
abv : R → S
inst✝ : IsAbsoluteValue abv
a b c : R
⊢ abv (a - c) ≤ abv (a - b) + abv (b - c)
[PROOFSTEP]
simpa [sub_eq_add_neg, add_assoc] using abv_add abv (a - b) (b - c)
