awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : Field R
inst_3 : IsOrderedRing R
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R) (-⊤) ⊤

Tactic:
simp [← mk_zero, ← mk_inv]

Premises used: ArchimedeanClass.mk_zero, ArchimedeanClass.mk_inv
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
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 ≠ ⊤
mk :
  ∀ (x : R) (h : Ne (α := ArchimedeanClass R) (ArchimedeanClass.mk x) ⊤),
    HAdd.hAdd (α := ArchimedeanClass R) (ArchimedeanClass.mk x) (-ArchimedeanClass.mk x) = 0
⊢ x + -x = 0

Tactic:
induction x with | mk x

Premises used: ArchimedeanClass.mk
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
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
h : Ne (α := ArchimedeanClass R) (mk x) ⊤
⊢ HAdd.hAdd (α := ArchimedeanClass R) (mk x) (-mk x) = 0

Tactic:
simp [← mk_inv, ← mk_mul, mul_inv_cancel₀ (mk_eq_top_iff.not.1 h)]

Premises used: mul_inv_cancel₀, Iff.not, ArchimedeanClass.mk_mul, Iff.mp, ArchimedeanClass.mk_eq_top_iff, ArchimedeanClass.mk_inv
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
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)
rw₃ rw₄ : HAdd.hAdd (α := ArchimedeanClass R) (mk x) (-mk y) = HAdd.hAdd (α := ArchimedeanClass R) (mk x) (-mk y)
⊢ 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]

Premises used: sub_eq_add_neg, ArchimedeanClass.mk_mul, div_eq_mul_inv, ArchimedeanClass.mk_inv
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : Field R
inst_2 : IsOrderedRing R
q : ℚ
h : q ≠ 0
x : ℚ
⊢ ∀ ⦃b : ℚ⦄,
    x ≤ b →
      ZeroHom.toFun ((↑(RingHom.toAddMonoidHom (Rat.castHom R)) : ZeroHom ℚ R) : ZeroHom ℚ R) x ≤
        ZeroHom.toFun ((↑(RingHom.toAddMonoidHom (Rat.castHom R)) : ZeroHom ℚ R) : ZeroHom ℚ R) b

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : Field R
inst_2 : IsOrderedRing R
q : ℚ
h : q ≠ 0
⊢ Eq.{u_1 + 1} (α := ArchimedeanClass R) (mk (↑q : R)) 0

Tactic:
simpa using mk_map_of_archimedean ⟨(Rat.castHom R).toAddMonoidHom, fun _ ↦ by simp⟩ h

Premises used: OrderAddMonoidHom.mk, RingHom.toAddMonoidHom, ArchimedeanClass.mk_map_of_archimedean, Rat.castHom
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
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))
inr : ∀ (hn : q ≠ 0), LE.le.{u_1} (α := ArchimedeanClass R) 0 (mk (↑q : R))
⊢ LE.le.{u_1} (α := ArchimedeanClass R) 0 (mk (↑q : R))

Tactic:
obtain rfl | hn := eq_or_ne q 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : Field R
inst_2 : IsOrderedRing R
⊢ LE.le.{u_1} (α := ArchimedeanClass R) 0 (mk (↑0 : R))

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : Field R
inst_2 : IsOrderedRing R
q : ℚ
hn : q ≠ 0
inr inr₁ : LE.le.{u_1} (α := ArchimedeanClass R) 0 0
⊢ LE.le.{u_1} (α := ArchimedeanClass R) 0 (mk (↑q : R))

Tactic:
rw [mk_ratCast hn]

Premises used: ArchimedeanClass.mk_ratCast
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : Field R
inst_2 : IsOrderedRing R
x y : R
⊢ LE.le (α := ArchimedeanClass R) (mk x) (mk y) ↔ ∃ (q : ℚ), 0 < q ∧ (↑q : R) * |y| ≤ |x|

Tactic:
simpa using mk_le_mk_iff_denselyOrdered (Rat.castHom _) Rat.cast_strictMono (x := x)

Premises used: ArchimedeanClass.mk_le_mk_iff_denselyOrdered, Rat.cast_strictMono, Rat.castHom
-- Module: Mathlib.Algebra.Order.Ring.Basic
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
rcases : ∀ (y : R), 0 ≤ y * y
⊢ 0 ≤ x

Tactic:
rcases h with ⟨y, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
y : R
⊢ 0 ≤ y * y

Tactic:
mul_self_nonneg y

Premises used: mul_self_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
y : R
⊢ 0 ≤ y * y

Tactic:
exact mul_self_nonneg y

Premises used: mul_self_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Basic
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 : x < 0
⊢ ¬IsSquare x

Tactic:
(h.not_ge ·.nonneg)

Premises used: IsSquare.nonneg, LT.lt.not_ge, Not
-- Module: Mathlib.Algebra.Order.Ring.Basic
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
rcases : ∀ (k : ℕ) (hn : k + 1 ≠ 0), x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
⊢ x ^ n + y ^ n ≤ (x + y) ^ n

Tactic:
rcases Nat.exists_eq_add_one_of_ne_zero hn with ⟨k, rfl⟩

Premises used: Nat.exists_eq_add_one_of_ne_zero, rfl
-- Module: Mathlib.Algebra.Order.Ring.Basic
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
hn : HAdd.hAdd (α := ℕ) 0 1 ≠ 0
⊢ x ^ HAdd.hAdd (α := ℕ) 0 1 + y ^ HAdd.hAdd (α := ℕ) 0 1 ≤ (x + y) ^ HAdd.hAdd (α := ℕ) 0 1

Tactic:
simp only [zero_add, pow_one, le_refl]

Premises used: le_refl, zero_add, pow_one
-- Module: Mathlib.Algebra.Order.Ring.Basic
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
⊢ 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))
-- Module: Mathlib.Algebra.Order.Ring.Basic
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
⊢ 0 ≤ x + y

Tactic:
have h2 := add_nonneg hx hy
-- Module: Mathlib.Algebra.Order.Ring.Basic
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 * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n)
⊢ x ^ (n + 1) + y ^ (n + 1) ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n)

Tactic:
rw [pow_succ' _ n, pow_succ' _ n]

Premises used: pow_succ'
-- Module: Mathlib.Algebra.Order.Ring.Basic
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 * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n)

Tactic:
le_add_of_nonneg_right h1

Premises used: le_add_of_nonneg_right
-- Module: Mathlib.Algebra.Order.Ring.Basic
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 * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n)

Tactic:
exact le_add_of_nonneg_right h1

Premises used: le_add_of_nonneg_right
-- Module: Mathlib.Algebra.Order.Ring.Basic
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)
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
rw₇ : x * x ^ n + y * y ^ n + x * y ^ n + y * x ^ n = x * x ^ n + (y * y ^ n + x * y ^ n) + y * x ^ n
rw₈ rw₉ : x * x ^ n + y * y ^ n + x * y ^ n + y * x ^ n = x * x ^ n + y * y ^ n + x * y ^ n + y * x ^ n
⊢ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = (x + 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]

Premises used: add_mul, HMul.hMul, add_assoc, add_comm, HPow.hPow, mul_add
-- Module: Mathlib.Algebra.Order.Ring.Basic
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 + y) * (x ^ n + y ^ n) ≤ (x + y) * (x + y) ^ n
⊢ (x + y) * (x ^ n + y ^ n) ≤ (x + y) ^ (n + 1)

Tactic:
rw [pow_succ' _ n]

Premises used: pow_succ'
-- Module: Mathlib.Algebra.Order.Ring.Basic
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
hbc : x ^ n + y ^ n ≤ (x + y) ^ n
⊢ (x + y) * (x ^ n + y ^ n) ≤ (x + y) * (x + y) ^ n

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Ring.Basic
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 + y ^ n ≤ (x + y) ^ n

Tactic:
ih (Nat.succ_ne_zero k)

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.Algebra.Order.Ring.Basic
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 + y ^ n ≤ (x + y) ^ n

Tactic:
exact ih (Nat.succ_ne_zero k)

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.Algebra.Order.Ring.Basic
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 + 1) + y ^ (n + 1) ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n)
x₂ : x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = (x + y) * (x ^ n + y ^ n)
x₃ : (x + y) * (x ^ n + y ^ n) ≤ (x + y) ^ (n + 1)
⊢ x ^ (k + 1 + 1) + y ^ (k + 1 + 1) ≤ (x + y) ^ (k + 1 + 1)

Tactic:
calc
      x ^ (n + 1) + y ^ (n + 1) ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) := by
        rw [pow_succ' _ n, pow_succ' _ n]
        exact le_add_of_nonneg_right h1
      _ = (x + y) * (x ^ n + y ^ n) := by
        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]
      _ ≤ (x + y) ^ (n + 1) := by
        rw [pow_succ' _ n]
        gcongr; exact ih (Nat.succ_ne_zero k)

Premises used: HMul.hMul, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Ring.Basic
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 : ℕ
hn : k + 1 ≠ 0
zero :
  ∀ (hn : HAdd.hAdd (α := ℕ) 0 1 ≠ 0),
    x ^ HAdd.hAdd (α := ℕ) 0 1 + y ^ HAdd.hAdd (α := ℕ) 0 1 ≤ (x + y) ^ HAdd.hAdd (α := ℕ) 0 1
succ :
  ∀ (k : ℕ) (ih : ∀ (hn : k + 1 ≠ 0), x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)) (hn : k + 1 + 1 ≠ 0),
    x ^ (k + 1 + 1) + y ^ (k + 1 + 1) ≤ (x + y) ^ (k + 1 + 1)
⊢ x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)

Tactic:
induction k with
  | zero => simp only [zero_add, pow_one, le_refl]
  | succ k ih =>
    let n := k.succ
    have h1 := add_nonneg (mul_nonneg hx (pow_nonneg hy n)) (mul_nonneg hy (pow_nonneg hx n))
    have h2 := add_nonneg hx hy
    calc
      x ^ (n + 1) + y ^ (n + 1) ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) := by
        rw [pow_succ' _ n, pow_succ' _ n]
        exact le_add_of_nonneg_right h1
      _ = (x + y) * (x ^ n + y ^ n) := by
        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]
      _ ≤ (x + y) ^ (n + 1) := by
        rw [pow_succ' _ n]
        gcongr; exact ih (Nat.succ_ne_zero k)

Premises used: le_refl, zero_add, HAdd.hAdd, pow_one, Int.succ
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
rw : a ^ n + b ^ n ≤ (a + b) ^ n + (a + b) ^ n
⊢ a ^ n + b ^ n ≤ 2 * (a + b) ^ n

Tactic:
rw [two_mul]

Premises used: two_mul
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
h₁ : a ≤ a + b
h₂ : b ≤ a + b
⊢ a ^ n + b ^ n ≤ (a + b) ^ n + (a + b) ^ n

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a ≤ a + b

Tactic:
le_add_of_nonneg_right hb

Premises used: le_add_of_nonneg_right
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ b ≤ a + b

Tactic:
le_add_of_nonneg_left ha

Premises used: le_add_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a ≤ a + b

Tactic:
exacts [le_add_of_nonneg_right hb, le_add_of_nonneg_left ha]

Premises used: le_add_of_nonneg_right, le_add_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
a : R
ha : a < 0
rw : 0 < a * a
⊢ 0 < HPow.hPow (β := ℕ) a 2

Tactic:
rw [sq]

Premises used: sq
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
a : R
ha : a < 0
⊢ 0 < a * a

Tactic:
mul_pos_of_neg_of_neg ha ha

Premises used: mul_pos_of_neg_of_neg
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
a : R
ha : a < 0
⊢ 0 < a * a

Tactic:
exact mul_pos_of_neg_of_neg ha ha

Premises used: mul_pos_of_neg_of_neg
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : ExistsAddOfLE R
n : ℕ
hn : Even n
a : R
obtain : ∀ (k : ℕ), 0 ≤ a ^ (k + k)
⊢ 0 ≤ a ^ n

Tactic:
obtain ⟨k, rfl⟩ := hn

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : ExistsAddOfLE R
a : R
k : ℕ
rw : 0 ≤ a ^ k * a ^ k
⊢ 0 ≤ a ^ (k + k)

Tactic:
rw [pow_add]

Premises used: pow_add
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : ExistsAddOfLE R
a : R
k : ℕ
⊢ 0 ≤ a ^ k * a ^ k

Tactic:
mul_self_nonneg _

Premises used: mul_self_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : ExistsAddOfLE R
a : R
k : ℕ
⊢ 0 ≤ a ^ k * a ^ k

Tactic:
exact mul_self_nonneg _

Premises used: mul_self_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : ExistsAddOfLE R
a b : R
h : HPow.hPow (β := ℕ) a 2 ≤ b
⊢ HPow.hPow (β := ℕ) a 4 ≤ HPow.hPow (β := ℕ) b 2

Tactic:
(pow_mul a 2 2).symm ▸ pow_le_pow_left₀ (sq_nonneg a) h 2

Premises used: pow_le_pow_left₀, Eq.rec, pow_mul, sq_nonneg, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
inst_3 : ExistsAddOfLE R
simp_rw :
  (a + b) * ((a + b) * HPow.hPow (β := ℕ) (a + b) 0) =
    a * (a * HPow.hPow (β := ℕ) a 0) + b * (b * HPow.hPow (β := ℕ) b 0) + (a * b + b * a)
simp_rw₁ : (a + b) * ((a + b) * 1) = a * (a * 1) + b * (b * 1) + (a * b + b * a)
simp_rw₂ : (a + b) * (a + b) = a * a + b * b + (a * b + b * a)
simp_rw₃ : a * (a + b) + b * (a + b) = a * a + b * b + (a * b + b * a)
simp_rw₄ : a * a + a * b + (b * a + b * b) = a * a + b * b + (a * b + b * a)
simp_rw₅ : a * a + a * b + (b * b + b * a) = a * a + b * b + (a * b + b * a)
⊢ HPow.hPow (β := ℕ) (a + b) 2 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + (a * b + b * a)

Tactic:
simp_rw [pow_succ', pow_zero, mul_one, add_mul, mul_add, add_comm (b * a), add_add_add_comm]

Premises used: add_mul, HMul.hMul, add_comm, pow_zero, mul_add, add_add_add_comm, mul_one, pow_succ'
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
inst_3 : ExistsAddOfLE R
⊢ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + (a * b + b * a) ≤
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + (a * a + b * b)

Tactic:
add_le_add_right ?_ _

Premises used: add_le_add_right
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
inst_3 : ExistsAddOfLE R
simp_rw :
  a * (a * HPow.hPow (β := ℕ) a 0) + b * (b * HPow.hPow (β := ℕ) b 0) + (a * a + b * b) =
    2 * (a * (a * HPow.hPow (β := ℕ) a 0) + b * (b * HPow.hPow (β := ℕ) b 0))
simp_rw₁ : a * (a * 1) + b * (b * 1) + (a * a + b * b) = 2 * (a * (a * 1) + b * (b * 1))
simp_rw₂ : a * a + b * b + (a * a + b * b) = 2 * (a * a + b * b)
⊢ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + (a * a + b * b) =
    2 * (HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2)

Tactic:
simp_rw [pow_succ', pow_zero, mul_one, two_mul]

Premises used: two_mul, pow_zero, mul_one, pow_succ'
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
inst_3 : ExistsAddOfLE R
a₁ : a * b + b * a ≤ a * a + b * b
⊢ HPow.hPow (β := ℕ) (a + b) 2 ≤ 2 * (HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2)

Tactic:
calc
    (a + b) ^ 2 = a ^ 2 + b ^ 2 + (a * b + b * a) := by
        simp_rw [pow_succ', pow_zero, mul_one, add_mul, mul_add, add_comm (b * a), add_add_add_comm]
    _ ≤ a ^ 2 + b ^ 2 + (a * a + b * b) := add_le_add_right ?_ _
    _ = _ := by simp_rw [pow_succ', pow_zero, mul_one, two_mul]

Premises used: HMul.hMul, add_le_add_right, HAdd.hAdd
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
inst_3 : ExistsAddOfLE R
inl : a ≤ b → a * b + b * a ≤ a * a + b * b
inr : b ≤ a → a * b + b * a ≤ a * a + b * b
⊢ a * b + b * a ≤ a * a + b * b

Tactic:
cases le_total a b

Premises used: le_total
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
inst_3 : ExistsAddOfLE R
h : a ≤ b
⊢ a * b + b * a ≤ a * a + b * b

Tactic:
mul_add_mul_le_mul_add_mul ‹_› ‹_›

Premises used: mul_add_mul_le_mul_add_mul
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
inst_3 : ExistsAddOfLE R
h : a ≤ b
⊢ a * b + b * a ≤ a * a + b * b

Tactic:
exact mul_add_mul_le_mul_add_mul ‹_› ‹_›

Premises used: mul_add_mul_le_mul_add_mul
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
inst_3 : ExistsAddOfLE R
h : b ≤ a
⊢ a * b + b * a ≤ a * a + b * b

Tactic:
mul_add_mul_le_mul_add_mul' ‹_› ‹_›

Premises used: mul_add_mul_le_mul_add_mul'
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
inst_3 : ExistsAddOfLE R
h : b ≤ a
⊢ a * b + b * a ≤ a * a + b * b

Tactic:
exact mul_add_mul_le_mul_add_mul' ‹_› ‹_›

Premises used: mul_add_mul_le_mul_add_mul'
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
inst_3 : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
⊢ HPow.hPow (β := ℕ) (a + b) 0 ≤
    HPow.hPow (α := R) 2 (HSub.hSub (α := ℕ) 0 1) * (HPow.hPow (β := ℕ) a 0 + HPow.hPow (β := ℕ) b 0)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
inst_3 : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
⊢ HPow.hPow (β := ℕ) (a + b) 1 ≤
    HPow.hPow (α := R) 2 (HSub.hSub (α := ℕ) 1 1) * (HPow.hPow (β := ℕ) a 1 + HPow.hPow (β := ℕ) b 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
inst_3 : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
rw : (a + b) ^ (n + 1) * (a + b) ≤ HPow.hPow (α := R) 2 (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))
⊢ (a + b) ^ (n + 2) ≤ HPow.hPow (α := R) 2 (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))

Tactic:
rw [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
inst_3 : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ (a + b) ^ (n + 1) * (a + b) ≤ HPow.hPow (α := R) 2 n * (a ^ (n + 1) + b ^ (n + 1)) * (a + b)

Tactic:
mul_le_mul_of_nonneg_right (add_pow_le ha hb (n + 1)) <| add_nonneg ha hb

Premises used: add_nonneg, mul_le_mul_of_nonneg_right, HAdd.hAdd, OfNat.ofNat