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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
⊢ i ≠ j → Adj (mp M) v w
Tactic:
intro h
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
h : i ≠ j
⊢ Adj (mp M) v w

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
h : i ≠ j
⊢ Adj (mp M) v w
Tactic:
refine' ⟨i, hi, j, hj, h, _⟩
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
h : i ≠ j
⊢ v ∈ MultiPart.P M i ∧ w ∈ MultiPart.P M j ∨ v ∈ MultiPart.P M j ∧ w ∈ MultiPart.P M i

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
h : i ≠ j
⊢ v ∈ MultiPart.P M i ∧ w ∈ MultiPart.P M j ∨ v ∈ MultiPart.P M j ∧ w ∈ MultiPart.P M i
Tactic:
left
State after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
h : i ≠ j
⊢ v ∈ MultiPart.P M i ∧ w ∈ MultiPart.P M j

State before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
h : i ≠ j
⊢ v ∈ MultiPart.P M i ∧ w ∈ MultiPart.P M j
Tactic:
exact ⟨hvi, hwj⟩
State after:
no goals