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

State before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
⊢ CliqueFree G 2 → 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 : CliqueFree G 2
⊢ G = ⊥

State before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : CliqueFree G 2
⊢ G = ⊥
Tactic:
contrapose h
State after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ¬G = ⊥
⊢ ¬CliqueFree G 2

State before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ¬G = ⊥
⊢ ¬CliqueFree G 2
Tactic:
obtain ⟨v, w, had⟩ := edge_of_not_empty h
State after:
case intro.intro
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ¬G = ⊥
v w : α
had : v ≠ w ∧ Adj G v w
⊢ ¬CliqueFree G 2

State before:
case intro.intro
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ¬G = ⊥
v w : α
had : v ≠ w ∧ Adj G v w
⊢ ¬CliqueFree G 2
Tactic:
intro hf
State after:
case intro.intro
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ¬G = ⊥
v w : α
had : v ≠ w ∧ Adj G v w
hf : CliqueFree G 2
⊢ False

State before:
case intro.intro
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ¬G = ⊥
v w : α
had : v ≠ w ∧ Adj G v w
hf : CliqueFree G 2
⊢ False
Tactic:
apply hf _ (adj_is2Clique had.2)
State after:
no goals