awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y_1 : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
y z : FiniteResidueField K
x : FiniteElement K
h : (FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x ≤ y
mk :
  ∀ (y : FiniteElement K)
    (h :
      LE.le (α := FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)),
    HAdd.hAdd (α := FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K) z ≤
      HAdd.hAdd (α := FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K) z
⊢ HAdd.hAdd (α := FiniteResidueField K)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K) z ≤
    y + z

Tactic:
induction y with | mk y

Premises used: ArchimedeanClass.FiniteResidueField.mk
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y_1 : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
z : FiniteResidueField K
x y : FiniteElement K
h :
  LE.le (α := FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
mk :
  ∀ (z : FiniteElement K),
    HAdd.hAdd (α := FiniteResidueField K) (β := FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K) ≤
      HAdd.hAdd (α := FiniteResidueField K) (β := FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K)
⊢ HAdd.hAdd (α := FiniteResidueField K)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K) z ≤
    HAdd.hAdd (α := FiniteResidueField K)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K) z

Tactic:
induction z with | mk z

Premises used: ArchimedeanClass.FiniteResidueField.mk
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y_1 : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x y : FiniteElement K
h :
  LE.le (α := FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
z : FiniteElement K
mk :
  ∀ (h : x ≤ y),
    HAdd.hAdd (α := FiniteResidueField K) (β := FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K) ≤
      HAdd.hAdd (α := FiniteResidueField K) (β := FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K)
mk₁ :
  ∀
    (h :
      Eq (α := FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)),
    HAdd.hAdd (α := FiniteResidueField K) (β := FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K) ≤
      HAdd.hAdd (α := FiniteResidueField K) (β := FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K)
⊢ HAdd.hAdd (α := FiniteResidueField K) (β := FiniteResidueField K)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K) ≤
    HAdd.hAdd (α := FiniteResidueField K) (β := FiniteResidueField K)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K)

Tactic:
obtain h | h := mk_le_mk.1 h

Premises used: ArchimedeanClass.FiniteResidueField.mk_le_mk, Iff.mp
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y_1 : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x y : FiniteElement K
h_1 :
  LE.le (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
z : FiniteElement K
h : x ≤ y
⊢ HAdd.hAdd (α := FiniteResidueField K) (β := FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K) ≤
    HAdd.hAdd (α := FiniteResidueField K) (β := FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K)

Tactic:
mk.monotone' <| add_le_add_left h _

Premises used: Submodule.Quotient.mk, Quotient.map₂, add_le_add_left, ArchimedeanClass.FiniteResidueField.mk, OrderRingHom.monotone'
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y_1 : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x y : FiniteElement K
h_1 :
  LE.le (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
z : FiniteElement K
h : x ≤ y
⊢ HAdd.hAdd (α := FiniteResidueField K) (β := FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K) ≤
    HAdd.hAdd (α := FiniteResidueField K) (β := FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K)

Tactic:
exact mk.monotone' <| add_le_add_left h _

Premises used: add_le_add_left, ArchimedeanClass.FiniteResidueField.mk, OrderRingHom.monotone'
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y_1 : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x y : FiniteElement K
h_1 :
  LE.le (α := FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
z : FiniteElement K
h :
  Eq (α := FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
mk mk₁ :
  HAdd.hAdd (α := FiniteResidueField K) (β := FiniteResidueField K)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K) ≤
    HAdd.hAdd (α := FiniteResidueField K) (β := FiniteResidueField K)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K)
⊢ HAdd.hAdd (α := FiniteResidueField K) (β := FiniteResidueField K)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K) ≤
    HAdd.hAdd (α := FiniteResidueField K) (β := FiniteResidueField K)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K)

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y_1 : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x : FiniteResidueField K
hx : 0 ≤ x
y z : FiniteResidueField K
h : y ≤ z
simp_rw : x * y ≤ x * z
⊢ y * x ≤ z * x

Tactic:
simp_rw [mul_comm _ x]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y_1 : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x : FiniteResidueField K
hx : 0 ≤ x
y z : FiniteResidueField K
h : y ≤ z
⊢ x * y ≤ x * z

Tactic:
mul_le_mul_of_nonneg_left' h hx

Premises used: _private.0.ArchimedeanClass.FiniteResidueField.mul_le_mul_of_nonneg_left'
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y_1 : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x : FiniteResidueField K
hx : 0 ≤ x
y z : FiniteResidueField K
h : y ≤ z
⊢ x * y ≤ x * z

Tactic:
exact mul_le_mul_of_nonneg_left' h hx

Premises used: _private.0.ArchimedeanClass.FiniteResidueField.mul_le_mul_of_nonneg_left'
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y_1 : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x y : FiniteResidueField K
hy : 0 < y
mk :
  ∀ (x : FiniteElement K), ∃ (n : ℕ), (FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x ≤ n • y
⊢ ∃ (n : ℕ), x ≤ n • y

Tactic:
induction x with | mk x

Premises used: ArchimedeanClass.FiniteResidueField.mk
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y_1 : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
y : FiniteResidueField K
hy : 0 < y
x : FiniteElement K
mk :
  ∀ (y : FiniteElement K)
    (hy :
      LT.lt (α := FiniteResidueField K) (0 : FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)),
    ∃ (n : ℕ),
      (FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x ≤
        HSMul.hSMul (β := FiniteResidueField K) n
          ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
⊢ ∃ (n : ℕ), (FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x ≤ n • y

Tactic:
induction y with | mk y

Premises used: ArchimedeanClass.FiniteResidueField.mk
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y_1 : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x y : FiniteElement K
hy :
  LT.lt (α := FiniteResidueField K) (0 : FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
mk :
  ∀
    (hx :
      LE.le (α := FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
        (0 : FiniteResidueField K)),
    ∃ (n : ℕ),
      (FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x ≤
        HSMul.hSMul (β := FiniteResidueField K) n
          ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
mk₁ :
  ∀
    (hx :
      LT.lt (α := FiniteResidueField K) (0 : FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)),
    ∃ (n : ℕ),
      (FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x ≤
        HSMul.hSMul (β := FiniteResidueField K) n
          ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
⊢ ∃ (n : ℕ),
    (FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x ≤
      HSMul.hSMul (β := FiniteResidueField K) n
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)

Tactic:
obtain hx | hx := le_or_gt (mk x) 0

Premises used: ArchimedeanClass.FiniteResidueField.mk, le_or_gt, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y_1 : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x y : FiniteElement K
hy :
  LT.lt (α := FiniteResidueField K) (0 : FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
hx :
  LE.le (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
    (0 : FiniteResidueField K)
h :
  (mk : (a : FiniteElement K) → FiniteResidueField K) x ≤
    HSMul.hSMul (α := ℕ) (β := FiniteResidueField K) 0
      ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
⊢ ∃ (n : ℕ),
    (mk : (a : FiniteElement K) → FiniteResidueField K) x ≤
      HSMul.hSMul (β := FiniteResidueField K) n
        ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)

Tactic:
use 0
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y_1 : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x y : FiniteElement K
hy :
  LT.lt (α := FiniteResidueField K) (0 : FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
hx :
  LE.le (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
    (0 : FiniteResidueField K)
h h₁ h₂ h₃ :
  LE.le (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
    (0 : FiniteResidueField K)
⊢ (mk : (a : FiniteElement K) → FiniteResidueField K) x ≤
    HSMul.hSMul (α := ℕ) (β := FiniteResidueField K) 0
      ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)

Tactic:
rwa [zero_nsmul]

Premises used: zero_nsmul
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y_1 : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x y : FiniteElement K
hy :
  LT.lt (α := FiniteResidueField K) (0 : FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
hx :
  LT.lt (α := FiniteResidueField K) (0 : FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
mk :
  ∀ (n : ℕ)
    (hn :
      |(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
            ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) (↑x : K) : ArchimedeanOrder K)| ≤
        HSMul.hSMul (β := K) n
          (|(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
                ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) (↑y : K) : ArchimedeanOrder K)| :
            K)),
    ∃ (n : ℕ),
      (FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x ≤
        HSMul.hSMul (β := FiniteResidueField K) n
          ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
⊢ ∃ (n : ℕ),
    (FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x ≤
      HSMul.hSMul (β := FiniteResidueField K) n
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)

Tactic:
obtain ⟨n, hn⟩ := ((mk_ne_zero.1 hy.ne').trans (mk_ne_zero.1 hx.ne').symm).le

Premises used: Eq.le, LT.lt.ne', ArchimedeanClass.FiniteResidueField.mk_ne_zero, Iff.mp, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y_1 : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x y : FiniteElement K
hy :
  LT.lt (α := FiniteResidueField K) (0 : FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
hx :
  LT.lt (α := FiniteResidueField K) (0 : FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
n : ℕ
hn :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
        ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) (↑x : K) : ArchimedeanOrder K)| ≤
    HSMul.hSMul (β := K) n
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
            ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) (↑y : K) : ArchimedeanOrder K)| :
        K)
⊢ ∃ (n : ℕ),
    (mk : (a : FiniteElement K) → FiniteResidueField K) x ≤
      HSMul.hSMul (β := FiniteResidueField K) n
        ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)

Tactic:
⟨n, mk.monotone' ?_⟩

Premises used: ArchimedeanClass.FiniteResidueField.mk, OrderRingHom.monotone', Exists.intro
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y_1 : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x y : FiniteElement K
hy :
  LT.lt (α := FiniteResidueField K) (0 : FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
hx :
  LT.lt (α := FiniteResidueField K) (0 : FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
n : ℕ
hn :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
        ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) (↑x : K) : ArchimedeanOrder K)| ≤
    HSMul.hSMul (β := K) n
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
            ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) (↑y : K) : ArchimedeanOrder K)| :
        K)
mk : x ≤ (fun (x : FiniteElement K) ↦ n • x) y
⊢ ∃ (n : ℕ),
    (FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x ≤
      HSMul.hSMul (β := FiniteResidueField K) n
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)

Tactic:
refine ⟨n, mk.monotone' ?_⟩
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y_1 : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x y : FiniteElement K
hy :
  LT.lt (α := FiniteResidueField K) (0 : FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
hx :
  LT.lt (α := FiniteResidueField K) (0 : FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
n : ℕ
hn :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
        ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) (↑x : K) : ArchimedeanOrder K)| ≤
    HSMul.hSMul (β := K) n
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
            ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) (↑y : K) : ArchimedeanOrder K)| :
        K)
mk : (↑x : K) ≤ n • (↑y : K)
⊢ x ≤ (fun (x : FiniteElement K) ↦ n • x) y

Tactic:
change x.1 ≤ n • y.1

Premises used: Subtype.val
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y_1 : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x y : FiniteElement K
hy :
  LT.lt (α := FiniteResidueField K) (0 : FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
hx :
  LT.lt (α := FiniteResidueField K) (0 : FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
n : ℕ
hn :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
        ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) (↑x : K) : ArchimedeanOrder K)| ≤
    HSMul.hSMul (β := K) n
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
            ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) (↑y : K) : ArchimedeanOrder K)| :
        K)
⊢ |(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
        ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) (↑x : K) : ArchimedeanOrder K)| ≤
    HSMul.hSMul (β := K) n
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
            ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) (↑y : K) : ArchimedeanOrder K)| :
        K)

Tactic:
hn
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y_1 : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x y : FiniteElement K
hy :
  LT.lt (α := FiniteResidueField K) (0 : FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
hx :
  LT.lt (α := FiniteResidueField K) (0 : FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
n : ℕ
hn :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
        ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) (↑x : K) : ArchimedeanOrder K)| ≤
    HSMul.hSMul (β := K) n
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
            ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) (↑y : K) : ArchimedeanOrder K)| :
        K)
h :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
        ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) (↑x : K) : ArchimedeanOrder K)| =
    (↑x : K)
h₁ :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
        ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) (↑y : K) : ArchimedeanOrder K)| =
    (↑y : K)
⊢ (↑x : K) ≤ n • (↑y : K)

Tactic:
convert! ← hn