Theorem: Choose_expansion_of_pos_n_k (BrownCs22/Homework/Hw8.lean)

State before:
n k : ℕ
⊢ 0 < n → 0 < k → (n C k) = n¡ / (k¡ * (n - k)¡)
Tactic:
intro hn hk
State after:
n k : ℕ
hn : 0 < n
hk : 0 < k
⊢ (n C k) = n¡ / (k¡ * (n - k)¡)

State before:
n k : ℕ
hn : 0 < n
hk : 0 < k
⊢ (n C k) = n¡ / (k¡ * (n - k)¡)
Tactic:
rewrite [Nat.pos_iff_ne_zero] at *
State after:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
⊢ (n C k) = n¡ / (k¡ * (n - k)¡)

State before:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
⊢ (n C k) = n¡ / (k¡ * (n - k)¡)
Tactic:
simp [Choose]
State after:
no goals