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

State before:
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
⊢ a * (n - a) + b * (n - b) < (a - 1) * (n - a + 1) + (b + 1) * (n - b - 1)
Tactic:
rw [mul_add,add_mul,mul_one,one_mul]
State after:
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
⊢ a * (n - a) + b * (n - b) < (a - 1) * (n - a) + (a - 1) + (b * (n - b - 1) + (n - b - 1))

State before:
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
⊢ a * (n - a) + b * (n - b) < (a - 1) * (n - a) + (a - 1) + (b * (n - b - 1) + (n - b - 1))
Tactic:
have ha := tsub_add_cancel_of_le ((le_tsub_of_add_le_left hb.le).trans tsub_le_self : 1 ≤ a)
State after:
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
⊢ a * (n - a) + b * (n - b) < (a - 1) * (n - a) + (a - 1) + (b * (n - b - 1) + (n - b - 1))

State before:
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
⊢ a * (n - a) + b * (n - b) < (a - 1) * (n - a) + (a - 1) + (b * (n - b - 1) + (n - b - 1))
Tactic:
have h2 : a ≤ n - b := le_tsub_of_add_le_right hn
State after:
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
⊢ a * (n - a) + b * (n - b) < (a - 1) * (n - a) + (a - 1) + (b * (n - b - 1) + (n - b - 1))

State before:
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
⊢ a * (n - a) + b * (n - b) < (a - 1) * (n - a) + (a - 1) + (b * (n - b - 1) + (n - b - 1))
Tactic:
have hnb := tsub_add_cancel_of_le (le_trans ((le_tsub_of_add_le_left hb.le).trans tsub_le_self : 1 ≤ a) h2)
State after:
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
⊢ a * (n - a) + b * (n - b) < (a - 1) * (n - a) + (a - 1) + (b * (n - b - 1) + (n - b - 1))

State before:
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
⊢ a * (n - a) + b * (n - b) < (a - 1) * (n - a) + (a - 1) + (b * (n - b - 1) + (n - b - 1))
Tactic:
nth_rw 1 [← ha,← hnb]
State after:
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
⊢ (a - 1 + 1) * (n - a) + b * (n - b - 1 + 1) < (a - 1) * (n - a) + (a - 1) + (b * (n - b - 1) + (n - b - 1))

State before:
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
⊢ (a - 1 + 1) * (n - a) + b * (n - b - 1 + 1) < (a - 1) * (n - a) + (a - 1) + (b * (n - b - 1) + (n - b - 1))
Tactic:
rw [add_mul, mul_add, one_mul, mul_one, add_assoc, add_assoc]
State after:
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
⊢ (a - 1) * (n - a) + (n - a + (b * (n - b - 1) + b)) < (a - 1) * (n - a) + (a - 1 + (b * (n - b - 1) + (n - b - 1)))

State before:
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
⊢ (a - 1) * (n - a) + (n - a + (b * (n - b - 1) + b)) < (a - 1) * (n - a) + (a - 1 + (b * (n - b - 1) + (n - b - 1)))
Tactic:
apply Nat.add_lt_add_left
State after:
case h
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
⊢ n - a + (b * (n - b - 1) + b) < a - 1 + (b * (n - b - 1) + (n - b - 1))

State before:
case h
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
⊢ n - a + (b * (n - b - 1) + b) < a - 1 + (b * (n - b - 1) + (n - b - 1))
Tactic:
rw [add_comm, ← add_assoc, add_comm (a - 1), add_assoc, add_assoc]
State after:
case h
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
⊢ b * (n - b - 1) + (b + (n - a)) < b * (n - b - 1) + (a - 1 + (n - b - 1))

State before:
case h
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
⊢ b * (n - b - 1) + (b + (n - a)) < b * (n - b - 1) + (a - 1 + (n - b - 1))
Tactic:
apply Nat.add_lt_add_left
State after:
case h.h
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
⊢ b + (n - a) < a - 1 + (n - b - 1)

State before:
case h.h
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
⊢ b + (n - a) < a - 1 + (n - b - 1)
Tactic:
have ab : b < a - 1 := lt_tsub_of_add_lt_right hb
State after:
case h.h
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
ab : b < a - 1
⊢ b + (n - a) < a - 1 + (n - b - 1)

State before:
case h.h
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
ab : b < a - 1
⊢ b + (n - a) < a - 1 + (n - b - 1)
Tactic:
have nba : n - a < n - b - 1
State after:
case nba
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
ab : b < a - 1
⊢ n - a < n - b - 1

case h.h
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
ab : b < a - 1
nba : n - a < n - b - 1
⊢ b + (n - a) < a - 1 + (n - b - 1)

State before:
case h.h
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
ab : b < a - 1
nba : n - a < n - b - 1
⊢ b + (n - a) < a - 1 + (n - b - 1)
Tactic:
exact Nat.add_lt_add ab nba
State after:
no goals

State before:
case nba
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
ab : b < a - 1
⊢ n - a < n - b - 1
Tactic:
have nba' : n - a < n - (b + 1)
State after:
case nba'
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
ab : b < a - 1
⊢ n - a < n - (b + 1)

case nba
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
ab : b < a - 1
nba' : n - a < n - (b + 1)
⊢ n - a < n - b - 1

State before:
case nba
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
ab : b < a - 1
nba' : n - a < n - (b + 1)
⊢ n - a < n - b - 1
Tactic:
rwa [tsub_add_eq_tsub_tsub] at nba'
State after:
no goals

State before:
case nba'
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
ab : b < a - 1
⊢ n - a < n - (b + 1)
Tactic:
rw [tsub_lt_tsub_iff_left_of_le <| h2.trans tsub_le_self ]
State after:
case nba'
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
ab : b < a - 1
⊢ b + 1 < a

State before:
case nba'
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
ab : b < a - 1
⊢ b + 1 < a
Tactic:
exact tsub_pos_iff_lt.1 <|tsub_pos_of_lt hb
State after:
no goals