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

State before:
n k : ℕ
⊢ n ≠ 0 → k ≠ 0 → n - k ≠ 0 → (n C k) = (n C n - k)
Tactic:
intros hn hk hnk
State after:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ (n C k) = (n C n - k)

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

State before:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n¡ / (k¡ * (n - k)¡) = n¡ / ((n - k)¡ * (n - (n - k))¡)
Tactic:
rewrite [mul_comm]
State after:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n¡ / ((n - k)¡ * k¡) = n¡ / ((n - k)¡ * (n - (n - k))¡)

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

n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k ≤ n

State before:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n¡ / ((n - k)¡ * k¡) = n¡ / ((n - k)¡ * k¡)

n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k ≤ n
Tactic:
{ reflexivity }
State after:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k ≤ n

State before:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k ≤ n
Tactic:
{ have : k < n
  { apply lt_of_not_le
    rewrite [← Nat.sub_eq_zero_iff_le]
    assumption }
  { linarith }
}
State after:
no goals

State before:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n¡ / ((n - k)¡ * k¡) = n¡ / ((n - k)¡ * k¡)
Tactic:
reflexivity
State after:
no goals

State before:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k ≤ n
Tactic:
have : k < n
State after:
case this
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k < n

n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
this : k < n
⊢ k ≤ n

State before:
case this
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k < n

n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
this : k < n
⊢ k ≤ n
Tactic:
{ apply lt_of_not_le
  rewrite [← Nat.sub_eq_zero_iff_le]
  assumption }
State after:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
this : k < n
⊢ k ≤ n

State before:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
this : k < n
⊢ k ≤ n
Tactic:
{ linarith }
State after:
no goals

State before:
case this
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k < n
Tactic:
apply lt_of_not_le
State after:
case this.h
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ ¬n ≤ k

State before:
case this.h
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ ¬n ≤ k
Tactic:
rewrite [← Nat.sub_eq_zero_iff_le]
State after:
case this.h
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ ¬n - k = 0

State before:
case this.h
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ ¬n - k = 0
Tactic:
assumption
State after:
no goals

State before:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
this : k < n
⊢ k ≤ n
Tactic:
linarith
State after:
no goals