n a b : ℕ
h : n = a + b
this : choose n (n - b) = choose n b
⊢ choose n a = choose n b

case this
n a b : ℕ
h : n = a + b
⊢ choose n (n - b) = choose n b
n a b : ℕ
h : n = a + b
⊢ choose n a = choose n b
suffices : choose n (n - b) = choose n b
case this
n a b : ℕ
h : n = a + b
⊢ choose n (n - b) = choose n b
n a b : ℕ
h : n = a + b
this : choose n (n - b) = choose n b
⊢ choose n a = choose n b

case this
n a b : ℕ
h : n = a + b
⊢ choose n (n - b) = choose n b
. rw [h, add_tsub_cancel_right] at this; rwa [h]
no goals
case this
n a b : ℕ
h : n = a + b
⊢ choose n (n - b) = choose n b
exact choose_symm (h ▸ le_add_left _ _)
n a b : ℕ
h : n = a + b
this : choose (a + b) a = choose (a + b) b
⊢ choose n a = choose n b
n a b : ℕ
h : n = a + b
this : choose n (n - b) = choose n b
⊢ choose n a = choose n b
rw [h, add_tsub_cancel_right] at this
no goals
n a b : ℕ
h : n = a + b
this : choose (a + b) a = choose (a + b) b
⊢ choose n a = choose n b
rwa [h]