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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
M : MultiPart α
hA : v ∈ M.A
⊢ ∃ i, i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
Tactic:
rw [M.uni, mem_biUnion] at hA
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
M : MultiPart α
hA : ∃ a, a ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M a
⊢ ∃ i, i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i

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