-- Mathlib/Data/Nat/Init.lean
lemma succ_div : ∀ a b : ℕ, (a + 1) / b = a / b + if b ∣ a + 1 then 1 else 0
  | a, 0 => by simp
  | 0, 1 => by simp
  | 0, b + 2 => by
    have hb2 : b + 2 > 1

Proof state:
case pos
a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0

Tactic:
have h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1 := ⟨succ_pos _, Nat.add_le_add_iff_right.2 hb_le_a⟩

Result:
case pos
a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0

Proof state:
case pos
a b : ℕ
hb_eq_a : b = a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0

Tactic:
simp [hb_eq_a, Nat.le_refl, Nat.not_succ_le_self, Nat.dvd_refl]

Result:
no goals

Proof state:
b : ℕ
⊢ (0 + 1) / (b + 2) = 0 / (b + 2) + if b + 2 ∣ 0 + 1 then 1 else 0

Tactic:
have hb2 : b + 2 > 1 := by simp

Result:
b : ℕ
hb2 : b + 2 > 1
⊢ (0 + 1) / (b + 2) = 0 / (b + 2) + if b + 2 ∣ 0 + 1 then 1 else 0

Proof state:
b : ℕ
hb2 : b + 2 > 1
⊢ (0 + 1) / (b + 2) = 0 / (b + 2) + if b + 2 ∣ 0 + 1 then 1 else 0

Tactic:
simp [ne_of_gt hb2, div_eq_of_lt hb2]

Result:
no goals

Proof state:
case pos
a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
dvd_iff : b + 1 ∣ a - b + 1 ↔ b + 1 ∣ a + 1 + 1
wf : a - b < a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0

Tactic:
rw [if_pos h₁, if_pos h₂, Nat.add_sub_add_right, Nat.add_sub_add_right, Nat.add_comm a,
  Nat.add_sub_assoc hb_le_a, Nat.add_comm 1,
  have := wf
  succ_div (a - b)]

Result:
case pos
a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
dvd_iff : b + 1 ∣ a - b + 1 ↔ b + 1 ∣ a + 1 + 1
wf : a - b < a + 1
⊢ ((a - b) / (b + 1) + if b + 1 ∣ a - b + 1 then 1 else 0) + 1 =
    (a - b) / (b + 1) + 1 + if b + 1 ∣ 1 + a + 1 then 1 else 0

Proof state:
case neg
a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : ¬b ≤ a + 1
hba : ¬b ≤ a
hb_dvd_a : ¬b + 1 ∣ a + 2
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0

Tactic:
simp [hba, hb_le_a1, hb_dvd_a]

Result:
no goals

Proof state:
a : ℕ
⊢ (a + 1) / 0 = a / 0 + if 0 ∣ a + 1 then 1 else 0

Tactic:
simp

Result:
no goals

Proof state:
a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
⊢ b + 1 ∣ a - b + 1 ↔ b + 1 ∣ a + 1 + 1

Tactic:
rw [Nat.dvd_add_iff_left (Nat.dvd_refl (b + 1)), ← Nat.add_sub_add_right a 1 b,
  Nat.add_comm (_ - _), Nat.add_assoc, Nat.sub_add_cancel (succ_le_succ hb_le_a),
  Nat.add_comm 1]

Result:
no goals

Proof state:
case pos
a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0

Tactic:
have hb_le_a : b ≤ a := le_of_lt_succ (Nat.lt_of_le_of_ne hb_le_a1 hb_eq_a)

Result:
case pos
a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0

Proof state:
a b : ℕ
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0

Tactic:
by_cases hb_eq_a : b = a + 1

Result:
case pos
a b : ℕ
hb_eq_a : b = a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0

case neg
a b : ℕ
hb_eq_a : ¬b = a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0

Proof state:
a b : ℕ
⊢ (a + 1 + 1) / (b + 1) = (a + 1) / (b + 1) + if b + 1 ∣ a + 1 + 1 then 1 else 0

Tactic:
rw [Nat.div_eq]

Result:
a b : ℕ
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (a + 1) / (b + 1) + if b + 1 ∣ a + 1 + 1 then 1 else 0

Proof state:
case pos
a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0

Tactic:
have dvd_iff : b + 1 ∣ a - b + 1 ↔ b + 1 ∣ a + 1 + 1 := by
  rw [Nat.dvd_add_iff_left (Nat.dvd_refl (b + 1)), ← Nat.add_sub_add_right a 1 b,
    Nat.add_comm (_ - _), Nat.add_assoc, Nat.sub_add_cancel (succ_le_succ hb_le_a),
    Nat.add_comm 1]

Result:
case pos
a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
dvd_iff : b + 1 ∣ a - b + 1 ↔ b + 1 ∣ a + 1 + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0

Proof state:
case pos
a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
dvd_iff : b + 1 ∣ a - b + 1 ↔ b + 1 ∣ a + 1 + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0

Tactic:
have wf : a - b < a + 1 := lt_succ_of_le (Nat.sub_le _ _)

Result:
case pos
a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
dvd_iff : b + 1 ∣ a - b + 1 ↔ b + 1 ∣ a + 1 + 1
wf : a - b < a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0

Proof state:
case neg
a b : ℕ
hb_eq_a : ¬b = a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0

Tactic:
by_cases hb_le_a1 : b ≤ a + 1

Result:
case pos
a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0

case neg
a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : ¬b ≤ a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0