Nat.choose_eq_one_iff

Stream: Is there code for X?

[Antoine Chambert-Loir]

I'm not particularly satisfied with this proof that cries for some golfing…

import Mathlib

theorem Nat.choose_eq_one_iff {n p : ℕ} : n.choose p = 1 ↔ p = 0 ∨ n = p := by
  rcases n.eq_zero_or_pos with ⟨rfl⟩ | hn
  · rcases p.eq_zero_or_pos with ⟨rfl⟩ | hp
    · simp
    · simp [Nat.choose_eq_zero_of_lt hp, eq_comm, Nat.ne_zero_of_lt hp]
  constructor
  · intro h
    rcases p.eq_zero_or_pos with ⟨rfl⟩ | hp
    · simp
    right
    apply le_antisymm
    · rw [← not_lt]
      intro hp'
      apply Nat.not_succ_le_self 1
      conv_rhs => rw [← h]
      rw [Nat.choose_eq_choose_pred_add hn hp]
      simp only [Nat.succ_eq_add_one]
      apply Nat.add_le_add <;>
        rw [Nat.one_le_iff_ne_zero, ne_eq, Nat.choose_eq_zero_iff, not_lt]
      · refine Nat.sub_le_sub_right ?_ 1
        apply le_of_lt hp'
      · exact (Nat.le_sub_one_iff_lt hn).mpr hp'
    · rw [← not_lt]
      intro hp'
      simp [Nat.choose_eq_zero_of_lt hp'] at h
  · rintro (rfl | rfl) <;> simp

[Kyle Miller]

This has a non-terminal simp... but it's a lot shorter:

import Mathlib

theorem Nat.choose_eq_one_iff {n p : ℕ} : n.choose p = 1 ↔ p = 0 ∨ n = p := by
  induction n generalizing p
    <;> cases p
    <;> simp [Nat.choose_succ_succ, Nat.add_eq_one_iff, Nat.choose_eq_zero_iff, *]
  omega

[Kyle Miller]

Here's a structured one:

import Mathlib

theorem Nat.choose_eq_one_iff {n p : ℕ} : n.choose p = 1 ↔ p = 0 ∨ n = p := by
  induction n generalizing p with
  | zero => cases p <;> simp
  | succ n ih =>
    cases p with
    | zero => simp
    | succ p =>
      simp only [Nat.choose_succ_succ, Nat.choose_eq_zero_iff, Nat.add_eq_one_iff, ih]
      omega

[Antoine Chambert-Loir]

great! docs#Nat.add_eq_one_iff is quite helpful!

[Jeremy Tan]

theorem Nat.choose_eq_one_iff {n k : ℕ} : n.choose k = 1 ↔ k = 0 ∨ n = k := by
  constructor <;> intro h
  · rcases lt_trichotomy k n with hk | rfl | hk
    · rw [← add_one_le_iff] at hk
      have := choose_mono k hk
      simp_rw [choose_succ_self_right, h] at this; omega
    · tauto
    · simp [choose_eq_zero_of_lt hk] at h
  · rcases h with rfl | rfl <;> simp

[Kenny Lau]

import Mathlib.Data.Nat.Choose.Basic

theorem Nat.choose_eq_one_iff {n k : ℕ} : n.choose k = 1 ↔ k = 0 ∨ n = k :=
  ⟨fun h ↦ or_iff_not_imp_right.2 fun hnk ↦ (lt_or_gt_of_ne hnk).elim
    (fun hnk ↦ Nat.zero_ne_one (choose_eq_zero_of_lt hnk ▸ h) |>.elim)
    (by simpa [h] using choose_mono k ·),
  fun h ↦ h.elim (· ▸ by simp) (· ▸ by simp)⟩

[Ruben Van de Velde]

That's scoring pretty poorly on the readability scale

[Eric Wieser]

Less readable?

theorem Nat.choose_pos_iff {n k : ℕ} : 0 < n.choose k ↔ k ≤ n :=
  ⟨fun h => le_of_not_gt fun h' => (choose_eq_zero_of_lt h').not_gt h, Nat.choose_pos⟩

theorem Nat.choose_eq_one_iff {n k : ℕ} : n.choose k = 1 ↔ k = 0 ∨ n = k where
  mp h := or_iff_not_imp_right.2 fun hnk ↦ by
    simpa [h] using choose_mono k <| lt_of_le_of_ne' (Nat.choose_pos_iff.mp <| by omega) hnk
  mpr | .inr rfl | .inl rfl => by simp

[Ruben Van de Velde]

That's a little better, so I made it worse again:

theorem Nat.choose_pos_iff {n k : ℕ} : 0 < n.choose k ↔ k ≤ n :=
  ⟨(le_of_not_gt <| mt choose_eq_zero_of_lt <| ne_of_gt ·), Nat.choose_pos⟩

[Kenny Lau]

Ruben Van de Velde said:

That's scoring pretty poorly on the readability scale

import Mathlib.Data.Nat.Choose.Basic

theorem Nat.choose_eq_one_iff {n k : ℕ} : n.choose k = 1 ↔ k = 0 ∨ n = k := by
  refine ⟨fun n_choose_k_eq_1 ↦ ?_, fun k_eq_0_or_n_eq_k ↦ ?_⟩
  · rcases lt_trichotomy k n with k_lt_n | rfl | n_lt_k
    · left; simpa [n_choose_k_eq_1] using choose_mono k k_lt_n
    · tauto
    · simp [choose_eq_zero_of_lt n_lt_k] at n_choose_k_eq_1
  · rcases k_eq_0_or_n_eq_k with rfl | rfl <;> simp

I've made it more like Jeremy's original proof

[Bhavik Mehta]

Ruben Van de Velde said:

That's a little better, so I made it worse again:

theorem Nat.choose_pos_iff {n k : ℕ} : 0 < n.choose k ↔ k ≤ n :=
  ⟨(le_of_not_gt <| mt choose_eq_zero_of_lt <| ne_of_gt ·), Nat.choose_pos⟩

theorem Nat.choose_pos_iff {n k : ℕ} : 0 < n.choose k ↔ k ≤ n := by
  simpa [pos_iff_ne_zero] using choose_eq_zero_iff.not