division_def not working?

Stream: new members

[Alex Kontorovich]

Stupid question: This seems to work just fine:

theorem exphomoinvC : Π (x y), complex.exp (x - y) = complex.exp x * ((complex.exp y)⁻¹) :=
begin
    intros,

    have expy: complex.exp (x-y) = complex.exp (x)/complex.exp (y),
    {
        exact complex.exp_sub x y,
    },
    rw expy,

    exact division_def,
end

But this fails???

theorem exphomoinv : Π (x y), real.exp (x - y) = real.exp x * ((real.exp y)⁻¹) :=
begin
    intros,

    have expy: real.exp (x-y) = real.exp (x)/ real.exp (y),
    {
        exact real.exp_sub x y,
    },
    rw expy,

    exact division_def,
    ---by library_search,
end

Any reason why it's not working? Thanks!

[Johan Commelin]

At what point does it fail? Which error do you get?

[Alex Kontorovich]

Whoops! Sorry, at the last step, division_def. Here's the error:

invalid type ascription, term has type
?m_3 / ?m_4 = ?m_3 * ?m_4⁻¹
but is expected to have type
real.exp x / real.exp y = real.exp x * (real.exp y)⁻¹
state:
x y : ℝ,
⊢ real.exp x / real.exp y = real.exp x * (real.exp y)⁻¹

[Johan Commelin]

What does #check @division_def say?

[Johan Commelin]

I don't know that lemma

[Rob Lewis]

@Alex Kontorovich It's very hard to debug code that we can't run ourselves. If you can post a #mwe you'll get better suggestions.

[Shing Tak Lam]

This works for Lean 3.20.0 and mathlib from about a week ago, importing just the file that defines real.exp/complex.exp, so I think we might need the information about Lean version/mathlib version as well.

import data.complex.exponential

theorem exphomoinv : Π (x y), real.exp (x - y) = real.exp x * ((real.exp y)⁻¹) :=
begin
    intros,

    have expy: real.exp (x-y) = real.exp (x)/ real.exp (y),
    {
        exact real.exp_sub x y,
    },
    rw expy,

    exact division_def,
end

[Alex Kontorovich]

Hmm how do I check my version? (I think I seem to have Lean-3.4.2?..)

[Heather Macbeth]

Try

#eval lean.version

[Alex Kontorovich]

Thanks! Output is: (3, (18, 4)). So maybe I just need to upload the latest version, and this issue will go away?...

[Heather Macbeth]

Yes, maybe! Although I'm not sure exactly what the relevant change would have been.

[Heather Macbeth]

You should be able to just run leanproject up at the command line.
https://leanprover-community.github.io/leanproject.html

[Shing Tak Lam]

ok, I just tried with 3.18.4 as well and it works. Git says no changes there for 3 months, so I don't expect mathlib/lean to be an issue. Alex Kontorovich can you post a #mwe (or just the whole file you're working in)?

[Alex Kontorovich]

Yeah, it works in the standalone code as you sent. Not sure what's going on... I'll come back to this. Thanks for your help!