Theorem: Nat.eq_of_dvd_of_lt_two_mul (LeanCamCombi/Mathlib/Data/Nat/Defs.lean)

State before:
a b : ℕ
ha : a ≠ 0
hdvd : b ∣ a
hlt : a < 2 * b
⊢ a = b
Tactic:
obtain ⟨_ | _ | c, rfl⟩ := hdvd
State after:
case intro.zero
b : ℕ
ha : b * 0 ≠ 0
hlt : b * 0 < 2 * b
⊢ b * 0 = b

case intro.succ.zero
b : ℕ
ha : b * (0 + 1) ≠ 0
hlt : b * (0 + 1) < 2 * b
⊢ b * (0 + 1) = b

case intro.succ.succ
b c : ℕ
ha : b * (c + 1 + 1) ≠ 0
hlt : b * (c + 1 + 1) < 2 * b
⊢ b * (c + 1 + 1) = b

State before:
case intro.zero
b : ℕ
ha : b * 0 ≠ 0
hlt : b * 0 < 2 * b
⊢ b * 0 = b
Tactic:
simp at ha
State after:
no goals

State before:
case intro.succ.zero
b : ℕ
ha : b * (0 + 1) ≠ 0
hlt : b * (0 + 1) < 2 * b
⊢ b * (0 + 1) = b
Tactic:
exact Nat.mul_one _
State after:
no goals

State before:
case intro.succ.succ
b c : ℕ
ha : b * (c + 1 + 1) ≠ 0
hlt : b * (c + 1 + 1) < 2 * b
⊢ b * (c + 1 + 1) = b
Tactic:
rw [Nat.mul_comm] at hlt
State after:
case intro.succ.succ
b c : ℕ
ha : b * (c + 1 + 1) ≠ 0
hlt : (c + 1 + 1) * b < 2 * b
⊢ b * (c + 1 + 1) = b

State before:
case intro.succ.succ
b c : ℕ
ha : b * (c + 1 + 1) ≠ 0
hlt : (c + 1 + 1) * b < 2 * b
⊢ b * (c + 1 + 1) = b
Tactic:
cases Nat.not_le_of_lt hlt (Nat.mul_le_mul_right _ (by omega))
State after:
no goals

State before:
b c : ℕ
ha : b * (c + 1 + 1) ≠ 0
hlt : (c + 1 + 1) * b < 2 * b
⊢ 2 ≤ c + 1 + 1
Tactic:
omega
State after:
no goals