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
inst_4 : Ring S
inst_5 : IsStrictOrderedRing S
inst_6 : DenselyOrdered R
inst_7 : Archimedean R
x y : S
f : R →+* S
hf : StrictMono.{u_1, u_2} (α := R) (β := S) (⇑f : (a : R) → S)
H : ∀ {q : R}, LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ↔ 0 < q
n : ℕ
hn :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder S) → S)
        ((ArchimedeanOrder.of : (a : S) → ArchimedeanOrder S) y : ArchimedeanOrder S)| ≤
    HSMul.hSMul (β := S) (n + 1)
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder S) → S)
            ((ArchimedeanOrder.of : (a : S) → ArchimedeanOrder S) x : ArchimedeanOrder S)| :
        S)
q : R
hq₀ : 0 < q
hq : (n + 1) • q < 1
⊢ HAdd.hAdd (α := S) (↑n : S) 1 * HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ HAdd.hAdd (α := S) (↑n : S) 1 * |x|

Tactic:
simpa [← mul_assoc] using mul_le_mul (hf hq).le hn (abs_nonneg y) (by simp)

Premises used: mul_assoc, LT.lt.le, mul_le_mul, abs_nonneg
-- 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
inst_4 : Ring S
inst_5 : IsStrictOrderedRing S
inst_6 : DenselyOrdered R
inst_7 : Archimedean R
x y : S
f : R →+* S
hf : StrictMono.{u_1, u_2} (α := R) (β := S) (⇑f : (a : R) → S)
H : ∀ {q : R}, LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ↔ 0 < q
q : R
hq₀ : LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S)
hq : HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ |x|
⊢ 0 < q

Tactic:
have hq₀' := H.1 hq₀
-- 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
inst_4 : Ring S
inst_5 : IsStrictOrderedRing S
inst_6 : DenselyOrdered R
inst_7 : Archimedean R
x y : S
f : R →+* S
hf : StrictMono.{u_1, u_2} (α := R) (β := S) (⇑f : (a : R) → S)
H : ∀ {q : R}, LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ↔ 0 < q
q : R
hq₀ : LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S)
hq : HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ |x|
hq₀' : 0 < q
mpr : ∀ (n : ℕ) (hn : 1 < n • q), LE.le (α := ArchimedeanClass S) (mk x) (mk y)
⊢ LE.le (α := ArchimedeanClass S) (mk x) (mk y)

Tactic:
obtain ⟨n, hn⟩ := exists_lt_nsmul hq₀' 1

Premises used: exists_lt_nsmul, OfNat.ofNat
-- 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
inst_4 : Ring S
inst_5 : IsStrictOrderedRing S
inst_6 : DenselyOrdered R
inst_7 : Archimedean R
x y : S
f : R →+* S
hf : StrictMono.{u_1, u_2} (α := R) (β := S) (⇑f : (a : R) → S)
H : ∀ {q : R}, LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ↔ 0 < q
q : R
hq₀ : LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S)
hq : HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ |x|
hq₀' : 0 < q
n : ℕ
hn : 1 < n • q
⊢ LE.le (α := ArchimedeanClass S) (mk x) (mk y)

Tactic:
⟨n, le_of_mul_le_mul_left ?_ hq₀⟩

Premises used: le_of_mul_le_mul_left, Exists.intro
-- 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
inst_4 : Ring S
inst_5 : IsStrictOrderedRing S
inst_6 : DenselyOrdered R
inst_7 : Archimedean R
x y : S
f : R →+* S
hf : StrictMono.{u_1, u_2} (α := R) (β := S) (⇑f : (a : R) → S)
H : ∀ {q : R}, LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ↔ 0 < q
q : R
hq₀ : LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S)
hq : HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ |x|
hq₀' : 0 < q
n : ℕ
hn : 1 < n • q
mpr :
  HMul.hMul (α := S) (β := S) ((f : (a : R) → S) q : S)
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder S) → S)
            ((ArchimedeanOrder.of : (a : S) → ArchimedeanOrder S) y : ArchimedeanOrder S)| :
        S) ≤
    HMul.hMul (α := S) ((f : (a : R) → S) q : S)
      (HSMul.hSMul (β := S) n
        (|(ArchimedeanOrder.val : (a : ArchimedeanOrder S) → S)
              ((ArchimedeanOrder.of : (a : S) → ArchimedeanOrder S) x : ArchimedeanOrder S)| :
          S))
⊢ LE.le (α := ArchimedeanClass S) (mk x) (mk y)

Tactic:
refine ⟨n, le_of_mul_le_mul_left ?_ hq₀⟩
-- 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
inst_4 : Ring S
inst_5 : IsStrictOrderedRing S
inst_6 : DenselyOrdered R
inst_7 : Archimedean R
x y : S
f : R →+* S
hf : StrictMono.{u_1, u_2} (α := R) (β := S) (⇑f : (a : R) → S)
H : ∀ {q : R}, LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ↔ 0 < q
q : R
hq₀ : LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S)
hq : HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ |x|
hq₀' : 0 < q
n : ℕ
hn : 1 < n • q
rw : LE.le.{u_2} (α := S) ((f : (a : R) → S) 0 : S) ((f : (a : R) → S) (n • q) : S)
⊢ LE.le.{u_2} (α := S) (0 : S) ((f : (a : R) → S) (n • q) : S)

Tactic:
rw [← f.map_zero]

Premises used: RingHom.map_zero
-- 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
inst_4 : Ring S
inst_5 : IsStrictOrderedRing S
inst_6 : DenselyOrdered R
inst_7 : Archimedean R
x y : S
f : R →+* S
hf : StrictMono.{u_1, u_2} (α := R) (β := S) (⇑f : (a : R) → S)
H : ∀ {q : R}, LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ↔ 0 < q
q : R
hq₀ : LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S)
hq : HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ |x|
hq₀' : 0 < q
n : ℕ
hn : 1 < n • q
⊢ LE.le.{u_2} (α := S) ((f : (a : R) → S) 0 : S) ((f : (a : R) → S) (n • q) : S)

Tactic:
hf.monotone (nsmul_nonneg hq₀'.le n)

Premises used: StrictMono.monotone, LT.lt.le, nsmul_nonneg
-- 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
inst_4 : Ring S
inst_5 : IsStrictOrderedRing S
inst_6 : DenselyOrdered R
inst_7 : Archimedean R
x y : S
f : R →+* S
hf : StrictMono.{u_1, u_2} (α := R) (β := S) (⇑f : (a : R) → S)
H : ∀ {q : R}, LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ↔ 0 < q
q : R
hq₀ : LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S)
hq : HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ |x|
hq₀' : 0 < q
n : ℕ
hn : 1 < n • q
⊢ LE.le.{u_2} (α := S) ((f : (a : R) → S) 0 : S) ((f : (a : R) → S) (n • q) : S)

Tactic:
exact hf.monotone (nsmul_nonneg hq₀'.le n)

Premises used: StrictMono.monotone, LT.lt.le, nsmul_nonneg
-- 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
inst_4 : Ring S
inst_5 : IsStrictOrderedRing S
inst_6 : DenselyOrdered R
inst_7 : Archimedean R
x y : S
f : R →+* S
hf : StrictMono.{u_1, u_2} (α := R) (β := S) (⇑f : (a : R) → S)
H : ∀ {q : R}, LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ↔ 0 < q
q : R
hq₀ : LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S)
hq : HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ |x|
hq₀' : 0 < q
n : ℕ
hn : 1 < n • q
⊢ LE.le.{u_2} (α := S) (0 : S) ((f : (a : R) → S) (n • q) : S)

Tactic:
have h : 0 ≤ f (n • q) := by
      rw [← f.map_zero]
      exact hf.monotone (nsmul_nonneg hq₀'.le n)
-- 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
inst_4 : Ring S
inst_5 : IsStrictOrderedRing S
inst_6 : DenselyOrdered R
inst_7 : Archimedean R
x y : S
f : R →+* S
hf : StrictMono.{u_1, u_2} (α := R) (β := S) (⇑f : (a : R) → S)
H : ∀ {q : R}, LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ↔ 0 < q
q : R
hq₀ : LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S)
hq : HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ |x|
hq₀' : 0 < q
n : ℕ
hn : 1 < n • q
h : LE.le.{u_2} (α := S) (0 : S) ((f : (a : R) → S) (n • q) : S)
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) q : S)
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder S) → S)
            ((ArchimedeanOrder.of : (a : S) → ArchimedeanOrder S) y : ArchimedeanOrder S)| :
        S) ≤
    HMul.hMul (α := S) ((f : (a : R) → S) q : S)
      (HSMul.hSMul (β := S) n
        (|(ArchimedeanOrder.val : (a : ArchimedeanOrder S) → S)
              ((ArchimedeanOrder.of : (a : S) → ArchimedeanOrder S) x : ArchimedeanOrder S)| :
          S))

Tactic:
simpa [mul_comm, mul_assoc] using mul_le_mul (hf hn).le hq (mul_nonneg hq₀.le (abs_nonneg y)) h

Premises used: mul_nonneg, mul_assoc, LT.lt.le, mul_le_mul, mul_comm, abs_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : Field R
inst_3 : IsOrderedRing R
x y : R
h : Eq (α := ArchimedeanClass R) (mk x) (mk y)
inl :
  ∀ (h : Eq (α := ArchimedeanClass R) (mk 0) (mk y)),
    Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) 0)
      ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) y)
inr :
  ∀ (hx : x ≠ 0),
    Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) x)
      ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) y)
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) x)
    ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) y)

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : Field R
inst_3 : IsOrderedRing R
y : R
h : Eq (α := ArchimedeanClass R) (mk 0) (mk y)
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) 0)
    ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) y)

Tactic:
simp_all
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : Field R
inst_3 : IsOrderedRing R
x y : R
h : Eq (α := ArchimedeanClass R) (mk x) (mk y)
hx : x ≠ 0
inr :
  ∀ (h : Eq (α := ArchimedeanClass R) (mk x) (mk 0)),
    Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) x)
      ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) 0)
inr₁ :
  ∀ (hy : y ≠ 0),
    Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) x)
      ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) y)
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) x)
    ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) y)

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
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : Field R
inst_3 : IsOrderedRing R
x : R
hx : x ≠ 0
h : Eq (α := ArchimedeanClass R) (mk x) (mk 0)
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) x)
    ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) 0)

Tactic:
simp_all
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : Field R
inst_3 : IsOrderedRing R
x y : R
h : Eq (α := ArchimedeanClass R) (mk x) (mk y)
hx : x ≠ 0
hy : y ≠ 0
⊢ Ne (α := ArchimedeanClass R) (mk x) ⊤

Tactic:
simpa using hx
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : Field R
inst_3 : IsOrderedRing R
x y : R
h : Eq (α := ArchimedeanClass R) (mk x) (mk y)
hx : x ≠ 0
hy : y ≠ 0
⊢ Ne (α := ArchimedeanClass R) (mk x) ⊤

Tactic:
have hx' : mk x ≠ ⊤ := by simpa using hx
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : Field R
inst_3 : IsOrderedRing R
x y : R
h : Eq (α := ArchimedeanClass R) (mk x) (mk y)
hx : x ≠ 0
hy : y ≠ 0
hx' : Ne (α := ArchimedeanClass R) (mk x) ⊤
inr :
  HAdd.hAdd (α := ArchimedeanClass R) (mk x) ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) x) =
    HAdd.hAdd (α := ArchimedeanClass R) (mk x) ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) y)
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) x)
    ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) y)

Tactic:
apply add_left_cancel_of_ne_top hx'

Premises used: ArchimedeanClass.add_left_cancel_of_ne_top
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : Field R
inst_3 : IsOrderedRing R
x y : R
h : Eq (α := ArchimedeanClass R) (mk x) (mk y)
hx : x ≠ 0
hy : y ≠ 0
hx' : Ne (α := ArchimedeanClass R) (mk x) ⊤
inr :
  HAdd.hAdd (α := ArchimedeanClass R) (mk x) ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) x) =
    HAdd.hAdd (α := ArchimedeanClass R) (mk y) ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) y)
⊢ HAdd.hAdd (α := ArchimedeanClass R) (mk x) ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) x) =
    HAdd.hAdd (α := ArchimedeanClass R) (mk x) ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) y)

Tactic:
nth_rw 2 [h]
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : Field R
inst_3 : IsOrderedRing R
x y : R
h : Eq (α := ArchimedeanClass R) (mk x) (mk y)
hx : x ≠ 0
hy : y ≠ 0
hx' : Ne (α := ArchimedeanClass R) (mk x) ⊤
⊢ HAdd.hAdd (α := ArchimedeanClass R) (mk x) ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) x) =
    HAdd.hAdd (α := ArchimedeanClass R) (mk y) ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) y)

Tactic:
simp [← mk_mul, hx, hy]

Premises used: ArchimedeanClass.mk_mul
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : Field R
inst_2 : IsOrderedRing R
x : R
⊢ Eq (α := ArchimedeanClass R) (mk x⁻¹) (-mk x)

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 : Field R
inst_3 : IsOrderedRing R
n : ℤ
x y : R
h : Eq (α := ArchimedeanClass R) (mk x) (mk y)
inl :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x : R) ↦ (mk (HPow.hPow (β := ℤ) x (↑n : ℤ)) : ArchimedeanClass R)) x)
      ((fun (x : R) ↦ (mk (HPow.hPow (β := ℤ) x (↑n : ℤ)) : ArchimedeanClass R)) y)
inr :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := ArchimedeanClass R)
      ((fun (x : R) ↦ (mk (HPow.hPow (β := ℤ) x (-(↑n : ℤ))) : ArchimedeanClass R)) x)
      ((fun (x : R) ↦ (mk (HPow.hPow (β := ℤ) x (-(↑n : ℤ))) : 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:
obtain ⟨n, rfl | rfl⟩ := n.eq_nat_or_neg

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : Field R
inst_3 : IsOrderedRing R
x y : R
h : Eq (α := ArchimedeanClass R) (mk x) (mk y)
n : ℕ
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x : R) ↦ (mk (HPow.hPow (β := ℤ) x (↑n : ℤ)) : ArchimedeanClass R)) x)
    ((fun (x : R) ↦ (mk (HPow.hPow (β := ℤ) x (↑n : ℤ)) : ArchimedeanClass R)) y)

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : Field R
inst_3 : IsOrderedRing R
x y : R
h : Eq (α := ArchimedeanClass R) (mk x) (mk y)
n : ℕ
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R)
    ((fun (x : R) ↦ (mk (HPow.hPow (β := ℤ) x (-(↑n : ℤ))) : ArchimedeanClass R)) x)
    ((fun (x : R) ↦ (mk (HPow.hPow (β := ℤ) x (-(↑n : ℤ))) : ArchimedeanClass R)) y)

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : Field R
inst_2 : IsOrderedRing R
n : ℤ
x : R
⊢ mk (x ^ n) = HSMul.hSMul (β := ArchimedeanClass R) n (mk x)

Tactic:
rfl

Premises used: ArchimedeanClass.lift, rfl, toAntisymmetrization, ArchimedeanClass.mk
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : Field R
inst_2 : IsOrderedRing R
n : ℕ
x : ArchimedeanClass R
mk :
  ∀ (x : R),
    HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n.succ : ℤ) (ArchimedeanClass.mk x) =
      HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n : ℤ) (ArchimedeanClass.mk x) + ArchimedeanClass.mk x
⊢ HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) x = HSMul.hSMul (α := ℤ) (↑n : ℤ) 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 : Field R
inst_2 : IsOrderedRing R
n : ℕ
x : R
mk :
  ArchimedeanClass.mk (x ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n : ℤ) (ArchimedeanClass.mk x) + ArchimedeanClass.mk x
⊢ HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n.succ : ℤ) (ArchimedeanClass.mk x) =
    HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n : ℤ) (ArchimedeanClass.mk x) + ArchimedeanClass.mk x

Tactic:
rw [← mk_zpow, Nat.cast_succ]

Premises used: Nat.cast_succ, ArchimedeanClass.mk_zpow
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : Field R
inst_2 : IsOrderedRing R
n : ℕ
x : R
mk :
  ArchimedeanClass.mk (HPow.hPow (α := R) 0 (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n : ℤ) (ArchimedeanClass.mk 0) + ArchimedeanClass.mk 0
mk₁ :
  ∀ (hx : x ≠ 0),
    ArchimedeanClass.mk (x ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
      HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n : ℤ) (ArchimedeanClass.mk x) + ArchimedeanClass.mk x
⊢ ArchimedeanClass.mk (x ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n : ℤ) (ArchimedeanClass.mk x) + ArchimedeanClass.mk x

Tactic:
obtain rfl | hx := eq_or_ne x 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 : Field R
inst_2 : IsOrderedRing R
n : ℕ
⊢ mk (HPow.hPow (α := R) 0 (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n : ℤ) (mk 0) + mk 0

Tactic:
simp [zero_zpow _ n.cast_add_one_ne_zero]

Premises used: zero_zpow, Nat.cast_add_one_ne_zero
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : Field R
inst_2 : IsOrderedRing R
n : ℕ
x : R
hx : x ≠ 0
mk :
  ArchimedeanClass.mk (HPow.hPow (β := ℤ) x (↑n : ℤ) * x) =
    HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n : ℤ) (ArchimedeanClass.mk x) + ArchimedeanClass.mk x
mk₁ :
  HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk (HPow.hPow (β := ℤ) 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
⊢ ArchimedeanClass.mk (x ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n : ℤ) (ArchimedeanClass.mk x) + ArchimedeanClass.mk x

Tactic:
rw [zpow_add_one₀ hx, mk_mul, mk_zpow]

Premises used: zpow_add_one₀, ArchimedeanClass.mk_mul, ArchimedeanClass.mk_zpow
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : Field R
inst_3 : IsOrderedRing 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_zpow, zpow_zero, mk_one]

Premises used: zpow_zero, ArchimedeanClass.mk_one, ArchimedeanClass.mk_zpow
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : Field R
inst_3 : IsOrderedRing 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_zpow, zpow_zero, mk_one]

Premises used: zpow_zero, ArchimedeanClass.mk_one, ArchimedeanClass.mk, ArchimedeanClass.mk_zpow
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : Field R
inst_3 : IsOrderedRing R
⊢ ∀ (n : ℕ) (a : ArchimedeanClass R), HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a = HSMul.hSMul (α := ℤ) (↑n : ℤ) a + a

Tactic:
zsmul_succ'

Premises used: _private.0.ArchimedeanClass.zsmul_succ'
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : Field R
inst_3 : IsOrderedRing R
⊢ ∀ (n : ℕ) (a : ArchimedeanClass R), HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a = HSMul.hSMul (α := ℤ) (↑n : ℤ) a + a

Tactic:
exact zsmul_succ'

Premises used: _private.0.ArchimedeanClass.zsmul_succ'
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : Field R
inst_3 : IsOrderedRing R
n : ℕ
x : ArchimedeanClass R
mk :
  ∀ (x : R),
    HSMul.hSMul (β := ArchimedeanClass R) (Int.negSucc n) (ArchimedeanClass.mk x) =
      -HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n.succ : ℤ) (ArchimedeanClass.mk x)
⊢ Int.negSucc n • x = -HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) 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 : Field R
inst_3 : IsOrderedRing R
n : ℕ
x : R
mk :
  ArchimedeanClass.mk (x ^ Int.negSucc n) =
    -HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n.succ : ℤ) (ArchimedeanClass.mk x)
mk₁ :
  ArchimedeanClass.mk (x ^ (n + 1))⁻¹ =
    -HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n.succ : ℤ) (ArchimedeanClass.mk x)
mk₂ :
  ArchimedeanClass.mk (x ^ n * x)⁻¹ =
    -HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n.succ : ℤ) (ArchimedeanClass.mk x)
mk₃ :
  ArchimedeanClass.mk (x ^ n * x)⁻¹ =
    -(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₆ :
  -HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk (HPow.hPow (β := ℤ) 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) (Int.negSucc n) (ArchimedeanClass.mk x) =
    -HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n.succ : ℤ) (ArchimedeanClass.mk x)

Tactic:
rw [← mk_zpow, zpow_negSucc, pow_succ, zsmul_succ', mk_inv, mk_mul, ← zpow_natCast, mk_zpow]

Premises used: zpow_natCast, zpow_negSucc, pow_succ, _private.0.ArchimedeanClass.zsmul_succ', ArchimedeanClass.mk_mul, ArchimedeanClass.mk_inv, ArchimedeanClass.mk_zpow
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : Field R
inst_3 : IsOrderedRing R
⊢ ∀ (x : ArchimedeanClass R), ⊤ + x = ⊤

Tactic:
simp