Theorem: SimpleGraph.edge_of_not_empty (Turan4/Fedges.lean)

State before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
⊢ G ≠ ⊥ → ∃ v w, v ≠ w ∧ Adj G v w
Tactic:
contrapose
State after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
⊢ (¬∃ v w, v ≠ w ∧ Adj G v w) → ¬G ≠ ⊥

State before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
⊢ (¬∃ v w, v ≠ w ∧ Adj G v w) → ¬G ≠ ⊥
Tactic:
intro h
State after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ¬∃ v w, v ≠ w ∧ Adj G v w
⊢ ¬G ≠ ⊥

State before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ¬∃ v w, v ≠ w ∧ Adj G v w
⊢ ¬G ≠ ⊥
Tactic:
push_neg at h
State after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ∀ (v w : α), v ≠ w → ¬Adj G v w
⊢ ¬G ≠ ⊥

State before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ∀ (v w : α), v ≠ w → ¬Adj G v w
⊢ ¬G ≠ ⊥
Tactic:
push_neg
State after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ∀ (v w : α), v ≠ w → ¬Adj G v w
⊢ G = ⊥

State before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ∀ (v w : α), v ≠ w → ¬Adj G v w
⊢ G = ⊥
Tactic:
ext x x_1
State after:
case Adj.h.h.a
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ∀ (v w : α), v ≠ w → ¬Adj G v w
x x_1 : α
⊢ Adj G x x_1 ↔ Adj ⊥ x x_1

State before:
case Adj.h.h.a
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ∀ (v w : α), v ≠ w → ¬Adj G v w
x x_1 : α
⊢ Adj G x x_1 ↔ Adj ⊥ x x_1
Tactic:
rw [bot_adj]
State after:
case Adj.h.h.a
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ∀ (v w : α), v ≠ w → ¬Adj G v w
x x_1 : α
⊢ Adj G x x_1 ↔ False

State before:
case Adj.h.h.a
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ∀ (v w : α), v ≠ w → ¬Adj G v w
x x_1 : α
⊢ Adj G x x_1 ↔ False
Tactic:
specialize h x x_1
State after:
case Adj.h.h.a
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
x x_1 : α
h : x ≠ x_1 → ¬Adj G x x_1
⊢ Adj G x x_1 ↔ False

State before:
case Adj.h.h.a
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
x x_1 : α
h : x ≠ x_1 → ¬Adj G x x_1
⊢ Adj G x x_1 ↔ False
Tactic:
by_cases h' : x = x_1
State after:
case pos
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
x x_1 : α
h : x ≠ x_1 → ¬Adj G x x_1
h' : x = x_1
⊢ Adj G x x_1 ↔ False

case neg
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
x x_1 : α
h : x ≠ x_1 → ¬Adj G x x_1
h' : ¬x = x_1
⊢ Adj G x x_1 ↔ False

State before:
case pos
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
x x_1 : α
h : x ≠ x_1 → ¬Adj G x x_1
h' : x = x_1
⊢ Adj G x x_1 ↔ False

case neg
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
x x_1 : α
h : x ≠ x_1 → ¬Adj G x x_1
h' : ¬x = x_1
⊢ Adj G x x_1 ↔ False
Tactic:
simp only [h,h', G.irrefl]
State after:
case neg
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
x x_1 : α
h : x ≠ x_1 → ¬Adj G x x_1
h' : ¬x = x_1
⊢ Adj G x x_1 ↔ False

State before:
case neg
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
x x_1 : α
h : x ≠ x_1 → ¬Adj G x x_1
h' : ¬x = x_1
⊢ Adj G x x_1 ↔ False
Tactic:
have := h h'
State after:
case neg
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
x x_1 : α
h : x ≠ x_1 → ¬Adj G x x_1
h' : ¬x = x_1
this : ¬Adj G x x_1
⊢ Adj G x x_1 ↔ False

State before:
case neg
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
x x_1 : α
h : x ≠ x_1 → ¬Adj G x x_1
h' : ¬x = x_1
this : ¬Adj G x x_1
⊢ Adj G x x_1 ↔ False
Tactic:
tauto
State after:
no goals