Theorem: SimpleGraph.mp_adj_imp (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
⊢ Adj (mp M) v w → i ≠ j
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 : Adj (mp M) v w
⊢ i ≠ j

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 : Adj (mp M) v w
⊢ i ≠ j
Tactic:
cases' h with a ha
State after:
case intro
α : 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
a : ℕ
ha :
  a ∈ range (M.t + 1) ∧
    ∃ j,
      j ∈ range (M.t + 1) ∧
        a ≠ j ∧ (v ∈ MultiPart.P M a ∧ w ∈ MultiPart.P M j ∨ v ∈ MultiPart.P M j ∧ w ∈ MultiPart.P M a)
⊢ i ≠ j

State before:
case intro
α : 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
a : ℕ
ha :
  a ∈ range (M.t + 1) ∧
    ∃ j,
      j ∈ range (M.t + 1) ∧
        a ≠ j ∧ (v ∈ MultiPart.P M a ∧ w ∈ MultiPart.P M j ∨ v ∈ MultiPart.P M j ∧ w ∈ MultiPart.P M a)
⊢ i ≠ j
Tactic:
obtain ⟨har, b, hbr, abne, ab⟩ := ha
State after:
case intro.intro.intro.intro.intro
α : 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
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : a ≠ b
ab : v ∈ MultiPart.P M a ∧ w ∈ MultiPart.P M b ∨ v ∈ MultiPart.P M b ∧ w ∈ MultiPart.P M a
⊢ i ≠ j

State before:
case intro.intro.intro.intro.intro
α : 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
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : a ≠ b
ab : v ∈ MultiPart.P M a ∧ w ∈ MultiPart.P M b ∨ v ∈ MultiPart.P M b ∧ w ∈ MultiPart.P M a
⊢ i ≠ j
Tactic:
cases ab with
| inl ab => 
  have ai := uniq_part hi har hvi ab.1; have bj := uniq_part hj hbr hwj ab.2
  rwa [← ai, ← bj] at abne 
| inr ab => 
  have aj := uniq_part hj har hwj ab.2; have bi := uniq_part hi hbr hvi ab.1
  rw [← aj, ← bi] at abne 
  exact abne.symm
State after:
no goals

State before:
case intro.intro.intro.intro.intro.inl
α : 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
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : a ≠ b
ab : v ∈ MultiPart.P M a ∧ w ∈ MultiPart.P M b
⊢ i ≠ j
Tactic:
have ai := uniq_part hi har hvi ab.1
State after:
case intro.intro.intro.intro.intro.inl
α : 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
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : a ≠ b
ab : v ∈ MultiPart.P M a ∧ w ∈ MultiPart.P M b
ai : i = a
⊢ i ≠ j

State before:
case intro.intro.intro.intro.intro.inl
α : 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
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : a ≠ b
ab : v ∈ MultiPart.P M a ∧ w ∈ MultiPart.P M b
ai : i = a
⊢ i ≠ j
Tactic:
have bj := uniq_part hj hbr hwj ab.2
State after:
case intro.intro.intro.intro.intro.inl
α : 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
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : a ≠ b
ab : v ∈ MultiPart.P M a ∧ w ∈ MultiPart.P M b
ai : i = a
bj : j = b
⊢ i ≠ j

State before:
case intro.intro.intro.intro.intro.inl
α : 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
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : a ≠ b
ab : v ∈ MultiPart.P M a ∧ w ∈ MultiPart.P M b
ai : i = a
bj : j = b
⊢ i ≠ j
Tactic:
rwa [← ai, ← bj] at abne
State after:
no goals

State before:
case intro.intro.intro.intro.intro.inr
α : 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
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : a ≠ b
ab : v ∈ MultiPart.P M b ∧ w ∈ MultiPart.P M a
⊢ i ≠ j
Tactic:
have aj := uniq_part hj har hwj ab.2
State after:
case intro.intro.intro.intro.intro.inr
α : 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
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : a ≠ b
ab : v ∈ MultiPart.P M b ∧ w ∈ MultiPart.P M a
aj : j = a
⊢ i ≠ j

State before:
case intro.intro.intro.intro.intro.inr
α : 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
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : a ≠ b
ab : v ∈ MultiPart.P M b ∧ w ∈ MultiPart.P M a
aj : j = a
⊢ i ≠ j
Tactic:
have bi := uniq_part hi hbr hvi ab.1
State after:
case intro.intro.intro.intro.intro.inr
α : 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
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : a ≠ b
ab : v ∈ MultiPart.P M b ∧ w ∈ MultiPart.P M a
aj : j = a
bi : i = b
⊢ i ≠ j

State before:
case intro.intro.intro.intro.intro.inr
α : 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
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : a ≠ b
ab : v ∈ MultiPart.P M b ∧ w ∈ MultiPart.P M a
aj : j = a
bi : i = b
⊢ i ≠ j
Tactic:
rw [← aj, ← bi] at abne
State after:
case intro.intro.intro.intro.intro.inr
α : 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
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : j ≠ i
ab : v ∈ MultiPart.P M b ∧ w ∈ MultiPart.P M a
aj : j = a
bi : i = b
⊢ i ≠ j

State before:
case intro.intro.intro.intro.intro.inr
α : 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
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : j ≠ i
ab : v ∈ MultiPart.P M b ∧ w ∈ MultiPart.P M a
aj : j = a
bi : i = b
⊢ i ≠ j
Tactic:
exact abne.symm
State after:
no goals