-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem Adj.card_commonNeighbors_lt_degree {G : SimpleGraph V} [DecidableRel G.Adj] {v w : V}
    (h : G.Adj v w) : Fintype.card (G.commonNeighbors v w) < G.degree v

Proof state:
case h.right.left
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ w ∈ G.neighborFinset v

Tactic:
simpa

Result:
no goals

Proof state:
case h.left
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ w ∉ (G.commonNeighbors v w).toFinset

Tactic:
rw [Set.mem_toFinset]

Result:
case h.left
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ w ∉ G.commonNeighbors v w

Proof state:
case h
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ (G.commonNeighbors v w).toFinset ⊂ G.neighborFinset v

Tactic:
rw [Finset.ssubset_iff]

Result:
case h
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ ∃ a ∉ (G.commonNeighbors v w).toFinset, insert a (G.commonNeighbors v w).toFinset ⊆ G.neighborFinset v

Proof state:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ #(G.commonNeighbors v w).toFinset < G.degree v

Tactic:
apply Finset.card_lt_card

Result:
case h
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ (G.commonNeighbors v w).toFinset ⊂ G.neighborFinset v

Proof state:
case h.right
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ w ∈ G.neighborFinset v ∧ (G.commonNeighbors v w).toFinset ⊆ G.neighborFinset v

Tactic:
constructor

Result:
case h.right.left
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ w ∈ G.neighborFinset v

case h.right.right
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ (G.commonNeighbors v w).toFinset ⊆ G.neighborFinset v

Proof state:
case h
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ w ∉ (G.commonNeighbors v w).toFinset ∧ insert w (G.commonNeighbors v w).toFinset ⊆ G.neighborFinset v

Tactic:
constructor

Result:
case h.left
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ w ∉ (G.commonNeighbors v w).toFinset

case h.right
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ insert w (G.commonNeighbors v w).toFinset ⊆ G.neighborFinset v

Proof state:
case h.right.right
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ (G.commonNeighbors v w).toFinset ⊆ G.neighborFinset v

Tactic:
rw [neighborFinset, Set.toFinset_subset_toFinset]

Result:
case h.right.right
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ G.commonNeighbors v w ⊆ G.neighborSet v

Proof state:
case h
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ ∃ a ∉ (G.commonNeighbors v w).toFinset, insert a (G.commonNeighbors v w).toFinset ⊆ G.neighborFinset v

Tactic:
use w

Result:
case h
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ w ∉ (G.commonNeighbors v w).toFinset ∧ insert w (G.commonNeighbors v w).toFinset ⊆ G.neighborFinset v

Proof state:
case h.left
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ w ∉ G.commonNeighbors v w

Tactic:
apply not_mem_commonNeighbors_right

Result:
no goals

Proof state:
case h.right.right
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ G.commonNeighbors v w ⊆ G.neighborSet v

Tactic:
exact G.commonNeighbors_subset_neighborSet_left _ _

Result:
no goals

Proof state:
case h.right
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ insert w (G.commonNeighbors v w).toFinset ⊆ G.neighborFinset v

Tactic:
rw [Finset.insert_subset_iff]

Result:
case h.right
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ w ∈ G.neighborFinset v ∧ (G.commonNeighbors v w).toFinset ⊆ G.neighborFinset v

Proof state:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ Fintype.card ↑(G.commonNeighbors v w) < G.degree v

Tactic:
rw [← Set.toFinset_card]

Result:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ #(G.commonNeighbors v w).toFinset < G.degree v