awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
a b : α
⊢ |a| ∣ b ↔ a ∣ b
have inl : ∀ (h : |a| = a), |a| ∣ b ↔ a ∣ b
Tactic: rcases abs_choice a with h | h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
a b : α
inl : ∀ (h : |a| = a), |a| ∣ b ↔ a ∣ b
⊢ |a| ∣ b ↔ a ∣ b
have inr : ∀ (h : |a| = -a), |a| ∣ b ↔ a ∣ b
Tactic: rcases abs_choice a with h | h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
a b : α
⊢ a ∣ |b| ↔ a ∣ b
have inl : ∀ (h : |b| = b), a ∣ |b| ↔ a ∣ b
Tactic: rcases abs_choice b with h | h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
a b : α
inl : ∀ (h : |b| = b), a ∣ |b| ↔ a ∣ b
⊢ a ∣ |b| ↔ a ∣ b
have inr : ∀ (h : |b| = -b), a ∣ |b| ↔ a ∣ b
Tactic: rcases abs_choice b with h | h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
n : ℕ
⊢ a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n
have inl : HPow.hPow (β := ℕ) a 0 = HPow.hPow (β := ℕ) b 0 ↔ Eq (α := ℕ) 0 0 ∨ a = b ∨ a = -b ∧ Even (α := ℕ) 0
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
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
⊢ a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n
have inr : ∀ (hn : n ≠ 0), a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n
Tactic: rcases eq_or_ne n 0 with rfl | 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₁ y₁ x₂ y₂ : R
hx : LE.le (α := ArchimedeanClass R) (mk x₁) (mk x₂)
hy : LE.le (α := ArchimedeanClass R) (mk y₁) (mk y₂)
⊢ LE.le (α := ArchimedeanClass R) (mk (x₁ * y₁)) (mk (x₂ * y₂))
have 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₂))
Tactic: obtain ⟨m, hm⟩ := 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₁ 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)
⊢ LE.le (α := ArchimedeanClass R) (mk (x₁ * y₁)) (mk (x₂ * y₂))
have 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₂))
Tactic: obtain ⟨n, hn⟩ := hy
Cleared hypotheses: hy
-- 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₁ 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)
⊢ LE.le (α := ArchimedeanClass R) (mk (x₁ * y₁)) (mk (x₂ * y₂))
have 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)
Tactic: use m * 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₁ 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)
⊢ |(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)
have 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)
Tactic: convert! mul_le_mul hm hn (abs_nonneg _) (nsmul_nonneg (abs_nonneg _) _) using 1
-- 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₁ 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)
⊢ |(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)
have 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)
Tactic: convert! mul_le_mul hm hn (abs_nonneg _) (nsmul_nonneg (abs_nonneg _) _) using 1
-- 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₁ 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)
⊢ |(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)
have h : |x₂ * y₂| = |x₂| * |y₂|
Tactic: simp_rw [ArchimedeanOrder.val_of, abs_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₁ 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)
⊢ 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)
have h : (m * n) • (|x₁| * |y₁|) = m • |x₁| * n • |y₁|
Tactic: simp_rw [ArchimedeanOrder.val_of, abs_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 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)))
⊢ 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)
have succ₂ : Eq (α := ArchimedeanClass R) (mk (x ^ n * x)) (mk (y ^ n * y))
Tactic: simp_rw [pow_succ, mk_mul, IH, 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
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))
⊢ 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)
have succ₃ : HAdd.hAdd (α := ArchimedeanClass R) (mk (x ^ n)) (mk x) = HAdd.hAdd (α := ArchimedeanClass R) (mk (y ^ n)) (mk y)
Tactic: simp_rw [pow_succ, mk_mul, IH, 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
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)
⊢ 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)
have succ₄ : HAdd.hAdd (α := ArchimedeanClass R) (mk (y ^ n)) (mk x) = HAdd.hAdd (α := ArchimedeanClass R) (mk (y ^ n)) (mk y)
Tactic: simp_rw [pow_succ, mk_mul, IH, 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
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 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)
Tactic: induction n with
    | zero => simp
    | succ n IH => simp_rw [pow_succ, mk_mul, IH, h]
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 : 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)
⊢ 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 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)
Tactic: induction n with
    | zero => simp
    | succ n IH => simp_rw [pow_succ, mk_mul, IH, h]
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 : CommRing R
inst_3 : IsStrictOrderedRing R
x y : ArchimedeanClass R
⊢ x + y = y + x
have mk : ∀ (x : R), mk x + y = y + 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
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : IsStrictOrderedRing R
y : ArchimedeanClass R
x : R
⊢ mk x + y = y + mk x
have mk : ∀ (y : R), HAdd.hAdd (α := ArchimedeanClass R) (mk x) (mk y) = HAdd.hAdd (α := ArchimedeanClass R) (mk y) (mk x)
Tactic: induction y with | mk y
Cleared hypotheses: y
-- 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
⊢ HAdd.hAdd (α := ArchimedeanClass R) (mk x) (mk y) = HAdd.hAdd (α := ArchimedeanClass R) (mk y) (mk x)
have mk : mk (x * y) = HAdd.hAdd (α := ArchimedeanClass R) (mk y) (mk x)
Tactic: rw [← mk_mul, mul_comm, mk_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 y : R
mk : ArchimedeanClass.mk (x * y) = HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk y) (ArchimedeanClass.mk x)
⊢ HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk x) (ArchimedeanClass.mk y) =
    HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk y) (ArchimedeanClass.mk x)
have mk₁ : ArchimedeanClass.mk (y * x) = HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk y) (ArchimedeanClass.mk x)
Tactic: rw [← mk_mul, mul_comm, mk_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 y : R
mk : ArchimedeanClass.mk (x * y) = HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk y) (ArchimedeanClass.mk x)
mk₁ : ArchimedeanClass.mk (y * x) = HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk y) (ArchimedeanClass.mk x)
⊢ HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk x) (ArchimedeanClass.mk y) =
    HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk y) (ArchimedeanClass.mk x)
have mk₂ : HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk y) (ArchimedeanClass.mk x) =
  HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk y) (ArchimedeanClass.mk x)
Tactic: rw [← mk_mul, mul_comm, 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 : ArchimedeanClass R
⊢ 0 + x = x
have mk : ∀ (x : R), HAdd.hAdd (α := ArchimedeanClass R) 0 (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 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
⊢ HAdd.hAdd (α := ArchimedeanClass R) 0 (mk x) = mk x
have mk : HAdd.hAdd (α := ArchimedeanClass R) (mk 1) (mk x) = mk x
Tactic: rw [← mk_one, ← mk_mul, one_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
mk : HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk 1) (ArchimedeanClass.mk x) = ArchimedeanClass.mk x
⊢ HAdd.hAdd (α := ArchimedeanClass R) 0 (ArchimedeanClass.mk x) = ArchimedeanClass.mk x
have mk₁ : Eq (α := ArchimedeanClass R) (ArchimedeanClass.mk (1 * x)) (ArchimedeanClass.mk x)
Tactic: rw [← mk_one, ← mk_mul, one_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
mk : HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk 1) (ArchimedeanClass.mk x) = ArchimedeanClass.mk x
mk₁ : Eq (α := ArchimedeanClass R) (ArchimedeanClass.mk (1 * x)) (ArchimedeanClass.mk x)
⊢ HAdd.hAdd (α := ArchimedeanClass R) 0 (ArchimedeanClass.mk x) = ArchimedeanClass.mk x
have mk₂ : Eq (α := ArchimedeanClass R) (ArchimedeanClass.mk x) (ArchimedeanClass.mk x)
Tactic: rw [← mk_one, ← mk_mul, one_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 y z : ArchimedeanClass R
⊢ x + y + z = x + (y + z)
have mk : ∀ (x : R), mk x + y + z = mk x + (y + z)
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 : CommRing R
inst_2 : IsStrictOrderedRing R
y z : ArchimedeanClass R
x : R
⊢ mk x + y + z = mk x + (y + z)
have mk : ∀ (y : R), HAdd.hAdd (α := ArchimedeanClass R) (mk x) (mk y) + z = mk x + (mk y + z)
Tactic: induction y with | mk y
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
z : ArchimedeanClass R
x y : R
⊢ HAdd.hAdd (α := ArchimedeanClass R) (mk x) (mk y) + z = mk x + (mk y + z)
have mk : ∀ (z : R),
  HAdd.hAdd (α := ArchimedeanClass R) (mk x) (mk y) + mk z = mk x + 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
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x y z : R
⊢ HAdd.hAdd (α := ArchimedeanClass R) (mk x) (mk y) + mk z = mk x + HAdd.hAdd (α := ArchimedeanClass R) (mk y) (mk z)
have mk : Eq (α := ArchimedeanClass R) (mk (x * y * z)) (mk (x * (y * z)))
Tactic: simp_rw [← mk_mul, mul_assoc]
-- 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
⊢ HSMul.hSMul (α := ℕ) (β := ArchimedeanClass R) 0 (mk x) = 0
have mk : Eq (α := ArchimedeanClass R) (mk (HPow.hPow (β := ℕ) x 0)) 0
Tactic: rw [← mk_pow, pow_zero, mk_one]
-- 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 : Eq (α := ArchimedeanClass R) (ArchimedeanClass.mk (HPow.hPow (β := ℕ) x 0)) 0
⊢ HSMul.hSMul (α := ℕ) (β := ArchimedeanClass R) 0 (ArchimedeanClass.mk x) = 0
have mk₁ : Eq.{u_1 + 1} (α := ArchimedeanClass R) (ArchimedeanClass.mk 1) 0
Tactic: rw [← mk_pow, pow_zero, mk_one]
-- 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 : Eq (α := ArchimedeanClass R) (ArchimedeanClass.mk (HPow.hPow (β := ℕ) x 0)) 0
mk₁ : Eq.{u_1 + 1} (α := ArchimedeanClass R) (ArchimedeanClass.mk 1) 0
⊢ HSMul.hSMul (α := ℕ) (β := ArchimedeanClass R) 0 (ArchimedeanClass.mk x) = 0
have mk₂ : Eq.{u_1 + 1} (α := ArchimedeanClass R) 0 0
Tactic: rw [← mk_pow, pow_zero, mk_one]