awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Ring.Pow
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ HPow.hPow (β := ℕ) b 2
Hsq' : 0 ≤ HPow.hPow (β := ℕ) (a + b) 2
H : 0 ≤ 2 * a + b
n : ℕ
simp :
  a * (a * (a * a ^ n)) +
        ((↑n : R) * (b * (a * (a * a ^ n))) + (b * (a * (a * a ^ n)) + b * (a * (a * a ^ n)) + b * (a * (a * a ^ n)))) +
      ((↑n : R) * (b * (b * (a * a ^ n))) + b * (b * (a * a ^ n)) +
            ((↑n : R) * (b * (b * (a * a ^ n))) + b * (b * (a * a ^ n))) +
          ((↑n : R) * (b * (b * (b * a ^ n))) + b * (b * (b * a ^ n))) +
        b * (b * (a * a ^ n))) =
    a * (a * (a * a ^ n)) + b * (a * (a * a ^ n)) + (b * (a * (a * a ^ n)) + b * (b * (a * a ^ n))) +
      ((↑n : R) * (b * (a * (a * a ^ n))) + (↑n : R) * (b * (b * (a * a ^ n))) +
          ((↑n : R) * (b * (b * (a * a ^ n))) + (↑n : R) * (b * (b * (b * a ^ n)))) +
        (b * (a * (a * a ^ n)) + b * (b * (a * a ^ n)) + (b * (b * (a * a ^ n)) + b * (b * (b * a ^ n)))))
⊢ a ^ (n + 3) + (↑(n + 3) : R) * a ^ (n + 2) * b +
      (HAdd.hAdd (α := R) (↑n : R) 1 * (HPow.hPow (β := ℕ) b 2 * (2 * a + b) * a ^ n) +
        a ^ (n + 1) * HPow.hPow (β := ℕ) b 2) =
    HPow.hPow (β := ℕ) (a + b) 2 * (a ^ (n + 1) + (↑(n + 1) : R) * a ^ n * b)

Tactic:
simp only [Nat.cast_add, Nat.cast_one, Nat.cast_ofNat, pow_succ', add_mul, mul_add,
          two_mul, pow_zero, mul_one,
          Hcomm.eq, (n.cast_commute (_ : R)).symm.left_comm, mul_assoc, (Hcomm.pow_left _).eq,
          (Hcomm.pow_left _).left_comm, Hcomm.left_comm, ← @two_add_one_eq_three R, one_mul]

Premises used: add_mul, Nat.cast_ofNat, Commute.left_comm, mul_assoc, two_mul, Commute.pow_left, pow_zero, Nat.cast_add, Commute.symm, mul_add, mul_one, two_add_one_eq_three, Nat.cast_one, Commute.eq, pow_succ', one_mul, Nat.cast_commute
-- Module: Mathlib.Algebra.Order.Ring.Pow
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ HPow.hPow (β := ℕ) b 2
Hsq' : 0 ≤ HPow.hPow (β := ℕ) (a + b) 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ a * (a * (a * a ^ n)) +
        ((↑n : R) * (b * (a * (a * a ^ n))) + (b * (a * (a * a ^ n)) + b * (a * (a * a ^ n)) + b * (a * (a * a ^ n)))) +
      ((↑n : R) * (b * (b * (a * a ^ n))) + b * (b * (a * a ^ n)) +
            ((↑n : R) * (b * (b * (a * a ^ n))) + b * (b * (a * a ^ n))) +
          ((↑n : R) * (b * (b * (b * a ^ n))) + b * (b * (b * a ^ n))) +
        b * (b * (a * a ^ n))) =
    a * (a * (a * a ^ n)) + b * (a * (a * a ^ n)) + (b * (a * (a * a ^ n)) + b * (b * (a * a ^ n))) +
      ((↑n : R) * (b * (a * (a * a ^ n))) + (↑n : R) * (b * (b * (a * a ^ n))) +
          ((↑n : R) * (b * (b * (a * a ^ n))) + (↑n : R) * (b * (b * (b * a ^ n)))) +
        (b * (a * (a * a ^ n)) + b * (b * (a * a ^ n)) + (b * (b * (a * a ^ n)) + b * (b * (b * a ^ n)))))

Tactic:
abel
-- Module: Mathlib.Algebra.Order.Ring.Pow
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ HPow.hPow (β := ℕ) b 2
Hsq' : 0 ≤ HPow.hPow (β := ℕ) (a + b) 2
H : 0 ≤ 2 * a + b
n : ℕ
hbc : a ^ (n + 1) + (↑(n + 1) : R) * a ^ n * b ≤ (a + b) ^ (n + 1)
⊢ HPow.hPow (β := ℕ) (a + b) 2 * (a ^ (n + 1) + (↑(n + 1) : R) * a ^ n * b) ≤
    HPow.hPow (β := ℕ) (a + b) 2 * (a + b) ^ (n + 1)

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Ring.Pow
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ HPow.hPow (β := ℕ) b 2
Hsq' : 0 ≤ HPow.hPow (β := ℕ) (a + b) 2
H : 0 ≤ 2 * a + b
n : ℕ
hbc : Commute a b
hbc₁ : 0 ≤ a
hbc₂ : 0 ≤ HPow.hPow (β := ℕ) b 2
hbc₃ : 0 ≤ HPow.hPow (β := ℕ) (a + b) 2
hbc₄ : 0 ≤ 2 * a + b
⊢ a ^ (n + 1) + (↑(n + 1) : R) * a ^ n * b ≤ (a + b) ^ (n + 1)

Tactic:
apply Commute.pow_add_mul_le_add_pow_of_sq_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Pow
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ HPow.hPow (β := ℕ) b 2
Hsq' : 0 ≤ HPow.hPow (β := ℕ) (a + b) 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ Commute a b

Tactic:
assumption
-- Module: Mathlib.Algebra.Order.Ring.Pow
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ HPow.hPow (β := ℕ) b 2
Hsq' : 0 ≤ HPow.hPow (β := ℕ) (a + b) 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ 0 ≤ a

Tactic:
assumption
-- Module: Mathlib.Algebra.Order.Ring.Pow
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ HPow.hPow (β := ℕ) b 2
Hsq' : 0 ≤ HPow.hPow (β := ℕ) (a + b) 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ 0 ≤ HPow.hPow (β := ℕ) b 2

Tactic:
assumption
-- Module: Mathlib.Algebra.Order.Ring.Pow
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ HPow.hPow (β := ℕ) b 2
Hsq' : 0 ≤ HPow.hPow (β := ℕ) (a + b) 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ 0 ≤ HPow.hPow (β := ℕ) (a + b) 2

Tactic:
assumption
-- Module: Mathlib.Algebra.Order.Ring.Pow
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ HPow.hPow (β := ℕ) b 2
Hsq' : 0 ≤ HPow.hPow (β := ℕ) (a + b) 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ 0 ≤ 2 * a + b

Tactic:
assumption
-- Module: Mathlib.Algebra.Order.Ring.Pow
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ HPow.hPow (β := ℕ) b 2
Hsq' : 0 ≤ HPow.hPow (β := ℕ) (a + b) 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ HPow.hPow (β := ℕ) (a + b) 2 * (a + b) ^ (n + 1) = (a + b) ^ (n + 3)

Tactic:
simp [pow_succ', mul_assoc]

Premises used: mul_assoc, pow_succ'
-- Module: Mathlib.Algebra.Order.Ring.Pow
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ HPow.hPow (β := ℕ) b 2
Hsq' : 0 ≤ HPow.hPow (β := ℕ) (a + b) 2
H : 0 ≤ 2 * a + b
n : ℕ
_ :
  a ^ (n + 3) + (↑(n + 3) : R) * a ^ (n + 2) * b +
      (HAdd.hAdd (α := R) (↑n : R) 1 * (HPow.hPow (β := ℕ) b 2 * (2 * a + b) * a ^ n) +
        a ^ (n + 1) * HPow.hPow (β := ℕ) b 2) =
    HPow.hPow (β := ℕ) (a + b) 2 * (a ^ (n + 1) + (↑(n + 1) : R) * a ^ n * b)
_₁ :
  HPow.hPow (β := ℕ) (a + b) 2 * (a ^ (n + 1) + (↑(n + 1) : R) * a ^ n * b) ≤
    HPow.hPow (β := ℕ) (a + b) 2 * (a + b) ^ (n + 1)
_₂ : HPow.hPow (β := ℕ) (a + b) 2 * (a + b) ^ (n + 1) = (a + b) ^ (n + 3)
⊢ a ^ (n + 3) + (↑(n + 3) : R) * a ^ (n + 3 - 1) * b ≤ (a + b) ^ (n + 3)

Tactic:
calc
      _ ≤ a ^ (n + 3) + ↑(n + 3) * a ^ (n + 2) * b +
            ((n + 1) * (b ^ 2 * (2 * a + b) * a ^ n) + a ^ (n + 1) * b ^ 2) :=
        le_add_of_nonneg_right <| by
          apply_rules [add_nonneg, mul_nonneg, Nat.cast_nonneg, pow_nonneg, zero_le_one]
      _ = (a + b) ^ 2 * (a ^ (n + 1) + ↑(n + 1) * a ^ n * b) := by
        simp only [Nat.cast_add, Nat.cast_one, Nat.cast_ofNat, pow_succ', add_mul, mul_add,
          two_mul, pow_zero, mul_one,
          Hcomm.eq, (n.cast_commute (_ : R)).symm.left_comm, mul_assoc, (Hcomm.pow_left _).eq,
          (Hcomm.pow_left _).left_comm, Hcomm.left_comm, ← @two_add_one_eq_three R, one_mul]
        abel
      _ ≤ (a + b) ^ 2 * (a + b) ^ (n + 1) := by
        gcongr
        apply Commute.pow_add_mul_le_add_pow_of_sq_nonneg <;> assumption
      _ = (a + b) ^ (n + 3) := by simp [pow_succ', mul_assoc]

Premises used: HMul.hMul, Nat.cast, le_add_of_nonneg_right, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Ring.Pow
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a : R
Hsq : 0 ≤ HPow.hPow (β := ℕ) a 2
Hsq' : 0 ≤ HPow.hPow (β := ℕ) (1 + a) 2
H : 0 ≤ 2 + a
n : ℕ
⊢ 0 ≤ HMul.hMul (α := R) 2 1 + a

Tactic:
simpa using H
-- Module: Mathlib.Algebra.Order.Ring.Pow
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a : R
Hsq : 0 ≤ HPow.hPow (β := ℕ) a 2
Hsq' : 0 ≤ HPow.hPow (β := ℕ) (1 + a) 2
H : 0 ≤ 2 + a
n : ℕ
⊢ 1 + (↑n : R) * a ≤ (1 + a) ^ n

Tactic:
simpa using (Commute.one_left a).pow_add_mul_le_add_pow_of_sq_nonneg zero_le_one Hsq Hsq'
    (by simpa using H) n

Premises used: Commute.pow_add_mul_le_add_pow_of_sq_nonneg, zero_le_one, Commute.one_left
-- Module: Mathlib.Algebra.Order.Ring.Pow
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b : R
ha : 0 ≤ a
Hsq : 0 ≤ HPow.hPow (β := ℕ) b 2
Hsq' : 0 ≤ HPow.hPow (β := ℕ) (a + b) 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ a ^ n + (↑n : R) * a ^ (n - 1) * b ≤ (a + b) ^ n

Tactic:
(Commute.all a b).pow_add_mul_le_add_pow_of_sq_nonneg ha Hsq Hsq' H n

Premises used: Commute.pow_add_mul_le_add_pow_of_sq_nonneg, Commute.all
-- Module: Mathlib.Algebra.Order.Ring.Pow
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : ExistsAddOfLE R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
H : 0 ≤ 2 * a + b
n : ℕ
⊢ a ^ n + (↑n : R) * a ^ (n - 1) * b ≤ (a + b) ^ n

Tactic:
Hcomm.pow_add_mul_le_add_pow_of_sq_nonneg ha (sq_nonneg _) (sq_nonneg _) H n

Premises used: Commute.pow_add_mul_le_add_pow_of_sq_nonneg, sq_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Pow
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : ExistsAddOfLE R
a b : R
ha : 0 ≤ a
H : 0 ≤ 2 * a + b
n : ℕ
⊢ a ^ n + (↑n : R) * a ^ (n - 1) * b ≤ (a + b) ^ n

Tactic:
(Commute.all a b).pow_add_mul_le_add_pow ha H n

Premises used: Commute.pow_add_mul_le_add_pow, Commute.all
-- Module: Mathlib.Algebra.Order.Ring.Pow
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : ExistsAddOfLE R
a : R
H : 0 ≤ 2 + a
n : ℕ
⊢ 1 + (↑n : R) * a ≤ (1 + a) ^ n

Tactic:
one_add_mul_le_pow_of_sq_nonneg (sq_nonneg _) (sq_nonneg _) H _

Premises used: sq_nonneg, one_add_mul_le_pow_of_sq_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Pow
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
H : -2 ≤ a
n : ℕ
⊢ 1 + (↑n : R) * a ≤ (1 + a) ^ n

Tactic:
one_add_le_pow_of_two_add_nonneg (neg_le_iff_add_nonneg'.mp H) n

Premises used: neg_le_iff_add_nonneg', one_add_le_pow_of_two_add_nonneg, Iff.mp
-- Module: Mathlib.Algebra.Order.Ring.Pow
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
H : -1 ≤ a
n : ℕ
rwa : -HAdd.hAdd (α := R) 1 1 ≤ a - 1
rwa₁ : HAdd.hAdd (α := R) (-1) (-1) ≤ a - 1
rwa₂ : HSub.hSub (α := R) (-1) 1 ≤ a - 1
rwa₃ rwa₄ rwa₅ rwa₆ : -1 ≤ a
⊢ -2 ≤ a - 1

Tactic:
rwa [← one_add_one_eq_two, neg_add, ← sub_eq_add_neg, sub_le_sub_iff_right]

Premises used: sub_eq_add_neg, neg_add, sub_le_sub_iff_right, one_add_one_eq_two
-- Module: Mathlib.Algebra.Order.Ring.Pow
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
H : -1 ≤ a
n : ℕ
⊢ -2 ≤ a - 1

Tactic:
have : -2 ≤ a - 1 := by
    rwa [← one_add_one_eq_two, neg_add, ← sub_eq_add_neg, sub_le_sub_iff_right]
-- Module: Mathlib.Algebra.Order.Ring.Pow
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
H : -1 ≤ a
n : ℕ
this : -2 ≤ a - 1
⊢ 1 + (↑n : R) * (a - 1) ≤ a ^ n

Tactic:
simpa only [add_sub_cancel] using one_add_mul_le_pow this n

Premises used: add_sub_cancel, one_add_mul_le_pow
-- Module: Mathlib.Algebra.Order.Ring.Rat
Goal:
⊢ IsStrictOrderedRing ℚ

Tactic:
.of_mul_pos fun _ _ ha hb ↦
  (Rat.mul_nonneg ha.le hb.le).lt_of_ne' (mul_ne_zero ha.ne' hb.ne')

Premises used: LT.lt.le, LT.lt.ne', Rat.mul_nonneg, IsStrictOrderedRing.of_mul_pos, mul_ne_zero, LE.le.lt_of_ne'
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
⊢ Eq.{u_1 + 1} (α := K) (↑0 : K) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
⊢ Eq.{u_1 + 1} (α := K) (↑1 : K) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : FiniteElement K
⊢ (↑(x + y) : K) = (↑x : K) + (↑y : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : FiniteElement K
⊢ (↑(x - y) : K) = (↑x : K) - (↑y : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : FiniteElement K
⊢ (↑(x * y) : K) = (↑x : K) * (↑y : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : FiniteElement K
h : (↑x : K) = (↑y : K)
⊢ x = y

Tactic:
Subtype.ext h

Premises used: ArchimedeanClass.FiniteElement, Subtype.ext
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
⊢ LE.le.{u_1} (α := ArchimedeanClass K) 0 (mk 0)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
⊢ Eq.{u_1 + 1} (α := FiniteElement K) (FiniteElement.mk 0 ⋯) 0

Tactic:
rfl

Premises used: ArchimedeanClass.FiniteElement.mk, rfl
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
⊢ LE.le.{u_1} (α := ArchimedeanClass K) 0 (mk 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
⊢ Eq.{u_1 + 1} (α := FiniteElement K) (FiniteElement.mk 1 ⋯) 1

Tactic:
rfl

Premises used: ArchimedeanClass.FiniteElement.mk, rfl
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
n : ℕ
⊢ Eq.{u_1 + 1} (α := FiniteElement K) (FiniteElement.mk (↑n : K) ⋯) (↑n : FiniteElement K)

Tactic:
rfl

Premises used: ArchimedeanClass.FiniteElement.mk, rfl
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
n : ℤ
⊢ Eq.{u_1 + 1} (α := FiniteElement K) (FiniteElement.mk (↑n : K) ⋯) (↑n : FiniteElement K)

Tactic:
rfl

Premises used: ArchimedeanClass.FiniteElement.mk, rfl
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x : K
h rwa rwa₁ rwa₂ rwa₃ : LE.le (α := ArchimedeanClass K) 0 (mk x)
⊢ LE.le (α := ArchimedeanClass K) 0 (mk (-x))

Tactic:
rwa [mk_neg]

Premises used: ArchimedeanClass.mk_neg
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
h : LE.le (α := ArchimedeanClass K) 0 (mk x)
⊢ Eq (α := FiniteElement K) (-FiniteElement.mk x h) (FiniteElement.mk (-x) ⋯)

Tactic:
rfl

Premises used: ArchimedeanClass.FiniteElement.mk, rfl
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
hy : LE.le (α := ArchimedeanClass K) 0 (mk y)
⊢ HAdd.hAdd (α := FiniteElement K) (FiniteElement.mk x hx) (FiniteElement.mk y hy) = FiniteElement.mk (x + y) ⋯

Tactic:
rfl

Premises used: ArchimedeanClass.FiniteElement.mk, rfl
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
hy : LE.le (α := ArchimedeanClass K) 0 (mk y)
⊢ HSub.hSub (α := FiniteElement K) (FiniteElement.mk x hx) (FiniteElement.mk y hy) = FiniteElement.mk (x - y) ⋯

Tactic:
rfl

Premises used: ArchimedeanClass.FiniteElement.mk, rfl
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
hy : LE.le (α := ArchimedeanClass K) 0 (mk y)
⊢ HMul.hMul (α := FiniteElement K) (FiniteElement.mk x hx) (FiniteElement.mk y hy) = FiniteElement.mk (x * y) ⋯

Tactic:
rfl

Premises used: ArchimedeanClass.FiniteElement.mk, rfl
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
hy : LE.le (α := ArchimedeanClass K) 0 (mk y)
⊢ LE.le (α := FiniteElement K) (FiniteElement.mk x hx) (FiniteElement.mk y hy) ↔ x ≤ y

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
hy : LE.le (α := ArchimedeanClass K) 0 (mk y)
⊢ LT.lt (α := FiniteElement K) (FiniteElement.mk x hx) (FiniteElement.mk y hy) ↔ x < y

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : FiniteElement K
⊢ ¬IsUnit x ↔ LT.lt (α := ArchimedeanClass K) 0 (mk (↑x : K))

Tactic:
Valuation.Integer.not_isUnit_iff_valuation_lt_one

Premises used: Set.Mem, Valuation.Integer.not_isUnit_iff_valuation_lt_one, ArchimedeanClass.FiniteElement
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : FiniteElement K
rw : ¬IsUnit x ↔ ¬Eq (α := ArchimedeanClass K) (mk (↑x : K)) 0
rw₁ : LT.lt (α := ArchimedeanClass K) 0 (mk (↑x : K)) ↔ ¬Eq (α := ArchimedeanClass K) (mk (↑x : K)) 0
rw₂ : ¬LE.le (α := ArchimedeanClass K) (mk (↑x : K)) 0 ↔ ¬Eq (α := ArchimedeanClass K) (mk (↑x : K)) 0
rw₃ rw₄ : ¬Eq (α := ArchimedeanClass K) (mk (↑x : K)) 0 ↔ ¬Eq (α := ArchimedeanClass K) (mk (↑x : K)) 0
⊢ IsUnit x ↔ Eq (α := ArchimedeanClass K) (mk (↑x : K)) 0

Tactic:
rw [← not_iff_not, not_isUnit_iff_mk_pos, lt_iff_not_ge, x.2.ge_iff_eq']

Premises used: not_iff_not, lt_iff_not_ge, ArchimedeanClass.FiniteElement.not_isUnit_iff_mk_pos, LE.le.ge_iff_eq'
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
q : ℚ
⊢ Eq.{u_1 + 1} (α := FiniteElement K) (FiniteElement.mk (↑q : K) ⋯) (↑q : FiniteElement K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x : FiniteElement K
obtain :
  ∀ (n : ℕ)
    (hn :
      |(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
            ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) (↑x : K) : ArchimedeanOrder K)| ≤
        HSMul.hSMul (β := K) n
          (|(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
                ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) 1 : ArchimedeanOrder K)| :
            K)),
    ∃ (n : ℕ), x ≤ (↑n : FiniteElement K)
⊢ ∃ (n : ℕ), x ≤ (↑n : FiniteElement K)

Tactic:
obtain ⟨n, hn⟩ := x.2

Premises used: Subtype.property
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x : FiniteElement K
n : ℕ
hn :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
        ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) (↑x : K) : ArchimedeanOrder K)| ≤
    HSMul.hSMul (β := K) n
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
            ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) 1 : ArchimedeanOrder K)| :
        K)
⊢ ∃ (n : ℕ), x ≤ (↑n : FiniteElement K)

Tactic:
⟨n, (le_abs_self x).trans ?_⟩

Premises used: le_abs_self, Exists.intro, LE.le.trans
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x : FiniteElement K
n : ℕ
hn :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
        ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) (↑x : K) : ArchimedeanOrder K)| ≤
    HSMul.hSMul (β := K) n
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
            ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) 1 : ArchimedeanOrder K)| :
        K)
refine : |x| ≤ (↑n : FiniteElement K)
⊢ ∃ (n : ℕ), x ≤ (↑n : FiniteElement K)

Tactic:
refine ⟨n, (le_abs_self x).trans ?_⟩
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x : FiniteElement K
n : ℕ
hn :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
        ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) (↑x : K) : ArchimedeanOrder K)| ≤
    HSMul.hSMul (β := K) n
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
            ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) 1 : ArchimedeanOrder K)| :
        K)
⊢ |x| ≤ (↑n : FiniteElement K)

Tactic:
simpa using hn
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
⊢ ∀ (x : Quotient (α := FiniteElement K) (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)))),
    Set.OrdConnected (α := FiniteElement K)
      (Set.preimage (β :=
        Quotient (α := FiniteElement K) (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))))
        (Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)))) {x})

Tactic:
fun x ↦ ⟨?_⟩

Premises used: Set.OrdConnected.mk
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
refine :
  ∀ (x : Quotient (α := FiniteElement K) (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))))
    ⦃x_1 : FiniteElement K⦄
    (hx :
      Membership.mem (γ := Set (FiniteElement K))
        (Set.preimage (β :=
          Quotient (α := FiniteElement K) (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))))
          (Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)))) {x})
        x_1)
    ⦃y : FiniteElement K⦄
    (hy :
      Membership.mem (γ := Set (FiniteElement K))
        (Set.preimage (β :=
          Quotient (α := FiniteElement K) (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))))
          (Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)))) {x})
        y),
    Set.Icc x_1 y ⊆
      Set.preimage (β :=
        Quotient (α := FiniteElement K) (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))))
        (Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)))) {x}
⊢ ∀ (x : Quotient (α := FiniteElement K) (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)))),
    Set.OrdConnected (α := FiniteElement K)
      (Set.preimage (β :=
        Quotient (α := FiniteElement K) (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))))
        (Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)))) {x})

Tactic:
refine fun x ↦ ⟨?_⟩