Theorem: Turanpartition.insert_P' (Turan4/Turanpartition.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
M : MultiPart α
h : Disjoint M.A B
⊢ ∀ (v : α), v ∈ B → v ∈ MultiPart.P (minsert M h) (M.t + 1)
Tactic:
intro v hv
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
M : MultiPart α
h : Disjoint M.A B
v : α
hv : v ∈ B
⊢ v ∈ MultiPart.P (minsert M h) (M.t + 1)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
M : MultiPart α
h : Disjoint M.A B
v : α
hv : v ∈ B
⊢ v ∈ MultiPart.P (minsert M h) (M.t + 1)
Tactic:
rw [insert_P]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
M : MultiPart α
h : Disjoint M.A B
v : α
hv : v ∈ B
⊢ v ∈ if M.t + 1 ≠ M.t + 1 then MultiPart.P M (M.t + 1) else B

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
M : MultiPart α
h : Disjoint M.A B
v : α
hv : v ∈ B
⊢ v ∈ if M.t + 1 ≠ M.t + 1 then MultiPart.P M (M.t + 1) else B
Tactic:
split_ifs with h_1
State after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
M : MultiPart α
h : Disjoint M.A B
v : α
hv : v ∈ B
h_1 : M.t + 1 ≠ M.t + 1
⊢ v ∈ MultiPart.P M (M.t + 1)

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
M : MultiPart α
h : Disjoint M.A B
v : α
hv : v ∈ B
h_1 : ¬M.t + 1 ≠ M.t + 1
⊢ v ∈ B

State before:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
M : MultiPart α
h : Disjoint M.A B
v : α
hv : v ∈ B
h_1 : M.t + 1 ≠ M.t + 1
⊢ v ∈ MultiPart.P M (M.t + 1)
Tactic:
contradiction
State after:
no goals

State before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
M : MultiPart α
h : Disjoint M.A B
v : α
hv : v ∈ B
h_1 : ¬M.t + 1 ≠ M.t + 1
⊢ v ∈ B
Tactic:
exact hv
State after:
no goals