error with differentiable_at.div_const

Stream: new members

[Jake Levinson]

Here is an odd type inference error with differentiable_at.div_const. #mwe:

import analysis.calculus.deriv

example (x : ℝ) :
  differentiable_at ℝ (λ (y : ℝ), y / 2) x :=
begin
  apply differentiable_at.div_const,
  exact differentiable_at_id, -- This works fine.
end

Whereas the following one-line proofs fail:

  exact differentiable_at_id.div_const 2, -- type mismatch at application

  apply (@differentiable_at_id _ _ _ _ _ _).div_const 2, -- type mismatch at application

I think div_const is failing to infer one of the implicit parameters, because the following do work:

  -- these all work:
  apply (@differentiable_at_id ℝ _ ℝ _ _ x).div_const,
  apply (@differentiable_at_id ℝ _ _ _ _ _).div_const,
  apply (@differentiable_at_id _ _ ℝ _ _ _).div_const,
  apply (@differentiable_at_id _ _ _ _ _ x).div_const,

Changing 2 to (c : ℝ) gives the same errors, as does using differentiable_at_id'. The show_term tactic suggests exact differentiable_at_id.div_const 2 which generates an error.

The error message is:

type mismatch at application
  differentiable_at_id.div_const
term
  differentiable_at_id
has type
  differentiable_at ?m_1 id ?m_6
but is expected to have type
  differentiable_at ?m_1 ?m_6 ?m_7

[Jake Levinson]

Not sure what's going on with it.

[Floris van Doorn]

That is indeed surprising, it seems that Lean cannot elaborate differentiable_at.div_const differentiable_at_id (2 : ℝ) without knowing the expected type. Not sure what is causing that.

import analysis.calculus.deriv

example (x : ℝ) :
  differentiable_at ℝ (λ (y : ℝ), y / 2) x :=
begin
  -- have := differentiable_at.div_const differentiable_at_id (2 : ℝ), -- fails
  -- exact differentiable_at.div_const differentiable_at_id (2 : ℝ) -- succeeds
end

[Eric Wieser]

I think differentiable_at_id needs an explicit type argument?

[Floris van Doorn]

Yeah, that would solve it.

[Jake Levinson]

I think some other lemmas like differentiable_at_pow also have the same problem.