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

State before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
⊢ card (largeParts h) ≤ t
Tactic:
have := Nat.add_le_add (card_pos.mpr (small_nonempty h)) (le_refl (card (largeParts h)))
State after:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : succ 0 + card (largeParts h) ≤ card (smallParts h) + card (largeParts h)
⊢ card (largeParts h) ≤ t

State before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : succ 0 + card (largeParts h) ≤ card (smallParts h) + card (largeParts h)
⊢ card (largeParts h) ≤ t
Tactic:
rw [parts_card_add h,add_comm] at this
State after:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : card (largeParts h) + succ 0 ≤ t + 1
⊢ card (largeParts h) ≤ t

State before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : card (largeParts h) + succ 0 ≤ t + 1
⊢ card (largeParts h) ≤ t
Tactic:
apply  le_of_add_le_add_right this
State after:
no goals