awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x : ArchimedeanClass R
⊢ HSMul.hSMul (α := ℕ) 0 x = 0
have mk : ∀ (x : R), HSMul.hSMul (α := ℕ) (β := ArchimedeanClass R) 0 (mk x) = 0
Tactic: induction x with | mk x => rw [← mk_pow, pow_zero, mk_one]
Cleared hypotheses: x
-- 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
n : ℕ
x : R
⊢ HSMul.hSMul (β := ArchimedeanClass R) (n + 1) (mk x) = HSMul.hSMul (β := ArchimedeanClass R) n (mk x) + mk x
have mk : mk (x ^ (n + 1)) = HSMul.hSMul (β := ArchimedeanClass R) n (mk x) + mk x
Tactic: rw [← mk_pow, pow_succ, mk_mul, mk_pow]
-- 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
n : ℕ
x : R
mk :
  ArchimedeanClass.mk (x ^ (n + 1)) =
    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
have mk₁ : ArchimedeanClass.mk (x ^ n * x) =
  HSMul.hSMul (β := ArchimedeanClass R) n (ArchimedeanClass.mk x) + ArchimedeanClass.mk x
Tactic: rw [← mk_pow, pow_succ, mk_mul, mk_pow]
-- 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
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
⊢ HSMul.hSMul (β := ArchimedeanClass R) (n + 1) (ArchimedeanClass.mk x) =
    HSMul.hSMul (β := ArchimedeanClass R) n (ArchimedeanClass.mk x) + ArchimedeanClass.mk x
have mk₂ : HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk (x ^ n)) (ArchimedeanClass.mk x) =
  HSMul.hSMul (β := ArchimedeanClass R) n (ArchimedeanClass.mk x) + ArchimedeanClass.mk x
Tactic: rw [← mk_pow, pow_succ, mk_mul, mk_pow]
-- 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
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
⊢ HSMul.hSMul (β := ArchimedeanClass R) (n + 1) (ArchimedeanClass.mk x) =
    HSMul.hSMul (β := ArchimedeanClass R) n (ArchimedeanClass.mk x) + ArchimedeanClass.mk x
have mk₃ : HSMul.hSMul (β := ArchimedeanClass R) n (ArchimedeanClass.mk x) + ArchimedeanClass.mk x =
  HSMul.hSMul (β := ArchimedeanClass R) n (ArchimedeanClass.mk x) + ArchimedeanClass.mk x
Tactic: rw [← mk_pow, pow_succ, mk_mul, mk_pow]
-- 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
n : ℕ
x : ArchimedeanClass R
⊢ (n + 1) • x = n • x + x
have mk : ∀ (x : R), HSMul.hSMul (β := ArchimedeanClass R) (n + 1) (mk x) = HSMul.hSMul (β := ArchimedeanClass R) n (mk x) + mk x
Tactic: induction x with | mk x => rw [← mk_pow, pow_succ, mk_mul, mk_pow]
Cleared hypotheses: x
-- 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
x y : ArchimedeanClass R
h : x ≤ y
z : ArchimedeanClass R
⊢ x + z ≤ y + z
have mk : ∀ (x : R) (h : mk x ≤ y), mk x + z ≤ y + z
Tactic: induction x with | mk x
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 : CommRing R
inst_3 : IsStrictOrderedRing R
y z : ArchimedeanClass R
x : R
h : mk x ≤ y
⊢ mk x + z ≤ y + z
have mk : ∀ (y : R) (h : LE.le (α := ArchimedeanClass R) (mk x) (mk y)), mk x + z ≤ mk y + z
Tactic: induction y with | mk y
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 : CommRing R
inst_3 : IsStrictOrderedRing R
z : ArchimedeanClass R
x y : R
h : LE.le (α := ArchimedeanClass R) (mk x) (mk y)
⊢ mk x + z ≤ mk y + z
have mk : ∀ (z : R), HAdd.hAdd (α := ArchimedeanClass R) (mk x) (mk z) ≤ HAdd.hAdd (α := ArchimedeanClass R) (mk y) (mk z)
Tactic: induction z with | mk z
Cleared hypotheses: z
-- 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
x y : R
h : LE.le (α := ArchimedeanClass R) (mk x) (mk y)
z : R
⊢ HAdd.hAdd (α := ArchimedeanClass R) (mk x) (mk z) ≤ HAdd.hAdd (α := ArchimedeanClass R) (mk y) (mk z)
have mk : LE.le (α := ArchimedeanClass R) (mk (x * z)) (mk (y * z))
Tactic: rw [← mk_mul, ← mk_mul]
-- 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 : x ≠ 0
⊢ IsAddRegular (R := ArchimedeanClass R) (mk x)
have rw : IsAddLeftRegular (R := ArchimedeanClass R) (mk x)
Tactic: rw [← isAddLeftRegular_iff_isAddRegular]
-- 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 : x ≠ 0
z : ArchimedeanClass R
y : 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) z)
⊢ mk y = z
have mk : ∀ (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: induction z with | mk z =>
  simpa [← mk_mul, mk_eq_mk, mul_left_comm _ (|x|), abs_pos.2 hx] using hyz
Cleared hypotheses: z, hyz
-- 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 : x ≠ 0
y z : ArchimedeanClass R
hyz :
  Eq.{u_1 + 1} (α := ArchimedeanClass R) ((fun (x_1 : ArchimedeanClass R) ↦ mk x + x_1) y)
    ((fun (x_1 : ArchimedeanClass R) ↦ mk x + x_1) z)
⊢ y = z
have mk : ∀ (y : 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) z)),
  mk 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
Cleared hypotheses: y, hyz
-- 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
x : R
⊢ HAdd.hAdd (α := ArchimedeanClass R) ⊤ (mk x) = ⊤
have mk : HAdd.hAdd (α := ArchimedeanClass R) (mk 0) (mk x) = mk 0
Tactic: rw [← mk_zero, ← mk_mul, zero_mul]
-- 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
x : R
mk : HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk 0) (ArchimedeanClass.mk x) = ArchimedeanClass.mk 0
⊢ HAdd.hAdd (α := ArchimedeanClass R) ⊤ (ArchimedeanClass.mk x) = ⊤
have mk₁ : Eq (α := ArchimedeanClass R) (ArchimedeanClass.mk (0 * x)) (ArchimedeanClass.mk 0)
Tactic: rw [← mk_zero, ← mk_mul, zero_mul]
-- 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
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)
⊢ HAdd.hAdd (α := ArchimedeanClass R) ⊤ (ArchimedeanClass.mk x) = ⊤
have mk₂ : Eq.{u_1 + 1} (α := ArchimedeanClass R) (ArchimedeanClass.mk 0) (ArchimedeanClass.mk 0)
Tactic: rw [← mk_zero, ← mk_mul, zero_mul]
-- 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
x : ArchimedeanClass R
⊢ ⊤ + x = ⊤
have mk : ∀ (x : R), HAdd.hAdd (α := ArchimedeanClass R) ⊤ (mk x) = ⊤
Tactic: induction x with | mk x => rw [← mk_zero, ← mk_mul, zero_mul]
Cleared hypotheses: x
-- 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
x : ArchimedeanClass R
⊢ x ≠ ⊤ → IsAddLeftRegular x
have mk : ∀ (x : R), Ne (α := ArchimedeanClass R) (mk x) ⊤ → IsAddLeftRegular (R := ArchimedeanClass R) (mk x)
Tactic: induction x with | mk x => simp +contextual [isAddRegular_mk]
Cleared hypotheses: x
-- 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
f : S →+o 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)
have 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)
Tactic: rw [← mk_one, orderHom_mk]
-- 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
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)
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R)
    ((orderHom f : (a : ArchimedeanClass S) → ArchimedeanClass R) 0 : ArchimedeanClass R)
    (mk ((f : (a : S) → R) 1) : ArchimedeanClass R)
have rw₁ : Eq.{u_1 + 1} (α := ArchimedeanClass R) (mk ((f : (a : S) → R) 1) : ArchimedeanClass R)
  (mk ((f : (a : S) → R) 1) : ArchimedeanClass R)
Tactic: rw [← mk_one, orderHom_mk]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
Goal:
S : Type u_3
inst : LinearOrder S
inst_1 : CommRing S
inst_2 : IsStrictOrderedRing S
inst_3 : Archimedean S
x : ArchimedeanClass S
⊢ x = 0 ∨ x = ⊤
have mk : ∀ (x : S), Eq (α := ArchimedeanClass S) (mk x) 0 ∨ Eq (α := ArchimedeanClass S) (mk x) ⊤
Tactic: induction x with | mk x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
Goal:
S : Type u_3
inst : LinearOrder S
inst_1 : CommRing S
inst_2 : IsStrictOrderedRing S
inst_3 : Archimedean S
x : S
⊢ Eq (α := ArchimedeanClass S) (mk x) 0 ∨ Eq (α := ArchimedeanClass S) (mk x) ⊤
have mk : Eq.{u_3 + 1} (α := ArchimedeanClass S) (mk 0) 0 ∨ Eq.{u_3 + 1} (α := ArchimedeanClass S) (mk 0) ⊤
Tactic: obtain rfl | h := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
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) ⊤
⊢ Eq (α := ArchimedeanClass S) (ArchimedeanClass.mk x) 0 ∨ Eq (α := ArchimedeanClass S) (ArchimedeanClass.mk x) ⊤
have mk₁ : ∀ (h : x ≠ 0),
  Eq (α := ArchimedeanClass S) (ArchimedeanClass.mk x) 0 ∨ Eq (α := ArchimedeanClass S) (ArchimedeanClass.mk x) ⊤
Tactic: obtain rfl | h := 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 : 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)
    (mk ((f : (a : S) → R) 1) : ArchimedeanClass R)
have 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)
Tactic: rw [← orderHom_mk, mk_eq_zero_of_archimedean h, orderHom_zero]
-- 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 : 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)
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R) (mk ((f : (a : S) → R) x) : ArchimedeanClass R)
    (mk ((f : (a : S) → R) 1) : ArchimedeanClass R)
have 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)
Tactic: rw [← orderHom_mk, mk_eq_zero_of_archimedean h, orderHom_zero]
-- 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 : 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)
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R) (mk ((f : (a : S) → R) x) : ArchimedeanClass R)
    (mk ((f : (a : S) → R) 1) : ArchimedeanClass R)
have rw₂ : Eq.{u_1 + 1} (α := ArchimedeanClass R) (mk ((f : (a : S) → R) 1) : ArchimedeanClass R)
  (mk ((f : (a : S) → R) 1) : ArchimedeanClass R)
Tactic: rw [← orderHom_mk, mk_eq_zero_of_archimedean h, orderHom_zero]
-- 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
y : S
⊢ mk x ≤
    HAdd.hAdd (α := ArchimedeanClass R) (β := ArchimedeanClass R) (mk ((f : (a : S) → R) y) : ArchimedeanClass R) (mk x)
have inl : mk x ≤
  HAdd.hAdd (α := ArchimedeanClass R) (β := ArchimedeanClass R) (mk ((f : (a : S) → R) 0) : ArchimedeanClass R) (mk x)
Tactic: obtain rfl | hy := eq_or_ne y 0
Cleared hypotheses: y
-- 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
y : S
inl :
  mk x ≤
    HAdd.hAdd (α := ArchimedeanClass R) (β := ArchimedeanClass R) (mk ((f : (a : S) → R) 0) : ArchimedeanClass R) (mk x)
⊢ mk x ≤
    HAdd.hAdd (α := ArchimedeanClass R) (β := ArchimedeanClass R) (mk ((f : (a : S) → R) y) : ArchimedeanClass R) (mk x)
have inr : ∀ (hy : y ≠ 0),
  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
-- 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
y : S
hy : y ≠ 0
⊢ mk x ≤
    HAdd.hAdd (α := ArchimedeanClass R) (β := ArchimedeanClass R) (mk ((f : (a : S) → R) y) : ArchimedeanClass R) (mk x)
have inr : mk x ≤ HAdd.hAdd (α := ArchimedeanClass R) 0 (mk x)
Tactic: rw [mk_map_of_archimedean' f hy, zero_add]
-- 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
y : S
hy : y ≠ 0
inr : mk x ≤ HAdd.hAdd (α := ArchimedeanClass R) 0 (mk x)
⊢ mk x ≤
    HAdd.hAdd (α := ArchimedeanClass R) (β := ArchimedeanClass R) (mk ((f : (a : S) → R) y) : ArchimedeanClass R) (mk x)
have inr₁ : LE.le (α := ArchimedeanClass R) (mk x) (mk x)
Tactic: rw [mk_map_of_archimedean' f hy, zero_add]
-- 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
y : S
⊢ mk x ≤
    HAdd.hAdd (α := ArchimedeanClass R) (β := ArchimedeanClass R) (mk x) (mk ((f : (a : S) → R) y) : ArchimedeanClass R)
have rw : mk x ≤
  HAdd.hAdd (α := ArchimedeanClass R) (β := ArchimedeanClass R) (mk ((f : (a : S) → R) y) : ArchimedeanClass R) (mk x)
Tactic: rw [add_comm]
-- 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
hx : LT.lt (α := ArchimedeanClass R) 0 (mk x)
y : S
hy : 0 < y
⊢ x < (f : (a : S) → R) y
have h : LT.lt.{u_1} (α := ArchimedeanClass R) (mk ((f : (a : S) → R) y) : ArchimedeanClass R) (mk x : ArchimedeanClass R)
Tactic: apply lt_of_mk_lt_mk_of_nonneg
-- 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
hx : LT.lt (α := ArchimedeanClass R) 0 (mk x)
y : S
hy : 0 < y
h : LT.lt.{u_1} (α := ArchimedeanClass R) (mk ((f : (a : S) → R) y) : ArchimedeanClass R) (mk x : ArchimedeanClass R)
⊢ x < (f : (a : S) → R) y
have hpos : LE.le.{u_1} (α := R) (0 : R) ((f : (a : S) → R) y : R)
Tactic: apply lt_of_mk_lt_mk_of_nonneg
-- 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
hx : LT.lt (α := ArchimedeanClass R) 0 (mk x)
y : S
hy : y < 0
⊢ (f : (a : S) → R) y < x
have h : LT.lt.{u_1} (α := ArchimedeanClass R) (mk ((f : (a : S) → R) y) : ArchimedeanClass R) (mk x : ArchimedeanClass R)
Tactic: apply lt_of_mk_lt_mk_of_nonpos
-- 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
hx : LT.lt (α := ArchimedeanClass R) 0 (mk x)
y : S
hy : y < 0
h : LT.lt.{u_1} (α := ArchimedeanClass R) (mk ((f : (a : S) → R) y) : ArchimedeanClass R) (mk x : ArchimedeanClass R)
⊢ (f : (a : S) → R) y < x
have hneg : LE.le.{u_1} (α := R) ((f : (a : S) → R) y : R) (0 : R)
Tactic: apply lt_of_mk_lt_mk_of_nonpos
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
Goal:
S : Type u_3
inst : LinearOrder S
inst_1 : CommRing S
inst_2 : IsStrictOrderedRing S
n : ℤ
h : n ≠ 0
⊢ Eq.{u_3 + 1} (α := ArchimedeanClass S) (mk (↑n : S)) 0
have inl : Subsingleton S → Eq.{u_3 + 1} (α := ArchimedeanClass S) (mk (↑n : S)) 0
Tactic: obtain _ | _ := subsingleton_or_nontrivial S
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
Goal:
S : Type u_3
inst : LinearOrder S
inst_1 : CommRing S
inst_2 : IsStrictOrderedRing S
n : ℤ
h : n ≠ 0
inl : Subsingleton S → Eq.{u_3 + 1} (α := ArchimedeanClass S) (mk (↑n : S)) 0
⊢ Eq.{u_3 + 1} (α := ArchimedeanClass S) (mk (↑n : S)) 0
have inr : Nontrivial S → Eq.{u_3 + 1} (α := ArchimedeanClass S) (mk (↑n : S)) 0
Tactic: obtain _ | _ := subsingleton_or_nontrivial S
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
Goal:
S : Type u_3
inst : LinearOrder S
inst_1 : CommRing S
inst_2 : IsStrictOrderedRing S
n : ℤ
⊢ LE.le.{u_3} (α := ArchimedeanClass S) 0 (mk (↑n : S))
have inl : LE.le.{u_3} (α := ArchimedeanClass S) 0 (mk (↑0 : S))
Tactic: obtain rfl | hn := eq_or_ne n 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
Goal:
S : Type u_3
inst : LinearOrder S
inst_1 : CommRing S
inst_2 : IsStrictOrderedRing S
n : ℤ
inl : LE.le.{u_3} (α := ArchimedeanClass S) 0 (mk (↑0 : S))
⊢ LE.le.{u_3} (α := ArchimedeanClass S) 0 (mk (↑n : S))
have inr : ∀ (hn : n ≠ 0), LE.le.{u_3} (α := ArchimedeanClass S) 0 (mk (↑n : S))
Tactic: obtain rfl | hn := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Archimedean (goal)
Goal:
S : Type u_3
inst : LinearOrder S
inst_1 : CommRing S
inst_2 : IsStrictOrderedRing S
n : ℤ
hn : n ≠ 0
⊢ LE.le.{u_3} (α := ArchimedeanClass S) 0 (mk (↑n : S))
have inr : LE.le.{u_3} (α := ArchimedeanClass S) 0 0
Tactic: rw [mk_intCast hn]
-- 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 :
    |(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
          ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x : ArchimedeanOrder R)| ≤
      HSMul.hSMul (β := R) n
        (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
              ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) 1 : ArchimedeanOrder R)| :
          R)),
  ∃ (n : ℕ), x ≤ (↑n : R)
Tactic: obtain ⟨n, hn⟩ := hx
Cleared hypotheses: 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
n : ℕ
hn :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
        ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x : ArchimedeanOrder R)| ≤
    HSMul.hSMul (β := R) n
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) 1 : ArchimedeanOrder R)| :
        R)
⊢ ∃ (n : ℕ), x ≤ (↑n : R)
have refine : |x| ≤ (↑n : R)
Tactic: refine ⟨n, le_of_abs_le ?_⟩