awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
ι : Type u_1
α : Type u_2
R_1 : Type u_3
S_1 : Type u_4
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder 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 ≤ { toFun := toFun, map_mul' := map_mul' : R →ₙ* S }.toFun x
eq_zero' : ∀ (x : R), { toFun := toFun, map_mul' := map_mul' : R →ₙ* S }.toFun x = 0 ↔ x = 0
add_le' :
  ∀ (x y : R),
    { toFun := toFun, map_mul' := map_mul' : R →ₙ* S }.toFun (x + y) ≤
      { toFun := toFun, map_mul' := map_mul' : R →ₙ* S }.toFun x +
        { toFun := toFun, map_mul' := map_mul' : R →ₙ* S }.toFun y
h :
  Eq (α := (a : R) → S)
    ((fun (f : AbsoluteValue R S) ↦ f.toFun)
      { toFun := toFun, map_mul' := map_mul', nonneg' := nonneg', eq_zero' := eq_zero', add_le' := add_le' })
    ((fun (f : AbsoluteValue R S) ↦ f.toFun) g)
obtain :
  ∀ (toFun_1 : R → S) (map_mul'_1 : ∀ (x y : R), toFun_1 (x * y) = toFun_1 x * toFun_1 y)
    (nonneg'_1 : ∀ (x : R), 0 ≤ { toFun := toFun_1, map_mul' := map_mul'_1 : R →ₙ* S }.toFun x)
    (eq_zero'_1 : ∀ (x : R), { toFun := toFun_1, map_mul' := map_mul'_1 : R →ₙ* S }.toFun x = 0 ↔ x = 0)
    (add_le'_1 :
      ∀ (x y : R),
        { toFun := toFun_1, map_mul' := map_mul'_1 : R →ₙ* S }.toFun (x + y) ≤
          { toFun := toFun_1, map_mul' := map_mul'_1 : R →ₙ* S }.toFun x +
            { toFun := toFun_1, map_mul' := map_mul'_1 : R →ₙ* S }.toFun y)
    (h :
      Eq (α := (a : R) → S)
        ((fun (f : AbsoluteValue R S) ↦ f.toFun)
          { toFun := toFun, map_mul' := map_mul', nonneg' := nonneg', eq_zero' := eq_zero', add_le' := add_le' })
        ((fun (f : AbsoluteValue R S) ↦ f.toFun)
          { toFun := toFun_1, map_mul' := map_mul'_1, nonneg' := nonneg'_1, eq_zero' := eq_zero'_1,
            add_le' := add_le'_1 })),
    { toFun := toFun, map_mul' := map_mul', nonneg' := nonneg', eq_zero' := eq_zero', add_le' := add_le' :
        AbsoluteValue R S } =
      { toFun := toFun_1, map_mul' := map_mul'_1, nonneg' := nonneg'_1, eq_zero' := eq_zero'_1, add_le' := add_le'_1 }
⊢ { toFun := toFun, map_mul' := map_mul', nonneg' := nonneg', eq_zero' := eq_zero', add_le' := add_le' :
      AbsoluteValue R S } =
    g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := g
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
ι : Type u_1
α : Type u_2
R_1 : Type u_3
S_1 : Type u_4
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
toFun : R → S
map_mul' : ∀ (x y : R), toFun (x * y) = toFun x * toFun y
nonneg' : ∀ (x : R), 0 ≤ { toFun := toFun, map_mul' := map_mul' : R →ₙ* S }.toFun x
eq_zero' : ∀ (x : R), { toFun := toFun, map_mul' := map_mul' : R →ₙ* S }.toFun x = 0 ↔ x = 0
add_le' :
  ∀ (x y : R),
    { toFun := toFun, map_mul' := map_mul' : R →ₙ* S }.toFun (x + y) ≤
      { toFun := toFun, map_mul' := map_mul' : R →ₙ* S }.toFun x +
        { toFun := toFun, map_mul' := map_mul' : R →ₙ* S }.toFun y
toFun_1 : R → S
map_mul'_1 : ∀ (x y : R), toFun_1 (x * y) = toFun_1 x * toFun_1 y
nonneg'_1 : ∀ (x : R), 0 ≤ { toFun := toFun_1, map_mul' := map_mul'_1 : R →ₙ* S }.toFun x
eq_zero'_1 : ∀ (x : R), { toFun := toFun_1, map_mul' := map_mul'_1 : R →ₙ* S }.toFun x = 0 ↔ x = 0
add_le'_1 :
  ∀ (x y : R),
    { toFun := toFun_1, map_mul' := map_mul'_1 : R →ₙ* S }.toFun (x + y) ≤
      { toFun := toFun_1, map_mul' := map_mul'_1 : R →ₙ* S }.toFun x +
        { toFun := toFun_1, map_mul' := map_mul'_1 : R →ₙ* S }.toFun y
h :
  Eq (α := (a : R) → S)
    ((fun (f : AbsoluteValue R S) ↦ f.toFun)
      { toFun := toFun, map_mul' := map_mul', nonneg' := nonneg', eq_zero' := eq_zero', add_le' := add_le' })
    ((fun (f : AbsoluteValue R S) ↦ f.toFun)
      { toFun := toFun_1, map_mul' := map_mul'_1, nonneg' := nonneg'_1, eq_zero' := eq_zero'_1, add_le' := add_le'_1 })
⊢ { toFun := toFun, map_mul' := map_mul', nonneg' := nonneg', eq_zero' := eq_zero', add_le' := add_le' :
      AbsoluteValue R S } =
    { toFun := toFun_1, map_mul' := map_mul'_1, nonneg' := nonneg'_1, eq_zero' := eq_zero'_1, add_le' := add_le'_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
ι : Type u_1
α : Type u_2
R_1 : Type u_3
S_1 : Type u_4
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
⊢ MulHomClass (AbsoluteValue R S) R S

Tactic:
{ AbsoluteValue.zeroHomClass (R := R) (S := S) with map_mul := fun f => f.map_mul' }

Premises used: AbsoluteValue.toMulHom, MulHom.map_mul', AbsoluteValue.zeroHomClass, MulHomClass.mk
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
ι : Type u_1
α : Type u_2
R_1 : Type u_3
S_1 : Type u_4
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
⊢ NonnegHomClass (AbsoluteValue R S) R S

Tactic:
{ AbsoluteValue.zeroHomClass (R := R) (S := S) with apply_nonneg := fun f => f.nonneg' }

Premises used: AbsoluteValue.nonneg', AbsoluteValue.zeroHomClass, NonnegHomClass.mk
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
ι : Type u_1
α : Type u_2
R_1 : Type u_3
S_1 : Type u_4
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
⊢ SubadditiveHomClass (AbsoluteValue R S) R S

Tactic:
{ AbsoluteValue.zeroHomClass (R := R) (S := S) with map_add_le_add := fun f => f.add_le' }

Premises used: AbsoluteValue.zeroHomClass, SubadditiveHomClass.mk, AbsoluteValue.add_le'
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
f : R →ₙ* S
h₁ : ∀ (x : R), 0 ≤ f.toFun x
h₂ : ∀ (x : R), f.toFun x = 0 ↔ x = 0
h₃ : ∀ (x y : R), f.toFun (x + y) ≤ f.toFun x + f.toFun y
⊢ Eq (α := (a : R) → S)
    (⇑{ toMulHom := f, nonneg' := h₁, eq_zero' := h₂, add_le' := h₃ : AbsoluteValue R S } : (a : R) → S)
    (⇑f : (a : R) → S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
f g : AbsoluteValue R S
⊢ (∀ (x : R), Eq.{u_6 + 1} (α := S) ((f : (a : R) → S) x : S) ((g : (a : R) → S) x : S)) → f = g

Tactic:
DFunLike.ext _ _

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
⊢ Eq (α := (a : R) → S) (⇑abv.toMulHom : (a : R) → S) (⇑abv : (a : R) → S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
x : R
⊢ LE.le.{u_6} (α := S) (0 : S) ((abv : (a : R) → S) x : S)

Tactic:
abv.nonneg' x

Premises used: AbsoluteValue.nonneg'
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
x : R
⊢ Eq.{u_6 + 1} (α := S) ((abv : (a : R) → S) x : S) (0 : S) ↔ x = 0

Tactic:
abv.eq_zero' x

Premises used: AbsoluteValue.eq_zero'
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
x y : R
⊢ (abv : (a : R) → S) (x + y) ≤ HAdd.hAdd (α := S) (β := S) ((abv : (a : R) → S) x : S) ((abv : (a : R) → S) y : S)

Tactic:
abv.add_le' x y

Premises used: AbsoluteValue.add_le'
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
inst_3 : AddLeftMono S
⊢ LE.le.{u_6} (α := S) ((abv : (a : R) → S) (List.sum []) : S)
    (List.sum (List.map.{u_5, u_6} (α := R) (⇑abv : (a : R) → S) []) : S)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
inst_3 : AddLeftMono S
head : R
tail : List R
ih : LE.le.{u_6} (α := S) ((abv : (a : R) → S) tail.sum : S) (List.sum (List.map (⇑abv : (a : R) → S) tail) : S)
⊢ LE.le.{u_6} (α := S) ((abv : (a : R) → S) (head :: tail).sum : S)
    (List.sum (List.map (⇑abv : (a : R) → S) (head :: tail)) : S)

Tactic:
(abv.add_le ..).trans <| add_le_add_right ih (abv head)

Premises used: List.sum, add_le_add_right, AbsoluteValue.add_le, LE.le.trans, List.foldr, DFunLike.coe
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
inst_3 : AddLeftMono S
head : R
tail : List R
ih : LE.le.{u_6} (α := S) ((abv : (a : R) → S) tail.sum : S) (List.sum (List.map (⇑abv : (a : R) → S) tail) : S)
⊢ LE.le.{u_6} (α := S) ((abv : (a : R) → S) (head :: tail).sum : S)
    (List.sum (List.map (⇑abv : (a : R) → S) (head :: tail)) : S)

Tactic:
exact (abv.add_le ..).trans <| add_le_add_right ih (abv head)

Premises used: add_le_add_right, AbsoluteValue.add_le, LE.le.trans, DFunLike.coe
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
inst_3 : AddLeftMono S
l : List R
nil :
  LE.le.{u_6} (α := S) ((abv : (a : R) → S) (List.sum []) : S)
    (List.sum (List.map.{u_5, u_6} (α := R) (⇑abv : (a : R) → S) []) : S)
cons :
  ∀ (head : R) (tail : List R)
    (ih : LE.le.{u_6} (α := S) ((abv : (a : R) → S) tail.sum : S) (List.sum (List.map (⇑abv : (a : R) → S) tail) : S)),
    LE.le.{u_6} (α := S) ((abv : (a : R) → S) (head :: tail).sum : S)
      (List.sum (List.map (⇑abv : (a : R) → S) (head :: tail)) : S)
⊢ LE.le.{u_6} (α := S) ((abv : (a : R) → S) l.sum : S) (List.sum (List.map (⇑abv : (a : R) → S) l) : S)

Tactic:
induction l with
  | nil => simp
  | cons head tail ih => exact (abv.add_le ..).trans <| add_le_add_right ih (abv head)

Premises used: AbsoluteValue.add_le, LE.le.trans
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
x y : R
⊢ (abv : (a : R) → S) (x * y) = HMul.hMul (α := S) (β := S) ((abv : (a : R) → S) x : S) ((abv : (a : R) → S) y : S)

Tactic:
abv.map_mul' x y

Premises used: AbsoluteValue.toMulHom, MulHom.map_mul'
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
x : R
⊢ Ne.{u_6 + 1} (α := S) ((abv : (a : R) → S) x : S) (0 : S) ↔ x ≠ 0

Tactic:
abv.eq_zero.not

Premises used: AbsoluteValue.eq_zero, Iff.not
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
x : R
⊢ LT.lt.{u_6} (α := S) (0 : S) ((abv : (a : R) → S) x : S) ↔ x ≠ 0

Tactic:
(abv.nonneg x).lt_iff_ne'.trans abv.ne_zero_iff

Premises used: AbsoluteValue.nonneg, AbsoluteValue.ne_zero_iff, Iff.trans, LE.le.lt_iff_ne'
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
x : R
⊢ LE.le.{u_6} (α := S) ((abv : (a : R) → S) x : S) (0 : S) ↔ x = 0

Tactic:
simp only [← abv.eq_zero, le_antisymm_iff, abv.nonneg, and_true]

Premises used: AbsoluteValue.eq_zero, and_true, AbsoluteValue.nonneg, le_antisymm_iff
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
h : IsLeftRegular.{u_6} (R := S) ((abv : (a : R) → S) 1 : S)
⊢ Eq.{u_6 + 1} (α := S) ((fun (x : S) ↦ HMul.hMul (α := S) ((abv : (a : R) → S) 1 : S) x) ((abv : (a : R) → S) 1))
    ((fun (x : S) ↦ HMul.hMul (α := S) ((abv : (a : R) → S) 1 : S) x) 1)

Tactic:
simp [← abv.map_mul]

Premises used: AbsoluteValue.map_mul
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
⊢ Eq.{u_6 + 1} (α := S) ((abv : (a : R) → S) 0 : S) (0 : S)

Tactic:
abv.eq_zero.2 rfl

Premises used: Iff.mpr, AbsoluteValue.eq_zero, rfl
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Ring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
a b c : R
⊢ (abv : (a : R) → S) (a - c) ≤
    HAdd.hAdd (α := S) (β := S) ((abv : (a : R) → S) (a - b) : S) ((abv : (a : R) → S) (b - c) : S)

Tactic:
simpa [sub_eq_add_neg, add_assoc] using abv.add_le (a - b) (b - c)

Premises used: add_assoc, sub_eq_add_neg, HSub.hSub, AbsoluteValue.add_le
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Ring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
a b : R
⊢ Eq.{u_6 + 1} (α := S) ((abv : (a : R) → S) (a - b) : S) (0 : S) ↔ a = b

Tactic:
abv.eq_zero.trans sub_eq_zero

Premises used: AbsoluteValue.eq_zero, sub_eq_zero, Iff.trans
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
inst_3 : IsDomain S
inst_4 : Nontrivial R
⊢ Eq.{u_6 + 1} (α := S) ((abv : (a : R) → S) 1 : S) (1 : S)

Tactic:
abv.map_one_of_isLeftRegular (IsRegular.of_ne_zero <| abv.ne_zero one_ne_zero).left

Premises used: AbsoluteValue.map_one_of_isLeftRegular, IsRegular.of_ne_zero, AbsoluteValue.ne_zero, IsRegular.left, one_ne_zero
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
ι : Type u_1
α : Type u_2
R_1 : Type u_3
S_1 : Type u_4
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
inst_3 : IsDomain S
inst_4 : Nontrivial R
⊢ MonoidWithZeroHomClass (AbsoluteValue R S) R S

Tactic:
{ AbsoluteValue.mulHomClass with
    map_zero := fun f => f.map_zero
    map_one := fun f => f.map_one }

Premises used: MonoidWithZeroHomClass.mk, AbsoluteValue.mulHomClass
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
inst_3 : IsDomain S
inst_4 : Nontrivial R
⊢ Eq (α := (a : R) → S) (⇑abv.toMonoidWithZeroHom : (a : R) → S) (⇑abv : (a : R) → S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
inst_3 : IsDomain S
inst_4 : Nontrivial R
⊢ Eq (α := (a : R) → S) (⇑abv.toMonoidHom : (a : R) → S) (⇑abv : (a : R) → S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
inst_3 : IsDomain S
inst_4 : Nontrivial R
a : R
n : ℕ
⊢ (abv : (a : R) → S) (a ^ n) = HPow.hPow (α := S) ((abv : (a : R) → S) a : S) n

Tactic:
abv.toMonoidHom.map_pow a n

Premises used: AbsoluteValue.toMonoidHom, MonoidHom.map_pow
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
inst_3 : IsDomain S
inst_4 : IsOrderedRing S
n : ℕ
inl : Subsingleton R → LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑n : R) : S) ((↑n : S) : S)
inr : Nontrivial R → LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑n : R) : S) ((↑n : S) : S)
⊢ LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑n : R) : S) ((↑n : S) : S)

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
inst_3 : IsDomain S
inst_4 : IsOrderedRing S
n : ℕ
h : Subsingleton R
⊢ LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑n : R) : S) ((↑n : S) : S)

Tactic:
simp [Subsingleton.eq_zero (n : R)]

Premises used: Nat.cast, Subsingleton.eq_zero
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
inst_3 : IsDomain S
inst_4 : IsOrderedRing S
h : Nontrivial R
⊢ LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑0 : R) : S) ((↑0 : S) : S)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
inst_3 : IsDomain S
inst_4 : IsOrderedRing S
h : Nontrivial R
n : ℕ
ih : LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑n : R) : S) ((↑n : S) : S)
inr : LE.le.{u_6} (α := S) ((abv : (a : R) → S) (HAdd.hAdd (α := R) (↑n : R) 1) : S) ((↑(n + 1) : S) : S)
inr₁ : (abv : (a : R) → S) (HAdd.hAdd (α := R) (↑n : R) 1) ≤ HAdd.hAdd (α := S) (↑n : S) 1
inr₂ :
  HAdd.hAdd (α := S) (β := S) ((abv : (a : R) → S) (↑n : R) : S) ((abv : (a : R) → S) 1 : S) ≤
    HAdd.hAdd (α := S) (↑n : S) 1
inr₃ : HAdd.hAdd (α := S) (β := S) ((abv : (a : R) → S) (↑n : R) : S) (1 : S) ≤ HAdd.hAdd (α := S) (↑n : S) 1
inr₄ inr₅ : HAdd.hAdd (α := S) (↑n : S) 1 ≤ HAdd.hAdd (α := S) (↑n : S) 1
⊢ LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑(n + 1) : R) : S) ((↑(n + 1) : S) : S)

Tactic:
grw [Nat.cast_succ, Nat.cast_succ, abv.add_le, abv.map_one, ih]

Premises used: Nat.cast_succ, AbsoluteValue.add_le, AbsoluteValue.map_one
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
inst_3 : IsDomain S
inst_4 : IsOrderedRing S
n : ℕ
h : Nontrivial R
inr : LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑0 : R) : S) ((↑0 : S) : S)
inr₁ :
  ∀ (n : ℕ) (ih : LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑n : R) : S) ((↑n : S) : S)),
    LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑(n + 1) : R) : S) ((↑(n + 1) : S) : S)
⊢ LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑n : R) : S) ((↑n : S) : S)

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
  · grw [Nat.cast_succ, Nat.cast_succ, abv.add_le, abv.map_one, ih]

Premises used: Nat.cast_succ, AbsoluteValue.add_le, AbsoluteValue.map_one
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
S : Type u_6
inst : Ring R
inst_1 : Ring S
inst_2 : PartialOrder S
inst_3 : IsOrderedRing S
abv : AbsoluteValue R S
a b : R
⊢ (abv : (a : R) → S) a ≤ HAdd.hAdd (α := S) (β := S) ((abv : (a : R) → S) (a - b) : S) ((abv : (a : R) → S) b : S)

Tactic:
simpa using abv.add_le (a - b) b

Premises used: HSub.hSub, AbsoluteValue.add_le
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : Ring R
abv : AbsoluteValue R S
inst_4 : NoZeroDivisors S
a : R
pos : ∀ (ha : a = 0), Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (-a) : S) ((abv : (a : R) → S) a : S)
neg : ∀ (ha : ¬a = 0), Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (-a) : S) ((abv : (a : R) → S) a : S)
⊢ Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (-a) : S) ((abv : (a : R) → S) a : S)

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : Ring R
abv : AbsoluteValue R S
inst_4 : NoZeroDivisors S
a : R
ha : a = 0
⊢ Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (-a) : S) ((abv : (a : R) → S) a : S)

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : Ring R
abv : AbsoluteValue R S
inst_4 : NoZeroDivisors S
a : R
ha : ¬a = 0
rw : (abv : (a : R) → S) (-a * -a) = HMul.hMul (α := S) (β := S) ((abv : (a : R) → S) a : S) ((abv : (a : R) → S) a : S)
rw₁ : (abv : (a : R) → S) (a * a) = HMul.hMul (α := S) (β := S) ((abv : (a : R) → S) a : S) ((abv : (a : R) → S) a : S)
rw₂ rw₃ :
  HMul.hMul (α := S) (β := S) ((abv : (a : R) → S) a : S) ((abv : (a : R) → S) a : S) =
    HMul.hMul (α := S) (β := S) ((abv : (a : R) → S) a : S) ((abv : (a : R) → S) a : S)
⊢ HMul.hMul (α := S) (β := S) ((abv : (a : R) → S) (-a) : S) ((abv : (a : R) → S) (-a) : S) =
    HMul.hMul (α := S) (β := S) ((abv : (a : R) → S) a : S) ((abv : (a : R) → S) a : S)

Tactic:
rw [← abv.map_mul, neg_mul_neg, abv.map_mul]

Premises used: neg_mul_neg, AbsoluteValue.map_mul
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : Ring R
abv : AbsoluteValue R S
inst_4 : NoZeroDivisors S
a : R
ha : ¬a = 0
neg : ¬Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (-a) : S) (-(abv : (a : R) → S) a : S)
⊢ Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (-a) : S) ((abv : (a : R) → S) a : S)

Tactic:
refine
    (mul_self_eq_mul_self_iff.mp (by rw [← abv.map_mul, neg_mul_neg, abv.map_mul])).resolve_right ?_

Premises used: mul_self_eq_mul_self_iff, Iff.mp, Or.resolve_right
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : Ring R
abv : AbsoluteValue R S
inst_4 : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ ¬Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (-a) : S) (-(abv : (a : R) → S) a : S)

Tactic:
((neg_lt_zero.mpr (abv.pos ha)).trans (abv.pos (neg_ne_zero.mpr ha))).ne'

Premises used: Iff.mpr, neg_lt_zero, AbsoluteValue.pos, LT.lt.ne', LT.lt.trans, neg_ne_zero
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : Ring R
abv : AbsoluteValue R S
inst_4 : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ ¬Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (-a) : S) (-(abv : (a : R) → S) a : S)

Tactic:
exact ((neg_lt_zero.mpr (abv.pos ha)).trans (abv.pos (neg_ne_zero.mpr ha))).ne'

Premises used: Iff.mpr, neg_lt_zero, AbsoluteValue.pos, LT.lt.ne', LT.lt.trans, neg_ne_zero
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : Ring R
abv : AbsoluteValue R S
inst_4 : NoZeroDivisors S
a b : R
rw : Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (-(b - a)) : S) ((abv : (a : R) → S) (b - a) : S)
rw₁ rw₂ : Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (b - a) : S) ((abv : (a : R) → S) (b - a) : S)
⊢ Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (a - b) : S) ((abv : (a : R) → S) (b - a) : S)

Tactic:
rw [← neg_sub, abv.map_neg]

Premises used: AbsoluteValue.map_neg, neg_sub
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : Ring R
abv : AbsoluteValue R S
inst_4 : NoZeroDivisors S
a b : R
⊢ HSub.hSub (α := S) (β := S) ((abv : (a : R) → S) a : S) ((abv : (a : R) → S) b : S) ≤ (abv : (a : R) → S) (a + b)

Tactic:
simpa only [tsub_le_iff_right, add_neg_cancel_right, abv.map_neg] using abv.add_le (a + b) (-b)

Premises used: AbsoluteValue.map_neg, add_neg_cancel_right, tsub_le_iff_right, HAdd.hAdd, AbsoluteValue.add_le, Neg.neg
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : Ring R
abv : AbsoluteValue R S
inst_4 : NoZeroDivisors S
a b : R
⊢ (abv : (a : R) → S) (a - b) ≤ HAdd.hAdd (α := S) (β := S) ((abv : (a : R) → S) a : S) ((abv : (a : R) → S) b : S)

Tactic:
simpa only [← sub_eq_add_neg, AbsoluteValue.map_neg] using abv.add_le a (-b)

Premises used: AbsoluteValue.map_neg, sub_eq_add_neg, AbsoluteValue.add_le, Neg.neg