Enumerate the factors of a small constant

Stream: new members

[AlumKal]

example {n : ℕ} (hn : n ∣ 6) : n = 1 ∨ n = 2 ∨ n = 3 ∨ n = 6 := sorry

How to elegantly prove this?

[Weiyi Wang]

oops one moment (edited

[Weiyi Wang]

example {n : ℕ} (hn : n ∣ 6) : n = 1 ∨ n = 2 ∨ n = 3 ∨ n = 6 := by
  have h : n ∈ Finset.Iic 6 := by simpa using Nat.le_of_dvd (by simp) hn
  fin_cases h <;> simp_all

[Kenny Lau]

Solution 1:

import Mathlib

lemma Nat.mem_divisors_iff {n m : ℕ} (hm : m ≠ 0) :
    n ∈ m.divisors ↔ n ∣ m :=
  ⟨(Nat.mem_divisors.1 · |>.1), (Nat.mem_divisors.2 ⟨·, hm⟩)⟩

example {n : ℕ} (hn : n ∣ 6) : n = 1 ∨ n = 2 ∨ n = 3 ∨ n = 6 := by
  rw [← Nat.mem_divisors_iff (by norm_num), show Nat.divisors 6 = {1, 2, 3, 6} from rfl] at hn
  simpa using hn

[Kenny Lau]

Solution 2:

import Mathlib

lemma Nat.mem_divisors_iff {n m : ℕ} (hm : m ≠ 0) :
    n ∈ m.divisors ↔ n ∣ m :=
  ⟨(Nat.mem_divisors.1 · |>.1), (Nat.mem_divisors.2 ⟨·, hm⟩)⟩

example {n : ℕ} (hn : n ∣ 6) : n = 1 ∨ n = 2 ∨ n = 3 ∨ n = 6 := by
  rw [← Nat.mem_divisors_iff (by norm_num)] at hn
  decide +revert

[Kenny Lau]

Solution 3:

import Mathlib

lemma Nat.mem_divisors_iff {n m : ℕ} (hm : m ≠ 0) :
    n ∈ m.divisors ↔ n ∣ m :=
  ⟨(Nat.mem_divisors.1 · |>.1), (Nat.mem_divisors.2 ⟨·, hm⟩)⟩

instance (p : ℕ → Prop) [DecidablePred p] (m : ℕ) : Decidable (∀ n, n ∣ m.succ → p n) :=
  decidable_of_iff (∀ n ∈ m.succ.divisors, p n)
    (by simp_rw [← Nat.mem_divisors_iff (Nat.succ_ne_zero m)])

example {n : ℕ} (hn : n ∣ 6) : n = 1 ∨ n = 2 ∨ n = 3 ∨ n = 6 := by
  decide +revert

[Eric Wieser]

There is now a simproc that can compute the factors for you

[Aaron Liu]

file#Tactic/Simproc/Divisors

[Aaron Liu]

import Mathlib

example {n : ℕ} (hn : n ∣ 6) : n = 1 ∨ n = 2 ∨ n = 3 ∨ n = 6 := by
  apply and_iff_left (show 6 ≠ 0 by norm_num) |>.mpr at hn
  rw [← Nat.mem_divisors] at hn
  dsimp [Nat.divisors_ofNat] at hn
  simpa using hn