Derivatives question

Stream: new members

[Janitha Aswedige]

I was surprised that the following proof seemed to go on forever. Is there a different way to do it?

example {f : ℝ → ℝ} {x : ℝ} (hf : ∀ x, f x = 2 * x^4 + 3 * x^2 + 4 * x + 5) : deriv f x = 8 * x^3 + 6 * x + 4 := by
  have hf' : f = fun x ↦ 2 * x^4 + 3 * x^2 + 4 * x + 5 := by ext; apply hf
  rw [hf']
  rw [deriv_add, deriv_add, deriv_add]
  rw [deriv_const_mul, deriv_const_mul, deriv_const_mul]
  simp [deriv_pow, deriv_pow]
  ring
  exact differentiableAt_id'
  exact differentiableAt_pow 2
  exact differentiableAt_pow 4
  apply DifferentiableAt.const_mul
  exact differentiableAt_pow 4
  apply DifferentiableAt.const_mul
  exact differentiableAt_pow 2
  apply DifferentiableAt.add
  apply DifferentiableAt.const_mul
  exact differentiableAt_pow 4
  apply DifferentiableAt.const_mul
  exact differentiableAt_pow 2
  apply DifferentiableAt.const_mul
  exact differentiableAt_id'
  apply DifferentiableAt.add
  apply DifferentiableAt.add
  apply DifferentiableAt.const_mul
  exact differentiableAt_pow 4
  apply DifferentiableAt.const_mul
  exact differentiableAt_pow 2
  apply DifferentiableAt.const_mul
  exact differentiableAt_id'
  exact differentiableAt_const 5

[Chris Birkbeck]

does fun_prop do it?

[Janitha Aswedige]

That worked. thanks!