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

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

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

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

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

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

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