-- Mathlib/Combinatorics/SimpleGraph/Operations.lean
theorem card_edgeFinset_replaceVertex_of_not_adj (hn : ¬G.Adj s t) :
    #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + G.degree s - G.degree t

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

Tactic:
rw [G.edgeFinset_replaceVertex_of_not_adj hn,
  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
hn : ¬G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #G.edgeFinset + #(image (fun x => s(x, t)) (G.neighborFinset s)) - G.degree t =
    #G.edgeFinset + G.degree s - G.degree t

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

Tactic:
simp [incidenceFinset, incidenceSet_subset]

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
hn : ¬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
hn : ¬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:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hn : ¬G.Adj s t
⊢ #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + G.degree s - G.degree t

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
hn : ¬G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + G.degree s - G.degree t

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
hn : ¬G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #(image (fun x => s(x, t)) (G.neighborFinset s)) = 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
hn : ¬G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ Function.Injective fun x => s(x, t)

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
hn : ¬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:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hn : ¬G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #G.edgeFinset + #(image (fun x => s(x, t)) (G.neighborFinset s)) - G.degree t =
    #G.edgeFinset + G.degree s - G.degree t

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
hn : ¬G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #(image (fun x => s(x, t)) (G.neighborFinset s)) = G.degree s