Problems with obtain

Stream: new members

[Madison Crim]

Can someone please explain why I'm getting an error here?

import Mathlib

example {m n : ℕ } (h : Nat.Coprime m n) : ℕ := by
  have := Int.mod_coprime h
  obtain ⟨y,hy⟩ := this -- error : 'Exists.casesOn' can only eliminate into Prop
  sorry

[Madison Crim]

Actually, I'm just looking for a converse to #Nat.coprime_of_mul_modEq_one, namely that if $a$ and $n$ are coprime then there exists a natural number $b$ such that $a*b=1 \mod n$

[Madison Crim]

and I'm trying to obtain this $b$

[Damiano Testa]

For some information about the initial error, search "large elimination" on Zulip.

[Damiano Testa]

Basically, if your goal is in Prop, then you can obtain a witness for your existentials. This is fine, since you are building a proof.

However, this is not allowed to construct a term of an actual Type, like Nat in your case above, since it could lead into issues.

[Damiano Testa]

Nevertheless, if you really want to do it, choose can do it for you:

example {m n : ℕ } (h : Nat.Coprime m n) : ℕ := by
  have := Int.mod_coprime h
  choose y hy using this -- all good
  exact y.natAbs

and then you see that Lean wants you to make it as noncomputable, since your "definition" depends on an arbitrary choice.

[Kyle Miller]

Of course, this is a very computable thing, so there's no need for choice.

If you look at the definition of Int.mod_coprime (https://github.com/leanprover-community/mathlib4/blob/ee3c8402eccc71786028ca6017afbabc062c7e33/Mathlib/Data/Int/ModEq.lean#L241-L248) you can see that the witness it is using Nat.gcdA m n.

[Damiano Testa]

Oh, yes, I did not intend my answer as "this is how to do it in this case", just as "in a situation where this is your only option, you could proceed as follows"!