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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v w : α
M : MultiPart α
hA : ¬v ∈ M.A
⊢ ¬Adj (mp M) v w
Tactic:
contrapose! hA
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v w : α
M : MultiPart α
hA :
  ∃ i,
    i ∈ range (M.t + 1) ∧
      ∃ j,
        j ∈ range (M.t + 1) ∧
          i ≠ j ∧ (v ∈ MultiPart.P M i ∧ w ∈ MultiPart.P M j ∨ v ∈ MultiPart.P M j ∧ w ∈ MultiPart.P M i)
⊢ v ∈ M.A

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v w : α
M : MultiPart α
hA :
  ∃ i,
    i ∈ range (M.t + 1) ∧
      ∃ j,
        j ∈ range (M.t + 1) ∧
          i ≠ j ∧ (v ∈ MultiPart.P M i ∧ w ∈ MultiPart.P M j ∨ v ∈ MultiPart.P M j ∧ w ∈ MultiPart.P M i)
⊢ v ∈ M.A
Tactic:
obtain ⟨i, hi, j, hj, _, hv⟩ := hA
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v w : α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
left✝ : i ≠ j
hv : v ∈ MultiPart.P M i ∧ w ∈ MultiPart.P M j ∨ v ∈ MultiPart.P M j ∧ w ∈ MultiPart.P M i
⊢ v ∈ M.A

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v w : α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
left✝ : i ≠ j
hv : v ∈ MultiPart.P M i ∧ w ∈ MultiPart.P M j ∨ v ∈ MultiPart.P M j ∧ w ∈ MultiPart.P M i
⊢ v ∈ M.A
Tactic:
cases hv with
| inl hv => exact (sub_part hi) hv.1
| inr hv =>  exact (sub_part hj) hv.1
State after:
no goals

State before:
case intro.intro.intro.intro.intro.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v w : α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
left✝ : i ≠ j
hv : v ∈ MultiPart.P M i ∧ w ∈ MultiPart.P M j
⊢ v ∈ M.A
Tactic:
exact (sub_part hi) hv.1
State after:
no goals

State before:
case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v w : α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
left✝ : i ≠ j
hv : v ∈ MultiPart.P M j ∧ w ∈ MultiPart.P M i
⊢ v ∈ M.A
Tactic:
exact (sub_part hj) hv.1
State after:
no goals