Theorem: Turanpartition.two (Turan4/Turanpartition.lean)

State before:
a : ℕ
⊢ 2 * Nat.choose a 2 = a * (a - 1)
Tactic:
induction a with
| zero => rfl
| succ n ih => 
  cases n with
  | zero => rfl
  | succ n =>
    rw [Nat.choose,Nat.choose_one_right,mul_add,ih]
    rw [succ_sub_succ_eq_sub,tsub_zero,mul_comm _ n,← add_mul];
    congr; rw [add_comm]
State after:
no goals

State before:
case zero

⊢ 2 * Nat.choose zero 2 = zero * (zero - 1)
Tactic:
rfl
State after:
no goals

State before:
case succ
n : ℕ
ih : 2 * Nat.choose n 2 = n * (n - 1)
⊢ 2 * Nat.choose (succ n) 2 = succ n * (succ n - 1)
Tactic:
cases n with
| zero => rfl
| succ n =>
  rw [Nat.choose,Nat.choose_one_right,mul_add,ih]
  rw [succ_sub_succ_eq_sub,tsub_zero,mul_comm _ n,← add_mul];
  congr; rw [add_comm]
State after:
no goals

State before:
case succ.zero
ih : 2 * Nat.choose zero 2 = zero * (zero - 1)
⊢ 2 * Nat.choose (succ zero) 2 = succ zero * (succ zero - 1)
Tactic:
rfl
State after:
no goals

State before:
case succ.succ
n : ℕ
ih : 2 * Nat.choose (succ n) 2 = succ n * (succ n - 1)
⊢ 2 * Nat.choose (succ (succ n)) 2 = succ (succ n) * (succ (succ n) - 1)
Tactic:
rw [Nat.choose,Nat.choose_one_right,mul_add,ih]
State after:
case succ.succ
n : ℕ
ih : 2 * Nat.choose (succ n) 2 = succ n * (succ n - 1)
⊢ 2 * (n + 1) + succ n * (succ n - 1) = succ (succ n) * (succ (succ n) - 1)

State before:
case succ.succ
n : ℕ
ih : 2 * Nat.choose (succ n) 2 = succ n * (succ n - 1)
⊢ 2 * (n + 1) + succ n * (succ n - 1) = succ (succ n) * (succ (succ n) - 1)
Tactic:
rw [succ_sub_succ_eq_sub,tsub_zero,mul_comm _ n,← add_mul]
State after:
case succ.succ
n : ℕ
ih : 2 * Nat.choose (succ n) 2 = succ n * (succ n - 1)
⊢ (2 + n) * (n + 1) = succ (succ n) * (succ (succ n) - 1)

State before:
case succ.succ
n : ℕ
ih : 2 * Nat.choose (succ n) 2 = succ n * (succ n - 1)
⊢ (2 + n) * (n + 1) = succ (succ n) * (succ (succ n) - 1)
Tactic:
congr
State after:
case succ.succ.e_a
n : ℕ
ih : 2 * Nat.choose (succ n) 2 = succ n * (succ n - 1)
⊢ 2 + n = succ (succ n)

State before:
case succ.succ.e_a
n : ℕ
ih : 2 * Nat.choose (succ n) 2 = succ n * (succ n - 1)
⊢ 2 + n = succ (succ n)
Tactic:
rw [add_comm]
State after:
no goals