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

State before:
n k : ℕ
⊢ k ≤ n → (n C k) = (n C n - k)
Tactic:
intro hk_le_n
State after:
n k : ℕ
hk_le_n : k ≤ n
⊢ (n C k) = (n C n - k)

State before:
n k : ℕ
hk_le_n : k ≤ n
⊢ (n C k) = (n C n - k)
Tactic:
eliminate (eq_zero_or_ne_zero n) with hn hn
State after:
case inl
n k : ℕ
hk_le_n : k ≤ n
hn : n = 0
⊢ (n C k) = (n C n - k)

case inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
⊢ (n C k) = (n C n - k)

State before:
case inl
n k : ℕ
hk_le_n : k ≤ n
hn : n = 0
⊢ (n C k) = (n C n - k)

case inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
⊢ (n C k) = (n C n - k)
Tactic:
{
  sorry
}
State after:
case inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
⊢ (n C k) = (n C n - k)

State before:
case inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
⊢ (n C k) = (n C n - k)
Tactic:
{
  eliminate (eq_zero_or_ne_zero k) with hk hk
  {sorry}
  {
    eliminate (eq_zero_or_ne_zero (n - k)) with hnk hnk
    {
      sorry
    }
    {
      apply binomial_symmetry_helper
      {sorry}
      {sorry}
      {sorry}
    }
  }
}
State after:
no goals

State before:
case inl
n k : ℕ
hk_le_n : k ≤ n
hn : n = 0
⊢ (n C k) = (n C n - k)
Tactic:
sorry
State after:
no goals

State before:
case inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
⊢ (n C k) = (n C n - k)
Tactic:
eliminate (eq_zero_or_ne_zero k) with hk hk
State after:
case inr.inl
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k = 0
⊢ (n C k) = (n C n - k)

case inr.inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
⊢ (n C k) = (n C n - k)

State before:
case inr.inl
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k = 0
⊢ (n C k) = (n C n - k)

case inr.inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
⊢ (n C k) = (n C n - k)
Tactic:
{sorry}
State after:
case inr.inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
⊢ (n C k) = (n C n - k)

State before:
case inr.inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
⊢ (n C k) = (n C n - k)
Tactic:
{
  eliminate (eq_zero_or_ne_zero (n - k)) with hnk hnk
  {
    sorry
  }
  {
    apply binomial_symmetry_helper
    {sorry}
    {sorry}
    {sorry}
  }
}
State after:
no goals

State before:
case inr.inl
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k = 0
⊢ (n C k) = (n C n - k)
Tactic:
sorry
State after:
no goals

State before:
case inr.inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
⊢ (n C k) = (n C n - k)
Tactic:
eliminate (eq_zero_or_ne_zero (n - k)) with hnk hnk
State after:
case inr.inr.inl
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k = 0
⊢ (n C k) = (n C n - k)

case inr.inr.inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ (n C k) = (n C n - k)

State before:
case inr.inr.inl
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k = 0
⊢ (n C k) = (n C n - k)

case inr.inr.inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ (n C k) = (n C n - k)
Tactic:
{
  sorry
}
State after:
case inr.inr.inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ (n C k) = (n C n - k)

State before:
case inr.inr.inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ (n C k) = (n C n - k)
Tactic:
{
  apply binomial_symmetry_helper
  {sorry}
  {sorry}
  {sorry}
}
State after:
no goals

State before:
case inr.inr.inl
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k = 0
⊢ (n C k) = (n C n - k)
Tactic:
sorry
State after:
no goals

State before:
case inr.inr.inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ (n C k) = (n C n - k)
Tactic:
apply binomial_symmetry_helper
State after:
case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n ≠ 0

case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k ≠ 0

case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n - k ≠ 0

State before:
case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n ≠ 0

case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k ≠ 0

case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n - k ≠ 0
Tactic:
{sorry}
State after:
case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k ≠ 0

case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n - k ≠ 0

State before:
case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k ≠ 0

case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n - k ≠ 0
Tactic:
{sorry}
State after:
case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n - k ≠ 0

State before:
case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n - k ≠ 0
Tactic:
{sorry}
State after:
no goals

State before:
case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n ≠ 0
Tactic:
sorry
State after:
no goals

State before:
case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k ≠ 0
Tactic:
sorry
State after:
no goals

State before:
case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n - k ≠ 0
Tactic:
sorry
State after:
no goals