/-
Copyright (c) 2021 Anne Baanen. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro, Anne Baanen

! This file was ported from Lean 3 source module algebra.order.absolute_value
! leanprover-community/mathlib commit fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.GroupWithZero.Units.Lemmas
import Mathlib.Algebra.Order.Field.Defs
import Mathlib.Algebra.Order.Hom.Basic
import Mathlib.Algebra.Ring.Regular

/-!
# Absolute values

This file defines a bundled type of absolute values `AbsoluteValue R S`.

## Main definitions

 * `AbsoluteValue R S` is the type of absolute values on `R` mapping to `S`.
 * `AbsoluteValue.abs` is the "standard" absolute value on `S`, mapping negative `x` to `-x`.
 * `AbsoluteValue.toMonoidWithZeroHom`: absolute values mapping to a
   linear ordered field preserve `0`, `*` and `1`
 * `IsAbsoluteValue`: a type class stating that `f : β → α` satisfies the axioms of an absolute
   value
-/


/-- `AbsoluteValue R S` is the type of absolute values on `R` mapping to `S`:
the maps that preserve `*`, are nonnegative, positive definite and satisfy the triangle equality. -/
structure AbsoluteValue: {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : OrderedSemiring S] →
        (toMulHom : R →ₙ* S) →
          (∀ (x : R), 0 ≤ MulHom.toFun toMulHom x) →
            (∀ (x : R), MulHom.toFun toMulHom x = 0 ↔ x = 0) →
              (∀ (x y : R), MulHom.toFun toMulHom (x + y) ≤ MulHom.toFun toMulHom x + MulHom.toFun toMulHom y) →
                AbsoluteValue R S
AbsoluteValue (R: Type ?u.2
R S: Type ?u.5
S : Type _: Type (?u.2+1)
Type _) [Semiring: Type ?u.8 → Type ?u.8
Semiring R: Type ?u.2
R] [OrderedSemiring: Type ?u.11 → Type ?u.11
OrderedSemiring S: Type ?u.5
S] extends R: Type ?u.2
R →ₙ* S: Type ?u.5
S where
  /-- The absolute value is nonnegative -/
  nonneg': ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedSemiring S] (self : AbsoluteValue R S) (x : R),
  0 ≤ MulHom.toFun self.toMulHom x
nonneg' : ∀ x: ?m.348
x, 0: ?m.353
0 ≤ toFun: R → S
toFun x: ?m.348
x
  /-- The absolute value is positive definitive -/
  eq_zero': ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedSemiring S] (self : AbsoluteValue R S) (x : R),
  MulHom.toFun self.toMulHom x = 0 ↔ x = 0
eq_zero' : ∀ x: ?m.652
x, toFun: R → S
toFun x: ?m.652
x = 0: ?m.657
0 ↔ x: ?m.652
x = 0: ?m.675
0
  /-- The absolute value satisfies the triangle inequality -/
  add_le': ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedSemiring S] (self : AbsoluteValue R S) (x y : R),
  MulHom.toFun self.toMulHom (x + y) ≤ MulHom.toFun self.toMulHom x + MulHom.toFun self.toMulHom y
add_le' : ∀ x: ?m.851
x y: ?m.854
y, toFun: R → S
toFun (x: ?m.851
x + y: ?m.854
y) ≤ toFun: R → S
toFun x: ?m.851
x + toFun: R → S
toFun y: ?m.854
y
#align absolute_value AbsoluteValue: (R : Type u_1) → (S : Type u_2) → [inst : Semiring R] → [inst : OrderedSemiring S] → Type (maxu_1u_2)
AbsoluteValue

namespace AbsoluteValue

-- Porting note: Removing nolints.
-- attribute [nolint doc_blame] AbsoluteValue.toMulHom

section OrderedSemiring

section Semiring

variable {R: Type ?u.15366
R S: Type ?u.4874
S : Type _: Type (?u.14362+1)
Type _} [Semiring: Type ?u.3627 → Type ?u.3627
Semiring R: Type ?u.1954
R] [OrderedSemiring: Type ?u.7335 → Type ?u.7335
OrderedSemiring S: Type ?u.3624
S] (abv: AbsoluteValue R S
abv : AbsoluteValue: (R : Type ?u.1967) → (S : Type ?u.1966) → [inst : Semiring R] → [inst : OrderedSemiring S] → Type (max?u.1967?u.1966)
AbsoluteValue R: Type ?u.1954
R S: Type ?u.1957
S)

instance zeroHomClass: {R : Type u_1} →
  {S : Type u_2} → [inst : Semiring R] → [inst_1 : OrderedSemiring S] → ZeroHomClass (AbsoluteValue R S) R S
zeroHomClass : ZeroHomClass: Type ?u.2022 →
  (M : outParam (Type ?u.2021)) →
    (N : outParam (Type ?u.2020)) → [inst : Zero M] → [inst : Zero N] → Type (max(max?u.2022?u.2021)?u.2020)
ZeroHomClass (AbsoluteValue: (R : Type ?u.2024) → (S : Type ?u.2023) → [inst : Semiring R] → [inst : OrderedSemiring S] → Type (max?u.2024?u.2023)
AbsoluteValue R: Type ?u.1987
R S: Type ?u.1990
S) R: Type ?u.1987
R S: Type ?u.1990
S where
  coe f: ?m.2433
f := f: ?m.2433
f.toFun: {M : Type ?u.2446} → {N : Type ?u.2445} → [inst : Mul M] → [inst_1 : Mul N] → (M →ₙ* N) → M → N
toFun
  coe_injective' f: ?m.2743
f g: ?m.2746
g h: ?m.2749
h := by
Goals accomplished! 🐙
    R: Type ?u.1987

S: Type ?u.1990

inst✝¹: Semiring R

inst✝: OrderedSemiring S

abv, f, g: AbsoluteValue R S

h: (fun f => f.toFun) f = (fun f => f.toFun) g

f = gobtain ⟨⟨_, _⟩, _⟩: AbsoluteValue R S
⟨⟨_, _⟩: R →ₙ* S
⟨_: R → S
_⟨_, _⟩: R →ₙ* S
, _: ∀ (x y : R), toFun✝ (x * y) = toFun✝ x * toFun✝ y
_⟨_, _⟩: R →ₙ* S
⟩⟨⟨_, _⟩, _⟩: AbsoluteValue R S
, _: unknown free variable '_uniq.2836'
_⟨⟨_, _⟩, _⟩: AbsoluteValue R S
⟩ := f: AbsoluteValue R S
fR: Type ?u.1987

S: Type ?u.1990

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

mk.mk{ toMulHom := { toFun := toFun✝, map_mul' := map_mul'✝ }, nonneg' := nonneg'✝, eq_zero' := eq_zero'✝,
    add_le' := add_le'✝ } =   g
    R: Type ?u.1987

S: Type ?u.1990

inst✝¹: Semiring R

inst✝: OrderedSemiring S

abv, f, g: AbsoluteValue R S

h: (fun f => f.toFun) f = (fun f => f.toFun) g

f = gobtain ⟨⟨_, _⟩, _⟩: AbsoluteValue R S
⟨⟨_, _⟩: R →ₙ* S
⟨_: R → S
_⟨_, _⟩: R →ₙ* S
, _: ∀ (x y : R), toFun✝ (x * y) = toFun✝ x * toFun✝ y
_⟨_, _⟩: R →ₙ* S
⟩⟨⟨_, _⟩, _⟩: AbsoluteValue R S
, _: unknown free variable '_uniq.2920'
_⟨⟨_, _⟩, _⟩: AbsoluteValue R S
⟩ := g: AbsoluteValue R S
gR: Type ?u.1987

S: Type ?u.1990

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'✝ }

mk.mk.mk.mk{ 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'✝ }
    R: Type ?u.1987

S: Type ?u.1990

inst✝¹: Semiring R

inst✝: OrderedSemiring S

abv, f, g: AbsoluteValue R S

h: (fun f => f.toFun) f = (fun f => f.toFun) g

f = gcongr
Goals accomplished! 🐙
  map_zero f: ?m.2762
f := (f: ?m.2762
f.eq_zero': ∀ {R : Type ?u.2765} {S : Type ?u.2764} [inst : Semiring R] [inst_1 : OrderedSemiring S] (self : AbsoluteValue R S)
  (x : R), MulHom.toFun self.toMulHom x = 0 ↔ x = 0
eq_zero' _: ?m.2766
_).2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 rfl: ∀ {α : Sort ?u.2784} {a : α}, a = a
rfl
#align absolute_value.zero_hom_class AbsoluteValue.zeroHomClass: {R : Type u_1} →
  {S : Type u_2} → [inst : Semiring R] → [inst_1 : OrderedSemiring S] → ZeroHomClass (AbsoluteValue R S) R S
AbsoluteValue.zeroHomClass

instance mulHomClass: MulHomClass (AbsoluteValue R S) R S
mulHomClass : MulHomClass: Type ?u.3656 →
  (M : outParam (Type ?u.3655)) →
    (N : outParam (Type ?u.3654)) → [inst : Mul M] → [inst : Mul N] → Type (max(max?u.3656?u.3655)?u.3654)
MulHomClass (AbsoluteValue: (R : Type ?u.3658) → (S : Type ?u.3657) → [inst : Semiring R] → [inst : OrderedSemiring S] → Type (max?u.3658?u.3657)
AbsoluteValue R: Type ?u.3621
R S: Type ?u.3624
S) R: Type ?u.3621
R S: Type ?u.3624
S :=
  { AbsoluteValue.zeroHomClass: {R : Type ?u.4001} →
  {S : Type ?u.4000} → [inst : Semiring R] → [inst_1 : OrderedSemiring S] → ZeroHomClass (AbsoluteValue R S) R S
AbsoluteValue.zeroHomClass with map_mul := fun f: ?m.4709
f => f: ?m.4709
f.map_mul': ∀ {M : Type ?u.4729} {N : Type ?u.4728} [inst : Mul M] [inst_1 : Mul N] (self : M →ₙ* N) (x y : M),
  MulHom.toFun self (x * y) = MulHom.toFun self x * MulHom.toFun self y
map_mul' }
#align absolute_value.mul_hom_class AbsoluteValue.mulHomClass: {R : Type u_1} →
  {S : Type u_2} → [inst : Semiring R] → [inst_1 : OrderedSemiring S] → MulHomClass (AbsoluteValue R S) R S
AbsoluteValue.mulHomClass

instance nonnegHomClass: {R : Type u_1} →
  {S : Type u_2} → [inst : Semiring R] → [inst_1 : OrderedSemiring S] → NonnegHomClass (AbsoluteValue R S) R S
nonnegHomClass : NonnegHomClass: Type ?u.4906 →
  outParam (Type ?u.4905) →
    (β : outParam (Type ?u.4904)) → [inst : Zero β] → [inst : LE β] → Type (max(max?u.4906?u.4905)?u.4904)
NonnegHomClass (AbsoluteValue: (R : Type ?u.4908) → (S : Type ?u.4907) → [inst : Semiring R] → [inst : OrderedSemiring S] → Type (max?u.4908?u.4907)
AbsoluteValue R: Type ?u.4871
R S: Type ?u.4874
S) R: Type ?u.4871
R S: Type ?u.4874
S :=
  { AbsoluteValue.zeroHomClass: {R : Type ?u.5226} →
  {S : Type ?u.5225} → [inst : Semiring R] → [inst_1 : OrderedSemiring S] → ZeroHomClass (AbsoluteValue R S) R S
AbsoluteValue.zeroHomClass with map_nonneg := fun f: ?m.5776
f => f: ?m.5776
f.nonneg': ∀ {R : Type ?u.5779} {S : Type ?u.5778} [inst : Semiring R] [inst_1 : OrderedSemiring S] (self : AbsoluteValue R S)
  (x : R), 0 ≤ MulHom.toFun self.toMulHom x
nonneg' }
#align absolute_value.nonneg_hom_class AbsoluteValue.nonnegHomClass: {R : Type u_1} →
  {S : Type u_2} → [inst : Semiring R] → [inst_1 : OrderedSemiring S] → NonnegHomClass (AbsoluteValue R S) R S
AbsoluteValue.nonnegHomClass

instance subadditiveHomClass: {R : Type u_1} →
  {S : Type u_2} → [inst : Semiring R] → [inst_1 : OrderedSemiring S] → SubadditiveHomClass (AbsoluteValue R S) R S
subadditiveHomClass : SubadditiveHomClass: Type ?u.5958 →
  (α : outParam (Type ?u.5957)) →
    (β : outParam (Type ?u.5956)) →
      [inst : Add α] → [inst : Add β] → [inst : LE β] → Type (max(max?u.5958?u.5957)?u.5956)
SubadditiveHomClass (AbsoluteValue: (R : Type ?u.5960) → (S : Type ?u.5959) → [inst : Semiring R] → [inst : OrderedSemiring S] → Type (max?u.5960?u.5959)
AbsoluteValue R: Type ?u.5923
R S: Type ?u.5926
S) R: Type ?u.5923
R S: Type ?u.5926
S :=
  { AbsoluteValue.zeroHomClass: {R : Type ?u.6389} →
  {S : Type ?u.6388} → [inst : Semiring R] → [inst_1 : OrderedSemiring S] → ZeroHomClass (AbsoluteValue R S) R S
AbsoluteValue.zeroHomClass with map_add_le_add := fun f: ?m.7174
f => f: ?m.7174
f.add_le': ∀ {R : Type ?u.7177} {S : Type ?u.7176} [inst : Semiring R] [inst_1 : OrderedSemiring S] (self : AbsoluteValue R S)
  (x y : R), MulHom.toFun self.toMulHom (x + y) ≤ MulHom.toFun self.toMulHom x + MulHom.toFun self.toMulHom y
add_le' }
#align absolute_value.subadditive_hom_class AbsoluteValue.subadditiveHomClass: {R : Type u_1} →
  {S : Type u_2} → [inst : Semiring R] → [inst_1 : OrderedSemiring S] → SubadditiveHomClass (AbsoluteValue R S) R S
AbsoluteValue.subadditiveHomClass

@[simp]
theorem coe_mk: ∀ (f : R →ₙ* S) {h₁ : ∀ (x : R), 0 ≤ MulHom.toFun f x} {h₂ : ∀ (x : R), MulHom.toFun f x = 0 ↔ x = 0}
  {h₃ : ∀ (x y : R), MulHom.toFun f (x + y) ≤ MulHom.toFun f x + MulHom.toFun f y},
  ↑{ toMulHom := f, nonneg' := h₁, eq_zero' := h₂, add_le' := h₃ } = ↑f
coe_mk (f: R →ₙ* S
f : R: Type ?u.7326
R →ₙ* S: Type ?u.7329
S) {h₁: ∀ (x : R), 0 ≤ MulHom.toFun f x
h₁ h₂: ?m.7691
h₂ h₃: ?m.7694
h₃} : (AbsoluteValue.mk: {R : Type ?u.7702} →
  {S : Type ?u.7701} →
    [inst : Semiring R] →
      [inst_1 : OrderedSemiring S] →
        (toMulHom : R →ₙ* S) →
          (∀ (x : R), 0 ≤ MulHom.toFun toMulHom x) →
            (∀ (x : R), MulHom.toFun toMulHom x = 0 ↔ x = 0) →
              (∀ (x y : R), MulHom.toFun toMulHom (x + y) ≤ MulHom.toFun toMulHom x + MulHom.toFun toMulHom y) →
                AbsoluteValue R S
AbsoluteValue.mk f: R →ₙ* S
f h₁: ?m.7688
h₁ h₂: ?m.7691
h₂ h₃: ?m.7694
h₃ : R: Type ?u.7326
R → S: Type ?u.7329
S) = f: R →ₙ* S
f :=
  rfl: ∀ {α : Sort ?u.10678} {a : α}, a = a
rfl
#align absolute_value.coe_mk AbsoluteValue.coe_mk: ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedSemiring S] (f : R →ₙ* S)
  {h₁ : ∀ (x : R), 0 ≤ MulHom.toFun f x} {h₂ : ∀ (x : R), MulHom.toFun f x = 0 ↔ x = 0}
  {h₃ : ∀ (x y : R), MulHom.toFun f (x + y) ≤ MulHom.toFun f x + MulHom.toFun f y},
  ↑{ toMulHom := f, nonneg' := h₁, eq_zero' := h₂, add_le' := h₃ } = ↑f
AbsoluteValue.coe_mk

@[ext]
theorem ext: ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedSemiring S] ⦃f g : AbsoluteValue R S⦄,
  (∀ (x : R), ↑f x = ↑g x) → f = g
ext ⦃f: AbsoluteValue R S
f g: AbsoluteValue R S
g : AbsoluteValue: (R : Type ?u.10781) →
  (S : Type ?u.10780) → [inst : Semiring R] → [inst : OrderedSemiring S] → Type (max?u.10781?u.10780)
AbsoluteValue R: Type ?u.10747
R S: Type ?u.10750
S⦄ : (∀ x: ?m.10809
x, f: AbsoluteValue R S
f x: ?m.10809
x = g: AbsoluteValue R S
g x: ?m.10809
x) → f: AbsoluteValue R S
f = g: AbsoluteValue R S
g :=
  FunLike.ext: ∀ {F : Sort ?u.11640} {α : Sort ?u.11641} {β : α → Sort ?u.11639} [i : FunLike F α β] (f g : F),
  (∀ (x : α), ↑f x = ↑g x) → f = g
FunLike.ext _: ?m.11642
_ _: ?m.11642
_
#align absolute_value.ext AbsoluteValue.ext: ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedSemiring S] ⦃f g : AbsoluteValue R S⦄,
  (∀ (x : R), ↑f x = ↑g x) → f = g
AbsoluteValue.ext

/-- See Note [custom simps projection]. -/
def Simps.apply: AbsoluteValue R S → R → S
Simps.apply (f: AbsoluteValue R S
f : AbsoluteValue: (R : Type ?u.12111) →
  (S : Type ?u.12110) → [inst : Semiring R] → [inst : OrderedSemiring S] → Type (max?u.12111?u.12110)
AbsoluteValue R: Type ?u.12077
R S: Type ?u.12080
S) : R: Type ?u.12077
R → S: Type ?u.12080
S := f: AbsoluteValue R S
f
#align absolute_value.simps.apply AbsoluteValue.Simps.apply: {R : Type u_1} → {S : Type u_2} → [inst : Semiring R] → [inst_1 : OrderedSemiring S] → AbsoluteValue R S → R → S
AbsoluteValue.Simps.apply

initialize_simps_projections AbsoluteValue: (R : Type u_1) → (S : Type u_2) → [inst : Semiring R] → [inst : OrderedSemiring S] → Type (maxu_1u_2)
AbsoluteValue (toFun: (R : Type u_1) → (S : Type u_2) → [inst : Semiring R] → [inst_1 : OrderedSemiring S] → AbsoluteValue R S → R → S
toFun → apply: {R : Type u_1} → {S : Type u_2} → [inst : Semiring R] → [inst_1 : OrderedSemiring S] → AbsoluteValue R S → R → S
apply)

-- Porting note:
-- These helper instances are unhelpful in Lean 4, so omitting:
-- /-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`
-- directly. -/
-- instance : CoeFun (AbsoluteValue R S) fun f => R → S :=
--   FunLike.hasCoeToFun

@[simp]
theorem coe_toMulHom: ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S),
  abv.toMulHom = ↑abv
coe_toMulHom : abv: AbsoluteValue R S
abv.toMulHom: {R : Type ?u.13173} →
  {S : Type ?u.13172} → [inst : Semiring R] → [inst_1 : OrderedSemiring S] → AbsoluteValue R S → R →ₙ* S
toMulHom = abv: AbsoluteValue R S
abv :=
  rfl: ∀ {α : Sort ?u.13420} {a : α}, a = a
rfl
#align absolute_value.coe_to_mul_hom AbsoluteValue.coe_toMulHom: ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S),
  abv.toMulHom = ↑abv
AbsoluteValue.coe_toMulHom

protected theorem nonneg: ∀ {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) (x : R),
  0 ≤ ↑abv x
nonneg (x: R
x : R: Type ?u.13446
R) : 0: ?m.13483
0 ≤ abv: AbsoluteValue R S
abv x: R
x :=
  abv: AbsoluteValue R S
abv.nonneg': ∀ {R : Type ?u.14324} {S : Type ?u.14323} [inst : Semiring R] [inst_1 : OrderedSemiring S] (self : AbsoluteValue R S)
  (x : R), 0 ≤ MulHom.toFun self.toMulHom x
nonneg' x: R
x
#align absolute_value.nonneg AbsoluteValue.nonneg: ∀ {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) (x : R),
  0 ≤ ↑abv x
AbsoluteValue.nonneg

@[simp]
protected theorem eq_zero: ∀ {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R},
  ↑abv x = 0 ↔ x = 0
eq_zero {x: R
x : R: Type ?u.14359
R} : abv: AbsoluteValue R S
abv x: R
x = 0: ?m.14822
0 ↔ x: R
x = 0: ?m.15103
0 :=
  abv: AbsoluteValue R S
abv.eq_zero': ∀ {R : Type ?u.15290} {S : Type ?u.15289} [inst : Semiring R] [inst_1 : OrderedSemiring S] (self : AbsoluteValue R S)
  (x : R), MulHom.toFun self.toMulHom x = 0 ↔ x = 0
eq_zero' x: R
x
#align absolute_value.eq_zero AbsoluteValue.eq_zero: ∀ {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R},
  ↑abv x = 0 ↔ x = 0
AbsoluteValue.eq_zero

protected theorem add_le: ∀ (x y : R), ↑abv (x + y) ≤ ↑abv x + ↑abv y
add_le (x: R
x y: R
y : R: Type ?u.15366
R) : abv: AbsoluteValue R S
abv (x: R
x + y: R
y) ≤ abv: AbsoluteValue R S
abv x: R
x + abv: AbsoluteValue R S
abv y: R
y :=
  abv: AbsoluteValue R S
abv.add_le': ∀ {R : Type ?u.17450} {S : Type ?u.17449} [inst : Semiring R] [inst_1 : OrderedSemiring S] (self : AbsoluteValue R S)
  (x y : R), MulHom.toFun self.toMulHom (x + y) ≤ MulHom.toFun self.toMulHom x + MulHom.toFun self.toMulHom y
add_le' x: R
x y: R
y
#align absolute_value.add_le AbsoluteValue.add_le: ∀ {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) (x y : R),
  ↑abv (x + y) ≤ ↑abv x + ↑abv y
AbsoluteValue.add_le

-- Porting note: Removed since `map_mul` proves the theorem
--@[simp]
--protected theorem map_mul (x y : R) : abv (x * y) = abv x * abv y := map_mul _ _ _
  --abv.map_mul' x y
#align absolute_value.map_mul map_mul: ∀ {M : Type u_2} {N : Type u_3} {F : Type u_1} [inst : Mul M] [inst_1 : Mul N] [inst_2 : MulHomClass F M N] (f : F)
  (x y : M), ↑f (x * y) = ↑f x * ↑f y
map_mul

protected theorem ne_zero_iff: ∀ {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R},
  ↑abv x ≠ 0 ↔ x ≠ 0
ne_zero_iff {x: R
x : R: Type ?u.17490
R} : abv: AbsoluteValue R S
abv x: R
x ≠ 0: ?m.17955
0 ↔ x: R
x ≠ 0: ?m.18222
0 :=
  abv: AbsoluteValue R S
abv.eq_zero: ∀ {R : Type ?u.18395} {S : Type ?u.18394} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
  {x : R}, ↑abv x = 0 ↔ x = 0
eq_zero.not: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)
not
#align absolute_value.ne_zero_iff AbsoluteValue.ne_zero_iff: ∀ {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R},
  ↑abv x ≠ 0 ↔ x ≠ 0
AbsoluteValue.ne_zero_iff

protected theorem pos: ∀ {x : R}, x ≠ 0 → 0 < ↑abv x
pos {x: R
x : R: Type ?u.18448
R} (hx: x ≠ 0
hx : x: R
x ≠ 0: ?m.18486
0) : 0: ?m.18662
0 < abv: AbsoluteValue R S
abv x: R
x :=
  lt_of_le_of_ne: ∀ {α : Type ?u.19503} [inst : PartialOrder α] {a b : α}, a ≤ b → a ≠ b → a < b
lt_of_le_of_ne (abv: AbsoluteValue R S
abv.nonneg: ∀ {R : Type ?u.19676} {S : Type ?u.19675} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
  (x : R), 0 ≤ ↑abv x
nonneg x: R
x) (Ne.symm: ∀ {α : Sort ?u.19704} {a b : α}, a ≠ b → b ≠ a
Ne.symm <| mt: ∀ {a b : Prop}, (a → b) → ¬b → ¬a
mt abv: AbsoluteValue R S
abv.eq_zero: ∀ {R : Type ?u.19718} {S : Type ?u.19717} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
  {x : R}, ↑abv x = 0 ↔ x = 0
eq_zero.mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp hx: x ≠ 0
hx)
#align absolute_value.pos AbsoluteValue.pos: ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R},
  x ≠ 0 → 0 < ↑abv x
AbsoluteValue.pos

@[simp]
protected theorem pos_iff: ∀ {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R},
  0 < ↑abv x ↔ x ≠ 0
pos_iff {x: R
x : R: Type ?u.19755
R} : 0: ?m.19792
0 < abv: AbsoluteValue R S
abv x: R
x ↔ x: R
x ≠ 0: ?m.20633
0 :=
  ⟨fun h₁: ?m.20814
h₁ => mt: ∀ {a b : Prop}, (a → b) → ¬b → ¬a
mt abv: AbsoluteValue R S
abv.eq_zero: ∀ {R : Type ?u.20821} {S : Type ?u.20820} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
  {x : R}, ↑abv x = 0 ↔ x = 0
eq_zero.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr h₁: ?m.20814
h₁.ne': ∀ {α : Type ?u.20854} [inst : Preorder α] {x y : α}, x < y → y ≠ x
ne', abv: AbsoluteValue R S
abv.pos: ∀ {R : Type ?u.21009} {S : Type ?u.21010} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
  {x : R}, x ≠ 0 → 0 < ↑abv x
pos⟩
#align absolute_value.pos_iff AbsoluteValue.pos_iff: ∀ {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R},
  0 < ↑abv x ↔ x ≠ 0
AbsoluteValue.pos_iff

protected theorem ne_zero: ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R},
  x ≠ 0 → ↑abv x ≠ 0
ne_zero {x: R
x : R: Type ?u.21080
R} (hx: x ≠ 0
hx : x: R
x ≠ 0: ?m.21118
0) : abv: AbsoluteValue R S
abv x: R
x ≠ 0: ?m.21720
0 :=
  (abv: AbsoluteValue R S
abv.pos: ∀ {R : Type ?u.21989} {S : Type ?u.21990} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
  {x : R}, x ≠ 0 → 0 < ↑abv x
pos hx: x ≠ 0
hx).ne': ∀ {α : Type ?u.22026} [inst : Preorder α] {x y : α}, x < y → y ≠ x
ne'
#align absolute_value.ne_zero AbsoluteValue.ne_zero: ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R},
  x ≠ 0 → ↑abv x ≠ 0
AbsoluteValue.ne_zero

theorem map_one_of_isLeftRegular: IsLeftRegular (↑abv 1) → ↑abv 1 = 1
map_one_of_isLeftRegular (h: IsLeftRegular (↑abv 1)
h : IsLeftRegular: {R : Type ?u.22224} → [inst : Mul R] → R → Prop
IsLeftRegular (abv: AbsoluteValue R S
abv 1: ?m.22677
1)) : abv: AbsoluteValue R S
abv 1: ?m.23343
1 = 1: ?m.23346
1 :=
  h: IsLeftRegular (↑abv 1)
h <| by
Goals accomplished! 🐙 R: Type u_2

S: Type u_1

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) 1simp [← map_mul: ∀ {M : Type ?u.23484} {N : Type ?u.23485} {F : Type ?u.23483} [inst : Mul M] [inst_1 : Mul N]
  [inst_2 : MulHomClass F M N] (f : F) (x y : M), ↑f (x * y) = ↑f x * ↑f y
map_mul]
Goals accomplished! 🐙
#align absolute_value.map_one_of_is_regular AbsoluteValue.map_one_of_isLeftRegular: ∀ {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S),
  IsLeftRegular (↑abv 1) → ↑abv 1 = 1
AbsoluteValue.map_one_of_isLeftRegular

-- Porting note: Removed since `map_zero` proves the theorem
--@[simp]
--protected theorem map_zero : abv 0 = 0 := map_zero _
  --abv.eq_zero.2 rfl
#align absolute_value.map_zero map_zero: ∀ {M : Type u_2} {N : Type u_3} {F : Type u_1} [inst : Zero M] [inst_1 : Zero N] [inst_2 : ZeroHomClass F M N] (f : F),
  ↑f 0 = 0
map_zero

end Semiring

section Ring

variable {R: Type ?u.27031
R S: Type ?u.27236
S : Type _: Type (?u.27236+1)
Type _} [Ring: Type ?u.27037 → Type ?u.27037
Ring R: Type ?u.27233
R] [OrderedSemiring: Type ?u.27242 → Type ?u.27242
OrderedSemiring S: Type ?u.27236
S] (abv: AbsoluteValue R S
abv : AbsoluteValue: (R : Type ?u.27044) →
  (S : Type ?u.27043) → [inst : Semiring R] → [inst : OrderedSemiring S] → Type (max?u.27044?u.27043)
AbsoluteValue R: Type ?u.27233
R S: Type ?u.38789
S)

protected theorem sub_le: ∀ {R : Type u_2} {S : Type u_1} [inst : Ring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) (a b c : R),
  ↑abv (a - c) ≤ ↑abv (a - b) + ↑abv (b - c)
sub_le (a: R
a b: R
b c: R
c : R: Type ?u.27233
R) : abv: AbsoluteValue R S
abv (a: R
a - c: R
c) ≤ abv: AbsoluteValue R S
abv (a: R
a - b: R
b) + abv: AbsoluteValue R S
abv (b: R
b - c: R
c) := by
Goals accomplished! 🐙
  R: Type u_2

S: Type u_1

inst✝¹: Ring R

inst✝: OrderedSemiring S

abv: AbsoluteValue R S

a, b, c: R

↑abv (a - c) ≤ ↑abv (a - b) + ↑abv (b - c)simpa [sub_eq_add_neg: ∀ {G : Type ?u.29361} [inst : SubNegMonoid G] (a b : G), a - b = a + -b
sub_eq_add_neg, add_assoc: ∀ {G : Type ?u.29377} [inst : AddSemigroup G] (a b c : G), a + b + c = a + (b + c)
add_assoc] using abv: AbsoluteValue R S
abv.add_le: ∀ {R : Type ?u.34005} {S : Type ?u.34004} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
  (x y : R), ↑abv (x + y) ≤ ↑abv x + ↑abv y
add_le (a: R
a - b: R
b) (b: R
b - c: R
c)
Goals accomplished! 🐙
#align absolute_value.sub_le AbsoluteValue.sub_le: ∀ {R : Type u_2} {S : Type u_1} [inst : Ring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) (a b c : R),
  ↑abv (a - c) ≤ ↑abv (a - b) + ↑abv (b - c)
AbsoluteValue.sub_le

@[simp (high)]
theorem map_sub_eq_zero_iff: ∀ (a b : R), ↑abv (a - b) = 0 ↔ a = b
map_sub_eq_zero_iff (a: R
a b: R
b : R: Type ?u.38786
R) : abv: AbsoluteValue R S
abv (a: R
a - b: R
b) = 0: ?m.39480
0 ↔ a: R
a = b: R
b :=
  abv: AbsoluteValue R S
abv.eq_zero: ∀ {R : Type ?u.39765} {S : Type ?u.39764} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
  {x : R}, ↑abv x = 0 ↔ x = 0
eq_zero.trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)
trans sub_eq_zero: ∀ {G : Type ?u.39980} [inst : AddGroup G] {a b : G}, a - b = 0 ↔ a = b
sub_eq_zero
#align absolute_value.map_sub_eq_zero_iff AbsoluteValue.map_sub_eq_zero_iff: ∀ {R : Type u_2} {S : Type u_1} [inst : Ring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) (a b : R),
  ↑abv (a - b) = 0 ↔ a = b
AbsoluteValue.map_sub_eq_zero_iff

end Ring

end OrderedSemiring

section OrderedRing

section Semiring

section IsDomain

-- all of these are true for `NoZeroDivisors S`; but it doesn't work smoothly with the
-- `IsDomain`/`CancelMonoidWithZero` API
variable {R: Type ?u.40085
R S: Type ?u.40211
S : Type _: Type (?u.40419+1)
Type _} [Semiring: Type ?u.44594 → Type ?u.44594
Semiring R: Type ?u.40085
R] [OrderedRing: Type ?u.48083 → Type ?u.48083
OrderedRing S: Type ?u.40088
S] (abv: AbsoluteValue R S
abv : AbsoluteValue: (R : Type ?u.40432) →
  (S : Type ?u.40431) → [inst : Semiring R] → [inst : OrderedSemiring S] → Type (max?u.40432?u.40431)
AbsoluteValue R: Type ?u.40208
R S: Type ?u.40088
S)

variable [IsDomain: (α : Type ?u.44711) → [inst : Semiring α] → Prop
IsDomain S: Type ?u.40422
S] [Nontrivial: Type ?u.42516 → Prop
Nontrivial R: Type ?u.42308
R]

@[simp (high)]
protected theorem map_one: ↑abv 1 = 1
map_one : abv: AbsoluteValue R S
abv 1: ?m.41058
1 = 1: ?m.41095
1 :=
  abv: AbsoluteValue R S
abv.map_one_of_isLeftRegular: ∀ {R : Type ?u.41280} {S : Type ?u.41279} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S),
  IsLeftRegular (↑abv 1) → ↑abv 1 = 1
map_one_of_isLeftRegular (isRegular_of_ne_zero: ∀ {R : Type ?u.41403} [inst : CancelMonoidWithZero R] {a : R}, a ≠ 0 → IsRegular a
isRegular_of_ne_zero <| abv: AbsoluteValue R S
abv.ne_zero: ∀ {R : Type ?u.41407} {S : Type ?u.41408} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
  {x : R}, x ≠ 0 → ↑abv x ≠ 0
ne_zero one_ne_zero: ∀ {α : Type ?u.41581} [inst : Zero α] [inst_1 : One α] [inst_2 : NeZero 1], 1 ≠ 0
one_ne_zero).left: ∀ {R : Type ?u.42189} [inst : Mul R] {c : R}, IsRegular c → IsLeftRegular c
left
#align absolute_value.map_one AbsoluteValue.map_one: ∀ {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst_1 : OrderedRing S] (abv : AbsoluteValue R S)
  [inst_2 : IsDomain S] [inst_3 : Nontrivial R], ↑abv 1 = 1
AbsoluteValue.map_one

instance: {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : OrderedRing S] →
        [inst_2 : IsDomain S] → [inst_3 : Nontrivial R] → MonoidWithZeroHomClass (AbsoluteValue R S) R S
instance : MonoidWithZeroHomClass: Type ?u.42521 →
  (M : outParam (Type ?u.42520)) →
    (N : outParam (Type ?u.42519)) →
      [inst : MulZeroOneClass M] → [inst : MulZeroOneClass N] → Type (max(max?u.42521?u.42520)?u.42519)
MonoidWithZeroHomClass (AbsoluteValue: (R : Type ?u.42523) →
  (S : Type ?u.42522) → [inst : Semiring R] → [inst : OrderedSemiring S] → Type (max?u.42523?u.42522)
AbsoluteValue R: Type ?u.42308
R S: Type ?u.42311
S) R: Type ?u.42308
R S: Type ?u.42311
S :=
  { AbsoluteValue.mulHomClass: {R : Type ?u.42750} →
  {S : Type ?u.42749} → [inst : Semiring R] → [inst_1 : OrderedSemiring S] → MulHomClass (AbsoluteValue R S) R S
AbsoluteValue.mulHomClass with map_zero := fun f: ?m.43396
f => map_zero: ∀ {M : Type ?u.43399} {N : Type ?u.43400} {F : Type ?u.43398} [inst : Zero M] [inst_1 : Zero N]
  [inst_2 : ZeroHomClass F M N] (f : F), ↑f 0 = 0
map_zero f: ?m.43396
f, map_one := fun f: ?m.43339
f => f: ?m.43339
f.map_one: ∀ {R : Type ?u.43342} {S : Type ?u.43341} [inst : Semiring R] [inst_1 : OrderedRing S] (abv : AbsoluteValue R S)
  [inst_2 : IsDomain S] [inst_3 : Nontrivial R], ↑abv 1 = 1
map_one }

/-- Absolute values from a nontrivial `R` to a linear ordered ring preserve `*`, `0` and `1`. -/
def toMonoidWithZeroHom: R →*₀ S
toMonoidWithZeroHom : R: Type ?u.44008
R →*₀ S: Type ?u.44011
S :=
  abv: AbsoluteValue R S
abv
#align absolute_value.to_monoid_with_zero_hom AbsoluteValue.toMonoidWithZeroHom: {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : OrderedRing S] → AbsoluteValue R S → [inst_2 : IsDomain S] → [inst_3 : Nontrivial R] → R →*₀ S
AbsoluteValue.toMonoidWithZeroHom

@[simp]
theorem coe_toMonoidWithZeroHom: ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedRing S] (abv : AbsoluteValue R S)
  [inst_2 : IsDomain S] [inst_3 : Nontrivial R], ↑(toMonoidWithZeroHom abv) = ↑abv
coe_toMonoidWithZeroHom : ⇑abv: AbsoluteValue R S
abv.toMonoidWithZeroHom: {R : Type ?u.44801} →
  {S : Type ?u.44800} →
    [inst : Semiring R] →
      [inst_1 : OrderedRing S] → AbsoluteValue R S → [inst_2 : IsDomain S] → [inst_3 : Nontrivial R] → R →*₀ S
toMonoidWithZeroHom = abv: AbsoluteValue R S
abv :=
  rfl: ∀ {α : Sort ?u.47283} {a : α}, a = a
rfl
#align absolute_value.coe_to_monoid_with_zero_hom AbsoluteValue.coe_toMonoidWithZeroHom: ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedRing S] (abv : AbsoluteValue R S)
  [inst_2 : IsDomain S] [inst_3 : Nontrivial R], ↑(toMonoidWithZeroHom abv) = ↑abv
AbsoluteValue.coe_toMonoidWithZeroHom

/-- Absolute values from a nontrivial `R` to a linear ordered ring preserve `*` and `1`. -/
def toMonoidHom: R →* S
toMonoidHom : R: Type ?u.47334
R →* S: Type ?u.47337
S :=
  abv: AbsoluteValue R S
abv
#align absolute_value.to_monoid_hom AbsoluteValue.toMonoidHom: {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : OrderedRing S] → AbsoluteValue R S → [inst_2 : IsDomain S] → [inst_3 : Nontrivial R] → R →* S
AbsoluteValue.toMonoidHom

@[simp]
theorem coe_toMonoidHom: ↑(toMonoidHom abv) = ↑abv
coe_toMonoidHom : ⇑abv: AbsoluteValue R S
abv.toMonoidHom: {R : Type ?u.48287} →
  {S : Type ?u.48286} →
    [inst : Semiring R] →
      [inst_1 : OrderedRing S] → AbsoluteValue R S → [inst_2 : IsDomain S] → [inst_3 : Nontrivial R] → R →* S
toMonoidHom = abv: AbsoluteValue R S
abv :=
  rfl: ∀ {α : Sort ?u.50674} {a : α}, a = a
rfl
#align absolute_value.coe_to_monoid_hom AbsoluteValue.coe_toMonoidHom: ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedRing S] (abv : AbsoluteValue R S)
  [inst_2 : IsDomain S] [inst_3 : Nontrivial R], ↑(toMonoidHom abv) = ↑abv
AbsoluteValue.coe_toMonoidHom

-- Porting note: Removed since `map_zero` proves the theorem
--@[simp]
--protected theorem map_pow (a : R) (n : ℕ) : abv (a ^ n) = abv a ^ n := map_pow _ _ _
  --abv.toMonoidHom.map_pow a n
#align absolute_value.map_pow map_pow: ∀ {G : Type u_1} {H : Type u_2} {F : Type u_3} [inst : Monoid G] [inst_1 : Monoid H] [inst_2 : MonoidHomClass F G H]
  (f : F) (a : G) (n : ℕ), ↑f (a ^ n) = ↑f a ^ n
map_pow

end IsDomain

end Semiring

section Ring

variable {R: Type ?u.51017
R S: Type ?u.51020
S : Type _: Type (?u.51020+1)
Type _} [Ring: Type ?u.50731 → Type ?u.50731
Ring R: Type ?u.50725
R] [OrderedRing: Type ?u.50734 → Type ?u.50734
OrderedRing S: Type ?u.51020
S] (abv: AbsoluteValue R S
abv : AbsoluteValue: (R : Type ?u.50738) →
  (S : Type ?u.50737) → [inst : Semiring R] → [inst : OrderedSemiring S] → Type (max?u.50738?u.50737)
AbsoluteValue R: Type ?u.50725
R S: Type ?u.50728
S)

protected theorem le_sub: ∀ (a b : R), ↑abv a - ↑abv b ≤ ↑abv (a - b)
le_sub (a: R
a b: R
b : R: Type ?u.51017
R) : abv: AbsoluteValue R S
abv a: R
a - abv: AbsoluteValue R S
abv b: R
b ≤ abv: AbsoluteValue R S
abv (a: R
a - b: R
b) :=
  sub_le_iff_le_add: ∀ {α : Type ?u.52859} [inst : AddGroup α] [inst_1 : LE α]
  [inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c : α},
  a - c ≤ b ↔ a ≤ b + c
sub_le_iff_le_add.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 <| by
Goals accomplished! 🐙 R: Type u_2

S: Type u_1

inst✝¹: Ring R

inst✝: OrderedRing S

abv: AbsoluteValue R S

a, b: R

↑abv a ≤ ↑abv (a - b) + ↑abv bsimpa using abv: AbsoluteValue R S
abv.add_le: ∀ {R : Type ?u.54789} {S : Type ?u.54788} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
  (x y : R), ↑abv (x + y) ≤ ↑abv x + ↑abv y
add_le (a: R
a - b: R
b) b: R
b
Goals accomplished! 🐙
#align absolute_value.le_sub AbsoluteValue.le_sub: ∀ {R : Type u_2} {S : Type u_1} [inst : Ring R] [inst_1 : OrderedRing S] (abv : AbsoluteValue R S) (a b : R),
  ↑abv a - ↑abv b ≤ ↑abv (a - b)
AbsoluteValue.le_sub

end Ring

end OrderedRing

section OrderedCommRing

variable {R: Type ?u.57154
R S: Type ?u.56663
S : Type _: Type (?u.57157+1)
Type _} [Ring: Type ?u.57160 → Type ?u.57160
Ring R: Type ?u.56410
R] [OrderedCommRing: Type ?u.57163 → Type ?u.57163
OrderedCommRing S: Type ?u.56413
S] (abv: AbsoluteValue R S
abv : AbsoluteValue: (R : Type ?u.56423) →
  (S : Type ?u.56422) → [inst : Semiring R] → [inst : OrderedSemiring S] → Type (max?u.56423?u.56422)
AbsoluteValue R: Type ?u.56410
R S: Type ?u.56413
S)

variable [NoZeroDivisors: (M₀ : Type ?u.57404) → [inst : Mul M₀] → [inst : Zero M₀] → Prop
NoZeroDivisors S: Type ?u.56663
S]

@[simp]
protected theorem map_neg: ∀ {R : Type u_2} {S : Type u_1} [inst : Ring R] [inst_1 : OrderedCommRing S] (abv : AbsoluteValue R S)
  [inst_2 : NoZeroDivisors S] (a : R), ↑abv (-a) = ↑abv a
map_neg (a: R
a : R: Type ?u.57154
R) : abv: AbsoluteValue R S
abv (-a: R
a) = abv: AbsoluteValue R S
abv a: R
a := by
Goals accomplished! 🐙
  R: Type u_2

S: Type u_1

inst✝²: Ring R

inst✝¹: OrderedCommRing S

abv: AbsoluteValue R S

inst✝: NoZeroDivisors S

a: R

↑abv (-a) = ↑abv aby_cases ha: ?m.58880
ha : a: R
a = 0: ?m.58501
0R: Type u_2

S: Type u_1

inst✝²: Ring R

inst✝¹: OrderedCommRing S

abv: AbsoluteValue R S

inst✝: NoZeroDivisors S

a: R

ha: a = 0

pos↑abv (-a) = ↑abv a
R: Type u_2

S: Type u_1

inst✝²: Ring R

inst✝¹: OrderedCommRing S

abv: AbsoluteValue R S

inst✝: NoZeroDivisors S

a: R

ha: ¬a = 0

neg↑abv (-a) = ↑abv a;R: Type u_2

S: Type u_1

inst✝²: Ring R

inst✝¹: OrderedCommRing S

abv: AbsoluteValue R S

inst✝: NoZeroDivisors S

a: R

ha: a = 0

pos↑abv (-a) = ↑abv a
R: Type u_2

S: Type u_1

inst✝²: Ring R

inst✝¹: OrderedCommRing S

abv: AbsoluteValue R S

inst✝: NoZeroDivisors S

a: R

ha: ¬a = 0

neg↑abv (-a) = ↑abv a R: Type u_2

S: Type u_1

inst✝²: Ring R

inst✝¹: OrderedCommRing S

abv: AbsoluteValue R S

inst✝: NoZeroDivisors S

a: R

↑abv (-a) = ↑abv a·R: Type u_2

S: Type u_1

inst✝²: Ring R

inst✝¹: OrderedCommRing S

abv: AbsoluteValue R S

inst✝: NoZeroDivisors S

a: R

ha: a = 0

pos↑abv (-a) = ↑abv a R: Type u_2

S: Type u_1

inst✝²: Ring R

inst✝¹: OrderedCommRing S

abv: AbsoluteValue R S

inst✝: NoZeroDivisors S

a: R

ha: a = 0

pos↑abv (-a) = ↑abv a
R: Type u_2

S: Type u_1

inst✝²: Ring R

inst✝¹: OrderedCommRing S

abv: AbsoluteValue R S

inst✝: NoZeroDivisors S

a: R

ha: ¬a = 0

neg↑abv (-a) = ↑abv asimp [ha: ?m.58873
ha]
Goals accomplished! 🐙
  R: Type u_2

S: Type u_1

inst✝²: Ring R

inst✝¹: OrderedCommRing S

abv: AbsoluteValue R S

inst✝: NoZeroDivisors S

a: R

↑abv (-a) = ↑abv arefine'
    (mul_self_eq_mul_self_iff: ∀ {R : Type ?u.59891} [inst : CommRing R] [inst_1 : NoZeroDivisors R] {a b : R}, a * a = b * b ↔ a = b ∨ a = -b
mul_self_eq_mul_self_iff.mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp (R: Type u_2

S: Type u_1

inst✝²: Ring R

inst✝¹: OrderedCommRing S

abv: AbsoluteValue R S

inst✝: NoZeroDivisors S

a: R

ha: ¬a = 0

neg↑abv (-a) = ↑abv aby
Goals accomplished! 🐙 R: Type u_2

S: Type u_1

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 arw [R: Type u_2

S: Type u_1

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← map_mul: ∀ {M : Type ?u.59966} {N : Type ?u.59967} {F : Type ?u.59965} [inst : Mul M] [inst_1 : Mul N]
  [inst_2 : MulHomClass F M N] (f : F) (x y : M), ↑f (x * y) = ↑f x * ↑f y
map_mul abv: AbsoluteValue R S
abv,R: Type u_2

S: Type u_1

inst✝²: Ring R

inst✝¹: OrderedCommRing S

abv: AbsoluteValue R S

inst✝: NoZeroDivisors S

a: R

ha: ¬a = 0

↑abv (-a * -a) = ↑abv a * ↑abv a R: Type u_2

S: Type u_1

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 aneg_mul_neg: ∀ {α : Type ?u.60176} [inst : Mul α] [inst_1 : HasDistribNeg α] (a b : α), -a * -b = a * b
neg_mul_neg,R: Type u_2

S: Type u_1

inst✝²: Ring R

inst✝¹: OrderedCommRing S

abv: AbsoluteValue R S

inst✝: NoZeroDivisors S

a: R

ha: ¬a = 0

↑abv (a * a) = ↑abv a * ↑abv a R: Type u_2

S: Type u_1

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 amap_mul: ∀ {M : Type ?u.60295} {N : Type ?u.60296} {F : Type ?u.60294} [inst : Mul M] [inst_1 : Mul N]
  [inst_2 : MulHomClass F M N] (f : F) (x y : M), ↑f (x * y) = ↑f x * ↑f y
map_mul abv: AbsoluteValue R S
abvR: Type u_2

S: Type u_1

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]
Goals accomplished! 🐙)).resolve_right: ∀ {a b : Prop}, a ∨ b → ¬b → a
resolve_right _: ¬?m.59928
_R: Type u_2

S: Type u_1

inst✝²: Ring R

inst✝¹: OrderedCommRing S

abv: AbsoluteValue R S

inst✝: NoZeroDivisors S

a: R

ha: ¬a = 0

neg¬↑abv (-a) = -↑abv a
  R: Type u_2

S: Type u_1

inst✝²: Ring R

inst✝¹: OrderedCommRing S

abv: AbsoluteValue R S

inst✝: NoZeroDivisors S

a: R

↑abv (-a) = ↑abv aexact ((neg_lt_zero: ∀ {α : Type ?u.60404} [inst : AddGroup α] [inst_1 : LT α]
  [inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α}, -a < 0 ↔ 0 < a
neg_lt_zero.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr (abv: AbsoluteValue R S
abv.pos: ∀ {R : Type ?u.60453} {S : Type ?u.60454} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
  {x : R}, x ≠ 0 → 0 < ↑abv x
pos ha: ?m.58880
ha)).trans: ∀ {α : Type ?u.60736} [inst : Preorder α] {a b c : α}, a < b → b < c → a < c
trans (abv: AbsoluteValue R S
abv.pos: ∀ {R : Type ?u.60834} {S : Type ?u.60835} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
  {x : R}, x ≠ 0 → 0 < ↑abv x
pos (neg_ne_zero: ∀ {α : Type ?u.60860} [inst : SubtractionMonoid α] {a : α}, -a ≠ 0 ↔ a ≠ 0
neg_ne_zero.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr ha: ?m.58880
ha))).ne': ∀ {α : Type ?u.60952} [inst : Preorder α] {x y : α}, x < y → y ≠ x
ne'
Goals accomplished! 🐙
#align absolute_value.map_neg AbsoluteValue.map_neg: ∀ {R : Type u_2} {S : Type u_1} [inst : Ring R] [inst_1 : OrderedCommRing S] (abv : AbsoluteValue R S)
  [inst_2 : NoZeroDivisors S] (a : R), ↑abv (-a) = ↑abv a
AbsoluteValue.map_neg

protected theorem map_sub: ∀ {R : Type u_2} {S : Type u_1} [inst : Ring R] [inst_1 : OrderedCommRing S] (abv : AbsoluteValue R S)
  [inst_2 : NoZeroDivisors S] (a b : R), ↑abv (a - b) = ↑abv (b - a)
map_sub (a: R
a b: R
b : R: Type ?u.61436
R) : abv: AbsoluteValue R S
abv (a: R
a - b: R
b) = abv: AbsoluteValue R S
abv (b: R
b - a: R
a) := by
Goals accomplished! 🐙 R: Type u_2

S: Type u_1

inst✝²: Ring R

inst✝¹: OrderedCommRing S

abv: AbsoluteValue R S

inst✝: NoZeroDivisors S

a, b: R

↑abv (a - b) = ↑abv (b - a)rw [R: Type u_2

S: Type u_1

inst✝²: Ring R

inst✝¹: OrderedCommRing S

abv: AbsoluteValue R S

inst✝: NoZeroDivisors S

a, b: R

↑abv (a - b) = ↑abv (b - a)← neg_sub: ∀ {α : Type ?u.62855} [inst : SubtractionMonoid α] (a b : α), -(a - b) = b - a
neg_sub,R: Type u_2

S: Type u_1

inst✝²: Ring R

inst✝¹: OrderedCommRing S

abv: AbsoluteValue R S

inst✝: NoZeroDivisors S

a, b: R

↑abv (-(b - a)) = ↑abv (b - a) R: Type u_2

S: Type u_1

inst✝²: Ring R

inst✝¹: OrderedCommRing S

abv: AbsoluteValue R S

inst✝: NoZeroDivisors S

a, b: R

↑abv (a - b) = ↑abv (b - a)abv: AbsoluteValue R S
abv.map_neg: ∀ {R : Type ?u.62986} {S : Type ?u.62985} [inst : Ring R] [inst_1 : OrderedCommRing S] (abv : AbsoluteValue R S)
  [inst_2 : NoZeroDivisors S] (a : R), ↑abv (-a) = ↑abv a
map_negR: Type u_2

S: Type u_1

inst✝²: Ring R

inst✝¹: OrderedCommRing S

abv: AbsoluteValue R S

inst✝: NoZeroDivisors S

a, b: R

↑abv (b - a) = ↑abv (b - a)]
Goals accomplished! 🐙
#align absolute_value.map_sub AbsoluteValue.map_sub: ∀ {R : Type u_2} {S : Type u_1} [inst : Ring R] [inst_1 : OrderedCommRing S] (abv : AbsoluteValue R S)
  [inst_2 : NoZeroDivisors S] (a b : R), ↑abv (a - b) = ↑abv (b - a)
AbsoluteValue.map_sub

end OrderedCommRing

section LinearOrderedRing

variable {R: Type ?u.63068
R S: Type ?u.63071
S : Type _: Type (?u.64298+1)
Type _} [Semiring: Type ?u.63177 → Type ?u.63177
Semiring R: Type ?u.63068
R] [LinearOrderedRing: Type ?u.63180 → Type ?u.63180
LinearOrderedRing S: Type ?u.63174
S] (abv: AbsoluteValue R S
abv : AbsoluteValue: (R : Type ?u.63184) →
  (S : Type ?u.63183) → [inst : Semiring R] → [inst : OrderedSemiring S] → Type (max?u.63184?u.63183)
AbsoluteValue R: Type ?u.63068
R S: Type ?u.63174
S)

/-- `AbsoluteValue.abs` is `abs` as a bundled `AbsoluteValue`. -/
@[simps: ∀ {S : Type u_1} [inst : LinearOrderedRing S] (a : S), ↑AbsoluteValue.abs a = abs a
simps]
protected def abs: AbsoluteValue S S
abs : AbsoluteValue: (R : Type ?u.63275) →
  (S : Type ?u.63274) → [inst : Semiring R] → [inst : OrderedSemiring S] → Type (max?u.63275?u.63274)
AbsoluteValue S: Type ?u.63174
S S: Type ?u.63174
S where
  toFun := abs: {α : Type ?u.63450} → [self : Abs α] → α → α
abs
  nonneg' := abs_nonneg: ∀ {α : Type ?u.63647} [inst : AddGroup α] [inst_1 : LinearOrder α]
  [inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α), 0 ≤ abs a
abs_nonneg
  eq_zero' _: ?m.63849
_ := abs_eq_zero: ∀ {α : Type ?u.63851} [inst : AddGroup α] [inst_1 : LinearOrder α]
  [inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}, abs a = 0 ↔ a = 0
abs_eq_zero
  add_le' := abs_add: ∀ {α : Type ?u.63921} [inst : LinearOrderedAddCommGroup α] (a b : α), abs (a + b) ≤ abs a + abs b
abs_add
  map_mul' := abs_mul: ∀ {α : Type ?u.63603} [inst : LinearOrderedRing α] (a b : α), abs (a * b) = abs a * abs b
abs_mul
#align absolute_value.abs AbsoluteValue.abs: {S : Type u_1} → [inst : LinearOrderedRing S] → AbsoluteValue S S
AbsoluteValue.abs
#align absolute_value.abs_apply AbsoluteValue.abs_apply: ∀ {S : Type u_1} [inst : LinearOrderedRing S] (a : S), ↑AbsoluteValue.abs a = abs a
AbsoluteValue.abs_apply
#align absolute_value.abs_to_mul_hom_apply AbsoluteValue.abs_apply: ∀ {S : Type u_1} [inst : LinearOrderedRing S] (a : S), ↑AbsoluteValue.abs a = abs a
AbsoluteValue.abs_apply

instance: {S : Type u_1} → [inst : LinearOrderedRing S] → Inhabited (AbsoluteValue S S)
instance : Inhabited: Sort ?u.64398 → Sort (max1?u.64398)
Inhabited (AbsoluteValue: (R : Type ?u.64400) →
  (S : Type ?u.64399) → [inst : Semiring R] → [inst : OrderedSemiring S] → Type (max?u.64400?u.64399)
AbsoluteValue S: Type ?u.64298
S S: Type ?u.64298
S) :=
  ⟨AbsoluteValue.abs: {S : Type ?u.64520} → [inst : LinearOrderedRing S] → AbsoluteValue S S
AbsoluteValue.abs⟩

end LinearOrderedRing

section LinearOrderedCommRing

variable {R: Type ?u.64581
R S: Type ?u.64820
S : Type _: Type (?u.64820+1)
Type _} [Ring: Type ?u.64823 → Type ?u.64823
Ring R: Type ?u.64581
R] [LinearOrderedCommRing: Type ?u.64590 → Type ?u.64590
LinearOrderedCommRing S: Type ?u.64584
S] (abv: AbsoluteValue R S
abv : AbsoluteValue: (R : Type ?u.64594) →
  (S : Type ?u.64593) → [inst : Semiring R] → [inst : OrderedSemiring S] → Type (max?u.64594?u.64593)
AbsoluteValue R: Type ?u.64581
R S: Type ?u.64584
S)

theorem abs_abv_sub_le_abv_sub: ∀ (a b : R), abs (↑abv a - ↑abv b) ≤ ↑abv (a - b)
abs_abv_sub_le_abv_sub (a: R
a b: R
b : R: Type ?u.64817
R) : abs: {α : Type ?u.65058} → [self : Abs α] → α → α
abs (abv: AbsoluteValue R S
abv a: R
a - abv: AbsoluteValue R S
abv b: R
b) ≤ abv: AbsoluteValue R S
abv (a: R
a - b: R
b) :=
  abs_sub_le_iff: ∀ {α : Type ?u.66670} [inst : LinearOrderedAddCommGroup α] {a b c : α}, abs (a - b) ≤ c ↔ a - b ≤ c ∧ b - a ≤ c
abs_sub_le_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 ⟨abv: AbsoluteValue R S
abv.le_sub: ∀ {R : Type ?u.66746} {S : Type ?u.66745} [inst : Ring R] [inst_1 : OrderedRing S] (abv : AbsoluteValue R S) (a b : R),
  ↑abv a - ↑abv b ≤ ↑abv (a - b)
le_sub _: ?m.66754
_ _: ?m.66754
_, by
Goals accomplished! 🐙 R: Type u_2

S: Type u_1

inst✝¹: Ring R

inst✝: LinearOrderedCommRing S

abv: AbsoluteValue R S

a, b: R

↑abv b - ↑abv a ≤ ↑abv (a - b)rw [R: Type u_2

S: Type u_1

inst✝¹: Ring R

inst✝: LinearOrderedCommRing S

abv: AbsoluteValue R S

a, b: R

↑abv b - ↑abv a ≤ ↑abv (a - b)abv: AbsoluteValue R S
abv.map_sub: ∀ {R : Type ?u.66876} {S : Type ?u.66875} [inst : Ring R] [inst_1 : OrderedCommRing S] (abv : AbsoluteValue R S)
  [inst_2 : NoZeroDivisors S] (a b : R), ↑abv (a - b) = ↑abv (b - a)
map_subR: Type u_2

S: Type u_1

inst✝¹: Ring R

inst✝: LinearOrderedCommRing S

abv: AbsoluteValue R S

a, b: R

↑abv b - ↑abv a ≤ ↑abv (b - a)]R: Type u_2

S: Type u_1

inst✝¹: Ring R

inst✝: LinearOrderedCommRing S

abv: AbsoluteValue R S

a, b: R

↑abv b - ↑abv a ≤ ↑abv (b - a);R: Type u_2

S: Type u_1

inst✝¹: Ring R

inst✝: LinearOrderedCommRing S

abv: AbsoluteValue R S

a, b: R

↑abv b - ↑abv a ≤ ↑abv (b - a) R: Type u_2

S: Type u_1

inst✝¹: Ring R

inst✝: LinearOrderedCommRing S

abv: AbsoluteValue R S

a, b: R

↑abv b - ↑abv a ≤ ↑abv (a - b)apply abv: AbsoluteValue R S
abv.le_sub: ∀ {R : Type ?u.67104} {S : Type ?u.67103} [inst : Ring R] [inst_1 : OrderedRing S] (abv : AbsoluteValue R S) (a b : R),
  ↑abv a - ↑abv b ≤ ↑abv (a - b)
le_sub
Goals accomplished! 🐙⟩
#align absolute_value.abs_abv_sub_le_abv_sub AbsoluteValue.abs_abv_sub_le_abv_sub: ∀ {R : Type u_2} {S : Type u_1} [inst : Ring R] [inst_1 : LinearOrderedCommRing S] (abv : AbsoluteValue R S) (a b : R),
  abs (↑abv a - ↑abv b) ≤ ↑abv (a - b)
AbsoluteValue.abs_abv_sub_le_abv_sub

end LinearOrderedCommRing

end AbsoluteValue

-- Porting note: Removed [] in fields, see
-- leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Infer.20kinds.20are.20unsupported

/-- A function `f` is an absolute value if it is nonnegative, zero only at 0, additive, and
multiplicative.
See also the type `AbsoluteValue` which represents a bundled version of absolute values.
-/
class IsAbsoluteValue: {S : Type u_1} → [inst : OrderedSemiring S] → {R : Type u_2} → [inst : Semiring R] → (R → S) → Prop
IsAbsoluteValue {S: ?m.67135
S} [OrderedSemiring: Type ?u.67138 → Type ?u.67138
OrderedSemiring S: ?m.67135
S] {R: ?m.67141
R} [Semiring: Type ?u.67144 → Type ?u.67144
Semiring R: ?m.67141
R] (f: R → S
f : R: ?m.67141
R → S: ?m.67135
S) : Prop: Type
Prop where
  /-- The absolute value is nonnegative -/
  abv_nonneg': ∀ {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] {f : R → S} [self : IsAbsoluteValue f]
  (x : R), 0 ≤ f x
abv_nonneg' : ∀ x: ?m.67153
x, 0: ?m.67158
0 ≤ f: R → S
f x: ?m.67153
x
  /-- The absolute value is positive definitive -/
  abv_eq_zero': ∀ {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] {f : R → S} [self : IsAbsoluteValue f]
  {x : R}, f x = 0 ↔ x = 0
abv_eq_zero' : ∀ {x: ?m.67487
x}, f: R → S
f x: ?m.67487
x = 0: ?m.67492
0 ↔ x: ?m.67487
x = 0: ?m.67510
0
  /-- The absolute value satisfies the triangle inequality -/
  abv_add': ∀ {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] {f : R → S} [self : IsAbsoluteValue f]
  (x y : R), f (x + y) ≤ f x + f y
abv_add' : ∀ x: ?m.67698
x y: ?m.67701
y, f: R → S
f (x: ?m.67698
x + y: ?m.67701
y) ≤ f: R → S
f x: ?m.67698
x + f: R → S
f y: ?m.67701
y
  /-- The absolute value is multiplicative -/
  abv_mul': ∀ {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] {f : R → S} [self : IsAbsoluteValue f]
  (x y : R), f (x * y) = f x * f y
abv_mul' : ∀ x: ?m.68272
x y: ?m.68275
y, f: R → S
f (x: ?m.68272
x * y: ?m.68275
y) = f: R → S
f x: ?m.68272
x * f: R → S
f y: ?m.68275
y
#align is_absolute_value IsAbsoluteValue: {S : Type u_1} → [inst : OrderedSemiring S] → {R : Type u_2} → [inst : Semiring R] → (R → S) → Prop
IsAbsoluteValue

namespace IsAbsoluteValue

section OrderedSemiring

variable {S: Type ?u.71634
S : Type _: Type (?u.71054+1)
Type _} [OrderedSemiring: Type ?u.72493 → Type ?u.72493
OrderedSemiring S: Type ?u.68820
S]

variable {R: Type ?u.68890
R : Type _: Type (?u.72496+1)
Type _} [Semiring: Type ?u.71643 → Type ?u.71643
Semiring R: Type ?u.68890
R] (abv: R → S
abv : R: Type ?u.68890
R → S: Type ?u.72490
S) [IsAbsoluteValue: {S : Type ?u.71071} → [inst : OrderedSemiring S] → {R : Type ?u.71070} → [inst : Semiring R] → (R → S) → Prop
IsAbsoluteValue abv: R → S
abv]

lemma abv_nonneg: ∀ {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R → S)
  [inst_2 : IsAbsoluteValue abv] (x : R), 0 ≤ abv x
abv_nonneg (x: R
x) : 0: ?m.68947
0 ≤ abv: R → S
abv x: ?m.68942
x := abv_nonneg': ∀ {S : Type ?u.69277} [inst : OrderedSemiring S] {R : Type ?u.69276} [inst_1 : Semiring R] {f : R → S}
  [self : IsAbsoluteValue f] (x : R), 0 ≤ f x
abv_nonneg' x: R
x
#align is_absolute_value.abv_nonneg IsAbsoluteValue.abv_nonneg: ∀ {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R → S)
  [inst_2 : IsAbsoluteValue abv] (x : R), 0 ≤ abv x
IsAbsoluteValue.abv_nonneg

open Lean Meta Mathlib Meta Positivity Qq in
/-- The `positivity` extension which identifies expressions of the form `abv a`. -/
@[positivity (_: α
_ : α: ?m.71047
α)]
def Mathlib.Meta.Positivity.evalAbv: PositivityExt
Mathlib.Meta.Positivity.evalAbv : PositivityExt: Type
PositivityExt where eval {_: ?m.69415
_ _α: ?m.69418
_α} _zα: ?m.69421
_zα _pα: ?m.69424
_pα e: ?m.69427
e := do
  let (.app: Expr → Expr → Expr
.app f: Expr
f a: Expr
a) ← whnfR: Expr → MetaM Expr
whnfR e: ?m.69427
e | throwError "not abv ·": ?m.69679 ?m.69680
throwErrorthrowError "not abv ·": ?m.69679 ?m.69680
 "not abv ·"
  let pa': ?m.69581
pa' ← mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``abv_nonneg: ∀ {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R → S)
  [inst_2 : IsAbsoluteValue abv] (x : R), 0 ≤ abv x
abv_nonneg #[f: Expr
f, a: Expr
a]
  pure: {f : Type ?u.69584 → Type ?u.69583} → [self : Pure f] → {α : Type ?u.69584} → α → f α
pure (.nonnegative: {u : Level} →
  {α : Q(Type u)} → {zα : Q(Zero «$α»)} → {pα : Q(PartialOrder «$α»)} → {e : Q(«$α»)} → Q(0 ≤ «$e») → Strictness zα pα e
.nonnegative pa': ?m.69581
pa')

lemma abv_eq_zero: ∀ {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R → S)
  [inst_2 : IsAbsoluteValue abv] {x : R}, abv x = 0 ↔ x = 0
abv_eq_zero {x: R
x} : abv: R → S
abv x: ?m.71112
x = 0: ?m.71117
0 ↔ x: ?m.71112
x = 0: ?m.71346
0 := abv_eq_zero': ∀ {S : Type ?u.71535} [inst : OrderedSemiring S] {R : Type ?u.71534} [inst_1 : Semiring R] {f : R → S}
  [self : IsAbsoluteValue f] {x : R}, f x = 0 ↔ x = 0
abv_eq_zero'
#align is_absolute_value.abv_eq_zero IsAbsoluteValue.abv_eq_zero: ∀ {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R → S)
  [inst_2 : IsAbsoluteValue abv] {x : R}, abv x = 0 ↔ x = 0
IsAbsoluteValue.abv_eq_zero

lemma abv_add: ∀ {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R → S)
  [inst_2 : IsAbsoluteValue abv] (x y : R), abv (x + y) ≤ abv x + abv y
abv_add (x: ?m.71692
x y: ?m.71695
y) : abv: R → S
abv (x: ?m.71692
x + y: ?m.71695
y) ≤ abv: R → S
abv x: ?m.71692
x + abv: R → S
abv y: ?m.71695
y := abv_add': ∀ {S : Type ?u.72402} [inst : OrderedSemiring S] {R : Type ?u.72401} [inst_1 : Semiring R] {f : R → S}
  [self : IsAbsoluteValue f] (x y : R), f (x + y) ≤ f x + f y
abv_add' x: R
x y: R
y
#align is_absolute_value.abv_add IsAbsoluteValue.abv_add: ∀ {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R → S)
  [inst_2 : IsAbsoluteValue abv] (x y : R), abv (x + y) ≤ abv x + abv y
IsAbsoluteValue.abv_add

lemma abv_mul: ∀ {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R → S)
  [inst_2 : IsAbsoluteValue abv] (x y : R), abv (x * y) = abv x * abv y
abv_mul (x: ?m.72548
x y: ?m.72551
y) : abv: R → S
abv (x: ?m.72548
x * y: ?m.72551
y) = abv: R → S
abv x: ?m.72548
x * abv: R → S
abv y: ?m.72551
y := abv_mul': ∀ {S : Type ?u.73180} [inst : OrderedSemiring S] {R : Type ?u.73179} [inst_1 : Semiring R] {f : R → S}
  [self : IsAbsoluteValue f] (x y : R), f (x * y) = f x * f y
abv_mul' x: R
x y: R
y
#align is_absolute_value.abv_mul IsAbsoluteValue.abv_mul: ∀ {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R → S)
  [inst_2 : IsAbsoluteValue abv] (x y : R), abv (x * y) = abv x * abv y
IsAbsoluteValue.abv_mul

/-- A bundled absolute value is an absolute value. -/
instance _root_.AbsoluteValue.isAbsoluteValue: ∀ {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : AbsoluteValue R S),
  IsAbsoluteValue ↑abv
_root_.AbsoluteValue.isAbsoluteValue (abv: AbsoluteValue R S
abv : AbsoluteValue: (R : Type ?u.73318) →
  (S : Type ?u.73317) → [inst : Semiring R] → [inst : OrderedSemiring S] → Type (max?u.73318?u.73317)
AbsoluteValue R: Type ?u.73265
R S: Type ?u.73259
S) :
    IsAbsoluteValue: {S : Type ?u.73339} → [inst : OrderedSemiring S] → {R : Type ?u.73338} → [inst : Semiring R] → (R → S) → Prop
IsAbsoluteValue abv: AbsoluteValue R S
abv where
  abv_nonneg' := abv: AbsoluteValue R S
abv.nonneg: ∀ {R : Type ?u.73799} {S : Type ?u.73798} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
  (x : R), 0 ≤ ↑abv x
nonneg
  abv_eq_zero' := abv: AbsoluteValue R S
abv.eq_zero: ∀ {R : Type ?u.73819} {S : Type ?u.73818} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
  {x : R}, ↑abv x = 0 ↔ x = 0
eq_zero
  abv_add' := abv: AbsoluteValue R S
abv.add_le: ∀ {R : Type ?u.73850} {S : Type ?u.73849} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
  (x y : R), ↑abv (x + y) ≤ ↑abv x + ↑abv y
add_le
  abv_mul' := abv: AbsoluteValue R S
abv.map_mul: ∀ {M : Type ?u.73880} {N : Type ?u.73881} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (a b : M),
  ↑f (a * b) = ↑f a * ↑f b
map_mul
#align absolute_value.is_absolute_value AbsoluteValue.isAbsoluteValue: ∀ {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : AbsoluteValue R S),
  IsAbsoluteValue ↑abv
AbsoluteValue.isAbsoluteValue

/-- Convert an unbundled `IsAbsoluteValue` to a bundled `AbsoluteValue`. -/
@[simps: ∀ {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R → S)
  [inst_2 : IsAbsoluteValue abv] (a : R), ↑(toAbsoluteValue abv) a = abv a
simps]
def toAbsoluteValue: {S : Type u_1} →
  [inst : OrderedSemiring S] →
    {R : Type u_2} → [inst_1 : Semiring R] → (abv : R → S) → [inst_2 : IsAbsoluteValue abv] → AbsoluteValue R S
toAbsoluteValue : AbsoluteValue: (R : Type ?u.74334) →
  (S : Type ?u.74333) → [inst : Semiring R] → [inst : OrderedSemiring S] → Type (max?u.74334?u.74333)
AbsoluteValue R: Type ?u.74281
R S: Type ?u.74275
S where
  toFun := abv: R → S
abv
  add_le' := abv_add': ∀ {S : Type ?u.74913} [inst : OrderedSemiring S] {R : Type ?u.74912} [inst_1 : Semiring R] {f : R → S}
  [self : IsAbsoluteValue f] (x y : R), f (x + y) ≤ f x + f y
abv_add'
  eq_zero' _: ?m.74856
_ := abv_eq_zero': ∀ {S : Type ?u.74859} [inst : OrderedSemiring S] {R : Type ?u.74858} [inst_1 : Semiring R] {f : R → S}
  [self : IsAbsoluteValue f] {x : R}, f x = 0 ↔ x = 0
abv_eq_zero'
  nonneg' := abv_nonneg': ∀ {S : Type ?u.74788} [inst : OrderedSemiring S] {R : Type ?u.74787} [inst_1 : Semiring R] {f : R → S}
  [self : IsAbsoluteValue f] (x : R), 0 ≤ f x
abv_nonneg'
  map_mul' := abv_mul': ∀ {S : Type ?u.74696} [inst : OrderedSemiring S] {R : Type ?u.74695} [inst_1 : Semiring R] {f : R → S}
  [self : IsAbsoluteValue f] (x y : R), f (x * y) = f x * f y
abv_mul'
#align is_absolute_value.to_absolute_value IsAbsoluteValue.toAbsoluteValue: {S : Type u_1} →
  [inst : OrderedSemiring S] →
    {R : Type u_2} → [inst_1 : Semiring R] → (abv : R → S) → [inst_2 : IsAbsoluteValue abv] → AbsoluteValue R S
IsAbsoluteValue.toAbsoluteValue
#align is_absolute_value.to_absolute_value_apply IsAbsoluteValue.toAbsoluteValue_apply: ∀ {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R → S)
  [inst_2 : IsAbsoluteValue abv] (a : R), ↑(toAbsoluteValue abv) a = abv a
IsAbsoluteValue.toAbsoluteValue_apply
#align is_absolute_value.to_absolute_value_to_mul_hom_apply IsAbsoluteValue.toAbsoluteValue_apply: ∀ {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R → S)
  [inst_2 : IsAbsoluteValue abv] (a : R), ↑(toAbsoluteValue abv) a = abv a
IsAbsoluteValue.toAbsoluteValue_apply

theorem abv_zero: abv 0 = 0
abv_zero : abv: R → S
abv 0: ?m.75172
0 = 0: ?m.75345
0 :=
  map_zero: ∀ {M : Type ?u.75574} {N : Type ?u.75575} {F : Type ?u.75573} [inst : Zero M] [inst_1 : Zero N]
  [inst_2 : ZeroHomClass F M N] (f : F), ↑f 0 = 0
map_zero (toAbsoluteValue: {S : Type ?u.75583} →
  [inst : OrderedSemiring S] →
    {R : Type ?u.75582} → [inst_1 : Semiring R] → (abv : R → S) → [inst_2 : IsAbsoluteValue abv] → AbsoluteValue R S
toAbsoluteValue abv: R → S
abv)
#align is_absolute_value.abv_zero IsAbsoluteValue.abv_zero: ∀ {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R → S)
  [inst_2 : IsAbsoluteValue abv], abv 0 = 0
IsAbsoluteValue.abv_zero

theorem abv_pos: ∀ {a : R}, 0 < abv a ↔ a ≠ 0
abv_pos {a: R
a : R: Type ?u.76125
R} : 0: ?m.76181
0 < abv: R → S
abv a: R
a ↔ a: R
a ≠ 0: ?m.76510
0 :=
  (toAbsoluteValue: {S : Type ?u.76685} →
  [inst : OrderedSemiring S] →
    {R : Type ?u.76684} → [inst_1 : Semiring R] → (abv : R → S) → [inst_2 : IsAbsoluteValue abv] → AbsoluteValue R S
toAbsoluteValue abv: R → S
abv).pos_iff: ∀ {R : Type ?u.76723} {S : Type ?u.76722} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
  {x : R}, 0 < ↑abv x ↔ x ≠ 0
pos_iff
#align is_absolute_value.abv_pos IsAbsoluteValue.abv_pos: ∀ {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R → S)
  [inst_2 : IsAbsoluteValue abv] {a : R}, 0 < abv a ↔ a ≠ 0
IsAbsoluteValue.abv_pos

end OrderedSemiring

section LinearOrderedRing

variable {S: Type ?u.76787
S : Type _: Type (?u.76787+1)
Type _} [LinearOrderedRing: Type ?u.76784 → Type ?u.76784
LinearOrderedRing S: Type ?u.76781
S]

instance abs_isAbsoluteValue: ∀ {S : Type u_1} [inst : LinearOrderedRing S], IsAbsoluteValue abs
abs_isAbsoluteValue : IsAbsoluteValue: {S : Type ?u.76794} → [inst : OrderedSemiring S] → {R : Type ?u.76793} → [inst : Semiring R] → (R → S) → Prop
IsAbsoluteValue (abs: {α : Type ?u.76818} → [self : Abs α] → α → α
abs : S: Type ?u.76787
S → S: Type ?u.76787
S) :=
  AbsoluteValue.abs: {S : Type ?u.77088} → [inst : LinearOrderedRing S] → AbsoluteValue S S
AbsoluteValue.abs.isAbsoluteValue: ∀ {S : Type ?u.77095} [inst : OrderedSemiring S] {R : Type ?u.77094} [inst_1 : Semiring R] (abv : AbsoluteValue R S),
  IsAbsoluteValue ↑abv
isAbsoluteValue
#align is_absolute_value.abs_is_absolute_value IsAbsoluteValue.abs_isAbsoluteValue: ∀ {S : Type u_1} [inst : LinearOrderedRing S], IsAbsoluteValue abs
IsAbsoluteValue.abs_isAbsoluteValue

end LinearOrderedRing

section OrderedRing

variable {S: Type ?u.77187
S : Type _: Type (?u.77335+1)
Type _} [OrderedRing: Type ?u.77184 → Type ?u.77184
OrderedRing S: Type ?u.77181
S]

section Semiring

variable {R: Type ?u.77193
R : Type _: Type (?u.77341+1)
Type _} [Semiring: Type ?u.78193 → Type ?u.78193
Semiring R: Type ?u.77193
R] (abv: R → S
abv : R: Type ?u.77574
R → S: Type ?u.78792
S) [IsAbsoluteValue: {S : Type ?u.77585} → [inst : OrderedSemiring S] → {R : Type ?u.77584} → [inst : Semiring R] → (R → S) → Prop
IsAbsoluteValue abv: R → S
abv]

variable [IsDomain: (α : Type ?u.78332) → [inst : Semiring α] → Prop
IsDomain S: Type ?u.77335
S]

theorem abv_one: ∀ [inst : Nontrivial R], abv 1 = 1
abv_one [Nontrivial: Type ?u.77801 → Prop
Nontrivial R: Type ?u.77574
R] : abv: R → S
abv 1: ?m.77806
1 = 1: ?m.77845
1 :=
  (toAbsoluteValue: {S : Type ?u.77998} →
  [inst : OrderedSemiring S] →
    {R : Type ?u.77997} → [inst_1 : Semiring R] → (abv : R → S) → [inst_2 : IsAbsoluteValue abv] → AbsoluteValue R S
toAbsoluteValue abv: R → S
abv).map_one: ∀ {R : Type ?u.78126} {S : Type ?u.78125} [inst : Semiring R] [inst_1 : OrderedRing S] (abv : AbsoluteValue R S)
  [inst_2 : IsDomain S] [inst_3 : Nontrivial R], ↑abv 1 = 1
map_one
#align is_absolute_value.abv_one IsAbsoluteValue.abv_one: ∀ {S : Type u_2} [inst : OrderedRing S] {R : Type u_1} [inst_1 : Semiring R] (abv : R → S)
  [inst_2 : IsAbsoluteValue abv] [inst_3 : IsDomain S] [inst_4 : Nontrivial R], abv 1 = 1
IsAbsoluteValue.abv_one

/-- `abv` as a `MonoidWithZeroHom`. -/
def abvHom: [inst : Nontrivial R] → R →*₀ S
abvHom [Nontrivial: Type ?u.78417 → Prop
Nontrivial R: Type ?u.78190
R] : R: Type ?u.78190
R →*₀ S: Type ?u.78184
S :=
  (toAbsoluteValue: {S : Type ?u.78569} →
  [inst : OrderedSemiring S] →
    {R : Type ?u.78568} → [inst_1 : Semiring R] → (abv : R → S) → [inst_2 : IsAbsoluteValue abv] → AbsoluteValue R S
toAbsoluteValue abv: R → S
abv).toMonoidWithZeroHom: {R : Type ?u.78668} →
  {S : Type ?u.78667} →
    [inst : Semiring R] →
      [inst_1 : OrderedRing S] → AbsoluteValue R S → [inst_2 : IsDomain S] → [inst_3 : Nontrivial R] → R →*₀ S
toMonoidWithZeroHom
#align is_absolute_value.abv_hom IsAbsoluteValue.abvHom: {S : Type u_1} →
  [inst : OrderedRing S] →
    {R : Type u_2} →
      [inst_1 : Semiring R] →
        (abv : R → S) → [inst_2 : IsAbsoluteValue abv] → [inst_3 : IsDomain S] → [inst_4 : Nontrivial R] → R →*₀ S
IsAbsoluteValue.abvHom

theorem abv_pow: ∀ [inst : Nontrivial R] (abv : R → S) [inst : IsAbsoluteValue abv] (a : R) (n : ℕ), abv (a ^ n) = abv a ^ n
abv_pow [Nontrivial: Type ?u.79025 → Prop
Nontrivial R: Type ?u.78798
R] (abv: R → S
abv : R: Type ?u.78798
R → S: Type ?u.78792
S) [IsAbsoluteValue: {S : Type ?u.79033} → [inst : OrderedSemiring S] → {R : Type ?u.79032} → [inst : Semiring R] → (R → S) → Prop
IsAbsoluteValue abv: R → S
abv] (a: R
a : R: Type ?u.78798
R) (n: ℕ
n : ℕ: Type
ℕ) :
    abv: R → S
abv (a: R
a ^ n: ℕ
n) = abv: R → S
abv a: R
a ^ n: ℕ
n :=
  map_pow: ∀ {G : Type ?u.79563} {H : Type ?u.79564} {F : Type ?u.79565} [inst : Monoid G] [inst_1 : Monoid H]
  [inst_2 : MonoidHomClass F G H] (f : F) (a : G) (n : ℕ), ↑f (a ^ n) = ↑f a ^ n
map_pow (toAbsoluteValue: {S : Type ?u.79573} →
  [inst : OrderedSemiring S] →
    {R : Type ?u.79572} → [inst_1 : Semiring R] → (abv : R → S) → [inst_2 : IsAbsoluteValue abv] → AbsoluteValue R S
toAbsoluteValue abv: R → S
abv) a: R
a n: ℕ
n
#align is_absolute_value.abv_pow IsAbsoluteValue.abv_pow: ∀ {S : Type u_2} [inst : OrderedRing S] {R : Type u_1} [inst_1 : Semiring R] [inst_2 : IsDomain S]
  [inst_3 : Nontrivial R] (abv : R → S) [inst_4 : IsAbsoluteValue abv] (a : R) (n : ℕ), abv (a ^ n) = abv a ^ n
IsAbsoluteValue.abv_pow

end Semiring

section Ring

variable {R: Type ?u.80372
R : Type _: Type (?u.80055+1)
Type _} [Ring: Type ?u.80058 → Type ?u.80058
Ring R: Type ?u.80055
R] (abv: R → S
abv : R: Type ?u.80055
R → S: Type ?u.80049
S) [IsAbsoluteValue: {S : Type ?u.80066} → [inst : OrderedSemiring S] → {R : Type ?u.80065} → [inst : Semiring R] → (R → S) → Prop
IsAbsoluteValue abv: R → S
abv]

theorem abv_sub_le: ∀ {S : Type u_1} [inst : OrderedRing S] {R : Type u_2} [inst_1 : Ring R] (abv : R → S) [inst_2 : IsAbsoluteValue abv]
  (a b c : R), abv (a - c) ≤ abv (a - b) + abv (b - c)
abv_sub_le (a: R
a b: R
b c: R
c : R: Type ?u.80372
R) : abv: R → S
abv (a: R
a - c: R
c) ≤ abv: R → S
abv (a: R
a - b: R
b) + abv: R → S
abv (b: R
b - c: R
c) := by
Goals accomplished! 🐙
  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)simpa [sub_eq_add_neg: ∀ {G : Type ?u.81062} [inst : SubNegMonoid G] (a b : G), a - b = a + -b
sub_eq_add_neg, add_assoc: ∀ {G : Type ?u.81078} [inst : AddSemigroup G] (a b c : G), a + b + c = a + (b + c)
add_assoc] using abv_add: ∀ {S : Type ?u.82152} [inst : OrderedSemiring S] {R : Type ?u.82153} [inst_1 : Semiring R] (abv : R → S)
  [inst_2 : IsAbsoluteValue abv] (x y : R), abv (x + y) ≤ abv x + abv y
abv_add abv: R → S
abv (a: R
a - b: R
b) (b: R
b - c: R
c)
Goals accomplished! 🐙
#align is_absolute_value.abv_sub_le IsAbsoluteValue.abv_sub_le: ∀ {S : Type u_1} [inst : OrderedRing S] {R : Type u_2} [inst_1 : Ring R] (abv : R → S) [inst_2 : IsAbsoluteValue abv]
  (a b c : R), abv (a - c) ≤ abv (a - b) + abv (b - c)
IsAbsoluteValue.abv_sub_le

theorem sub_abv_le_abv_sub: ∀ {S : Type u_1} [inst : OrderedRing S] {R : Type u_2} [inst_1 : Ring R] (abv : R → S) [inst_2 : IsAbsoluteValue abv]
  (a b : R), abv a - abv b ≤ abv (a - b)
sub_abv_le_abv_sub (a: R
a b: R
b : R: Type ?u.83601
R) : abv: R → S
abv a: R
a - abv: R → S
abv b: R
b ≤ abv: R → S
abv (a: R
a - b: R
b) :=
  (toAbsoluteValue: {S : Type ?u.84188} →
  [inst : OrderedSemiring S] →
    {R : Type ?u.84187} → [inst_1 : Semiring R] → (abv : R → S) → [inst_2 : IsAbsoluteValue abv] → AbsoluteValue R S
toAbsoluteValue abv: R → S
abv).le_sub: ∀ {R : Type ?u.84485} {S : Type ?u.84484} [inst : Ring R] [inst_1 : OrderedRing S] (abv : AbsoluteValue R S) (a b : R),
  ↑abv a - ↑abv b ≤ ↑abv (a - b)
le_sub a: R
a b: R
b
#align is_absolute_value.sub_abv_le_abv_sub IsAbsoluteValue.sub_abv_le_abv_sub: ∀ {S : Type u_1} [inst : OrderedRing S] {R : Type u_2} [inst_1 : Ring R] (abv : R → S) [inst_2 : IsAbsoluteValue abv]
  (a b : R), abv a - abv b ≤ abv (a - b)
IsAbsoluteValue.sub_abv_le_abv_sub

end Ring

end OrderedRing

section OrderedCommRing

variable {S: Type ?u.84529
S : Type _: Type (?u.84535+1)
Type _} [OrderedCommRing: Type ?u.84538 → Type ?u.84538
OrderedCommRing S: Type ?u.86188
S]

section Ring

variable {R: Type ?u.86194
R : Type _: Type (?u.85335+1)
Type _} [Ring: Type ?u.84544 → Type ?u.84544
Ring R: Type ?u.84541
R] (abv: R → S
abv : R: Type ?u.84541
R → S: Type ?u.84535
S) [IsAbsoluteValue: {S : Type ?u.84552} → [inst : OrderedSemiring S] → {R : Type ?u.84551} → [inst : Semiring R] → (R → S) → Prop
IsAbsoluteValue abv: R → S
abv]

variable [NoZeroDivisors: (M₀ : Type ?u.86463) → [inst : Mul M₀] → [inst : Zero M₀] → Prop
NoZeroDivisors S: Type ?u.84810
S]

theorem abv_neg: ∀ {S : Type u_1} [inst : OrderedCommRing S] {R : Type u_2} [inst_1 : Ring R] (abv : R → S)
  [inst_2 : IsAbsoluteValue abv] [inst : NoZeroDivisors S] (a : R), abv (-a) = abv a
abv_neg (a: R
a : R: Type ?u.85335
R) : abv: R → S
abv (-a: R
a) = abv: R → S
abv a: R
a :=
  (toAbsoluteValue: {S : Type ?u.85878} →
  [inst : OrderedSemiring S] →
    {R : Type ?u.85877} → [inst_1 : Semiring R] → (abv : R → S) → [inst_2 : IsAbsoluteValue abv] → AbsoluteValue R S
toAbsoluteValue abv: R → S
abv).map_neg: ∀ {R : Type ?u.86133} {S : Type ?u.86132} [inst : Ring R] [inst_1 : OrderedCommRing S] (abv : AbsoluteValue R S)
  [inst_2 : NoZeroDivisors S] (a : R), ↑abv (-a) = ↑abv a
map_neg a: R
a
#align is_absolute_value.abv_neg IsAbsoluteValue.abv_neg: ∀ {S : Type u_1} [inst : OrderedCommRing S] {R : Type u_2} [inst_1 : Ring R] (abv : R → S)
  [inst_2 : IsAbsoluteValue abv] [inst : NoZeroDivisors S] (a : R), abv (-a) = abv a
IsAbsoluteValue.abv_neg

theorem abv_sub: ∀ (a b : R), abv (a - b) = abv (b - a)
abv_sub (a: R
a b: R
b : R: Type ?u.86194
R) : abv: R → S
abv (a: R
a - b: R
b) = abv: R → S
abv (b: R
b - a: R
a) :=
  (toAbsoluteValue: {S : Type ?u.86811} →
  [inst : OrderedSemiring S] →
    {R : Type ?u.86810} → [inst_1 : Semiring R] → (abv : R → S) → [inst_2 : IsAbsoluteValue abv] → AbsoluteValue R S
toAbsoluteValue abv: R → S
abv).map_sub: ∀ {R : Type ?u.87066} {S : Type ?u.87065} [inst : Ring R] [inst_1 : OrderedCommRing S] (abv : AbsoluteValue R S)
  [inst_2 : NoZeroDivisors S] (a b : R), ↑abv (a - b) = ↑abv (b - a)
map_sub a: R
a b: R
b
#align is_absolute_value.abv_sub IsAbsoluteValue.abv_sub: ∀ {S : Type u_1} [inst : OrderedCommRing S] {R : Type u_2} [inst_1 : Ring R] (abv : R → S)
  [inst_2 : IsAbsoluteValue abv] [inst : NoZeroDivisors S] (a b : R), abv (a - b) = abv (b - a)
IsAbsoluteValue.abv_sub

end Ring

end OrderedCommRing

section LinearOrderedCommRing

variable {S: Type ?u.87129
S : Type _: Type (?u.87123+1)
Type _} [LinearOrderedCommRing: Type ?u.87126 → Type ?u.87126
LinearOrderedCommRing S: Type ?u.87123
S]

section Ring

variable {R: Type ?u.87396
R : Type _: Type (?u.87135+1)
Type _} [Ring: Type ?u.87138 → Type ?u.87138
Ring R: Type ?u.87135
R] (abv: R → S
abv : R: Type ?u.87135
R → S: Type ?u.87390
S) [IsAbsoluteValue: {S : Type ?u.87146} → [inst : OrderedSemiring S] → {R : Type ?u.87145} → [inst : Semiring R] → (R → S) → Prop
IsAbsoluteValue abv: R → S
abv]

theorem abs_abv_sub_le_abv_sub: ∀ {S : Type u_1} [inst : LinearOrderedCommRing S] {R : Type u_2} [inst_1 : Ring R] (abv : R → S)
  [inst_2 : IsAbsoluteValue abv] (a b : R), abs (abv a - abv b) ≤ abv (a - b)
abs_abv_sub_le_abv_sub (a: R
a b: R
b : R: Type ?u.87396
R) : abs: {α : Type ?u.87656} → [self : Abs α] → α → α
abs (abv: R → S
abv a: R
a - abv: R → S
abv b: R
b) ≤ abv: R → S
abv (a: R
a - b: R
b) :=
  (toAbsoluteValue: {S : Type ?u.87973} →
  [inst : OrderedSemiring S] →
    {R : Type ?u.87972} → [inst_1 : Semiring R] → (abv : R → S) → [inst_2 : IsAbsoluteValue abv] → AbsoluteValue R S
toAbsoluteValue abv: R → S
abv).abs_abv_sub_le_abv_sub: ∀ {R : Type ?u.88214} {S : Type ?u.88213} [inst : Ring R] [inst_1 : LinearOrderedCommRing S] (abv : AbsoluteValue R S)
  (a b : R), abs (↑abv a - ↑abv b) ≤ ↑abv (a - b)
abs_abv_sub_le_abv_sub a: R
a b: R
b
#align is_absolute_value.abs_abv_sub_le_abv_sub IsAbsoluteValue.abs_abv_sub_le_abv_sub: ∀ {S : Type u_1} [inst : LinearOrderedCommRing S] {R : Type u_2} [inst_1 : Ring R] (abv : R → S)
  [inst_2 : IsAbsoluteValue abv] (a b : R), abs (abv a - abv b) ≤ abv (a - b)
IsAbsoluteValue.abs_abv_sub_le_abv_sub

end Ring

end LinearOrderedCommRing

section LinearOrderedField

variable {S: Type ?u.90880
S : Type _: Type (?u.88273+1)
Type _} [LinearOrderedSemifield: Type ?u.88276 → Type ?u.88276
LinearOrderedSemifield S: Type ?u.88273
S]

section Semiring

variable {R: Type ?u.88373
R : Type _: Type (?u.88285+1)
Type _} [Semiring: Type ?u.88288 → Type ?u.88288
Semiring R: Type ?u.88285
R] [Nontrivial: Type ?u.88291 → Prop
Nontrivial R: Type ?u.88285
R] (abv: R → S
abv : R: Type ?u.88285
R → S: Type ?u.88279
S) [IsAbsoluteValue: {S : Type ?u.88299} → [inst : OrderedSemiring S] → {R : Type ?u.88298} → [inst : Semiring R] → (R → S) → Prop
IsAbsoluteValue abv: R → S
abv]

theorem abv_one': abv 1 = 1
abv_one' : abv: R → S
abv 1: ?m.88457
1 = 1: ?m.88496
1 :=
  (toAbsoluteValue: {S : Type ?u.88574} →
  [inst : OrderedSemiring S] →
    {R : Type ?u.88573} → [inst_1 : Semiring R] → (abv : R → S) → [inst_2 : IsAbsoluteValue abv] → AbsoluteValue R S
toAbsoluteValue abv: R → S
abv).map_one_of_isLeftRegular: ∀ {R : Type ?u.88639} {S : Type ?u.88638} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S),
  IsLeftRegular (↑abv 1) → ↑abv 1 = 1
map_one_of_isLeftRegular <|
    (isRegular_of_ne_zero: ∀ {R : Type ?u.88657} [inst : CancelMonoidWithZero R] {a : R}, a ≠ 0 → IsRegular a
isRegular_of_ne_zero <| (toAbsoluteValue: {S : Type ?u.88662} →
  [inst : OrderedSemiring S] →
    {R : Type ?u.88661} → [inst_1 : Semiring R] → (abv : R → S) → [inst_2 : IsAbsoluteValue abv] → AbsoluteValue R S
toAbsoluteValue abv: R → S
abv).ne_zero: ∀ {R : Type ?u.88671} {S : Type ?u.88672} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
  {x : R}, x ≠ 0 → ↑abv x ≠ 0
ne_zero one_ne_zero: ∀ {α : Type ?u.89176} [inst : Zero α] [inst_1 : One α] [inst_2 : NeZero 1], 1 ≠ 0
one_ne_zero).left: ∀ {R : Type ?u.89955} [inst : Mul R] {c : R}, IsRegular c → IsLeftRegular c
left
#align is_absolute_value.abv_one' IsAbsoluteValue.abv_one': ∀ {S : Type u_1} [inst : LinearOrderedSemifield S] {R : Type u_2} [inst_1 : Semiring R] [inst_2 : Nontrivial R]
  (abv : R → S) [inst_3 : IsAbsoluteValue abv], abv 1 = 1
IsAbsoluteValue.abv_one'

/-- An absolute value as a monoid with zero homomorphism, assuming the target is a semifield. -/
def abvHom': R →*₀ S
abvHom' : R: Type ?u.90155
R →*₀ S: Type ?u.90149
S :=
  ⟨⟨abv: R → S
abv, abv_zero: ∀ {S : Type ?u.90438} [inst : OrderedSemiring S] {R : Type ?u.90439} [inst_1 : Semiring R] (abv : R → S)
  [inst_2 : IsAbsoluteValue abv], abv 0 = 0
abv_zero abv: R → S
abv⟩, abv_one': ∀ {S : Type ?u.90706} [inst : LinearOrderedSemifield S] {R : Type ?u.90707} [inst_1 : Semiring R]
  [inst_2 : Nontrivial R] (abv : R → S) [inst_3 : IsAbsoluteValue abv], abv 1 = 1
abv_one' abv: R → S
abv, abv_mul: ∀ {S : Type ?u.90734} [inst : OrderedSemiring S] {R : Type ?u.90735} [inst_1 : Semiring R] (abv : R → S)
  [inst_2 : IsAbsoluteValue abv] (x y : R), abv (x * y) = abv x * abv y
abv_mul abv: R → S
abv⟩
#align is_absolute_value.abv_hom' IsAbsoluteValue.abvHom': {S : Type u_1} →
  [inst : LinearOrderedSemifield S] →
    {R : Type u_2} →
      [inst_1 : Semiring R] → [inst_2 : Nontrivial R] → (abv : R → S) → [inst_3 : IsAbsoluteValue abv] → R →*₀ S
IsAbsoluteValue.abvHom'

end Semiring

section DivisionSemiring

variable {R: Type ?u.91080
R : Type _: Type (?u.92071+1)
Type _} [DivisionSemiring: Type ?u.90889 → Type ?u.90889
DivisionSemiring R: Type ?u.90886
R] (abv: R → S
abv : R: Type ?u.90886
R → S: Type ?u.90880
S) [IsAbsoluteValue: {S : Type ?u.91091} → [inst : OrderedSemiring S] → {R : Type ?u.91090} → [inst : Semiring R] → (R → S) → Prop
IsAbsoluteValue abv: R → S
abv]

theorem abv_inv: ∀ (a : R), abv a⁻¹ = (abv a)⁻¹
abv_inv (a: R
a : R: Type ?u.91080
R) : abv: R → S
abv a: R
a⁻¹ = (abv: R → S
abv a: R
a)⁻¹ :=
  map_inv₀: ∀ {G₀ : Type ?u.91391} {G₀' : Type ?u.91390} {F : Type ?u.91392} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero G₀']
  [inst_2 : MonoidWithZeroHomClass F G₀ G₀'] (f : F) (a : G₀), ↑f a⁻¹ = (↑f a)⁻¹
map_inv₀ (abvHom': {S : Type ?u.91400} →
  [inst : LinearOrderedSemifield S] →
    {R : Type ?u.91399} →
      [inst_1 : Semiring R] → [inst_2 : Nontrivial R] → (abv : R → S) → [inst_3 : IsAbsoluteValue abv] → R →*₀ S
abvHom' abv: R → S
abv) a: R
a
#align is_absolute_value.abv_inv IsAbsoluteValue.abv_inv: ∀ {S : Type u_1} [inst : LinearOrderedSemifield S] {R : Type u_2} [inst_1 : DivisionSemiring R] (abv : R → S)
  [inst_2 : IsAbsoluteValue abv] (a : R), abv a⁻¹ = (abv a)⁻¹
IsAbsoluteValue.abv_inv

theorem abv_div: ∀ (a b : R), abv (a / b) = abv a / abv b
abv_div (a: R
a b: R
b : R: Type ?u.92071
R) : abv: R → S
abv (a: R
a / b: R
b) = abv: R → S
abv a: R
a / abv: R → S
abv b: R
b :=
  map_div₀: ∀ {G₀ : Type ?u.92467} {G₀' : Type ?u.92466} {F : Type ?u.92468} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero G₀']
  [inst_2 : MonoidWithZeroHomClass F G₀ G₀'] (f : F) (a b : G₀), ↑f (a / b) = ↑f a / ↑f b
map_div₀ (abvHom': {S : Type ?u.92476} →
  [inst : LinearOrderedSemifield S] →
    {R : Type ?u.92475} →
      [inst_1 : Semiring R] → [inst_2 : Nontrivial R] → (abv : R → S) → [inst_3 : IsAbsoluteValue abv] → R →*₀ S
abvHom' abv: R → S
abv) a: R
a b: R
b
#align is_absolute_value.abv_div IsAbsoluteValue.abv_div: ∀ {S : Type u_1} [inst : LinearOrderedSemifield S] {R : Type u_2} [inst_1 : DivisionSemiring R] (abv : R → S)
  [inst_2 : IsAbsoluteValue abv] (a b : R), abv (a / b) = abv a / abv b
IsAbsoluteValue.abv_div

end DivisionSemiring

end LinearOrderedField

end IsAbsoluteValue