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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
⊢ card M.A = card (M.A \ MultiPart.P M i) + card (MultiPart.P M i)
Tactic:
nth_rw 1 [sdiff_part hi]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
⊢ card (M.A \ MultiPart.P M i ∪ MultiPart.P M i) = card (M.A \ MultiPart.P M i) + card (MultiPart.P M i)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
⊢ card (M.A \ MultiPart.P M i ∪ MultiPart.P M i) = card (M.A \ MultiPart.P M i) + card (MultiPart.P M i)
Tactic:
apply card_disjoint_union sdiff_disjoint
State after:
no goals