Theorem: SimpleGraph.kill_of_not_isContained (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 γ
hGH : ¬G ⊑ H
⊢ G.kill H = H
Tactic:
obtain rfl | hG := eq_or_ne G ⊥
State after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hGH : ¬⊥ ⊑ H
⊢ ⊥.kill H = H

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hGH : ¬G ⊑ H
hG : G ≠ ⊥
⊢ G.kill H = H

State before:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hGH : ¬⊥ ⊑ H
⊢ ⊥.kill H = H
Tactic:
exact bot_kill _
State after:
no goals

State before:
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hGH : ¬G ⊑ H
hG : G ≠ ⊥
⊢ G.kill H = H
Tactic:
exact (kill_eq_right hG).2 hGH
State after:
no goals