awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
a b : α
inl : ∀ (h : |a| = a), |a| ∣ b ↔ a ∣ b
inr : ∀ (h : |a| = -a), |a| ∣ b ↔ a ∣ b
⊢ |a| ∣ b ↔ a ∣ b

Tactic:
rcases abs_choice a with h | h

Premises used: abs_choice
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
a b : α
h : |a| = a
⊢ |a| ∣ b ↔ a ∣ b

Tactic:
simp only [h, neg_dvd]

Premises used: neg_dvd
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
a b : α
h : |a| = -a
⊢ |a| ∣ b ↔ a ∣ b

Tactic:
simp only [h, neg_dvd]

Premises used: neg_dvd
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
a : α
⊢ |a| ∣ a

Tactic:
(abs_dvd a a).mpr (dvd_refl a)

Premises used: Iff.mpr, abs_dvd, dvd_refl
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
a b : α
inl : ∀ (h : |b| = b), a ∣ |b| ↔ a ∣ b
inr : ∀ (h : |b| = -b), a ∣ |b| ↔ a ∣ b
⊢ a ∣ |b| ↔ a ∣ b

Tactic:
rcases abs_choice b with h | h

Premises used: abs_choice
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
a b : α
h : |b| = b
⊢ a ∣ |b| ↔ a ∣ b

Tactic:
simp only [h, dvd_neg]

Premises used: dvd_neg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
a b : α
h : |b| = -b
⊢ a ∣ |b| ↔ a ∣ b

Tactic:
simp only [h, dvd_neg]

Premises used: dvd_neg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
a : α
⊢ a ∣ |a|

Tactic:
(dvd_abs a a).mpr (dvd_refl a)

Premises used: Iff.mpr, dvd_abs, dvd_refl
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
a b : α
⊢ |a| ∣ |b| ↔ a ∣ b

Tactic:
(abs_dvd _ _).trans (dvd_abs _ _)

Premises used: abs_dvd, Iff.trans, dvd_abs
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
n : ℕ
hn : n ≠ 0
hne : Even n ∧ ¬Odd n
⊢ a ^ n = b ^ n ↔ a = b ∨ a = -b ∧ Even n

Tactic:
simp only [*, and_true, ← abs_eq_abs,
    ← pow_left_inj₀ (abs_nonneg a) (abs_nonneg b) hn, hne.1.pow_abs]

Premises used: and_true, pow_left_inj₀, And.left, abs_eq_abs, abs_nonneg, Even.pow_abs
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
n : ℕ
hn_1 : n ≠ 0
hn : Odd n ∧ ¬Even n
⊢ a ^ n = b ^ n ↔ a = b ∨ a = -b ∧ Even n

Tactic:
simp [hn, (hn.1.strictMono_pow (R := R)).injective.eq_iff]

Premises used: Function.Injective.eq_iff, Odd.strictMono_pow, StrictMono.injective, And.left
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
n : ℕ
inl : HPow.hPow (β := ℕ) a 0 = HPow.hPow (β := ℕ) b 0 ↔ Eq (α := ℕ) 0 0 ∨ a = b ∨ a = -b ∧ Even (α := ℕ) 0
inr : ∀ (hn : n ≠ 0), a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n
⊢ a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
⊢ HPow.hPow (β := ℕ) a 0 = HPow.hPow (β := ℕ) b 0 ↔ Eq (α := ℕ) 0 0 ∨ a = b ∨ a = -b ∧ Even (α := ℕ) 0

Tactic:
simp [pow_eq_pow_iff_of_ne_zero, *]

Premises used: pow_eq_pow_iff_of_ne_zero
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
n : ℕ
hn : n ≠ 0
⊢ a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n

Tactic:
simp [pow_eq_pow_iff_of_ne_zero, *]

Premises used: pow_eq_pow_iff_of_ne_zero
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
n : ℕ
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a = 1 ∨ a = -1 ∧ Even n

Tactic:
simp [← pow_eq_pow_iff_of_ne_zero hn]

Premises used: pow_eq_pow_iff_of_ne_zero
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
n : ℕ
⊢ a ^ n = 1 ↔ n = 0 ∨ a = 1 ∨ a = -1 ∧ Even n

Tactic:
simp [← pow_eq_pow_iff_cases]

Premises used: pow_eq_pow_iff_cases
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
n : ℕ
hb : b ≠ 0
he : Even n
⊢ -b ^ n < 0

Tactic:
simp [he.pow_pos hb]

Premises used: Even.pow_pos
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
n : ℕ
hb : b ≠ 0
he : Even n
this : a ^ n > -b ^ n
⊢ a ^ n = -b ^ n ↔ a = -b ∧ Odd n

Tactic:
simpa [he, not_odd_iff_even.2 he] using this.ne'

Premises used: Iff.mpr, Nat.not_odd_iff_even, LT.lt.ne'
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
n : ℕ
hb : b ≠ 0
ho : Odd n
⊢ a ^ n = -b ^ n ↔ a = -b ∧ Odd n

Tactic:
simp only [ho, and_true, ← ho.neg_pow, (ho.strictMono_pow (R := R)).injective.eq_iff]

Premises used: Odd.neg_pow, and_true, Function.Injective.eq_iff, Odd.strictMono_pow, StrictMono.injective
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
n : ℕ
⊢ a ^ n = -1 ↔ a = -1 ∧ Odd n

Tactic:
simpa using pow_eq_neg_pow_iff (R := R) one_ne_zero

Premises used: pow_eq_neg_pow_iff, one_ne_zero
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
n a : ℕ
ha : Even a
⊢ Odd (n % a) ↔ Odd n

Tactic:
((even_sub' <| mod_le n a).mp <|
      even_iff_two_dvd.mpr <| (even_iff_two_dvd.mp ha).trans <| dvd_sub_mod n).symm

Premises used: Iff.mpr, Nat.dvd_sub_mod, Nat.even_sub', Nat.mod_le, Iff.mp, even_iff_two_dvd, Iff.symm, Dvd.dvd.trans
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
n a : ℕ
ha : Even a
⊢ Even (n % a) ↔ Even n

Tactic:
((even_sub <| mod_le n a).mp <|
      even_iff_two_dvd.mpr <| (even_iff_two_dvd.mp ha).trans <| dvd_sub_mod n).symm

Premises used: Iff.mpr, Nat.dvd_sub_mod, Nat.mod_le, Iff.mp, even_iff_two_dvd, Iff.symm, Dvd.dvd.trans, Nat.even_sub
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
n a : ℕ
hn : Odd n
ha : Even a
⊢ Odd (n % a)

Tactic:
(Odd.mod_even_iff ha).mpr hn

Premises used: Iff.mpr, Odd.mod_even_iff
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
n a : ℕ
hn : Even n
ha : Even a
⊢ Even (n % a)

Tactic:
(Even.mod_even_iff ha).mpr hn

Premises used: Iff.mpr, Even.mod_even_iff
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
m n : ℕ
hn : Odd n
hm : m ∣ n
⊢ Odd m

Tactic:
not_even_iff_odd.1 <| mt hm.even (not_even_iff_odd.2 hn)

Premises used: Iff.mpr, mt, Dvd.dvd.even, Nat.not_even_iff_odd, Iff.mp
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
n : ℕ
hn : Odd n
hm : 2 ∣ n
⊢ ¬Odd (α := ℕ) 2

Tactic:
decide
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
n : ℕ
hn : Odd n
hm : 2 ∣ n
⊢ False

Tactic:
exact absurd (hn.of_dvd_nat hm) (by decide)

Premises used: Odd.of_dvd_nat, absurd
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
a b : ℤ
h₁ : b ≠ 0
h₂ : a ∣ b
⊢ 0 < |b|

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
a b : ℤ
h₁ : b ≠ 0
h₂ : a ∣ b
⊢ a ∣ |b|

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R) (mk 1) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
⊢ Ne.{u_1 + 1} (α := ArchimedeanClass R) ⊤ 0

Tactic:
simp [← mk_one]

Premises used: ArchimedeanClass.mk_one
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
⊢ Ne.{u_1 + 1} (α := ArchimedeanClass R) 0 ⊤

Tactic:
top_ne_zero.symm

Premises used: ArchimedeanClass.top_ne_zero, Ne.symm
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x₁ y₁ x₂ y₂ : R
hx : LE.le (α := ArchimedeanClass R) (mk x₁) (mk x₂)
hy : LE.le (α := ArchimedeanClass R) (mk y₁) (mk y₂)
obtain :
  ∀ (m : ℕ)
    (hm :
      |(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x₂ : ArchimedeanOrder R)| ≤
        HSMul.hSMul (β := R) m
          (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
                ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x₁ : ArchimedeanOrder R)| :
            R)),
    LE.le (α := ArchimedeanClass R) (mk (x₁ * y₁)) (mk (x₂ * y₂))
⊢ LE.le (α := ArchimedeanClass R) (mk (x₁ * y₁)) (mk (x₂ * y₂))

Tactic:
obtain ⟨m, hm⟩ := hx
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x₁ y₁ x₂ y₂ : R
hy : LE.le (α := ArchimedeanClass R) (mk y₁) (mk y₂)
m : ℕ
hm :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
        ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x₂ : ArchimedeanOrder R)| ≤
    HSMul.hSMul (β := R) m
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x₁ : ArchimedeanOrder R)| :
        R)
obtain :
  ∀ (n : ℕ)
    (hn :
      |(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) y₂ : ArchimedeanOrder R)| ≤
        HSMul.hSMul (β := R) n
          (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
                ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) y₁ : ArchimedeanOrder R)| :
            R)),
    LE.le (α := ArchimedeanClass R) (mk (x₁ * y₁)) (mk (x₂ * y₂))
⊢ LE.le (α := ArchimedeanClass R) (mk (x₁ * y₁)) (mk (x₂ * y₂))

Tactic:
obtain ⟨n, hn⟩ := hy
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x₁ y₁ x₂ y₂ : R
m : ℕ
hm :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
        ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x₂ : ArchimedeanOrder R)| ≤
    HSMul.hSMul (β := R) m
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x₁ : ArchimedeanOrder R)| :
        R)
n : ℕ
hn :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
        ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) y₂ : ArchimedeanOrder R)| ≤
    HSMul.hSMul (β := R) n
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) y₁ : ArchimedeanOrder R)| :
        R)
h :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
        ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) (x₂ * y₂) : ArchimedeanOrder R)| ≤
    HSMul.hSMul (β := R) (m * n)
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) (x₁ * y₁) : ArchimedeanOrder R)| :
        R)
⊢ LE.le (α := ArchimedeanClass R) (mk (x₁ * y₁)) (mk (x₂ * y₂))

Tactic:
use m * n
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x₁ y₁ x₂ y₂ : R
m : ℕ
hm :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
        ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x₂ : ArchimedeanOrder R)| ≤
    HSMul.hSMul (β := R) m
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x₁ : ArchimedeanOrder R)| :
        R)
n : ℕ
hn :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
        ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) y₂ : ArchimedeanOrder R)| ≤
    HSMul.hSMul (β := R) n
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) y₁ : ArchimedeanOrder R)| :
        R)
⊢ HMul.hMul (α := R) (β := R)
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x₂ : ArchimedeanOrder R)| :
        R)
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) y₂ : ArchimedeanOrder R)| :
        R) ≤
    HSMul.hSMul (β := R) m
        (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
              ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x₁ : ArchimedeanOrder R)| :
          R) *
      HSMul.hSMul (β := R) n
        (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
              ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) y₁ : ArchimedeanOrder R)| :
          R)

Tactic:
mul_le_mul hm hn (abs_nonneg _) (nsmul_nonneg (abs_nonneg _) _)

Premises used: nsmul_nonneg, mul_le_mul, abs_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x₁ y₁ x₂ y₂ : R
m : ℕ
hm :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
        ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x₂ : ArchimedeanOrder R)| ≤
    HSMul.hSMul (β := R) m
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x₁ : ArchimedeanOrder R)| :
        R)
n : ℕ
hn :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
        ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) y₂ : ArchimedeanOrder R)| ≤
    HSMul.hSMul (β := R) n
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) y₁ : ArchimedeanOrder R)| :
        R)
h :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
        ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) (x₂ * y₂) : ArchimedeanOrder R)| =
    HMul.hMul (α := R) (β := R)
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x₂ : ArchimedeanOrder R)| :
        R)
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) y₂ : ArchimedeanOrder R)| :
        R)
h₁ :
  HSMul.hSMul (β := R) (m * n)
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) (x₁ * y₁) : ArchimedeanOrder R)| :
        R) =
    HSMul.hSMul (β := R) m
        (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
              ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x₁ : ArchimedeanOrder R)| :
          R) *
      HSMul.hSMul (β := R) n
        (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
              ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) y₁ : ArchimedeanOrder R)| :
          R)
⊢ |(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
        ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) (x₂ * y₂) : ArchimedeanOrder R)| ≤
    HSMul.hSMul (β := R) (m * n)
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) (x₁ * y₁) : ArchimedeanOrder R)| :
        R)

Tactic:
convert! mul_le_mul hm hn (abs_nonneg _) (nsmul_nonneg (abs_nonneg _) _) using 1

Premises used: nsmul_nonneg, mul_le_mul, abs_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x₁ y₁ x₂ y₂ : R
m : ℕ
hm :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
        ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x₂ : ArchimedeanOrder R)| ≤
    HSMul.hSMul (β := R) m
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x₁ : ArchimedeanOrder R)| :
        R)
n : ℕ
hn :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
        ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) y₂ : ArchimedeanOrder R)| ≤
    HSMul.hSMul (β := R) n
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) y₁ : ArchimedeanOrder R)| :
        R)
h : |x₂ * y₂| = |x₂| * |y₂|
⊢ |(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
        ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) (x₂ * y₂) : ArchimedeanOrder R)| =
    HMul.hMul (α := R) (β := R)
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x₂ : ArchimedeanOrder R)| :
        R)
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) y₂ : ArchimedeanOrder R)| :
        R)

Tactic:
simp_rw [ArchimedeanOrder.val_of, abs_mul]

Premises used: abs_mul, ArchimedeanOrder.val_of
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x₁ y₁ x₂ y₂ : R
m : ℕ
hm :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
        ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x₂ : ArchimedeanOrder R)| ≤
    HSMul.hSMul (β := R) m
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x₁ : ArchimedeanOrder R)| :
        R)
n : ℕ
hn :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
        ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) y₂ : ArchimedeanOrder R)| ≤
    HSMul.hSMul (β := R) n
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) y₁ : ArchimedeanOrder R)| :
        R)
h : (m * n) • (|x₁| * |y₁|) = m • |x₁| * n • |y₁|
⊢ HSMul.hSMul (β := R) (m * n)
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) (x₁ * y₁) : ArchimedeanOrder R)| :
        R) =
    HSMul.hSMul (β := R) m
        (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
              ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x₁ : ArchimedeanOrder R)| :
          R) *
      HSMul.hSMul (β := R) n
        (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
              ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) y₁ : ArchimedeanOrder R)| :
          R)

Tactic:
simp_rw [ArchimedeanOrder.val_of, abs_mul]

Premises used: abs_mul, ArchimedeanOrder.val_of
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x₁ y₁ x₂ y₂ : R
m : ℕ
hm :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
        ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x₂ : ArchimedeanOrder R)| ≤
    HSMul.hSMul (β := R) m
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x₁ : ArchimedeanOrder R)| :
        R)
n : ℕ
hn :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
        ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) y₂ : ArchimedeanOrder R)| ≤
    HSMul.hSMul (β := R) n
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) y₁ : ArchimedeanOrder R)| :
        R)
⊢ (m * n) • (|x₁| * |y₁|) = m • |x₁| * n • |y₁|

Tactic:
ring
-- 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 x_1 x_2 x_3 : R
hx : Eq (α := ArchimedeanClass R) (mk x) (mk x_1)
hy : Eq (α := ArchimedeanClass R) (mk x_2) (mk x_3)
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x y : R) ↦ (mk (x * y) : ArchimedeanClass R)) x x_2)
    ((fun (x y : R) ↦ (mk (x * y) : ArchimedeanClass R)) x_1 x_3)

Tactic:
(mk_mul_le_of_le hx.le hy.le).antisymm (mk_mul_le_of_le hx.ge hy.ge)

Premises used: Eq.ge, LE.le.antisymm, Eq.le, _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 x_1 x_2 x_3 : R
hx : Eq (α := ArchimedeanClass R) (mk x) (mk x_1)
hy : Eq (α := ArchimedeanClass R) (mk x_2) (mk x_3)
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x y : R) ↦ (mk (x * y) : ArchimedeanClass R)) x x_2)
    ((fun (x y : R) ↦ (mk (x * y) : ArchimedeanClass R)) x_1 x_3)

Tactic:
exact (mk_mul_le_of_le hx.le hy.le).antisymm (mk_mul_le_of_le hx.ge hy.ge)

Premises used: Eq.ge, LE.le.antisymm, Eq.le, _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 y : R
⊢ mk (x * y) = HAdd.hAdd (α := ArchimedeanClass R) (mk x) (mk y)

Tactic:
rfl

Premises used: ArchimedeanClass.lift₂, rfl, toAntisymmetrization, 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 : Eq (α := ArchimedeanClass R) (mk x) (mk y)
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x : R) ↦ (mk (HPow.hPow (β := ℕ) x 0) : ArchimedeanClass R)) x)
    ((fun (x : R) ↦ (mk (HPow.hPow (β := ℕ) x 0) : ArchimedeanClass R)) y)

Tactic:
simp
-- 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 : Eq (α := ArchimedeanClass R) (mk x) (mk y)
n : ℕ
IH :
  Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x : R) ↦ (mk (x ^ n) : ArchimedeanClass R)) x)
    ((fun (x : R) ↦ (mk (x ^ n) : ArchimedeanClass R)) y)
succ succ₁ : Eq (α := ArchimedeanClass R) (mk (x ^ (n + 1))) (mk (y ^ (n + 1)))
succ₂ : Eq (α := ArchimedeanClass R) (mk (x ^ n * x)) (mk (y ^ n * y))
succ₃ :
  HAdd.hAdd (α := ArchimedeanClass R) (mk (x ^ n)) (mk x) = HAdd.hAdd (α := ArchimedeanClass R) (mk (y ^ n)) (mk y)
succ₄ :
  HAdd.hAdd (α := ArchimedeanClass R) (mk (y ^ n)) (mk x) = HAdd.hAdd (α := ArchimedeanClass R) (mk (y ^ n)) (mk y)
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x : R) ↦ (mk (x ^ (n + 1)) : ArchimedeanClass R)) x)
    ((fun (x : R) ↦ (mk (x ^ (n + 1)) : ArchimedeanClass R)) y)

Tactic:
simp_rw [pow_succ, mk_mul, IH, h]

Premises used: 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 y : R
h : Eq (α := ArchimedeanClass R) (mk x) (mk y)
zero :
  Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x : R) ↦ (mk (HPow.hPow (β := ℕ) x 0) : ArchimedeanClass R)) x)
    ((fun (x : R) ↦ (mk (HPow.hPow (β := ℕ) x 0) : ArchimedeanClass R)) y)
succ :
  ∀ (n : ℕ)
    (IH :
      Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x : R) ↦ (mk (x ^ n) : ArchimedeanClass R)) x)
        ((fun (x : R) ↦ (mk (x ^ n) : ArchimedeanClass R)) y)),
    Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x : R) ↦ (mk (x ^ (n + 1)) : ArchimedeanClass R)) x)
      ((fun (x : R) ↦ (mk (x ^ (n + 1)) : ArchimedeanClass R)) y)
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x : R) ↦ (mk (x ^ n) : ArchimedeanClass R)) x)
    ((fun (x : R) ↦ (mk (x ^ n) : ArchimedeanClass R)) y)

Tactic:
induction n with
    | zero => simp
    | succ n IH => simp_rw [pow_succ, mk_mul, IH, h]

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

Tactic:
rfl

Premises used: ArchimedeanClass.lift, rfl, toAntisymmetrization, ArchimedeanClass.mk