awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : LE.le (α := ArchimedeanClass R) 0 (mk x)
⊢ ∃ (n : ℕ), x < (↑n : R)
have obtain : ∀ (n : ℕ) (hn : x ≤ (↑n : R)), ∃ (n : ℕ), x < (↑n : R)
Tactic: obtain ⟨n, hn⟩ := exists_nat_ge_of_mk_nonneg hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : LE.le (α := ArchimedeanClass R) 0 (mk x)
n : ℕ
hn : x ≤ (↑n : R)
⊢ ∃ (n : ℕ), x < (↑n : R)
have refine : LT.lt.{u_1} (α := R) (↑n : R) (↑(n + 1) : R)
Tactic: refine ⟨n + 1, hn.trans_lt ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : LE.le (α := ArchimedeanClass R) 0 (mk x)
⊢ ∃ (n : ℤ), x ≤ (↑n : R)
have obtain : ∀ (n : ℕ) (hn : x ≤ (↑n : R)), ∃ (n : ℤ), x ≤ (↑n : R)
Tactic: obtain ⟨n, hn⟩ := exists_nat_ge_of_mk_nonneg hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : LE.le (α := ArchimedeanClass R) 0 (mk x)
⊢ ∃ (n : ℤ), x < (↑n : R)
have obtain : ∀ (n : ℕ) (hn : x < (↑n : R)), ∃ (n : ℤ), x < (↑n : R)
Tactic: obtain ⟨n, hn⟩ := exists_nat_gt_of_mk_nonneg hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : LE.le (α := ArchimedeanClass R) 0 (mk x)
⊢ ∃ (n : ℤ), (↑n : R) ≤ x
have obtain : ∀ (n : ℕ) (hn : -x ≤ (↑n : R)), ∃ (n : ℤ), (↑n : R) ≤ x
Tactic: obtain ⟨n, hn⟩ := exists_nat_ge_of_mk_nonneg (mk_neg x ▸ hx)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : LE.le (α := ArchimedeanClass R) 0 (mk x)
n : ℕ
hn : -x ≤ (↑n : R)
⊢ ∃ (n : ℤ), (↑n : R) ≤ x
have h : (↑(-(↑n : ℤ)) : R) ≤ x
Tactic: use -n
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : LE.le (α := ArchimedeanClass R) 0 (mk x)
⊢ ∃ (n : ℤ), (↑n : R) < x
have obtain : ∀ (n : ℕ) (hn : -x < (↑n : R)), ∃ (n : ℤ), (↑n : R) < x
Tactic: obtain ⟨n, hn⟩ := exists_nat_gt_of_mk_nonneg (mk_neg x ▸ hx)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : LE.le (α := ArchimedeanClass R) 0 (mk x)
n : ℕ
hn : -x < (↑n : R)
⊢ ∃ (n : ℤ), (↑n : R) < x
have h : (↑(-(↑n : ℤ)) : R) < x
Tactic: use -n
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
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
r s : S
hr : (f : (a : S) → R) r ≤ x
hs : x ≤ (f : (a : S) → R) s
⊢ LE.le (α := ArchimedeanClass R) 0 (mk x)
have apply : LE.le.{u_1} (α := ArchimedeanClass R) (0 : ArchimedeanClass R)
  (min (mk ((f : (a : S) → R) r)) (mk ((f : (a : S) → R) s)) : ArchimedeanClass R)
Tactic: apply (min_le_mk_of_le_of_le hr hs).trans'
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (hypothesis)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x y z : ArchimedeanClass R
hx : x ≠ ⊤
h : y + x = z + x
⊢ y = z
have h₁ : x + y = x + z
Tactic: simp_rw [← add_comm x] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (hypothesis)
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)
⊢ LE.le (α := ArchimedeanClass S) (mk x) (mk y) ↔
    ∃ (q : R),
      LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ∧ HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ |x|
have H : ∀ {q : R}, LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ↔ 0 < q
Tactic: have H {q} : 0 < f q ↔ 0 < q := by simpa using hf.lt_iff_lt (a := 0)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
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
⊢ LE.le (α := ArchimedeanClass S) (mk x) (mk y) ↔
    ∃ (q : R),
      LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ∧ HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ |x|
have mp : LE.le (α := ArchimedeanClass S) (mk x) (mk y) →
  ∃ (q : R),
    LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ∧ HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ |x|
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
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
mp :
  LE.le (α := ArchimedeanClass S) (mk x) (mk y) →
    ∃ (q : R),
      LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ∧ HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ |x|
⊢ LE.le (α := ArchimedeanClass S) (mk x) (mk y) ↔
    ∃ (q : R),
      LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ∧ HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ |x|
have mpr : (∃ (q : R),
    LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ∧ HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ |x|) →
  LE.le (α := ArchimedeanClass S) (mk x) (mk y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
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),
    LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ∧ HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ |x|
have mp : ∀ (q : R) (hq₀ : 0 < q) (hq : (n + 1) • q < 1),
  ∃ (q : R),
    LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ∧ HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ |x|
Tactic: obtain ⟨q, hq₀, hq⟩ := exists_nsmul_lt_of_pos (one_pos (α := R)) (n + 1)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
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
⊢ ∃ (q : R),
    LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ∧ HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ |x|
have mp : HAdd.hAdd (α := S) (↑n : S) 1 * HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ HAdd.hAdd (α := S) (↑n : S) 1 * |x|
Tactic: refine ⟨q, H.2 hq₀, le_of_mul_le_mul_left ?_ n.cast_add_one_pos⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (hypothesis)
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|
⊢ LE.le (α := ArchimedeanClass S) (mk x) (mk y)
have hq₀' : 0 < q
Tactic: have hq₀' := H.1 hq₀
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
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
⊢ LE.le (α := ArchimedeanClass S) (mk x) (mk y)
have mpr : ∀ (n : ℕ) (hn : 1 < n • q), LE.le (α := ArchimedeanClass S) (mk x) (mk y)
Tactic: obtain ⟨n, hn⟩ := exists_lt_nsmul hq₀' 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
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)
have 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))
Tactic: refine ⟨n, le_of_mul_le_mul_left ?_ hq₀⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
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)
have rw : LE.le.{u_2} (α := S) ((f : (a : R) → S) 0 : S) ((f : (a : R) → S) (n • q) : S)
Tactic: rw [← f.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (hypothesis)
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
⊢ 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))
have h : 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)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
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)
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) x)
    ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) y)
have 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)
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
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)
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) x)
    ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) y)
have 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)
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
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
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) x)
    ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) y)
have 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)
Tactic: obtain rfl | hy := eq_or_ne y 0
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
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)
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) x)
    ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) y)
have 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)
Tactic: obtain rfl | hy := eq_or_ne y 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (hypothesis)
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
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) x)
    ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) y)
have hx' : Ne (α := ArchimedeanClass R) (mk x) ⊤
Tactic: have hx' : mk x ≠ ⊤ := by simpa using hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
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) ⊤
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) x)
    ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) y)
have 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)
Tactic: apply add_left_cancel_of_ne_top hx'
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
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 x) ((fun (x : R) ↦ (mk x⁻¹ : ArchimedeanClass R)) y)
have 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)
Tactic: nth_rw 2 [h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
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)
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x : R) ↦ (mk (x ^ n) : ArchimedeanClass R)) x)
    ((fun (x : R) ↦ (mk (x ^ n) : ArchimedeanClass R)) y)
have 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)
Tactic: obtain ⟨n, rfl | rfl⟩ := n.eq_nat_or_neg
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
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)
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x : R) ↦ (mk (x ^ n) : ArchimedeanClass R)) x)
    ((fun (x : R) ↦ (mk (x ^ n) : ArchimedeanClass R)) y)
have 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)
Tactic: obtain ⟨n, rfl | rfl⟩ := n.eq_nat_or_neg
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : Field R
inst_2 : IsOrderedRing R
n : ℕ
x : ArchimedeanClass R
⊢ HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) x = HSMul.hSMul (α := ℤ) (↑n : ℤ) x + x
have mk : ∀ (x : R),
  HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n.succ : ℤ) (mk x) =
    HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n : ℤ) (mk x) + mk x
Tactic: induction x with | mk x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : Field R
inst_2 : IsOrderedRing R
n : ℕ
x : R
⊢ HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n.succ : ℤ) (mk x) =
    HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n : ℤ) (mk x) + mk x
have mk : mk (x ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n : ℤ) (mk x) + mk x
Tactic: rw [← mk_zpow, Nat.cast_succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : Field R
inst_2 : IsOrderedRing R
n : ℕ
x : R
⊢ mk (x ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n : ℤ) (mk x) + mk x
have mk : mk (HPow.hPow (α := R) 0 (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
  HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n : ℤ) (mk 0) + mk 0
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
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
⊢ ArchimedeanClass.mk (x ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n : ℤ) (ArchimedeanClass.mk x) + ArchimedeanClass.mk x
have mk₁ : ∀ (hx : x ≠ 0),
  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
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : Field R
inst_2 : IsOrderedRing R
n : ℕ
x : R
hx : x ≠ 0
⊢ mk (x ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n : ℤ) (mk x) + mk x
have mk : mk (HPow.hPow (β := ℤ) x (↑n : ℤ) * x) = HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n : ℤ) (mk x) + mk x
Tactic: rw [zpow_add_one₀ hx, mk_mul, mk_zpow]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
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
⊢ ArchimedeanClass.mk (x ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n : ℤ) (ArchimedeanClass.mk x) + ArchimedeanClass.mk x
have 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
Tactic: rw [zpow_add_one₀ hx, mk_mul, mk_zpow]