awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : IsStrictOrderedRing R
x y : ArchimedeanClass R
mk : ∀ (x : R), ArchimedeanClass.mk x + y = y + ArchimedeanClass.mk x
⊢ x + y = y + x

Tactic:
induction x with | mk x

Premises used: ArchimedeanClass.mk
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : IsStrictOrderedRing R
y : ArchimedeanClass R
x : R
mk :
  ∀ (y : R),
    HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk x) (ArchimedeanClass.mk y) =
      HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk y) (ArchimedeanClass.mk x)
⊢ ArchimedeanClass.mk x + y = y + ArchimedeanClass.mk x

Tactic:
induction y with | mk y

Premises used: ArchimedeanClass.mk
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : IsStrictOrderedRing R
x y : R
mk : ArchimedeanClass.mk (x * y) = HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk y) (ArchimedeanClass.mk x)
mk₁ : ArchimedeanClass.mk (y * x) = HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk y) (ArchimedeanClass.mk x)
mk₂ mk₃ :
  HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk y) (ArchimedeanClass.mk x) =
    HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk y) (ArchimedeanClass.mk x)
⊢ HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk x) (ArchimedeanClass.mk y) =
    HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk y) (ArchimedeanClass.mk x)

Tactic:
rw [← mk_mul, mul_comm, mk_mul]

Premises used: ArchimedeanClass.mk_mul, mul_comm
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : ArchimedeanClass R
mk : ∀ (x : R), HAdd.hAdd (α := ArchimedeanClass R) 0 (ArchimedeanClass.mk x) = ArchimedeanClass.mk x
⊢ 0 + x = x

Tactic:
induction x with | mk x

Premises used: ArchimedeanClass.mk
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
mk : HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk 1) (ArchimedeanClass.mk x) = ArchimedeanClass.mk x
mk₁ : Eq (α := ArchimedeanClass R) (ArchimedeanClass.mk (1 * x)) (ArchimedeanClass.mk x)
mk₂ mk₃ : Eq (α := ArchimedeanClass R) (ArchimedeanClass.mk x) (ArchimedeanClass.mk x)
⊢ HAdd.hAdd (α := ArchimedeanClass R) 0 (ArchimedeanClass.mk x) = ArchimedeanClass.mk x

Tactic:
rw [← mk_one, ← mk_mul, one_mul]

Premises used: ArchimedeanClass.mk_mul, ArchimedeanClass.mk_one, one_mul
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x y z : ArchimedeanClass R
mk : ∀ (x : R), ArchimedeanClass.mk x + y + z = ArchimedeanClass.mk x + (y + z)
⊢ x + y + z = x + (y + z)

Tactic:
induction x with | mk x

Premises used: ArchimedeanClass.mk
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
y z : ArchimedeanClass R
x : R
mk :
  ∀ (y : R),
    HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk x) (ArchimedeanClass.mk y) + z =
      ArchimedeanClass.mk x + (ArchimedeanClass.mk y + z)
⊢ ArchimedeanClass.mk x + y + z = ArchimedeanClass.mk x + (y + z)

Tactic:
induction y with | mk y

Premises used: ArchimedeanClass.mk
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
z : ArchimedeanClass R
x y : R
mk :
  ∀ (z : R),
    HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk x) (ArchimedeanClass.mk y) + ArchimedeanClass.mk z =
      ArchimedeanClass.mk x + HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk y) (ArchimedeanClass.mk z)
⊢ HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk x) (ArchimedeanClass.mk y) + z =
    ArchimedeanClass.mk x + (ArchimedeanClass.mk y + z)

Tactic:
induction z with | mk z

Premises used: ArchimedeanClass.mk
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x y z : R
mk : Eq (α := ArchimedeanClass R) (ArchimedeanClass.mk (x * y * z)) (ArchimedeanClass.mk (x * (y * z)))
⊢ HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk x) (ArchimedeanClass.mk y) + ArchimedeanClass.mk z =
    ArchimedeanClass.mk x + HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk y) (ArchimedeanClass.mk z)

Tactic:
simp_rw [← mk_mul, mul_assoc]

Premises used: mul_assoc, ArchimedeanClass.mk_mul
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : IsStrictOrderedRing R
x : R
mk : Eq (α := ArchimedeanClass R) (ArchimedeanClass.mk (HPow.hPow (β := ℕ) x 0)) 0
mk₁ : Eq.{u_1 + 1} (α := ArchimedeanClass R) (ArchimedeanClass.mk 1) 0
mk₂ mk₃ : Eq.{u_1 + 1} (α := ArchimedeanClass R) 0 0
⊢ HSMul.hSMul (α := ℕ) (β := ArchimedeanClass R) 0 (ArchimedeanClass.mk x) = 0

Tactic:
rw [← mk_pow, pow_zero, mk_one]

Premises used: ArchimedeanClass.mk_pow, pow_zero, ArchimedeanClass.mk_one
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : IsStrictOrderedRing R
x : ArchimedeanClass R
mk : ∀ (x : R), HSMul.hSMul (α := ℕ) (β := ArchimedeanClass R) 0 (ArchimedeanClass.mk x) = 0
⊢ HSMul.hSMul (α := ℕ) 0 x = 0

Tactic:
induction x with | mk x => rw [← mk_pow, pow_zero, mk_one]

Premises used: ArchimedeanClass.mk_pow, pow_zero, ArchimedeanClass.mk_one, ArchimedeanClass.mk
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : IsStrictOrderedRing R
n : ℕ
x : R
mk :
  ArchimedeanClass.mk (x ^ (n + 1)) =
    HSMul.hSMul (β := ArchimedeanClass R) n (ArchimedeanClass.mk x) + ArchimedeanClass.mk x
mk₁ :
  ArchimedeanClass.mk (x ^ n * x) =
    HSMul.hSMul (β := ArchimedeanClass R) n (ArchimedeanClass.mk x) + ArchimedeanClass.mk x
mk₂ :
  HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk (x ^ n)) (ArchimedeanClass.mk x) =
    HSMul.hSMul (β := ArchimedeanClass R) n (ArchimedeanClass.mk x) + ArchimedeanClass.mk x
mk₃ mk₄ :
  HSMul.hSMul (β := ArchimedeanClass R) n (ArchimedeanClass.mk x) + ArchimedeanClass.mk x =
    HSMul.hSMul (β := ArchimedeanClass R) n (ArchimedeanClass.mk x) + ArchimedeanClass.mk x
⊢ HSMul.hSMul (β := ArchimedeanClass R) (n + 1) (ArchimedeanClass.mk x) =
    HSMul.hSMul (β := ArchimedeanClass R) n (ArchimedeanClass.mk x) + ArchimedeanClass.mk x

Tactic:
rw [← mk_pow, pow_succ, mk_mul, mk_pow]

Premises used: ArchimedeanClass.mk_pow, pow_succ, ArchimedeanClass.mk_mul
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : IsStrictOrderedRing R
n : ℕ
x : ArchimedeanClass R
mk :
  ∀ (x : R),
    HSMul.hSMul (β := ArchimedeanClass R) (n + 1) (ArchimedeanClass.mk x) =
      HSMul.hSMul (β := ArchimedeanClass R) n (ArchimedeanClass.mk x) + ArchimedeanClass.mk x
⊢ (n + 1) • x = n • x + x

Tactic:
induction x with | mk x => rw [← mk_pow, pow_succ, mk_mul, mk_pow]

Premises used: ArchimedeanClass.mk_pow, pow_succ, ArchimedeanClass.mk_mul, ArchimedeanClass.mk
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : IsStrictOrderedRing R
x y : ArchimedeanClass R
h : x ≤ y
z : ArchimedeanClass R
mk : ∀ (x : R) (h : ArchimedeanClass.mk x ≤ y), ArchimedeanClass.mk x + z ≤ y + z
⊢ x + z ≤ y + z

Tactic:
induction x with | mk x

Premises used: ArchimedeanClass.mk
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : IsStrictOrderedRing R
y z : ArchimedeanClass R
x : R
h : ArchimedeanClass.mk x ≤ y
mk :
  ∀ (y : R) (h : LE.le (α := ArchimedeanClass R) (ArchimedeanClass.mk x) (ArchimedeanClass.mk y)),
    ArchimedeanClass.mk x + z ≤ ArchimedeanClass.mk y + z
⊢ ArchimedeanClass.mk x + z ≤ y + z

Tactic:
induction y with | mk y

Premises used: ArchimedeanClass.mk
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : IsStrictOrderedRing R
z : ArchimedeanClass R
x y : R
h : LE.le (α := ArchimedeanClass R) (ArchimedeanClass.mk x) (ArchimedeanClass.mk y)
mk :
  ∀ (z : R),
    HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk x) (ArchimedeanClass.mk z) ≤
      HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk y) (ArchimedeanClass.mk z)
⊢ ArchimedeanClass.mk x + z ≤ ArchimedeanClass.mk y + z

Tactic:
induction z with | mk z

Premises used: ArchimedeanClass.mk
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : IsStrictOrderedRing R
x y : R
h : LE.le (α := ArchimedeanClass R) (ArchimedeanClass.mk x) (ArchimedeanClass.mk y)
z : R
mk : LE.le (α := ArchimedeanClass R) (ArchimedeanClass.mk (x * z)) (ArchimedeanClass.mk (y * z))
⊢ HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk x) (ArchimedeanClass.mk z) ≤
    HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk y) (ArchimedeanClass.mk z)

Tactic:
rw [← mk_mul, ← mk_mul]

Premises used: ArchimedeanClass.mk_mul
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : IsStrictOrderedRing R
x y : R
h : LE.le (α := ArchimedeanClass R) (mk x) (mk y)
z : R
⊢ LE.le (α := ArchimedeanClass R) (mk (x * z)) (mk (y * z))

Tactic:
mk_mul_le_of_le h le_rfl

Premises used: le_rfl, _private.0.ArchimedeanClass.mk_mul_le_of_le
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : IsStrictOrderedRing R
x y : R
h : LE.le (α := ArchimedeanClass R) (mk x) (mk y)
z : R
⊢ LE.le (α := ArchimedeanClass R) (mk (x * z)) (mk (y * z))

Tactic:
exact mk_mul_le_of_le h le_rfl

Premises used: le_rfl, _private.0.ArchimedeanClass.mk_mul_le_of_le
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : x ≠ 0
rw : IsAddLeftRegular (R := ArchimedeanClass R) (mk x)
⊢ IsAddRegular (R := ArchimedeanClass R) (mk x)

Tactic:
rw [← isAddLeftRegular_iff_isAddRegular]

Premises used: isAddLeftRegular_iff_isAddRegular
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : x ≠ 0
y z : R
hyz :
  Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x_1 : ArchimedeanClass R) ↦ mk x + x_1) (mk y))
    ((fun (x_1 : ArchimedeanClass R) ↦ mk x + x_1) (mk z))
⊢ Eq (α := ArchimedeanClass R) (mk y) (mk z)

Tactic:
simpa [← mk_mul, mk_eq_mk, mul_left_comm _ (|x|), abs_pos.2 hx] using hyz

Premises used: Iff.mpr, abs, mul_left_comm, ArchimedeanClass.mk_mul, abs_pos, ArchimedeanClass.mk_eq_mk
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : x ≠ 0
z : ArchimedeanClass R
y : R
hyz :
  Eq.{u_1 + 1} (α := ArchimedeanClass R)
    ((fun (x_1 : ArchimedeanClass R) ↦ ArchimedeanClass.mk x + x_1) (ArchimedeanClass.mk y))
    ((fun (x_1 : ArchimedeanClass R) ↦ ArchimedeanClass.mk x + x_1) z)
mk :
  ∀ (z : R)
    (hyz :
      Eq.{u_1 + 1} (α := ArchimedeanClass R)
        ((fun (x_1 : ArchimedeanClass R) ↦ ArchimedeanClass.mk x + x_1) (ArchimedeanClass.mk y))
        ((fun (x_1 : ArchimedeanClass R) ↦ ArchimedeanClass.mk x + x_1) (ArchimedeanClass.mk z))),
    Eq (α := ArchimedeanClass R) (ArchimedeanClass.mk y) (ArchimedeanClass.mk z)
⊢ ArchimedeanClass.mk y = z

Tactic:
induction z with | mk z =>
  simpa [← mk_mul, mk_eq_mk, mul_left_comm _ (|x|), abs_pos.2 hx] using hyz

Premises used: Iff.mpr, abs, mul_left_comm, ArchimedeanClass.mk_mul, abs_pos, ArchimedeanClass.mk_eq_mk, ArchimedeanClass.mk
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : x ≠ 0
y z : ArchimedeanClass R
hyz :
  Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x_1 : ArchimedeanClass R) ↦ ArchimedeanClass.mk x + x_1) y)
    ((fun (x_1 : ArchimedeanClass R) ↦ ArchimedeanClass.mk x + x_1) z)
mk :
  ∀ (y : R)
    (hyz :
      Eq.{u_1 + 1} (α := ArchimedeanClass R)
        ((fun (x_1 : ArchimedeanClass R) ↦ ArchimedeanClass.mk x + x_1) (ArchimedeanClass.mk y))
        ((fun (x_1 : ArchimedeanClass R) ↦ ArchimedeanClass.mk x + x_1) z)),
    ArchimedeanClass.mk y = z
⊢ y = z

Tactic:
induction y with | mk y =>
  induction z with | mk z =>
  simpa [← mk_mul, mk_eq_mk, mul_left_comm _ (|x|), abs_pos.2 hx] using hyz

Premises used: Iff.mpr, abs, mul_left_comm, ArchimedeanClass.mk_mul, abs_pos, ArchimedeanClass.mk_eq_mk, ArchimedeanClass.mk
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : IsStrictOrderedRing R
x : R
mk : HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk 0) (ArchimedeanClass.mk x) = ArchimedeanClass.mk 0
mk₁ : Eq (α := ArchimedeanClass R) (ArchimedeanClass.mk (0 * x)) (ArchimedeanClass.mk 0)
mk₂ mk₃ : Eq.{u_1 + 1} (α := ArchimedeanClass R) (ArchimedeanClass.mk 0) (ArchimedeanClass.mk 0)
⊢ HAdd.hAdd (α := ArchimedeanClass R) ⊤ (ArchimedeanClass.mk x) = ⊤

Tactic:
rw [← mk_zero, ← mk_mul, zero_mul]

Premises used: MulZeroClass.zero_mul, ArchimedeanClass.mk_zero, ArchimedeanClass.mk_mul
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : IsStrictOrderedRing R
x : ArchimedeanClass R
mk : ∀ (x : R), HAdd.hAdd (α := ArchimedeanClass R) ⊤ (ArchimedeanClass.mk x) = ⊤
⊢ ⊤ + x = ⊤

Tactic:
induction x with | mk x => rw [← mk_zero, ← mk_mul, zero_mul]

Premises used: MulZeroClass.zero_mul, ArchimedeanClass.mk_zero, ArchimedeanClass.mk_mul, ArchimedeanClass.mk
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : IsStrictOrderedRing R
x : R
⊢ Ne (α := ArchimedeanClass R) (mk x) ⊤ → IsAddLeftRegular (R := ArchimedeanClass R) (mk x)

Tactic:
simp +contextual [isAddRegular_mk]

Premises used: ArchimedeanClass.isAddRegular_mk
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : IsStrictOrderedRing R
x : ArchimedeanClass R
mk :
  ∀ (x : R),
    Ne (α := ArchimedeanClass R) (ArchimedeanClass.mk x) ⊤ →
      IsAddLeftRegular (R := ArchimedeanClass R) (ArchimedeanClass.mk x)
⊢ x ≠ ⊤ → IsAddLeftRegular x

Tactic:
induction x with | mk x => simp +contextual [isAddRegular_mk]

Premises used: ArchimedeanClass.isAddRegular_mk, ArchimedeanClass.mk
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
a : R
⊢ Eq (α := ArchimedeanClass R) ((addValuation R : (a : R) → ArchimedeanClass R) a : ArchimedeanClass R)
    (mk a : ArchimedeanClass R)

Tactic:
rfl

Premises used: rfl, toAntisymmetrization, ArchimedeanClass.mk
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
S : Type u_3
inst_3 : LinearOrder S
inst_4 : CommRing S
inst_5 : IsStrictOrderedRing S
f : S →+o R
rw :
  Eq.{u_1 + 1} (α := ArchimedeanClass R)
    ((orderHom f : (a : ArchimedeanClass S) → ArchimedeanClass R) (mk 1) : ArchimedeanClass R)
    (mk ((f : (a : S) → R) 1) : ArchimedeanClass R)
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := ArchimedeanClass R) (mk ((f : (a : S) → R) 1) : ArchimedeanClass R)
    (mk ((f : (a : S) → R) 1) : ArchimedeanClass R)
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R)
    ((orderHom f : (a : ArchimedeanClass S) → ArchimedeanClass R) 0 : ArchimedeanClass R)
    (mk ((f : (a : S) → R) 1) : ArchimedeanClass R)

Tactic:
rw [← mk_one, orderHom_mk]

Premises used: ArchimedeanClass.mk_one, ArchimedeanClass.orderHom_mk
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
S : Type u_3
inst : LinearOrder S
inst_1 : CommRing S
inst_2 : IsStrictOrderedRing S
inst_3 : Archimedean S
x : S
h : x ≠ 0
⊢ Eq (α := ArchimedeanClass S) (mk x) 0

Tactic:
mk_eq_mk_of_archimedean h one_ne_zero

Premises used: ArchimedeanClass.mk_eq_mk_of_archimedean, one_ne_zero
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
S : Type u_3
inst : LinearOrder S
inst_1 : CommRing S
inst_2 : IsStrictOrderedRing S
inst_3 : Archimedean S
x : ArchimedeanClass S
mk :
  ∀ (x : S),
    Eq (α := ArchimedeanClass S) (ArchimedeanClass.mk x) 0 ∨ Eq (α := ArchimedeanClass S) (ArchimedeanClass.mk x) ⊤
⊢ x = 0 ∨ x = ⊤

Tactic:
induction x with | mk x

Premises used: ArchimedeanClass.mk
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
S : Type u_3
inst : LinearOrder S
inst_1 : CommRing S
inst_2 : IsStrictOrderedRing S
inst_3 : Archimedean S
x : S
mk :
  Eq.{u_3 + 1} (α := ArchimedeanClass S) (ArchimedeanClass.mk 0) 0 ∨
    Eq.{u_3 + 1} (α := ArchimedeanClass S) (ArchimedeanClass.mk 0) ⊤
mk₁ :
  ∀ (h : x ≠ 0),
    Eq (α := ArchimedeanClass S) (ArchimedeanClass.mk x) 0 ∨ Eq (α := ArchimedeanClass S) (ArchimedeanClass.mk x) ⊤
⊢ Eq (α := ArchimedeanClass S) (ArchimedeanClass.mk x) 0 ∨ Eq (α := ArchimedeanClass S) (ArchimedeanClass.mk x) ⊤

Tactic:
obtain rfl | h := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
S : Type u_3
inst : LinearOrder S
inst_1 : CommRing S
inst_2 : IsStrictOrderedRing S
inst_3 : Archimedean S
⊢ Eq.{u_3 + 1} (α := ArchimedeanClass S) (mk 0) 0 ∨ Eq.{u_3 + 1} (α := ArchimedeanClass S) (mk 0) ⊤

Tactic:
simp_all
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
S : Type u_3
inst : LinearOrder S
inst_1 : CommRing S
inst_2 : IsStrictOrderedRing S
inst_3 : Archimedean S
x : S
h : x ≠ 0
⊢ Eq (α := ArchimedeanClass S) (mk x) 0 ∨ Eq (α := ArchimedeanClass S) (mk x) ⊤

Tactic:
simp_all
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
S : Type u_3
inst_3 : LinearOrder S
inst_4 : CommRing S
inst_5 : IsStrictOrderedRing S
inst_6 : Archimedean S
f : S →+o R
x : S
h : x ≠ 0
rw :
  Eq.{u_1 + 1} (α := ArchimedeanClass R)
    ((orderHom f : (a : ArchimedeanClass S) → ArchimedeanClass R) (mk x) : ArchimedeanClass R)
    (mk ((f : (a : S) → R) 1) : ArchimedeanClass R)
rw₁ :
  Eq.{u_1 + 1} (α := ArchimedeanClass R)
    ((orderHom f : (a : ArchimedeanClass S) → ArchimedeanClass R) 0 : ArchimedeanClass R)
    (mk ((f : (a : S) → R) 1) : ArchimedeanClass R)
rw₂ rw₃ :
  Eq.{u_1 + 1} (α := ArchimedeanClass R) (mk ((f : (a : S) → R) 1) : ArchimedeanClass R)
    (mk ((f : (a : S) → R) 1) : ArchimedeanClass R)
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R) (mk ((f : (a : S) → R) x) : ArchimedeanClass R)
    (mk ((f : (a : S) → R) 1) : ArchimedeanClass R)

Tactic:
rw [← orderHom_mk, mk_eq_zero_of_archimedean h, orderHom_zero]

Premises used: ArchimedeanClass.orderHom_zero, ArchimedeanClass.orderHom_mk, ArchimedeanClass.mk_eq_zero_of_archimedean
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
S : Type u_3
inst_3 : LinearOrder S
inst_4 : CommRing S
inst_5 : IsStrictOrderedRing S
inst_6 : Archimedean S
f : S →+*o R
x : S
h : x ≠ 0
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R) (mk ((f : (a : S) → R) x) : ArchimedeanClass R) (0 : ArchimedeanClass R)

Tactic:
simpa using mk_map_of_archimedean f.toOrderAddMonoidHom h

Premises used: OrderRingHom.toOrderAddMonoidHom, ArchimedeanClass.mk_map_of_archimedean
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
S : Type u_3
inst_3 : LinearOrder S
inst_4 : CommRing S
inst_5 : IsStrictOrderedRing S
inst_6 : Archimedean S
f : S →+*o R
x : R
y : S
inl :
  mk x ≤
    HAdd.hAdd (α := ArchimedeanClass R) (β := ArchimedeanClass R) (mk ((f : (a : S) → R) 0) : ArchimedeanClass R) (mk x)
inr :
  ∀ (hy : y ≠ 0),
    mk x ≤
      HAdd.hAdd (α := ArchimedeanClass R) (β := ArchimedeanClass R) (mk ((f : (a : S) → R) y) : ArchimedeanClass R)
        (mk x)
⊢ mk x ≤
    HAdd.hAdd (α := ArchimedeanClass R) (β := ArchimedeanClass R) (mk ((f : (a : S) → R) y) : ArchimedeanClass R) (mk x)

Tactic:
obtain rfl | hy := eq_or_ne y 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
S : Type u_3
inst_3 : LinearOrder S
inst_4 : CommRing S
inst_5 : IsStrictOrderedRing S
inst_6 : Archimedean S
f : S →+*o R
x : R
⊢ mk x ≤
    HAdd.hAdd (α := ArchimedeanClass R) (β := ArchimedeanClass R) (mk ((f : (a : S) → R) 0) : ArchimedeanClass R) (mk x)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
S : Type u_3
inst_3 : LinearOrder S
inst_4 : CommRing S
inst_5 : IsStrictOrderedRing S
inst_6 : Archimedean S
f : S →+*o R
x : R
y : S
hy : y ≠ 0
inr : mk x ≤ HAdd.hAdd (α := ArchimedeanClass R) 0 (mk x)
inr₁ inr₂ : LE.le (α := ArchimedeanClass R) (mk x) (mk x)
⊢ mk x ≤
    HAdd.hAdd (α := ArchimedeanClass R) (β := ArchimedeanClass R) (mk ((f : (a : S) → R) y) : ArchimedeanClass R) (mk x)

Tactic:
rw [mk_map_of_archimedean' f hy, zero_add]

Premises used: zero_add, ArchimedeanClass.mk_map_of_archimedean'
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
S : Type u_3
inst_3 : LinearOrder S
inst_4 : CommRing S
inst_5 : IsStrictOrderedRing S
inst_6 : Archimedean S
f : S →+*o R
x : R
y : S
rw :
  mk x ≤
    HAdd.hAdd (α := ArchimedeanClass R) (β := ArchimedeanClass R) (mk ((f : (a : S) → R) y) : ArchimedeanClass R) (mk x)
⊢ mk x ≤
    HAdd.hAdd (α := ArchimedeanClass R) (β := ArchimedeanClass R) (mk x) (mk ((f : (a : S) → R) y) : ArchimedeanClass R)

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
S : Type u_3
inst_3 : LinearOrder S
inst_4 : CommRing S
inst_5 : IsStrictOrderedRing S
inst_6 : Archimedean S
f : S →+*o R
x : R
y : S
⊢ mk x ≤
    HAdd.hAdd (α := ArchimedeanClass R) (β := ArchimedeanClass R) (mk ((f : (a : S) → R) y) : ArchimedeanClass R) (mk x)

Tactic:
mk_le_mk_add_of_archimedean f x y

Premises used: ArchimedeanClass.mk_le_mk_add_of_archimedean
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
S : Type u_3
inst_3 : LinearOrder S
inst_4 : CommRing S
inst_5 : IsStrictOrderedRing S
inst_6 : Archimedean S
f : S →+*o R
x : R
y : S
⊢ mk x ≤
    HAdd.hAdd (α := ArchimedeanClass R) (β := ArchimedeanClass R) (mk ((f : (a : S) → R) y) : ArchimedeanClass R) (mk x)

Tactic:
exact mk_le_mk_add_of_archimedean f x y

Premises used: ArchimedeanClass.mk_le_mk_add_of_archimedean
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
S : Type u_3
inst_3 : LinearOrder S
inst_4 : CommRing S
inst_5 : IsStrictOrderedRing S
inst_6 : Archimedean S
f : S →+*o R
y : S
⊢ LE.le.{u_1} (α := ArchimedeanClass R) (0 : ArchimedeanClass R) (mk ((f : (a : S) → R) y) : ArchimedeanClass R)

Tactic:
simpa using mk_le_mk_add_of_archimedean f 1 y

Premises used: ArchimedeanClass.mk_le_mk_add_of_archimedean, OfNat.ofNat