feat(data/nat/with_bot): add nat.with_bot.add_eq_iff lemmas (#17629)

src/data/nat/order/basic.lean

@@ -177,11 +177,15 @@ iff.intro
     apply add_pos_right _ npos
   end
 
-lemma add_eq_one_iff : ∀ {a b : ℕ}, a + b = 1 ↔ (a = 0 ∧ b = 1) ∨ (a = 1 ∧ b = 0)
-| 0     0     := dec_trivial
-| 1     0     := dec_trivial
-| (a+2) _     := by rw add_right_comm; exact dec_trivial
-| _     (b+1) := by rw [← add_assoc]; simp only [nat.succ_inj', nat.succ_ne_zero]; simp
+lemma add_eq_one_iff : m + n = 1 ↔ m = 0 ∧ n = 1 ∨ m = 1 ∧ n = 0 :=
+by cases n; simp [succ_eq_add_one, ← add_assoc, succ_inj']
+
+lemma add_eq_two_iff : m + n = 2 ↔ m = 0 ∧ n = 2 ∨ m = 1 ∧ n = 1 ∨ m = 2 ∧ n = 0 :=
+by cases n; simp [(succ_ne_zero 1).symm, succ_eq_add_one, ← add_assoc, succ_inj', add_eq_one_iff]
+
+lemma add_eq_three_iff :
+  m + n = 3 ↔ m = 0 ∧ n = 3 ∨ m = 1 ∧ n = 2 ∨ m = 2 ∧ n = 1 ∨ m = 3 ∧ n = 0 :=
+by cases n; simp [(succ_ne_zero 1).symm, succ_eq_add_one, ← add_assoc, succ_inj', add_eq_two_iff]
 
 theorem le_add_one_iff {i j : ℕ} : i ≤ j + 1 ↔ (i ≤ j ∨ i = j + 1) :=
 ⟨λ h,

src/data/nat/with_bot.lean

@@ -11,43 +11,63 @@ import algebra.order.monoid.with_top
 
 Lemmas about the type of natural numbers with a bottom element adjoined.
 -/
+
 namespace nat
 
-lemma with_bot.add_eq_zero_iff : ∀ {n m : with_bot ℕ}, n + m = 0 ↔ n = 0 ∧ m = 0
-| none     m        := iff_of_false dec_trivial (λ h, absurd h.1 dec_trivial)
-| n        none     := iff_of_false (by cases n; exact dec_trivial)
-  (λ h, absurd h.2 dec_trivial)
-| (some n) (some m) := show (n + m : with_bot ℕ) = (0 : ℕ) ↔ (n : with_bot ℕ) = (0 : ℕ) ∧
-    (m : with_bot ℕ) = (0 : ℕ),
-  by rw [← with_bot.coe_add, with_bot.coe_eq_coe, with_bot.coe_eq_coe,
-    with_bot.coe_eq_coe, add_eq_zero_iff' (nat.zero_le _) (nat.zero_le _)]
-
-lemma with_bot.add_eq_one_iff : ∀ {n m : with_bot ℕ}, n + m = 1 ↔ (n = 0 ∧ m = 1) ∨ (n = 1 ∧ m = 0)
-| none     none     := dec_trivial
-| none     (some m) := dec_trivial
-| (some n) none     := iff_of_false dec_trivial (λ h, h.elim (λ h, absurd h.2 dec_trivial)
-  (λ h, absurd h.2 dec_trivial))
-| (some n) (some 0) := by erw [with_bot.coe_eq_coe, with_bot.coe_eq_coe, with_bot.coe_eq_coe,
-    with_bot.coe_eq_coe]; simp
-| (some n) (some (m + 1)) := by erw [with_bot.coe_eq_coe, with_bot.coe_eq_coe, with_bot.coe_eq_coe,
-    with_bot.coe_eq_coe, with_bot.coe_eq_coe]; simp [nat.add_succ, nat.succ_inj', nat.succ_ne_zero]
-
-@[simp] lemma with_bot.coe_nonneg {n : ℕ} : 0 ≤ (n : with_bot ℕ) :=
-by rw [← with_bot.coe_zero, with_bot.coe_le_coe]; exact nat.zero_le _
-
-@[simp] lemma with_bot.lt_zero_iff (n : with_bot ℕ) : n < 0 ↔ n = ⊥ :=
-option.cases_on n dec_trivial (λ n, iff_of_false
-  (by simp [with_bot.some_eq_coe]) (λ h, option.no_confusion h))
-
-lemma with_bot.one_le_iff_zero_lt {x : with_bot ℕ} : 1 ≤ x ↔ 0 < x :=
+namespace with_bot
+
+lemma add_eq_zero_iff {n m : with_bot ℕ} : n + m = 0 ↔ n = 0 ∧ m = 0 :=
+begin
+  rcases ⟨n, m⟩ with ⟨_ | _, _ | _⟩,
+  any_goals { tautology },
+  repeat { erw [with_bot.coe_eq_coe] },
+  exact add_eq_zero_iff
+end
+
+lemma add_eq_one_iff {n m : with_bot ℕ} : n + m = 1 ↔ n = 0 ∧ m = 1 ∨ n = 1 ∧ m = 0 :=
+begin
+  rcases ⟨n, m⟩ with ⟨_ | _, _ | _⟩,
+  any_goals { tautology },
+  repeat { erw [with_bot.coe_eq_coe] },
+  exact add_eq_one_iff
+end
+
+lemma add_eq_two_iff {n m : with_bot ℕ} :
+  n + m = 2 ↔ n = 0 ∧ m = 2 ∨ n = 1 ∧ m = 1 ∨ n = 2 ∧ m = 0 :=
+begin
+  rcases ⟨n, m⟩ with ⟨_ | _, _ | _⟩,
+  any_goals { tautology },
+  repeat { erw [with_bot.coe_eq_coe] },
+  exact add_eq_two_iff
+end
+
+lemma add_eq_three_iff {n m : with_bot ℕ} :
+  n + m = 3 ↔ n = 0 ∧ m = 3 ∨ n = 1 ∧ m = 2 ∨ n = 2 ∧ m = 1 ∨ n = 3 ∧ m = 0 :=
+begin
+  rcases ⟨n, m⟩ with ⟨_ | _, _ | _⟩,
+  any_goals { tautology },
+  repeat { erw [with_bot.coe_eq_coe] },
+  exact add_eq_three_iff
+end
+
+@[simp] lemma coe_nonneg {n : ℕ} : 0 ≤ (n : with_bot ℕ) :=
+by { rw [← with_bot.coe_zero, with_bot.coe_le_coe], exact nat.zero_le _ }
+
+@[simp] lemma lt_zero_iff (n : with_bot ℕ) : n < 0 ↔ n = ⊥ :=
+option.cases_on n dec_trivial $ λ n, iff_of_false
+  (by simp [with_bot.some_eq_coe]) (λ h, option.no_confusion h)
+
+lemma one_le_iff_zero_lt {x : with_bot ℕ} : 1 ≤ x ↔ 0 < x :=
 begin
   refine ⟨λ h, lt_of_lt_of_le (with_bot.coe_lt_coe.mpr zero_lt_one) h, λ h, _⟩,
   induction x using with_bot.rec_bot_coe,
   { exact (not_lt_bot h).elim },
   { exact with_bot.coe_le_coe.mpr (nat.succ_le_iff.mpr (with_bot.coe_lt_coe.mp h)) }
 end
 
-lemma with_bot.lt_one_iff_le_zero {x : with_bot ℕ} : x < 1 ↔ x ≤ 0 :=
-not_iff_not.mp (by simpa using with_bot.one_le_iff_zero_lt)
+lemma lt_one_iff_le_zero {x : with_bot ℕ} : x < 1 ↔ x ≤ 0 :=
+not_iff_not.mp (by simpa using one_le_iff_zero_lt)
+
+end with_bot
 
 end nat