turn iinequality of the natural numbers to cases

Stream: new members

[Siyuan Yan]

d : ℕ
a : ℤ
k : ℕ
hqd : d * k ≥ 2 ∧ d ≥ 2
hh : a.gcd ↑(d * k) = 1
H : ¬a.gcd ↑d = 1
hhh : a.gcd ↑d ≠ 1
⊢ false

Noting that the codomain of gcd is the natural numbers, how do I get a.gcd d = 0 ∨ a.gcd d > 1 from hhh?

[Michael Stoll]

docs#nat.one_lt_iff_ne_zero_and_ne_one could be helpful.

[Ruben Van de Velde]

I'd start with hhh.lt_or_lt

[Ruben Van de Velde]

And hope that docs#nat.lt_one_iff exists

[Siyuan Yan]

I tried have := a.gcd d = 0 ∨ a.gcd d > 1 := by library_searchbut nothing showed up. This makes me want to use by sorry so much.

[Ruben Van de Velde]

And it does, so

have := hhh.lt_or_lt,
rw nat.lt_one_iff at this,

should work

[Siyuan Yan]

thanks! I gotta be more familiar with the libraries

[Siyuan Yan]

And then how do I eliminate the a.gcd d = 0 disjunct? as hqd says d >= 2 and a.gcd d is only zero when both a and d are zero?

[Michael Stoll]

docs#nat.gcd_eq_zero_iff or docs#nat.eq_zero_of_gcd_eq_zero_right

[Julian Berman]

Another tip is to have a glance at https://leanprover-community.github.io/contribute/naming.html i.e. the naming conventions in mathlib -- good folks here basically can guess names of lemmas that seem like they should exist :) -- combining that with your editor's tab completion would likely have found ^

[Julian Berman]

(possibly via nat.gcd_iff<tab> or whatever)

[Michael Stoll]

I found these using the search box on the API documentation pages. Type "nat.gcd_eq_zero" there, and you'll get a list of things that probably contains what you are looking for.