-- Mathlib/Algebra/Order/Ring/Basic.lean
lemma Odd.strictMono_pow (hn : Odd n) : StrictMono fun a : R => a ^ n

Proof state:
case inr.inr.intro.intro
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : 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
⊢ (fun a => a ^ n) a + (c ^ n + d ^ n) < (fun a => a ^ n) b + (c ^ n + d ^ n)

Tactic:
dsimp

Result:
case inr.inr.intro.intro
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : 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
⊢ a ^ n + (c ^ n + d ^ n) < b ^ n + (c ^ n + d ^ n)

Proof state:
case inr.inr.intro.intro
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : 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
⊢ (fun a => a ^ n) a < (fun a => a ^ n) b

Tactic:
have hd := nonneg_of_le_add_right (hb.trans_eq hbd)

Result:
case inr.inr.intro.intro
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : 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
⊢ (fun a => a ^ n) a < (fun a => a ^ n) b

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
⊢ n ≠ 0

Tactic:
rintro rfl

Result:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
inst✝ : ExistsAddOfLE R
hn : Odd 0
⊢ False

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
⊢ StrictMono fun a => a ^ n

Tactic:
have hn₀ : n ≠ 0 := by rintro rfl; simp [Odd, eq_comm (a := 0)] at hn

Result:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
⊢ StrictMono fun a => a ^ n

Proof state:
case inr
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
⊢ (fun a => a ^ n) a < (fun a => a ^ n) b

Tactic:
obtain hb | hb := lt_or_le 0 b

Result:
case inr.inl
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : 0 < b
⊢ (fun a => a ^ n) a < (fun a => a ^ n) b

case inr.inr
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
⊢ (fun a => a ^ n) a < (fun a => a ^ n) b

Proof state:
case inr.inr.intro.intro
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : 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
⊢ d < c

Tactic:
refine lt_of_add_lt_add_right (a := a + b) ?_

Result:
case inr.inr.intro.intro
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : 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
⊢ d + (a + b) < c + (a + b)

Proof state:
case inr.inr
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
⊢ (fun a => a ^ n) a < (fun a => a ^ n) b

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

Result:
case inr.inr.intro
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : 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
⊢ (fun a => a ^ n) a < (fun a => a ^ n) b

Proof state:
case inl
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : 0 ≤ a
⊢ (fun a => a ^ n) a < (fun a => a ^ n) b

Tactic:
exact pow_lt_pow_left₀ hab ha hn₀

Result:
no goals

Proof state:
case inr.inr.intro
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : 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
⊢ (fun a => a ^ n) a < (fun a => a ^ n) b

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

Result:
case inr.inr.intro.intro
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : 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
⊢ (fun a => a ^ n) a < (fun a => a ^ n) b

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : 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
⊢ a ^ n + (c ^ n + d ^ n) = d ^ n

Tactic:
rw [← add_assoc, hn.pow_add_pow_eq_zero hac.symm, zero_add]

Result:
no goals

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : 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
⊢ c ^ n = b ^ n + (c ^ n + d ^ n)

Tactic:
rw [add_left_comm, hn.pow_add_pow_eq_zero hbd.symm, add_zero]

Result:
no goals

Proof state:
case inr.inl
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : 0 < b
⊢ (fun a => a ^ n) a < (fun a => a ^ n) b

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

Result:
no goals

Proof state:
case inr.inr.intro.intro
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : 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
⊢ d + (a + b) < c + (a + b)

Tactic:
rwa [add_rotate', ← hbd, add_zero, add_left_comm, ← add_assoc, ← hac, zero_add]

Result:
no goals

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
⊢ StrictMono fun a => a ^ n

Tactic:
intro a b hab

Result:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
⊢ (fun a => a ^ n) a < (fun a => a ^ n) b

Proof state:
case inr.inr.intro.intro
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : 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
⊢ (fun a => a ^ n) a < (fun a => a ^ n) b

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

Result:
case inr.inr.intro.intro
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : 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
⊢ (fun a => a ^ n) a + (c ^ n + d ^ n) < (fun a => a ^ n) b + (c ^ n + d ^ n)

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
⊢ (fun a => a ^ n) a < (fun a => a ^ n) b

Tactic:
obtain ha | ha := le_total 0 a

Result:
case inl
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : 0 ≤ a
⊢ (fun a => a ^ n) a < (fun a => a ^ n) b

case inr
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
⊢ (fun a => a ^ n) a < (fun a => a ^ n) b