awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  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))
rw₈ 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))
⊢ 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)]

Premises used: add_mul, HMul.hMul, pow_succ, mul_assoc, add_comm, HPow.hPow, mul_add, add_add_add_comm
-- 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 : ℕ
ha₁ : 0 ≤ HPow.hPow (α := R) 2 n
hbc : a ^ (n + 1) * b + b ^ (n + 1) * a ≤ a ^ (n + 1) * a + 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 + 2) + b ^ (n + 2) + (a ^ (n + 1) * a + b ^ (n + 1) * b))

Tactic:
gcongr _ * (_ + _ + ?_)

Premises used: 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
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ 0 ≤ HPow.hPow (α := R) 2 n

Tactic:
pow_nonneg zero_le_two _

Premises used: pow_nonneg
-- 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 : ℕ
⊢ 0 ≤ HPow.hPow (α := R) 2 n

Tactic:
exact pow_nonneg zero_le_two _

Premises used: pow_nonneg
-- 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 : ℕ
hbc : ∀ (hab : a ≤ b), a ^ (n + 1) * b + b ^ (n + 1) * a ≤ a ^ (n + 1) * a + b ^ (n + 1) * b
hbc₁ : ∀ (hba : b ≤ a), 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

Tactic:
obtain hab | hba := 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
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
hab : a ≤ b
ha₁ : 0 ≤ a
⊢ a ^ (n + 1) ≤ b ^ (n + 1)

Tactic:
gcongr
-- 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 : ℕ
hab : a ≤ b
⊢ a ^ (n + 1) * b + b ^ (n + 1) * a ≤ a ^ (n + 1) * a + b ^ (n + 1) * b

Tactic:
exact mul_add_mul_le_mul_add_mul (by gcongr) hab

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
n : ℕ
hba : b ≤ a
ha₁ : 0 ≤ b
⊢ b ^ (n + 1) ≤ a ^ (n + 1)

Tactic:
gcongr
-- 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 : ℕ
hba : b ≤ a
⊢ a ^ (n + 1) * b + b ^ (n + 1) * a ≤ a ^ (n + 1) * a + b ^ (n + 1) * b

Tactic:
exact mul_add_mul_le_mul_add_mul' (by gcongr) hba

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
n : ℕ
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))
⊢ 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:
simp only [← pow_succ, ← two_mul, ← mul_assoc]

Premises used: pow_succ, mul_assoc, two_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
n : ℕ
⊢ 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:
rfl
-- 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 : ℕ
_ :
  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))
_₂ :
  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))
⊢ (a + b) ^ (n + 1) * (a + 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

Premises used: HMul.hMul, add_nonneg, mul_le_mul_of_nonneg_right, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- 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
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Even n
obtain : ∀ (n : ℕ), (a + b) ^ (n + n) ≤ HPow.hPow (α := R) 2 (n + n - 1) * (a ^ (n + n) + b ^ (n + n))
⊢ (a + b) ^ n ≤ HPow.hPow (α := R) 2 (n - 1) * (a ^ n + b ^ n)

Tactic:
obtain ⟨n, 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 : IsStrictOrderedRing R
a b : R
inst_3 : ExistsAddOfLE R
n : ℕ
rw : HPow.hPow (β := ℕ) (a + b) 2 ^ n ≤ HPow.hPow (α := R) 2 (2 * n - 1) * (a ^ (2 * n) + b ^ (2 * n))
⊢ (a + b) ^ (n + n) ≤ HPow.hPow (α := R) 2 (n + n - 1) * (a ^ (n + n) + b ^ (n + n))

Tactic:
rw [← two_mul, pow_mul]

Premises used: two_mul, pow_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
n : ℕ
⊢ HPow.hPow (β := ℕ) (a + b) 2 ^ n ≤ (2 * (HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2)) ^ n

Tactic:
pow_le_pow_left₀ (sq_nonneg _) add_sq_le _

Premises used: pow_le_pow_left₀, add_sq_le
-- 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
n : ℕ
h : Commute 2 (HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2)
⊢ (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:
rw [Commute.mul_pow]

Premises used: Commute.mul_pow
-- 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
n : ℕ
⊢ Commute 2 (HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2)

Tactic:
simp [Commute, SemiconjBy, two_mul, mul_two]

Premises used: SemiconjBy, Commute, two_mul, mul_two
-- 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
n : ℕ
⊢ HPow.hPow (α := R) 2 n * (HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2) ^ n ≤
    HPow.hPow (α := R) 2 n * (HPow.hPow (α := R) 2 (n - 1) * (HPow.hPow (β := ℕ) a 2 ^ n + HPow.hPow (β := ℕ) b 2 ^ n))

Tactic:
mul_le_mul_of_nonneg_left
          (add_pow_le (sq_nonneg _) (sq_nonneg _) _) <| pow_nonneg (zero_le_two (α := R)) _

Premises used: pow_nonneg, add_pow_le, sq_nonneg, zero_le_two, mul_le_mul_of_nonneg_left
-- 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
n : ℕ
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))
⊢ 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:
simp only [← mul_assoc, ← pow_add, ← pow_mul]

Premises used: mul_assoc, pow_add, pow_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
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)
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)))
⊢ 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:
cases n
-- 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 (α := 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:
rfl
-- 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
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:
simp [Nat.two_mul]

Premises used: Nat.two_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
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 (α := 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))
⊢ HPow.hPow (β := ℕ) (a + 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]

Premises used: HMul.hMul, pow_nonneg, HSub.hSub, pow_le_pow_left₀, add_pow_le, add_sq_le, HPow.hPow, HAdd.hAdd, sq_nonneg, zero_le_two, OfNat.ofNat, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Ring.Basic
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
ha : a ≠ 0
⊢ 0 < a ^ n

Tactic:
(hn.pow_nonneg _).lt_of_ne' (pow_ne_zero _ ha)

Premises used: Even.pow_nonneg, pow_ne_zero, LE.le.lt_of_ne'
-- Module: Mathlib.Algebra.Order.Ring.Basic
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
obtain : ∀ (k : ℕ) (h₀ : k + k ≠ 0), 0 < a ^ (k + k) ↔ a ≠ 0
⊢ 0 < a ^ n ↔ a ≠ 0

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 : IsStrictOrderedRing R
a : R
inst_3 : ExistsAddOfLE R
k : ℕ
h₀ : k + k ≠ 0
⊢ k ≠ 0

Tactic:
simpa using h₀
-- Module: Mathlib.Algebra.Order.Ring.Basic
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
rw₁ : a ^ k ≠ 0 ↔ a ≠ 0
rw₂ rw₃ : a ≠ 0 ↔ a ≠ 0
⊢ 0 < a ^ (k + k) ↔ a ≠ 0

Tactic:
rw [pow_add, mul_self_pos, pow_ne_zero_iff (by simpa using h₀)]

Premises used: pow_add, mul_self_pos, pow_ne_zero_iff
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
⊢ a ^ n < 0 ↔ a < 0

Tactic:
⟨lt_imp_lt_of_le_imp_le (pow_nonneg · _), fun ha ↦ ?_⟩

Premises used: pow_nonneg, Iff.intro, lt_imp_lt_of_le_imp_le
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
refine : ∀ (ha : a < 0), a ^ n < 0
⊢ a ^ n < 0 ↔ a < 0

Tactic:
refine ⟨lt_imp_lt_of_le_imp_le (pow_nonneg · _), fun ha ↦ ?_⟩
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
ha : a < 0
obtain : ∀ (k : ℕ), a ^ (2 * k + 1) < 0
⊢ a ^ n < 0

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 : IsStrictOrderedRing R
a : R
inst_3 : ExistsAddOfLE R
ha : a < 0
k : ℕ
rw : a ^ (2 * k) * a < 0
⊢ a ^ (2 * k + 1) < 0

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 : R
inst_3 : ExistsAddOfLE R
ha : a < 0
k : ℕ
⊢ a ^ (2 * k) * a < 0

Tactic:
mul_neg_of_pos_of_neg ((even_two_mul _).pow_pos ha.ne) ha

Premises used: Even.pow_pos, even_two_mul, mul_neg_of_pos_of_neg, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
inst_3 : ExistsAddOfLE R
ha : a < 0
k : ℕ
⊢ a ^ (2 * k) * a < 0

Tactic:
exact mul_neg_of_pos_of_neg ((even_two_mul _).pow_pos ha.ne) ha

Premises used: Even.pow_pos, even_two_mul, mul_neg_of_pos_of_neg, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
⊢ 0 ≤ a ^ n ↔ 0 ≤ a

Tactic:
le_iff_le_iff_lt_iff_lt.2 hn.pow_neg_iff

Premises used: Iff.mpr, le_iff_le_iff_lt_iff_lt, Odd.pow_neg_iff
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
rw : n ≠ 0
⊢ a ^ n ≤ 0 ↔ a ≤ 0

Tactic:
rw [le_iff_lt_or_eq, le_iff_lt_or_eq, hn.pow_neg_iff, pow_eq_zero_iff]

Premises used: pow_eq_zero_iff, Odd.pow_neg_iff, le_iff_lt_or_eq
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
inst_3 : ExistsAddOfLE R
hn : Odd (α := ℕ) 0
⊢ False

Tactic:
simp at hn
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
⊢ 0 < a ^ n ↔ 0 < a

Tactic:
lt_iff_lt_of_le_iff_le hn.pow_nonpos_iff

Premises used: lt_iff_lt_of_le_iff_le, Odd.pow_nonpos_iff
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
hn : Odd (α := ℕ) 0
⊢ False

Tactic:
simp [Odd] at hn

Premises used: Odd
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
⊢ n ≠ 0

Tactic:
have hn₀ : n ≠ 0 := by rintro rfl; simp [Odd] at hn
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
inl : ∀ (ha : 0 ≤ a), LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)
inr : ∀ (ha : a ≤ 0), LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)
⊢ LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)

Tactic:
obtain ha | ha := le_total 0 a

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : 0 ≤ a
⊢ LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)

Tactic:
pow_lt_pow_left₀ hab ha hn₀

Premises used: pow_lt_pow_left₀
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : 0 ≤ a
⊢ LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)

Tactic:
exact pow_lt_pow_left₀ hab ha hn₀

Premises used: pow_lt_pow_left₀
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
inr : ∀ (hb : 0 < b), LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)
inr₁ : ∀ (hb : b ≤ 0), LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)
⊢ LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)

Tactic:
obtain hb | hb := lt_or_ge 0 b

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : 0 < b
⊢ LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)

Tactic:
(hn.pow_nonpos ha).trans_lt (pow_pos hb _)

Premises used: pow_pos, Odd.pow_nonpos, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : 0 < b
⊢ LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)

Tactic:
exact (hn.pow_nonpos ha).trans_lt (pow_pos hb _)

Premises used: pow_pos, Odd.pow_nonpos, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
inr : ∀ (c : R) (hac : 0 = a + c), LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)
⊢ LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)

Tactic:
obtain ⟨c, hac⟩ := exists_add_of_le ha

Premises used: ExistsAddOfLE.exists_add_of_le
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
inr : ∀ (d : R) (hbd : 0 = b + d), LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)
⊢ LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)

Tactic:
obtain ⟨d, hbd⟩ := exists_add_of_le hb

Premises used: ExistsAddOfLE.exists_add_of_le
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
⊢ 0 ≤ d

Tactic:
have hd := nonneg_of_le_add_right (hb.trans_eq hbd)
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)

Tactic:
lt_of_add_lt_add_right (a := c ^ n + d ^ n) ?_

Premises used: lt_of_add_lt_add_right
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
inr : (fun (a : R) ↦ a ^ n) a + (c ^ n + d ^ n) < (fun (a : R) ↦ a ^ n) b + (c ^ n + d ^ n)
⊢ LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)

Tactic:
refine lt_of_add_lt_add_right (a := c ^ n + d ^ n) ?_

Premises used: lt_of_add_lt_add_right