Theorem: SimpleGraph.kill_le (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 γ
⊢ G.kill H ≤ H
Tactic:
rw [kill]
State after:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
⊢ (if hG : G = ⊥ then H else H.deleteEdges (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})) ≤ H

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

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
h✝ : ¬G = ⊥
⊢ H.deleteEdges (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some}) ≤ H

State before:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
h✝ : G = ⊥
⊢ H ≤ H

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
h✝ : ¬G = ⊥
⊢ H.deleteEdges (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some}) ≤ H
Tactic:
exacts [le_rfl, deleteEdges_le _]
State after:
no goals