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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hne : i ≠ j
⊢ card (MultiPart.P M i) + card (MultiPart.P M j) ≤ card M.A
Tactic:
rw [card_uni,← sum_erase_add (range (M.t + 1)) _ hj]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hne : i ≠ j
⊢ card (MultiPart.P M i) + card (MultiPart.P M j) ≤
    ∑ x in erase (range (M.t + 1)) j, card (MultiPart.P M x) + card (MultiPart.P M j)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hne : i ≠ j
⊢ card (MultiPart.P M i) + card (MultiPart.P M j) ≤
    ∑ x in erase (range (M.t + 1)) j, card (MultiPart.P M x) + card (MultiPart.P M j)
Tactic:
apply Nat.add_le_add_right
State after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hne : i ≠ j
⊢ card (MultiPart.P M i) ≤ ∑ x in erase (range (M.t + 1)) j, card (MultiPart.P M x)

State before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hne : i ≠ j
⊢ card (MultiPart.P M i) ≤ ∑ x in erase (range (M.t + 1)) j, card (MultiPart.P M x)
Tactic:
rw [← sum_erase_add ((range (M.t + 1)).erase j) _ (mem_erase_of_ne_of_mem hne hi)]
State after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hne : i ≠ j
⊢ card (MultiPart.P M i) ≤ ∑ x in erase (erase (range (M.t + 1)) j) i, card (MultiPart.P M x) + card (MultiPart.P M i)

State before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hne : i ≠ j
⊢ card (MultiPart.P M i) ≤ ∑ x in erase (erase (range (M.t + 1)) j) i, card (MultiPart.P M x) + card (MultiPart.P M i)
Tactic:
apply Nat.le_add_left
State after:
no goals