Theorem: SimpleGraph.not_nbhr_same_part (Turan4/Multipartite.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
⊢ Adj (mp M) v w → ¬w ∈ MultiPart.P M i
Tactic:
intro h1
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
h1 : Adj (mp M) v w
⊢ ¬w ∈ MultiPart.P M i

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
h1 : Adj (mp M) v w
⊢ ¬w ∈ MultiPart.P M i
Tactic:
by_contra h
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
h1 : Adj (mp M) v w
h : w ∈ MultiPart.P M i
⊢ False

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
h1 : Adj (mp M) v w
h : w ∈ MultiPart.P M i
⊢ False
Tactic:
apply mp_adj_imp hi hi hv h h1
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
h1 : Adj (mp M) v w
h : w ∈ MultiPart.P M i
⊢ i = i

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
h1 : Adj (mp M) v w
h : w ∈ MultiPart.P M i
⊢ i = i
Tactic:
rfl
State after:
no goals