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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ M.A = Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
Tactic:
ext x
State after:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
⊢ x ∈ M.A ↔ x ∈ Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i

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

State before:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
⊢ x ∈ M.A ↔ ∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a
Tactic:
constructor
State after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
⊢ x ∈ M.A → ∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a

case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
⊢ (∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a) → x ∈ M.A

State before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
⊢ x ∈ M.A → ∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a
Tactic:
intro hA
State after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
hA : x ∈ M.A
⊢ ∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a

State before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
hA : x ∈ M.A
⊢ ∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a
Tactic:
obtain ⟨i,hi⟩:= (inv_part hA)
State after:
case a.mp.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
hA : x ∈ M.A
i : ℕ
hi : i ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M i
⊢ ∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a

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

State before:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
⊢ (∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a) → x ∈ M.A
Tactic:
intro hA
State after:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
hA : ∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a
⊢ x ∈ M.A

State before:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
hA : ∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a
⊢ x ∈ M.A
Tactic:
obtain ⟨i, hi, hi2⟩ := hA
State after:
case a.mpr.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
i : ℕ
hi : i ∈ range (M.t + 1)
hi2 : x ∈ MultiPart.P M i
⊢ x ∈ M.A

State before:
case a.mpr.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
i : ℕ
hi : i ∈ range (M.t + 1)
hi2 : x ∈ MultiPart.P M i
⊢ x ∈ M.A
Tactic:
exact mem_part hi hi2
State after:
no goals