case inl
s : ℝ
hs : -1 ≤ s
hp : 1 ≤ 1
⊢ 1 + 1 * s ≤ (1 + s) ^ 1

case inr
s : ℝ
hs : -1 ≤ s
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ 1 + p * s ≤ (1 + s) ^ p
s : ℝ
hs : -1 ≤ s
p : ℝ
hp : 1 ≤ p
⊢ 1 + p * s ≤ (1 + s) ^ p
rcases eq_or_lt_of_le hp with (rfl | hp)
case pos
s : ℝ
hs : -1 ≤ s
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
hs' : s = 0
⊢ 1 + p * s ≤ (1 + s) ^ p

case neg
s : ℝ
hs : -1 ≤ s
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
hs' : ¬s = 0
⊢ 1 + p * s ≤ (1 + s) ^ p
case inr
s : ℝ
hs : -1 ≤ s
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ 1 + p * s ≤ (1 + s) ^ p
by_cases hs' : s = 0
no goals
case neg
s : ℝ
hs : -1 ≤ s
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
hs' : ¬s = 0
⊢ 1 + p * s ≤ (1 + s) ^ p
exact (one_add_mul_self_lt_rpow_one_add hs hs' hp).le
no goals
case inl
s : ℝ
hs : -1 ≤ s
hp : 1 ≤ 1
⊢ 1 + 1 * s ≤ (1 + s) ^ 1
simp
no goals
case pos
s : ℝ
hs : -1 ≤ s
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
hs' : s = 0
⊢ 1 + p * s ≤ (1 + s) ^ p
simp [hs']