case inl.h
m n k l : ℕ
h : k + l = m + n - 1
h' : m ≤ k
⊢ m ≤ k

case inr.h
m n k l : ℕ
h : k + l = m + n - 1
h' : k < m
⊢ n ≤ l
m n k l : ℕ
h : k + l = m + n - 1
⊢ m ≤ k ∨ n ≤ l
cases' le_or_lt m k with h' h' <;> [left; right]
no goals
case inl.h
m n k l : ℕ
h : k + l = m + n - 1
h' : m ≤ k
⊢ m ≤ k
exact h'
case inr.h
m n k l : ℕ
h : k + l = m + n - 1
h' : k + l < m + l
⊢ n ≤ l
case inr.h
m n k l : ℕ
h : k + l = m + n - 1
h' : k < m
⊢ n ≤ l
replace h' := add_lt_add_right h' l
case inr.h
m n k l : ℕ
h : k + l = m + n - 1
h' : m + n - 1 < m + l
⊢ n ≤ l
case inr.h
m n k l : ℕ
h : k + l = m + n - 1
h' : k + l < m + l
⊢ n ≤ l
rw [h] at h'
case inr.h.inl
m n k l : ℕ
h : k + l = m + n - 1
h' : m + n - 1 < m + l
hn : n = 0
⊢ n ≤ l

case inr.h.inr
m n k l : ℕ
h : k + l = m + n - 1
h' : m + n - 1 < m + l
hn : n > 0
⊢ n ≤ l
case inr.h
m n k l : ℕ
h : k + l = m + n - 1
h' : m + n - 1 < m + l
⊢ n ≤ l
cases' n.eq_zero_or_pos with hn hn
case inr.h.inr
m n k l : ℕ
h : k + l = m + n - 1
h' : n - succ 0 < l
hn : n > 0
⊢ n ≤ l
case inr.h.inr
m n k l : ℕ
h : k + l = m + n - 1
h' : m + n - 1 < m + l
hn : n > 0
⊢ n ≤ l
rw [n.add_sub_assoc (Nat.succ_le_of_lt hn), add_lt_add_iff_left] at h'
no goals
case inr.h.inr
m n k l : ℕ
h : k + l = m + n - 1
h' : n - succ 0 < l
hn : n > 0
⊢ n ≤ l
exact Nat.le_of_pred_lt h'
case inr.h.inl
m n k l : ℕ
h : k + l = m + n - 1
h' : m + n - 1 < m + l
hn : n = 0
⊢ 0 ≤ l
case inr.h.inl
m n k l : ℕ
h : k + l = m + n - 1
h' : m + n - 1 < m + l
hn : n = 0
⊢ n ≤ l
rw [hn]
no goals
case inr.h.inl
m n k l : ℕ
h : k + l = m + n - 1
h' : m + n - 1 < m + l
hn : n = 0
⊢ 0 ≤ l
exact zero_le l