Theorem: SimpleGraph.isClique_insert (Turan4/CliqueFreeSets.lean)

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
⊢ IsClique G (insert v ↑B)
Tactic:
intro x hx y hy hne
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x : α
hx : x ∈ insert v ↑B
y : α
hy : y ∈ insert v ↑B
hne : x ≠ y
⊢ Adj G x y

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x : α
hx : x ∈ insert v ↑B
y : α
hy : y ∈ insert v ↑B
hne : x ≠ y
⊢ Adj G x y
Tactic:
cases hx with
| inl hx => 
  cases hy with
  | inl hy => rw [hx,hy] at hne; contradiction
  | inr hy => 
    rw [hx]; 
    apply G.subset_res_nbhd hB hy
| inr hx => 
  cases hy with
  | inl hy => 
    rw [hy, G.adj_comm]
    apply G.subset_res_nbhd hB hx
  | inr hy => exact h hx hy hne
State after:
no goals

State before:
case inl
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x y : α
hy : y ∈ insert v ↑B
hne : x ≠ y
hx : x = v
⊢ Adj G x y
Tactic:
cases hy with
| inl hy => rw [hx,hy] at hne; contradiction
| inr hy => 
  rw [hx]; 
  apply G.subset_res_nbhd hB hy
State after:
no goals

State before:
case inl.inl
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x y : α
hne : x ≠ y
hx : x = v
hy : y = v
⊢ Adj G x y
Tactic:
rw [hx,hy] at hne
State after:
case inl.inl
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x y : α
hne : v ≠ v
hx : x = v
hy : y = v
⊢ Adj G x y

State before:
case inl.inl
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x y : α
hne : v ≠ v
hx : x = v
hy : y = v
⊢ Adj G x y
Tactic:
contradiction
State after:
no goals

State before:
case inl.inr
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x y : α
hne : x ≠ y
hx : x = v
hy : y ∈ ↑B
⊢ Adj G x y
Tactic:
rw [hx]
State after:
case inl.inr
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x y : α
hne : x ≠ y
hx : x = v
hy : y ∈ ↑B
⊢ Adj G v y

State before:
case inl.inr
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x y : α
hne : x ≠ y
hx : x = v
hy : y ∈ ↑B
⊢ Adj G v y
Tactic:
apply G.subset_res_nbhd hB hy
State after:
no goals

State before:
case inr
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x y : α
hy : y ∈ insert v ↑B
hne : x ≠ y
hx : x ∈ ↑B
⊢ Adj G x y
Tactic:
cases hy with
| inl hy => 
  rw [hy, G.adj_comm]
  apply G.subset_res_nbhd hB hx
| inr hy => exact h hx hy hne
State after:
no goals

State before:
case inr.inl
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x y : α
hne : x ≠ y
hx : x ∈ ↑B
hy : y = v
⊢ Adj G x y
Tactic:
rw [hy, G.adj_comm]
State after:
case inr.inl
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x y : α
hne : x ≠ y
hx : x ∈ ↑B
hy : y = v
⊢ Adj G v x

State before:
case inr.inl
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x y : α
hne : x ≠ y
hx : x ∈ ↑B
hy : y = v
⊢ Adj G v x
Tactic:
apply G.subset_res_nbhd hB hx
State after:
no goals

State before:
case inr.inr
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x y : α
hne : x ≠ y
hx : x ∈ ↑B
hy : y ∈ ↑B
⊢ Adj G x y
Tactic:
exact h hx hy hne
State after:
no goals