Theorem: SimpleGraph.kill_eq_right (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 ≠ ⊥
⊢ G.kill H = H ↔ ¬G ⊑ H
Tactic:
simp only [kill_of_ne_bot hG, Set.disjoint_left, isContained_iff_exists_subgraph,
  @forall_swap _ H.Subgraph, Set.iUnion_singleton_eq_range, deleteEdges_eq_self, Set.mem_iUnion,
  Set.mem_range, not_exists, not_nonempty_iff, Nonempty.forall]
State after:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
⊢ (∀ (y : H.Subgraph), ∀ x ∈ H.edgeSet, ∀ (a : G ≃g y.coe), x ∉ {⋯.some}) ↔ ∀ (x : H.Subgraph), IsEmpty (G ≃g x.coe)

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
⊢ (∀ (y : H.Subgraph), ∀ x ∈ H.edgeSet, ∀ (a : G ≃g y.coe), x ∉ {⋯.some}) ↔ ∀ (x : H.Subgraph), IsEmpty (G ≃g x.coe)
Tactic:
exact forall_congr' fun H' ↦ ⟨fun h ↦ ⟨fun f ↦ h _
  (Subgraph.edgeSet_subset _ $ (aux hG ⟨f⟩).choose_spec) f rfl⟩, fun h _ _ ↦ h.elim⟩
State after:
no goals