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
x y : FiniteElement K
hy :
  Membership.mem (γ := Set (FiniteElement K))
    (Set.preimage (β :=
      Quotient (α := FiniteElement K) (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))))
      (Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)))) {⟦x⟧})
    y
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
⊢ x ≤ y

Tactic:
have := hxz.trans hzy
-- 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 :
  Membership.mem (γ := Set (FiniteElement K))
    (Set.preimage (β :=
      Quotient (α := FiniteElement K) (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))))
      (Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)))) {⟦x⟧})
    y
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
this : x ≤ y
rw :
  ∀ (hy : LT.lt (α := ArchimedeanClass K) 0 (mk (↑(y - x) : K))) ⦃z : FiniteElement K⦄ (hxz : x ≤ z) (hzy : z ≤ y)
    (this : x ≤ y), LT.lt (α := ArchimedeanClass K) 0 (mk (↑(z - x) : K))
⊢ Membership.mem (γ := Set (FiniteElement K))
    (Set.preimage (β :=
      Quotient (α := FiniteElement K) (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))))
      (Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)))) {⟦x⟧})
    z

Tactic:
rw [Set.mem_preimage, Set.mem_singleton_iff, Quotient.eq, Submodule.quotientRel_def,
    IsLocalRing.mem_maximalIdeal, mem_nonunits_iff, FiniteElement.not_isUnit_iff_mk_pos] at hy ⊢

Premises used: Submodule.quotientRel_def, mem_nonunits_iff, IsLocalRing.mem_maximalIdeal, ArchimedeanClass.FiniteElement.not_isUnit_iff_mk_pos, Set.mem_singleton_iff, Quotient.eq, Set.mem_preimage
-- 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 (α := ArchimedeanClass K) 0 (mk (↑(y - x) : K))
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
this : x ≤ y
apply : Membership.mem (γ := Set K) (Set.Ici 0) (↑(z - x) : K)
apply₁ : Membership.mem (γ := Set K) (Set.Ici 0) (↑(y - x) : K)
apply₂ : (↑(z - x) : K) ≤ (↑(y - x) : K)
⊢ LT.lt (α := ArchimedeanClass K) 0 (mk (↑(z - x) : K))

Tactic:
apply hy.trans_le (mk_antitoneOn _ _ _)

Premises used: LT.lt.trans_le, ArchimedeanClass.mk_antitoneOn
-- 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 (α := ArchimedeanClass K) 0 (mk (↑(y - x) : K))
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
this : x ≤ y
⊢ Membership.mem (γ := Set K) (Set.Ici 0) (↑(z - x) : K)

Tactic:
simpa
-- 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 (α := ArchimedeanClass K) 0 (mk (↑(y - x) : K))
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
this : x ≤ y
⊢ Membership.mem (γ := Set K) (Set.Ici 0) (↑(y - x) : K)

Tactic:
simpa
-- 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 (α := ArchimedeanClass K) 0 (mk (↑(y - x) : K))
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
this : x ≤ y
⊢ (↑(z - x) : K) ≤ (↑(y - x) : K)

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
motive : FiniteResidueField K → Prop
mk : ∀ (x : FiniteElement K), motive ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x)
⊢ ∀ (x : FiniteResidueField K), motive x

Tactic:
Quotient.ind mk

Premises used: Quotient.ind, ArchimedeanClass.FiniteResidueField, IsLocalRing.ResidueField
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
⊢ ∀ (x : FiniteResidueField K),
    Set.OrdConnected (α := FiniteElement K)
      (Set.preimage (β := FiniteResidueField K) (⇑mk : (a : FiniteElement K) → FiniteResidueField K) {x})

Tactic:
ordConnected_preimage_mk'

Premises used: Submodule.Quotient.mk, ArchimedeanClass.FiniteResidueField.ordConnected_preimage_mk', ArchimedeanClass.FiniteResidueField, IsLocalRing.ResidueField
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : FiniteElement K
apply :
  (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)) : FiniteElement K → FiniteElement K → Prop) x y ↔
    LT.lt (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk ((↑x : K) - (↑y : K)))
⊢ Eq (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K) ↔
    LT.lt (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk ((↑x : K) - (↑y : K)))

Tactic:
apply Quotient.eq.trans

Premises used: Iff.trans, Quotient.eq
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : FiniteElement K
rw :
  Membership.mem (γ := Submodule (FiniteElement K) (FiniteElement K)) (IsLocalRing.maximalIdeal (FiniteElement K))
      (x - y) ↔
    LT.lt (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk ((↑x : K) - (↑y : K)))
rw₁ :
  Membership.mem (γ := Set (FiniteElement K)) (nonunits (FiniteElement K)) (x - y) ↔
    LT.lt (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk ((↑x : K) - (↑y : K)))
rw₂ : ¬IsUnit (x - y) ↔ LT.lt (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk ((↑x : K) - (↑y : K)))
rw₃ :
  LT.lt (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk (↑(x - y) : K)) ↔
    LT.lt (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk ((↑x : K) - (↑y : K)))
rw₄ rw₅ :
  LT.lt (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk ((↑x : K) - (↑y : K))) ↔
    LT.lt (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk ((↑x : K) - (↑y : K)))
⊢ (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)) : FiniteElement K → FiniteElement K → Prop) x y ↔
    LT.lt (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk ((↑x : K) - (↑y : K)))

Tactic:
rw [Submodule.quotientRel_def, IsLocalRing.mem_maximalIdeal, mem_nonunits_iff,
    FiniteElement.not_isUnit_iff_mk_pos, AddSubgroupClass.coe_sub]

Premises used: Submodule.quotientRel_def, AddSubgroupClass.coe_sub, mem_nonunits_iff, IsLocalRing.mem_maximalIdeal, ArchimedeanClass.FiniteElement.not_isUnit_iff_mk_pos
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : FiniteElement K
apply :
  LT.lt (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk ((↑x : K) - (↑0 : K))) ↔
    LT.lt (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk (↑x : K))
⊢ Eq (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
      (0 : FiniteResidueField K) ↔
    LT.lt (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk (↑x : K))

Tactic:
apply mk_eq_mk.trans

Premises used: ArchimedeanClass.FiniteResidueField.mk_eq_mk, Iff.trans
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : FiniteElement K
⊢ LT.lt (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk ((↑x : K) - (↑0 : K))) ↔
    LT.lt (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk (↑x : K))

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : FiniteElement K
rw :
  ¬Eq (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
        (0 : FiniteResidueField K) ↔
    Eq (α := ArchimedeanClass K) (ArchimedeanClass.mk (↑x : K)) 0
rw₁ :
  ¬LT.lt (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk (↑x : K)) ↔
    Eq (α := ArchimedeanClass K) (ArchimedeanClass.mk (↑x : K)) 0
rw₂ :
  LE.le (α := ArchimedeanClass K) (ArchimedeanClass.mk (↑x : K)) 0 ↔
    Eq (α := ArchimedeanClass K) (ArchimedeanClass.mk (↑x : K)) 0
rw₃ rw₄ :
  Eq (α := ArchimedeanClass K) (ArchimedeanClass.mk (↑x : K)) 0 ↔
    Eq (α := ArchimedeanClass K) (ArchimedeanClass.mk (↑x : K)) 0
⊢ Ne (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
      (0 : FiniteResidueField K) ↔
    Eq (α := ArchimedeanClass K) (ArchimedeanClass.mk (↑x : K)) 0

Tactic:
rw [ne_eq, mk_eq_zero, not_lt, x.2.ge_iff_eq']

Premises used: ArchimedeanClass.FiniteResidueField.mk_eq_zero, ne_eq, LE.le.ge_iff_eq', not_lt
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : FiniteElement K
⊢ LE.le (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K) ↔
    x ≤ y ∨
      Eq (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
        ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)

Tactic:
(Quotient.mk_le_mk (H := ordConnected_preimage_mk')).trans ?_

Premises used: Set.Mem, Iff.trans, Quotient.mk_le_mk
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : FiniteElement K
refine :
  x ≤ y ∨ x ≈ y ↔
    x ≤ y ∨
      Eq (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
        ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
⊢ LE.le (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K) ↔
    x ≤ y ∨
      Eq (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
        ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)

Tactic:
refine (Quotient.mk_le_mk (H := ordConnected_preimage_mk')).trans ?_

Premises used: Iff.trans, Quotient.mk_le_mk
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : FiniteElement K
rw :
  x ≤ y ∨
      Eq (α := Quotient (α := FiniteElement K) (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)))) ⟦x⟧
        ⟦y⟧ ↔
    x ≤ y ∨
      Eq (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
        ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
⊢ x ≤ y ∨ x ≈ y ↔
    x ≤ y ∨
      Eq (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
        ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)

Tactic:
rw [← Quotient.eq_iff_equiv]

Premises used: Quotient.eq_iff_equiv
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : FiniteElement K
⊢ x ≤ y ∨
      Eq (α := Quotient (α := FiniteElement K) (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)))) ⟦x⟧
        ⟦y⟧ ↔
    x ≤ y ∨
      Eq (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
        ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : FiniteElement K
⊢ LT.lt (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K) ↔
    x < y ∧
      Ne (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
        ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)

Tactic:
(Quotient.mk_lt_mk (H := ordConnected_preimage_mk')).trans ?_

Premises used: Set.Mem, Quotient.mk_lt_mk, Iff.trans
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : FiniteElement K
refine :
  x < y ∧ ¬x ≈ y ↔
    x < y ∧
      Ne (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
        ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
⊢ LT.lt (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K) ↔
    x < y ∧
      Ne (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
        ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)

Tactic:
refine (Quotient.mk_lt_mk (H := ordConnected_preimage_mk')).trans ?_

Premises used: Quotient.mk_lt_mk, Iff.trans
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : FiniteElement K
rw :
  x < y ∧
      ¬Eq (α := Quotient (α := FiniteElement K) (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))))
          ⟦x⟧ ⟦y⟧ ↔
    x < y ∧
      Ne (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
        ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
⊢ x < y ∧ ¬x ≈ y ↔
    x < y ∧
      Ne (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
        ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)

Tactic:
rw [← Quotient.eq_iff_equiv]

Premises used: Quotient.eq_iff_equiv
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : FiniteElement K
⊢ x < y ∧
      ¬Eq (α := Quotient (α := FiniteElement K) (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))))
          ⟦x⟧ ⟦y⟧ ↔
    x < y ∧
      Ne (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
        ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : FiniteElement K
h :
  LT.lt (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
⊢ x < y

Tactic:
(mk_lt_mk.1 h).1

Premises used: And.left, Iff.mp, ArchimedeanClass.FiniteResidueField.mk_lt_mk
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y z : FiniteResidueField K
h : x ≤ y
hz : 0 ≤ z
mk :
  ∀ (x : FiniteElement K) (h : (FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x ≤ y),
    HMul.hMul (β := FiniteResidueField K) z
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K) ≤
      z * y
⊢ z * x ≤ z * 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
y z : FiniteResidueField K
hz : 0 ≤ z
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)),
    HMul.hMul (β := FiniteResidueField K) z
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K) ≤
      HMul.hMul (β := FiniteResidueField K) z
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
⊢ HMul.hMul (β := FiniteResidueField K) z
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K) ≤
    z * 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
z : FiniteResidueField K
hz : 0 ≤ z
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)
    (hz :
      LE.le (α := FiniteResidueField K) (0 : FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K)),
    HMul.hMul (α := FiniteResidueField K) (β := FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K) ≤
      HMul.hMul (α := FiniteResidueField K) (β := FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
⊢ HMul.hMul (β := FiniteResidueField K) z
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K) ≤
    HMul.hMul (β := FiniteResidueField K) z
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)

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 y : FiniteElement K
h :
  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
hz :
  LE.le (α := FiniteResidueField K) (0 : FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K)
⊢ LE.le (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) 0 : FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K)

Tactic:
rw [← map_zero mk] at hz

Premises used: map_zero, 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 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
hz :
  LE.le (α := FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) 0 : FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K)
mk :
  ∀
    (h :
      x ≤ y ∨
        Eq (α := 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)
    (hz :
      0 ≤ z ∨
        Eq (α := FiniteResidueField K)
          ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) 0 : FiniteResidueField K)
          ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K)),
    z * x ≤ z * y ∨
      Eq (α := FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (z * x) : FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (z * y) : FiniteResidueField K)
⊢ LE.le (α := FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (z * x) : FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (z * y) : FiniteResidueField K)

Tactic:
rw [mk_le_mk] at h hz ⊢

Premises used: ArchimedeanClass.FiniteResidueField.mk_le_mk
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : FiniteElement K
h :
  x ≤ y ∨
    Eq (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
z : FiniteElement K
hz :
  0 ≤ z ∨
    Eq (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) 0 : FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K)
⊢ z * x ≤ z * y ∨
    Eq (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) (z * x) : FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K) (z * y) : FiniteResidueField K)

Tactic:
grind [mul_le_mul_of_nonneg_left]

Premises used: 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
h : x ≤ y
z : FiniteResidueField K
mk :
  ∀ (x : FiniteElement K) (h : (FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x ≤ y),
    HAdd.hAdd (α := FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K) z ≤
      y + z
⊢ x + z ≤ y + z

Tactic:
induction x with | mk x

Premises used: ArchimedeanClass.FiniteResidueField.mk