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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
⊢ MultiPart.P M i ⊆ M.A
Tactic:
rw [M.uni]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
⊢ MultiPart.P M i ⊆ Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
⊢ MultiPart.P M i ⊆ Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
Tactic:
intro x hx
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
x : α
hx : x ∈ MultiPart.P M i
⊢ x ∈ Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
x : α
hx : x ∈ MultiPart.P M i
⊢ x ∈ Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
Tactic:
rw [mem_biUnion]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
x : α
hx : x ∈ MultiPart.P M i
⊢ ∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
x : α
hx : x ∈ MultiPart.P M i
⊢ ∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a
Tactic:
exact ⟨i, hi, hx⟩
State after:
no goals