awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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)
⊢ LT.lt (α := ArchimedeanClass K) 0 (mk (↑(z - x) : K))
have apply₂ : (↑(z - x) : K) ≤ (↑(y - x) : K)
Tactic: apply hy.trans_le (mk_antitoneOn _ _ _)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : FiniteElement 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)))
have 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)))
Tactic: apply Quotient.eq.trans
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : FiniteElement 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)))
have 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)))
Tactic: rw [Submodule.quotientRel_def, IsLocalRing.mem_maximalIdeal, mem_nonunits_iff,
    FiniteElement.not_isUnit_iff_mk_pos, AddSubgroupClass.coe_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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)))
⊢ (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)) : FiniteElement K → FiniteElement K → Prop) x y ↔
    LT.lt (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk ((↑x : K) - (↑y : K)))
have rw₁ : Membership.mem (γ := Set (FiniteElement K)) (nonunits (FiniteElement K)) (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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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)))
⊢ (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)) : FiniteElement K → FiniteElement K → Prop) x y ↔
    LT.lt (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk ((↑x : K) - (↑y : K)))
have rw₂ : ¬IsUnit (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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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)))
⊢ (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)) : FiniteElement K → FiniteElement K → Prop) x y ↔
    LT.lt (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk ((↑x : K) - (↑y : K)))
have rw₃ : LT.lt (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk (↑(x - y) : K)) ↔
  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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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)))
⊢ (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)) : FiniteElement K → FiniteElement K → Prop) x y ↔
    LT.lt (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk ((↑x : K) - (↑y : K)))
have rw₄ : LT.lt (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk ((↑x : K) - (↑y : K))) ↔
  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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : FiniteElement 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))
have apply : LT.lt (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk ((↑x : K) - (↑0 : K))) ↔
  LT.lt (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk (↑x : K))
Tactic: apply mk_eq_mk.trans
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : FiniteElement K
⊢ Ne (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
      (0 : FiniteResidueField K) ↔
    Eq (α := ArchimedeanClass K) (ArchimedeanClass.mk (↑x : K)) 0
have rw : ¬Eq (α := 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']
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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
⊢ Ne (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
      (0 : FiniteResidueField K) ↔
    Eq (α := ArchimedeanClass K) (ArchimedeanClass.mk (↑x : K)) 0
have rw₁ : ¬LT.lt (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk (↑x : K)) ↔
  Eq (α := ArchimedeanClass K) (ArchimedeanClass.mk (↑x : K)) 0
Tactic: rw [ne_eq, mk_eq_zero, not_lt, x.2.ge_iff_eq']
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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
⊢ Ne (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
      (0 : FiniteResidueField K) ↔
    Eq (α := ArchimedeanClass K) (ArchimedeanClass.mk (↑x : K)) 0
have rw₂ : LE.le (α := ArchimedeanClass K) (ArchimedeanClass.mk (↑x : K)) 0 ↔
  Eq (α := ArchimedeanClass K) (ArchimedeanClass.mk (↑x : K)) 0
Tactic: rw [ne_eq, mk_eq_zero, not_lt, x.2.ge_iff_eq']
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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
⊢ Ne (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
      (0 : FiniteResidueField K) ↔
    Eq (α := ArchimedeanClass K) (ArchimedeanClass.mk (↑x : K)) 0
have rw₃ : Eq (α := ArchimedeanClass K) (ArchimedeanClass.mk (↑x : K)) 0 ↔
  Eq (α := ArchimedeanClass K) (ArchimedeanClass.mk (↑x : K)) 0
Tactic: rw [ne_eq, mk_eq_zero, not_lt, x.2.ge_iff_eq']
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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)
have 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)
Tactic: refine (Quotient.mk_le_mk (H := ordConnected_preimage_mk')).trans ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : FiniteElement 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)
have 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)
Tactic: rw [← Quotient.eq_iff_equiv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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)
have 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)
Tactic: refine (Quotient.mk_lt_mk (H := ordConnected_preimage_mk')).trans ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : FiniteElement 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)
have 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)
Tactic: rw [← Quotient.eq_iff_equiv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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
⊢ z * x ≤ z * y
have mk : ∀ (x : FiniteElement K) (h : (mk : (a : FiniteElement K) → FiniteResidueField K) x ≤ y),
  HMul.hMul (β := FiniteResidueField K) z
      ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K) ≤
    z * y
Tactic: induction x with | mk x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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 : (mk : (a : FiniteElement K) → FiniteResidueField K) x ≤ y
⊢ HMul.hMul (β := FiniteResidueField K) z
      ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K) ≤
    z * y
have mk : ∀ (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)),
  HMul.hMul (β := FiniteResidueField K) z
      ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K) ≤
    HMul.hMul (β := FiniteResidueField K) z
      ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
Tactic: induction y with | mk y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
⊢ HMul.hMul (β := FiniteResidueField K) z
      ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K) ≤
    HMul.hMul (β := FiniteResidueField K) z
      ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
have mk : ∀ (z : FiniteElement K)
  (hz :
    LE.le (α := FiniteResidueField K) (0 : FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K)),
  HMul.hMul (α := FiniteResidueField K) (β := FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K) ≤
    HMul.hMul (α := FiniteResidueField K) (β := FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
Tactic: induction z with | mk z
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (hypothesis)
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) (z * x) : FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) (z * y) : FiniteResidueField K)
have hz₁ : 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
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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) ((mk : (a : FiniteElement K) → FiniteResidueField K) 0 : FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) z : FiniteResidueField K)
⊢ LE.le (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) (z * x) : FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) (z * y) : FiniteResidueField K)
have mk : ∀
  (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: rw [mk_le_mk] at h hz ⊢
Cleared hypotheses: h, z, hz
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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
⊢ x + z ≤ y + z
have mk : ∀ (x : FiniteElement K) (h : (mk : (a : FiniteElement K) → FiniteResidueField K) x ≤ y),
  HAdd.hAdd (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
      z ≤
    y + z
Tactic: induction x with | mk x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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 : (mk : (a : FiniteElement K) → FiniteResidueField K) x ≤ y
⊢ HAdd.hAdd (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
      z ≤
    y + z
have mk : ∀ (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)),
  HAdd.hAdd (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
      z ≤
    HAdd.hAdd (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
      z
Tactic: induction y with | mk y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
⊢ HAdd.hAdd (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
      z ≤
    HAdd.hAdd (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
      z
have mk : ∀ (z : FiniteElement K),
  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: induction z with | mk z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
z : FiniteElement K
⊢ 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)
have mk : ∀ (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: obtain h | h := mk_le_mk.1 h