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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v w : α
M : MultiPart α
⊢ Adj (mp M) v w → v ∈ M.A
Tactic:
intro h1
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v w : α
M : MultiPart α
h1 : Adj (mp M) v w
⊢ v ∈ M.A

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v w : α
M : MultiPart α
h1 : Adj (mp M) v w
⊢ v ∈ M.A
Tactic:
by_contra h
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v w : α
M : MultiPart α
h1 : Adj (mp M) v w
h : ¬v ∈ M.A
⊢ False

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v w : α
M : MultiPart α
h1 : Adj (mp M) v w
h : ¬v ∈ M.A
⊢ False
Tactic:
exact no_nbhrs h h1
State after:
no goals