rw [kill]
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
H : SimpleGraph β
⊢ ⊥.kill H = H
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
H : SimpleGraph β
⊢ (if hG : ⊥ = ⊥ then H else H.deleteEdges (⋃ H', ⋃ (hH' : Nonempty (⊥ ≃g H'.coe)), {⋯.some})) = H