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
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)
⊢ 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)
have 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)
Tactic: obtain h | h := mk_le_mk.1 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
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 :
  Eq (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField 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 : HAdd.hAdd (α := FiniteResidueField K) (β := FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) y : 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: rw [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
x : FiniteResidueField K
hx : 0 ≤ x
y z : FiniteResidueField K
h : y ≤ z
⊢ y * x ≤ z * x
have simp_rw : x * y ≤ x * z
Tactic: simp_rw [mul_comm _ x]
-- 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
hy : 0 < y
⊢ ∃ (n : ℕ), x ≤ n • y
have mk : ∀ (x : FiniteElement K), ∃ (n : ℕ), (mk : (a : FiniteElement K) → FiniteResidueField K) x ≤ n • y
Tactic: induction x with | mk x
Cleared hypotheses: x
-- 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 : FiniteResidueField K
hy : 0 < y
x : FiniteElement K
⊢ ∃ (n : ℕ), (mk : (a : FiniteElement K) → FiniteResidueField K) x ≤ n • y
have mk : ∀ (y : FiniteElement K)
  (hy :
    LT.lt (α := FiniteResidueField K) (0 : FiniteResidueField K)
      ((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: induction y with | mk y
Cleared hypotheses: y, hy
-- 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 (α := FiniteResidueField K) (0 : FiniteResidueField K)
    ((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)
have mk : ∀
  (hx :
    LE.le (α := FiniteResidueField K) ((mk : (a : FiniteElement K) → FiniteResidueField K) x : FiniteResidueField K)
      (0 : 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: obtain hx | hx := le_or_gt (mk x) 0
-- 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 (α := 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)
⊢ ∃ (n : ℕ),
    (FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) x ≤
      HSMul.hSMul (β := FiniteResidueField K) n
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
have 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)
Tactic: obtain hx | hx := le_or_gt (mk x) 0
-- 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 (α := 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)
⊢ ∃ (n : ℕ),
    (mk : (a : FiniteElement K) → FiniteResidueField K) x ≤
      HSMul.hSMul (β := FiniteResidueField K) n
        ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
have h : (mk : (a : FiniteElement K) → FiniteResidueField K) x ≤
  HSMul.hSMul (α := ℕ) (β := FiniteResidueField K) 0
    ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
Tactic: use 0
-- 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 (α := 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 : ℕ),
    (mk : (a : FiniteElement K) → FiniteResidueField K) x ≤
      HSMul.hSMul (β := FiniteResidueField K) n
        ((mk : (a : FiniteElement K) → FiniteResidueField K) y : FiniteResidueField K)
have 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 : ℕ),
    (mk : (a : FiniteElement K) → FiniteResidueField K) x ≤
      HSMul.hSMul (β := FiniteResidueField K) n
        ((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
-- 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 (α := 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)
have mk : x ≤ (fun (x : FiniteElement K) ↦ n • x) y
Tactic: refine ⟨n, mk.monotone' ?_⟩
-- 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 (α := 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)
⊢ x ≤ (fun (x : FiniteElement K) ↦ n • x) y
have mk : (↑x : K) ≤ n • (↑y : K)
Tactic: change x.1 ≤ n • y.1
-- 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 (α := 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)
⊢ (↑x : K) ≤ n • (↑y : K)
have h : |(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
      ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) (↑x : K) : ArchimedeanOrder K)| =
  (↑x : K)
Tactic: convert! ← hn
-- 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 (α := 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)
⊢ (↑x : K) ≤ n • (↑y : K)
have h₁ : |(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
      ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) (↑y : K) : ArchimedeanOrder K)| =
  (↑y : K)
Tactic: convert! ← hn
-- 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
q : ℚ
⊢ Eq.{u_1 + 1} (α := FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk (↑q : K) ⋯) : FiniteResidueField K)
    ((↑q : FiniteResidueField K) : FiniteResidueField K)
have div : ∀ (n : ℤ) (d : ℕ) (hd : d ≠ 0),
  n.natAbs.Coprime d →
    Eq.{u_1 + 1} (α := FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K)
          (FiniteElement.mk (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) : K) sorry) :
        FiniteResidueField K)
      ((↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) : FiniteResidueField K) : FiniteResidueField K)
Tactic: cases q with | div n d hd
Cleared hypotheses: q
-- 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
n : ℤ
d : ℕ
hd : d ≠ 0
h : n.natAbs.Coprime d
⊢ Eq.{u_1 + 1} (α := FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K)
        (FiniteElement.mk (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) : K) ⋯) :
      FiniteResidueField K)
    ((↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) : FiniteResidueField K) : FiniteResidueField K)
have div : (mk : (a : FiniteElement K) → FiniteResidueField K)
    (FiniteElement.mk (HMul.hMul (α := K) (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) : K) (↑d : K)) sorry) =
  HMul.hMul (α := FiniteResidueField K) (β := FiniteResidueField K)
    ((↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) : FiniteResidueField K) : FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk (↑d : K) sorry) : FiniteResidueField K)
Tactic: rw [← mul_left_inj' (c := ↑d) (mod_cast hd), ← map_natCast mk d, ← map_mul,
    ← FiniteElement.mk_natCast, FiniteElement.mk_mul_mk]
-- 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
f : R →+*o K
x y : R
⊢ (mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk ((f : (a : R) → K) (x * y)) ⋯) =
    HMul.hMul (α := FiniteResidueField K) (β := FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk ((f : (a : R) → K) x) ⋯) :
        FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk ((f : (a : R) → K) y) ⋯) :
        FiniteResidueField K)
have simp_rw : (mk : (a : FiniteElement K) → FiniteResidueField K)
    (FiniteElement.mk (HMul.hMul (α := K) (β := K) ((f : (a : R) → K) x : K) ((f : (a : R) → K) y : K)) sorry) =
  HMul.hMul (α := FiniteResidueField K) (β := FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk ((f : (a : R) → K) x) sorry) :
      FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk ((f : (a : R) → K) y) sorry) :
      FiniteResidueField K)
Tactic: simp_rw [map_mul]
-- 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
f : R →+*o K
x y : R
⊢ (mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk ((f : (a : R) → K) (x + y)) ⋯) =
    HAdd.hAdd (α := FiniteResidueField K) (β := FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk ((f : (a : R) → K) x) ⋯) :
        FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk ((f : (a : R) → K) y) ⋯) :
        FiniteResidueField K)
have simp_rw : (mk : (a : FiniteElement K) → FiniteResidueField K)
    (FiniteElement.mk (HAdd.hAdd (α := K) (β := K) ((f : (a : R) → K) x : K) ((f : (a : R) → K) y : K)) sorry) =
  HAdd.hAdd (α := FiniteResidueField K) (β := FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk ((f : (a : R) → K) x) sorry) :
      FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk ((f : (a : R) → K) y) sorry) :
      FiniteResidueField K)
Tactic: simp_rw [map_add]
-- 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
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
f : R →+*o K
⊢ Function.Injective.{u_2 + 1, u_1 + 1} (α := R) (β := FiniteResidueField K)
    (⇑(ofArchimedean f) : (a : R) → FiniteResidueField K)
have rw : ∀ (a : R),
  Eq.{u_1 + 1} (α := FiniteResidueField K)
      (((ofArchimedean f : OrderRingHom.{u_2, u_1} R (FiniteResidueField K)) : (a : R) → FiniteResidueField K) a :
        FiniteResidueField K)
      (0 : FiniteResidueField K) →
    a = 0
Tactic: rw [injective_iff_map_eq_zero]
-- 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
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
f : R →+*o K
r : R
hr :
  Eq.{u_1 + 1} (α := FiniteResidueField K)
    (((ofArchimedean f : OrderRingHom.{u_2, u_1} R (FiniteResidueField K)) : (a : R) → FiniteResidueField K) r :
      FiniteResidueField K)
    (0 : FiniteResidueField K)
⊢ r = 0
have contrapose! : ∀ (hr : r ≠ 0),
  Ne.{u_1 + 1} (α := FiniteResidueField K)
    (((ofArchimedean f : OrderRingHom.{u_2, u_1} R (FiniteResidueField K)) : (a : R) → FiniteResidueField K) r :
      FiniteResidueField K)
    (0 : FiniteResidueField K)
Tactic: contrapose! hr
Cleared hypotheses: hr
-- 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
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
f : R →+*o K
r : R
hr : r ≠ 0
⊢ Ne.{u_1 + 1} (α := FiniteResidueField K)
    (((ofArchimedean f : OrderRingHom.{u_2, u_1} R (FiniteResidueField K)) : (a : R) → FiniteResidueField K) r :
      FiniteResidueField K)
    (0 : FiniteResidueField K)
have rw : Eq.{u_1 + 1} (α := ArchimedeanClass K)
  (ArchimedeanClass.mk (↑(FiniteElement.mk ((f : (a : R) → K) r) sorry) : K) : ArchimedeanClass K) (0 : ArchimedeanClass K)
Tactic: rw [ofArchimedean_apply, mk_ne_zero]
-- 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 : K
f : FiniteResidueField K →+*o ℝ
h : LE.le (α := ArchimedeanClass K) 0 (mk x)
⊢ stdPart x =
    (f : (a : FiniteResidueField K) → ℝ)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x h) :
        FiniteResidueField K)
have rw : Eq (α := ℝ)
  ((Classical.ofNonempty : (a : FiniteResidueField K) → ℝ)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x h) :
        FiniteResidueField K) :
    ℝ)
  ((f : (a : FiniteResidueField K) → ℝ)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x h) :
        FiniteResidueField K) :
    ℝ)
Tactic: rw [stdPart, dif_pos h, OrderRingHom.comp_apply]