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 : 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
⊢ ArchimedeanClass.mk (x ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    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 [zpow_add_one₀ hx, mk_mul, mk_zpow]
-- 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 : R
⊢ HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) 0 (mk x) = 0
have mk : Eq (α := ArchimedeanClass R) (mk (HPow.hPow (β := ℤ) x 0)) 0
Tactic: rw [← mk_zpow, zpow_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 : Field R
inst_3 : IsOrderedRing 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_zpow, zpow_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 : 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
⊢ HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) 0 (ArchimedeanClass.mk x) = 0
have mk₂ : Eq.{u_1 + 1} (α := ArchimedeanClass R) 0 0
Tactic: rw [← mk_zpow, zpow_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 : Field R
inst_3 : IsOrderedRing 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_zpow, zpow_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 : Field R
inst_3 : IsOrderedRing R
n : ℕ
x : ArchimedeanClass R
⊢ Int.negSucc n • x = -HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) x
have mk : ∀ (x : R),
  HSMul.hSMul (β := ArchimedeanClass R) (Int.negSucc n) (mk x) =
    -HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n.succ : ℤ) (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 : Field R
inst_3 : IsOrderedRing R
n : ℕ
x : R
⊢ HSMul.hSMul (β := ArchimedeanClass R) (Int.negSucc n) (mk x) =
    -HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n.succ : ℤ) (mk x)
have mk : mk (x ^ Int.negSucc n) = -HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n.succ : ℤ) (mk x)
Tactic: rw [← mk_zpow, zpow_negSucc, pow_succ, zsmul_succ', mk_inv, mk_mul, ← zpow_natCast, mk_zpow]
-- 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 : R
mk :
  ArchimedeanClass.mk (x ^ Int.negSucc n) =
    -HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n.succ : ℤ) (ArchimedeanClass.mk x)
⊢ HSMul.hSMul (β := ArchimedeanClass R) (Int.negSucc n) (ArchimedeanClass.mk x) =
    -HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n.succ : ℤ) (ArchimedeanClass.mk x)
have mk₁ : ArchimedeanClass.mk (x ^ (n + 1))⁻¹ =
  -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]
-- 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 : 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)
⊢ HSMul.hSMul (β := ArchimedeanClass R) (Int.negSucc n) (ArchimedeanClass.mk x) =
    -HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n.succ : ℤ) (ArchimedeanClass.mk x)
have mk₂ : ArchimedeanClass.mk (x ^ n * 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]
-- 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 : 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)
⊢ HSMul.hSMul (β := ArchimedeanClass R) (Int.negSucc n) (ArchimedeanClass.mk x) =
    -HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n.succ : ℤ) (ArchimedeanClass.mk x)
have mk₃ : ArchimedeanClass.mk (x ^ n * x)⁻¹ =
  -(HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n : ℤ) (ArchimedeanClass.mk x) + ArchimedeanClass.mk x)
Tactic: rw [← mk_zpow, zpow_negSucc, pow_succ, zsmul_succ', mk_inv, mk_mul, ← zpow_natCast, mk_zpow]
-- 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 : 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)
⊢ HSMul.hSMul (β := ArchimedeanClass R) (Int.negSucc n) (ArchimedeanClass.mk x) =
    -HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n.succ : ℤ) (ArchimedeanClass.mk x)
have mk₄ : -ArchimedeanClass.mk (x ^ n * x) =
  -(HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n : ℤ) (ArchimedeanClass.mk x) + ArchimedeanClass.mk x)
Tactic: rw [← mk_zpow, zpow_negSucc, pow_succ, zsmul_succ', mk_inv, mk_mul, ← zpow_natCast, mk_zpow]
-- 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 : 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)
⊢ HSMul.hSMul (β := ArchimedeanClass R) (Int.negSucc n) (ArchimedeanClass.mk x) =
    -HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n.succ : ℤ) (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_zpow, zpow_negSucc, pow_succ, zsmul_succ', mk_inv, mk_mul, ← zpow_natCast, mk_zpow]
-- 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 : 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)
⊢ HSMul.hSMul (β := ArchimedeanClass R) (Int.negSucc n) (ArchimedeanClass.mk x) =
    -HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n.succ : ℤ) (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 [← mk_zpow, zpow_negSucc, pow_succ, zsmul_succ', mk_inv, mk_mul, ← zpow_natCast, mk_zpow]
-- 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 : 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)
⊢ HSMul.hSMul (β := ArchimedeanClass R) (Int.negSucc n) (ArchimedeanClass.mk x) =
    -HSMul.hSMul (α := ℤ) (β := ArchimedeanClass R) (↑n.succ : ℤ) (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_zpow, zpow_negSucc, pow_succ, zsmul_succ', mk_inv, mk_mul, ← zpow_natCast, mk_zpow]
-- 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 : ArchimedeanClass R
h : x ≠ ⊤
⊢ x + -x = 0
have mk : ∀ (x : R) (h : Ne (α := ArchimedeanClass R) (mk x) ⊤), HAdd.hAdd (α := ArchimedeanClass R) (mk x) (-mk x) = 0
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
inst : LinearOrder R
inst_1 : Field R
inst_2 : IsOrderedRing R
x y : R
⊢ mk (x / y) = HSub.hSub (α := ArchimedeanClass R) (mk x) (mk y)
have rw : mk (x * y⁻¹) = HSub.hSub (α := ArchimedeanClass R) (mk x) (mk y)
Tactic: rw [div_eq_mul_inv, mk_mul, mk_inv, sub_eq_add_neg]
-- 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
x y : R
rw : mk (x * y⁻¹) = HSub.hSub (α := ArchimedeanClass R) (mk x) (mk y)
⊢ mk (x / y) = HSub.hSub (α := ArchimedeanClass R) (mk x) (mk y)
have rw₁ : HAdd.hAdd (α := ArchimedeanClass R) (mk x) (mk y⁻¹) = HSub.hSub (α := ArchimedeanClass R) (mk x) (mk y)
Tactic: rw [div_eq_mul_inv, mk_mul, mk_inv, sub_eq_add_neg]
-- 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
x y : R
rw : mk (x * y⁻¹) = HSub.hSub (α := ArchimedeanClass R) (mk x) (mk y)
rw₁ : HAdd.hAdd (α := ArchimedeanClass R) (mk x) (mk y⁻¹) = HSub.hSub (α := ArchimedeanClass R) (mk x) (mk y)
⊢ mk (x / y) = HSub.hSub (α := ArchimedeanClass R) (mk x) (mk y)
have rw₂ : HAdd.hAdd (α := ArchimedeanClass R) (mk x) (-mk y) = HSub.hSub (α := ArchimedeanClass R) (mk x) (mk y)
Tactic: rw [div_eq_mul_inv, mk_mul, mk_inv, sub_eq_add_neg]
-- 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
x y : R
rw : mk (x * y⁻¹) = HSub.hSub (α := ArchimedeanClass R) (mk x) (mk y)
rw₁ : HAdd.hAdd (α := ArchimedeanClass R) (mk x) (mk y⁻¹) = HSub.hSub (α := ArchimedeanClass R) (mk x) (mk y)
rw₂ : HAdd.hAdd (α := ArchimedeanClass R) (mk x) (-mk y) = HSub.hSub (α := ArchimedeanClass R) (mk x) (mk y)
⊢ mk (x / y) = HSub.hSub (α := ArchimedeanClass R) (mk x) (mk y)
have rw₃ : HAdd.hAdd (α := ArchimedeanClass R) (mk x) (-mk y) = HAdd.hAdd (α := ArchimedeanClass R) (mk x) (-mk y)
Tactic: rw [div_eq_mul_inv, mk_mul, mk_inv, sub_eq_add_neg]
-- 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
q : ℚ
⊢ LE.le.{u_1} (α := ArchimedeanClass R) 0 (mk (↑q : R))
have inl : LE.le.{u_1} (α := ArchimedeanClass R) 0 (mk (↑0 : R))
Tactic: obtain rfl | hn := eq_or_ne q 0
Cleared hypotheses: q
-- 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
q : ℚ
inl : LE.le.{u_1} (α := ArchimedeanClass R) 0 (mk (↑0 : R))
⊢ LE.le.{u_1} (α := ArchimedeanClass R) 0 (mk (↑q : R))
have inr : ∀ (hn : q ≠ 0), LE.le.{u_1} (α := ArchimedeanClass R) 0 (mk (↑q : R))
Tactic: obtain rfl | hn := eq_or_ne q 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
q : ℚ
hn : q ≠ 0
⊢ LE.le.{u_1} (α := ArchimedeanClass R) 0 (mk (↑q : R))
have inr : LE.le.{u_1} (α := ArchimedeanClass R) 0 0
Tactic: rw [mk_ratCast hn]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
x : R
h : IsSquare x
⊢ 0 ≤ x
have rcases : ∀ (y : R), 0 ≤ y * y
Tactic: rcases h with ⟨y, rfl⟩
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x y : R
n : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
hn : n ≠ 0
⊢ x ^ n + y ^ n ≤ (x + y) ^ n
have rcases : ∀ (k : ℕ) (hn : k + 1 ≠ 0), x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
Tactic: rcases Nat.exists_eq_add_one_of_ne_zero hn with ⟨k, rfl⟩
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (hypothesis)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : ∀ (hn : k + 1 ≠ 0), x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
⊢ x ^ (k + 1 + 1) + y ^ (k + 1 + 1) ≤ (x + y) ^ (k + 1 + 1)
have h1 : 0 ≤ x * y ^ n + y * x ^ n
Tactic: have h1 := add_nonneg (mul_nonneg hx (pow_nonneg hy n)) (mul_nonneg hy (pow_nonneg hx n))
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (hypothesis)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : ∀ (hn : k + 1 ≠ 0), x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
⊢ x ^ (k + 1 + 1) + y ^ (k + 1 + 1) ≤ (x + y) ^ (k + 1 + 1)
have h2 : 0 ≤ x + y
Tactic: have h2 := add_nonneg hx hy
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : ∀ (hn : k + 1 ≠ 0), x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x ^ (n + 1) + y ^ (n + 1) ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n)
have rw : x * x ^ n + y * y ^ n ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n)
Tactic: rw [pow_succ' _ n, pow_succ' _ n]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : ∀ (hn : k + 1 ≠ 0), x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = (x + y) * (x ^ n + y ^ n)
have rw : x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = x * (x ^ n + y ^ n) + y * (x ^ n + y ^ n)
Tactic: rw [add_mul, mul_add, mul_add, add_comm (y * x ^ n), ← add_assoc, ← add_assoc,
          add_assoc (x * x ^ n) (x * y ^ n), add_comm (x * y ^ n) (y * y ^ n), ← add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : ∀ (hn : k + 1 ≠ 0), x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
rw : x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = x * (x ^ n + y ^ n) + y * (x ^ n + y ^ n)
⊢ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = (x + y) * (x ^ n + y ^ n)
have rw₁ : x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = x * x ^ n + x * y ^ n + y * (x ^ n + y ^ n)
Tactic: rw [add_mul, mul_add, mul_add, add_comm (y * x ^ n), ← add_assoc, ← add_assoc,
          add_assoc (x * x ^ n) (x * y ^ n), add_comm (x * y ^ n) (y * y ^ n), ← add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : ∀ (hn : k + 1 ≠ 0), x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
rw : x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = x * (x ^ n + y ^ n) + y * (x ^ n + y ^ n)
rw₁ : x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = x * x ^ n + x * y ^ n + y * (x ^ n + y ^ n)
⊢ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = (x + y) * (x ^ n + y ^ n)
have rw₂ : x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = x * x ^ n + x * y ^ n + (y * x ^ n + y * y ^ n)
Tactic: rw [add_mul, mul_add, mul_add, add_comm (y * x ^ n), ← add_assoc, ← add_assoc,
          add_assoc (x * x ^ n) (x * y ^ n), add_comm (x * y ^ n) (y * y ^ n), ← add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : ∀ (hn : k + 1 ≠ 0), x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
rw : x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = x * (x ^ n + y ^ n) + y * (x ^ n + y ^ n)
rw₁ : x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = x * x ^ n + x * y ^ n + y * (x ^ n + y ^ n)
rw₂ : x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = x * x ^ n + x * y ^ n + (y * x ^ n + y * y ^ n)
⊢ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = (x + y) * (x ^ n + y ^ n)
have rw₃ : x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = x * x ^ n + x * y ^ n + (y * y ^ n + y * x ^ n)
Tactic: rw [add_mul, mul_add, mul_add, add_comm (y * x ^ n), ← add_assoc, ← add_assoc,
          add_assoc (x * x ^ n) (x * y ^ n), add_comm (x * y ^ n) (y * y ^ n), ← add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : ∀ (hn : k + 1 ≠ 0), x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
rw : x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = x * (x ^ n + y ^ n) + y * (x ^ n + y ^ n)
rw₁ : x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = x * x ^ n + x * y ^ n + y * (x ^ n + y ^ n)
rw₂ : x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = x * x ^ n + x * y ^ n + (y * x ^ n + y * y ^ n)
rw₃ : x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = x * x ^ n + x * y ^ n + (y * y ^ n + y * x ^ n)
⊢ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = (x + y) * (x ^ n + y ^ n)
have rw₄ : x * x ^ n + y * y ^ n + x * y ^ n + y * x ^ n = x * x ^ n + x * y ^ n + (y * y ^ n + y * x ^ n)
Tactic: rw [add_mul, mul_add, mul_add, add_comm (y * x ^ n), ← add_assoc, ← add_assoc,
          add_assoc (x * x ^ n) (x * y ^ n), add_comm (x * y ^ n) (y * y ^ n), ← add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : ∀ (hn : k + 1 ≠ 0), x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
rw : x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = x * (x ^ n + y ^ n) + y * (x ^ n + y ^ n)
rw₁ : x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = x * x ^ n + x * y ^ n + y * (x ^ n + y ^ n)
rw₂ : x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = x * x ^ n + x * y ^ n + (y * x ^ n + y * y ^ n)
rw₃ : x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = x * x ^ n + x * y ^ n + (y * y ^ n + y * x ^ n)
rw₄ : x * x ^ n + y * y ^ n + x * y ^ n + y * x ^ n = x * x ^ n + x * y ^ n + (y * y ^ n + y * x ^ n)
⊢ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = (x + y) * (x ^ n + y ^ n)
have rw₅ : x * x ^ n + y * y ^ n + x * y ^ n + y * x ^ n = x * x ^ n + x * y ^ n + y * y ^ n + y * x ^ n
Tactic: rw [add_mul, mul_add, mul_add, add_comm (y * x ^ n), ← add_assoc, ← add_assoc,
          add_assoc (x * x ^ n) (x * y ^ n), add_comm (x * y ^ n) (y * y ^ n), ← add_assoc]