case zero
z x y p✝ : ℝ
n : ℕ
h✝ : ↑n ≤ p✝
p : ℝ
h : ↑Nat.zero ≤ p
⊢ ContDiff ℝ ↑Nat.zero fun x => x ^ p

case succ
z x y p✝ : ℝ
n✝ : ℕ
h✝ : ↑n✝ ≤ p✝
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑(Nat.succ n) ≤ p
⊢ ContDiff ℝ ↑(Nat.succ n) fun x => x ^ p
z x y p : ℝ
n : ℕ
h : ↑n ≤ p
⊢ ContDiff ℝ ↑n fun x => x ^ p
induction' n with n ihn generalizing p
no goals
case zero
z x y p✝ : ℝ
n : ℕ
h✝ : ↑n ≤ p✝
p : ℝ
h : ↑Nat.zero ≤ p
⊢ ContDiff ℝ ↑Nat.zero fun x => x ^ p
exact contDiff_zero.2 (continuous_id.rpow_const fun x => Or.inr <| by simpa using h)
no goals
z x✝ y p✝ : ℝ
n : ℕ
h✝ : ↑n ≤ p✝
p : ℝ
h : ↑Nat.zero ≤ p
x : ℝ
⊢ 0 ≤ p
simpa using h
case succ
z x y p✝ : ℝ
n✝ : ℕ
h✝ : ↑n✝ ≤ p✝
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑(Nat.succ n) ≤ p
h1 : 1 ≤ p
⊢ ContDiff ℝ ↑(Nat.succ n) fun x => x ^ p
case succ
z x y p✝ : ℝ
n✝ : ℕ
h✝ : ↑n✝ ≤ p✝
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑(Nat.succ n) ≤ p
⊢ ContDiff ℝ ↑(Nat.succ n) fun x => x ^ p
have h1 : 1 ≤ p := le_trans (by simp) h
case succ
z x y p✝ : ℝ
n✝ : ℕ
h✝ : ↑n✝ ≤ p✝
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑n ≤ p - 1
h1 : 1 ≤ p
⊢ ContDiff ℝ ↑(Nat.succ n) fun x => x ^ p
case succ
z x y p✝ : ℝ
n✝ : ℕ
h✝ : ↑n✝ ≤ p✝
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑(Nat.succ n) ≤ p
h1 : 1 ≤ p
⊢ ContDiff ℝ ↑(Nat.succ n) fun x => x ^ p
rw [Nat.cast_succ, ← le_sub_iff_add_le] at h
case succ
z x y p✝ : ℝ
n✝ : ℕ
h✝ : ↑n✝ ≤ p✝
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑n ≤ p - 1
h1 : 1 ≤ p
⊢ (Differentiable ℝ fun x => x ^ p) ∧ ContDiff ℝ ↑n fun x => p * x ^ (p - 1)
case succ
z x y p✝ : ℝ
n✝ : ℕ
h✝ : ↑n✝ ≤ p✝
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑n ≤ p - 1
h1 : 1 ≤ p
⊢ ContDiff ℝ ↑(Nat.succ n) fun x => x ^ p
rw [contDiff_succ_iff_deriv, deriv_rpow_const' h1]
no goals
case succ
z x y p✝ : ℝ
n✝ : ℕ
h✝ : ↑n✝ ≤ p✝
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑n ≤ p - 1
h1 : 1 ≤ p
⊢ (Differentiable ℝ fun x => x ^ p) ∧ ContDiff ℝ ↑n fun x => p * x ^ (p - 1)
refine' ⟨differentiable_rpow_const h1, contDiff_const.mul (ihn h)⟩
no goals
z x y p✝ : ℝ
n✝ : ℕ
h✝ : ↑n✝ ≤ p✝
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑(Nat.succ n) ≤ p
⊢ 1 ≤ ↑(Nat.succ n)
simp