-- Mathlib/Combinatorics/SimpleGraph/Operations.lean
theorem card_edgeFinset_replaceVertex_of_adj (ha : G.Adj s t) :
    #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + G.degree s - G.degree t - 1

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ {s(t, t)} ⊆ G.edgeFinset \ G.incidenceFinset t ∪ image (fun x => s(x, t)) (G.neighborFinset s)

Tactic:
simp [ha]

Result:
no goals

Proof state:
case e_a.e_a.H
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ Function.Injective fun x => s(x, t)

Tactic:
unfold Function.Injective

Result:
case e_a.e_a.H
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ ∀ ⦃a₁ a₂ : V⦄, (fun x => s(x, t)) a₁ = (fun x => s(x, t)) a₂ → a₁ = a₂

Proof state:
case e_a.e_a.H
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ ∀ ⦃a₁ a₂ : V⦄, (fun x => s(x, t)) a₁ = (fun x => s(x, t)) a₂ → a₁ = a₂

Tactic:
aesop

Result:
no goals

Proof state:
case e_a.e_a
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #G.edgeFinset + #(image (fun x => s(x, t)) (G.neighborFinset s)) = #G.edgeFinset + G.degree s

Tactic:
rw [card_image_of_injective, card_neighborFinset_eq_degree]

Result:
case e_a.e_a.H
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ Function.Injective fun x => s(x, t)

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + G.degree s - G.degree t - 1

Tactic:
rw [G.edgeFinset_replaceVertex_of_adj ha, card_sdiff (by simp [ha]),
  card_union_of_disjoint G.disjoint_sdiff_neighborFinset_image, card_sdiff inc,
  ← Nat.sub_add_comm <| card_le_card inc, card_incidenceFinset_eq_degree]

Result:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #G.edgeFinset + #(image (fun x => s(x, t)) (G.neighborFinset s)) - G.degree t - #{s(t, t)} =
    #G.edgeFinset + G.degree s - G.degree t - 1

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #G.edgeFinset + #(image (fun x => s(x, t)) (G.neighborFinset s)) - G.degree t - #{s(t, t)} =
    #G.edgeFinset + G.degree s - G.degree t - 1

Tactic:
congr 2

Result:
case e_a.e_a
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #G.edgeFinset + #(image (fun x => s(x, t)) (G.neighborFinset s)) = #G.edgeFinset + G.degree s

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
ha : G.Adj s t
⊢ G.incidenceFinset t ⊆ G.edgeFinset

Tactic:
simp [incidenceFinset, incidenceSet_subset]

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
ha : G.Adj s t
⊢ #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + G.degree s - G.degree t - 1

Tactic:
have inc : G.incidenceFinset t ⊆ G.edgeFinset := by simp [incidenceFinset, incidenceSet_subset]

Result:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + G.degree s - G.degree t - 1