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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
⊢ M.A = M.A \ MultiPart.P M i ∪ MultiPart.P M i
Tactic:
have := sub_part hi
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
this : MultiPart.P M i ⊆ M.A
⊢ M.A = M.A \ MultiPart.P M i ∪ MultiPart.P M i

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
this : MultiPart.P M i ⊆ M.A
⊢ M.A = M.A \ MultiPart.P M i ∪ MultiPart.P M i
Tactic:
rwa [sdiff_union_self_eq_union, left_eq_union_iff_subset]
State after:
no goals