ι : Sort ?u.300641
𝕜 : Type ?u.300644
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : Adj G v w
⊢ card (Set.toFinset (commonNeighbors G v w)) < degree G v
ι : Sort ?u.300641
𝕜 : Type ?u.300644
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : Adj G v w
⊢ Fintype.card ↑(commonNeighbors G v w) < degree G v
erw [← Set.toFinset_card]
case h
ι : Sort ?u.300641
𝕜 : Type ?u.300644
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : Adj G v w
⊢ Set.toFinset (commonNeighbors G v w) ⊂ neighborFinset G v
ι : Sort ?u.300641
𝕜 : Type ?u.300644
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : Adj G v w
⊢ card (Set.toFinset (commonNeighbors G v w)) < degree G v
apply Finset.card_lt_card
case h
ι : Sort ?u.300641
𝕜 : Type ?u.300644
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : Adj G v w
⊢ ∃ a x, insert a (Set.toFinset (commonNeighbors G v w)) ⊆ neighborFinset G v
case h
ι : Sort ?u.300641
𝕜 : Type ?u.300644
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : Adj G v w
⊢ Set.toFinset (commonNeighbors G v w) ⊂ neighborFinset G v
rw [Finset.ssubset_iff]
case h
ι : Sort ?u.300641
𝕜 : Type ?u.300644
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : Adj G v w
⊢ ∃ x, insert w (Set.toFinset (commonNeighbors G v w)) ⊆ neighborFinset G v
case h
ι : Sort ?u.300641
𝕜 : Type ?u.300644
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : Adj G v w
⊢ ∃ a x, insert a (Set.toFinset (commonNeighbors G v w)) ⊆ neighborFinset G v
use w
case h.h
ι : Sort ?u.300641
𝕜 : Type ?u.300644
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : Adj G v w
⊢ insert w (Set.toFinset (commonNeighbors G v w)) ⊆ neighborFinset G v

case h.w
ι : Sort ?u.300641
𝕜 : Type ?u.300644
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : Adj G v w
⊢ ¬w ∈ Set.toFinset (commonNeighbors G v w)
case h
ι : Sort ?u.300641
𝕜 : Type ?u.300644
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : Adj G v w
⊢ ∃ x, insert w (Set.toFinset (commonNeighbors G v w)) ⊆ neighborFinset G v
constructor
case h.h
ι : Sort ?u.300641
𝕜 : Type ?u.300644
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : Adj G v w
⊢ w ∈ neighborFinset G v ∧ Set.toFinset (commonNeighbors G v w) ⊆ neighborFinset G v
case h.h
ι : Sort ?u.300641
𝕜 : Type ?u.300644
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : Adj G v w
⊢ insert w (Set.toFinset (commonNeighbors G v w)) ⊆ neighborFinset G v
rw [Finset.insert_subset]
case h.h.left
ι : Sort ?u.300641
𝕜 : Type ?u.300644
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : Adj G v w
⊢ w ∈ neighborFinset G v

case h.h.right
ι : Sort ?u.300641
𝕜 : Type ?u.300644
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : Adj G v w
⊢ Set.toFinset (commonNeighbors G v w) ⊆ neighborFinset G v
case h.h
ι : Sort ?u.300641
𝕜 : Type ?u.300644
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : Adj G v w
⊢ w ∈ neighborFinset G v ∧ Set.toFinset (commonNeighbors G v w) ⊆ neighborFinset G v
constructor
no goals
case h.h.left
ι : Sort ?u.300641
𝕜 : Type ?u.300644
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : Adj G v w
⊢ w ∈ neighborFinset G v
simpa
case h.h.right
ι : Sort ?u.300641
𝕜 : Type ?u.300644
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : Adj G v w
⊢ commonNeighbors G v w ⊆ neighborSet G v
case h.h.right
ι : Sort ?u.300641
𝕜 : Type ?u.300644
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : Adj G v w
⊢ Set.toFinset (commonNeighbors G v w) ⊆ neighborFinset G v
rw [neighborFinset, Set.toFinset_subset_toFinset]
no goals
case h.h.right
ι : Sort ?u.300641
𝕜 : Type ?u.300644
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : Adj G v w
⊢ commonNeighbors G v w ⊆ neighborSet G v
exact G.commonNeighbors_subset_neighborSet_left _ _
case h.w
ι : Sort ?u.300641
𝕜 : Type ?u.300644
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : Adj G v w
⊢ ¬w ∈ commonNeighbors G v w
case h.w
ι : Sort ?u.300641
𝕜 : Type ?u.300644
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : Adj G v w
⊢ ¬w ∈ Set.toFinset (commonNeighbors G v w)
rw [Set.mem_toFinset]
no goals
case h.w
ι : Sort ?u.300641
𝕜 : Type ?u.300644
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : Adj G v w
⊢ ¬w ∈ commonNeighbors G v w
apply not_mem_commonNeighbors_right