Int version of caseswork of divisors

Stream: Is there code for X?

[Kunhao Zheng]

Hi! I'm looking for a way to give proof of a similar statement here https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Easiest.20way.20to.20do.20casework.20on.20factors.20of.20.20nat/near/303342058

But my case is for int. Is there any lemma that deals with symmetry here? And do we have something like int.divisors?

example (n : int) : n ∣ 10 ↔ n = 1 ∨ n = 2  ∨ n = 5 ∨ n = 10 ∨ n = -1 ∨ n = -2 ∨ n = -5 ∨ n = -10 :=
begin
  sorry
end

Any hint welcome! Thank you in advance!

[Junyan Xu]

You may use docs#int.coe_nat_dvd_right applied to n=10, apply the method in the other thread to get n.nat_abs = 1,2,5,10, then rewrite by docs#int.nat_abs_eq_iff, then I imagine simp will get you there.

[Ruben Van de Velde]

And if simp doesn't do it, maybe tauto will

[Kunhao Zheng]

Thank you guys @Junyan Xu @Ruben Van de Velde! My simp or tauto cannot close that final goal, probably because my mathlib is a little bit old.

The last step just needs a bunch of docs#declarations-about-codeorcode.

But I found that finish can do the job!

example (n : int) : n ∣ 10 ↔ n = 1 ∨ n = 2  ∨ n = 5 ∨ n = 10 ∨ n = -1 ∨ n = -2 ∨ n = -5 ∨ n = -10 :=
begin
    intros n,
    have coe := @int.coe_nat_dvd_right 10 n,
    norm_cast at coe,
    rw coe,
    have h_div : nat.divisors 10 = ⟨quot.mk _ [1, 2, 5, 10], _⟩ := rfl,
    rw [← nat.mem_divisors.trans (and_iff_left (by norm_num : 10 ≠ 0)), h_div],
    change n.nat_abs ∈ (_:list _) ↔ _,
    simp only [list.mem_cons_iff, list.mem_singleton, int.nat_abs_eq_iff, int.coe_nat_succ, int.coe_nat_zero, zero_add,
  int.coe_nat_bit0, int.coe_nat_bit1],
    finish,
end