awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
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 + (y * y ^ n + x * 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)
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
⊢ 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 * y ^ n + x * 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
⊢ (x + y) * (x ^ n + y ^ n) ≤ (x + y) ^ (n + 1)
have rw : (x + y) * (x ^ n + y ^ n) ≤ (x + y) * (x + y) ^ n
Tactic: rw [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 + y) * (x ^ n + y ^ n) ≤ (x + y) * (x + y) ^ n
have hbc : x ^ n + y ^ n ≤ (x + y) ^ n
Tactic: gcongr
-- 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 ^ (k + 1 + 1) + y ^ (k + 1 + 1) ≤ (x + y) ^ (k + 1 + 1)
have x₁ : x ^ (n + 1) + y ^ (n + 1) ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n)
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)
-- 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 + 1) + y ^ (n + 1) ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n)
⊢ x ^ (k + 1 + 1) + y ^ (k + 1 + 1) ≤ (x + y) ^ (k + 1 + 1)
have x₂ : x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = (x + y) * (x ^ n + y ^ n)
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)
-- 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 + 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 ^ (k + 1 + 1) + y ^ (k + 1 + 1) ≤ (x + y) ^ (k + 1 + 1)
have x₃ : (x + y) * (x ^ n + y ^ n) ≤ (x + y) ^ (n + 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)
-- 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 : ℕ
hn : k + 1 ≠ 0
⊢ x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
have zero : ∀ (hn : HAdd.hAdd (α := ℕ) 0 1 ≠ 0),
  x ^ HAdd.hAdd (α := ℕ) 0 1 + y ^ HAdd.hAdd (α := ℕ) 0 1 ≤ (x + y) ^ HAdd.hAdd (α := ℕ) 0 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)
Cleared hypotheses: k, hn
-- 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 : ℕ
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
⊢ x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
have 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)
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)
Cleared hypotheses: k, hn
-- 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
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a ^ n + b ^ n ≤ 2 * (a + b) ^ n
have rw : a ^ n + b ^ n ≤ (a + b) ^ n + (a + b) ^ n
Tactic: rw [two_mul]
-- 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
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a ^ n + b ^ n ≤ (a + b) ^ n + (a + b) ^ n
have h₁ : a ≤ a + b
Tactic: gcongr
-- 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
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
h₁ : a ≤ a + b
⊢ a ^ n + b ^ n ≤ (a + b) ^ n + (a + b) ^ n
have h₂ : b ≤ a + b
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
a : R
ha : a < 0
⊢ 0 < HPow.hPow (β := ℕ) a 2
have rw : 0 < a * a
Tactic: rw [sq]
-- 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 : IsOrderedRing R
inst_3 : ExistsAddOfLE R
n : ℕ
hn : Even n
a : R
⊢ 0 ≤ a ^ n
have obtain : ∀ (k : ℕ), 0 ≤ a ^ (k + k)
Tactic: obtain ⟨k, rfl⟩ := hn
Cleared hypotheses: n, 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 : IsOrderedRing R
inst_3 : ExistsAddOfLE R
a : R
k : ℕ
⊢ 0 ≤ a ^ (k + k)
have rw : 0 ≤ a ^ k * a ^ k
Tactic: rw [pow_add]
-- 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 : IsStrictOrderedRing R
a b : R
inst_3 : ExistsAddOfLE R
⊢ HPow.hPow (β := ℕ) (a + b) 2 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + (a * b + b * a)
have 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)
Tactic: simp_rw [pow_succ', pow_zero, mul_one, add_mul, mul_add, add_comm (b * a), add_add_add_comm]
-- 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 : 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)
⊢ HPow.hPow (β := ℕ) (a + b) 2 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + (a * b + b * a)
have simp_rw₁ : (a + b) * ((a + b) * 1) = a * (a * 1) + b * (b * 1) + (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]
-- 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 : 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)
⊢ HPow.hPow (β := ℕ) (a + b) 2 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + (a * b + b * a)
have simp_rw₂ : (a + b) * (a + b) = a * a + b * b + (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]
-- 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 : 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)
⊢ HPow.hPow (β := ℕ) (a + b) 2 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + (a * b + b * a)
have simp_rw₃ : a * (a + b) + b * (a + b) = a * a + b * b + (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]
-- 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 : 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)
⊢ HPow.hPow (β := ℕ) (a + b) 2 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + (a * b + b * a)
have simp_rw₄ : a * a + a * b + (b * a + b * b) = a * a + b * b + (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]
-- 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 : 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)
⊢ HPow.hPow (β := ℕ) (a + b) 2 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + (a * b + b * a)
have simp_rw₅ : a * a + a * b + (b * b + b * a) = a * a + b * b + (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]
-- 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 : IsStrictOrderedRing R
a b : R
inst_3 : ExistsAddOfLE R
⊢ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + (a * a + b * b) =
    2 * (HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2)
have 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))
Tactic: simp_rw [pow_succ', pow_zero, mul_one, two_mul]
-- 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 : 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))
⊢ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + (a * a + b * b) =
    2 * (HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2)
have simp_rw₁ : a * (a * 1) + b * (b * 1) + (a * a + b * b) = 2 * (a * (a * 1) + b * (b * 1))
Tactic: simp_rw [pow_succ', pow_zero, mul_one, two_mul]
-- 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 : 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))
⊢ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + (a * a + b * b) =
    2 * (HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2)
have simp_rw₂ : a * a + b * b + (a * a + b * b) = 2 * (a * a + b * b)
Tactic: simp_rw [pow_succ', pow_zero, mul_one, two_mul]
-- 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 : IsStrictOrderedRing R
a b : R
inst_3 : ExistsAddOfLE R
⊢ HPow.hPow (β := ℕ) (a + b) 2 ≤ 2 * (HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2)
have a₁ : a * b + b * a ≤ a * a + b * b
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]
-- 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 : IsStrictOrderedRing R
a b : R
inst_3 : ExistsAddOfLE R
⊢ a * b + b * a ≤ a * a + b * b
have inl : a ≤ b → a * b + b * a ≤ a * a + b * b
Tactic: cases le_total a b
-- 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 : IsStrictOrderedRing R
a b : R
inst_3 : ExistsAddOfLE R
inl : a ≤ b → a * b + b * a ≤ a * a + b * b
⊢ a * b + b * a ≤ a * a + b * b
have inr : b ≤ a → a * b + b * a ≤ a * a + b * b
Tactic: cases le_total a b
-- 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 : IsStrictOrderedRing R
a b : R
inst_3 : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ (a + b) ^ (n + 2) ≤ HPow.hPow (α := R) 2 (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))
have rw : (a + b) ^ (n + 1) * (a + b) ≤ HPow.hPow (α := R) 2 (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))
Tactic: rw [pow_succ]
-- 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 : IsStrictOrderedRing R
a b : R
inst_3 : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ HPow.hPow (α := R) 2 n * (a ^ (n + 1) + b ^ (n + 1)) * (a + b) =
    HPow.hPow (α := R) 2 n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a))
have rw : HPow.hPow (α := R) 2 n * ((a ^ (n + 1) + b ^ (n + 1)) * (a + b)) =
  HPow.hPow (α := R) 2 n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a))
Tactic: rw [mul_assoc, mul_add, add_mul, add_mul, ← pow_succ, ← pow_succ, add_comm _ (b ^ _),
            add_add_add_comm, add_comm (_ * a)]
-- 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 : IsStrictOrderedRing R
a b : R
inst_3 : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
rw :
  HPow.hPow (α := R) 2 n * ((a ^ (n + 1) + b ^ (n + 1)) * (a + b)) =
    HPow.hPow (α := R) 2 n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a))
⊢ HPow.hPow (α := R) 2 n * (a ^ (n + 1) + b ^ (n + 1)) * (a + b) =
    HPow.hPow (α := R) 2 n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a))
have rw₁ : HPow.hPow (α := R) 2 n * ((a ^ (n + 1) + b ^ (n + 1)) * a + (a ^ (n + 1) + b ^ (n + 1)) * b) =
  HPow.hPow (α := R) 2 n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a))
Tactic: rw [mul_assoc, mul_add, add_mul, add_mul, ← pow_succ, ← pow_succ, add_comm _ (b ^ _),
            add_add_add_comm, add_comm (_ * a)]
-- 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 : IsStrictOrderedRing R
a b : R
inst_3 : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
rw :
  HPow.hPow (α := R) 2 n * ((a ^ (n + 1) + b ^ (n + 1)) * (a + b)) =
    HPow.hPow (α := R) 2 n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a))
rw₁ :
  HPow.hPow (α := R) 2 n * ((a ^ (n + 1) + b ^ (n + 1)) * a + (a ^ (n + 1) + b ^ (n + 1)) * b) =
    HPow.hPow (α := R) 2 n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a))
⊢ HPow.hPow (α := R) 2 n * (a ^ (n + 1) + b ^ (n + 1)) * (a + b) =
    HPow.hPow (α := R) 2 n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a))
have rw₂ : HPow.hPow (α := R) 2 n * (a ^ (n + 1) * a + b ^ (n + 1) * a + (a ^ (n + 1) + b ^ (n + 1)) * b) =
  HPow.hPow (α := R) 2 n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a))
Tactic: rw [mul_assoc, mul_add, add_mul, add_mul, ← pow_succ, ← pow_succ, add_comm _ (b ^ _),
            add_add_add_comm, add_comm (_ * a)]