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 :
  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)| =
    (↑x : K)

Tactic:
abs_of_pos <| lt_of_mk_lt_mk hx

Premises used: ArchimedeanClass.FiniteResidueField.lt_of_mk_lt_mk, abs_of_pos
-- 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)| =
    (↑x : K)

Tactic:
exact abs_of_pos <| lt_of_mk_lt_mk hx

Premises used: ArchimedeanClass.FiniteResidueField.lt_of_mk_lt_mk, abs_of_pos
-- 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) (↑y : K) : ArchimedeanOrder K)| =
    (↑y : K)

Tactic:
abs_of_pos <| lt_of_mk_lt_mk hy

Premises used: ArchimedeanClass.FiniteResidueField.lt_of_mk_lt_mk, abs_of_pos
-- 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) (↑y : K) : ArchimedeanOrder K)| =
    (↑y : K)

Tactic:
exact abs_of_pos <| lt_of_mk_lt_mk hy

Premises used: ArchimedeanClass.FiniteResidueField.lt_of_mk_lt_mk, abs_of_pos
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
q : ℚ
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) ⋯) :
          FiniteResidueField K)
        ((↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) : FiniteResidueField K) : FiniteResidueField K)
⊢ Eq.{u_1 + 1} (α := FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk (↑q : K) ⋯) : FiniteResidueField K)
    ((↑q : FiniteResidueField K) : FiniteResidueField K)

Tactic:
cases q with | div n d hd
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
div :
  (mk : (a : FiniteElement K) → FiniteResidueField K)
      (FiniteElement.mk (HMul.hMul (α := K) (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) : K) (↑d : K)) ⋯) =
    HMul.hMul (α := FiniteResidueField K) (β := FiniteResidueField K)
      ((↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) : FiniteResidueField K) : FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk (↑d : K) ⋯) : FiniteResidueField K)
⊢ 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)

Tactic:
rw [← mul_left_inj' (c := ↑d) (mod_cast hd), ← map_natCast mk d, ← map_mul,
    ← FiniteElement.mk_natCast, FiniteElement.mk_mul_mk]

Premises used: ArchimedeanClass.FiniteElement.mk_mul_mk, ArchimedeanClass.FiniteResidueField.mk, map_mul, map_natCast, mul_left_inj', ArchimedeanClass.FiniteElement.mk_natCast
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
⊢ (mk : (a : FiniteElement K) → FiniteResidueField K)
      (FiniteElement.mk (HMul.hMul (α := K) (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) : K) (↑d : K)) ⋯) =
    HMul.hMul (α := FiniteResidueField K) (β := FiniteResidueField K)
      ((↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) : FiniteResidueField K) : FiniteResidueField K)
      ((mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk (↑d : K) ⋯) : FiniteResidueField K)

Tactic:
simp_all
-- 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
f : R →+*o K
⊢ Eq.{u_1 + 1} (α := FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk ((f : (a : R) → K) 1) ⋯) :
      FiniteResidueField K)
    (1 : FiniteResidueField 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_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
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)) ⋯) =
    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)
⊢ (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)

Tactic:
simp_rw [map_mul]

Premises used: map_mul
-- 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
f : R →+*o K
x y : R
⊢ (mk : (a : FiniteElement K) → FiniteResidueField K)
      (FiniteElement.mk (HMul.hMul (α := K) (β := K) ((f : (a : R) → K) x : K) ((f : (a : R) → K) y : K)) ⋯) =
    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)

Tactic:
mk.map_mul
      (.mk _ (mk_map_nonneg_of_archimedean f x)) (.mk _ (mk_map_nonneg_of_archimedean f y))

Premises used: ArchimedeanClass.FiniteElement.mk, ArchimedeanClass.mk_map_nonneg_of_archimedean, ArchimedeanClass.FiniteResidueField.mk, RingHom.map_mul, OrderRingHom.toRingHom
-- 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
f : R →+*o K
x y : R
⊢ (mk : (a : FiniteElement K) → FiniteResidueField K)
      (FiniteElement.mk (HMul.hMul (α := K) (β := K) ((f : (a : R) → K) x : K) ((f : (a : R) → K) y : K)) ⋯) =
    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)

Tactic:
exact mk.map_mul
      (.mk _ (mk_map_nonneg_of_archimedean f x)) (.mk _ (mk_map_nonneg_of_archimedean f y))

Premises used: ArchimedeanClass.FiniteElement.mk, ArchimedeanClass.mk_map_nonneg_of_archimedean, ArchimedeanClass.FiniteResidueField.mk, RingHom.map_mul, OrderRingHom.toRingHom
-- 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
f : R →+*o K
⊢ Eq.{u_1 + 1} (α := FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk ((f : (a : R) → K) 0) ⋯) :
      FiniteResidueField K)
    (0 : FiniteResidueField 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_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
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)) ⋯) =
    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)
⊢ (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)

Tactic:
simp_rw [map_add]

Premises used: map_add
-- 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
f : R →+*o K
x y : R
⊢ (mk : (a : FiniteElement K) → FiniteResidueField K)
      (FiniteElement.mk (HAdd.hAdd (α := K) (β := K) ((f : (a : R) → K) x : K) ((f : (a : R) → K) y : K)) ⋯) =
    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)

Tactic:
mk.map_add
      (.mk _ (mk_map_nonneg_of_archimedean f x)) (.mk _ (mk_map_nonneg_of_archimedean f y))

Premises used: ArchimedeanClass.FiniteElement.mk, ArchimedeanClass.mk_map_nonneg_of_archimedean, ArchimedeanClass.FiniteResidueField.mk, RingHom.map_add, OrderRingHom.toRingHom
-- 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
f : R →+*o K
x y : R
⊢ (mk : (a : FiniteElement K) → FiniteResidueField K)
      (FiniteElement.mk (HAdd.hAdd (α := K) (β := K) ((f : (a : R) → K) x : K) ((f : (a : R) → K) y : K)) ⋯) =
    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)

Tactic:
exact mk.map_add
      (.mk _ (mk_map_nonneg_of_archimedean f x)) (.mk _ (mk_map_nonneg_of_archimedean f y))

Premises used: ArchimedeanClass.FiniteElement.mk, ArchimedeanClass.mk_map_nonneg_of_archimedean, ArchimedeanClass.FiniteResidueField.mk, RingHom.map_add, OrderRingHom.toRingHom
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
⊢ Eq.{u_1 + 1} (α := FiniteResidueField K)
    (((ofArchimedean f : OrderRingHom.{u_2, u_1} R (FiniteResidueField K)) : (a : R) → FiniteResidueField K) r :
      FiniteResidueField K)
    ((mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk ((f : (a : R) → K) r) ⋯) :
      FiniteResidueField K)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, rfl
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
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
⊢ Function.Injective.{u_2 + 1, u_1 + 1} (α := R) (β := FiniteResidueField K)
    (⇑(ofArchimedean f) : (a : R) → FiniteResidueField K)

Tactic:
rw [injective_iff_map_eq_zero]

Premises used: injective_iff_map_eq_zero
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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)
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)
⊢ r = 0

Tactic:
contrapose! hr
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
rw :
  Eq.{u_1 + 1} (α := ArchimedeanClass K)
    (ArchimedeanClass.mk (↑(FiniteElement.mk ((f : (a : R) → K) r) ⋯) : K) : ArchimedeanClass K)
    (0 : ArchimedeanClass K)
⊢ 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:
rw [ofArchimedean_apply, mk_ne_zero]

Premises used: ArchimedeanClass.FiniteResidueField.ofArchimedean_apply, ArchimedeanClass.FiniteResidueField.mk_ne_zero
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass K)
    (ArchimedeanClass.mk (↑(FiniteElement.mk ((f : (a : R) → K) r) ⋯) : K) : ArchimedeanClass K)
    (0 : ArchimedeanClass K)

Tactic:
mk_map_of_archimedean' f hr

Premises used: ArchimedeanClass.mk_map_of_archimedean'
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass K)
    (ArchimedeanClass.mk (↑(FiniteElement.mk ((f : (a : R) → K) r) ⋯) : K) : ArchimedeanClass K)
    (0 : ArchimedeanClass K)

Tactic:
exact mk_map_of_archimedean' f hr

Premises used: ArchimedeanClass.mk_map_of_archimedean'
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
x y : R
⊢ Eq.{u_1 + 1} (α := FiniteResidueField K)
      (((ofArchimedean f : OrderRingHom.{u_2, u_1} R (FiniteResidueField K)) : (a : R) → FiniteResidueField K) x :
        FiniteResidueField K)
      (((ofArchimedean f : OrderRingHom.{u_2, u_1} R (FiniteResidueField K)) : (a : R) → FiniteResidueField K) y :
        FiniteResidueField K) ↔
    x = y

Tactic:
(ofArchimedean_injective f).eq_iff

Premises used: Function.Injective.eq_iff, ArchimedeanClass.FiniteResidueField.ofArchimedean_injective
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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)
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) :
      ℝ)
⊢ stdPart x =
    (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]

Premises used: dif_pos, ArchimedeanClass.stdPart, OrderRingHom.comp_apply
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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)
e_a : Classical.ofNonempty = f
⊢ 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:
congr
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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)
⊢ Classical.ofNonempty = f

Tactic:
Subsingleton.allEq _ _

Premises used: Subsingleton.allEq
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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)
⊢ Classical.ofNonempty = f

Tactic:
exact Subsingleton.allEq _ _

Premises used: Subsingleton.allEq
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
contrapose! : Eq (α := ArchimedeanClass K) (mk x) 0 → stdPart x ≠ 0
⊢ stdPart x = 0 → Ne (α := ArchimedeanClass K) (mk x) 0

Tactic:
contrapose!
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
h : Eq (α := ArchimedeanClass K) (mk x) 0
rwa :
  Ne (α := ℝ)
    ((Classical.ofNonempty : (a : FiniteResidueField K) → ℝ)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x ⋯) :
          FiniteResidueField K) :
      ℝ)
    (0 : ℝ)
rwa₁ :
  Ne (α := FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x ⋯) :
      FiniteResidueField K)
    (0 : FiniteResidueField K)
rwa₂ rwa₃ rwa₄ rwa₅ : Eq (α := ArchimedeanClass K) (mk (↑(FiniteElement.mk x ⋯) : K)) 0
⊢ stdPart x ≠ 0

Tactic:
rwa [stdPart_of_mk_nonneg Classical.ofNonempty h.ge, map_ne_zero, FiniteResidueField.mk_ne_zero]

Premises used: Classical.ofNonempty, Eq.ge, ArchimedeanClass.FiniteResidueField.mk_ne_zero, map_ne_zero, ArchimedeanClass.stdPart_of_mk_nonneg
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
h : Ne (α := ArchimedeanClass K) (mk x) 0
inl : ∀ (h : LT.lt (α := ArchimedeanClass K) (mk x) 0), stdPart x = 0
inr : ∀ (h : LT.lt (α := ArchimedeanClass K) 0 (mk x)), stdPart x = 0
⊢ stdPart x = 0

Tactic:
obtain h | h := h.lt_or_gt

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
h_1 : Ne (α := ArchimedeanClass K) (mk x) 0
h : LT.lt (α := ArchimedeanClass K) (mk x) 0
⊢ stdPart x = 0

Tactic:
dif_neg h.not_ge

Premises used: dif_neg, ArchimedeanClass.stdPart, LT.lt.not_ge