Theorem: SimpleGraph.kill_of_ne_bot (LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Containment.lean)

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

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H : SimpleGraph β
⊢ (if hG : G = ⊥ then H else H.deleteEdges (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})) =
    H.deleteEdges (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})
Tactic:
exact dif_neg hG
State after:
no goals