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 : 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))
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))
⊢ 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 + 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))
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))
rw₃ :
  HPow.hPow (α := R) 2 n * (a ^ (n + 1) * a + b ^ (n + 1) * a + (a ^ (n + 1) * b + 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 + 1) + b ^ (n + 1) * a + (a ^ (n + 1) * b + 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))
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))
rw₃ :
  HPow.hPow (α := R) 2 n * (a ^ (n + 1) * a + b ^ (n + 1) * a + (a ^ (n + 1) * b + b ^ (n + 1) * 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 + 1) + b ^ (n + 1) * a + (a ^ (n + 1) * b + 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 + 1) + b ^ (n + 1) * a + (a ^ (n + 1) * b + b ^ (n + 1 + 1))) =
  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))
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))
rw₃ :
  HPow.hPow (α := R) 2 n * (a ^ (n + 1) * a + b ^ (n + 1) * a + (a ^ (n + 1) * b + b ^ (n + 1) * 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 + 1) + b ^ (n + 1) * a + (a ^ (n + 1) * b + b ^ (n + 1) * 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 + 1) + b ^ (n + 1) * a + (a ^ (n + 1) * b + b ^ (n + 1 + 1))) =
    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 + 1) + b ^ (n + 1) * a + (b ^ (n + 1 + 1) + a ^ (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))
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))
rw₃ :
  HPow.hPow (α := R) 2 n * (a ^ (n + 1) * a + b ^ (n + 1) * a + (a ^ (n + 1) * b + b ^ (n + 1) * 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 + 1) + b ^ (n + 1) * a + (a ^ (n + 1) * b + b ^ (n + 1) * 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 + 1) + b ^ (n + 1) * a + (a ^ (n + 1) * b + b ^ (n + 1 + 1))) =
    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 + 1) + b ^ (n + 1) * a + (b ^ (n + 1 + 1) + a ^ (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 + 1) + b ^ (n + 1 + 1) + (b ^ (n + 1) * a + a ^ (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))
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))
rw₃ :
  HPow.hPow (α := R) 2 n * (a ^ (n + 1) * a + b ^ (n + 1) * a + (a ^ (n + 1) * b + b ^ (n + 1) * 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 + 1) + b ^ (n + 1) * a + (a ^ (n + 1) * b + b ^ (n + 1) * 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 + 1) + b ^ (n + 1) * a + (a ^ (n + 1) * b + b ^ (n + 1 + 1))) =
    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 + 1) + b ^ (n + 1) * a + (b ^ (n + 1 + 1) + a ^ (n + 1) * 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 + 1) + b ^ (n + 1 + 1) + (b ^ (n + 1) * a + a ^ (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 + 1) + b ^ (n + 1 + 1) + (a ^ (n + 1) * b + b ^ (n + 1) * a)) =
  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 : ℕ
⊢ 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 + 2) + b ^ (n + 2) + (a ^ (n + 1) * a + b ^ (n + 1) * b))
have ha₁ : 0 ≤ HPow.hPow (α := R) 2 n
Tactic: gcongr _ * (_ + _ + ?_)
-- 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 : ℕ
ha₁ : 0 ≤ HPow.hPow (α := R) 2 n
⊢ 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 + 2) + b ^ (n + 2) + (a ^ (n + 1) * a + b ^ (n + 1) * b))
have hbc : a ^ (n + 1) * b + b ^ (n + 1) * a ≤ a ^ (n + 1) * a + b ^ (n + 1) * b
Tactic: gcongr _ * (_ + _ + ?_)
-- 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 ^ (n + 1) * b + b ^ (n + 1) * a ≤ a ^ (n + 1) * a + b ^ (n + 1) * b
have hbc : ∀ (hab : a ≤ b), a ^ (n + 1) * b + b ^ (n + 1) * a ≤ a ^ (n + 1) * a + b ^ (n + 1) * b
Tactic: obtain hab | hba := 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 : ℕ
hbc : ∀ (hab : a ≤ b), a ^ (n + 1) * b + b ^ (n + 1) * a ≤ a ^ (n + 1) * a + b ^ (n + 1) * b
⊢ a ^ (n + 1) * b + b ^ (n + 1) * a ≤ a ^ (n + 1) * a + b ^ (n + 1) * b
have hbc₁ : ∀ (hba : b ≤ a), a ^ (n + 1) * b + b ^ (n + 1) * a ≤ a ^ (n + 1) * a + b ^ (n + 1) * b
Tactic: obtain hab | hba := 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 : ℕ
⊢ HPow.hPow (α := R) 2 n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * a + b ^ (n + 1) * b)) =
    HPow.hPow (α := R) 2 (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))
have simp : HPow.hPow (α := R) 2 (n + 1) * (a ^ (n + 2) + b ^ (n + 2)) =
  HPow.hPow (α := R) 2 (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))
Tactic: simp only [← pow_succ, ← two_mul, ← mul_assoc]
-- 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 + 1) * (a + b) ≤ HPow.hPow (α := R) 2 (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))
have _ : 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: calc
      _ ≤ 2 ^ n * (a ^ (n + 1) + b ^ (n + 1)) * (a + b) :=
          mul_le_mul_of_nonneg_right (add_pow_le ha hb (n + 1)) <| add_nonneg ha hb
      _ = 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a)) := by
          rw [mul_assoc, mul_add, add_mul, add_mul, ← pow_succ, ← pow_succ, add_comm _ (b ^ _),
            add_add_add_comm, add_comm (_ * a)]
      _ ≤ 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * a + b ^ (n + 1) * b)) := by
        gcongr _ * (_ + _ + ?_)
        · exact pow_nonneg zero_le_two _
        obtain hab | hba := le_total a b
        · exact mul_add_mul_le_mul_add_mul (by gcongr) hab
        · exact mul_add_mul_le_mul_add_mul' (by gcongr) hba
      _ = _ := by simp only [← pow_succ, ← two_mul, ← mul_assoc]; rfl
-- 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))
⊢ (a + b) ^ (n + 1) * (a + b) ≤ HPow.hPow (α := R) 2 (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))
have _₁ : 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 + 2) + b ^ (n + 2) + (a ^ (n + 1) * a + b ^ (n + 1) * b))
Tactic: calc
      _ ≤ 2 ^ n * (a ^ (n + 1) + b ^ (n + 1)) * (a + b) :=
          mul_le_mul_of_nonneg_right (add_pow_le ha hb (n + 1)) <| add_nonneg ha hb
      _ = 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a)) := by
          rw [mul_assoc, mul_add, add_mul, add_mul, ← pow_succ, ← pow_succ, add_comm _ (b ^ _),
            add_add_add_comm, add_comm (_ * a)]
      _ ≤ 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * a + b ^ (n + 1) * b)) := by
        gcongr _ * (_ + _ + ?_)
        · exact pow_nonneg zero_le_two _
        obtain hab | hba := le_total a b
        · exact mul_add_mul_le_mul_add_mul (by gcongr) hab
        · exact mul_add_mul_le_mul_add_mul' (by gcongr) hba
      _ = _ := by simp only [← pow_succ, ← two_mul, ← mul_assoc]; rfl
-- 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))
_₁ :
  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 + 2) + b ^ (n + 2) + (a ^ (n + 1) * a + b ^ (n + 1) * b))
⊢ (a + b) ^ (n + 1) * (a + b) ≤ HPow.hPow (α := R) 2 (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))
have _₂ : HPow.hPow (α := R) 2 n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * a + b ^ (n + 1) * b)) =
  HPow.hPow (α := R) 2 (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))
Tactic: calc
      _ ≤ 2 ^ n * (a ^ (n + 1) + b ^ (n + 1)) * (a + b) :=
          mul_le_mul_of_nonneg_right (add_pow_le ha hb (n + 1)) <| add_nonneg ha hb
      _ = 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a)) := by
          rw [mul_assoc, mul_add, add_mul, add_mul, ← pow_succ, ← pow_succ, add_comm _ (b ^ _),
            add_add_add_comm, add_comm (_ * a)]
      _ ≤ 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * a + b ^ (n + 1) * b)) := by
        gcongr _ * (_ + _ + ?_)
        · exact pow_nonneg zero_le_two _
        obtain hab | hba := le_total a b
        · exact mul_add_mul_le_mul_add_mul (by gcongr) hab
        · exact mul_add_mul_le_mul_add_mul' (by gcongr) hba
      _ = _ := by simp only [← pow_succ, ← two_mul, ← mul_assoc]; rfl
-- 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
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Even n
⊢ (a + b) ^ n ≤ HPow.hPow (α := R) 2 (n - 1) * (a ^ n + b ^ n)
have obtain : ∀ (n : ℕ), (a + b) ^ (n + n) ≤ HPow.hPow (α := R) 2 (n + n - 1) * (a ^ (n + n) + b ^ (n + n))
Tactic: obtain ⟨n, 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 : IsStrictOrderedRing R
a b : R
inst_3 : ExistsAddOfLE R
n : ℕ
⊢ (a + b) ^ (n + n) ≤ HPow.hPow (α := R) 2 (n + n - 1) * (a ^ (n + n) + b ^ (n + n))
have rw : HPow.hPow (β := ℕ) (a + b) 2 ^ n ≤ HPow.hPow (α := R) 2 (2 * n - 1) * (a ^ (2 * n) + b ^ (2 * n))
Tactic: rw [← two_mul, pow_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
n : ℕ
⊢ (2 * (HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2)) ^ n =
    HPow.hPow (α := R) 2 n * (HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2) ^ n
have h : Commute 2 (HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2)
Tactic: rw [Commute.mul_pow]
-- 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
n : ℕ
⊢ HPow.hPow (α := R) 2 n * (HPow.hPow (α := R) 2 (n - 1) * (HPow.hPow (β := ℕ) a 2 ^ n + HPow.hPow (β := ℕ) b 2 ^ n)) =
    HPow.hPow (α := R) 2 (2 * n - 1) * (a ^ (2 * n) + b ^ (2 * n))
have simp : HPow.hPow (α := R) 2 (n + (n - 1)) * (a ^ (2 * n) + b ^ (2 * n)) =
  HPow.hPow (α := R) 2 (2 * n - 1) * (a ^ (2 * n) + b ^ (2 * n))
Tactic: simp only [← mul_assoc, ← pow_add, ← pow_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
n : ℕ
⊢ HPow.hPow (α := R) 2 (n + (n - 1)) * (a ^ (2 * n) + b ^ (2 * n)) =
    HPow.hPow (α := R) 2 (2 * n - 1) * (a ^ (2 * n) + b ^ (2 * n))
have zero : HPow.hPow (α := R) 2 (0 + HSub.hSub (α := ℕ) 0 1) * (a ^ HMul.hMul (α := ℕ) 2 0 + b ^ HMul.hMul (α := ℕ) 2 0) =
  HPow.hPow (α := R) 2 (HMul.hMul (α := ℕ) 2 0 - 1) * (a ^ HMul.hMul (α := ℕ) 2 0 + b ^ HMul.hMul (α := ℕ) 2 0)
Tactic: cases n
Cleared hypotheses: n
-- 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
n : ℕ
zero :
  HPow.hPow (α := R) 2 (0 + HSub.hSub (α := ℕ) 0 1) * (a ^ HMul.hMul (α := ℕ) 2 0 + b ^ HMul.hMul (α := ℕ) 2 0) =
    HPow.hPow (α := R) 2 (HMul.hMul (α := ℕ) 2 0 - 1) * (a ^ HMul.hMul (α := ℕ) 2 0 + b ^ HMul.hMul (α := ℕ) 2 0)
⊢ HPow.hPow (α := R) 2 (n + (n - 1)) * (a ^ (2 * n) + b ^ (2 * n)) =
    HPow.hPow (α := R) 2 (2 * n - 1) * (a ^ (2 * n) + b ^ (2 * n))
have succ : ∀ (n : ℕ),
  HPow.hPow (α := R) 2 (n + 1 + (n + 1 - 1)) * (a ^ (2 * (n + 1)) + b ^ (2 * (n + 1))) =
    HPow.hPow (α := R) 2 (2 * (n + 1) - 1) * (a ^ (2 * (n + 1)) + b ^ (2 * (n + 1)))
Tactic: cases n
Cleared hypotheses: n
-- 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
n : ℕ
⊢ HPow.hPow (β := ℕ) (a + b) 2 ^ n ≤ HPow.hPow (α := R) 2 (2 * n - 1) * (a ^ (2 * n) + b ^ (2 * n))
have _ : (2 * (HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2)) ^ n =
  HPow.hPow (α := R) 2 n * (HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2) ^ n
Tactic: calc
    _ ≤ (2 * (a ^ 2 + b ^ 2)) ^ n := pow_le_pow_left₀ (sq_nonneg _) add_sq_le _
    _ = 2 ^ n * (a ^ 2 + b ^ 2) ^ n := by -- TODO: Should be `Nat.cast_commute`
        rw [Commute.mul_pow]; simp [Commute, SemiconjBy, two_mul, mul_two]
    _ ≤ 2 ^ n * (2 ^ (n - 1) * ((a ^ 2) ^ n + (b ^ 2) ^ n)) := mul_le_mul_of_nonneg_left
          (add_pow_le (sq_nonneg _) (sq_nonneg _) _) <| pow_nonneg (zero_le_two (α := R)) _
    _ = _ := by
      simp only [← mul_assoc, ← pow_add, ← pow_mul]
      cases n
      · rfl
      · simp [Nat.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
n : ℕ
_ :
  (2 * (HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2)) ^ n =
    HPow.hPow (α := R) 2 n * (HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2) ^ n
⊢ HPow.hPow (β := ℕ) (a + b) 2 ^ n ≤ HPow.hPow (α := R) 2 (2 * n - 1) * (a ^ (2 * n) + b ^ (2 * n))
have _₁ : HPow.hPow (α := R) 2 n * (HPow.hPow (α := R) 2 (n - 1) * (HPow.hPow (β := ℕ) a 2 ^ n + HPow.hPow (β := ℕ) b 2 ^ n)) =
  HPow.hPow (α := R) 2 (2 * n - 1) * (a ^ (2 * n) + b ^ (2 * n))
Tactic: calc
    _ ≤ (2 * (a ^ 2 + b ^ 2)) ^ n := pow_le_pow_left₀ (sq_nonneg _) add_sq_le _
    _ = 2 ^ n * (a ^ 2 + b ^ 2) ^ n := by -- TODO: Should be `Nat.cast_commute`
        rw [Commute.mul_pow]; simp [Commute, SemiconjBy, two_mul, mul_two]
    _ ≤ 2 ^ n * (2 ^ (n - 1) * ((a ^ 2) ^ n + (b ^ 2) ^ n)) := mul_le_mul_of_nonneg_left
          (add_pow_le (sq_nonneg _) (sq_nonneg _) _) <| pow_nonneg (zero_le_two (α := R)) _
    _ = _ := by
      simp only [← mul_assoc, ← pow_add, ← pow_mul]
      cases n
      · rfl
      · simp [Nat.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 : R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Even n
h₀ : n ≠ 0
⊢ 0 < a ^ n ↔ a ≠ 0
have obtain : ∀ (k : ℕ) (h₀ : k + k ≠ 0), 0 < a ^ (k + k) ↔ a ≠ 0
Tactic: obtain ⟨k, rfl⟩ := hn
Cleared hypotheses: n, hn, h₀
-- 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 : R
inst_3 : ExistsAddOfLE R
k : ℕ
h₀ : k + k ≠ 0
⊢ 0 < a ^ (k + k) ↔ a ≠ 0
have rw : 0 < a ^ k * a ^ k ↔ a ≠ 0
Tactic: rw [pow_add, mul_self_pos, pow_ne_zero_iff (by simpa using h₀)]
-- 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 : R
inst_3 : ExistsAddOfLE R
k : ℕ
h₀ : k + k ≠ 0
rw : 0 < a ^ k * a ^ k ↔ a ≠ 0
⊢ 0 < a ^ (k + k) ↔ a ≠ 0
have rw₁ : a ^ k ≠ 0 ↔ a ≠ 0
Tactic: rw [pow_add, mul_self_pos, pow_ne_zero_iff (by simpa using h₀)]